Lógica de predicados: ¿Cómo autoverificas la estructura lógica de tus propios argumentos?

Las tablas de verdad no son suficientes para capturar la lógica de primer orden (con cuantificadores), por lo que usamos reglas de inferencia en su lugar. Cada regla de inferencia se elige para que sea sólida, lo que significa que si comienza con declaraciones verdaderas y usa la regla, deducirá solo declaraciones verdaderas. Decimos que estas reglas preservan la verdad. Si elige con suficiente cuidado, puede hacer que las reglas no solo preserven la verdad, sino que también le permitan deducir cada declaración (bien formada) que sea necesariamente verdadera (en todas las situaciones).

Lo que probablemente esté buscando (es decir, una forma práctica de verificar rigurosamente la validez lógica de sus argumentos) es la deducción natural. Hay muchos estilos diferentes, el tipo más intuitivo es el estilo Fitch , que marca los subcontextos usando sangría o alguna demarcación visual relacionada. El siguiente sistema usa sangría y sigue la intuición más de cerca en mi opinión.$\def\block#1{\begin{array}{ll}\ &{#1}\end{array}} \def\fitch#1#2{\begin{array}{|l}#1\\\hline#2\end{array}} \def\sub#1#2{\text{#1}:\\\block{#2}} \def\imp{\Rightarrow} \def\eq{\Leftrightarrow} \def\nn{\mathbb{N}} \def\none{\varnothing} \def\pow{\mathcal{P}}$

---

Contextos

Cada línea es un encabezado o una declaración. Pondremos dos puntos después de cada encabezado y un punto después de cada declaración. Cada encabezado especifica algún subcontexto (contenido por el contexto actual), y las líneas gobernadas por ese encabezado se indican mediante la sangría. El contexto completo de cada línea está especificado por todos los encabezados que la gobiernan (es decir, todos los encabezados más cercanos por encima de ella en cada nivel de sangría inferior).

Por ejemplo, un análisis de caso anidado podría verse así:

  $\sub{If $A$}{\sub{If $B$}{...} \\ \sub{If $¬B$}{...}} \\ \sub{If $\neg A$}{...}$

Y razonar sobre un miembro arbitrario de una colección.$S$se vería como:

  $\sub{Given $x{∈}S$}{...}$

Tenga en cuenta que lo que se afirma en algún contexto puede no ser válido en otros contextos. Una vez que comprenda el principio detrás de los contextos y la sangría, las siguientes reglas son muy naturales. También tenga en cuenta que para la lógica de primer orden, estos dos tipos de encabezados de contexto (para subcontextos condicionales y subcontextos universales, respectivamente) son los únicos tipos necesarios.

Reglas de sintaxis

Una declaración debe ser una proposición atómica (indivisible) o una declaración compuesta formada de la manera habitual usando operaciones booleanas o cuantificadores, con la restricción de que cada variable que está limitada por un cuantificador no se usa ya para referirse a algún objeto en el contexto actual. , y que no hay cuantificadores anidados que vinculen la misma variable.

Reglas de deducción natural

Cada regla de inferencia es de la forma:

  $\fitch{\text{X}}{\text{Y}}$

lo que significa que si las últimas líneas que ha escrito coinciden con "X", puede escribir "Y" inmediatamente después con el mismo nivel de sangría. Cada aplicación de una regla de inferencia también está ligada al contexto actual, a saber, el contexto de "X". No mencionaremos el "contexto actual" todo el tiempo.

---

operaciones booleanas

Toma cualquier declaración$A,B,C$(en el contexto actual).

replantear : Si probamos algo, podemos afirmarlo nuevamente en el mismo contexto.

  $\fitch{A.\\ ...}{A.}$

Tenga en cuenta que "$...$" denota cualquier número de líneas que estén al menos en el nivel de sangría representado. En la regla anterior, esto significa que todas las líneas escritas desde la escritura anterior de "$A.$" debe estar en el mismo contexto (o en algún subcontexto).

