Probaremos dos teoremas muy importantes que en algún sentido nos dicen que el reemplazo sintáctico conmuta con la valuación semántica. Usaremos la notación declaratoria para expresarlos ya que los vuelve mucho mas accesibles e intuitivos.
7.4 (Teorema de Reemplazo para Términos). Supongamos \(t=_{d}t(w_{1},...,w_{k}),\) \(s_{1}=_{d}s_{1}(v_{1},...,v_{n}),...,s_{k}=_{d}s_{k}(v_{1},...,v_{n})\). Entonces
adhocprefix(a)adhocsufix \(t(s_{1},...,s_{k})\in T^{\tau}\)
adhocprefix(b)adhocsufix Todas las variables de \(t(s_{1},...,s_{k})\) están en \(\{v_{1},...,v_{n}\}\)
adhocprefix(c)adhocsufix Si declaramos \(t(s_{1},...,s_{k})=_{d}t(s_{1},...,s_{k})(v_{1},...,v_{n})\), entonces para cada estructura \(\mathbf{A}\) y \(a_{1},....,a_{n}\in A,\) se tiene que \[t(s_{1},...,s_{k})^{\mathbf{A}}[a_{1},....,a_{n}]=t^{\mathbf{A}}[s_{1}^{\mathbf{A}}[a_{1},....,a_{n}],...,s_{k}^{\mathbf{A}}[a_{1},....,a_{n}]].\]
Proof. Usaremos la Regla de Inducción desde 0. Para cada \(l\in\omega\) sea \(\mathrm{Enu}_{l}\) el siguiente enunciado:
adhocprefix\(\mathrm{Enu}_{l}\):adhocsufix Supongamos \(t=_{d}t(w_{1},...,w_{k})\in T_{l}^{\tau}\) y \(s_{1}=_{d}s_{1}(v_{1},...,v_{n}),...,s_{k}=_{d}s_{k}(v_{1},...,v_{n})\). Entonces
adhocprefix(a)adhocsufix \(t(s_{1},...,s_{k})\in T^{\tau}\)
adhocprefix(b)adhocsufix Todas las variables de \(t(s_{1},...,s_{k})\) están en \(\{v_{1},...,v_{n}\}\)
adhocprefix(c)adhocsufix Si declaramos \(t(s_{1},...,s_{k})=_{d}t(s_{1},...,s_{k})(v_{1},...,v_{n})\), entonces para cada estructura \(\mathbf{A}\) y \(a_{1},....,a_{n}\in A,\) se tiene que \[t(s_{1},...,s_{k})^{\mathbf{A}}[a_{1},....,a_{n}]=t^{\mathbf{A}}[s_{1}^{\mathbf{A}}[a_{1},....,a_{n}],...,s_{k}^{\mathbf{A}}[a_{1},....,a_{n}]].\]
Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).
Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Supongamos \(t=_{d}t(w_{1},...,w_{k})\in T_{0}^{\tau}\) y \(s_{1}=_{d}s_{1}(v_{1},...,v_{n}),...,s_{k}=_{d}s_{k}(v_{1},...,v_{n})\). Probaremos que se cumplen (a), (b) y (c) para \(t,s_{1},...,s_{k}\). Ya que \(t\in T_{0}^{\tau}=Var\cup\mathcal{C}\) tenemos dos casos.
Caso \(t=w_{j}\), para algún \(j\). Notar que \(t(s_{1},...,s_{k})=s_{j}\) por lo cual se cumplen (a) y (b). Veamos que se cumple (c). Declaremos \(t(s_{1},...,s_{k})=_{d}t(s_{1},...,s_{k})(v_{1},...,v_{n})\) (esta declaración ya estaba hecha ya que \(t(s_{1},...,s_{k})=s_{j}\)). Sea \(\mathbf{A}\)una estructura y \(a_{1},....,a_{n}\in A\). Aplicando el Lema Caracter Recursivo de la Notación \(t^{\mathbf{A}}[a_{1},....,a_{n}]\) tenemos que \[\begin{array}{ccl} t(s_{1},...,s_{k})^{\mathbf{A}}[\vec{a}] & = & s_{j}^{\mathbf{A}}[\vec{a}]\\ & = & w_{j}^{\mathbf{A}}[s_{1}^{\mathbf{A}}[a_{1},....,a_{n}],...,s_{k}^{\mathbf{A}}[a_{1},....,a_{n}]]\\ & = & t^{\mathbf{A}}[s_{1}^{\mathbf{A}}[a_{1},....,a_{n}],...,s_{k}^{\mathbf{A}}[a_{1},....,a_{n}]] \end{array}\]
Caso \(t=c\), para algún \(c\in\mathcal{C}\). Notar que \(t(s_{1},...,s_{k})=c\) por lo cual se cumplen (a) y (b). Veamos que se cumple (c). Declaremos \(t(s_{1},...,s_{k})=_{d}t(s_{1},...,s_{k})(v_{1},...,v_{n})\). Sea \(\mathbf{A}\) una estructura y \(a_{1},....,a_{n}\in A\). Aplicando el Lema Caracter Recursivo de la Notación \(t^{\mathbf{A}}[a_{1},....,a_{n}]\) tenemos que \[\begin{array}{ccl} t(s_{1},...,s_{k})^{\mathbf{A}}[\vec{a}] & = & c^{\mathbf{A}}[\vec{a}]\\ & = & c^{\mathbf{A}}\\ & = & t^{\mathbf{A}}[s_{1}^{\mathbf{A}}[a_{1},....,a_{n}],...,s_{k}^{\mathbf{A}}[a_{1},....,a_{n}]] \end{array}\]
Prueba de que si \(\mathrm{Enu}_{l}\) es verdadero entonces \(\mathrm{Enu}_{l+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{l}\). Supongamos \(t=_{d}t(w_{1},...,w_{k})\in T_{l+1}^{\tau}\) y \(s_{1}=_{d}s_{1}(v_{1},...,v_{n}),...,s_{k}=_{d}s_{k}(v_{1},...,v_{n})\). Probaremos que se cumplen (a), (b) y (c) para \(t,s_{1},...,s_{k}\). Por el Lema de Lectura Única de Términos Declarados hay varios casos.
Caso \(t=c,\) para algún \(c\in\mathcal{C}\). Ya fue probado en la prueba de \(\mathrm{Enu}_{0}\).
Caso \(t=w_{j}\), para algún \(j\). Ya fue probado en la prueba de \(\mathrm{Enu}_{0}\).
Caso \(t=f(t_{1},...,t_{m})\), con \(f\in\mathcal{F}_{m}\), \(m\geq1\) y \(t_{1},...,t_{m}\in T^{\tau}\). Ya que \(t\in T_{l+1}^{\tau}\) el mismo lema nos dice que \(t_{1},...,t_{m}\in T_{l}^{\tau}\). Nótese que por nuestra Convención Notacional 3 asumimos ya hechas las declaraciones \[t_{1}=_{d}t_{1}(w_{1},...,w_{k}),...,t_{m}=_{d}t_{m}(w_{1},...,w_{k})\] Ya que \(\mathrm{Enu}_{l}\) es verdadero tenemos que cada \(t_{i}(s_{1},...,s_{k})\) es un término cuyas variables están en \(\{v_{1},...,v_{n}\}\). Declaremos entonces: \[t_{i}(s_{1},...,s_{k})=_{d}t_{i}(s_{1},...,s_{k})(v_{1},...,v_{n}),\text{ }i=1,...,m\] Ya que \[t(s_{1},...,s_{k})=f(t_{1}(s_{1},...,s_{k}),...,t_{m}(s_{1},...,s_{k}))\] tenemos que \(t(s_{1},...,s_{k})\) es un término cuyas variables están en \(\{v_{1},...,v_{n}\}\). Esto prueba que se cumplen (a) y (b) para \(t,s_{1},...,s_{k}\). Para probar (c), notemos que por \(\mathrm{Enu}_{l}\) se tiene que \[t_{i}(s_{1},...,s_{k})^{\mathbf{A}}[\vec{a}]=t_{i}^{\mathbf{A}}[s_{1}^{\mathbf{A}}[\vec{a}],...,s_{k}^{\mathbf{A}}[\vec{a}]],\text{ }i=1,...,m\] Declaremos \(t(s_{1},...,s_{k})=_{d}t(s_{1},...,s_{k})(v_{1},...,v_{n})\). Se tiene que \[\begin{array}{ccl} t(s_{1},...,s_{k})^{\mathbf{A}}[\vec{a}] & = & f(t_{1}(s_{1},...,s_{k}),...,t_{m}(s_{1},...,s_{k}))^{\mathbf{A}}[\vec{a}]\\ & = & f^{\mathbf{A}}(t_{1}(s_{1},...,s_{k})^{\mathbf{A}}[\vec{a}],...,t_{m}(s_{1},...,s_{k})^{\mathbf{A}}[\vec{a}])\\ & = & f^{\mathbf{A}}(t_{1}^{\mathbf{A}}[s_{1}^{\mathbf{A}}[\vec{a}],...,s_{k}^{\mathbf{A}}[\vec{a}]],...,t_{m}^{\mathbf{A}}[s_{1}^{\mathbf{A}}[\vec{a}],...,s_{k}^{\mathbf{A}}[\vec{a}]])\\ & = & t^{\mathbf{A}}[s_{1}^{\mathbf{A}}[\vec{a}],...,s_{k}^{\mathbf{A}}[\vec{a}]] \end{array}\] lo cual prueba que se cumple (c) para \(t,s_{1},...,s_{k}\).
En el sentido mas general, el reemplazo de variables libres en fórmulas por términos no preserva el significado. Por ejemplo sea \(\varphi=\exists x_{1}(f(x_{1})\equiv x_{2})\) y declaremos \(\varphi=_{d}\varphi(x_{2})\). Es claro que dada una estructura \(\mathbf{A}\), tenemos que \(\mathbf{A}\models\varphi[a]\) si y solo si \(a\) está en la imagen de \(f^{\mathbf{A}}\), es decir la fórmula \(\varphi(x_{2})\) dice "\(x_{2}\) está en la imagen de \(f^{\mathbf{A}}\)". Uno entonces esperaría que \(\varphi(x_{1})\) diga "\(x_{1}\) está en la imagen de \(f^{\mathbf{A}}\)" pero esto no es así ya que \(\varphi(x_{1})\) es igual a \(\exists x_{1}(f(x_{1})\equiv x_{1})\) y por lo tanto ni siquiera habla acerca de \(x_{1}\) ya que \(\varphi(x_{1})\) es una sentencia. Mas aún, esta sentencia es verdadera en \(\mathbf{A}\) sii \(f^{\mathbf{A}}(a)=a\), para algún \(a\in A\).
El problema aquí surge porque la variable que va a reemplazar a la variable libre \(x_{2}\) (o sea \(x_{1}\)) queda afectada por el cuantificador \(\exists x_{1}\) ya que la ocurrencia libre de \(x_{2}\) que será reemplazada por \(x_{1}\) está justamente en el alcance de dicho cuantificador. Esto obviamente rompe el significado original.
O sea que para expresar el teorema de reemplazo para fórmulas necesitaremos dar una definición que garantice que cuando reemplazamos una variable libre \(v\) por otra variable \(w\) en una fórmula, el significado de la fórmula no se altere. Daremos a continuación el concepto de sustitución de variables en forma precisa. Antes el concepto de alcance el cual esta emparentado con el de sustitución de variables.
7.35. Si \(Qv\) ocurre en \(\varphi\) a partir de \(i\), entonces hay una única fórmula \(\psi\) tal que \(Qv\psi\) ocurre en \(\varphi\) a partir de \(i\).
Proof. Nótese que la formula \(\psi\) de la que habla el enunciado es siempre única ya que nunca una formula puede ser tramo inicial propio de otra formula. O sea que sólo es necesario probar la existencia. Para esto usaremos la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:
adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Si \(Qv\) ocurre en \(\varphi\) a partir de \(i\) y \(\varphi\in F_{k}^{\tau}\), entonces hay una fórmula \(\psi\) tal que \(Qv\psi\) ocurre en \(\varphi\) a partir de \(i\).
Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).
Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Trivial ya que \(Qv\) nunca ocurre en una fórmula atómica.
Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Supongamos \(Qv\) ocurre en \(\varphi\) a partir de \(i\) y \(\varphi\in F_{k+1}^{\tau}\). Por definición de \(F_{k+1}^{\tau}\), hay varios casos.
Caso \(\varphi\in F_{k}^{\tau}\). Ya que es verdadero \(\mathrm{Enu}_{k}\), es claro que se cumple la conclusión de \(\mathrm{Enu}_{k+1}\).
Caso \(\varphi=(\varphi_{1}\vee\varphi_{2})\), con \(\varphi_{1},\varphi_{2}\in F_{k}^{\tau}\). Nótese que \(i\in\{2,\left|\varphi_{1}\right|\}\) o \(i\in\{\left|(\varphi_{1}\vee\right|+1,\left|(\varphi_{1}\vee\varphi_{2}\right|\}\). En el primer caso resulta que \(Qv\) ocurre en \(\varphi_{1}\) a partir de \(i-1\) lo cual por ser verdadero \(\mathrm{Enu}_{k}\) nos dice que hay una fórmula \(\psi\) tal que \(Qv\psi\) ocurre en \(\varphi_{1}\) a partir de \(i-1\). En el segundo caso resulta que \(Qv\) ocurre en \(\varphi_{2}\) a partir de \(i-\left|(\varphi_{1}\vee\right|\) lo cual por ser verdadero \(\mathrm{Enu}_{k}\) nos dice que hay una fórmula \(\psi\) tal que \(Qv\psi\) ocurre en \(\varphi_{1}\) a partir de \(i-\left|(\varphi_{1}\vee\right|\). En ambos casos \(Qv\psi\) ocurre en \(\varphi\) a partir de \(i\).
Los casos \(\varphi=(\varphi_{1}\wedge\varphi_{2})\), \(\varphi=(\varphi_{1}\rightarrow\varphi_{2})\), \(\varphi=(\varphi_{1}\leftrightarrow\varphi_{2})\) y \(\varphi=\neg\varphi_{1}\) son análogos al caso anterior.
Caso \(\varphi=\forall x_{j}\varphi_{1}\), \(\varphi_{1}\in F_{k}^{\tau}\) y \(j\in\mathbf{N}\). Si \(i=1\), entonces \(Q=\forall\) y \(v=x_{j}\) y claramente podemos tomar \(\psi=\varphi_{1}\) para corroborar que \(\mathrm{Enu}_{k+1}\) es cierto. Si \(i>1\), entonces claramente deberá suceder que \(i\in\{\left|\forall x_{j}\right|+1,\left|\varphi\right|\}\). Pero entonces \(Qv\) ocurre en \(\varphi_{1}\) a partir de \(i-\left|\forall x_{j}\right|\) lo cual por ser verdadero \(\mathrm{Enu}_{k}\) nos dice que hay una fórmula \(\psi\) tal que \(Qv\psi\) ocurre en \(\varphi_{1}\) a partir de \(i-\left|\forall x_{j}\right|\). Pero entonces \(Qv\psi\) ocurre en \(\varphi\) a partir de \(i\).
Caso \(\varphi=\exists x_{j}\varphi_{1}\), \(\varphi_{1}\in F_{k}^{\tau}\) y \(j\in\mathbf{N}\). Similar al caso anterior.
Dada una ocurrencia de \(Qv\) en una fórmula \(\varphi\), la fórmula \(\psi\) del lema anterior será llamada el alcance de dicha ocurrencia en \(\varphi\). Nótese que dos ocurrencias distintas de \(Qv\) en \(\varphi\) pueden tener alcances distintos por lo cual el concepto de alcance es relativo a una ocurrencia de un cuantificador y no relativo a un cuantificador a secas.
Diremos que \(v\) es sustituible por \(w\) en \(\varphi\) cuando ninguna ocurrencia libre de \(v\) en \(\varphi\) sucede dentro de una ocurrencia de una subfórmula de la forma \(Qw\psi\) en \(\varphi\). En otras palabras \(v\) no será sustituible por \(w\) en \(\varphi\) cuando alguna ocurrencia libre de \(v\) en \(\varphi\) suceda dentro de una ocurrencia en \(\varphi\) de una fórmula de la forma \(Qw\psi\). Nótese que puede suceder que \(v\) sea sustituible por \(w\) en \(\varphi\) y que sin embargo haya una subfórmula de la forma \(Qw\psi\) para la cual \(v\in Li(Qw\psi)\). Dejamos como ejercicio encontrar un ejemplo de esta situación.
Usando lemas anteriores podemos ver que se dan las siguientes propiedades:
adhocprefix(1)adhocsufix Si \(\varphi\) es atómica, entonces \(v\) es sustituible por \(w\) en \(\varphi\)
adhocprefix(2)adhocsufix Si \(\varphi=(\varphi_{1}\eta\varphi_{2})\), entonces \(v\) es sustituible por \(w\) en \(\varphi\) sii \(v\) es sustituible por \(w\) en \(\varphi_{1}\) y \(v\) es sustituible por \(w\) en \(\varphi_{2}\)
adhocprefix(3)adhocsufix Si \(\varphi=\lnot\varphi_{1}\), entonces \(v\) es sustituible por \(w\) en \(\varphi\) sii \(v\) es sustituible por \(w\) en \(\varphi_{1}\)
adhocprefix(4)adhocsufix Si \(\varphi=Qv\varphi_{1}\), entonces \(v\) es sustituible por \(w\) en \(\varphi\)
adhocprefix(5)adhocsufix Si \(\varphi=Qw\varphi_{1}\) y \(v\in Li(\varphi_{1})\), entonces \(v\) no es sustituible por \(w\) en \(\varphi\)
adhocprefix(6)adhocsufix Si \(\varphi=Qw\varphi_{1}\) y \(v\not\in Li(\varphi_{1})\), entonces \(v\) es sustituible por \(w\) en \(\varphi\)
adhocprefix(7)adhocsufix Si \(\varphi=Qu\varphi_{1}\), con \(u\neq v,w\), entonces \(v\) es sustituible por \(w\) en \(\varphi\) sii \(v\) es sustituible por \(w\) en \(\varphi_{1}\)
Nótese que las propiedades (1),...,(7) pueden usarse para dar una definición recursiva de la relación \("v\) \(\mathit{es\ sustituible\ por\ }w\mathit{\ en}\) \(\varphi"\).
Dado un término \(t\), diremos que una variable \(v\) es sustituible por \(t\) en \(\varphi\) cuando \(v\) sea sustituible en \(\varphi\) por cada variable que ocurre en \(t\).
7.5 (Teorema de Reemplazo para Fórmulas). Supongamos \(\varphi=_{d}\varphi(w_{1},...,w_{k})\), \(t_{1}=_{d}t_{1}(v_{1},...,v_{n}),...,t_{k}=_{d}t_{k}(v_{1},...,v_{n})\) y supongamos además que cada \(w_{j}\) es sustituible por \(t_{j}\) en \(\varphi.\) Entonces
adhocprefix(a)adhocsufix \(\varphi(t_{1},...,t_{k})\in F^{\tau}\)
adhocprefix(b)adhocsufix \(Li(\varphi(t_{1},...,t_{k}))\subseteq\{v_{1},...,v_{n}\}\)
adhocprefix(c)adhocsufix Si declaramos \(\varphi(t_{1},...,t_{k})=_{d}\varphi(t_{1},...,t_{k})(v_{1},...,v_{n})\), entonces para cada estructura \(\mathbf{A}\) y \(a_{1},...,a_{n}\in A\) se tiene \[\mathbf{A}\models\varphi(t_{1},...,t_{k})[a_{1},...,a_{n}]\text{ si y solo si }\mathbf{A}\models\varphi[t_{1}^{\mathbf{A}}[a_{1},...,a_{n}],...,t_{k}^{\mathbf{A}}[a_{1},...,a_{n}]]\]
Proof. Usaremos la Regla de Inducción desde 0. Para cada \(l\in\omega\) sea \(\mathrm{Enu}_{l}\) el siguiente enunciado:
adhocprefix\(\mathrm{Enu}_{l}\):adhocsufix Supongamos \(\varphi=_{d}\varphi(w_{1},...,w_{k})\in F_{l}^{\tau}\), \(t_{1}=_{d}t_{1}(v_{1},...,v_{n}),...,t_{k}=_{d}t_{k}(v_{1},...,v_{n})\) y supongamos además que cada \(w_{j}\) es sustituible por \(t_{j}\) en \(\varphi.\) Entonces
adhocprefix(a)adhocsufix \(\varphi(t_{1},...,t_{k})\in F^{\tau}\)
adhocprefix(b)adhocsufix \(Li(\varphi(t_{1},...,t_{k}))\subseteq\{v_{1},...,v_{n}\}\)
adhocprefix(c)adhocsufix Si declaramos \(\varphi(t_{1},...,t_{k})=_{d}\varphi(t_{1},...,t_{k})(v_{1},...,v_{n})\), entonces para cada estructura \(\mathbf{A}\) y \(a_{1},...,a_{n}\in A\) se tiene \[\mathbf{A}\models\varphi(t_{1},...,t_{k})[a_{1},...,a_{n}]\text{ si y solo si }\mathbf{A}\models\varphi[t_{1}^{\mathbf{A}}[a_{1},...,a_{n}],...,t_{k}^{\mathbf{A}}[a_{1},...,a_{n}]]\]
Antes de comenzar con lo que nos encomienda la Regla de Inducción desde \(0\) consideremos el siguiente enunciado:
adhocprefix\(\widetilde{\mathrm{Enu}_{l}}\):adhocsufix Supongamos \(\varphi=_{d}\varphi(w_{1},...,w_{k})\in F_{l}^{\tau}\), \(t_{1}=_{d}t_{1}(v_{1},...,v_{n}),...,t_{k}=_{d}t_{k}(v_{1},...,v_{n})\) y supongamos además que cada \(w_{j}\) es sustituible por \(t_{j}\) en \(\varphi\), cada \(v_{i}\) ocurre en algún \(t_{j}\), y que \(\{w_{1},...,w_{k}\}\subseteq Li(\varphi)\). Entonces
adhocprefix(a)adhocsufix \(\varphi(t_{1},...,t_{k})\in F^{\tau}\)
adhocprefix(b)adhocsufix \(Li(\varphi(t_{1},...,t_{k}))\subseteq\{v_{1},...,v_{n}\}\)
adhocprefix(c)adhocsufix Si declaramos \(\varphi(t_{1},...,t_{k})=_{d}\varphi(t_{1},...,t_{k})(v_{1},...,v_{n})\), entonces para cada estructura \(\mathbf{A}\) y \(a_{1},...,a_{n}\in A\) se tiene \[\mathbf{A}\models\varphi(t_{1},...,t_{k})[a_{1},...,a_{n}]\text{ si y solo si }\mathbf{A}\models\varphi[t_{1}^{\mathbf{A}}[a_{1},...,a_{n}],...,t_{k}^{\mathbf{A}}[a_{1},...,a_{n}]]\]
Es fácil (aunque largo) probar que cualquiera sea el \(l\in\omega\), se tiene que si \(\widetilde{\mathrm{Enu}_{l}}\) es verdadero, entonces \(\mathrm{Enu}_{l}\) lo es. Ahora sí hagamos lo que nos encomienda la Regla de Inducción desde \(0\).
Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Supongamos \(\varphi=_{d}\varphi(w_{1},...,w_{k})\in F_{0}^{\tau}\), \(t_{1}=_{d}t_{1}(v_{1},...,v_{n}),...,t_{k}=_{d}t_{k}(v_{1},...,v_{n})\) y supongamos además que cada \(w_{j}\) es sustituible por \(t_{j}\) en \(\varphi.\) Hay dos casos.
Caso \(\varphi=(t\equiv s)\), con \(t,s\in T^{\tau}\). Nótese que nuestra Convención Notacional 6 nos dice que tenemos implícitamente hecha las declaraciones \(t=_{d}t(w_{1},...,w_{k})\) y \(s=_{d}s(w_{1},...,w_{k})\). Ahora es fácil concluir que (a), (b) y (c) son ciertas para \(\varphi,t_{1},...,t_{k}\) usando el Teorema de Reemplazo para Términos.
Caso \(\varphi=r(s_{1},...,s_{m})\), con \(r\in\mathcal{R}_{m}\) y \(s_{1},...,s_{m}\in T^{\tau}\). La prueba es similar a la del caso anterior.
Prueba de que si \(\mathrm{Enu}_{l}\) es verdadero entonces \(\mathrm{Enu}_{l+1}\) lo es. Supongamos que vale \(\mathrm{Enu}_{l}\). En lugar de probar que vale \(\mathrm{Enu}_{l+1}\), probaremos que vale \(\widetilde{\mathrm{Enu}_{l+1}}\). Supongamos entonces \(\varphi=_{d}\varphi(w_{1},...,w_{k})\in F_{l+1}^{\tau}\), \(t_{1}=_{d}t_{1}(v_{1},...,v_{n}),...,t_{k}=_{d}t_{k}(v_{1},...,v_{n})\) y supongamos además que cada \(w_{j}\) es sustituible por \(t_{j}\) en \(\varphi\), cada \(v_{i}\) ocurre en algún \(t_{j}\), y que \(\{w_{1},...,w_{k}\}\subseteq Li(\varphi)\). Probaremos que se dan (a), (b) y (c) para \(\varphi,t_{1},...,t_{k}\). Por el Lema de Lectura Única de Fórmulas Declaradas hay varios casos.
Caso \(\varphi=(t\equiv s)\), con \(t,s\in T^{\tau}\). Ya fue probado en la prueba de \(\mathrm{Enu}_{0}\).
Caso \(\varphi=r(s_{1},...,s_{m})\), con \(r\in\mathcal{R}_{m}\) y \(s_{1},...,s_{m}\in T^{\tau}\). Ya fue probado en la prueba de \(\mathrm{Enu}_{0}\).
Caso \(\varphi=(\varphi_{1}\vee\varphi_{2})\), con \(\varphi_{1},\varphi_{2}\in F^{\tau}\). Ya que \(\varphi\in F_{l+1}^{\tau}\), el Lema de Lectura Única de Fórmulas Declaradas nos asegura que \(\varphi_{1},\varphi_{2}\in F_{l}^{\tau}\). Nuestra Convención Notacional 6 nos dice que tenemos implícitamente hecha las declaraciones \(\varphi_{1}=_{d}\varphi_{1}(w_{1},...,w_{k})\) y \(\varphi_{2}=_{d}\varphi_{2}(w_{1},...,w_{k})\). Ya que \(\mathrm{Enu}_{l}\) es verdadero y que \(\varphi_{1},\varphi_{2}\in F_{l}^{\tau}\), tenemos que se dan las siguientes propiedades:
adhocprefix(i)adhocsufix \(\varphi_{i}(t_{1},...,t_{k})\in F^{\tau}\), para \(i=1,2\)
adhocprefix(ii)adhocsufix \(Li(\varphi_{i}(t_{1},...,t_{k}))\subseteq\{v_{1},...,v_{n}\}\), para \(i=1,2\)
adhocprefix(iii)adhocsufix Para \(i=1,2\), si declaramos \(\varphi_{i}(t_{1},...,t_{k})=_{d}\varphi(t_{1},...,t_{k})(v_{1},...,v_{n})\), entonces para cada estructura \(\mathbf{A}\) y \(a_{1},...,a_{n}\in A\) se tiene \[\mathbf{A}\models\varphi_{i}(t_{1},...,t_{k})[a_{1},...,a_{n}]\text{ si y solo si }\mathbf{A}\models\varphi_{i}[t_{1}^{\mathbf{A}}[a_{1},...,a_{n}],...,t_{k}^{\mathbf{A}}[a_{1},...,a_{n}]]\]
Usando (i), (ii) y (iii) es fácil probar que se cumplen (a), (b) y (c) para \(\varphi,t_{1},...,t_{k}\).
Caso \(\varphi=\forall w\varphi_{1}\), con \(\varphi_{1}\in F_{l}^{\tau}\) y \(w\not\in\{w_{1},...,w_{k}\}\). Ya que \(\{w_{1},...,w_{k}\}\subseteq Li(\varphi)\) tenemos que cada \(w_{j}\in Li(\varphi_{1})\). Además nótese que \(w\not\in\{v_{1},...,v_{n}\}\) ya que de lo contrario \(w\) ocurriría en algún \(t_{j}\), y entonces \(w_{j}\) no sería sustituible por \(t_{j}\) en \(\varphi\). Sean \[\begin{array}{ccc} \tilde{t}_{1} & = & t_{1}\\ & \vdots\\ \tilde{t}_{k} & = & t_{k}\\ \tilde{t}_{k+1} & = & w \end{array}\] Declaremos \[\tilde{t}_{j}=_{d}\tilde{t}_{j}(v_{1},...,v_{n},w)\] Nótese que nuestra Convención Notacional 6 nos dice que tenemos implícitamente hecha la declaración \(\varphi_{1}=_{d}\varphi_{1}(w_{1},...,w_{k},w)\). Ya que \(\mathrm{Enu}_{l}\) es verdadero y \(\varphi_{1}\in F_{l}^{\tau}\), tenemos que se dan las siguientes propiedades:
adhocprefix(i)adhocsufix \(\varphi_{1}(\tilde{t}_{1},...,\tilde{t}_{k},\tilde{t}_{k+1})\in F^{\tau}\)
adhocprefix(ii)adhocsufix \(Li(\varphi_{1}(\tilde{t}_{1},...,\tilde{t}_{k},\tilde{t}_{k+1}))\subseteq\{v_{1},...,v_{n},w\}\)
adhocprefix(iii)adhocsufix Si declaramos \(\varphi_{1}(\tilde{t}_{1},...,\tilde{t}_{k},\tilde{t}_{k+1})=_{d}\varphi_{1}(\tilde{t}_{1},...,\tilde{t}_{k},\tilde{t}_{k+1})(v_{1},...,v_{n},w)\), entonces para cada estructura \(\mathbf{A}\) y \(a_{1},...,a_{n},a\in A\) se tiene \[\mathbf{A}\models\varphi_{1}(\tilde{t}_{1},...,\tilde{t}_{k},\tilde{t}_{k+1})[a_{1},...,a_{n},a]\text{ si y solo si }\mathbf{A}\models\varphi_{1}[\tilde{t}_{1}^{\mathbf{A}}[a_{1},...,a_{n},a],...,\tilde{t}_{k}^{\mathbf{A}}[a_{1},...,a_{n},a],\tilde{t}_{k+1}^{\mathbf{A}}[a_{1},...,a_{n},a]]\]
Además \[\varphi_{1}(\tilde{t}_{1},...,\tilde{t}_{k},\tilde{t}_{k+1})=\varphi_{1}(t_{1},...,t_{k},w)\] O sea que (i) y (ii) claramente implican que \(\varphi(t_{1},...,t_{k})\in F^{\tau}\) y \[Li(\varphi(t_{1},...,t_{k}))\subseteq\{v_{1},...,v_{n}\}\] lo cual prueba (a) y (b) para \(\varphi,t_{1},...,t_{k}\). Para probar que vale (c) para \(\varphi,t_{1},...,t_{k}\), declaremos \(\varphi(t_{1},...,t_{k})=_{d}\varphi(t_{1},...,t_{k})(v_{1},...,v_{n})\). Se tiene que \[\begin{array}{c} \mathbf{A}\models\varphi(t_{1},...,t_{k})\mathbf{[}\vec{a}]\\ \Updownarrow\\ \mathbf{A}\models\varphi_{1}(\tilde{t}_{1},...,\tilde{t}_{k},\tilde{t}_{k+1})[\vec{a},a]\text{, para todo }a\in A\\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \Updownarrow\ \text{(por (iii))}\\ \mathbf{A}\models\varphi_{1}[\tilde{t}_{1}^{\mathbf{A}}[\vec{a},a],...,\tilde{t}_{k}^{\mathbf{A}}[\vec{a},a],\tilde{t}_{k+1}^{\mathbf{A}}[\vec{a},a]]\text{, para todo }a\in A\\ \Updownarrow\\ \mathbf{A}\models\varphi_{1}[t_{1}^{\mathbf{A}}[\vec{a}],...,t_{k}^{\mathbf{A}}[\vec{a}],a]\text{, para todo }a\in A\\ \Updownarrow\\ \mathbf{A}\models\varphi[t_{1}^{\mathbf{A}}[\vec{a}],...,t_{k}^{\mathbf{A}}[\vec{a}]] \end{array}\] lo cual prueba (c).
Dejamos al lector los casos restantes.
Veamos un par de aplicaciones del teorema anterior. Recordemos que un término \(t\in T^{\tau}\) es llamado cerrado si ninguna variable es subtérmino de \(t\).
7.4. Supongamos \(\varphi=_{d}\varphi(w_{1},...,w_{k})\) y \(t_{1},...,t_{k}\) son términos cerrados. Entonces \(\varphi(t_{1},...,t_{k})\) es una sentencia
Proof. Podemos declarar \(t_{i}=_{d}t_{i}()\) para cada \(i\) y usar (a) y (b) del teorema.
7.5. Supongamos \(\varphi=_{d}\varphi(w)\) y sea \(t\) un término cerrado. Entonces \(\varphi(t)\) es una sentencia y una ves declarado \(t=_{d}t()\) se tiene que \[\mathbf{A}\models\varphi(t)\text{ si y solo si }\mathbf{A}\models\varphi[t^{\mathbf{A}}[]]\] para cada estructura \(\mathbf{A}\)
Ejemplo: Sea \(\tau=(\emptyset,\{f\},\emptyset,\{(f,1)\})\). Sean \(\varphi=\exists v_{1}(f(v_{1})\equiv w_{1})\) y \(t=v_{1}\), donde \(v_{1}\) y \(w_{1}\) son variables distintas. Declaremos \(\varphi=_{d}\varphi(w_{1})\) y \(t=_{d}t(v_{1})\). Nótese que \(w_{1}\) no es sustituible en \(\varphi\) por \(t\), por lo cual el teorema anterior no se puede aplicar. De hecho la conclusión del teorema no se da en este caso ya que puede verse fácilmente que, cualesquiera sea la estructura de tipo \(\tau\), \(\mathbf{A}\) y \(a_{1}\in A\), tenemos que:
\(\mathbf{A}\models\varphi(t)[a_{1}]\) si y solo si \(f^{\mathbf{A}}\) tiene un punto fijo, es decir, \(f^{\mathbf{A}}(a)=a\), para algún \(a\in A\)
\(\mathbf{A}\models\varphi[t^{\mathbf{A}}[a_{1}]]\) si y solo si \(a_{1}\) esta en la imagen de \(f^{\mathbf{A}}\)
las cuales son condiciones claramente no equivalentes.