2.5: Solidez

Los matemáticos son por naturaleza un grupo conservador. No hablamos de inclinaciones políticas o sociales, sino de su visión profesional. En particular, a un matemático le gusta saber que cuando algo ha sido probado, es cierto. En esta sección probaremos un teorema que demuestra que el sistema lógico que hemos desarrollado tiene esta propiedad altamente deseable. A este resultado se le llama Teorema de la Solidez.

Reafirmemos la lista de requisitos que establecemos para nuestros axiomas y reglas de inferencia:

1. Habrá un algoritmo que decidirá, dada una fórmula\(\theta\), si\(\theta\) es o no un axioma lógico.
2. Habrá un algoritmo que decidirá, dado un conjunto finito de fórmulas\(\Gamma\) y una fórmula\(\theta\), si\(\left( \Gamma, \theta \right)\) es o no una regla de inferencia.
3. Para cada regla de inferencia\(\left( \Gamma, \theta \right)\),\(\Gamma\) será un conjunto finito de fórmulas.
4. Cada axioma lógico será válido.
5. Nuestras reglas de inferencia preservarán la verdad. Es decir, para cada regla de inferencia\(\left( \Gamma, \theta \right)\),\(\Gamma \models \theta\).

Estos requisitos sirven para dos propósitos: Permiten verificar mecánicamente que una supuesta deducción es en realidad una deducción, y proporcionan la base del Teorema de la Solidez. Por supuesto, primero debemos verificar que el sistema de axiomas y reglas que hemos establecido en los dos apartados anteriores satisfaga estos requisitos.

Que los tres primeros requisitos anteriores son satisfechos por nuestro sistema de deducción se señaló a medida que se presentaron los axiomas y reglas. Estas son las reglas que se necesitan para la verificación de deducción. Discutiremos los dos últimos requisitos con más detalle y luego los usaremos para probar el Teorema de la Solidez.

Teorema 2.5.1. Los axiomas lógicos son válidos.

Comprobante. Debemos verificar tanto los axiomas de igualdad como los axiomas del cuantificador. Primero, considere axiomas de igualdad de tipo (E2). [(E1) y (E3) se probarán en los Ejercicios.]

Chafia: Mencionemos que vamos a utilizar el Teorema 2.6.2 en esta prueba. Si bien la presentación de ese resultado se ha retrasado para ayudar al flujo de la exposición, es posible que desee mirar ahora la afirmación de ese teorema para que no se sorprenda cuando aparezca.

Así que arregla una estructura\(\mathfrak{A}\) y una función de asignación\(s \: : \: Vars \rightarrow A\). Debemos demostrar que

\[\mathfrak{A} \models \left( \left[ \left( x_1 = y_1 \right) \land \left( x_2 = y_2 \right) \land \cdots \land \left( x_n = y_n \right) \right] \rightarrow \left( f \left( x_1, x_2, \ldots, x_n \right) = f \left( y_1, y_2, \ldots, y_n \right) \right) \right) \left[ s \right].\]

Como la fórmula en cuestión es una implicación, podemos suponer que el antecedente es satisfecho por el par\(\left( \mathfrak{A}, s \right)\), y así\(s \left( x_1 \right) = s \left( y_1 \right)\),\(s \left( x_2 \right) = s \left( y_2 \right), \ldots,\) y\(s \left( x_n \right) = s \left( y_n \right)\). Eso debemos probarlo\(\mathfrak{A} \models \left( f \left( x_1, x_2, \ldots, x_n \right) = f \left( y_1, y_2, \ldots, y_n \right) \right) \left[ s \right]\). A partir de la definición de satisfacción (Definición 1.7.4), sabemos que esto significa que tenemos que mostrar

\[\bar{s} \left( f \left( x_1, x_2, \ldots, x_n \right) \right) = \bar{s} \left( f \left( y_1, y_2, \ldots, y_n \right) \right).\]

Ahora nos fijamos en la definición de función de asignación de términos (Definición 1.7.3) y vemos que debemos probar