En la práctica nunca escribimos la misma línea dos veces. Para indicar que podemos omitir una línea en una prueba, la marcaré con corchetes como este:

  $\fitch{A. \\ ...}{[A.]}$

⇒sub       ⇒restate     (Podemos crear un subcontexto condicional donde$A$sostiene.)

  $\fitch{}{\sub{If $A$}{[A.]}}$   $\fitch{B. \\ ... \\ \sub{If $A$}{...}}{\block{[B.]}}$

⇒introducción       ⇒eliminación

  $\fitch{\sub{If $A$}{... \\ B.}}{[A \imp B.]}$   $\fitch{A \imp B. \\ A.}{B.}$

∧introducción     ∧eliminación

  $\fitch{A. \\ B.}{A \land B.}$   $\fitch{A \land B.}{[A.] \\ [B.]}$

∨introducción     ∨elim

  $\fitch{A.}{[A \lor B.] \\ [B \lor A.]}$   $\fitch{A \lor B. \\ A \imp C. \\ B \imp C.}{C.}$

¬introducción     ¬eliminar     ¬¬eliminar

  $\fitch{A \imp \bot.}{\neg A.}$   $\fitch{A. \\ \neg A.}{\bot.}$   $\fitch{\neg \neg A.}{A.}$

Tenga en cuenta que al usar ¬intro y ¬¬elim podemos obtener la siguiente regla de inferencia adicional:

  $\fitch{\neg A \imp \bot.}{A.}$

que corresponde a cómo uno intentaría probar$A$ por contradicción , es decir, mostrar que suponiendo$\neg A$implica una falsedad.

⇔introducción     ⇔eliminar

  $\fitch{A \imp B. \\ B \imp A.}{A \eq B.}$   $\fitch{A \eq B.}{[A \imp B.] \\ [B \imp A.]}$

Cuantificadores e igualdad

Las reglas aquí son para cuantificadores restringidos porque generalmente pensamos en términos de ellos. Primero necesitamos algunas definiciones.

Variable utilizada : una variable que se declara en el encabezado de algún contexto contenedor o se declara en algún paso anterior de eliminación ("let") de algún contexto contenedor.

Variable no utilizada : una variable que no se utiliza.

Variable nueva : una variable que no aparece en ninguna declaración anterior en ningún contexto que la contenga.

Expresión de objeto : una expresión que hace referencia a un objeto (por ejemplo, una variable utilizada o un símbolo de función aplicado a expresiones de objeto).

Propiedad con$k$parámetros : una cadena$P$con algunos espacios en blanco donde cada espacio en blanco tiene alguna etiqueta de$1$a$k$, tal que reemplazando cada espacio en blanco en$P$por alguna expresión de objeto produce una declaración. Si$k = 2$, entonces$P(E,F)$es el resultado de reemplazar cada espacio en blanco etiquetado$1$por$E$y reemplazando cada espacio en blanco etiquetado$2$por$F$. Del mismo modo para otros$k$.

En esta sección,$E,F$(si está involucrado) puede ser cualquier expresión de objeto (en el contexto actual).

Comenzamos con las siguientes reglas que proporcionan un tipo de todos los objetos.

universo :$obj$es un tipo

  $\fitch{}{[E{∈}obj.]}$

Ahora toma cualquier tipo$S$y una propiedad de 1 parámetro$P$y una variable no utilizada$x$que no aparece en$S$o$P$.

∀sub           ∀restate         (Podemos crear un ∀-subcontexto en el que$x$es de tipo$S$.)

  $\fitch{}{\sub{Given $x{∈}S$}{[x{∈}S.]}}$   $\fitch{A. \\ ... \\ \sub{Given $x{∈}S$}{...}}{\block{[A.]}}$($x$no debe aparecer en$A$)

