Probaremos dos teoremas muy importantes que en algun sentido nos dicen que el reemplazo sintactico se lleva bien con la semantica. Usaremos la notacion declaratoria para expresarlos ya que los vuelve mucho mas accesibles e intuitivos.
7.4. 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 Todas las variables de \(t(s_{1},...,s_{k})\) estan en \(\{v_{1},...,v_{n}\}\)
adhocprefix(b)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. Probaremos que se dan (a) y (b), por induccion en el \(l\) tal que \(t\in T_{l}^{\tau}\). El caso \(l=0\) es dejado al lector. Supongamos entonces que el teorema vale siempre que \(t\in T_{l}^{\tau}\) y veamos que entonces vale cuando \(t\in T_{l+1}^{\tau}-T_{l}^{\tau}\). Por el Lema 7.24 hay \(f\in\mathcal{F}_{m}\) y \(t_{1},...,t_{m}\) terminos tales \(t=f(t_{1},...,t_{m})\) y las variables que ocurren en cada \(t_{i}\) estan en \(\{w_{1},...,w_{k}\}\). Por la unicidad de la lectura de terminos tenemos que \(t_{1},...,t_{m}\in T_{l}^{\tau}\) (por que?). Notese que por nuestra Convencion 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})\] Por HI tenemos que las variables de cada \(t_{i}(s_{1},...,s_{k})\) estan en \(\{v_{1},...,v_{n}\}\), lo cual nos permite hacer las siguientes declaraciones: \[t_{i}(s_{1},...,s_{k})=_{d}t_{i}(s_{1},...,s_{k})(v_{1},...,v_{n}),\text{ }i=1,...,m\] Por HI tenemos entonces 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\] Ya que las variables de cada \(t_{i}(s_{1},...,s_{k})\) estan en \(\{v_{1},...,v_{n}\}\), tenemos que las variables de \(t(s_{1},...,s_{k})=f(t_{1}(s_{1},...,s_{k}),...,t_{m}(s_{1},...,s_{k}))\) estan en \(\{v_{1},...,v_{n}\}\). Declaremos entonces \(t(s_{1},...,s_{k})=_{d}t(s_{1},...,s_{k})(v_{1},...,v_{n})\). Solo nos falta probar 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}]].\] lo cual se detalla a continuacion \[\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}\]
Para expresar este teorema necesitaremos dar una definicion que garantice que cuando reemplazamos una variable libre \(v\) por otra variable \(w\) en una formula, el significado de la formula no se altere. Por supuesto esto es solo una idea y a continuacion daremos el concepto en forma precisa. Antes el concepto de alcance el cual esta emparentado con el de sustitucion de variables.
7.28. Si \(Qv\) ocurre en \(\varphi\) a partir de \(i\), entonces hay una unica formula \(\psi\) tal que \(Qv\psi\) ocurre en \(\varphi\) a partir de \(i\).
Proof. Por induccion en el \(k\) tal que \(\varphi\in F^{\tau}\).
Dada una ocurrencia de \(Qv\) en una formula \(\varphi\), la formula \(\psi\) del lema anterior sera llamada el alcance de dicha ocurrencia en \(\varphi\). Notese 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 subformula de la forma \(Qw\psi\) en \(\varphi\). En otras palabras \(v\) no sera sustituible por \(w\) en \(\varphi\) cuando alguna ocurrencia libre de \(v\) en \(\varphi\) suceda dentro de una ocurrencia en \(\varphi\) de una formula de la forma \(Qw\psi\). Notese que puede suceder que \(v\) sea sustituible por \(w\) en \(\varphi\) y que sin envargo haya una subformula de la forma \(Qw\psi\) para la cual \(v\in Li(Qw\psi)\). Dejamos como ejercicio encontrar un ejemplo de esta situacion.
Usando lemas anteriores podemos ver que se dan las siguientes propiedades:
adhocprefix(1)adhocsufix Si \(\varphi\) es atomica, 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}\)
Notese que las propiedades (1),...,(7) pueden usarse para dar una definicion recursiva de la relacion \("v\) \(\mathit{es\ sustituible\ por\ }w\mathit{\ en}\) \(\varphi"\).
Dado un termino \(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. 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 ademas que cada \(w_{j}\) es sustituible por \(t_{j}\) en \(\varphi.\) Entonces
adhocprefix(a)adhocsufix \(Li(\varphi(t_{1},...,t_{k}))\subseteq\{v_{1},...,v_{n}\}\)
adhocprefix(b)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 \(\vec{a}\in A^{n}\) se tiene \[\mathbf{A}\models\varphi(t_{1},...,t_{k})[\vec{a}]\text{ si y solo si }\mathbf{A}\models\varphi[t_{1}^{\mathbf{A}}[\vec{a}],...,t_{k}^{\mathbf{A}}[\vec{a}]]\]
Proof. Probaremos que se dan (a) y (b), por induccion en el \(l\) tal que \(\varphi\in F_{l}^{\tau}.\) El caso \(l=0\) es una consecuencia directa del Teorema 7.4. Supongamos (a) y (b) valen para cada \(\varphi\in F_{l}^{\tau}\) y sea \(\varphi\in F_{l+1}^{\tau}-F_{l}^{\tau}.\) Notese que se puede suponer que cada \(v_{i}\) ocurre en algun \(t_{i}\), y que cada \(w_{i}\in Li(\varphi)\), ya que para cada \(\varphi\), el caso general se desprende del caso con estas restricciones. Hay varios casos
CASO \(\varphi=\forall w\varphi_{1}\), con \(w\not\in\{w_{1},...,w_{k}\}\).
Notese que cada \(w_{j}\in Li(\varphi_{1})\). Ademas notese que \(w\not\in\{v_{1},...,v_{n}\}\) ya que de lo contrario \(w\) ocurriria en algun \(t_{j}\), y entonces \(w_{j}\) no seria 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)\] Notese que nuestra Convencion Notacional 6 nos dice que tenemos implicitamente hecha la declaracion \(\varphi_{1}=_{d}\varphi_{1}(w_{1},...,w_{k},w)\). Por (a) de la hipotesis inductiva tenemos que \[Li(\varphi_{1}(t_{1},...,t_{k},w))=Li(\varphi_{1}(\tilde{t}_{1},...,\tilde{t}_{k},\tilde{t}_{k+1}))\subseteq\{v_{1},...,v_{n},w\}\] y por lo tanto \[Li(\varphi(t_{1},...,t_{k}))\subseteq\{v_{1},...,v_{n}\}\] lo cual prueba (a). Finalmente para probar (b) 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 HI)}\\ \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 pueba (b). Dejamos al lector los casos restantes.
adhocprefixEjemplo:adhocsufix 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})\). Notese que \(w_{1}\) no es sustituible en \(\varphi\) por \(t\), por lo cual el teorema anterior no se puede aplicar. De hecho la conclusion del teorema no se da en este caso ya que puede verse facilmente 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 pto fijo, es decir, \(f^{\mathbf{A}}(a)=a\), para algun \(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.