\[f^\mathfrak{A} \left( \bar{s} \left( x_1 \right), \bar{s} \left( x_2 \right), \ldots, \bar{s} \left( x_n \right) \right) = f^\mathfrak{A} \left( \bar{s} \left( y_1 \right), \bar{s} \left( y_2 \right), \ldots, \bar{s} \left( y_n \right) \right).\]

Pero como\(\bar{s} \left( x_i \right) = s \left( x_i \right) = s \left( y_i \right) = \bar{s} \left( y_i \right)\), y como\(f^\mathfrak{A}\) es una función, esto es cierto. Así nuestro axioma de igualdad (E2) es válido.

Ahora examinamos el axioma cuantificador de tipo (Q1), reservando (Q2) para los Ejercicios. Una vez más, fijar\(\mathfrak{A}\) y\(s\), y asumir que el término\(t\) es sustituible por la variable\(x\) en la fórmula\(\phi\). Debemos demostrar que

\[\mathfrak{A} \models \left[ \left( \forall x \phi \right) \rightarrow \phi_t^x \right] \left[ s \right].\]

Entonces, una vez más, asumimos eso\(\mathfrak{A} \models \left( \forall x \phi \right) \left[ s \right]\), y lo demostramos\(\mathfrak{A} \models \phi_t^x \left[ s \right]\). Por suposición,\(\mathfrak{A} \models \phi \left[ s \left[ x | a \right] \right]\) para cualquier elemento\(a \in A\), así en particular,\(\mathfrak{A} \models \phi \left[ s \left[ x | \bar{s} \left( t \right) \right] \right]\).

Informalmente, esto dice que\(\phi\) es cierto en\(\mathfrak{A}\) con función de asignación\(s\), donde interpretas\(x\) como\(\bar{s} \left( t \right)\). Es plausible, dado nuestro supuesto que\(t\) es sustituible por\(x\) in\(\phi\), que si alteramos la fórmula reemplazando\(\phi\)\(x\) por\(t\), entonces\(\phi_t^x\) sería cierto adentro\(\mathfrak{A}\) con función de asignación\(s\). Este es el contenido del Teorema 2.6.2. Ya que sabemos eso\(\mathfrak{A} \models \phi \left[ s \left[ x | \bar{s} \left( t \right) \right] \right]\) y el Teorema 2.6.2 afirma que esto es equivalente a\(\mathfrak{A} \models \phi_t^x \left[ s \right]\), lo hemos establecido\(\mathfrak{A} \models \phi_t^x \left[ s \right]\), por lo que hemos demostrado que los axiomas de tipo (Q1) son válidos.

Así, módulo sus pruebas de (E1), (E3), y (Q2), y la prueba retardada del Teorema 2.6.2, todos nuestros axiomas lógicos son válidos, y nuestra prueba es completa.

Esto deja un ítem más en nuestra lista de requisitos para verificar. Debemos demostrar que nuestras reglas de inferencia preservan la verdad.

Teorema 2.5.2. Supongamos que\(\left( \Gamma, \theta \right)\) es una regla de inferencia. Entonces\(\Gamma \models \theta\).

Comprobante. Primero, supongamos que\(\left( \Gamma, \theta \right)\) es una regla de tipo (PC). Entonces\(\Gamma\) es finito, y por Lema 2.4.2, sabemos que

\[\left[ \gamma_{1 \: P} \land \gamma_{2 \: P} \land \cdots \land \gamma_{n \: P} \right] \rightarrow \theta_P\]

es una tautología, donde\(\Gamma_P = \{ \gamma_{1 \: P}, \gamma_{2 \: P}, \ldots, \gamma_{n \: P} \}\) está el conjunto de fórmulas proposicionales correspondientes a\(\Gamma\) y\(\theta_P\) es la fórmula proposicional correspondiente a\(\theta\). Pero entonces, por el Ejercicio 6 de la Sección 2.4, sabemos que