∀introducción           ∀eliminar

  $\fitch{\sub{Given $x{∈}S$}{... \\ P(x).}}{\forall x{∈}S\ ( \ P(x) \ ).}$   $\fitch{\forall x{∈}S\ ( \ P(x) \ ). \\ E{∈}S.}{P(E).}$($E$no debe compartir ninguna variable no utilizada con$P$)

∃ introducción           ∃ elim

  $\fitch{E{∈}S. \\ P(E).}{\exists x{∈}S\ ( \ P(x) \ ).}$   $\fitch{\exists x{∈}S\ ( \ P(x) \ ).}{\text{Let $y{∈}S$ such that $P(y)$}. \\ [y{∈}S.] \\ [P(y).]}$(dónde$y$es una variable fresca)

= introducción       = eliminar

  $\fitch{}{[E=E.]}$   $\fitch{E=F. \\ P(E).}{P(F).}$($F$no debe compartir ninguna variable no utilizada con$P$)

Cambio de nombre de variables

Finalmente, las siguientes reglas para renombrar variables son redundantes, pero acortarían las demostraciones.

∀renombrar         ∃renombrar

  $\fitch{\forall x{∈}S\ ( \ P(x) \ ).}{[\forall y{∈}S\ ( \ P(y) \ ).]}$   $\fitch{\exists x{∈}S\ ( \ P(x) \ ).}{[\exists y{∈}S\ ( \ P(y) \ ).]}$

  (dónde$y$es una variable no utilizada que no aparece en$P$)

Formas cortas

Por conveniencia escribimos "$\forall x,y{∈}S\ ( \ P(x,y) \ )$" como abreviatura de "$\forall x{∈}S\ ( \ \forall y{∈}S\ ( \ P(x,y) \ ) \ )$", y de manera similar para más variables y para "$\exists$". También comprimiremos los encabezados de subcontexto ∀ anidados de la siguiente forma:

  $\sub{Given $x{∈}S$}{\sub{Given $y{∈}S$}{...}}$

a:

  $\sub{Given $x,y{∈}S$}{...}$

Además, "$\exists! x{∈}S\ ( \ P(x) \ )$" es la forma abreviada de "$\exists x{∈}S\ ( \ P(x) \land \forall y{∈}S\ ( \ P(y) \imp x=y \ ) \ )$".

---

Ejemplo

He aquí un ejemplo, donde$S,T$son de cualquier tipo y$P$es cualquier propiedad con dos parámetros.

Primero con todas las líneas mostradas:

  Si$\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ )$: [⇒sub]
    $\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ )$. [⇒sub]
    Deja$a{∈}S$tal que$\forall y{∈}T\ ( \ P(a,y) \ )$. [∃eliminar]
    $a{∈}S$. [∃eliminar]
    $\forall y{∈}T\ ( \ P(a,y) \ )$. [∃eliminar]
    $\forall z{∈}T\ ( \ P(a,z) \ )$. [∀renombrar]
    Dado$y{∈}T$: [∀sub]
      $y{∈}T$. [∀sub]
      $\forall z{∈}T\ ( \ P(a,z) \ )$. [∀reiterar]
      $y{∈}T$. [reafirmar]
      $P(a,y)$. [∀eliminar]
      $a{∈}S$. [∀reiterar]
      $\exists x{∈}S\ ( \ P(x,y) \ )$. [∃introducción]
    $\forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$. [∀introducción]
  $\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ ) \imp \forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$. [⇒introducción]

Finalmente, con todas las líneas entre corchetes eliminadas:

  Si$\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ )$: [⇒sub]
    Vamos$a{∈}S$tal que$\forall y{∈}T\ ( \ P(a,y) \ )$. [∃elim]
    Dado$y{∈}T$: [∀sub]
      $P(a,y)$. [∀eliminar]
      $\exists x{∈}S\ ( \ P(x,y) \ )$. [∃introducción]
    $\forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$. [∀introducción]
  $\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ ) \imp \forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$. [⇒introducción]

