2.6: Dos Lemmas Técnicos

En esta sección presentamos dos lemas bastante técnicos que necesitamos para completar la prueba del Teorema 2.5.1. Las pruebas que están involucradas no son bonitas, y si usted es del tipo de confianza, es posible que desee escanear a través de esta sección con bastante rapidez. Por otro lado, si te acercas a estos resultados, obtendrás una mejor apreciación por los detalles de sustituibilidad y funciones de asignación.

Para motivar el primer lema, considere este ejemplo: Supongamos que estamos trabajando en el lenguaje de la teoría de números y que la estructura bajo consideración comprende los números naturales. Que el término\(u\) sea\(x \cdot v\) y el término\(t\) sea\(y + z\). Entonces\(u_t^x\) es\(\left( y + z \right) \cdot v\). Ahora tenemos que arreglar un par de funciones de asignación. Deje que la función de asignación\(s\) se vea así:

\[\begin{array}{c|c} Vars & s \\ \hline x & 12 \\ y & 3 \\ z & 7 \\ v & 4 \\ \vdots & \vdots \end{array}\]

Entonces\(s \left( x \right) = 12\),\(s \left( y \right) = 3\), y así sucesivamente.

Ahora, supongamos que\(s'\) es una función de asignación que es igual\(s\), excepto que\(s'\) envía\(x\) al valor\(\bar{s} \left( t \right)\), que es\(\bar{s} \left( y + z \right) = 3 + 7 = 10\):