\[\left[ \gamma_1 \land \gamma_2 \land \cdots \land \gamma_n \right] \rightarrow \theta\]

es válido, y por lo tanto\(\Gamma \models \theta\).

La otra posibilidad es que nuestra regla de inferencia sea una regla cuantificadora. Entonces, supongamos que no\(x\) es gratis en\(\psi\). Eso lo demostramos\(\left( \psi \rightarrow \phi \right) \models \left[ \psi \rightarrow \left( \forall x \phi \right) \right]\), dejando la otra regla (Q2) para los Ejercicios.

Así que arregla una estructura\(\mathfrak{A}\) y asumamos\(\mathfrak{A} \models \left( \psi \rightarrow \phi \right)\). Así nuestra suposición es que para cualquier asignación\(s\),\(\mathfrak{A} \models \left( \psi \rightarrow \phi \right) \left[ s \right]\). Debemos demostrar eso\(\mathfrak{A} \models \left( \psi \rightarrow \forall x \phi \right)\), lo que significa que debemos demostrar que\(\left( \psi \rightarrow \forall x \phi \right)\) se satisface en\(\mathfrak{A}\) bajo cada función de asignación. Así que dejemos que\(t \: : \: Vars \rightarrow A\) se le dé una función de asignación. Debemos demostrarlo\(\mathfrak{A} \models \left( \psi \rightarrow \forall x \phi \right) \left[ t \right]\). Si\(\mathfrak{A} \not\models \psi \left[ t \right]\), ya terminamos, asumamos eso\(\mathfrak{A} \models \psi \left[ t \right]\). Eso queremos probarlo\(\mathfrak{A} \models \forall x \phi \left[ t \right]\), lo que quiere decir que si\(a\) es algún elemento de\(A\), debemos demostrarlo\(\mathfrak{A} \models \phi \left[ t \left[ x | a \right] \right]\).

Sabemos, por suposición, eso\(\mathfrak{A} \models \left( \psi \rightarrow \phi \right) \left[ t \left[ x | a \right] \right]\). Además, la Proposición 1.7.7 nos dice que\(\mathfrak{A} \models \psi \left[ \left[ x | a \right] \right]\), como\(\mathfrak{A} \models \psi \left[ t \right]\),\(t\) y de\(t \left[ x | a \right]\) acuerdo en todas las variables libres de\(\psi\) (no\(x\) es libre en\(\psi\) por suposición). Pero entonces, por la definición de satisfacción\(\mathfrak{A} \models \phi \left[ t \left[ x | a \right] \right]\),, y estamos acabados.

Ahora estamos en un punto en el que podemos probar el Teorema de la Solidez. La idea detrás de este teorema es muy sencilla. Supongamos que\(\Sigma\) es un conjunto de\(\mathcal{L}\) -fórmulas y supongamos que hay una deducción de\(\phi\) de\(\Sigma\). Lo que nos dice el Teorema de la Solidez es\(\mathfrak{A}\) que en cualquier estructura que haga que todas las fórmulas de\(\Sigma\) verdad, también lo\(\phi\) es.

Teorema 2.5.3 (Solidez). Si\(\Sigma + \phi\), entonces\(\Sigma \models \phi\).

Comprobante. Deja a\(_\Sigma\)\(= \{ \phi | \Sigma \vdash \phi \}\) Thm, y deja\(C = \{ \phi | \Sigma \models \phi \}\). Mostramos que Thm\(_\Sigma\)\(\subseteq C\), lo que prueba el teorema.

Aviso que\(C\) tiene las siguientes características:

1. \(\Sigma \subseteq C\). Si\(\sigma \in \Sigma\), entonces ciertamente\(\Sigma \models \sigma\).
2. \(\Lambda \subseteq C\). Como los axiomas lógicos son válidos, son ciertos en cualquier estructura. Así\(\Sigma \models \lambda\) para cualquier axioma lógico\(\lambda\), lo que significa que si\(\lambda \in \Lambda\), entonces\(\lambda \in C\), según sea necesario.
3. Si\(\left( \Gamma, \theta \right)\) es una regla de inferencia y\(\Gamma \subseteq C\), entonces\(\theta \in C\). Entonces asumamos eso\(\Gamma \subseteq C\). Para\(\theta \in C\) probarlo debemos demostrar\(\Sigma \models \theta\). Fijar una estructura\(\mathfrak{A}\) tal que\(\mathfrak{A} \models \Sigma\). Eso debemos probarlo\(\mathfrak{A} \models \theta\).
   Si\(\gamma\) hay algún elemento de\(\Gamma\), entonces ya\(\gamma \in C\), eso lo sabemos\(\Sigma \models \gamma\). Desde\(\mathfrak{A} \models \Sigma\) y\(\Sigma \models \gamma\), eso lo sabemos\(\mathfrak{A} \models \gamma\). Pero esto dice que\(\mathfrak{A} \models \gamma\) para cada uno\(\gamma \in \Gamma\), entonces\(\mathfrak{A} \models \Gamma\). Pero el Teorema 2.5.2 nos dice que\(\Gamma \models \theta\), ya que\(\left( \Gamma, \theta \right)\) es una regla de inferencia. Por lo tanto, desde\(\mathfrak{A} \models \Gamma\) y\(\Gamma \models \theta\),\(\mathfrak{A} \models \theta\), según sea necesario.

Así\(C\) es un conjunto del tipo descrito en la Proposición 2.2.4, y por esa proposición, Thm\(_\Sigma\)\(\subseteq C\), según sea necesario.

Observe que el Teorema de la Solidez comienza a unir las nociones de deducibilidad e implicación lógica. Dice: “Si hay una deducción\(\Sigma\) de\(\phi\), entonces implica\(\Sigma\) lógicamente”\(\phi\). Así, la noción puramente sintáctica de deducción, noción que se basa únicamente en consideraciones tipográficas, está ligada a las nociones de verdad e implicación lógica, ideas que están inextricablemente ligadas a las estructuras matemáticas y sus propiedades. Esta vinculación se estrechará en el Capítulo 3.

Chafia: La prueba del Teorema de la Solidez que hemos presentado anteriormente tiene las cualidades deseables de ser neto y rápido. Destaca un hecho central sobre las consecuencias de\(\Sigma\), a saber, que Thm\(_\Sigma\) es el conjunto más pequeño de fórmulas que satisfacen las tres condiciones dadas. Desafortunadamente, la prueba tiene el atributo menos deseable de ser bastante abstracta. El ejercicio 5 esboza una prueba más directa y menos abstracta del Teorema de la Solidez.

Ejercicios

1. Ingrid entra a tu oficina un día y anuncia que está desconcertada. Tiene un conjunto de axiomas\(\Sigma\) en el lenguaje de la teoría de números, y tiene una fórmula en la\(\phi\) que ha demostrado utilizando las suposiciones\(\Sigma\). Desafortunadamente,\(\phi\) es una afirmación que no es cierta en el modelo estándar\(\mathfrak{N}\). ¿Esto es un problema? Si es un problema, ¿qué posibles explicaciones se te ocurren que explicarían qué salió mal? Si no es un problema, ¿por qué no es un problema?
2. Demostrar que los axiomas de igualdad de tipo (E1) y (E3) son válidos.
3. Mostrar que los axiomas cuantificadores de tipo (Q2) son válidos.
4. Demostrar que, si no\(x\) es libre en\(\psi\),\(\left( \phi \rightarrow \psi \right) \models \left[ \left( \exists x \phi \right) \rightarrow \psi \right]\).
5. Demostrar el teorema de la solidez por inducción sobre la complejidad de la prueba de\(\phi\). Para los casos base,\(\phi\) es ya sea un axioma lógico o un miembro de\(\Sigma\). Entonces supongamos que\(\phi\) se prueba por referencia a una regla de inferencia. Demostrar que en este caso también,\(\Sigma \models \phi\).