Esta prueba final está limpia pero aún es fácilmente verificable por computadora.

Expansión definitoria

Para facilitar las definiciones , que pueden acortar significativamente las demostraciones, también tenemos las siguientes reglas de expansión definitoria.

Para cada$k$-propiedad del parámetro$P$y predicado-símbolo fresco$Q$:

  $\fitch{}{\text{Let $Q(x_1,...x_k) ≡ P(x_1,...x_k)$ for each $x_1{∈}S_1$ and ... and $x_k{∈}S_k$.} \\ [∀x_1{∈}S_1\ \cdots ∀x_k{∈}S_k\ ( \ Q(x_1,...x_k) ⇔ P(x_1,...x_k) \ ).]}$

Para cada$(k+1)$-propiedad del parámetro$R$y nuevo símbolo de función$f$:

  $\fitch{∀x_1{∈}S_1 \cdots ∀x_k{∈}S_k\ ∃!y{∈}T ( \ R(x_1,...x_k,y) \ ) } {\text{Let $f : S_1{×}{\cdots}{×}S_k{→}T$ such that $R(x_1,...x_k,f(x_1,...x_k))$ for each $x_1{∈}S_1$ and ... and $x_k{∈}S_k$.} \\ [∀x_1{∈}S_1\ \cdots ∀x_k{∈}S_k\ ( \ f(x_1,...x_k)∈T ∧ R(x_1,...x_k,f(x_1,...x_k)) \ ).]}$

Estas reglas son redundantes en el sentido de que cualquier declaración que pueda probar que no use ninguno de los nuevos símbolos puede probarse sin usar la expansión definitoria.

notas

Las reglas anteriores evitan el problema habitual que tienen muchos otros sistemas, donde las variables utilizadas para testigos de declaraciones existenciales deben distinguirse de las variables utilizadas para objetos arbitrarios. La razón es que cada variable aquí está especificada por un subcontexto ∀ o por una instrucción "let"; en otras palabras, no hay variables libres. El hecho de que toda variable esté ligada está fuertemente relacionado con el hecho de que este sistema permite un universo vacío, si no hay otros axiomas.

Además, cada variable se especifica mediante un encabezado único o una declaración "let" en el contexto actual; en otras palabras, no hay sombreado variable. Esto es por diseño, y en la práctica matemática real también lo cumplimos, aunque la mayoría de los otros sistemas formales no lo hacen. En consecuencia, oraciones como "$\exists x\ \forall x\ ( x=x )$." simplemente no se puede escribir en este sistema. Si desea permitir este tipo de oraciones terribles, tendría que modificar las reglas apropiadamente, pero lo más probable es que le cause un dolor de cabeza.

Finalmente, hubo algunas decisiones técnicas sutiles. Para las reglas del cuantificador, la razón por la que exigí que$x$no aparece en$S,P$es que, si más adelante incluyéramos reglas para especificar tipos, normalmente tendríamos nombres de variables en su sintaxis, lo que daría problemas. Por ejemplo, si hemos escrito en el contexto actual "$x∈\{y:y∈S∧y∈T\}$" y "$x∈U$", no será sensato permitir la escritura"$∃y∈U\ ( y∈\{y:y∈S∧y∈T\} )$". Del mismo modo, si hemos escrito "$x=\{y:P(y)\}$" y "$∃y∈U\ ( Q(x,y) )$", no queremos permitir la escritura"$∃y∈U\ ( Q(\{y:P(y)\},y) )$".

Además, para permitir que una variable se actualice nuevamente después de dejar el subcontexto en el que fue declarada, requerí que las reglas ⇒intro e ∀intro se puedan aplicar solo inmediatamente después del ⇒-subcontext o ∀-subcontext correspondiente. Sería más sencillo simplemente definir una variable nueva como una que no aparece en ninguna línea anterior, pero luego fácilmente podemos quedarnos sin nombres de variables nuevas en una prueba larga.