\[\begin{array}{c|c|c} Vars & s & s' \\ \hline x & 12 & 10 \\ y & 3 & 3 \\ z & 7 & 7 \\ v & v & v \\ \vdots & \vdots & \vdots \end{array}\]

Ahora, si comparas\(\bar{s} \left( u_t^x \right)\) y\(\bar{s'} \left( u \right)\), encuentras que

\[\left. \begin{array} { c } { \overline { s } \left( u _ { t } ^ { x } \right) = \overline { s } ( ( y + z ) \cdot v ) = ( 3 + 7 ) \cdot 4 = 10 \cdot 4 = 40 } \\ { \overline { s ^ { \prime } } ( u ) = \overline { s ^ { \prime } } ( x \cdot v ) = 10 \cdot 4 = 40 } \end{array} \right.\]

Entonces, en esta situación, el elemento del universo que es asignado por\(s\) a\(u_t^x\) es el mismo que el elemento del universo que es asignado por\(s^\prime\) a\(u\). En cierto sentido, el lema establece que no importa si alteras el término o la función de asignación, el resultado es el mismo.

Aquí está la declaración formal:

Lema 2.6.1. Supongamos que\(u\) es un término,\(x\) es una variable, y\(t\) es un término. Supongamos que\(s \: : \: Vars \rightarrow A\) es una función de asignación de variables y eso\(s^\prime = s \left[ x | \overline{s} \left( t \right) \right]\). Entonces\(\overline{s} \left( u_t^x \right) = \overline{s^\prime} \left( u \right)\).

Comprobante. La prueba es por inducción sobre la complejidad del término\(u\). Si\(u\) es la variable\(x\), entonces

\[\left.\begin{aligned} \overline { s } \left( u _ { t } ^ { x } \right) & = \overline { s } \left( x _ { t } ^ { x } \right) \\ & = \overline { s } ( t ) \\ & = \overline { s ^ { \prime } } ( x ) \\ & = \overline { s ^ { \prime } } ( u ) \end{aligned} \right.\]

Si\(u\) es la variable\(y\) y\(y\) es diferente a\(x\), entonces

\[\left.\begin{aligned} \overline { s } \left( u _ { t } ^ { x } \right) & = \overline { s } \left( y _ { t } ^ { x } \right) \\ & = \overline { s } ( y ) \\ & = s ( y ) \\ & = s ^ { \prime } ( y ) \\ & = \overline { s } ^ { \prime } ( u ) \end{aligned} \right.\]

Si\(u\) es un símbolo constante\(c\), entonces\(\overline{s} \left( u_t^x \right) = \overline{s} \left( c_t^x \right) = \overline{s} \left( c \right) = c^\mathfrak{A} = \overline{s^\prime} \left( u \right)\).

El último caso inductivo es si\(u\) es\(f \left( r_1, r_2, \ldots, r_n \right)\), con cada uno\(r_i\) un término. En este caso,

\[\begin{array}{rcll} \overline{s} \left( u_t^x \right) & = & \overline{s} \left( \left[ f \left( r_1, r_2, \ldots, r_n \right) \right]_t^x \right) & \\ & = & \overline{s} \left( f \left( \left( r_1 \right)_t^x, \left( r_2 \right)_t^x, \ldots, \left( r_n \right)_t^x \right) \right) & \\ & = & f^\mathfrak{A} \left( \overline{s} \left[ \left( r_1 \right)_t^x \right], \overline{s} \left[ \left( r_2 \right)_t^x \right], \ldots, \overline{s} \left[ \left( r_n \right)_t^x \right] \right) & \text{definition of} \: \overline{s} \\ & = & f^\mathfrak{A} \left( \overline{s^\prime} \left( r_1 \right), \overline{s^\prime} \left( r_2 \right), \ldots, \overline{s^\prime} \left( r_n \right) \right) & \text{inductive hypothesis} \\ & = & \overline{s^\prime} \left( f \left( r_1, r_2, \ldots, r_n \right) \right) & \text{definition of} \: \overline{s^\prime} \\ & = & \overline{s^\prime} \left( u \right) & \end{array}\]

Entonces para cada término\(u\),\(\overline{s} \left( u_t^x \right) = \overline{s^\prime} \left( u \right)\).

Chaf: Eso fue duro. Si entendiste esa prueba la primera vez a través, has hecho algo bastante fuera de lo común. Si, por otro lado, eres un mero mortal, tal vez quieras volver a trabajar a través de la prueba, teniendo en cuenta un ejemplo mientras trabajas. Elige un idioma, términos\(u\) y\(t\) en tu idioma, y una variable\(x\). Corregir una función de asignación en particular\(s\). Entonces solo sigue los pasos de la prueba, haciendo un seguimiento de hacia dónde va todo. Nosotros lo escribiríamos por ti, pero sacarás más de hacerlo por ti mismo. ¡Ve a ello!

Nuestro siguiente resultado técnico es el lema que citamos explícitamente en la prueba del Teorema 2.5.1. Este teorema afirma que mientras\(t\) sea sustitutable\(x\) en\(\phi\), las dos formas diferentes de evaluar la verdad de "\(\phi\), donde interpretes\(x\) como\(t\)" coinciden. La primera forma de evaluar la verdad sería formando la fórmula\(\phi_t^x\) y viendo si\(\mathfrak{A} \models \phi_t^x \left[ s \right]\). La segunda forma sería cambiar la función de asignación\(s\) para interpretar\(x\) como\(\overline{s} \left( t \right)\) y verificar si la fórmula original\(\phi\) es verdadera con esta nueva función de asignación. El teorema afirma que los dos métodos son equivalentes.

Teorema 2.6.2. Supongamos que\(\phi\) es una\(\mathcal{L}\) -fórmula,\(x\) es una variable,\(t\) es un término, y\(t\) es sustitutable por\(x\) in\(\phi\). Supongamos que\(s \: : \: Vars \rightarrow A\) es una función de asignación de variables y eso\(s^\prime = s \left[ x | \overline{s} \left( t \right) \right]\). Entonces\(\mathfrak{A} \models \phi_t^x \left[ s \right]\) si y sólo si\(\mathfrak{A} \models \phi \left[ s^\prime \right]\).

Comprobante. Utilizamos la inducción en la complejidad de\(\phi\). El primer caso base es dónde\(\phi : \equiv u_1 = u_2\), dónde\(u_1\) y\(u_2\) son términos. Entonces los siguientes son equivalentes:

\[\begin{array}{ll} \mathfrak{A} \models \phi_t^x \left[ s \right] & \\ \mathfrak{A} \models \left( u_1 \right)_t^x = \left( u_2 \right)_t^x \left[ s \right] & \\ \overline{s} \left( \left( u_1 \right)_t^x \right) = \overline{s} \left( \left( u_2 \right)_t^x \right) & \text{definition of satisfaction} \\ \overline{s^\prime} \left( u_1 \right) = \overline{s^\prime} \left( u_2 \right) & \text{by Lemma 2.6.1} \\ \mathfrak{A} \models \phi \left[ s^\prime \right] & \end{array}\]

El segundo caso base es donde\ (\ phi:\ equiv R\ left (u_1, u_2,\ ldots, u_n\ right). Este caso es similar al caso anterior.

Los casos inductivos que involucran a los conectivos\(\lor\) y\(\neg\) siguen inmediatamente de la hipótesis inductiva.

Esto deja el último caso inductivo, donde\(\phi : \equiv \forall y \psi\). Desglosamos este caso en dos subcasos: En el primer subcaso\(x\) es\(y\), y en el segundo subcaso no lo\(x\) es\(y\).

Si\(\phi : \equiv \forall y \psi\) y\(y\) es\(x\), entonces lo\(\phi_t^x\) es\(\phi\). Por lo tanto,\(\mathfrak{A} \models \phi_t^x \left[ s \right]\) si y sólo si\(\mathfrak{A} \models \phi \left[ s \right]\). Pero como\(s\) y de\(s^\prime\) acuerdo en todas las variables libres de\(\phi\) (no\(x\) es libre\), por la Proposición 1.7.7,\(\mathfrak{A} \models \phi \left[ s \right]\) si y sólo si\(\mathfrak{A} \models \phi \left[ s^\prime \right]\), según sea necesario para este subcaso.

El segundo subcaso, donde\(\phi : \equiv \forall y \psi\) y no\(y\) es\(x\), se examina en dos subcasos:

Subsubcaso 1: Si\(\phi : \equiv \forall y \psi\), no\(y\) es\(x\), y no\(x\) es libre en\(\psi\), entonces sabemos por Ejercicio 5 en la Sección 1.8 que\(\psi_t^x\) es\(\psi\), y así\(\phi_t^x\) es\(\phi\). Pero entonces

\[\begin{array}{ll} \mathfrak{A} \models \phi_t^x \left[ s \right] & \text{iff} \\ \mathfrak{A} \models \left( \forall y \right) \left( \psi_t^x \right) \left[ s \right] & \text{iff} \\ \mathfrak{A} \models \left( \psi_t^x \right) \left[ s \left[ y | a \right] \right] & \text{for every} \: a \in A \end{array}.\]

Pero también sabemos que

\[\begin{array}{ll} \mathfrak{A} \models \phi \left[ s^\prime \right] & \text{iff} \\ \mathfrak{A} \models \left( \forall y \right) \left( \psi \right) \left[ s^\prime \right] & \text{iff} \\ \mathfrak{A} \models \psi \left[ s^\prime \left[ y | a \right] \right] & \text{for every} \: a \in A \end{array}.\]

Pero como no lo\(x\) es\(y\), sabemos que para cualquiera\(a \in A\)\(s^\prime \left[ y | a \right] = s \left[ y | a \right] \left[ x | \overline{s} \left( t \right) \right]\),, así por la hipótesis inductiva (aviso que\(t\) se puede sustituir\(x\) en\(\psi\)) tenemos

\[\mathfrak{A} \models \left( \psi_t^x \right) \left[ s \left[ y | a \right] \right] \: \text{iff} \: \mathfrak{A} \models \psi \left[ s^\prime \left[ y | a \right] \right].\]

Entonces\(\mathfrak{A} \models \phi_t^x \left[ s \right]\) si y sólo si\(\mathfrak{A} \models \phi \left[ s^\prime \right]\), según sea necesario.