~ ~ ~ ~ ~ ~ ~

Para ilustrar la flexibilidad de este sistema, expresaré tanto la Aritmética de Peano como la Teoría de conjuntos como reglas adicionales que pueden agregarse simplemente al sistema.

Aritmética Peano

Agrega el tipo$\nn$y los símbolos de PA, a saber, los símbolos constantes$0,1$y el$2$-símbolos de función de entrada$+,·$y el$2$-input predicado-símbolo$<$.

Añadir los axiomas de PA$^-$, adaptado de aquí :

• $\forall x,y{∈}\nn\ ( \ x+y ∈ \nn \ )$.
• $\forall x,y{∈}\nn\ ( \ x·y ∈ \nn \ )$.
• $\forall x,y{∈}\nn\ ( \ x+y=y+x \ )$.
• $\forall x,y{∈}\nn\ ( \ x·y=y·x \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x+(y+z)=(x+y)+z \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x·(y·z)=(x·y)·z \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x·(y+z)=x·y+x·z \ )$.
• $\forall x{∈}\nn\ ( \ x+0=x \ )$.
• $\forall x{∈}\nn\ ( \ x·1=x \ )$.
• $\forall x{∈}\nn\ ( \ \neg x<x \ )$.
• $\forall x,y{∈}\nn\ ( \ x<y \lor y<x \lor x=y \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x<y \land y<z \imp x<z \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x<y \imp x+z<y+z \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x<y \land 0<z \imp x·z<y·z \ )$.
• $\forall x,y{∈}\nn\ ( \ x<y \imp \exists z{∈}\nn\ ( \ x+z=y \ ) \ )$.
• $0<1$.
• $\forall x{∈}\nn\ ( \ 0=x \lor 1=x \lor 1<x \ )$.

Agregue los axiomas de inducción, es decir, para cada propiedad$P$involucrando solo los símbolos de PA y cuantificadores sobre$\nn$agregue el siguiente axioma (donde$k$no aparece en$P$):

• $P(0) \land \forall k{∈}\nn\ ( \ P(k) \imp P(k+1) \ ) \imp \forall k{∈}\nn\ ( \ P(k) \ )$.

Teoría de conjuntos

Agrega el tipo$set$y la regla de que todo miembro de$set$también es un tipo.

Agregue los símbolos de función unarios$\pow,\bigcup$, los símbolos de funciones binarias$×,→$, y el símbolo constante$\none$. Reutilizamos el predicado-símbolo binario$\in$, ya que no habrá ambigüedad. También agregue las siguientes reglas (en cada contexto) para la otra notación:

• Si$E,F \in obj$, entonces$(E,F) \in obj$y$\{E,F\} \in set$.
• Si$S,T \in set$, entonces$S×T \in set$y$(S{→}T) \in set$y$\pow(S) \in set$.
• Si$S,T \in set$y$f \in (S{→}T)$y$x \in S$, entonces$f(x) \in T$.
• Si$S \in set$y$\forall x{∈}S\ ( \ x \in set \ )$, entonces$\bigcup(S) \in set$.

Agregue los siguientes axiomas:

• extensionalidad :   $\forall S,T{∈}set\ ( \ S=T \eq \forall x{∈}obj\ ( \ x \in S \eq x \in T \ ) \ ).$
• conjunto vacío :   $\forall x{∈}obj\ ( \ \neg x \in \none \ ).$
• naturales :   $\nn{∈}set$.
• conjunto de potencia :   $\forall S{∈}set\ ( \ \pow(S) = \{ T : T \in set \land \forall x{∈}T\ ( \ x \in S \ ) \} ).$
• pareja :   $\forall x,y{∈}obj\ ( \ \{x,y\} = \{ z : z=x \lor z=y \} ).$
• par ordenado :   $\forall x,y{∈}obj\ \forall z,w{∈}obj\ ( \ (x,y)=(z,w) \eq x=z \land y=w \ ).$
• tipo de producto :   $\forall S,T{∈}set\ ( \ S×T = \{ t : \exists x{∈}S\ \exists y{∈}T\ ( \ t=(x,y) \ ) \} \ ).$
• tipo de función :   $\forall S,T{∈}set\ ( \ (S→T) = \\ \{ F : F \in \pow(S×T) \land \forall x{∈}S\ \exists! y{∈}T\ ( \ (x,y) \in F \ ) \} \ ).$
• función-aplicación :   $\forall S,T{∈}set\ \forall f{∈}(S{→}T)\ \forall x{∈}S\ ( \ (x,f(x)) \in f \ ).$
• unión :   $\forall S{∈}set\ ( \ \bigcup(S) = \{ x : \exists T{∈}set\ ( \ x \in T \land T \in S \ ) \} \ ).$
• elección :   $\forall S,T{∈}set\ \forall R{∈}\pow(S×T)\ ( \ \forall x{∈}S\ \exists y{∈}T\ ( \ (x,y) \in R \ ) \\ \imp \exists f{∈}(S{→}T)\ \forall x{∈}S\ ( \ (x,f(x)) \in R \ ) \ ).$

Agregue las siguientes reglas:

notación de tipo

Tomar (en el contexto actual) cualquier propiedad$P$y expresión de objetos$E$y variable no utilizada$x$.

Entonces$\{ x : P(x) \}$es un tipo y su pertenencia se rige por:

  $\fitch{}{E \in \{ x : P(x) \} \eq P(E).}$. ($x$no debe aparecer en$E$o$P$)

comprensión

Tomar cualquier propiedad$P$y variable no utilizada$x$.

  $\fitch{S \in set.}{\{ x : x \in S \land P(x) \} \in set.}$. ($x$no debe aparecer en$S$o$P$)

reemplazo

Tomar cualquiera$2$-propiedad del parámetro$P$y variables no utilizadas$x,y$.

  $\fitch{S \in set. \\ \forall x{∈}S\ \exists! y{∈}obj\ ( \ P(x,y) \ ).}{\{ y : \exists x{∈}S\ ( \ P(x,y) \ ) \} \in set.}$($x,y$no debe aparecer en$S$o$P$)

inducción

Tomar cualquier propiedad$P$con$1$parámetro de$\nn$.

  $\fitch{P(0). \\ \forall k{∈}\nn\ ( \ P(k) \imp P(k+1) \ ).}{\forall k{∈}\nn\ ( \ P(k) \ ).}$($k$no debe aparecer en$P$)

La regla de inducción subsume los axiomas de inducción para PA, y esencialmente la única diferencia es que la propiedad$P$puede involucrar operaciones de conjuntos y cuantificación sobre conjuntos.

notación de función

Esta regla es teóricamente innecesaria pero pragmáticamente muy conveniente (también conocida como expresiones lambda en informática).

Toma cualquier conjunto$S$y cualquier expresión de objeto$E$con$1$parámetro de$S$y variable no utilizada$x$.

Entonces$( S\ x \mapsto E(x) )$es un objeto y su comportamiento se rige por:

  $\fitch{\forall x{∈}S\ ( \ E(x) \in T \ ). \\ f = ( S\ x \mapsto E(x) ).}{f \in (S→T) \land \forall x{∈}S ( \ f(x) = E(x) \ ).}$

sistema fundacional

La combinación de la Aritmética de Peano anterior más la Teoría de conjuntos produce un sistema fundamental que es esencialmente tan fuerte como ZFC pero mucho más fácil de usar. También es agnóstico a la existencia de objetos que no son conjuntos, y ni siquiera asume que los miembros de$\nn$son conjuntos. También trata los productos cartesianos y los pares ordenados como nociones abstractas incorporadas. Así es como los usamos en las matemáticas reales. (Más precisamente, el sistema anterior interpreta directamente ZFC menos la regularidad).