7.13 Teorías de Primer Orden

En esta sección nos avocaremos a dar una solución al punto (3) de nuestro Programa de Lógica Matemática. O sea nos abocaremos al siguiente problema:

1. adhocprefix(3)adhocsufix Dar un modelo matemático del concepto de prueba elemental en una teoría elemental.

Este problema involucra el concepto de teoría elemental definido en la Sección Teorías Elementales y Pruebas Elementales, el cual es intuitivo y no fue definido en forma precisa ya que depende del concepto de sentencia elemental pura de tipo \(\tau\). O sea que un primer paso en la resolución de (3) será dar un modelo matemático del concepto de teoría elemental. Recordemos que una teoría elemental es por definición un par \((\Sigma,\tau)\) tal que \(\tau\) es un tipo cualquiera y \(\Sigma\) es un conjunto de sentencias elementales puras de tipo \(\tau\). Dado que ya tenemos nuestro modelo matemático para las sentencias elementales puras de tipo \(\tau\) (i.e. las sentencias de tipo \(\tau\)), podemos dar el siguiente modelo matemático del concepto de teoría elemental:

Una teoría (de primer orden) será un par \((\Sigma,\tau)\), donde \(\tau\) es un tipo y \(\Sigma\) es un conjunto de sentencias de tipo \(\tau\). Esto ya es un buen comienzo en la resolución del punto (3) pero aun nos queda por hacer lo mas complicado.

Dada una teoría de primer orden \((\Sigma,\tau)\), los elementos de \(\Sigma\) serán llamados axiomas propios de \((\Sigma,\tau)\). Un modelo de \((\Sigma,\tau)\) será una estructura de tipo \(\tau\) la cual satisfaga todos los axiomas propios de \((\Sigma,\tau)\).

Algunos ejemplos de teorías de primer orden:

La Teoría \(Po\). Sea \[Po=(\{\mathrm{A}_{\leq R},\mathrm{A}_{\leq T},\mathrm{A}_{\leq A}\},\tau_{Po})\] donde \(\tau_{Po}\) es el tipo de los posets, es decir \((\emptyset,\emptyset,\{\leq\},\{(\leq,2)\})\) y \[\begin{aligned} \mathrm{A}_{\leq R} & =\forall x_{1}\;\mathrm{\leq}(x_{1},x_{1})\\ \mathrm{A}_{\leq T} & =\forall x_{1}\forall x_{2}\forall x_{3}\;((\mathrm{\leq}(x_{1},x_{2})\wedge\mathrm{\leq}(x_{2},x_{3}))\rightarrow\mathrm{\leq}(x_{1},x_{3}))\\ \mathrm{A}_{\leq A} & =\forall x_{1}\forall x_{2}\;((\mathrm{\leq}(x_{1},x_{2})\wedge\mathrm{\leq}(x_{2},x_{1}))\rightarrow(x_{1}\equiv x_{2})) \end{aligned}\] Nótese que una estructura \(\mathbf{A}\) de tipo \(\tau_{Po}\) es un modelo de \(Po\) si y solo si \(\leq^{\mathbf{A}}\) es un orden parcial sobre \(A\). Estrictamente hablando un modelo de \(Po\) no es un poset ya que es un par \((A,i)\) donde \(A\) es un conjunto no vacío e \(i\) es una función con dominio \(\{\leq\}\) tal que \(i(\leq)\) es un orden parcial sobre \(A\). Es decir, un modelo de \(Po\) es un par \((A,\{(\leq,R)\})\) donde \(A\) es un conjunto no vacío y \(R\) es un orden parcial sobre \(A\). De todas maneras debería quedar claro que en esencia un poset y un modelo de \(Po\) son la misma cosa por lo cual llamaremos a \(Po\) la teoría de los posets y muchas veces nos referiremos a los modelos de \(Po\) como si fueran posets. Dejamos al lector el ejercicio de encontrar una biyección natural entre la clase de los modelos de \(Po\) y la clase de los posets.

La teoría \(RetCua\). Sea \(\tau_{RetCua}=(\emptyset,\{\mathsf{s}^{2},\mathsf{i}^{2}\},\{\leq^{2}\},a)\) y sea \(\Sigma_{RetCua}\) el siguiente conjunto de sentencias: \[\begin{aligned} \mathrm{A}_{\leq R} & =\forall x_{1}\;\mathrm{\leq}(x_{1},x_{1})\\ \mathrm{A}_{\leq T} & =\forall x_{1}\forall x_{2}\forall x_{3}\;((\mathrm{\leq}(x_{1},x_{2})\wedge\mathrm{\leq}(x_{2},x_{3}))\rightarrow\mathrm{\leq}(x_{1},x_{3}))\\ \mathrm{A}_{\leq A} & =\forall x_{1}\forall x_{2}\;((\mathrm{\leq}(x_{1},x_{2})\wedge\mathrm{\leq}(x_{2},x_{1}))\rightarrow(x_{1}\equiv x_{2}))\\ \mathrm{A}_{\mathsf{s}esC} & =\forall x_{1}\forall x_{2}\;(\mathrm{\leq}(x_{1},\mathsf{s}(x_{1},x_{2}))\wedge\mathrm{\leq}(x_{2},\mathsf{s}(x_{1},x_{2})))\\ \mathrm{A}_{\mathsf{s}\leq C} & =\forall x_{1}\forall x_{2}\forall x_{3}\;\left((\mathrm{\leq}(x_{1},x_{3})\wedge\mathrm{\leq}(x_{2},x_{3}))\rightarrow\mathrm{\leq}(\mathsf{s}(x_{1},x_{2}),x_{3}\right))\\ \mathrm{A}_{\mathsf{i}esC} & =\forall x_{1}\forall x_{2}\;(\mathrm{\leq}(\mathsf{i}(x_{1},x_{2}),x_{1})\wedge\mathrm{\leq}(\mathsf{i}(x_{1},x_{2}),x_{2}))\\ \mathrm{A}_{\mathsf{i}\geq C} & =\forall x_{1}\forall x_{2}\forall x_{3}\;\left((\mathrm{\leq}(x_{3},x_{1})\wedge\mathrm{\leq}(x_{3},x_{2}))\rightarrow\mathrm{\leq}(x_{3},\mathsf{i}(x_{1},x_{2}))\right) \end{aligned}\] Definamos \(RetCua=(\Sigma_{RetCua},\tau_{RetCua})\). Obviamente los modelos de esta teoría son esencialmente reticulados cuaterna en el sentido que una estructura \(\mathbf{A}\) de tipo \(\tau_{RetCua}\) es un modelo de \(RetCua\) si y solo si \((A,\mathsf{s}^{\mathbf{A}},\mathsf{i}^{\mathbf{A}},\leq^{\mathbf{A}})\) es un reticulado cuaterna. Llamaremos a \(RetCua\) la teoría de los reticulados cuaterna y muchas veces nos referiremos a los modelos de \(RetCua\) como si fueran reticulados cuaterna.

7.13.1 Definición del Concepto de Prueba Formal

Recomendamos al lector repasar el concepto de prueba elemental en una teoría elemental, dado en el Capítulo Estructuras y su Lenguaje Elemental. Aquí daremos un modelo matemático de dicho concepto. Tal como lo hemos visto en numerosos ejemplos, una prueba es una sucesión de sentencias junto con una sucesión de "justificaciones" las cuales van explicando o justificando por que es licito que cada una de dichas sentencias aparezca en la sucesión. Por supuesto nuestra definición será precisa y matemática por lo que deberemos trabajar bastante para poder escribirla correctamente. Como objeto matemático una prueba resultara ser un par ordenado de palabras cuya primera coordenada codificara en forma natural la sucesión de sentencias y su segunda coordenada codificará la sucesión de justificaciones.

La formalización matemática del concepto de prueba elemental es uno de los grandes logros de la ciencia moderna y este hecho se debe en gran medida a que si elegimos bien la teoría, las pruebas elementales no son ni más ni menos que las pruebas de la matemática misma por lo cual se tiene una definición matemática que modeliza a la deducción matemática real!

7.13.1.1 Reglas Universales

Muchas veces los matemáticos cuando realizan pruebas usan de manera tácita reglas de deducción. Por ejemplo si un matemático ha probado una sentencia \(\varphi\) y antes había probado la sentencia \((\varphi\rightarrow\psi)\), entonces dicho matemático haciendo referencia a estas dos sentencias concluye que también es verdadera la sentencia \(\psi\). Por supuesto este uso es tácito (i.e. sin ninguna explicación) debido a su obviedad y solidez. Y esta obviedad y solidez básicamente se debe a que cualquier estructura que haga verdaderas a las sentencias \(\varphi\) y \((\varphi\rightarrow\psi)\) también hará verdadera a la sentencia \(\psi\). Ya que nosotros estamos haciendo un modelo matemático de la deducción elemental de los matemáticos les pondremos nombre a dichas reglas usadas tácitamente por los matemáticos. Por ejemplo la anterior se llamara Modus Ponens. También diremos que \(\psi\) se deduce por la regla Modus Ponens de \(\varphi\) y \((\varphi\rightarrow\psi)\). A continuación describiremos varias reglas que, como Modus Ponens, tienen la propiedad común de ser universales en el sentido que preservan la verdad (i.e. la sentencia deducida es verdadera en cada estructura que hace verdaderas a aquellas sentencias a partir de las cuales se la deduce).

Para hacer las cosas en forma más precisa matemáticamente hablando, representaremos dichas reglas con conjuntos.

Algunas Reglas Proposicionales

Algunas reglas serán llamadas proposicionales ya que se basan solo en la fisonomía de las sentencias en relación a los símbolos proposicionales (\(\wedge\text{ }\vee\text{ }\rightarrow\text{ }\leftrightarrow\text{ }\neg\)). (No daremos una definición matemática precisa de este concepto). Veamos algunas.

Sean \[\begin{aligned} ModPon^{\tau} & =\{(\varphi,(\varphi\rightarrow\psi),\psi):\varphi,\psi\in S^{\tau}\}\\ ConjInt^{\tau} & =\{(\varphi,\psi,(\varphi\wedge\psi)):\varphi,\psi\in S^{\tau}\}\\ EquivInt^{\tau} & =\{((\varphi\rightarrow\psi),(\psi\rightarrow\varphi),(\varphi\leftrightarrow\psi)):\varphi,\psi\in S^{\tau}\}\\ DisjElim^{\tau} & =\{(\lnot\varphi,(\varphi\vee\psi),\psi):\varphi,\psi\in S^{\tau}\}\cup\{(\lnot\psi,(\varphi\vee\psi),\varphi):\varphi,\psi\in S^{\tau}\} \end{aligned}\] Diremos que \(\varphi\) se deduce de \(\psi_{1}\) y \(\psi_{2}\) por la regla de Modus Ponens (resp. conjunción-introducción, equivalencia-introducción, disjunción-eliminación), con respecto a \(\tau\) para expresar que \((\psi_{1},\psi_{2},\varphi)\in ModPon^{\tau}\) (resp. \((\psi_{1},\psi_{2},\varphi)\in ConjInt^{\tau}\), \((\psi_{1},\psi_{2},\varphi)\in EquivInt^{\tau}\), \((\psi_{1},\psi_{2},\varphi)\in DisjElim^{\tau}\)).

Sean \[\begin{aligned} Evoc^{\tau} & =\{(\varphi,\varphi):\varphi\in S^{\tau}\}\\ ConjElim^{\tau} & =\{((\varphi\wedge\psi),\varphi):\varphi,\psi\in S^{\tau}\}\cup\{((\varphi\wedge\psi),\psi):\varphi,\psi\in S^{\tau}\}\\ EquivElim^{\tau} & =\{((\varphi\leftrightarrow\psi),(\varphi\rightarrow\psi)):\varphi,\psi\in S^{\tau}\}\cup\{((\varphi\leftrightarrow\psi),(\psi\rightarrow\varphi)):\varphi,\psi\in S^{\tau}\}\\ DisjInt^{\tau} & =\{(\varphi,(\varphi\vee\psi)):\varphi,\psi\in S^{\tau}\}\cup\{(\psi,(\varphi\vee\psi)):\varphi,\psi\in S^{\tau}\}\cup\{((\lnot\varphi\rightarrow\psi),(\varphi\vee\psi)):\varphi,\psi\in S^{\tau}\} \end{aligned}\] Diremos que \(\varphi\) se deduce de \(\psi\) por la regla de evocación (resp. conjunción-eliminación, equivalencia-eliminación, disjunción-introducción), con respecto a \(\tau\) para expresar que \((\psi,\varphi)\in Evoc^{\tau}\) (resp. \((\psi,\varphi)\in ConjElim^{\tau}\), \((\psi,\varphi)\in EquivElim^{\tau}\), \((\psi,\varphi)\in DisjInt^{\tau}\)).

Sea \[Absur^{\tau}=Absur1^{\tau}\cup Absur2^{\tau}\cup Absur3^{\tau}\] donde \[\begin{aligned} Absur1^{\tau} & =\{((\lnot\varphi\rightarrow(\psi\wedge\lnot\psi)),\varphi):\varphi,\psi\in S^{\tau}\}\\ Absur2^{\tau} & =\{((\varphi\rightarrow(\psi\wedge\lnot\psi)),\lnot\varphi):\varphi,\psi\in S^{\tau}\}\\ Absur3^{\tau} & =\{((\psi\wedge\lnot\psi),\varphi):\varphi,\psi\in S^{\tau}\} \end{aligned}\] Diremos que \(\varphi\) se deduce de \(\psi\) por la regla del absurdo, con respecto a \(\tau\) para expresar que \((\psi,\varphi)\in Absur^{\tau}\).

Sea \[DivPorCas^{\tau}=\{((\varphi_{1}\vee\varphi_{2}),(\varphi_{1}\rightarrow\psi),(\varphi_{2}\rightarrow\psi),\psi):\varphi_{1},\varphi_{2},\psi\in S^{\tau}\}\] Diremos que \(\varphi\) se deduce de \(\psi_{1}\), \(\psi_{2}\) y \(\psi_{3}\) por la regla de división por casos, con respecto a \(\tau\) para expresar que \((\psi_{1},\psi_{2},\psi_{3},\varphi)\in DivPorCas^{\tau}\).

Reglas de Conmutatividad y Transitividad

Sea \[Commut^{\tau}=Commut1^{\tau}\cup Commut2^{\tau}\] donde \[\begin{aligned} Commut1^{\tau} & =\{((t\equiv s),(s\equiv t)):s,t\in T_{c}^{\tau}\}\\ Commut2^{\tau} & =\{((\varphi\leftrightarrow\psi),(\psi\leftrightarrow\varphi)):\varphi,\psi\in S^{\tau}\} \end{aligned}\] Diremos que \(\varphi\) se deduce de \(\psi\) por la regla de conmutatividad, con respecto a \(\tau\) para expresar que \((\psi,\varphi)\in Commut^{\tau}\).

Sea \[Trans^{\tau}=Trans1^{\tau}\cup Trans2^{\tau}\cup Trans3^{\tau}\] donde \[\begin{aligned} Trans1^{\tau} & =\{((t\equiv s),(s\equiv u),(t\equiv u)):t,s,u\in T_{c}^{\tau}\}\\ Trans2^{\tau} & =\{((\varphi\rightarrow\psi),(\psi\rightarrow\Phi),(\varphi\rightarrow\Phi)):\varphi,\psi,\Phi\in S^{\tau}\}\\ Trans3^{\tau} & =\{((\varphi\leftrightarrow\psi),(\psi\leftrightarrow\Phi),(\varphi\leftrightarrow\Phi)):\varphi,\psi,\Phi\in S^{\tau}\} \end{aligned}\] Diremos que \(\varphi\) se deduce de \(\psi_{1}\)y \(\psi_{2}\) por la regla de transitividad, con respecto a \(\tau\) para expresar que \((\psi_{1},\psi_{2},\varphi)\in Trans^{\tau}\).

Reglas de Particularización y Existencia

Recordemos que si \(\tau\) es un tipo cualquiera, un término \(t\in T^{\tau}\) es llamado cerrado si ninguna variable es subtérmino de \(t\). Con \(T_{c}^{\tau}\) denotamos el conjunto formado por todos los términos cerrados.

Sean \[Partic^{\tau}=\{(\forall v\varphi(v),\varphi(t)):\varphi=_{d}\varphi(v)\in F^{\tau}\ \mathrm{y\ }t\in T_{c}^{\tau}\}\] \[Exist^{\tau}=\{(\varphi(t),\exists v\varphi(v)):\varphi=_{d}\varphi(v)\in F^{\tau}\ \mathrm{y\ }t\in T_{c}^{\tau}\}\] Nótese que cuando \(\varphi=_{d}\varphi(v)\in F^{\tau}\ \mathrm{y\ }t\in T_{c}^{\tau}\) se tiene que \(\varphi(t)\) es una sentencia. Esto es consecuencia de (a) y (b) del Teorema de Reemplazo para Fórmulas, si hacemos la declaración \(t=_{d}t()\). O sea que los conjuntos \(Partic^{\tau}\text{ y }Exist^{\tau}\) esta contenidos en \(S^{\tau}\times S^{\tau}\).

Diremos que \(\varphi\) se deduce de \(\psi\) por la regla de particularización (resp. existencia), con respecto a \(\tau\) para expresar que \((\psi,\varphi)\in Partic^{\tau}\) (resp. \((\psi,\varphi)\in Exist^{\tau}\)).

Regla de Reemplazo

Si \(t\) es un término y \(\varphi\) una fórmula, una ocurrencia de \(t\) en \(\varphi\) se llamara contigua cuando dicha ocurrencia no es a partir del primer símbolo de \(\varphi\) y además el símbolo anterior en \(\varphi\) a dicha ocurrencia es ya sea \(\forall\) o \(\exists\). Dicho de otra forma una ocurrencia de \(t\) en \(\varphi\) se llamara contigua cuando dicha ocurrencia este contenida en una ocurrencia de una palabra de la forma \(Qt\), con \(Q\in\{\forall,\exists\}\). Ya probamos en el Lema de Ocurrencias de Términos en Fórmulas que si reemplazamos una ocurrencia no contigua de un término en una fórmula, por otro término, el resultado es una fórmula.

Sea \[Reemp^{\tau}=Reemp1^{\tau}\cup Reemp2^{\tau}\] donde

\(Reemp1^{\tau}=\{(\forall v_{1}...\forall v_{n}(t\equiv s),\gamma,\tilde{\gamma}):s,t\in T^{\tau},\) \(Li((t\equiv s))\subseteq\{v_{1},...,v_{n}\}\),

\(\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ n\geq0,\text{ }\gamma,\tilde{\gamma}\in S^{\tau}\ \mathrm{y\ }\tilde{\gamma}=\mathrm{resultado\ de\ reemplazar\ en\ }\gamma\ \)

\(\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \mathrm{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ una\ ocurrencia\ no\ contigua\ de\ }t\ \mathrm{por\ }s\}\)

\(Reemp2^{\tau}=\{(\forall v_{1}...\forall v_{n}(\varphi\leftrightarrow\psi),\gamma,\tilde{\gamma}):\varphi,\psi\in F^{\tau}\), \(Li(\varphi)\cup Li(\psi)\subseteq\{v_{1},...,v_{n}\}\),

\(\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ n\geq0,\) \(\gamma,\tilde{\gamma}\in S^{\tau}\ \mathrm{y\ }\tilde{\gamma}=\mathrm{resultado\ de\ reemplazar\ en\ }\gamma\ \mathrm{una\ ocurrencia\ de\ }\varphi\ \mathrm{por\ }\psi\}\)

Diremos que \(\varphi\) se deduce de \(\psi_{1}\)y \(\psi_{2}\) por la regla de reemplazo, con respecto a \(\tau\), para expresar que \((\psi_{1},\psi_{2},\varphi)\in Reemp^{\tau}\).

Universalidad

Una regla \(R\) será llamada universal cuando se dé que si \(\varphi\) se deduce de \(\psi_{1},...,\psi_{k}\) por \(R\), entonces \(\left((\psi_{1}\wedge...\wedge\psi_{k})\rightarrow\varphi\right)\) es una sentencia universalmente válida. Nótese que la regla \(R\) será universal si cada ves que se dé que

1. adhocprefix-adhocsufix \(\varphi\) se deduce de \(\psi_{1},...,\psi_{k}\) por \(R\)

2. adhocprefix-adhocsufix \(\mathbf{A}\models\psi_{i}\), para cada \(i=1,...,k\)

se tiene que \(\mathbf{A}\models\varphi\).

Proof. Veamos que la regla de existencia es universal. Por definición, un par de \(Exist^{\tau}\) es siempre de la forma \((\varphi(t),\exists v\varphi(v))\), con \(\varphi=_{d}\varphi(v)\) y \(t\in T_{c}^{\tau}\). Sea \(\mathbf{A}\) una estructura de tipo \(\tau\) tal que \(\mathbf{A}\models\varphi(t)\), veremos que entonces \(\mathbf{A}\models\exists v\varphi(v)\). Declaremos \(t=_{d}t()\). Entonces ya que \(v\) es substituible por \(t\) en \(\varphi\), (c) del Teorema de Reemplazo para Fórmulas nos dice que \(\varphi(t)\) es una sentencia y que si declaramos \(\varphi(t)=_{d}\varphi(t)()\), entonces \[\mathbf{A}\models\varphi(t)[]\text{ si y solo si }\mathbf{A}\models\varphi[t^{\mathbf{A}}[]]\] Pero ya que \(\mathbf{A}\models\varphi(t)\), tenemos que \(\mathbf{A}\models\varphi(t)[]\) por lo cual \(\mathbf{A}\models\varphi[t^{\mathbf{A}}[]]\). Ahora podemos aplicar el Corolario 7.3 y obtener que \(\mathbf{A}\models\exists v\varphi(v)\).

Que la regla de particularización es universal se prueba en forma completamente análoga y es dejada al lector en un ejercicio.

Veamos que la regla de reemplazo es universal. Supongamos entonces que \((\psi_{1},\psi_{2},\varphi)\in Reemp^{\tau}=Reemp1^{\tau}\cup Reemp2^{\tau}\).

Para el caso en que \((\psi_{1},\psi_{2},\varphi)\in Reemp2^{\tau}\) basta con probar, usando la Regla de Inducción desde 0, que cualquiera sea el \(k\in\omega\), el siguiente enunciado es verdadero:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Supongamos que

   1. adhocprefix-adhocsufix \(\alpha\in F_{k}^{\tau}\) y \(\varphi_{1},\varphi_{2}\in F^{\tau}\)

   2. adhocprefix-adhocsufix \(\mathbf{A}\) es una estructura de tipo \(\tau\)

   3. adhocprefix-adhocsufix \(\overline{\alpha}=\) resultado de reemplazar en \(\alpha\) una ocurrencia de \(\varphi_{1}\) por \(\varphi_{2}\),

   4. adhocprefix-adhocsufix \(\mathbf{A}\models\varphi_{1}\left[\vec{a}\right]\) si y solo si \(\mathbf{A}\models\varphi_{2}\left[\vec{a}\right]\), para cada \(\vec{a}\in A^{\mathbf{N}}\).

   Entonces \(\mathbf{A}\models\alpha\left[\vec{a}\right]\) si y solo si \(\mathbf{A}\models\overline{\alpha}\left[\vec{a}\right]\), para cada \(\vec{a}\in A^{\mathbf{N}}\).

Hagamos lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Ya que \(\alpha\) es atómica, \(\alpha\) es la única subfórmula de \(\alpha\).

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos que vale \(\mathrm{Enu}_{k}\) y supongamos que

1. adhocprefix-adhocsufix \(\alpha\in F_{k+1}^{\tau}\) y \(\varphi_{1},\varphi_{2}\in F^{\tau}\)

2. adhocprefix-adhocsufix \(\mathbf{A}\) es una estructura de tipo \(\tau\)

3. adhocprefix-adhocsufix \(\overline{\alpha}=\) resultado de reemplazar en \(\alpha\) una ocurrencia de \(\varphi_{1}\) por \(\varphi_{2}\),

4. adhocprefix-adhocsufix \(\mathbf{A}\models\varphi_{1}\left[\vec{a}\right]\) si y solo si \(\mathbf{A}\models\varphi_{2}\left[\vec{a}\right]\), para cada \(\vec{a}\in A^{\mathbf{N}}\).

Probaremos que \(\mathbf{A}\models\alpha\left[\vec{a}\right]\) si y solo si \(\mathbf{A}\models\overline{\alpha}\left[\vec{a}\right]\), para cada \(\vec{a}\in A^{\mathbf{N}}\). Por definición de \(F_{k+1}^{\tau}\), hay varios casos.

Caso \(\alpha\in F_{k}^{\tau}\). Trivial ya que vale \(\mathrm{Enu}_{k}\).

Caso \(\alpha=\forall x_{i}\alpha_{1}\), con \(\alpha_{1}\in F_{k}^{\tau}\) y \(i\in\mathbf{N}\). Si \(\varphi_{1}=\alpha\), entonces la situación es fácil de probar. Si \(\varphi_{1}\neq\alpha\), entonces por el Lema de Ocurrencias de Fórmulas en Fórmulas la ocurrencia de \(\varphi_{1}\) en \(\alpha\), a reemplazar por \(\varphi_{2}\), sucede en \(\alpha_{1}\). Sea \(\overline{\alpha_{1}}=\) resultado de reemplazar en \(\alpha_{1}\) dicha ocurrencia de \(\varphi_{1}\) por \(\varphi_{2}\). O sea que \(\overline{\alpha}=\forall x_{i}\overline{\alpha_{1}}\). Ya que \(\alpha_{1}\in F_{k}^{\tau}\) y \(\mathrm{Enu}_{k}\) es verdadero, tenemos que

1. adhocprefix(*)adhocsufix \(\mathbf{A}\models\alpha_{1}\left[\vec{a}\right]\text{ si y solo si \ensuremath{\mathbf{A}}\models\ensuremath{\overline{\alpha_{1}}\left[\vec{a}\right]}},\)para cada \(\vec{a}\in A^{\mathbf{N}}\).

Fijemos un \(\vec{a}\in A^{\mathbf{N}}\). Se tiene que \[\begin{array}{cc} \mathbf{A}\models\alpha\left[\vec{a}\right]\\ \Updownarrow\\ \mathbf{A}\models\alpha_{1}\left[\downarrow_{i}^{a}(\vec{a})\right],\text{ para cada }a\in A\\ \Updownarrow & (\text{por }(*))\\ \mathbf{A}\models\overline{\alpha_{1}}\left[\downarrow_{i}^{a}(\vec{a})\right],\text{ para cada }a\in A\\ \Updownarrow\\ \mathbf{A}\models\overline{\alpha}\left[\vec{a}\right] \end{array}\] Caso \(\alpha=(\alpha_{1}\vee\alpha_{2})\), , con \(\alpha_{1},\alpha_{2}\in F_{k}^{\tau}\). Si \(\varphi_{1}=\alpha\), entonces la situación es fácil de probar. Si \(\varphi_{1}\neq\alpha\), entonces por el Lema de Ocurrencias de Fórmulas en Fórmulas la ocurrencia de \(\varphi_{1}\) en \(\alpha\), a reemplazar por \(\varphi_{2}\), sucede en \(\alpha_{1}\) o en \(\alpha_{2}\). Supongamos que sucede en \(\alpha_{2}\). Sea \(\overline{\alpha_{2}}=\) resultado de reemplazar en \(\alpha_{2}\) dicha ocurrencia de \(\varphi_{1}\) por \(\varphi_{2}\). O sea que \(\overline{\alpha}=(\alpha_{1}\vee\overline{\alpha_{2}})\). Ya que \(\alpha_{2}\in F_{k}^{\tau}\) y \(\mathrm{Enu}_{k}\) es verdadero, tenemos que

1. adhocprefix(**)adhocsufix \(\mathbf{A}\models\alpha_{2}\left[\vec{a}\right]\text{ si y solo si \ensuremath{\mathbf{A}}\models\ensuremath{\overline{\alpha_{2}}\left[\vec{a}\right]}},\)para cada \(\vec{a}\in A^{\mathbf{N}}\).

Fijemos un \(\vec{a}\in A^{\mathbf{N}}\). Se tiene que

\[\begin{array}{cc} \mathbf{A}\models\alpha\left[\vec{a}\right]\\ \Updownarrow\\ \mathbf{A}\models\alpha_{1}\left[\vec{a}\right]\text{ o }\mathbf{A}\models\alpha_{2}\left[\vec{a}\right]\\ \Updownarrow & (\text{por }(**))\\ \mathbf{A}\models\alpha_{2}\left[\vec{a}\right]\text{ o }\mathbf{A}\models\overline{\alpha_{2}}\left[\vec{a}\right]\\ \Updownarrow\\ \mathbf{A}\models\overline{\alpha}\left[\vec{a}\right] \end{array}\] Los demás casos son dejados al lector.

El caso en el que \((\psi_{1},\psi_{2},\varphi)\in Reemp1^{\tau}\), es consecuencia directa del siguiente resultado el cual es dejado como ejercicio.

1. adhocprefix(***)adhocsufix Supongamos \(s,t\in T^{\tau}\). Sea \(\gamma\in F^{\tau}\) y sea \[\tilde{\gamma}=\mathrm{resultado\ de\ reemplazar\ en\ }\gamma\ una\ ocurrencia\ no\ contigua\ de\ t\ \mathrm{por\ }s\] Entonces \(\tilde{\gamma}\in F^{\tau}\) y si \(\mathbf{A}\) es una estructura de tipo \(\tau\) tal que \(t^{\mathbf{A}}\left[\vec{a}\right]=s^{\mathbf{A}}\left[\vec{a}\right]\), para cada \(\vec{a}\in A^{\mathbf{N}}\), se tiene que \[\mathbf{A}\models\gamma\left[\vec{a}\right]\text{ si y solo si }\mathbf{A}\models\tilde{\gamma}\left[\vec{a}\right]\] para cada \(\vec{a}\in A^{\mathbf{N}}\)

El chequeo de la universalidad del resto de las reglas es mas directo y es dejado al lector.  

La Regla Generalización

Esta regla es muy usada por los matemáticos cuando pasan de haber probado cierta propiedad para un elemento fijo pero arbitrario a escribir que dicha propiedad se cumple para todos los elementos de la estructura en cuestión. Tomemos: \[Generaliz^{\tau}=\{(\varphi(c),\forall v\varphi(v)):\varphi=_{d}\varphi(v)\in F^{\tau},\ Li(\varphi)=\{v\}\ \mathrm{y\ }c\in\mathcal{C}\ \mathrm{no\ ocurre\ en}\ \varphi\}\] Es importante el siguiente

Proof. Nótese que \(c\) es el único nombre de constante que ocurre en \(\varphi_{1}\) y no ocurre en \(\varphi_{2}\)  

Escribiremos \((\varphi_{1},\varphi_{2})\in Generaliz^{\tau}\) vía \(c\) para expresar que \((\varphi_{1},\varphi_{2})\in Generaliz^{\tau}\) y que \(c\) es el único nombre de constante que ocurre en \(\varphi_{1}\) y no ocurre en \(\varphi_{2}\). Diremos que \(\varphi_{2}\) se deduce de \(\varphi_{1}\) por la regla de generalización con nombre de constante \(c\), con respecto a \(\tau\), para expresar que \((\varphi_{1},\varphi_{2})\in Generaliz^{\tau}\) vía \(c\).

La Regla de Elección

Otra regla muy usada por los matemáticos en sus pruebas elementales es aquella que le permite, una ves probada una sentencia que asegura la existencia de al menos un objeto con cierta propiedad, introducir un nuevo nombre para denotar alguno de esos objetos con tal propiedad. Tomemos \[Elec^{\tau}=\{(\exists v\varphi(v),\varphi(e)):\varphi=_{d}\varphi(v)\in F^{\tau},\ Li(\varphi)=\{v\}\ \mathrm{y\ }e\in\mathcal{C}\ \mathrm{no\ ocurre\ en}\ \varphi\}\] Es importante el siguiente

Proof. Nótese que \(e\) es el único nombre de constante que ocurre en \(\varphi_{2}\) y no ocurre en \(\varphi_{1}\).  

Escribiremos \((\varphi_{1},\varphi_{2})\in Elec^{\tau}\) vía \(e\) para expresar que \((\varphi_{1},\varphi_{2})\in Elec^{\tau}\) y que \(e\) es el único nombre de constante que ocurre en \(\varphi_{2}\) y no ocurre en \(\varphi_{1}\). Diremos que \(\varphi_{2}\) se deduce de \(\varphi_{1}\) por la regla de elección con nombre de constante \(e\), con respecto a \(\tau\) para expresar que \((\varphi_{1},\varphi_{2})\in Elec^{\tau}\) vía \(e\).

7.13.1.2 Axiomas Lógicos

Recordemos que dada una teoría \((\Sigma,\tau)\), los elementos de \(\Sigma\) son llamados axiomas propios y en general no son sentencias universalmente válidas.

En las pruebas formales será necesario usar ciertas verdades universales y obvias las cuales llamaremos axiomas lógicos. Mas concretamente, llamaremos axiomas lógicos de tipo \(\tau\) a todas las sentencias de alguna de las siguientes formas.

1. adhocprefix(1)adhocsufix \((t\equiv t)\), con \(t\in T_{c}^{\tau}\)

2. adhocprefix(2)adhocsufix \((Qv\varphi\leftrightarrow\varphi)\), con \(Q\in\{\forall,\exists\}\), \(v\in Var\) y \(\varphi\in S^{\tau}\)

3. adhocprefix(3)adhocsufix \((\lnot(\varphi\vee\psi)\leftrightarrow(\lnot\varphi\wedge\lnot\psi))\), con \(\varphi,\psi\in S^{\tau}\)

4. adhocprefix(4)adhocsufix \((\lnot(\varphi\wedge\psi)\leftrightarrow(\lnot\varphi\vee\lnot\psi))\), con \(\varphi,\psi\in S^{\tau}\)

5. adhocprefix(5)adhocsufix \((\lnot(\varphi\rightarrow\psi)\leftrightarrow(\varphi\wedge\lnot\psi))\), con \(\varphi,\psi\in S^{\tau}\)

6. adhocprefix(6)adhocsufix \((\lnot(\varphi\leftrightarrow\psi)\leftrightarrow((\varphi\wedge\lnot\psi)\vee(\lnot\varphi\wedge\psi)))\), con \(\varphi,\psi\in S^{\tau}\)

7. adhocprefix(7)adhocsufix \((\lnot\lnot\varphi\leftrightarrow\varphi)\), con \(\varphi\in S^{\tau}\)

8. adhocprefix(8)adhocsufix \((\lnot\forall v\gamma\leftrightarrow\exists v\lnot\gamma)\), con \(v\in Var\), \(\gamma\in F^{\tau}\) y \(Li(\gamma)\subseteq\{v\}\)

9. adhocprefix(9)adhocsufix \((\lnot\exists v\gamma\leftrightarrow\forall v\lnot\gamma)\), con \(v\in Var\), \(\gamma\in F^{\tau}\) y \(Li(\gamma)\subseteq\{v\}\)

Con \(AxLog^{\tau}\) denotaremos el conjunto \[\{\varphi\in S^{\tau}:\varphi\ \mathrm{es\ un\ axioma\ logico\ de\ tipo\ }\tau\}\] Nótese que hay infinitos axiomas lógicos de tipo \(\tau\), es decir el conjunto \(AxLog^{\tau}\) es un conjunto infinito de palabras. Por ejemplo, el formato dado en (4) produce una cantidad infinita de axiomas lógicos, a saber todas las sentencias de la forma \((\lnot(\varphi\wedge\psi)\leftrightarrow(\lnot\varphi\vee\lnot\psi))\), donde \(\varphi\) y \(\psi\) son cualquier par de sentencias de tipo \(\tau\). O sea que cada renglón de arriba corresponde no a un axioma sino a una cantidad infinita de axiomas, todos con un formato determinado. Se le suelen llamar Axiomas Esquema a este tipo de formatos que describen una morfología de cierta familia de axiomas.

El axioma esquema dado en (1) sin dudas describe la familia de axiomas mas básicos que uno puede imaginar. Llamaremos a este axioma esquema el Axioma Esquema de Identidad. Al axioma esquema dado en (2) lo llamaremos el Axioma Esquema de Cuantificación Vacua. Al axioma esquema dado en (3) lo llamaremos el Axioma Esquema de Negación del \(\vee\). Al dado en (4) lo llamaremos el Axioma Esquema de Negación del \(\wedge\). Al dado en (5) lo llamaremos el Axioma Esquema de Negación del \(\rightarrow\). Al dado en (6) lo llamaremos el Axioma Esquema de Negación del \(\leftrightarrow\). Al dado en (7) lo llamaremos el Axioma Esquema de Negación de \(\neg\). Al dado en (8) lo llamaremos el Axioma Esquema de Negación del \(\forall\). Al dado en (9) lo llamaremos el Axioma Esquema de Negación del \(\exists\).

Nótese que los 7 últimos axiomas esquema nos dan formas equivalentes a las negaciones de cada uno de los formatos posibles de fórmulas no atómicas dados en el Teorema de Lectura Única de Fórmulas. Ya veremos en Mecánicas de negación como estos axiomas se pueden usar para simular los comienzos de pruebas por el absurdo que usualmente hacen los matemáticos.

1. adhocprefixEjercicio:adhocsufix Pruebe que cada sentencia de \(AxLog^{\tau}\) es universalmente válida

7.13.1.3 Justificaciones

Llamaremos numerales a los siguientes símbolos \[0\ 1\ 2\ 3\ 4\ 5\ 6\ 7\ 8\ 9\] Usaremos \(Num\) para denotar el conjunto de numerales. Nótese que \(Num\cap\omega=\emptyset\). Sea \(Sig:Num^{\ast}\rightarrow Num^{\ast}\) definida de la siguiente manera \[\begin{aligned} Sig(\varepsilon) & =1\\ Sig(\alpha0) & =\alpha1\\ Sig(\alpha1) & =\alpha2\\ Sig(\alpha2) & =\alpha3\\ Sig(\alpha3) & =\alpha4\\ Sig(\alpha4) & =\alpha5\\ Sig(\alpha5) & =\alpha6\\ Sig(\alpha6) & =\alpha7\\ Sig(\alpha7) & =\alpha8\\ Sig(\alpha8) & =\alpha9\\ Sig(\alpha9) & =Sig(\alpha)0 \end{aligned}\] Definamos \(Dec:\omega\rightarrow Num^{\ast}\) de la siguiente manera \[\begin{aligned} Dec(0) & =\varepsilon\\ Dec(n+1) & =Sig(Dec(n)) \end{aligned}\] Nótese que para \(n\in\mathbf{N}\), la palabra \(Dec(n)\) es la notación usual decimal de \(n\). Para hacer mas ágil la notación escribiremos \(\bar{n}\) en lugar de \(Dec(n)\).

Sea \(Nombres_{1}\) el conjunto formado por las siguientes palabras \[\begin{aligned} & \text{EXISTENCIA}\\ & \text{COMMUTATIVIDAD}\\ & \text{PARTICULARIZACION}\\ & \text{ABSURDO}\\ & \text{EVOCACION}\\ & \text{CONJUNCIONELIMINACION}\\ & \text{EQUIVALENCIAELIMINACION}\\ & \text{DISJUNCIONINTRODUCCION}\\ & \text{ELECCION}\\ & \text{GENERALIZACION} \end{aligned}\] Sea \(Nombres_{2}\) el conjunto formado por las siguientes palabras \[\begin{aligned} & \text{MODUSPONENS}\\ & \text{TRANSITIVIDAD}\\ & \text{CONJUNCIONINTRODUCCION}\\ & \text{EQUIVALENCIAINTRODUCCION}\\ & \text{DISJUNCIONELIMINACION}\\ & \text{REEMPLAZO} \end{aligned}\] Una justificación básica es una palabra perteneciente a la unión de los siguientes conjuntos de palabras \[\{\text{CONCLUSION},\text{AXIOMAPROPIO},\text{AXIOMALOGICO}\}\] \[\{\alpha(\bar{k}):k\in\mathbf{N}\text{ y }\alpha\in Nombres_{1}\}\] \[\{\alpha(\bar{j},\bar{k}):j,k\in\mathbf{N}\text{ y }\alpha\in Nombres_{2}\}\] \[\{\text{DIVISIONPORCASOS}(\bar{j},\bar{k},\bar{l}):j,k,l\in\mathbf{N}\}\] Usaremos \(JustBas\) para denotar el conjunto formado por todas las justificaciones básicas. Una justificación es una palabra que ya sea es una justificación básica o pertenece a la unión de los siguientes conjuntos de palabras \[\{\text{HIPOTESIS}\bar{k}:k\in\mathbf{N}\}\] \[\{\text{TESIS}\bar{j}\alpha:j\in\mathbf{N}\text{ y }\alpha\in JustBas\}\] Usaremos \(Just\) para denotar el conjunto formado por todas las justificaciones. Cabe destacar que los elementos de \(Just\) son palabras del alfabeto formado por los siguientes símbolos \[(\ )\ ,\ 0\ 1\ 2\ 3\ 4\ 5\ 6\ 7\ 8\ 9\ \mathrm{A}\ \mathrm{B}\ \mathrm{C}\ \mathrm{D}\ \mathrm{E}\ \mathrm{G}\ \mathrm{H}\ \mathrm{I}\ \mathrm{J}\ \mathrm{L}\ \mathrm{M}\ \mathrm{N}\ \mathrm{O}\ \mathrm{P}\ \mathrm{Q}\ \mathrm{R}\ \mathrm{S}\ \mathrm{T}\ \mathrm{U}\ \mathrm{V}\ \mathrm{X}\ \mathrm{Z}\]

7.13.1.4 Concatenaciones Balanceadas de Justificaciones

Para construir el concepto de prueba elemental deberíamos trabajar con sucesiones finitas de justificaciones pero el siguiente lema nos dice que podemos reemplazarlas por ciertas palabras, i.e. sus concatenaciones, sin perder información. Recordemos que si \(L\) es un conjunto de palabras, entonces denotaremos con \(L^{+}\) al conjunto formado por todas las concatenaciones de sucesiones finitas no nulas de elementos de \(L\). Es decir: \[L^{+}=\{\alpha_{1}...\alpha_{n}:\alpha_{1},...,\alpha_{n}\in L\text{ y }n\geq1\}\]

Proof. Supongamos \(J_{1},...,J_{n}\), \(J_{1}^{\prime},...,J_{m}^{\prime}\), con \(n,m\geq1\), son justificaciones tales que \(J_{1}...J_{n}=J_{1}^{\prime}...J_{m}^{\prime}\). Es fácil ver que entonces tenemos \(J_{1}=J_{1}^{\prime}\), por lo cual \(J_{2}...J_{n}=J_{2}^{\prime}...J_{m}^{\prime}\). Un argumento inductivo nos dice que entonces \(n=m\) y \(J_{i}=J_{i}^{\prime}\), \(i=1,...,n\)  

Es decir el lema anterior nos dice que la sucesión \(J_{1},...,J_{n}\) se puede codificar con la palabra \(J_{1}...J_{n}\) sin perder información. Dada \(\mathbf{J}\in Just^{+}\), usaremos \(n(\mathbf{J})\) y \(\mathbf{J}_{1},...,\mathbf{J}_{n(\mathbf{J})}\) para denotar los únicos \(n\) y \(J_{1},...,J_{n}\) cuya existencia garantiza el lema anterior.

Dados números naturales \(i\leq j\), usaremos \(\left\langle i,j\right\rangle\) para denotar el conjunto \(\{i,i+1,...,j\}.\) A los conjuntos de la forma \(\left\langle i,j\right\rangle\) los llamaremos bloques.

Dada \(\mathbf{J}\in Just^{+}\) definamos \[\begin{gathered} \mathcal{B}^{\mathbf{J}}=\{\left\langle i,j\right\rangle :1\leq i\leq j\leq n(\mathbf{J})\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \exists k\ \mathbf{J}_{i}=\text{HIPOTESIS}\bar{k}\text{ y}\\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \mathbf{J}_{j}=\text{TESIS}\bar{k}\alpha\text{ para algún }\alpha\in JustBas\} \end{gathered}\] Diremos que \(\mathbf{J}\in Just^{+}\) es balanceada si se dan las siguientes

1. adhocprefix(1)adhocsufix Por cada \(k\in\mathbf{N}\) a lo sumo hay un \(i\) tal que \(\mathbf{J}_{i}=\) \(\mathrm{HIPOTESIS}\bar{k}\) y a lo sumo hay un \(i\) tal que \(\mathbf{J}_{i}=\) \(\mathrm{TESIS}\bar{k}\alpha\), con \(\alpha\in JustBas\)

2. adhocprefix(2)adhocsufix Si \(\mathbf{J}_{i}=\mathrm{HIPOTESIS}\bar{k}\) entonces hay un \(l>i\) tal que \(\mathbf{J}_{l}=\mathrm{TESIS}\bar{k}\alpha\), con \(\alpha\in JustBas\)

3. adhocprefix(3)adhocsufix Si \(\mathbf{J}_{i}=\mathrm{TESIS}\bar{k}\alpha\), con \(\alpha\in JustBas\), entonces hay un \(l<i\) tal que \(\mathbf{J}_{l}=\mathrm{HIPOTESIS}\bar{k}\)

4. adhocprefix(4)adhocsufix Si \(B_{1},B_{2}\in\mathcal{B}^{\mathbf{J}}\), entonces \(B_{1}\cap B_{2}=\emptyset\) o \(B_{1}\subseteq B_{2}\) o \(B_{2}\subseteq B_{1}\)

1. adhocprefixEjercicio:adhocsufix Supongamos \(\mathbf{J}\in Just^{+}\) es balanceada. Entonces

   1. Si \(\left\langle i,j\right\rangle \in\mathcal{B}^{\mathbf{J}}\), entonces \(i<j\)

   2. Si \(\left\langle i,j\right\rangle ,\left\langle i^{\prime},j^{\prime}\right\rangle \in\mathcal{B}^{\mathbf{J}}\) y \(i=i^{\prime}\), entonces \(j=j^{\prime}\)

   3. Si \(\left\langle i,j\right\rangle ,\left\langle i^{\prime},j^{\prime}\right\rangle \in\mathcal{B}^{\mathbf{J}}\) y \(j=j^{\prime}\), entonces \(i=i^{\prime}\)

7.13.1.5 Pares Adecuados

Para construir el concepto de prueba elemental deberíamos trabajar con sucesiones finitas de sentencias pero el siguiente lema nos dice que podemos reemplazarlas por ciertas palabras, i.e. sus concatenaciones, sin perder información.

Proof. Solo hay que probar la unicidad la cual sigue de la Proposición 7.1.  

Es decir el lema anterior nos dice que la sucesión \(\varphi_{1},...,\varphi_{n}\) se puede codificar con la palabra \(\varphi_{1}...\varphi_{n}\) sin perder información. Dada \(\boldsymbol{\varphi}\in S^{\tau+}\), usaremos \(n(\boldsymbol{\varphi})\) y \(\boldsymbol{\varphi}_{1},...,\boldsymbol{\varphi}_{n(\boldsymbol{\varphi})}\) para denotar los únicos \(n\) y \(\varphi_{1},...,\varphi_{n}\) cuya existencia garantiza el lema anterior.

Un par adecuado de tipo \(\tau\) es un par \((\boldsymbol{\varphi},\mathbf{J})\in S^{\tau+}\times Just^{+}\) tal que \(n(\boldsymbol{\varphi})=n(\mathbf{J})\) y \(\mathbf{J}\) es balanceada.

Sea \((\boldsymbol{\varphi},\mathbf{J})\) un par adecuado de tipo \(\tau\). Si \(\left\langle i,j\right\rangle \in\mathcal{B}^{\mathbf{J}}\), entonces \(\boldsymbol{\varphi}_{i}\) será la hipótesis del bloque \(\left\langle i,j\right\rangle\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \(\boldsymbol{\varphi}_{j}\) será la tesis del bloque \(\left\langle i,j\right\rangle\) en \((\boldsymbol{\varphi},\mathbf{J})\). Diremos que \(\boldsymbol{\varphi}_{i}\) esta bajo la hipótesis \(\boldsymbol{\varphi}_{l}\) en \((\boldsymbol{\varphi},\mathbf{J})\) o que \(\boldsymbol{\varphi}_{l}\) es una hipótesis de \(\boldsymbol{\varphi}_{i}\) en \((\boldsymbol{\varphi},\mathbf{J})\) cuando haya en \(\mathcal{B}^{\mathbf{J}}\) un bloque de la forma \(\left\langle l,j\right\rangle\) el cual contenga a \(i\). Sean \(i,j\in\left\langle 1,n(\boldsymbol{\varphi})\right\rangle .\) Diremos que \(i\) es anterior a \(j\) en \((\boldsymbol{\varphi},\mathbf{J})\) si \(i<j\) y además para todo \(B\in\mathcal{B}^{\mathbf{J}}\) se tiene que \(i\in B\Rightarrow j\in B\).

7.13.1.6 Dependencia de Nombres de Constante en Pares Adecuados

Sea \((\boldsymbol{\varphi},\mathbf{J})\) un par adecuado de tipo \(\tau\). Dadas \(e,d\in\mathcal{C}\), diremos que \(e\) depende directamente de \(d\) en \((\boldsymbol{\varphi},\mathbf{J})\) si hay números \(1\leq l<j\leq n(\boldsymbol{\varphi})\) tales que

1. adhocprefix(1)adhocsufix \(l\) es anterior a \(j\) en \((\boldsymbol{\varphi},\mathbf{J})\)

2. adhocprefix(2)adhocsufix \(\mathbf{J}_{j}=\alpha\mathrm{ELECCION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{j})\in Elec^{\tau}\) vía \(e\)

3. adhocprefix(3)adhocsufix \(d\) ocurre en \(\boldsymbol{\varphi}_{l}\).

Dados \(e,d\in\mathcal{C}\), diremos que \(e\) depende de \(d\) en \((\boldsymbol{\varphi},\mathbf{J})\) si existen \(e_{0},...,e_{k+1}\in\mathcal{C}\), con \(k\geq0\), tales que

1. adhocprefix(1)adhocsufix \(e_{0}=e\) y \(e_{k+1}=d\)

2. adhocprefix(2)adhocsufix \(e_{i}\) depende directamente de \(e_{i+1}\) en \((\boldsymbol{\varphi},\mathbf{J})\), para \(i=0,...,k\).

7.13.1.7 Definición de Prueba Formal

Ahora sí estamos en condiciones de definir el concepto de prueba formal en una teoría de primer orden. Sea \((\Sigma,\tau)\) una teoría de primer orden. Sea \(\varphi\) una sentencia de tipo \(\tau\). Una prueba formal de \(\varphi\) en \((\Sigma,\tau)\) será un par adecuado \((\boldsymbol{\varphi},\mathbf{J})\) de algún tipo \(\tau_{1}=(\mathcal{C}\cup\mathcal{C}_{1},\mathcal{F},\mathcal{R},a)\), con \(\mathcal{C}_{1}\) finito y disjunto con \(\mathcal{C}\), tal que

1. adhocprefix(1)adhocsufix Cada \(\boldsymbol{\varphi}_{i}\) es una sentencia de tipo \(\tau_{1}\)

2. adhocprefix(2)adhocsufix \(\boldsymbol{\varphi}_{n(\boldsymbol{\varphi})}=\varphi\)

3. adhocprefix(3)adhocsufix Si \(\left\langle i,j\right\rangle \in\mathcal{B}^{\mathbf{J}}\), entonces \(\boldsymbol{\varphi}_{j+1}=(\boldsymbol{\varphi}_{i}\rightarrow\boldsymbol{\varphi}_{j})\) y \(\mathbf{J}_{j+1}=\alpha\mathrm{CONCLUSION}\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\)

4. adhocprefix(4)adhocsufix Para cada \(i=1,...,n(\boldsymbol{\varphi})\), se da una de las siguientes

   1. adhocprefix(a)adhocsufix \(\mathbf{J}_{i}=\mathrm{HIPOTESIS}\bar{k}\) para algún \(k\in\mathbf{N}\)

   2. adhocprefix(b)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{CONCLUSION}\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y hay un \(j\) tal que \(\left\langle j,i-1\right\rangle \in\mathcal{B}^{\mathbf{J}}\) y \(\boldsymbol{\varphi}_{i}=(\boldsymbol{\varphi}_{j}\rightarrow\boldsymbol{\varphi}_{i-1})\)

   3. adhocprefix(c)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{AXIOMALOGICO}\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \(\boldsymbol{\varphi}_{i}\) es un axioma lógico de tipo \(\tau_{1}\)

   4. adhocprefix(d)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{AXIOMAPROPIO}\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \(\boldsymbol{\varphi}_{i}\in\Sigma\)

   5. adhocprefix(e)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{PARTICULARIZACION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Partic^{\tau_{1}}\)

   6. adhocprefix(f)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{COMMUTATIVIDAD}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Commut^{\tau_{1}}\)

   7. adhocprefix(g)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{ABSURDO}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Absur^{\tau_{1}}\)

   8. adhocprefix(h)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{EVOCACION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Evoc^{\tau_{1}}\)

   9. adhocprefix(i)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{EXISTENCIA}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Exist^{\tau_{1}}\)

   10. adhocprefix(j)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{CONJUNCIONELIMINACION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in ConjElim^{\tau_{1}}\)

   11. adhocprefix(k)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{DISJUNCIONINTRODUCCION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in DisjInt^{\tau_{1}}\)

   12. adhocprefix(l)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{EQUIVALENCIAELIMINACION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in EquivElim^{\tau_{1}}\)

   13. adhocprefix(m)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{MODUSPONENS}(\overline{l_{1}},\overline{l_{2}})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l_{1}\) y \(l_{2}\) anteriores a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l_{1}},\boldsymbol{\varphi}_{l_{2}},\boldsymbol{\varphi}_{i})\in ModPon^{\tau_{1}}\)

   14. adhocprefix(n)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{CONJUNCIONINTRODUCCION}(\overline{l_{1}},\overline{l_{2}})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l_{1}\) y \(l_{2}\) anteriores a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l_{1}},\boldsymbol{\varphi}_{l_{2}},\boldsymbol{\varphi}_{i})\in ConjInt^{\tau_{1}}\)

   15. adhocprefix(o)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{EQUIVALENCIAINTRODUCCION}(\overline{l_{1}},\overline{l_{2}})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l_{1}\) y \(l_{2}\) anteriores a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l_{1}},\boldsymbol{\varphi}_{l_{2}},\boldsymbol{\varphi}_{i})\in EquivInt^{\tau_{1}}\)

   16. adhocprefix(p)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{DISJUNCIONELIMINACION}(\overline{l_{1}},\overline{l_{2}})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l_{1}\) y \(l_{2}\) anteriores a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l_{1}},\boldsymbol{\varphi}_{l_{2}},\boldsymbol{\varphi}_{i})\in DisjElim^{\tau_{1}}\)

   17. adhocprefix(q)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{REEMPLAZO}(\overline{l_{1}},\overline{l_{2}})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l_{1}\) y \(l_{2}\) anteriores a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l_{1}},\boldsymbol{\varphi}_{l_{2}},\boldsymbol{\varphi}_{i})\in Reemp^{\tau_{1}}\)

   18. adhocprefix(r)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{TRANSITIVIDAD}(\overline{l_{1}},\overline{l_{2}})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l_{1}\) y \(l_{2}\) anteriores a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l_{1}},\boldsymbol{\varphi}_{l_{2}},\boldsymbol{\varphi}_{i})\in Trans^{\tau_{1}}\)

   19. adhocprefix(s)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{DIVISIONPORCASOS}(\overline{l_{1}},\overline{l_{2}},\overline{l_{3}})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l_{1},l_{2}\) y \(l_{3}\) anteriores a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l_{1}},\boldsymbol{\varphi}_{l_{2}},\boldsymbol{\varphi}_{l_{3}},\boldsymbol{\varphi}_{i})\in DivPorCas^{\tau_{1}}\)

   20. adhocprefix(t)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{ELECCION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Elec^{\tau_{1}}\) vía un nombre de cte \(e\), el cual no pertenece a \(\mathcal{C}\) y no ocurre en \(\boldsymbol{\varphi}_{1},...,\boldsymbol{\varphi}_{i-1}\).

   21. adhocprefix(u)adhocsufix \(\mathbf{J}_{i}=\alpha\mathrm{GENERALIZACION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Generaliz^{\tau_{1}}\) vía un nombre de cte \(c\) el cual cumple:

       1. adhocprefix(i)adhocsufix \(c\not\in\mathcal{C}\)

       2. adhocprefix(ii)adhocsufix \(c\) no es un nombre de cte que sea introducido en \((\boldsymbol{\varphi},\mathbf{J})\) por la aplicación de la regla de elección; es decir para cada \(u\in\{1,...,n(\boldsymbol{\varphi})\}\), si \(\mathbf{J}_{u}=\alpha\mathrm{ELECCION}(\bar{v})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \(v\) anterior a \(u\) en \((\boldsymbol{\varphi},\mathbf{J})\), entonces no se da que \((\boldsymbol{\varphi}_{v},\boldsymbol{\varphi}_{u})\in Elec^{\tau_{1}}\) vía \(c\).

       3. adhocprefix(iii)adhocsufix Para cada \(u\in\{1,...,n(\boldsymbol{\varphi})\}\), si \(\boldsymbol{\varphi}_{u}\) es hipótesis de \(\boldsymbol{\varphi}_{l}\) en \((\boldsymbol{\varphi},\mathbf{J})\), entonces \(c\) no ocurre en \(\boldsymbol{\varphi}_{u}\)

       4. adhocprefix(iv)adhocsufix Ningún nombre de constante que ocurra en \(\boldsymbol{\varphi}_{l}\) depende de \(c\) en \((\boldsymbol{\varphi},\mathbf{J})\)

       5. adhocprefix(v)adhocsufix Para cada \(u\in\{1,...,n(\boldsymbol{\varphi})\}\), si \(\boldsymbol{\varphi}_{u}\) es hipótesis de \(\boldsymbol{\varphi}_{l}\) en \((\boldsymbol{\varphi},\mathbf{J})\), entonces ningún nombre de constante que ocurra en \(\boldsymbol{\varphi}_{u}\) depende de \(c\) en \((\boldsymbol{\varphi},\mathbf{J})\)

Los nombres de constante de \(\mathcal{C}_{1}\) que ocurran en \(\boldsymbol{\varphi}\) serán llamados los nombres de constante auxiliares de \((\boldsymbol{\varphi},\mathbf{J})\). Nótese que los nombres de constante auxiliares de \((\boldsymbol{\varphi},\mathbf{J})\) son la versión formalizada de los nombres de elementos fijos usados en una prueba elemental. Al tipo \((\mathcal{C}\cup\{\text{nombres de cte auxiliares de }(\boldsymbol{\varphi},\mathbf{J})\},\mathcal{F},\mathcal{R},a)\) lo llamaremos el tipo ambiente de \((\boldsymbol{\varphi},\mathbf{J})\).

7.13.2 El Concepto de Teorema

Cuando haya una prueba de \(\varphi\) en \((\Sigma,\tau)\), diremos que \(\varphi\) es un teorema de la teoría \((\Sigma,\tau)\) y escribiremos \((\Sigma,\tau)\vdash\varphi\). A continuación daremos algunos ejemplos de teoremas exhibiendo sus pruebas formales.

En la teoría \(Po\)

Sea \(\mu=\forall x_{1}\forall x_{2}((\forall x_{3}\leq(x_{3},x_{1})\wedge\forall x_{3}\leq(x_{3},x_{2}))\rightarrow(x_{1}\equiv x_{2}))\). Veamos que \(\mu\) es un teorema de \(Po\). La idea para hacer la prueba formal es ir copiando la estructura de la prueba elemental de \(\mu\) dada la Sección Pruebas Elementales de Posets. Para facilitar la lectura la escribiremos secuencialmente \[\begin{array}{llll} 1.\; & (\forall x_{3}\leq(x_{3},a)\wedge\forall x_{3}\leq(x_{3},b)) & & \mathrm{HIPOTESIS}1\\ 2.\; & \forall x_{3}\leq(x_{3},a) & & \mathrm{CONJUNCIONELIMINACION}(1)\\ 3.\; & \leq(b,a) & & \mathrm{PARTICULARIZACION}(2)\\ 4.\; & \forall x_{3}\leq(x_{3},b) & & \mathrm{CONJUNCIONELIMINACION}(1)\\ 5. & \leq(a,b) & & \mathrm{PARTICULARIZACION}(4)\\ 6. & (\leq(a,b)\wedge\leq(b,a)) & & \text{CONJUNCIONINTRODUCCION}(5,3)\\ 7. & \forall x_{1}\forall x_{2}((\leq(x_{1},x_{2})\wedge\leq(x_{2},x_{1}))\rightarrow(x_{1}\equiv x_{2})) & & \text{AXIOMAPROPIO}\\ 8. & \forall x_{2}((\leq(a,x_{2})\wedge\leq(x_{2},a))\rightarrow(a\equiv x_{2})) & & \text{PARTICULARIZACION}(7)\\ 9. & ((\leq(a,b)\wedge\leq(b,a))\rightarrow(a\equiv b)) & & \text{PARTICULARIZACION}(8)\\ 10. & (a\equiv b) & & \text{TESIS}1\text{MODUSPONENS}(6,9)\\ 11. & ((\forall x_{3}\leq(x_{3},a)\wedge\forall x_{3}\leq(x_{3},b))\rightarrow(a\equiv b)) & & \text{CONCLUSION}\\ 12. & \forall x_{2}((\forall x_{3}\leq(x_{3},a)\wedge\forall x_{3}\leq(x_{3},x_{2}))\rightarrow(a\equiv x_{2})) & & \text{GENERALIZACION}(11)\\ 13. & \forall x_{1}\forall x_{2}((\forall x_{3}\leq(x_{3},x_{1})\wedge\forall x_{3}\leq(x_{3},x_{2}))\rightarrow(x_{1}\equiv x_{2})) & & \text{GENERALIZACION}(12) \end{array}\] Pero por supuesto, nuestra prueba formal es en realidad el par \((\boldsymbol{\varphi},\mathbf{J})\) donde \(\boldsymbol{\varphi}\) es la concatenación de la secuencia de sentencias de arriba y \(\mathbf{J}\) es la concatenación de la secuencia de justificaciones de arriba. Nótese que las sentencias de esta prueba formal son de tipo \((\{a,b\},\emptyset,\{\leq\},\{(\leq,2)\})\) es decir extendimos \(\tau_{Po}\) agregando dos nombres de constante nuevos, los cuales en la “idea” de la prueba denotan elementos fijos pero arbitrarios. O sea que para esta prueba tenemos que el \(\mathcal{C}_{1}\) al que se refiere la definición de prueba es el conjunto \(\{a,b\}\). Es decir las palabras \(a\) y \(b\) son los nombres de constante auxiliares de \((\boldsymbol{\varphi},\mathbf{J})\) y el tipo ambiente de \((\boldsymbol{\varphi},\mathbf{J})\) es \((\{a,b\},\emptyset,\{\leq\},\{(\leq,2)\})\).

En la teoría \((\emptyset,\tau)\)

Veamos algunos teoremas con sus pruebas formales de esta teoría.

1. adhocprefix-adhocsufix \(\forall x_{1}(x_{1}\equiv x_{1})\) es un teorema de \((\emptyset,\tau)\), atestiguado por la prueba formal \[\begin{array}{llll} 1.\; & c\equiv c & & \text{AXIOMALOGICO}\\ 2.\; & \forall x_{1}(x_{1}\equiv x_{1}) & & \text{GENERALIZACION}(1) \end{array}\] (\(c\) es un nombre de cte no perteneciente a \(\mathcal{C}\) y tal que \((\mathcal{C}\cup\{c\},\mathcal{F},\mathcal{R},a)\) es un tipo).

2. adhocprefix-adhocsufix Cualesquiera sea la sentencia \(\varphi\) de tipo \(\tau\) se tiene que \((\varphi\rightarrow\varphi)\) es un teorema de \((\emptyset,\tau)\). Una prueba formal: \[\begin{array}{llll} 1. & \varphi & & \text{HIPOTESIS}1\\ 2. & \varphi & & \text{TESIS}1\text{EVOCACION}(1)\\ 3. & (\varphi\rightarrow\varphi) & & \text{CONCLUSION} \end{array}\]

3. adhocprefix-adhocsufix Cualesquiera sea la sentencia \(\varphi\) de tipo \(\tau\) se tiene que \((\varphi\leftrightarrow\varphi)\) es un teorema de \((\emptyset,\tau)\). Una prueba formal: \[\begin{array}{llll} 1. & \varphi & & \text{HIPOTESIS}1\\ 2. & \varphi & & \text{TESIS}1\text{EVOCACION}(1)\\ 3. & (\varphi\rightarrow\varphi) & & \text{CONCLUSION}\\ 4. & (\varphi\rightarrow\varphi) & & \text{EVOCACION}(3)\\ 5. & (\varphi\leftrightarrow\varphi) & & \text{EQUIVALENCIAINTRODUCCION}(3,4) \end{array}\] Cualesquiera sea la sentencias \(\varphi\) de tipo \(\tau\) se tiene que \((\varphi\vee\neg\varphi)\) es un teorema de \((\emptyset,\tau)\). Una prueba formal: \[\begin{array}{llll} 1. & \neg\varphi & & \text{HIPOTESIS}1\\ 2. & \neg\varphi & & \text{TESIS}1\text{EVOCACION}(1)\\ 3. & (\neg\varphi\rightarrow\neg\varphi) & & \text{CONCLUSION}\\ 4. & (\varphi\vee\neg\varphi) & & \text{DISJUNCIONINTRODUCCION}(3) \end{array}\] Cualesquiera sea la sentencias \(\varphi\) de tipo \(\tau\) se tiene que \(\neg(\varphi\wedge\neg\varphi)\) es un teorema de \((\emptyset,\tau)\). Una prueba formal: \[\begin{array}{llll} 1. & (\varphi\wedge\neg\varphi) & & \text{HIPOTESIS}1\\ 2. & (\varphi\wedge\neg\varphi) & & \text{TESIS}1\text{EVOCACION}(1)\\ 3. & ((\varphi\wedge\neg\varphi)\rightarrow(\varphi\wedge\neg\varphi)) & & \text{CONCLUSION}\\ 4. & \neg(\varphi\wedge\neg\varphi) & & \text{ABSURDO}(3) \end{array}\] Cualesquiera sean las sentencias \(\varphi_{1}\text{ y }\varphi_{2}\) de tipo \(\tau\) se tiene que \(((\varphi_{1}\vee\varphi_{2})\rightarrow(\varphi_{2}\vee\varphi_{1}))\) es un teorema de \((\emptyset,\tau)\). Una prueba formal: \[\begin{array}{llll} 1. & (\varphi_{1}\vee\varphi_{2}) & & \text{HIPOTESIS}1\\ 2. & \varphi_{1} & & \text{HIPOTESIS}2\\ 3. & (\varphi_{2}\vee\varphi_{1}) & & \text{TESIS}2\text{DISJUNCIONINTRODUCCION}(2)\\ 4. & (\varphi_{1}\rightarrow(\varphi_{2}\vee\varphi_{1})) & & \text{CONCLUSION}\\ 5. & \varphi_{2} & & \text{HIPOTESIS}3\\ 6. & (\varphi_{2}\vee\varphi_{1}) & & \text{TESIS}3\text{DISJUNCIONINTRODUCCION}(5)\\ 7. & \varphi_{2}\rightarrow(\varphi_{2}\vee\varphi_{1}) & & \text{CONCLUSION}\\ 8. & (\varphi_{2}\vee\varphi_{1}) & & \text{TESIS}1\text{DIVISIONPORCASOS}(1,4,7)\\ 9. & ((\varphi_{1}\vee\varphi_{2})\rightarrow(\varphi_{2}\vee\varphi_{1})) & & \text{CONCLUSION} \end{array}\]

4. adhocprefix-adhocsufix Cualesquiera sean las sentencias \(\varphi_{1},\varphi_{2},\varphi_{3}\) de tipo \(\tau\) se tiene que \(((\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3}))\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}))\) es un teorema de \((\emptyset,\tau)\). Una prueba formal: \[\begin{array}{llll} 1. & (\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3})) & & \text{HIPOTESIS}1\\ 2. & \varphi_{1} & & \text{HIPOTESIS}2\\ 3. & (\varphi_{1}\vee\varphi_{2}) & & \text{DISJUNCIONINTRODUCCION}(2)\\ 4. & ((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{TESIS}2\text{DISJUNCIONINTRODUCCION}(3)\\ 5. & (\varphi_{1}\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3})) & & \text{CONCLUSION}\\ 6. & (\varphi_{2}\vee\varphi_{3}) & & \text{HIPOTESIS}3\\ 7. & \varphi_{2} & & \text{HIPOTESIS}4\\ 8. & (\varphi_{1}\vee\varphi_{2}) & & \text{DISJUNCIONINTRODUCCION}(7)\\ 9. & ((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{TESIS}4\text{DISJUNCIONINTRODUCCION}(8)\\ 10. & (\varphi_{2}\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3})) & & \text{CONCLUSION}\\ 11. & \varphi_{3} & & \text{HIPOTESIS}5\\ 12. & ((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{TESIS}5\text{DISJUNCIONINTRODUCCION}(11)\\ 13. & (\varphi_{3}\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3})) & & \text{CONCLUSION}\\ 14. & ((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{TESIS}3\text{DIVISIONPORCASOS}(6,10,13)\\ 15. & ((\varphi_{2}\vee\varphi_{3})\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3})) & & \text{CONCLUSION}\\ 16. & ((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{TESIS}1\text{DIVISIONPORCASOS}(1,5,15)\\ 17. & ((\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3}))\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3})) & & \text{CONCLUSION} \end{array}\]

5. adhocprefix-adhocsufix Cualesquiera sean las sentencias \(\varphi\text{ y }\psi\) la sentencia \(((\varphi\wedge(\varphi\vee\psi))\leftrightarrow\varphi)\) es un teorema de \((\emptyset,\tau)\). Una prueba formal: \[\begin{array}{llll} 1.\; & (\varphi\wedge(\varphi\vee\psi)) & & \text{HIPOTESIS}1\\ 2.\; & \varphi & & \text{TESIS}1\text{CONJUNCIONELIMINACION}(1)\\ 3.\; & ((\varphi\wedge(\varphi\vee\psi))\rightarrow\varphi) & & \text{CONCLUSION}\\ 4.\; & \varphi & & \text{HIPOTESIS}2\\ 5. & (\varphi\vee\psi) & & \text{DISJUNCIONINTRODUCCION}(4)\\ 6. & (\varphi\wedge(\varphi\vee\psi)) & & \text{TESIS}2\text{CONJUNCIONINTRODUCCION}(4,5)\\ 7. & (\varphi\rightarrow(\varphi\wedge(\varphi\vee\psi))) & & \text{CONCLUSION}\\ 8. & ((\varphi\wedge(\varphi\vee\psi))\leftrightarrow\varphi) & & \text{EQUIVALENCIAINTRODUCCION}(3,7) \end{array}\]

6. adhocprefix-adhocsufix Cualesquiera sean las sentencias \(\varphi\text{ y }\psi\) la sentencia \(((\varphi\vee(\varphi\wedge\psi))\leftrightarrow\varphi)\) es un teorema de \((\emptyset,\tau)\). Una prueba formal: \[\begin{array}{llll} 1.\; & (\varphi\vee(\varphi\wedge\psi)) & & \text{HIPOTESIS}1\\ 2.\; & \varphi & & \text{HIPOTESIS}2\\ 3.\; & \varphi & & \text{TESIS}2\text{EVOCACION}(2)\\ 4.\; & (\varphi\rightarrow\varphi) & & \text{CONCLUSION}\\ 5. & (\varphi\wedge\psi) & & \text{HIPOTESIS}3\\ 6. & \varphi & & \text{TESIS}3\text{CONJUNCIONELIMINACION}(5)\\ 7. & ((\varphi\wedge\psi)\rightarrow\varphi) & & \text{CONCLUSION}\\ 8. & \varphi & & \text{TESIS}1\text{DIVISIONPORCASOS}(1,4,7)\\ 9. & ((\varphi\vee(\varphi\wedge\psi))\rightarrow\varphi) & & \text{CONCLUSION}\\ 10. & \varphi & & \text{HIPOTESIS}4\\ 11. & (\varphi\vee(\varphi\wedge\psi)) & & \text{TESIS}4\text{DISJUNCIONINTRODUCCION}(10)\\ 12. & (\varphi\rightarrow(\varphi\vee(\varphi\wedge\psi))) & & \text{CONCLUSION}\\ 13. & ((\varphi\vee(\varphi\wedge\psi))\leftrightarrow\varphi) & & \text{EQUIVALENCIAINTRODUCCION}(9,12) \end{array}\]

7. adhocprefix-adhocsufix Cualesquiera sean las sentencias \(\varphi_{1},\varphi_{2}\text{ y }\varphi\) la sentencia \(((\varphi\wedge(\varphi_{1}\vee\varphi_{2}))\rightarrow((\varphi\wedge\varphi_{1})\vee(\varphi\wedge\varphi_{2})))\) es un teorema de \((\emptyset,\tau)\). Una prueba formal: \[\begin{array}{llll} 1.\; & (\varphi\wedge(\varphi_{1}\vee\varphi_{2})) & & \text{HIPOTESIS}1\\ 2.\; & \varphi & & \text{CONJUNCIONELIMINACION}(1)\\ 3.\; & (\varphi_{1}\vee\varphi_{2}) & & \text{CONJUNCIONELIMINACION}(1)\\ 4.\; & \varphi_{1} & & \text{HIPOTESIS}2\\ 5. & (\varphi\wedge\varphi_{1}) & & \text{CONJUNCIONINTRODUCCION}(2,4)\\ 6. & ((\varphi\wedge\varphi_{1})\vee(\varphi\wedge\varphi_{2})) & & \text{TESIS}2\text{DISJUNCIONINTRODUCCION}(5)\\ 7. & (\varphi_{1}\rightarrow((\varphi\wedge\varphi_{1})\vee(\varphi\wedge\varphi_{2}))) & & \text{CONCLUSION}\\ 8. & \varphi_{2} & & \text{HIPOTESIS}3\\ 9. & (\varphi\wedge\varphi_{2}) & & \text{CONJUNCIONINTRODUCCION}(2,8)\\ 10. & ((\varphi\wedge\varphi_{1})\vee(\varphi\wedge\varphi_{2})) & & \text{TESIS}3\text{DISJUNCIONINTRODUCCION}(9)\\ 11. & (\varphi_{2}\rightarrow((\varphi\wedge\varphi_{1})\vee(\varphi\wedge\varphi_{2}))) & & \text{CONCLUSION}\\ 12. & ((\varphi\wedge\varphi_{1})\vee(\varphi\wedge\varphi_{2})) & & \text{TESIS}1\text{DIVISIONPORCASOS}(3,7,11)\\ 13. & ((\varphi\wedge(\varphi_{1}\vee\varphi_{2}))\rightarrow((\varphi\wedge\varphi_{1})\vee(\varphi\wedge\varphi_{2}))) & & \text{CONCLUSION} \end{array}\]

8. adhocprefix-adhocsufix Cualesquiera sean las sentencias \(\varphi_{1},\varphi_{2}\text{ y }\varphi\) la sentencia \((((\varphi\wedge\varphi_{1})\vee(\varphi\wedge\varphi_{2}))\rightarrow(\varphi\wedge(\varphi_{1}\vee\varphi_{2})))\) es un teorema de \((\emptyset,\tau)\). Una prueba formal: \[\begin{array}{llll} 1.\; & ((\varphi\wedge\varphi_{1})\vee(\varphi\wedge\varphi_{2})) & & \text{HIPOTESIS}1\\ 2.\; & (\varphi\wedge\varphi_{1}) & & \text{HIPOTESIS}2\\ 3.\; & \varphi & & \text{CONJUNCIONELIMINACION}(2)\\ 4.\; & \varphi_{1} & & \text{CONJUNCIONELIMINACION}(2)\\ 5. & (\varphi_{1}\vee\varphi_{2}) & & \text{DISJUNCIONINTRODUCCION}(4)\\ 6. & (\varphi\wedge(\varphi_{1}\vee\varphi_{2})) & & \text{TESIS}2\text{CONJUNCIONINTRODUCCION}(3,5)\\ 7. & ((\varphi\wedge\varphi_{1})\rightarrow(\varphi\wedge(\varphi_{1}\vee\varphi_{2}))) & & \text{CONCLUSION}\\ 8. & (\varphi\wedge\varphi_{2}) & & \text{HIPOTESIS}3\\ 9. & \varphi & & \text{CONJUNCIONELIMINACION}(8)\\ 10. & \varphi_{2} & & \text{CONJUNCIONELIMINACION}(8)\\ 11. & (\varphi_{1}\vee\varphi_{2}) & & \text{DISJUNCIONINTRODUCCION}(10)\\ 12. & (\varphi\wedge(\varphi_{1}\vee\varphi_{2})) & & \text{TESIS}3\text{CONJUNCIONINTRODUCCION}(9,11)\\ 13. & ((\varphi\wedge\varphi_{2})\rightarrow(\varphi\wedge(\varphi_{1}\vee\varphi_{2}))) & & \text{CONCLUSION}\\ 14. & (\varphi\wedge(\varphi_{1}\vee\varphi_{2})) & & \text{TESIS}1\text{DIVISIONPORCASOS}(1,7,13)\\ 15. & (((\varphi\wedge\varphi_{1})\vee(\varphi\wedge\varphi_{2}))\rightarrow(\varphi\wedge(\varphi_{1}\vee\varphi_{2}))) & & \text{CONCLUSION} \end{array}\]

7.13.2.1 Algunos Teoremas de \(RetCua\)

A continuación damos varias sentencias para que el lector de pruebas formales en \(RetCua\). La forma mas fácil de hacer esto es primero dar la prueba elemental tal como se lo hizo en la Sección de Reticulados Cuaterna y luego traducir la prueba elemental a una prueba formal. No se recomienda al lector que “cuan escarabajo” intente aplicar las reglas mecánicamente para obtener la prueba formal. Todo lo contrario el debe volver a la sección de reticulados cuaterna y hacer la respectiva prueba elemental imaginando como matemático la “novela” de su prueba elemental para luego dedicarse a traducirla a una formal. Reescribimos aquí los consejos dados en la sección de reticulados cuaterna para realizar pruebas elementales de reticulados cuaterna:

1. adhocprefixConsejos importantes:adhocsufix Por favor contengan a su escarabajo interior...

   1. adhocprefix-adhocsufix Cuando queramos hacer una prueba elemental de alguna sentencia elemental pura es importante no perder nuestro rol de matemáticos y creer que porque debemos realizar la prueba escribiendo las cosas con sentencias elementales debemos dejar de pensar como matemáticos y volvernos escarabajos sintácticos mecánicos que solo usan reglas y van encadenando sentencias elementales sin pensar e imaginar. Es decir, debemos hacer la prueba a lo mariposa pensando, imaginando. Tal como lo venimos haciendo pero agregando la consigna de que a la matemática involucrada la escribamos usando sentencias elementales.

   2. adhocprefix-adhocsufix Una buena manera de hacer una prueba elemental de una sentencia elemental pura \(\varphi\) es primero hacer la prueba matemática sin fijarse demasiado si es elemental o no. Es decir partir de la suposición de que tenemos un reticulado cuaterna \((L,\mathsf{s},\mathsf{i},\leq)\) fijo (pero arbitrario) e intentar (como matemáticos) probar que entonces en \((L,\mathsf{s},\mathsf{i},\leq)\) se cumple \(\varphi\). Muchas ideas para esto las podrá obtener de las pruebas dadas en la Sección de Reticulados Par. Una ves que hayamos hecho nuestra prueba como matemáticos, intentar tunearla para que se vuelva una prueba elemental.

   3. adhocprefix-adhocsufix Es decir debemos ser el mismo matemático de siempre solo que haciendo pruebas de un estilo muy particular.

   4. adhocprefix-adhocsufix Además es un sano consejo que cuando hagamos la prueba matemática y también la elemental, no llenemos de “basura lógica”. Es decir, debemos ser fieles a que en tales pruebas nuestro rol es el de un matemático común y corriente (que hasta podría odiar la lógica como disciplina!) por lo cual no tiene sentido ahí hacer referencia a las reglas y mecánicas que constituyen una prueba formal. Por ejemplo poner en la prueba matemática o en la prueba elemental: Por Modus Ponens se tiene que....., es obviamente algo que un matemático no haría! Otro ejemplo: Usar \(\equiv\) en lugar del \(=\). Es decir todas estas cosas distraen y nos alejan de las ideas (por eso enojan en algún sentido a los matemáticos) en momentos donde la concentración e imaginación matemáticas son cruciales. Consejo: guarde para la prueba formal todos esos impulsos.

Cabe destacar que dar una prueba formal concreta no es ni mas ni menos que dar una formalización matemáticamente perfecta de la matemática informal existente en la respectiva prueba elemental. Es decir estamos formalizando “porciones de matemática real”.

1. adhocprefixEjercicio:adhocsufix De una prueba formal de \(\forall x_{1}(\mathsf{s}(x_{1},x_{1})\equiv x_{1})\) en \(RetCua\)

2. adhocprefixEjercicio:adhocsufix De una prueba formal de \(\forall x_{1}\forall x_{2}(\mathsf{s}(x_{1},x_{2})\equiv\mathsf{s}(x_{2},x_{1}))\) en \(RetCua\)

3. adhocprefixEjercicio:adhocsufix De una prueba formal de \(\forall x_{1}\forall x_{2}(\mathsf{i}(\mathsf{s}(x_{1},x_{2}),x_{1})\equiv x_{1})\) en \(RetCua\)

4. adhocprefixEjercicio:adhocsufix De una prueba formal de \(\forall x_{1}\forall x_{2}(\leq(x_{1},x_{2})\leftrightarrow(\mathsf{s}(x_{1},x_{2})\equiv x_{2}))\) en \(RetCua\)

7.13.3 Simulación de Mecánicas de Prueba (Azuquita para Escarabajo)

Las pruebas formales modelizan nuestras pruebas elementales y hemos hecho las cosas para que la modelización sea lo mas fidedigna posible. En general el pasaje de la prueba elemental a la formal es rutinario y obvio. Es decir la idea subyacente a nuestra definición de prueba formal es que las pruebas (elementales) hechas por un matemático sean traducibles a una formal de la forma mas natural posible. A continuación daremos algunas de las mecánicas mas comunes usadas por los matemáticos en las pruebas y para cada caso daremos la forma en la que podemos “copiar” esto dentro de una prueba formal.

Reemplazo directo

Es muy común que el matemático deduzca la sentencia \(\psi\) a partir de sentencias \((\varphi\leftrightarrow\psi)\) y \(\varphi\). Esto formalmente se puede hacer exactamente igual ya que \(\psi\) se deduce por la regla de reemplazo de \((\varphi\leftrightarrow\psi)\) y \(\varphi\) (es justo el caso \(n=0\) y \(\gamma=\varphi\)).

Cuando probamos un implica en forma directa

Cuando un matemático en el contexto de una prueba intenta probar una sentencia de la forma \((\varphi\rightarrow\psi)\) suele asumir como hipótesis \(\varphi\), luego sigue razonando y prueba \(\psi\) para entonces concluir que vale \((\varphi\rightarrow\psi)\). Esto formalmente lo podemos hacer de la misma manera: \[\begin{array}{llll} \;\;\vdots & \vdots & & \;\;\;\vdots\\ \;\;k.\; & \varphi & & \text{HIPOTESIS}1\\ \;\;\vdots & \vdots & & \;\;\;\vdots\\ \;\;j. & \psi & & \text{TESIS1}...\\ \;j+1. & (\varphi\rightarrow\psi) & & \text{CONCLUSION}\\ \;\;\vdots & \vdots & & \;\;\;\vdots \end{array}\]

Cuando probamos una disjunción en forma directa

Cuando un matemático en el contexto de una prueba intenta probar una sentencia de la forma \((\varphi\vee\psi)\) suele probar \((\lnot\varphi\rightarrow\psi)\) y entonces concluir que vale \((\varphi\vee\psi)\). Esto claramente puede emularse en nuestras pruebas formales usando la regla de disjunción-introducción (caso 3).

Cuando probamos un si y solo si en forma directa

Cuando un matemático en el contexto de una prueba intenta probar una sentencia de la forma \((\varphi\leftrightarrow\psi)\) suele probar \((\varphi\rightarrow\psi)\) y \((\psi\rightarrow\varphi)\) y entonces concluir que vale \((\varphi\leftrightarrow\psi)\). Esto claramente puede emularse en nuestras pruebas formales usando la regla de equivalencia-introducción

Cuando sabemos que es cierta una disjunción

Cuando un matemático ya sabe que es cierta una disjunción \((\varphi\vee\psi)\) e intenta probar una sentencia \(\gamma\) suele probar \((\varphi\rightarrow\gamma)\) y \((\psi\rightarrow\gamma)\) y entonces concluir que vale \(\gamma\). Esto claramente puede emularse en nuestras pruebas formales usando la regla de división por casos

Mecánicas de negación

Cuando un matemático intenta probar una sentencia por el absurdo asume su negación pero muchas veces se saltea un paso y pone directamente algo equivalente a la negación de dicha sentencia. Por ejemplo: El matemático va a probar por el absurdo una sentencia de la forma \((\varphi\vee\psi)\). Para esto asume \((\lnot\varphi\wedge\lnot\psi)\) y luego de cierto razonamiento llega a una contradicción de la forma \((\gamma\wedge\lnot\gamma)\). Concluye entonces \((\varphi\vee\psi)\). Formalmente haremos: \[\begin{array}{llll} \;\;\;1.\; & \lnot(\varphi\vee\psi) & & \text{HIPOTESIS}1\\ \;\;\;2.\; & (\lnot(\varphi\vee\psi)\leftrightarrow(\lnot\varphi\wedge\lnot\psi)) & & \text{AXIOMALOGICO}\\ \;\;\;3.\; & (\lnot\varphi\wedge\lnot\psi) & & \text{REEMPLAZO}(1,2)\\ \;\;\;\vdots & \;\;\;\vdots & & \;\;\;\;\;\vdots\\ \;\;\;k. & (\gamma\wedge\lnot\gamma) & & \text{TESIS1}...\\ \;k+1. & (\lnot(\varphi\vee\psi)\rightarrow(\gamma\wedge\lnot\gamma)) & & \text{CONCLUSION}\\ \;k+2. & (\varphi\vee\psi) & & \text{ABSURDO}(k+1) \end{array}\] Es decir hacemos exactamente lo mismo pero sin saltearnos el paso de negar la sentencia que queremos probar (i.e. \((\varphi\vee\psi)\)). Otro ejemplo: El matemático va a probar por el absurdo una sentencia de la forma \(\forall v\varphi\). Para esto asume \(\exists v\lnot\varphi(v)\) y luego de cierto razonamiento llega a una contradicción de la forma \((\gamma\wedge\lnot\gamma)\). Concluye entonces \(\forall v\varphi(v)\). Formalmente haremos: \[\begin{array}{llll} \;\;\;1.\; & \lnot\forall v\varphi & & \text{HIPOTESIS}1\\ \;\;\;2.\; & (\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi) & & \text{AXIOMALOGICO}\\ \;\;\;3.\; & \exists v\lnot\varphi & & \text{REEMPLAZO}(1,2)\\ \;\;\;\vdots & \;\;\;\vdots & & \;\;\;\;\;\vdots\\ \;\;\;k. & (\gamma\wedge\lnot\gamma) & & \text{TESIS1}...\\ \;k+1. & (\lnot\forall v\varphi\rightarrow(\gamma\wedge\lnot\gamma)) & & \text{CONCLUSION}\\ \;k+2. & \forall v\varphi & & \text{ABSURDO}(k+1) \end{array}\] Un último ejemplo: El matemático va a probar por el absurdo una sentencia de la forma \((\varphi\rightarrow\psi)\). Para esto asume \((\varphi\wedge\lnot\psi)\) y luego de cierto razonamiento llega a una contradicción de la forma \((\gamma\wedge\lnot\gamma)\). Concluye entonces \((\varphi\rightarrow\psi)\). Formalmente haremos: \[\begin{array}{llll} \;\;\;1.\; & \lnot(\varphi\rightarrow\psi) & & \text{HIPOTESIS}1\\ \;\;\;2.\; & (\lnot(\varphi\rightarrow\psi)\leftrightarrow(\varphi\wedge\lnot\psi)) & & \text{AXIOMALOGICO}\\ \;\;\;3.\; & (\varphi\wedge\lnot\psi) & & \text{REEMPLAZO}(1,2)\\ \;\;\;\vdots & \;\;\;\vdots & & \;\;\;\;\;\vdots\\ \;\;\;k. & (\gamma\wedge\lnot\gamma) & & \text{TESIS1}...\\ \;k+1. & (\lnot(\varphi\rightarrow\psi)\rightarrow(\gamma\wedge\lnot\gamma)) & & \text{CONCLUSION}\\ \;k+2. & (\varphi\rightarrow\psi) & & \text{ABSURDO}(k+1) \end{array}\] Nótese que este tipo de situaciones se dan para los 7 distintos tipos de fórmulas no atómicas dados en el Lema Menú para Fórmulas. En cada caso para formalizar usamos el respectivo axioma esquema de negación junto con la regla de reemplazo. Dejamos al lector hacer lo mismo con los conectivos restantes (i.e. \(\wedge,\leftrightarrow,\neg,\exists\)).

Ojo escarabajo ...

Si bien acabamos de dar muchas mecánicas de deducción, cabe destacar que han sido dadas para mostrar como emular a los matemáticos en determinadas situaciones cotidianas y no para que el alumno suelte a su escarabajo y que cuando intente dar una prueba formal se saltee la prueba matemática, se olvide de su rol matemático y se dedique a aplicar estas reglas mecánicamente sin pensar!!! Es decir, es importante que se olvide de estas mecánicas (y de todas las baratijas lógicas) y primero intente dar una prueba como matemático, luego tunee esta prueba a una elemental y recién cuando empiece a traducir esta prueba elemental a una formal se fije en como estas mecánicas ayudan a emular ciertas partes de la prueba matemática.

7.13.4 Redundancia de Axiomas y Reglas

Ya que nuestra definición de prueba formal esta hecha intentando que las pruebas (elementales) hechas por un matemático sean traducibles a una formal de la forma mas natural posible, muchas veces habrá “redundancia deductiva”. Algunos ejemplos de redundancia deductiva:

1. adhocprefix-adhocsufix Se podrán probar algunos axiomas lógicos usando solo los otros, es decir algunos axiomas lógicos podrían sacarse y el concepto de prueba resultante tendría la misma “potencia” (i.e. se podrían seguir probando los mismos teoremas). Por ejemplo el lector no tendrá problemas en dar una prueba de \((\lnot\exists v\varphi\leftrightarrow\forall v\lnot\varphi)\) (por supuesto sin usarlo a el como axioma). Sin embargo se lo incluye como axioma dado que interviene naturalmente cuando un matemático quiere probar por el absurdo una sentencia de la forma \(\exists v\varphi\) (ver arriba en Mecánicas de negación)

2. adhocprefix-adhocsufix Muchas de las reglas podrían sacarse y se podrían seguir probando los mismos teoremas, por ejemplo la regla de elección.

De todas maneras esta redundancia es anecdótica ya que lo importante es que nuestro concepto de prueba formal sea un modelo lo mas natural posible. Cuando quitamos redundancia puede volverse muy ingenioso probar alguna sentencia obviamente cierta. Veamos un ejemplo: Sea \(\varphi=_{d}\varphi(v)\) una fórmula de tipo \(\tau\). Ya que \((\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi)\) es un axioma lógico, tenemos que \[((\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi),\text{AXIOMALOGICO})\] es una prueba formal de \((\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi)\) en la teoría \((\emptyset,\tau)\). A continuación se da una prueba formal en la teoría \((\emptyset,\tau)\) de la sentencia \((\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi)\) la cual no usa el hecho de que \((\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi)\) sea un axioma lógico. Notar que en las primeras 10 lineas se prueba \((\lnot\exists v\lnot\varphi\rightarrow\lnot\lnot\forall v\varphi)\), es decir el contrarecíproco de \((\lnot\forall v\varphi\rightarrow\exists v\lnot\varphi)\). De la linea 11 hasta la 17 se prueba \((\lnot\forall v\varphi\rightarrow\exists v\lnot\varphi)\). En las lineas restantes se prueba la implicación reciproca de \((\lnot\forall v\varphi\rightarrow\exists v\lnot\varphi)\), es decir \((\exists v\lnot\varphi\rightarrow\lnot\forall v\varphi)\) y en el último paso se obtiene \((\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi)\) por la regla de equivalencia-introducción. Cabe observar que esta prueba formal no es natural u obvia, mas bien es difícil de encontrar. \[\begin{array}{clll} 1. & \lnot\exists v\lnot\varphi & & \text{HIPOTESIS}1\\ 2. & \lnot\varphi(c) & & \text{HIPOTESIS}2\\ 3. & \exists v\lnot\varphi & & \text{EXISTENCIAL}(2)\\ 4. & (\exists v\lnot\varphi\wedge\lnot\exists v\lnot\varphi) & & \text{TESIS}2\text{CONJUNCIONINTRODUCCION}(3,1)\\ 5. & \lnot\varphi(c)\rightarrow(\exists v\lnot\varphi\wedge\lnot\exists v\lnot\varphi) & & \text{CONCLUSION}\\ 6. & \varphi(c) & & \text{ABSURDO}(5)\\ 7. & \forall v\varphi & & \text{GENERALIZACION}(6)\\ 8. & (\forall v\varphi\leftrightarrow\lnot\lnot\forall v\varphi) & & \text{AXIOMALOGICO}\\ 9. & \lnot\lnot\forall v\varphi & & \text{TESIS}1\text{REEMPLAZO}(7,8)\\ 10. & (\lnot\exists v\lnot\varphi\rightarrow\lnot\lnot\forall v\varphi) & & \text{CONCLUSION}\\ 11. & \lnot\forall v\varphi & & \text{HIPOTESIS}3\\ 12. & \lnot\exists v\lnot\varphi & & \text{HIPOTESIS}4\\ 13. & \lnot\lnot\forall v\varphi & & \text{MODUSPONENS}(12,10)\\ 14. & (\lnot\forall v\varphi\wedge\lnot\lnot\forall v\varphi) & & \text{TESIS}4\text{CONJUNCIONINTRODUCCION}(11,13)\\ 15. & \lnot\exists v\lnot\varphi\rightarrow(\lnot\forall v\varphi\wedge\lnot\lnot\forall v\varphi) & & \text{CONCLUSION}\\ 16. & \exists v\lnot\varphi & & \text{TESIS}3\text{ABSURDO}(15)\\ 17. & (\lnot\forall v\varphi\rightarrow\exists v\lnot\varphi) & & \text{CONCLUSION}\\ 18. & \exists v\lnot\varphi & & \text{HIPOTESIS}5\\ 19. & \lnot\varphi(e) & & \text{ELECCION}(18)\\ 20. & \forall v\varphi & & \text{HIPOTESIS}6\\ 21. & \varphi(e) & & \text{PARTICULARIZACION}(20)\\ 22. & (\varphi(e)\wedge\lnot\varphi(e)) & & \text{TESIS}6\text{CONJUNCIONINTRODUCCION}(21,19)\\ 23. & \forall v\varphi\rightarrow(\varphi(e)\wedge\lnot\varphi(e)) & & \text{CONCLUSION}\\ 24. & \lnot\forall v\varphi & & \text{TESIS}5\text{ABSURDO}(23)\\ 25. & (\exists v\lnot\varphi\rightarrow\lnot\forall v\varphi) & & \text{CONCLUSION}\\ 26. & (\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi) & & \text{EQUIVALENCIAINTRODUCCION}(17,25) \end{array}\]

Como detalle sorprendente de cuanto mas minimal se puede hacer la definición de prueba, el concepto de prueba dado en el libro de Mendelson solo usa cinco axiomas esquema y dos reglas, (Modus Ponens y generalización) y prueba los mismos teoremas que el nuestro ya que también en dicho texto se prueba el Teorema de Completitud relativo a tal definición de prueba. Por supuesto esta simplificación del concepto de prueba hace mucho mas difícil y técnico el desarrollo.

7.13.5 Propiedades Básicas de Pruebas y Teoremas

Por supuesto los números asociados a las hipótesis en una prueba son completamente arbitrarios y pueden cambiarse, es decir:

Proof. Es un chequeo largo pero trivial.  

También podemos cambiar los nombres de cte auxiliares

Proof. Sean \[\begin{aligned} \tau_{1} & =(\mathcal{C}\cup\mathcal{C}_{1},\mathcal{F},\mathcal{R},a)\\ \tau_{2} & =(\mathcal{C}\cup(\mathcal{C}_{1}-\{e\})\cup\{\tilde{e}\},\mathcal{F},\mathcal{R},a) \end{aligned}\] Para cada \(c\in\mathcal{C}\cup(\mathcal{C}_{1}-\{e\})\) definamos \(\tilde{c}=c\). Nótese que el mapeo \(c\rightarrow\tilde{c}\) es una biyección entre el conjunto de nombres de constante de \(\tau_{1}\) y el conjunto de nombres de cte de \(\tau_{2}\). Para cada \(t\in T^{\tau_{1}}\) sea \(\tilde{t}=\) resultado de reemplazar en \(t\) cada ocurrencia de \(c\) por \(\tilde{c}\), para cada \(c\in\mathcal{C}\cup\mathcal{C}_{1}\). Análogamente para una fórmula \(\psi\in F^{\tau_{1}}\), sea \(\tilde{\psi}=\) resultado de reemplazar en \(\psi\) cada ocurrencia de \(c\) por \(\tilde{c}\), para cada \(c\in\mathcal{C}\cup\mathcal{C}_{1}\). Nótese que los mapeos \(t\rightarrow\tilde{t}\) y \(\psi\rightarrow\tilde{\psi}\) son biyecciones naturales entre \(T^{\tau_{1}}\) y \(T^{\tau_{2}}\) y entre \(F^{\tau_{1}}\) y \(F^{\tau_{2}}\), respectivamente. Nótese que cualesquiera sean \(\psi_{1},\psi_{2}\in F^{\tau_{1}}\), tenemos que \(\psi_{1}\) se deduce de \(\psi_{2}\) por la regla de generalización con constante \(c\) sii \(\tilde{\psi}_{1}\) se deduce de \(\tilde{\psi}_{2}\) por la regla de generalización con constante \(\tilde{c}\). Para las otras reglas sucede lo mismo. Nótese también que \(c\) ocurre en \(\psi\) sii \(\tilde{c}\) ocurre en \(\tilde{\psi}.\) Mas aun nótese que \(c\) depende de \(d\) en \((\boldsymbol{\varphi},\mathbf{J})\) sii \(\tilde{c}\) depende de \(\tilde{d}\) en \((\mathbf{\tilde{\boldsymbol{\varphi}}},\mathbf{J})\), donde \(\mathbf{\tilde{\boldsymbol{\varphi}}}=\widetilde{\boldsymbol{\varphi}_{1}}...\widetilde{\boldsymbol{\varphi}_{n(\boldsymbol{\varphi})}}\). Ahora es fácil chequear que \((\mathbf{\tilde{\boldsymbol{\varphi}}},\mathbf{J})\) es una prueba formal de \(\varphi\) en \((\Sigma,\tau)\) basándose en que \((\boldsymbol{\varphi},\mathbf{J})\) es una prueba formal de \(\varphi\) en \((\Sigma,\tau)\).  

Proof. (1) Nótese que basta con hacer el caso \(n=1\). El caso con \(n\geq2\) se obtiene aplicando \(n\) veces el caso \(n=1\). Supongamos entonces que \((\Sigma,\tau)\vdash\varphi_{1}\) y \((\Sigma\cup\{\varphi_{1}\},\tau)\vdash\varphi\). Sea \((\alpha_{1}...\alpha_{h},I_{1}...I_{h})\) una prueba formal de \(\varphi_{1}\) en \((\Sigma,\tau)\). Sea \((\psi_{1}...\psi_{m},J_{1}...J_{m})\) una prueba formal de \(\varphi\) en \((\Sigma\cup\{\varphi_{1}\},\tau)\). Nótese que por los Lemas 7.41 y 7.42 podemos suponer que estas dos pruebas no comparten ningún nombre de constante auxiliar y que tampoco comparten números asociados a hipótesis o tesis. Para cada \(i=1,...,m\), definamos \(\widetilde{J_{i}}\) de la siguiente manera.

1. adhocprefix-adhocsufix Si \(J_{i}=\alpha\mathrm{AXIOMAPROPIO}\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \(\psi_{i}=\varphi_{1}\), entonces \(\widetilde{J_{i}}=\alpha\mathrm{EVOCACION}(\overline{h})\)

2. adhocprefix-adhocsufix Si \(J_{i}=\alpha\mathrm{AXIOMAPROPIO}\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \(\psi_{i}\notin\{\varphi_{1}\}\), entonces \(\widetilde{J_{i}}=\alpha\mathrm{AXIOMAPROPIO}\).

3. adhocprefix-adhocsufix Si \(J_{i}=\alpha\mathrm{AXIOMALOGICO}\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), entonces \(\widetilde{J_{i}}=\alpha\mathrm{AXIOMALOGICO}\)

4. adhocprefix-adhocsufix Si \(J_{i}=\alpha\mathrm{CONCLUSION}\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), entonces \(\widetilde{J_{i}}=\alpha\mathrm{CONCLUSION}\).

5. adhocprefix-adhocsufix Si \(J_{i}=\mathrm{HIPOTESIS}\bar{k}\), entonces \(\widetilde{J_{i}}=\mathrm{HIPOTESIS}\bar{k}\)

6. adhocprefix-adhocsufix Si \(J_{i}=\alpha R(\overline{l_{1}},...,\overline{l_{k}})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), entonces \(\widetilde{J_{i}}=\alpha R(\overline{l_{1}+h},...,\overline{l_{k}+h})\)

Es fácil chequear que \[(\alpha_{1}...\alpha_{h}\psi_{1}...\psi_{m},I_{1}...I_{h}\widetilde{J_{1}}...\widetilde{J_{m}})\] es una prueba formal de \(\varphi\) en \((\Sigma,\tau)\)

(2) Nótese que \[\begin{array}{llll} 1.\; & \varphi_{1} & & \text{AXIOMAPROPIO}\\ 2.\; & \varphi_{2} & & \text{AXIOMAPROPIO}\\ \vdots & \vdots & & \vdots\\ n. & \varphi_{n} & & \text{AXIOMAPROPIO}\\ n+1. & \varphi & & R(\bar{1},...,\bar{n}) \end{array}\] es una prueba formal de \(\varphi\) en \((\Sigma\cup\{\varphi_{1},...,\varphi_{n}\},\tau)\), lo cual por (1) nos dice que \((\Sigma,\tau)\vdash\varphi\).

(3) Supongamos \((\Sigma,\tau)\vdash(\varphi\rightarrow\psi)\). Entonces tenemos que \((\Sigma\cup\{\varphi\},\tau)\vdash(\varphi\rightarrow\psi),\varphi\), lo cual por (2) nos dice que \((\Sigma\cup\{\varphi\},\tau)\vdash\psi\). Supongamos ahora que \((\Sigma\cup\{\varphi\},\tau)\vdash\psi\). Sea \((\varphi_{1}...\varphi_{n},J_{1}...,J_{n})\) una prueba formal de \(\psi\) en \((\Sigma\cup\{\varphi\},\tau)\). Para cada \(i=1,...,n\), definamos \(\widetilde{J_{i}}\) de la siguiente manera.

1. adhocprefix-adhocsufix Si \(\varphi_{i}=\varphi\) y \(J_{i}=\alpha\mathrm{AXIOMAPROPIO}\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), entonces \(\widetilde{J_{i}}=\alpha\mathrm{EVOCACION}(1)\)

2. adhocprefix-adhocsufix Si \(\varphi_{i}\neq\varphi\) y \(J_{i}=\alpha\mathrm{AXIOMAPROPIO}\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), entonces \(\widetilde{J_{i}}=\alpha\mathrm{AXIOMAPROPIO}\)

3. adhocprefix-adhocsufix Si \(J_{i}=\alpha\mathrm{AXIOMALOGICO}\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), entonces \(\widetilde{J_{i}}=\alpha\mathrm{AXIOMALOGICO}\)

4. adhocprefix-adhocsufix Si \(J_{i}=\alpha\mathrm{CONCLUSION}\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), entonces \(\widetilde{J_{i}}=\alpha\mathrm{CONCLUSION}\)

5. adhocprefix-adhocsufix Si \(J_{i}=\mathrm{HIPOTESIS}\bar{k}\), entonces \(\widetilde{J_{i}}=\mathrm{HIPOTESIS}\bar{k}\)

6. adhocprefix-adhocsufix Si \(J_{i}=\alpha R(\overline{l_{1}},...,\overline{l_{k}})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), entonces \(\widetilde{J_{i}}=\alpha R(\overline{l_{1}+1},...,\overline{l_{k}+1})\)

Sea \(m\) tal que ninguna \(J_{i}\) es igual a \(\mathrm{HIPOTESIS}\bar{m}\). Nótese que \(\widetilde{J_{n}}\) no es de la forma \(\mathrm{TESIS}\bar{k}\beta\) ni de la forma \(\mathrm{HIPOTESIS}\bar{k}\) (por que?) por lo cual \(\mathrm{TESIS}\bar{m}\widetilde{J_{n}}\) es una justificación. Es fácil chequear que \[(\varphi\varphi_{1}...\varphi_{n}(\varphi\rightarrow\psi),\text{HIPOTESIS}\bar{m}\widetilde{J_{1}}...\widetilde{J_{n-1}}\mathrm{TESIS}\bar{m}\widetilde{J_{n}}\text{CONCLUSION})\] es una prueba formal de \((\varphi\rightarrow\psi)\) en \((\Sigma,\tau)\)  

7.13.6 Consistencia

Una teoría \((\Sigma,\tau)\) será inconsistente cuando haya una sentencia \(\varphi\) tal que \((\Sigma,\tau)\vdash(\varphi\wedge\lnot\varphi).\) Una teoría \((\Sigma,\tau)\) será consistente cuando no sea inconsistente.

Proof. (1) Si \((\Sigma,\tau)\) es inconsistente, entonces por definición tenemos que \((\Sigma,\tau)\vdash\psi\wedge\lnot\psi\) para alguna sentencia \(\psi\). Dada una sentencia cualquiera \(\varphi\) tenemos que \(\varphi\) se deduce por la regla del absurdo a partir de \(\psi\wedge\lnot\psi\) con lo cual (2) del Lema 7.43 nos dice que \((\Sigma,\tau)\vdash\varphi\)

(2) Supongamos \((\Sigma,\tau)\) es consistente y \((\Sigma,\tau)\vdash\varphi\). Si \((\Sigma\cup\{\varphi\},\tau)\) fuera inconsistente, entonces \((\Sigma\cup\{\varphi\},\tau)\vdash\psi\wedge\lnot\psi\), para alguna sentencia \(\psi\), lo cual por (1) del Lema 7.43 nos diría que \((\Sigma,\tau)\vdash\psi\wedge\lnot\psi\), es decir nos diría que \((\Sigma,\tau)\) es inconsistente.

(3) es dejada al lector.  

7.13.7 El Teorema de Corrección

Como ya vimos en las secciones anteriores, el concepto matemático de prueba formal en una teoría \((\Sigma,\tau)\) fue hecho como un intento de modelizar ciertas pruebas que realizan los matemáticos profesionales, a las que llamamos pruebas elementales. Es claro que cuando un matemático hace una prueba elemental de una sentencia \(\varphi\) en una teoría \((\Sigma,\tau)\), comienza imaginando una estructura \(\mathbf{A}\) de tipo \(\tau\) de la cual lo único que sabe es que ella satisface todas las sentencias de \(\Sigma\), y luego al finalizar la prueba concluye que dicho modelo imaginario satisface la última sentencia de la prueba, i.e. \(\varphi\). En algún sentido la misión de una prueba es justamente eso: justificar con solidez que la sentencia a probar vale en todos los modelos de la teoría.

O sea que si nuestro concepto de prueba formal permitiera probar sentencias que no sean verdaderas en todos los modelos de la teoría, no seria correcto. Este no es el caso y el teorema que asegura que las pruebas formales solo prueban sentencias verdaderas en todos los modelos de la teoría se llama Teorema de Corrección. Lo enunciaremos formalmente a continuación aunque no daremos la prueba ya que es dificultosa. Antes una definición. Dada \((\Sigma,\tau)\) una teoría y \(\varphi\) una sentencia de tipo \(\tau\), escribiremos \((\Sigma,\tau)\models\varphi\) cuando \(\varphi\) sea verdadera en todo modelo de \((\Sigma,\tau)\).

Cabe destacar que el Teorema de Corrección hace parte de la tarea encomendada en el punto (4) del Programa de Lógica Matemática ya que asegura que nuestro concepto de prueba formal no es demasiado permisivo como para permitir probar sentencias que son falsas en algún modelo de la teoría. Pero dicho concepto podría ser incorrecto en el sentido que podría haber pruebas elementales dadas por matemáticos la cuales no puedan ser simuladas por pruebas formales. Por ejemplo podría pasar que mañana un matemático diera una prueba elemental de una sentencia \(\varphi\) en una teoría \((\Sigma,\tau)\) pero que no haya una prueba formal de \(\varphi\) en \((\Sigma,\tau)\). En tal caso nuestro modelo de prueba formal seria un modelo erróneo del concepto de prueba elemental, por ser incompleto. Por supuesto en ese caso podríamos mejorarlo viendo la prueba elemental dada por dicho matemático y enriqueciendo a la luz de dicha prueba nuestra definición de prueba formal. De todas maneras nos quedaría la duda de que aun esta nueva definición de prueba sea incompleta .... Como veremos el Teorema de Completitud de Godel prueba que este no es el caso!

Un corolario muy importante del Teorema de Corrección es el siguiente.

Proof. Supongamos \(\mathbf{A}\) es un modelo de \((\Sigma,\tau)\). Si \((\Sigma,\tau)\) fuera inconsistente, entonces toda sentencia de tipo \(\tau\) seria un teorema de \((\Sigma,\tau)\), en particular tendríamos que \(\exists x_{1}\lnot(x_{1}\equiv x_{1})\) seria un teorema de \((\Sigma,\tau)\), lo cual por el Teorema de Corrección nos diría que \(\mathbf{A}\models\exists x_{1}\lnot(x_{1}\equiv x_{1})\), lo cual no es cierto. O sea que \((\Sigma,\tau)\) es consistente  

El Teorema de Corrección es muy útil para asegurar que una sentencia no es un teorema de una teoría dada. Mas concretamente tenemos el siguiente criterio:

1. adhocprefixNoEsTeoremaadhocsufix Si Ud quiere probar que una sentencia \(\varphi\in S^{\tau}\) no es teorema de una teoría \((\Sigma,\tau)\) basta con encontrar un modelo de \((\Sigma,\tau)\) para el cual \(\varphi\) sea falsa.

Dejamos al lector justificar este criterio usando el Teorema de Corrección. Podemos usarlo, por ejemplo, para ver que ni la sentencia \[Dis_{1}=\forall x_{1}\forall x_{2}(\mathsf{i}(x_{1},\mathsf{s}(x_{2},x_{3}))\equiv\mathsf{s}(\mathsf{i}(x_{1},x_{2}),\mathsf{i}(x_{1},x_{3})))\] ni su negación son teoremas de \(RetCua\) ya que hay reticulados cuaterna distributivos y también hay reticulados cuaterna no distributivos.

Concluimos la subsección dando algunos ejemplos que muestran que si hacemos mas permisiva la definición de prueba formal, esta ya no resulta correcta, es decir ya no vale el Teorema de Corrección.

1. adhocprefixEjemplo 1:adhocsufix Este ejemplo muestra que en la sentencia a generalizar (dentro de una prueba formal) no puede ocurrir un nombre de cte el cual dependa del nombre de cte a generalizar. Sea \(\tau=(\emptyset,\{f^{1}\},\emptyset,a)\) y sea \(\Sigma=\{\forall y\exists x\;y\equiv f(x)\}\). Sea \(T=(\Sigma,\tau)\). Nótese que una estructura \(\mathbf{A}\) de tipo \(\tau\) es modelo de \(T\) sii \(f^{\mathbf{A}}\) es una función sobre. Consideremos \[\begin{array}{llll} \ 1. & \forall y\exists x\;y\equiv f(x) & & \text{AXIOMAPROPIO}\\ \ 2. & \exists x\;y_{0}\equiv f(x) & & \text{PARTICULARIZACION}(1)\\ \ 3. & y_{0}\equiv f(e) & & \text{ELECCION}(2)\\ \ 4. & \forall y\;y\equiv f(e) & & \text{GENERALIZACION}(3)\\ \ 5. & c\equiv f(e) & & \text{PARTICULARIZACION}(4)\\ \ 6. & d\equiv f(e) & & \text{PARTICULARIZACION}(4)\\ \ 7. & f(e)\equiv d & & \text{COMMUTATIVIDAD}(6)\\ \ 8. & c\equiv d & & \text{TRANSITIVIDAD}(5,7)\\ \ 9. & \forall y\;c\equiv y & & \text{GENERALIZACION}(8)\\ 10. & \forall x\forall y\;x\equiv y & & \text{GENERALIZACION}(9) \end{array}\] Obviamente, si permitiéramos que lo anterior fuera una prueba formal, dejaría de valer el Teorema de Corrección ya que hay muchos modelos de \(T\), los cuales no satisfacen \(\forall x\forall y\;x\equiv y\).

2. adhocprefixEjemplo 2:adhocsufix El siguiente ejemplo muestra que el nombre de cte a generalizar no puede ocurrir en hipótesis de la sentencia a la cual se le aplica la generalización. Sea \(\tau=(\{1\},\emptyset,\emptyset,\emptyset)\) y sea \(T=(\emptyset,\tau)\). Consideremos \[\begin{array}{llll} 1.\; & c\equiv1 & & \text{HIPOTESIS}1\\ 2.\; & \forall x\;x\equiv1 & & \text{TESIS}1\text{GENERALIZACION}(1)\\ 3.\; & (c\equiv1\rightarrow\forall x\;x\equiv1) & & \text{CONCLUSION}\\ 4.\; & \forall y\;\left(y\equiv1\rightarrow\forall x\;x\equiv1\right) & & \text{GENERALIZACION}(3)\\ 5.\; & \left(1\equiv1\rightarrow\forall x\;x\equiv1\right) & & \text{PARTICULARIZACION}(4)\\ 6. & 1\equiv1 & & \text{AXIOMALOGICO}\\ 7. & \forall x\;x\equiv1 & & \text{MODUSPONENS}(5,6) \end{array}\] Si permitiéramos que lo anterior fuera una prueba formal, dejaría de valer el Teorema de Corrección ya que hay muchos modelos de \(T\) (toda estructura es un modelo de \(T\)) los cuales no satisfacen \(\forall x\;x\equiv1\).

3. adhocprefixEjemplo 3:adhocsufix El siguiente ejemplo muestra que la sentencia a generalizar no puede tener una hipótesis en la cual ocurra un nombre de cte que dependa del nombre de cte que se generaliza. Sea \(\tau=(\emptyset,\emptyset,\emptyset,\emptyset)\) y sea \(T=(\emptyset,\tau)\). Consideremos \[\begin{array}{llll} \ 1. & c\equiv c & & \text{AXIOMALOGICO}\\ \ 2. & \exists z\;z\equiv c & & \text{EXISTENCIA}(1)\\ \ 3. & e\equiv c & & \text{ELECCION}(2)\\ \ 4. & d\equiv e & & \text{HIPOTESIS}1\\ \ 5. & d\equiv c & & \text{TRANSITIVIDAD}(4,3)\\ \ 6. & \forall y\;d\equiv y & & \text{TESIS}1\text{GENERALIZACION}(5)\\ \ 7. & d\equiv e\rightarrow\forall y\;d\equiv y & & \text{CONCLUSION}\\ \ 8. & \forall x(x\equiv e\rightarrow\forall y\;x\equiv y) & & \text{GENERALIZACION}(7)\\ \ 9. & e\equiv e\rightarrow\forall y\;e\equiv y & & \text{PARTICULARIZACION}(8)\\ 10. & e\equiv e & & \text{AXIOMALOGICO}\\ 11. & \forall y\;e\equiv y & & \text{MODUSPONENS}(10,9)\\ 12. & \forall y\;c\equiv y & & \text{REEMPLAZO}(3,11)\\ 13. & \forall x\forall y\;x\equiv y & & \text{GENERALIZACION}(12) \end{array}\]

7.13.8 El Álgebra de Lindenbaum

Recordemos que dado un tipo \(\tau\), con \(S^{\tau}\) denotamos el conjunto de las sentencias de tipo \(\tau\), es decir \[S^{\tau}=\{\varphi\in F^{\tau}:Li(\varphi)=\emptyset\}\] Sea \(T=(\Sigma,\tau)\) una teoría. Podemos definir la siguiente relación binaria sobre \(S^{\tau}\): \[\varphi\dashv\vdash_{T}\psi\text{ si y solo si }T\vdash\left(\varphi\leftrightarrow\psi\right)\] Es decir \[\dashv\vdash_{T}=\{(\varphi,\psi)\in S^{\tau}\times S^{\tau}:T\vdash\left(\varphi\leftrightarrow\psi\right)\}\]

Proof. La relación es reflexiva ya que cualquiera sea la \(\varphi\in S^{\tau}\) tenemos que \[\begin{array}{llll} 1. & \varphi & & \text{HIPOTESIS}1\\ 2. & \varphi & & \text{TESIS}1\text{EVOCACION}(1)\\ 3. & (\varphi\rightarrow\varphi) & & \text{CONCLUSION}\\ 4. & (\varphi\rightarrow\varphi) & & \text{EVOCACION}(3)\\ 5. & (\varphi\leftrightarrow\varphi) & & \text{EQUIVALENCIAINTRODUCCION}(3,4) \end{array}\] es una prueba formal de \(((\varphi\leftrightarrow\varphi)\) en \(T\). Veamos que es simétrica. Supongamos que \(\varphi\dashv\vdash_{T}\psi\), es decir \(T\vdash\left(\varphi\leftrightarrow\psi\right)\). Ya que \(\left(\psi\leftrightarrow\varphi\right)\) se deduce de \((\varphi\leftrightarrow\psi)\) por la regla de conmutatividad, (2) del Lema 7.43 nos dice que \(T\vdash\left(\psi\leftrightarrow\varphi\right)\).

Análogamente, usando la regla de transitividad se puede probar que \(\dashv\vdash_{T}\) es transitiva.  

Dada una teoría \(T=(\Sigma,\tau)\) y \(\varphi\in S^{\tau}\), \([\varphi]_{T}\) denotará la clase de \(\varphi\) con respecto a la relación de equivalencia \(\dashv\vdash_{T}\). Una sentencia \(\varphi\) se dice refutable en \(T\) si \(T\vdash\lnot\varphi\).

Proof. Haremos la prueba de (2) y dejaremos la prueba de (1) como ejercicio. Nótese que \(\exists x_{1}\neg(x_{1}\equiv x_{1})\) es refutable en \(T\) ya que \[\begin{array}{llll} 1.\; & \exists x_{1}\neg(x_{1}\equiv x_{1}) & & \text{HIPOTESIS1}\\ 2.\; & \neg(e\equiv e) & & \text{ELECCION}(1)\\ 3.\; & (e\equiv e) & & \text{AXIOMALOGICO}\\ 4.\; & ((e\equiv e)\wedge\neg(e\equiv e)) & & \text{TESIS1CONJUNCIONINTRODUCCION}(3,2)\\ 5.\; & (\exists x_{1}\neg(x_{1}\equiv x_{1})\rightarrow((e\equiv e)\wedge\neg(e\equiv e))) & & \text{CONCLUSION}\\ 6.\; & \neg\exists x_{1}\neg(x_{1}\equiv x_{1}) & & \text{ABSURDO}(5) \end{array}\] es una prueba de \(\neg\exists x_{1}\neg(x_{1}\equiv x_{1})\) en \(T\). Ahora veamos que si \(\varphi\) es refutable en \(T\) y \(\varphi\dashv\vdash_{T}\psi\), entonces \(\psi\) es refutable en \(T\). Nótese que \[\begin{array}{llll} 1.\; & \lnot\varphi & & \text{AXIOMAPROPIO}\\ 2.\; & (\varphi\leftrightarrow\psi) & & \text{AXIOMAPROPIO}\\ 3.\; & \lnot\psi & & \text{REEMPLAZO}(2,1) \end{array}\] es una prueba de \(\lnot\psi\) en \((\Sigma\cup\{\lnot\varphi,(\varphi\leftrightarrow\psi)\},\tau)\), lo cual por (1) del Lema 7.43 nos dice que \(\psi\) es refutable en \(T\). Ya que \(\exists x_{1}\neg(x_{1}\equiv x_{1})\) es refutable en \(T\), lo anterior nos dice que \[[\exists x_{1}\neg(x_{1}\equiv x_{1})]_{T}\subseteq\{\varphi\in S^{\tau}:\varphi\text{ es refutable en }T\}\] Para terminar la prueba de (2) nótese que basta con probar que si \(\varphi\text{ y }\psi\) son refutables en \(T\), entonces \(\varphi\dashv\vdash_{T}\psi\). Pero \[\begin{array}{llll} 1.\; & \varphi & & \text{HIPOTESIS}1\\ 2.\; & \lnot\varphi & & \text{AXIOMAPROPIO}\\ 3.\; & (\varphi\wedge\lnot\varphi) & & \text{CONJUNCIONINTRODUCCION}(1,3)\\ 4. & \psi & & \text{TESIS}1\text{ABSURDO}(3)\\ 5. & (\varphi\rightarrow\psi) & & \text{CONCLUSION}\\ 6. & \psi & & \text{HIPOTESIS}2\\ 7. & \lnot\psi & & \text{AXIOMAPROPIO}\\ 8. & (\psi\wedge\lnot\psi) & & \text{CONJUNCIONINTRODUCCION}(6,7)\\ 9. & \varphi & & \text{TESIS}2\text{ABSURDO}(8)\\ 10. & (\psi\rightarrow\varphi) & & \text{CONCLUSION}\\ 11. & (\varphi\leftrightarrow\psi) & & \text{EQUIVALENCIAINTRODUCCION}(5,10) \end{array}\] justifica que \((\Sigma\cup\{\lnot\varphi,\lnot\psi\},\tau)\vdash(\varphi\leftrightarrow\psi)\) por lo cual si \(\varphi\text{ y }\psi\) son refutables en \(T\), se puede aplicar (1) del Lema 7.43 y obtener que \(\varphi\dashv\vdash_{T}\psi\).  

Definiremos sobre \(S^{\tau}/\mathrm{\dashv\vdash}_{T}\) la siguiente operación binaria \(\mathsf{s}^{T}\): \[[\varphi]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\psi]_{T}=[(\varphi\vee\psi)]_{T}\] Una observación importante es que para que la definición anterior de la operación \(\mathsf{s}^{T}\) sea inambigua, debemos probar la siguiente propiedad

1. adhocprefix-adhocsufix Si \([\varphi]_{T}=[\varphi^{\prime}]_{T}\) y \([\psi]_{T}=[\psi^{\prime}]_{T}\) entonces \([(\varphi\vee\psi)]_{T}=[(\varphi^{\prime}\vee\psi^{\prime})]_{T}\)

Es decir debemos probar que si \(T\vdash\left(\varphi\leftrightarrow\varphi^{\prime}\right)\) y \(T\vdash\left(\psi\leftrightarrow\psi^{\prime}\right)\), entonces \(T\vdash((\varphi\vee\psi)\leftrightarrow(\varphi^{\prime}\vee\psi^{\prime}))\). Supongamos que \(T\vdash\left(\varphi\leftrightarrow\varphi^{\prime}\right)\) y \(T\vdash\left(\psi\leftrightarrow\psi^{\prime}\right)\). Nótese que también \(T\vdash((\varphi\vee\psi)\leftrightarrow(\varphi\vee\psi))\) (ya probamos que \(\dashv\vdash_{T}\) es reflexiva). Además tenemos que \[\begin{array}{llll} 1.\; & \left(\varphi\leftrightarrow\varphi^{\prime}\right) & & \text{AXIOMAPROPIO}\\ 2.\; & \left(\psi\leftrightarrow\psi^{\prime}\right) & & \text{AXIOMAPROPIO}\\ 3.\; & ((\varphi\vee\psi)\leftrightarrow(\varphi\vee\psi)) & & \text{AXIOMALOGICO}\\ 4.\; & ((\varphi\vee\psi)\leftrightarrow(\varphi^{\prime}\vee\psi)) & & \text{REEMPLAZO}(1,3)\\ 5.\; & ((\varphi\vee\psi)\leftrightarrow(\varphi^{\prime}\vee\psi^{\prime})) & & \text{REEMPLAZO}(2,4) \end{array}\] atestigua que \[(\Sigma\cup\{\left(\varphi\leftrightarrow\varphi^{\prime}\right),\left(\psi\leftrightarrow\psi^{\prime}\right),((\varphi\vee\psi)\leftrightarrow(\varphi\vee\psi))\},\tau)\vdash((\varphi\vee\psi)\leftrightarrow(\varphi^{\prime}\vee\psi^{\prime}))\] lo cual nos dice por (1) del Lema 7.43 que \(T\vdash((\varphi\vee\psi)\leftrightarrow(\varphi^{\prime}\vee\psi^{\prime}))\).

En forma análoga se puede ver que las siguientes igualdades definen en forma inambigua una operación binaria \(\mathsf{i}^{T}\) sobre \(S^{\tau}/\mathrm{\dashv\vdash}_{T}\) y una operación unaria \(^{\mathsf{c}^{T}}\) sobre \(S^{\tau}/\mathrm{\dashv\vdash}_{T}\): \[\begin{aligned} _{T}\;\mathsf{i}^{T}\mathsf{\;}[\psi]_{T} & =[(\varphi\wedge\psi)]_{T}\\ ([\varphi]_{T})^{\mathsf{c}^{T}} & =[\lnot\varphi]_{T} \end{aligned}\] Dejamos al lector los detalles.

Dada una teoría \(T=(\Sigma,\tau)\), denotemos con \(1^{T}\) al conjunto \(\{\varphi\in S^{\tau}:\varphi\) es un teorema de \(T\}\) y con \(0^{T}\) al conjunto \(\{\varphi\in S^{\tau}:\varphi\) es refutable en \(T\}\). Ya vimos en un lema anterior que \(0^{T}\) y \(1^{T}\) pertenecen a \(S^{\tau}/\mathrm{\dashv\vdash}_{T}\). Podemos enunciar ahora el siguiente resultado, inspirado en la idea clásica de Boole para el calculo proposicional.

Proof. Por definición de álgebra de Boole, debemos probar que cualesquiera sean \(\varphi_{1},\varphi_{2},\varphi_{3}\in S^{\tau}\), se cumplen las siguientes igualdades:

1. adhocprefix(1)adhocsufix \([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{1}]_{T}=[\varphi_{1}]_{T}\)

2. adhocprefix(2)adhocsufix \([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{1}]_{T}=[\varphi_{1}]_{T}\)

3. adhocprefix(3)adhocsufix \([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{2}]_{T}=[\varphi_{2}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{1}]_{T}\)

4. adhocprefix(4)adhocsufix \([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{2}]_{T}=[\varphi_{2}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{1}]_{T}\)

5. adhocprefix(5)adhocsufix \([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}([\varphi_{2}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{3}]_{T})=([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{2}]_{T})\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{3}]_{T}\)

6. adhocprefix(6)adhocsufix \([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}([\varphi_{2}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T})=([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{2}]_{T})\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T}\)

7. adhocprefix(7)adhocsufix \([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{2}]_{T})=[\varphi_{1}]_{T}\)

8. adhocprefix(8)adhocsufix \([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{2}]_{T})=[\varphi_{1}]_{T}\)

9. adhocprefix(9)adhocsufix \(0^{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{1}]_{T}=[\varphi_{1}]_{T}\)

10. adhocprefix(10)adhocsufix \([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}1^{T}=1^{T}\)

11. adhocprefix(11)adhocsufix \([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}([\varphi_{1}]_{T})^{\mathsf{c}^{T}}=1^{T}\)

12. adhocprefix(12)adhocsufix \([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}([\varphi_{1}]_{T})^{\mathsf{c}^{T}}=0^{T}\)

13. adhocprefix(13)adhocsufix \([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}([\varphi_{2}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T})=([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{2}]_{T})\;\mathsf{s}^{T}\mathsf{\;}([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{3}]_{T})\)

Veamos por ejemplo que se da (10), es decir probaremos que \([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}1^{T}=1^{T}\), cualesquiera sea la sentencia \(\varphi_{1}\). Por el Lema 7.46 debemos probar que para cualquier \(\varphi_{1}\in S^{\tau}\), se da que \[[\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\forall x_{1}(x_{1}\equiv x_{1})]_{T}=[\forall x_{1}(x_{1}\equiv x_{1})]_{T}\] Ya que \([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\forall x_{1}(x_{1}\equiv x_{1})]_{T}=[(\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1}))]_{T}\), debemos probar que \[[(\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1}))]_{T}=[\forall x_{1}(x_{1}\equiv x_{1})]_{T}\] o equivalentemente \[T\vdash((\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1}))\leftrightarrow\forall x_{1}(x_{1}\equiv x_{1}))\] Nótese que por (2) del Lema 7.43, basta con probar que \[\begin{aligned} T & \vdash((\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1}))\rightarrow\forall x_{1}(x_{1}\equiv x_{1}))\\ T & \vdash(\forall x_{1}(x_{1}\equiv x_{1})\rightarrow(\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1}))) \end{aligned}\] Dejamos la segunda al lector. Para la primera tenemos la siguiente prueba formal \[\begin{array}{llll} 1.\; & c\equiv c & & \text{AXIOMALOGICO}\\ 2.\; & \forall x_{1}(x_{1}\equiv x_{1}) & & \text{GENERALIZACION}(1)\\ 3. & (\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1})) & & \text{HIPOTESIS1}\\ 4. & \forall x_{1}(x_{1}\equiv x_{1}) & & \text{TESIS1EVOCACION}\text{(2)}\\ 5. & ((\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1}))\rightarrow\forall x_{1}(x_{1}\equiv x_{1})) & & \text{CONCLUSION} \end{array}\] (\(c\) es un nombre de cte no perteneciente a \(\mathcal{C}\) y tal que \((\mathcal{C}\cup\{c\},\mathcal{F},\mathcal{R},a)\) es un tipo).

Veamos ahora que se da (6), es decir veamos que \[[\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}([\varphi_{2}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T})=([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{2}]_{T})\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T}\] cualesquiera sean \(\varphi_{1},\varphi_{2},\varphi_{3}\in S^{\tau}\). Sean \(\varphi_{1},\varphi_{2},\varphi_{3}\in S^{\tau}\) fijas. Por la definición de la operación \(\mathsf{s}^{T}\) tenemos que \[\begin{array}{llll} [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}([\varphi_{2}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T}) & = & [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[(\varphi_{2}\vee\varphi_{3})]_{T}\\ & = & [(\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3}))]_{T}\\ \\([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{2}]_{T})\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T} & = & [(\varphi_{1}\vee\varphi_{2})]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T}\\ & = & [((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3})]_{T} \end{array}\] O sea que debemos probar que \[[(\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3}))]_{T}=[((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3})]_{T}\] es decir, debemos probar que \[T\vdash((\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3}))\leftrightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}))\] Nótese que por (2) del Lema 7.43, basta con probar que \[\begin{aligned} T & \vdash((\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3}))\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}))\\ T & \vdash(((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3})\rightarrow(\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3}))) \end{aligned}\] La siguiente es una prueba formal de \(((\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3}))\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}))\) en \(T\) y dejamos al lector la otra prueba formal. \[\begin{array}{llll} 1. & (\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3})) & & \text{HIPOTESIS}1\\ 2. & \varphi_{1} & & \text{HIPOTESIS}2\\ 3. & (\varphi_{1}\vee\varphi_{2}) & & \text{DISJUNCIONINTRODUCCION}(2)\\ 4. & ((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{TESIS}2\text{DISJUNCIONINTRODUCCION}(3)\\ 5. & \varphi_{1}\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{CONCLUSION}\\ 6. & (\varphi_{2}\vee\varphi_{3}) & & \text{HIPOTESIS}3\\ 7. & \varphi_{2} & & \text{HIPOTESIS}4\\ 8. & (\varphi_{1}\vee\varphi_{2}) & & \text{DISJUNCIONINTRODUCCION}(7)\\ 9. & ((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{TESIS}4\text{DISJUNCIONINTRODUCCION}(8)\\ 10. & \varphi_{2}\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{CONCLUSION}\\ 11. & \varphi_{3} & & \text{HIPOTESIS}5\\ 12. & ((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{TESIS}5\text{DISJUNCIONINTRODUCCION}(11)\\ 13. & \varphi_{3}\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{CONCLUSION}\\ 14. & ((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{TESIS}3\text{DIVISIONPORCASOS}(6,10,13)\\ 15. & (\varphi_{2}\vee\varphi_{3})\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{CONCLUSION}\\ 16. & ((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{TESIS}1\text{DIVISIONPORCASOS}(1,5,15)\\ 17. & (\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3}))\rightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{CONCLUSION} \end{array}\] El resto de las propiedades pueden ser probadas en forma similar, algunas de las pruebas formales necesarias han sido dadas en los ejemplos que siguen a la definición de prueba formal  

Dada una teoría \(T=(\Sigma,\tau)\), denotaremos con \(\mathcal{A}_{T}\) al álgebra de Boole \((S^{\tau}/\mathrm{\dashv\vdash}_{T},\mathsf{s}^{T},\mathsf{i}^{T},^{\mathsf{c}^{T}},0^{T},1^{T})\). El álgebra \(\mathcal{A}_{T}\) será llamada el álgebra de Lindenbaum de \(T\). Denotaremos con \(\leq^{T}\) al orden parcial asociado al álgebra de Boole \(\mathcal{A}_{T}\) (es decir \([\varphi]_{T}\leq^{T}[\psi]_{T}\) si y solo si \([\varphi]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\psi]_{T}=[\psi]_{T}\)). El siguiente lema nos da una descripción agradable de \(\leq^{T}\).

Proof. Supongamos que \([\varphi]_{T}\leq^{T}[\psi]_{T}\), es decir supongamos que \([\varphi]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\psi]_{T}=[\psi]_{T}\). Por la definición de \(\mathsf{s}^{T}\) tenemos que \([(\varphi\vee\psi)]_{T}=[\psi]_{T}\), es decir \(T\vdash((\varphi\vee\psi)\leftrightarrow\psi)\). Es fácil ver entonces que \(T\vdash\left(\varphi\rightarrow\psi\right)\). Recíprocamente si \(T\vdash\left(\varphi\rightarrow\psi\right)\), entonces fácilmente podemos probar que \(T\vdash((\varphi\vee\psi)\leftrightarrow\psi)\), lo cual nos dice que \([(\varphi\vee\psi)]_{T}=[\psi]_{T}\). Por la definición de\(\ \mathsf{s}^{T}\) tenemos que \([\varphi]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\psi]_{T}=[\psi]_{T}\), lo cual nos dice que \([\varphi]_{T}\leq^{T}[\psi]_{T}\)  

7.13.9 Teorema de Completitud

Hasta el momento tenemos una definición matemática de prueba formal que modeliza el concepto intuitivo de prueba elemental, el cual corresponde al mundo real de los matemáticos profesionales. Ahora bien, nada nos asegura que no aparezca un matemático que realice una prueba elemental de una sentencia \(\varphi\) en una teoría \((\Sigma,\tau)\), y que no haya una prueba formal de \(\varphi\) en \((\Sigma,\tau)\). En tal caso nuestro concepto de prueba seria incompleto (como modelo) aunque, como ya se vio, el mismo es correcto. Esto podría pasar por ejemplo si nos hubiésemos olvidado de incluir en nuestra definición de prueba formal alguna regla o acción que el matemático usara para probar dicha \(\varphi\), es decir nos podría pasar que no podamos "traducir" dicha prueba elemental a una prueba formal. Parece difícil poder asegurar o probar que nuestro concepto de prueba formal sea completo en el sentido antes descripto ya que el concepto de prueba elemental es empírico puesto que depende de las acciones de la comunidad matemática profesional y además no tiene una formulación precisa. Por otra parte nada nos asegura que los matemáticos profesionales no vayan a descubrir en el futuro algún nuevo "truco" elemental y que nuestro concepto que era completo pase a ser incompleto.

Fue un verdadero desafío científico (de los años cercanos a 1900) lidiar con estos problemas, y el Teorema de Completitud de Godel resuelve todo de una manera limpia y asombrosa. La razón es muy simple: Godel prueba que si una sentencia \(\varphi\) es verdadera en todos los modelos de \((\Sigma,\tau)\), entonces hay una prueba formal de \(\varphi\) en \((\Sigma,\tau)\). Ya que toda prueba elemental que haga un matemático (ahora o en el futuro) siempre probara una sentencia que es verdadera en cada modelo de \((\Sigma,\tau)\), el teorema de Godel nos garantiza que para cada prueba elemental (de ahora y del futuro) habrá una prueba formal que pruebe la misma sentencia!

Por supuesto queda la posibilidad de que una prueba elemental dada por algún matemático (ahora o en el futuro) no sea traducible en forma natural a una prueba formal que pruebe lo mismo (mas allá de que sepamos que hay una gracias a Godel). Sin embargo el lector se ira convenciendo que esto es improbable que suceda, a medida que vaya formalizando distintas pruebas elementales clásicas dadas por los matemáticos a lo largo de la historia.

Cabe destacar que entonces el Teorema de Corrección junto con el Teorema de Completitud resuelven el punto (4) del Programa de Lógica Matemática.

Para probar el Teorema de Completitud necesitaremos algunos resultados. Dados dos tipos cualesquiera \(\tau\) y \(\tau^{\prime}\) definamos \(\tau_{\cap}=(\mathcal{C}_{\cap},\mathcal{F}_{\cap},\mathcal{R}_{\cap},a_{\cap})\), donde \[\begin{aligned} \mathcal{C}_{\cap} & =\mathcal{C}\cap\mathcal{C}^{\prime}\\ \mathcal{F}_{\cap} & =\{f\in\mathcal{F}\cap\mathcal{F}^{\prime}:a(f)=a^{\prime}(f)\}\\ \mathcal{R}_{\cap} & =\{r\in\mathcal{R}\cap\mathcal{R}^{\prime}:a(r)=a^{\prime}(r)\}\\ a_{\cap} & =a|_{\mathcal{F}_{\cap}\cup\mathcal{R}_{\cap}} \end{aligned}\]

Proof. (a) Es directo y dejado al lector.

(b) Es directo (y dejado al lector) probar por inducción que \(T_{k}^{\tau_{\cap}}\subseteq T^{\tau}\cap T^{\tau^{\prime}}\), para cada \(k\in\omega\). Esto prueba que \(T^{\tau_{\cap}}\subseteq T^{\tau}\cap T^{\tau^{\prime}}\). Veamos la otra inclusión. Lo probaremos usando la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Si \(t\in T_{k}^{\tau}\cap T^{\tau^{\prime}}\), entonces \(t\in T^{\tau_{\cap}}\).

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Supongamos \(t\in T_{0}^{\tau}\cap T^{\tau^{\prime}}\). Obviamente si \(t\in Var\), entonces \(t\in T^{\tau_{\cap}}\). Supongamos que \(t\in\mathcal{C}\). Ya que en \(t\) no ocurren paréntesis ni numerales y además \(t\in T^{\tau^{\prime}}\), tenemos que \(t\) debe estar en \(\mathcal{C}^{\prime}\). O sea que \(t\in\mathcal{C}\cap\mathcal{C}^{\prime}\subseteq T^{\tau_{\cap}}\).

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Supongamos \(t\in T_{k+1}^{\tau}\cap T^{\tau^{\prime}}\). Veremos que \(t\in T^{\tau_{\cap}}\). Por la definición de \(T_{k+1}^{\tau}\) hay dos casos.

Caso \(t\in T_{k}^{\tau}\). Trivial ya que vale \(\mathrm{Enu}_{k}\).

Caso \(t=f(t_{1},...,t_{n})\), con \(f\in\mathcal{F}\), \(a(f)=n\) y \(t_{1},...,t_{n}\in T_{k}^{\tau}\). Ya que \(t\in T^{\tau^{\prime}}\) y en \(t\) ocurren paréntesis se tiene que \(t\) es de la forma \(g(s_{1},...,s_{m})\), con \(g\in\mathcal{F}^{\prime}\), \(a^{\prime}(g)=m\) y \(s_{1},...,s_{m}\in T^{\tau^{\prime}}\). Tenemos entonces que \[f(t_{1},...,t_{n})=g(s_{1},...,s_{m})\] lo cual claramente nos dice que \(f=g\) ya que ambas palabras no tienen paréntesis. O sea que

1. adhocprefix(1)adhocsufix \(t_{1},...,t_{n}=s_{1},...,s_{m}\)

Probaremos que

1. adhocprefix(2)adhocsufix \(n=m\) y \(t_{i}=s_{i}\), para \(i=1,...,n\)

Nótese que (1) nos dice que \(t_{1}\) es tramo inicial de \(s_{1}\) o viceversa. Supongamos \(t_{1}\) es tramo inicial propio de \(s_{1}\). O sea que debe ser \(n>1\) y la palabra \(t_{1},\) debe ser tramo inicial de \(s_{1}\). Ya que \(,\) ocurre en \(s_{1}\) tenemos que \(s_{1}\) es de la forma \(h(u_{1},...,u_{l})\), con \(h\in\mathcal{F}^{\prime}\), \(a^{\prime}(h)=l\) y \(u_{1},...,u_{l}\in T^{\tau^{\prime}}\). Esto nos dice que \(t_{1}\) no es una variable ya que \(s_{1}\) no comienza con \(\mathsf{X}\). Si \(t_{1}\in\mathcal{C}\), entonces ya que \(t_{1},\) es inicial de \(s_{1}\) llegamos a un absurdo. O sea que en \(t_{1}\) ocurren paréntesis. Pero entonces (4) del Lema \(SPar\) en Términos (aplicado al término \(s_{1}\)) nos dice que \(SPar(t_{1},)>0\), lo cual es absurdo porque (1) del mismo lema (aplicado al término \(t_{1}\)) nos dice que \(SPar(t_{1},)=0\). El absurdo provino de suponer que \(t_{1}\) es tramo inicial propio de \(s_{1}\). De la misma forma si suponemos que \(s_{1}\) es tramo inicial propio de \(t_{1}\) llegamos a un absurdo. Esto prueba que \(t_{1}=s_{1}\). Sea \(i_{0}\) el mayor \(i\in\{1,...,min\{n,m\}\}\) tal que \(t_{j}=s_{j}\), para \(j\in\{1,...,i\}\). Si \(i_{0}=n\), entonces \(m\) no puede ser mayor que \(n\) ya que en tal caso tendríamos simplificando en (1) que \[\varepsilon=s_{n+1},...,s_{m}\] Similarmente si \(i_{0}=m\), entonces \(n\) no puede ser mayor que \(m\). O sea que \(i_{0}=n=m\) o \(i_{0}<n,m\). Si \(i_{0}=n=m\) entonces claramente hemos probado (2). Pero veamos que \(i_{0}<n,m\) conduce a un absurdo. Supongamos \(i_{0}<n,m\). Entonces simplificando tenemos que \[t_{i_{0}+1},...,t_{n}=s_{i_{0}+1},...,s_{m}\] y además \(t_{i_{0}+1}\neq s_{i_{0}+1}\). Pero haciendo el mismo argumento hecho para ver que \(t_{1}=s_{1}\)podríamos probar que \(t_{i_{0}+1}=s_{i_{0}+1}\) y llegar a un absurdo. O sea que siempre \(i_{0}=n=m\) lo cual completa la prueba de (2).

Ya que \(t_{i}=s_{i}\), para \(i=1,...,n\) tenemos que \(t_{i}\in T_{k}^{\tau}\cap T^{\tau^{\prime}}\) para \(i=1,...,n\). O sea que como vale \(\mathrm{Enu}_{k}\) tenemos que \(t_{i}\in T^{\tau_{\cap}}\) para \(i=1,...,n\). Pero \(f=g\) y \(n=m\) nos dice que \(f\in\mathcal{F}_{\cap}\), lo cual implica que \(t=f(t_{1},...,t_{n})\in T^{\tau_{\cap}}\).

(c) Es directo (y dejado al lector) probar por inducción que \(F_{k}^{\tau_{\cap}}\subseteq F^{\tau}\cap F^{\tau^{\prime}}\), para cada \(k\in\omega\). Esto prueba que \(F^{\tau_{\cap}}\subseteq F^{\tau}\cap F^{\tau^{\prime}}\). Veamos la otra inclusión. Lo probaremos usando la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Si \(\varphi\in F_{k}^{\tau}\cap F^{\tau^{\prime}}\), entonces \(\varphi\in F^{\tau_{\cap}}\).

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Supongamos \(\varphi\in F_{0}^{\tau}\cap F^{\tau^{\prime}}\). Ya que \(\varphi\in F_{0}^{\tau}\) hay dos casos.

Caso \(\varphi=(t\equiv s)\), con \(t,s\in T^{\tau}\). Ya que \(\varphi\in F^{\tau^{\prime}}\) y en \(\varphi\) no ocurre ningún símbolo del conjunto \(\{\vee,\wedge,\leftrightarrow,\rightarrow,\neg,\exists,\forall\}\cup\mathcal{R}^{\prime}\), el Teorema de Lectura Única de Fórmulas nos dice que \(\varphi=(u\equiv v)\), con \(u,v\in T^{\tau^{\prime}}\). Obviamente esto nos dice que \(t=u\) y \(s=v\), por lo cual \(t,s\in T^{\tau}\cap T^{\tau^{\prime}}\). Por (b) obtenemos entonces que \(t,s\in T^{\tau_{\cap}}\). Pero esto claramente nos asegura que \(\varphi\in F^{\tau_{\cap}}\).

Caso \(\varphi=r(t_{1},...,t_{n})\), con \(r\in\mathcal{R}\), \(a(r)=n\) y \(t_{1},...,t_{n}\in T^{\tau}\). Ya que \(\varphi\in F^{\tau^{\prime}}\) y en \(\varphi\) no ocurre ningún símbolo del conjunto \(\{\equiv,\vee,\wedge,\leftrightarrow,\rightarrow,\neg,\exists,\forall\}\), el Teorema de Lectura Única de Fórmulas nos dice que \(\varphi=h(s_{1},...,s_{m})\), con \(h\in\mathcal{R}\), \(a(h)=m\) y \(s_{1},...,s_{m}\in T^{\tau^{\prime}}\). Pero entonces ya que \[r(t_{1},...,t_{n})=h(s_{1},...,s_{m})\] deberá suceder que \(r=h\) y \(t_{1},...,t_{n}=s_{1},...,s_{m}\). Usando el mismo argumento que se uso para probar (2) en la prueba de (b) obtenemos que \(n=m\) y \(t_{i}=s_{i}\), para \(i=1,...,n\). Ya que \(t_{i}\in T^{\tau}\cap T^{\tau^{\prime}}\), para \(i=1,...,n\), (b) nos dice que \(t_{i}\in T^{\tau_{\cap}}\), para \(i=1,...,n\). Pero \(f=g\) y \(n=m\) nos dice que \(r\in\mathcal{R}_{\cap}\), lo cual implica que \(\varphi=r(t_{1},...,t_{n})\in F^{\tau_{\cap}}\).

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Supongamos \(\varphi\in F_{k+1}^{\tau}\cap F^{\tau^{\prime}}\). Veremos que \(\varphi\in F^{\tau_{\cap}}\). Por la definición de \(F_{k+1}^{\tau}\) hay varios casos.

Caso \(\varphi\in F_{k}^{\tau}\). Trivial ya que vale \(\mathrm{Enu}_{k}\).

Caso \(\varphi=\left(\varphi_{1}\eta\varphi_{2}\right)\), con \(\eta\in\{\vee,\wedge,\leftrightarrow,\rightarrow\}\) y \(\varphi_{1},\varphi_{2}\in F_{k}^{\tau}\). Ya que \(\varphi\in F^{\tau^{\prime}}\)el Teorema de Lectura Única de Fórmulas nos dice que \(\varphi=\left(\psi_{1}\mu\psi_{2}\right)\), con \(\mu\in\{\vee,\wedge,\leftrightarrow,\rightarrow\}\) y \(\psi_{1},\psi_{2}\in F^{\tau^{\prime}}\) (\(\varphi\) no puede ser de la forma \((t\equiv s)\) ya que en \((t\equiv s)\) no ocurre ningún símbolo de \(\{\vee,\wedge,\leftrightarrow,\rightarrow\}\)). Ya que \(\left(\varphi_{1}\eta\varphi_{2}\right)=\left(\psi_{1}\mu\psi_{2}\right)\) tenemos que \(\varphi_{1}\eta\varphi_{2}=\psi_{1}\mu\psi_{2}\) por lo cual \(\varphi_{1}\) es tramo inicial de \(\psi_{1}\) o viceversa. Supongamos \(\varphi_{1}\) es tramo inicial propio de \(\psi_{1}\). Ya que en \(\varphi_{1}\) ocurren paréntesis el Lema \(SPar\) en Fórmulas (aplicado a \(\psi_{1}\)) nos dice que \(SPar(\varphi_{1})>0\). Pero (1) del mismo lema (aplicado ahora a \(\varphi_{1}\)) nos dice que \(SPar(\varphi_{1})=0\), lo cual es absurdo. De la misma manera podemos llegar a un absurdo suponiendo que \(\psi_{1}\) es tramo inicial propio de \(\varphi_{1}\), lo cual nos dice que \(\varphi_{1}=\psi_{1}\). O sea que \(\eta=\mu\) y \(\varphi_{2}=\psi_{2}\). Esto nos garantiza que \(\varphi_{1},\varphi_{2}\in F_{k}^{\tau}\cap F^{\tau^{\prime}}\), lo cual ya que \(\mathrm{Enu}_{k}\) es verdadero nos dice que \(\varphi_{1},\varphi_{2}\in F^{\tau_{\cap}}\). Claramente entonces tenemos que \(\varphi\in F^{\tau_{\cap}}\).

Caso \(\varphi=Qv\varphi_{1}\), con \(Q\in\{\forall,\exists\}\), \(v\in Var\) y \(\varphi_{1}\in F_{k}^{\tau}\). Ya que \(\varphi\in F^{\tau^{\prime}}\)el Teorema de Lectura Única de Fórmulas nos dice que \(\varphi=Q^{\prime}v^{\prime}\varphi_{1}^{\prime}\), con \(Q^{\prime}\in\{\forall,\exists\}\), \(v^{\prime}\in Var\) y \(\varphi_{1}^{\prime}\in F^{\tau^{\prime}}\). Obviamente deberá suceder \(Q=Q^{\prime}\), \(v=v^{\prime}\) y \(\varphi_{1}=\varphi_{1}^{\prime}\). O sea que \(\varphi_{1}\in F_{k}^{\tau}\cap F^{\tau^{\prime}}\), lo cual ya que \(\mathrm{Enu}_{k}\) es verdadero nos dice que \(\varphi_{1}\in F^{\tau_{\cap}}\). Claramente entonces tenemos que \(\varphi\in F^{\tau_{\cap}}\).

Caso \(\varphi=\neg\varphi_{1}\), con \(\varphi_{1}\in F_{k}^{\tau}\). Es dejado al lector.  

Proof. (a) Lo probaremos usando la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Supongamos \(t=_{d}t(\vec{v})\in T_{k}^{\tau_{\cap}}\) y sean \(\mathbf{A}\) y \(\mathbf{A}^{\prime}\) modelos de tipo \(\tau\) y \(\tau^{\prime}\) respectivamente tales que \(A=A^{\prime}\), \(c^{\mathbf{A}}=c^{\mathbf{A}^{\prime}}\), para cada \(c\in\mathcal{C}_{\cap}\), \(f^{\mathbf{A}}=f^{\mathbf{A}^{\prime}}\), para cada \(f\in\mathcal{F}_{\cap}\) y \(r^{\mathbf{A}}=r^{\mathbf{A}^{\prime}}\), para cada \(r\in\mathcal{R}_{\cap}\). Entonces \(t^{\mathbf{A}}[\vec{a}]=t^{\mathbf{A}^{\prime}}[\vec{a}]\), para cada \(\vec{a}\in A^{n}\).

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Trivial.

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Supongamos \(t=_{d}t(\vec{v})\in T_{k+1}^{\tau_{\cap}}\) y sean \(\mathbf{A}\) y \(\mathbf{A}^{\prime}\) modelos de tipo \(\tau\) y \(\tau^{\prime}\) respectivamente tales que \(A=A^{\prime}\), \(c^{\mathbf{A}}=c^{\mathbf{A}^{\prime}}\), para cada \(c\in\mathcal{C}_{\cap}\), \(f^{\mathbf{A}}=f^{\mathbf{A}^{\prime}}\), para cada \(f\in\mathcal{F}_{\cap}\) y \(r^{\mathbf{A}}=r^{\mathbf{A}^{\prime}}\), para cada \(r\in\mathcal{R}_{\cap}\). Por el Lema de Lectura Única de Términos Declarados, hay varios casos:

Caso \(t=v_{i}\), con \(i\in\{1,...,n\}\). Sea \(\vec{a}\in A^{n}\). Tenemos que \[\begin{aligned} t^{\mathbf{A}}[\vec{a}] & =a_{i}\\ & =t^{\mathbf{A}^{\prime}}[\vec{a}] \end{aligned}\] Por lo cual \(t^{\mathbf{A}}[\vec{a}]=t^{\mathbf{A}^{\prime}}[\vec{a}]\), para cada \(\vec{a}\in A^{n}\).

Caso \(t\in\mathcal{C}_{\cap}\). Sea \(\vec{a}\in A^{n}\). Tenemos que \[\begin{aligned} t^{\mathbf{A}}[\vec{a}] & =t^{\mathbf{A}}\\ & =t^{\mathbf{A}^{\prime}}\\ & =t^{\mathbf{A}^{\prime}}[\vec{a}] \end{aligned}\] Por lo cual \(t^{\mathbf{A}}[\vec{a}]=t^{\mathbf{A}^{\prime}}[\vec{a}]\), para cada \(\vec{a}\in A^{n}\).

Caso \(t=f(t_{1},...,t_{m})\), con \(f\in\mathcal{F}_{\cap}\), \(a_{\cap}(f)=m\) y \(t_{1},...,t_{m}\in T_{k}^{\tau}\). Dado que hemos declarado \(t=_{d}t(v_{1},...,v_{n})\), por la Convención Notacional 3, tenemos declarados también \(t_{1}=_{d}t_{1}(v_{1},...,v_{n}),...,t_{m}=_{d}t_{m}(v_{1},...,v_{n})\). O sea que \(\mathrm{Enu}_{k}\) nos dice que \(t_{i}^{\mathbf{A}}[\vec{a}]=t_{i}^{\mathbf{A}^{\prime}}[\vec{a}]\), para cada \(\vec{a}\in A^{n}\) y \(i=1,...,m\). Sea \(\vec{a}\in A^{n}\). Tenemos que \[\begin{aligned} t^{\mathbf{A}}[\vec{a}] & =f^{\mathbf{A}}(t_{1}^{\mathbf{A}}[\vec{a}],...,t_{m}^{\mathbf{A}}[\vec{a}])\\ & =f^{\mathbf{A}}(t_{1}^{\mathbf{A}^{\prime}}[\vec{a}],...,t_{m}^{\mathbf{A}^{\prime}}[\vec{a}])\\ & =f^{\mathbf{A}^{\prime}}(t_{1}^{\mathbf{A}^{\prime}}[\vec{a}],...,t_{m}^{\mathbf{A}^{\prime}}[\vec{a}])\\ & =t^{\mathbf{A}^{\prime}}[\vec{a}] \end{aligned}\] Por lo cual \(t^{\mathbf{A}}[\vec{a}]=t^{\mathbf{A}^{\prime}}[\vec{a}]\), para cada \(\vec{a}\in A^{n}\).

(b) Es dejado al lector.

(c) Supongamos que \((\Sigma,\tau)\models\varphi\). Probaremos que \((\Sigma,\tau^{\prime})\models\varphi\). Sea \(\mathbf{A}^{\prime}\) un modelo de \(\tau^{\prime}\) tal que \(\mathbf{A}^{\prime}\models\Sigma\). Sea \(a\in A^{\prime}\) un elemento fijo. Sea \(\mathbf{A}\) el modelo de tipo \(\tau\) definido de la siguiente manera

1. adhocprefix-adhocsufix universo de \(\mathbf{A}=\) \(A^{\prime}\)

2. adhocprefix-adhocsufix \(c^{\mathbf{A}}=c^{\mathbf{A}^{\prime}}\), para cada \(c\in\mathcal{C}_{\cap}\),

3. adhocprefix-adhocsufix \(f^{\mathbf{A}}=f^{\mathbf{A}^{\prime}}\), para cada \(f\in\mathcal{F}_{\cap}\)

4. adhocprefix-adhocsufix \(r^{\mathbf{A}}=r^{\mathbf{A}^{\prime}}\), para cada \(r\in\mathcal{R}_{\cap}\)

5. adhocprefix-adhocsufix \(c^{\mathbf{A}}=a\), para cada \(c\in\mathcal{C}-\mathcal{C}_{\cap}\)

6. adhocprefix-adhocsufix \(f^{\mathbf{A}}(a_{1},...,a_{a(f)})=a\), para cada \(f\in\mathcal{F}-\mathcal{F}_{\cap}\), \(a_{1},...,a_{a(f)}\in A^{\prime}\)

7. adhocprefix-adhocsufix \(r^{\mathbf{A}}=\emptyset\), para cada \(r\in\mathcal{R-R}_{\cap}\)

Ya que \(\mathbf{A}^{\prime}\models\Sigma\), (b) nos dice que \(\mathbf{A}\models\Sigma\), lo cual nos dice que \(\mathbf{A}\models\varphi\). Nuevamente por (b) tenemos que \(\mathbf{A}^{\prime}\models\varphi\), con lo cual hemos probado que \((\Sigma,\tau^{\prime})\models\varphi\).

Dejamos al lector la prueba de la reciproca.  

Proof. (1) Supongamos \((\Sigma,\tau)\vdash\varphi\). Entonces hay una prueba formal \((\varphi_{1}...\varphi_{n},J_{1}...J_{n})\) de \(\varphi\) en \((\Sigma,\tau)\). Nótese que aplicando varias veces el Lema 7.42 podemos obtener una prueba formal \((\tilde{\varphi}_{1}...\tilde{\varphi}_{n},J_{1}...J_{n})\) de \(\varphi\) en \((\Sigma,\tau)\) la cual cumple que si \(\mathcal{C}_{2}\) es el conjunto de nombres de constante que ocurren en \(\tilde{\varphi}_{1}...\tilde{\varphi}_{n}\) y que no pertenecen a \(\mathcal{C}\), entonces:

1. adhocprefix-adhocsufix \(\mathcal{C}_{2}\cap\mathcal{C}^{\prime}=\emptyset\)

2. adhocprefix-adhocsufix \((\mathcal{C}^{\prime}\cup\mathcal{C}_{2},\mathcal{F}^{\prime},\mathcal{R}^{\prime},a^{\prime})\) es un tipo

Pero entonces \((\tilde{\varphi}_{1}...\tilde{\varphi}_{n},J_{1}...J_{n})\) es una prueba formal de \(\varphi\) en \((\Sigma,\tau^{\prime})\), con lo cual \((\Sigma,\tau^{\prime})\vdash\varphi\)

(2) Supongamos \((\Sigma,\tau^{\prime})\vdash\varphi\). Entonces hay una prueba formal \((\boldsymbol{\varphi},\mathbf{J})\) de \(\varphi\) en \((\Sigma,\tau^{\prime})\). Veremos que \((\boldsymbol{\varphi},\mathbf{J})\) es una prueba formal de \(\varphi\) en \((\Sigma,\tau)\). Ya que \((\boldsymbol{\varphi},\mathbf{J})\) es una prueba formal de \(\varphi\) en \((\Sigma,\tau^{\prime})\) hay un conjunto finito \(\mathcal{C}_{1}\), disjunto con \(\mathcal{C}^{\prime}\), tal que \((\mathcal{C}^{\prime}\cup\mathcal{C}_{1},\mathcal{F},\mathcal{R},a)\) es un tipo y cada \(\boldsymbol{\varphi}_{i}\) es una sentencia de tipo \((\mathcal{C}^{\prime}\cup\mathcal{C}_{1},\mathcal{F},\mathcal{R},a)\). Sea \(\widetilde{\mathcal{C}_{1}}=\mathcal{C}_{1}\cup(\mathcal{C}^{\prime}-\mathcal{C})\). Nótese que \(\mathcal{C}\cup\widetilde{\mathcal{C}_{1}}=\mathcal{C}^{\prime}\cup\mathcal{C}_{1}\) por lo cual \((\mathcal{C}\cup\widetilde{\mathcal{C}_{1}},\mathcal{F},\mathcal{R},a)\) es un tipo y cada \(\boldsymbol{\varphi}_{i}\) es una sentencia de tipo \((\mathcal{C}\cup\widetilde{\mathcal{C}_{1}},\mathcal{F},\mathcal{R},a)\). Esto nos dice que \((\boldsymbol{\varphi},\mathbf{J})\) cumple (1) de la definición de prueba formal en \((\Sigma,\tau)\). Todos los otros puntos se cumplen en forma directa, excepto los puntos (4)(t) y (4)(u)(i) para los cuales es necesario notar que \(\mathcal{C}\subseteq\mathcal{C}^{\prime}\).  

Proof. Haremos primero el caso en que \(v\) no ocurre libremente en \(\varphi\), es decir cuando \(\varphi\) es una sentencia. En este caso tenemos que \(\{[\varphi(t)]_{T}:t\in T_{c}^{\tau}\}=\{[\varphi]_{T}\}\), por lo cual \(\inf(\{[\varphi(t)]_{T}:t\in T_{c}^{\tau}\})=[\varphi]_{T}\). Es decir que debemos probar que \([\forall v\varphi(v)]_{T}=[\varphi]_{T}\). Pero el Axioma Esquema de Cuantificación Vacua nos dice que \((\forall v\varphi\leftrightarrow\varphi)\) es un axioma lógico por lo cual \(T\vdash(\forall v\varphi\leftrightarrow\varphi))\), obteniendo que \([\forall v\varphi(v)]_{T}=[\varphi]_{T}\).

Hagamos ahora el caso en el que \(Li(\varphi)=\{v\}\). Primero veamos que \([\forall v\varphi(v)]_{T}\) es cota inferior del conjunto \(\{[\varphi(t)]_{T}:t\in T_{c}^{\tau}\}\). Por el Lema 7.47 debemos probar que para todo término cerrado \(t\), se da que \(T\vdash(\forall v\varphi(v)\rightarrow\varphi(t))\). Pero esto es fácil ya que \[\begin{array}{cllll} 1. & \forall v\varphi(v) & & & \text{HIPOTESIS}1\\ 2. & \varphi(t) & & & \text{TESIS}1\text{PARTICULARIZACION}(1)\\ 3. & (\forall v\varphi(v)\rightarrow\varphi(t)) & & & \text{CONCLUSION} \end{array}\] es una prueba formal de \((\forall v\varphi(v)\rightarrow\varphi(t))\) en \(T\). Supongamos ahora que \([\psi]_{T}\leq^{T}[\varphi(t)]_{T}\), para todo término cerrado \(t.\) Probaremos que \([\psi]_{T}\leq^{T}[\forall v\varphi(v)]_{T}\). Por hipótesis hay un nombre de cte \(c\in\mathcal{C}\) el cual no ocurre en los elementos de \(\Sigma\cup\{\psi,\varphi(v)\}\). Ya que \([\psi]_{T}\leq^{T}[\varphi(c)]_{T}\), hay una prueba formal \((\boldsymbol{\varphi},\mathbf{J})=(\boldsymbol{\varphi}_{1}...\boldsymbol{\varphi}_{n},\mathbf{J}_{1}...\mathbf{J}_{n})\) de \(\left(\psi\rightarrow\varphi(c)\right)\) en \(T\). Sean \(c_{1},...,c_{k}\) los nombres de constante auxiliares de \((\boldsymbol{\varphi},\mathbf{J})\) (es decir, \((\mathcal{C}\cup\{c_{1},...,c_{k}\},\mathcal{F},\mathcal{R},a))\) es el tipo ambiente de \((\boldsymbol{\varphi},\mathbf{J})\)). Sea \(m\in\mathbf{N}\) tal que \(J_{i}\neq\text{HIPOTESIS}\bar{m}\) para cada \(i=1,...,n\). Nótese que \((\mathcal{C}-\{c\},\mathcal{F},\mathcal{R},a))\) es un tipo y los elementos de \(\Sigma\) son sentencias de este tipo ya que \(c\) no ocurre en las sentencias de \(\Sigma\). O sea que \(T_{r}=(\Sigma,\mathcal{C}-\{c\},\mathcal{F},\mathcal{R},a))\) es una teoría. Veamos que la siguiente es una prueba formal en \(T_{r}\) de \(\left(\psi\rightarrow\forall v\varphi(v)\right)\): \[\begin{array}{rlcl} 1. & \boldsymbol{\varphi}_{1} & & \mathbf{J}_{1}\\ 2. & \boldsymbol{\varphi}_{2} & & \mathbf{J}_{2}\\ \vdots & \vdots & & \vdots\\ n. & \boldsymbol{\varphi}_{n}=\left(\psi\rightarrow\varphi(c)\right) & & \mathbf{J}_{n}\\ n+1. & \psi & & \text{HIPOTESIS}\bar{m}\\ n+2. & \varphi(c) & & \text{MODUSPONENS}(\overline{n+1},\bar{n})\\ n+3. & \forall v\varphi(v) & & \text{TESIS}\bar{m}\text{GENERALIZACION}(\overline{n+2})\\ n+4. & \left(\psi\rightarrow\forall v\varphi(v)\right) & & \text{CONCLUSION} \end{array}\] Nótese que nuestra candidata a prueba formal, como objeto matemático es el par \((\boldsymbol{\gamma},\mathbf{K})\) donde \(\boldsymbol{\gamma}\) es la palabra \[\boldsymbol{\varphi}\psi\varphi(c)\forall v\varphi(v)\left(\psi\rightarrow\forall v\varphi(v)\right)\] y \(\mathbf{K}\) es la palabra \[\mathbf{J}\text{HIPOTESIS}\bar{m}\text{MODUSPONENS}(\overline{n+1},\bar{n})\text{TESIS}\bar{m}\text{GENERALIZACION}(\overline{n+2})\text{CONCLUSION}\] Nótese que

1. adhocprefix(I)adhocsufix \(n(\boldsymbol{\gamma})=n+4=n(\mathbf{K})\)

2. adhocprefix(II)adhocsufix \(\boldsymbol{\gamma}_{i}=\boldsymbol{\varphi}_{i}\), para \(i\in\{1,...,n\}\), \(\boldsymbol{\gamma}_{n+1}=\psi\), \(\boldsymbol{\gamma}_{n+2}=\varphi(c)\), \(\boldsymbol{\gamma}_{n+3}=\forall v\varphi(v)\) y \(\boldsymbol{\gamma}_{n+4}=(\psi\rightarrow\forall v\varphi(v))\)

3. adhocprefix(III)adhocsufix \(\boldsymbol{\mathbf{K}}_{i}=\mathbf{J}_{i}\), para \(i\in\{1,...,n\}\), \(\mathbf{J}_{n+1}=\text{HIPOTESIS}\bar{m}\), \(\mathbf{J}_{n+2}=\text{MODUSPONENS}(\overline{n+1},\bar{n})\), \(\mathbf{J}_{n+3}=\text{TESIS}\bar{m}\text{GENERALIZACION}(\overline{n+2})\) y \(\mathbf{J}_{n+4}=\text{CONCLUSION}\)

4. adhocprefix(IV)adhocsufix \(\mathbf{K}\) es balanceada ya que \(\mathbf{J}\) lo es y \(\mathcal{B}^{\mathbf{K}}=\mathcal{B}^{\mathbf{J}}\cup\{\left\langle n+1,n+3\right\rangle \}\)

Nótese que el tipo \(\tau_{1}\) de la definición de prueba para \((\boldsymbol{\gamma},\mathbf{K})\) puede ser \[\tau_{1}=((\mathcal{C}-\{c\})\cup\{c,c_{1},...,c_{k}\},\mathcal{F},\mathcal{R},a)=(\mathcal{C}\cup\{c_{1},...,c_{k}\},\mathcal{F},\mathcal{R},a))\] (i.e. el tipo ambiente de \((\boldsymbol{\gamma},\mathbf{K})\)). O sea justamente es el tipo ambiente de \((\boldsymbol{\varphi},\mathbf{J})\) pero en \((\boldsymbol{\varphi},\mathbf{J})\) el nombre de cte \(c\) no es auxiliar ya que esta en el tipo de la teoría \(T\) y en cambio \(c\) es un nombre de constante auxiliar de \((\boldsymbol{\gamma},\mathbf{K})\) ya que no pertenece al tipo de la teoría \(T_{r}\). O sea los nombres de constante auxiliares de \((\boldsymbol{\gamma},\mathbf{K})\) son \(c,c_{1},...,c_{k}\). O sea que I y IV nos dicen que \((\boldsymbol{\gamma},\mathbf{K})\) es un par adecuado de tipo \(\tau_{1}\).

Solo nos falta ver que se cumplen (3) y (4) de la definición de prueba formal. Dejamos al lector verificar que se cumple (3). Para chequear que se cumple (4) primero notemos que:

1. adhocprefix(V)adhocsufix Para \(i,j\in\{1,...,n\}\) se tiene que \(i\) es anterior a \(j\) en \((\boldsymbol{\gamma},\mathbf{K})\) si y solo si \(i\) es anterior a \(j\) en \((\boldsymbol{\varphi},\mathbf{J})\) (esto es directo de IV)

2. adhocprefix(VI)adhocsufix Si \(i,j\in\{1,...,n\}\) entonces \(\boldsymbol{\gamma}_{i}\) es hipótesis de \(\boldsymbol{\gamma}_{j}\) en \((\boldsymbol{\gamma},\mathbf{K})\) si y solo si \(\boldsymbol{\varphi}_{i}\) es hipótesis de \(\boldsymbol{\varphi}_{i}\) en \((\boldsymbol{\varphi},\mathbf{J})\) (esto es directo de IV)

3. adhocprefix(VII)adhocsufix Dadas \(e,d\in\mathcal{C}\cup\{c_{1},...,c_{k}\}\) se tiene que \(e\) depende de \(d\) en \((\boldsymbol{\gamma},\mathbf{K})\) si y solo si \(e\) depende de \(d\) en \((\boldsymbol{\varphi},\mathbf{J})\)

Probemos VII. Sean \(e,d\in\mathcal{C}\cup\{c_{1},...,c_{k}\}\) tales que \(e\) depende directamente de \(d\) en \((\boldsymbol{\gamma},\mathbf{K})\). O sea que hay números \(1\leq l<j\leq n(\boldsymbol{\gamma})=n+4\) tales que

1. adhocprefix-adhocsufix \(l\) es anterior a \(j\) en \((\boldsymbol{\gamma},\mathbf{K})\)

2. adhocprefix-adhocsufix \(\mathbf{K}_{j}=\alpha\mathrm{ELECCION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \((\boldsymbol{\gamma}_{l},\boldsymbol{\gamma}_{j})\in Elec^{\tau_{1}}\) vía \(e\)

3. adhocprefix-adhocsufix \(d\) ocurre en \(\boldsymbol{\gamma}_{l}\).

Ya que \(\mathbf{K}_{j}=\alpha\mathrm{ELECCION}(\bar{l})\), III nos dice que \(j\leq n\) y por lo tanto \(l\leq n\). Usando V, III y II obtenemos que

1. adhocprefix-adhocsufix \(l\) es anterior a \(j\) en \((\boldsymbol{\varphi},\mathbf{J})\)

2. adhocprefix-adhocsufix \(\mathbf{J}_{j}=\alpha\mathrm{ELECCION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{j})\in Elec^{\tau_{1}}\) vía \(e\)

3. adhocprefix-adhocsufix \(d\) ocurre en \(\boldsymbol{\varphi}_{l}\).

lo cual nos dice que \(e\) depende directamente de \(d\) en \((\boldsymbol{\varphi},\mathbf{J})\). Similarmente podemos probar que si \(e\) depende directamente de \(d\) en \((\boldsymbol{\varphi},\mathbf{J})\), entonces \(e\) depende directamente de \(d\) en \((\boldsymbol{\gamma},\mathbf{K})\). Por supuesto esto ya alcanza para probar VII.

Ahora sí, veamos que se cumple (4) de la definición de prueba formal. Para cada \(i=1,...,n+4\) debemos probar que se cumple alguna de las propiedades (a), (b), (c), ..., (u) de (4) de la definición de prueba. Primero supongamos \(i\in\{1,...,n\}\). Ya que \((\boldsymbol{\varphi},\mathbf{J})\) cumple (4) tenemos que se cumple alguna de las propiedades (a), (b), (c), ...., (u), con respecto a la prueba \((\boldsymbol{\varphi},\mathbf{J})\). Por ejemplo supongamos se cumple (f) con respecto a la prueba \((\boldsymbol{\varphi},\mathbf{J})\). Entonces tenemos que \(\mathbf{J}_{i}=\alpha\mathrm{COMMUTATIVIDAD}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Commut^{\tau_{1}}\). Pero ya que \(\mathbf{K}_{i}=\mathbf{J}_{i}\), \(\boldsymbol{\varphi}_{l}=\boldsymbol{\gamma}_{l}\text{ y }\boldsymbol{\varphi}_{i}=\boldsymbol{\gamma}_{i}\), V nos dice que

1. adhocprefix-adhocsufix \(\mathbf{K}_{i}=\alpha\mathrm{COMMUTATIVIDAD}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\gamma},\mathbf{K})\) y \((\boldsymbol{\gamma}_{l},\boldsymbol{\gamma}_{i})\in Commut^{\tau_{1}}\)(recordar que \(\tau_{1}\) es el tipo ambiente de \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\gamma},\mathbf{K})\))

lo cual nos dice que se cumple (f) con respecto a \((\boldsymbol{\gamma},\mathbf{K})\). Supongamos ahora se cumple (t) respecto de la prueba \((\boldsymbol{\varphi},\mathbf{J})\). Es decir \(\mathbf{J}_{i}=\alpha\mathrm{ELECCION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Elec^{\tau_{1}}\) vía un nombre de cte \(e\), el cual no pertenece a \(\mathcal{C}\) y no ocurre en \(\boldsymbol{\varphi}_{1},...,\boldsymbol{\varphi}_{i-1}\). Ya que \(\mathbf{K}_{i}=\mathbf{J}_{i}\) y \(\boldsymbol{\gamma}_{j}=\boldsymbol{\varphi}_{j}\), para \(j\in\{1,...,n\}\), V nos dice que

1. adhocprefix-adhocsufix \(\mathbf{K}_{i}=\alpha\mathrm{ELECCION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\gamma},\mathbf{K})\) y \((\boldsymbol{\gamma}_{l},\boldsymbol{\gamma}_{i})\in Elec^{\tau_{1}}\) vía un nombre de cte \(e\), el cual no pertenece a \(\mathcal{C}-\{c\}\) y no ocurre en \(\boldsymbol{\gamma}_{1},...,\boldsymbol{\gamma}_{i-1}\).

O sea que se cumple (t) con respecto a \((\boldsymbol{\gamma},\mathbf{K})\). La prueba de los otros casos es similar, salvo el caso (u). Supongamos entonces que se cumple (u) respecto de la prueba \((\boldsymbol{\varphi},\mathbf{J})\) y veamos que entonces también se cumple (u) respecto de \((\boldsymbol{\gamma},\mathbf{K})\). O sea que sabemos que \(\mathbf{J}_{i}=\alpha\mathrm{GENERALIZACION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Generaliz^{\tau_{1}}\) vía un nombre de cte \(d\) el cual cumple:

1. adhocprefix(i)adhocsufix \(d\not\in\mathcal{C}\)

2. adhocprefix(ii)adhocsufix Para cada \(u\in\{1,...,n\}\), si \(\mathbf{J}_{u}=\alpha\mathrm{ELECCION}(\bar{v})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \(v\) anterior a \(u\) en \((\boldsymbol{\varphi},\mathbf{J})\), entonces no se da que \((\boldsymbol{\varphi}_{v},\boldsymbol{\varphi}_{u})\in Elec^{\tau_{1}}\) vía \(d\).

3. adhocprefix(iii)adhocsufix Para cada \(u\in\{1,...,n\}\), si \(\boldsymbol{\varphi}_{u}\) es hipótesis de \(\boldsymbol{\varphi}_{l}\) en \((\boldsymbol{\varphi},\mathbf{J})\), entonces \(d\) no ocurre en \(\boldsymbol{\varphi}_{u}\)

4. adhocprefix(iv)adhocsufix Ningún nombre de constante que ocurra en \(\boldsymbol{\varphi}_{l}\) depende de \(d\) en \((\boldsymbol{\varphi},\mathbf{J})\)

5. adhocprefix(v)adhocsufix Para cada \(u\in\{1,...,n\}\), si \(\boldsymbol{\varphi}_{u}\) es hipótesis de \(\boldsymbol{\varphi}_{l}\) en \((\boldsymbol{\varphi},\mathbf{J})\), entonces ningún nombre de constante que ocurra en \(\boldsymbol{\varphi}_{u}\) depende de \(d\) en \((\boldsymbol{\varphi},\mathbf{J})\)

Usando entonces las propiedades ya probadas es fácil ver que \(\mathbf{K}_{i}=\alpha\mathrm{GENERALIZACION}(\bar{l})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), \(l\) anterior a \(i\) en \((\boldsymbol{\gamma},\mathbf{K})\) y \((\boldsymbol{\gamma}_{l},\boldsymbol{\gamma}_{i})\in Generaliz^{\tau_{1}}\) vía un nombre de cte \(d\) el cual cumple:

1. adhocprefix(i)’adhocsufix \(d\not\in\mathcal{C}-\{c\}\)

2. adhocprefix(ii)’adhocsufix Para cada \(u\in\{1,...,n\}\), si \(\mathbf{K}_{u}=\alpha\mathrm{ELECCION}(\bar{v})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \(v\) anterior a \(u\) en \((\boldsymbol{\gamma},\mathbf{K})\), entonces no se da que \((\boldsymbol{\gamma}_{v},\boldsymbol{\gamma}_{u})\in Elec^{\tau_{1}}\) vía \(d\).

3. adhocprefix(iii)’adhocsufix Para cada \(u\in\{1,...,n\}\), si \(\boldsymbol{\gamma}_{u}\) es hipótesis de \(\boldsymbol{\gamma}_{l}\) en \((\boldsymbol{\gamma},\mathbf{K})\), entonces \(d\) no ocurre en \(\boldsymbol{\gamma}_{u}\)

4. adhocprefix(iv)’adhocsufix Ningún nombre de constante que ocurra en \(\boldsymbol{\gamma}_{l}\) depende de \(d\) en \((\boldsymbol{\gamma},\mathbf{K})\)

5. adhocprefix(v)’adhocsufix Para cada \(u\in\{1,...,n\}\), si \(\boldsymbol{\gamma}_{u}\) es hipótesis de \(\boldsymbol{\gamma}_{l}\) en \((\boldsymbol{\gamma},\mathbf{K})\), entonces ningún nombre de constante que ocurra en \(\boldsymbol{\gamma}_{u}\) depende de \(d\) en \((\boldsymbol{\gamma},\mathbf{K})\)

Nótese que hemos “casi” probado que se cumple (u) respecto de \((\boldsymbol{\gamma},\mathbf{K})\) ya que deberíamos tener \(n+4\) en lugar de \(n\) en las propiedades (ii)’, (iii)’ y (v)’. Pero nótese que podemos poner \(n+4\) en lugar de \(n\) en dichas propiedades y se seguirán cumpliendo. Por ejemplo si \(\mathbf{K}_{u}=\alpha\mathrm{ELECCION}(\bar{v})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\), entonces \(u\leq n\) (por como son \(\mathbf{K}_{n+1},...,\mathbf{K}_{n+4}\)) y por lo tanto en (ii)’ es irrelevante reemplazar \(n\) por \(n+4\). Además si \(\boldsymbol{\gamma}_{u}\) es hipótesis de \(\boldsymbol{\gamma}_{l}\) en \((\boldsymbol{\gamma},\mathbf{K})\), entonces \(u\leq l<i\leq n\) por lo cual en (iii)’ y (v)’ es irrelevante reemplazar \(n\) por \(n+4\). Ahora sí hemos probado que se cumple (u) respecto de \((\boldsymbol{\gamma},\mathbf{K})\).

Nos falta ver que para \(i\in\{n+1,n+2,n+3,n+4\}\) se cumple alguna de las propiedades (a), (b), (c), ..., (u) de (4) de la definición de prueba, respecto de \((\boldsymbol{\gamma},\mathbf{K})\). Cuando \(i\in\{n+1,n+2,n+4\}\) es fácil y dejado al lector. Veamos el caso \(i=n+3\). Veremos que se da (u). Es claro que \(\mathbf{K}_{i}=\text{TESIS}\bar{m}\text{GENERALIZACION}(\overline{n+2})\), que \(n+2\) es anterior a \(i\) en \((\boldsymbol{\gamma},\mathbf{K})\) y que \((\boldsymbol{\gamma}_{n+2},\boldsymbol{\gamma}_{i})\in Generaliz^{\tau_{1}}\) vía el nombre de cte \(c\). Nos faltaría ver entonces que:

1. adhocprefix(i)”adhocsufix \(c\not\in\mathcal{C}-\{c\}\)

2. adhocprefix(ii)”adhocsufix Para cada \(u\in\{1,...,n+4\}\), si \(\mathbf{K}_{u}=\alpha\mathrm{ELECCION}(\bar{v})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \(v\) anterior a \(u\) en \((\boldsymbol{\gamma},\mathbf{K})\), entonces no se da que \((\boldsymbol{\gamma}_{v},\boldsymbol{\gamma}_{u})\in Elec^{\tau_{1}}\) vía \(c\).

3. adhocprefix(iii)”adhocsufix Para cada \(u\in\{1,...,n+4\}\), si \(\boldsymbol{\gamma}_{u}\) es hipótesis de \(\boldsymbol{\gamma}_{n+2}\) en \((\boldsymbol{\gamma},\mathbf{K})\), entonces \(c\) no ocurre en \(\boldsymbol{\gamma}_{u}\)

4. adhocprefix(iv)”adhocsufix Ningún nombre de constante que ocurra en \(\boldsymbol{\gamma}_{n+2}\) depende de \(c\) en \((\boldsymbol{\gamma},\mathbf{K})\)

5. adhocprefix(v)”adhocsufix Para cada \(u\in\{1,...,n+4\}\), si \(\boldsymbol{\gamma}_{u}\) es hipótesis de \(\boldsymbol{\gamma}_{n+2}\) en \((\boldsymbol{\gamma},\mathbf{K})\), entonces ningún nombre de constante que ocurra en \(\boldsymbol{\gamma}_{u}\) depende de \(c\) en \((\boldsymbol{\gamma},\mathbf{K})\)

Obviamente se cumple (i)”. Veamos que se cumple (ii)”. Supongamos entonces \(\mathbf{K}_{u}=\alpha\mathrm{ELECCION}(\bar{v})\), con \(u\in\{1,...,n+4\}\), \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \(v\) anterior a \(u\) en \((\boldsymbol{\gamma},\mathbf{K})\). Note que \(u\leq n\) por lo cual también \(v\leq n\). O sea que por las propiedades ya probadas tenemos que \(\mathbf{J}_{u}=\alpha\mathrm{ELECCION}(\bar{v})\), con \(\alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}\) y \(v\) anterior a \(u\) en \((\boldsymbol{\varphi},\mathbf{J})\). Pero entonces ya que \((\boldsymbol{\varphi},\mathbf{J})\) es una prueba formal, debe darse que \((\boldsymbol{\varphi}_{v},\boldsymbol{\varphi}_{u})\in Elec^{\tau_{1}}\) vía un nombre de cte \(e\), el cual no pertenece a \(\mathcal{C}\) y no ocurre en \(\boldsymbol{\varphi}_{1},...,\boldsymbol{\varphi}_{u-1}\). Ya que \(c\) no es igual a \(e\), tenemos que no se da \((\boldsymbol{\varphi}_{v},\boldsymbol{\varphi}_{u})\in Elec^{\tau_{1}}\) vía \(c\), por lo cual no se da \((\boldsymbol{\gamma}_{v},\boldsymbol{\gamma}_{u})\in Elec^{\tau_{1}}\) vía \(c\). Para probar (iii)” note que si \(\boldsymbol{\gamma}_{u}\) es hipótesis de \(\boldsymbol{\gamma}_{n+2}\) en \((\boldsymbol{\gamma},\mathbf{K})\), entonces \(u=n+1\). O sea que \(\boldsymbol{\gamma}_{u}=\psi\) y claramente entonces \(c\) no ocurre en \(\boldsymbol{\gamma}_{u}\). Para probar (iv)” y (v)” nótese que los nombres de cte que ocurren en \(\boldsymbol{\gamma}_{n+2}\) o en hipótesis de \(\boldsymbol{\gamma}_{n+2}\) en \((\boldsymbol{\gamma},\mathbf{K})\) pertenecen todos a \(\mathcal{C}\), por lo cual no dependen de ningún otro nombre de cte en \((\boldsymbol{\gamma},\mathbf{K})\) ya que no dependen de ningún nombre de cte en \((\boldsymbol{\varphi},\mathbf{J})\).

O sea que ya probamos que \((\boldsymbol{\gamma},\mathbf{K})\) es una prueba por lo cual tenemos que \(T_{r}\vdash\left(\psi\rightarrow\forall v\varphi(v)\right)\). Por el Lema 7.50 tenemos entonces que \(T\vdash\left(\psi\rightarrow\forall v\varphi(v)\right)\), lo cual nos dice que \([\psi]_{T}\leq^{T}[\forall v\varphi(v)]_{T}\).  

Para entender la prueba del siguiente resultado es conveniente que el lector repase el final de la Sección Ordenes Naturales sobre \(\Sigma^{*}\) donde dado un orden total \(\leq\) para un alfabeto \(\Sigma\) se define un orden total sobre \(\Sigma^{*}\) el cual extiende a \(\leq\) (y es llamado el orden total de \(\Sigma^{*}\) inducido por \(\leq\)).

Proof. Sea \(\Sigma_{\tau}\) el alfabeto finito formado por todos los símbolos que ocurren en alguna palabra de \(\mathcal{C}\cup\mathcal{F}\cup\mathcal{R}\) junto con los símbolos \[\forall\ \ \exists\ \ \lnot\ \ \vee\ \ \wedge\ \ \rightarrow\ \ \leftrightarrow\ \ (\ \ )\ \ ,\ \ \equiv\ \ \mathsf{X}\ \ \mathit{0}\ \ \mathit{1}\ \ ...\ \ \mathit{9}\ \ \mathbf{0}\ \ \mathbf{1}\ \ ...\ \ \mathbf{9}\] Nótese que el conjunto \(F^{\tau}\) es \(\Sigma_{\tau}\)-mixto. Sea \(\leq\) un orden total sobre \(\Sigma_{\tau}\). Sea \(L=\{\alpha\in F^{\tau}:\left\vert Li(\alpha)\right\vert \leq1\}\). Definamos para \(t\in\mathbf{N}\), \[\gamma_{t}=t\mathrm{\text{-}esimo}\text{ }\mathrm{elemento\text{ }de}\text{ }L\text{ }\mathrm{con\text{ }respecto\text{ }al\text{ }orden\text{ }total\text{ }de\text{ }}\Sigma_{\tau}^{*}\text{ }\mathrm{inducido\text{ }por}\text{ }\leq\] Nótese que \[\begin{aligned} \gamma_{1} & =\text{menor }\alpha\in F^{\tau}\text{ tal que }\left\vert Li(\alpha)\right\vert \leq1\\ \gamma_{t+1} & =\text{menor }\alpha\in F^{\tau}\text{ tal que }\left\vert Li(\alpha)\right\vert \leq1\text{ y }\alpha\notin\{\gamma_{1},...,\gamma_{t}\} \end{aligned}\] Claramente entonces la infinitupla \((\gamma_{1},\gamma_{2},...)\) cumple (1) y (2).  

Observación: Cuando los conjuntos \(\mathcal{C},\mathcal{F}\text{ y }\mathcal{R}\) son \(\Sigma_{\tau}\)-efectivamente computables y la función \(a:\mathcal{F}\cup\mathcal{R}\rightarrow\mathbf{N}\) es \(\Sigma_{\tau}\)-efectivamente computable (esto sucede por ejemplo cuando los conjuntos \(\mathcal{C},\mathcal{F}\text{ y }\mathcal{R}\) son finitos), el conjunto \(F^{\tau}\) es \(\Sigma_{\tau}\)-efectivamente computable y por supuesto también lo es \(\{\alpha\in F^{\tau}:\left\vert Li(\alpha)\right\vert \leq1\}\). Dejamos al lector convencerse de esto y también de que en tal caso la función \(f:\mathbf{N}\rightarrow F^{\tau}\)dada por \(f(t)=\gamma_{t}\) es \(\Sigma_{\tau}\)-efectivamente computable. También se podría probar, usando las técnicas dadas en la Sección Análisis de Recursividad del Lenguaje de Primer Orden, que si \(\mathcal{C},\mathcal{F}\text{ y }\mathcal{R}\) son conjuntos \(\Sigma_{\tau}\)-p.r. y \(a\) es una función \(\Sigma_{\tau}\)-p.r., entonces \(f\) es \(\Sigma_{\tau}\)-p.r..

Ahora sí, el famoso resultado de Godel.

Proof. Primero probaremos completitud para el caso en que \(\tau\) tiene una cantidad infinita de nombres de cte que no ocurren en las sentencias de \(\Sigma\). Lo probaremos por el absurdo, es decir supongamos que hay una sentencia \(\varphi_{0}\) tal que \(T\models\varphi_{0}\) y \(T\not\vdash\varphi_{0}\). Nótese que ya que \(T\not\vdash\varphi_{0}\), tenemos que \([\varphi_{0}]_{T}\neq1^{T}=\{\varphi\in S^{\tau}:T\vdash\varphi\}\). O sea que \([\lnot\varphi_{0}]_{T}\not=0^{T}\). Por el lema anterior hay una infinitupla \((\gamma_{1},\gamma_{2},...)\in F^{\tau\mathbf{N}}\) tal que:

1. adhocprefix-adhocsufix \(\left\vert Li(\gamma_{j})\right\vert \leq1\), para cada \(j=1,2,...\)

2. adhocprefix-adhocsufix Si \(\left\vert Li(\gamma)\right\vert \leq1\), entonces \(\gamma=\gamma_{j}\), para algún \(j\in\mathbf{N}\)

Para cada \(j\in\mathbf{N}\), sea \(w_{j}\in Var\) tal que \(Li(\gamma_{j})\subseteq\{w_{j}\}\). Para cada \(j\), declaremos \(\gamma_{j}=_{d}\gamma_{j}(w_{j})\). Nótese que por el Lema 7.51 tenemos que \(\inf(\{[\gamma_{j}(t)]_{T}:t\in T_{c}^{\tau}\})=[\forall w_{j}\gamma_{j}(w_{j})]_{T}\), para cada \(j=1,2,...\). Por el Teorema de Rasiowa y Sikorski tenemos que hay un filtro primo \(\mathcal{U}\) de \(\mathcal{A}_{T}\), el cual cumple:

1. adhocprefix(a)adhocsufix \([\lnot\varphi_{0}]_{T}\in\mathcal{U}\)

2. adhocprefix(b)adhocsufix Para cada \(j\in\mathbf{N}\), \(\{[\gamma_{j}(t)]_{T}:t\in T_{c}^{\tau}\}\subseteq\mathcal{U}\) implica que \([\forall w_{j}\gamma_{j}(w_{j})]_{T}\in\mathcal{U}\)

Ya que la infinitupla \((\gamma_{1},\gamma_{2},...)\) cubre todas las fórmulas con a lo sumo una variable libre, podemos reescribir la propiedad (b) de la siguiente manera

1. adhocprefix(b)\(^{\prime}\)adhocsufix Para cada \(\varphi=_{d}\varphi(v)\in F^{\tau}\), si \(\{[\varphi(t)]_{T}:t\in T_{c}^{\tau}\}\subseteq\mathcal{U}\) entonces \([\forall v\varphi(v)]_{T}\in\mathcal{U}\)

Definamos sobre \(T_{c}^{\tau}\) la siguiente relación: \[t\bowtie s\text{ si y solo si }[(t\equiv s)]_{T}\in\mathcal{U}\text{.}\] Veamos entonces que:

1. adhocprefix(1)adhocsufix \(\bowtie\) es de equivalencia.

2. adhocprefix(2)adhocsufix Para cada \(\varphi=_{d}\varphi(v_{1},...,v_{n})\in F^{\tau}\), \(t_{1},...,t_{n},s_{1},...,s_{n}\in T_{c}^{\tau}\), si \(t_{1}\bowtie s_{1}\), \(t_{2}\bowtie s_{2}\), \(...\), \(t_{n}\bowtie s_{n}\), entonces \([\varphi(t_{1},...,t_{n})]_{T}\in\mathcal{U}\) si y solo si \([\varphi(s_{1},...,s_{n})]_{T}\in\mathcal{U}\).

3. adhocprefix(3)adhocsufix Para cada \(f\in\mathcal{F}_{n}\), \(t_{1},...,t_{n},s_{1},...,s_{n}\in T_{c}^{\tau}\), \[t_{1}\bowtie s_{1},t_{2}\bowtie s_{2},...,\;t_{n}\bowtie s_{n}\text{ implica }f(t_{1},...,t_{n})\bowtie f(s_{1},...,s_{n}).\]

Probaremos (2). Nótese que \[T\vdash\left((t_{1}\equiv s_{1})\wedge(t_{2}\equiv s_{2})\wedge...\wedge(t_{n}\equiv s_{n})\wedge\varphi(t_{1},...,t_{n})\right)\rightarrow\varphi(s_{1},...,s_{n})\] lo cual nos dice que \[[(t_{1}\equiv s_{1})]_{T}\;\mathsf{i}^{T}\mathsf{\;}[(t_{2}\equiv s_{2})]_{T}\;\mathsf{i}^{T}\mathsf{\;}...\;\mathsf{i}^{T}\mathsf{\;}[(t_{n}\equiv s_{n})]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi(t_{1},...,t_{n})]_{T}\leq^{T}[\varphi(s_{1},...,s_{n})]_{T}\] de lo cual se desprende que \[[\varphi(t_{1},...,t_{n})]_{T}\in\mathcal{U}\text{ implica }[\varphi(s_{1},...,s_{n})]_{T}\in\mathcal{U}\] ya que \(\mathcal{U}\) es un filtro. La otra implicación es análoga.

Para probar (3) podemos tomar \(\varphi=\left(f(v_{1},...,v_{n})\equiv f(s_{1},...,s_{n})\right)\) y aplicar (2).

Definamos ahora un modelo \(\mathbf{A}_{\mathcal{U}}\) de tipo \(\tau\) de la siguiente manera:

1. adhocprefix-adhocsufix Universo de \(\mathbf{A}_{\mathcal{U}}=T_{c}^{\tau}/\mathrm{\bowtie}\)

2. adhocprefix-adhocsufix \(c^{\mathbf{A}_{\mathcal{U}}}=c/\mathrm{\bowtie}\), para cada \(c\in\mathcal{C}\).

3. adhocprefix-adhocsufix \(f^{\mathbf{A}_{\mathcal{U}}}(t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie})=f(t_{1},...,t_{n})/\mathrm{\bowtie}\), para cada \(f\in\mathcal{F}_{n}\), \(t_{1},...,t_{n}\in T_{c}^{\tau}\;\)

4. adhocprefix-adhocsufix \(r^{\mathbf{A}_{\mathcal{U}}}=\{(t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}):[r(t_{1},...,t_{n})]_{T}\in\mathcal{U}\}\), para cada \(r\in\mathcal{R}_{n}\).

Nótese que la definición de \(f^{\mathbf{A}_{\mathcal{U}}}\) es inambigua por (3). Probaremos las siguientes propiedades básicas:

1. adhocprefix(4)adhocsufix Para cada \(t=_{d}t(v_{1},...,v_{n})\in T^{\tau}\), \(t_{1},...,t_{n}\in T_{c}^{\tau}\), tenemos que \[t^{\mathbf{A}_{\mathcal{U}}}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}]=t(t_{1},...,t_{n})/\mathrm{\bowtie}\]

2. adhocprefix(5)adhocsufix Para cada \(\varphi=_{d}\varphi(v_{1},...,v_{n})\in F^{\tau}\), \(t_{1},...,t_{n}\in T_{c}^{\tau}\), tenemos que \[\mathbf{A}_{\mathcal{U}}\models\varphi[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}]\text{ si y solo si }[\varphi(t_{1},...,t_{n})]_{T}\in\mathcal{U}.\]

Para probar (4) usaremos la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Para cada \(t=_{d}t(v_{1},...,v_{n})\in T_{k}^{\tau}\), \(t_{1},...,t_{n}\in T_{c}^{\tau}\), tenemos que \[t^{\mathbf{A}_{\mathcal{U}}}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}]=t(t_{1},...,t_{n})/\mathrm{\bowtie}\]

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Trivial.

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Supongamos \(t=_{d}t(v_{1},...,v_{n})\in T_{k+1}^{\tau}\) y sean \(t_{1},...,t_{n}\in T_{c}^{\tau}\). Por el Lema de Lectura Única de Términos Declarados, hay varios casos:

Caso \(t\in\{v_{1},...,v_{n}\}\). Trivial.

Caso \(t\in\mathcal{C}\). Trivial.

Caso \(t=f(s_{1},...,s_{m})\), con \(f\in\mathcal{F}_{m}\), \(m\geq1\) y \(s_{1},...,s_{m}\in T_{k}^{\tau}\). Dado a que hemos declarado \(t=_{d}t(v_{1},...,v_{n})\), por la Convención Notacional 3, tenemos declarados también \(s_{1}=_{d}s_{1}(v_{1},...,v_{n}),...,s_{m}=_{d}s_{m}(v_{1},...,v_{n})\). O sea que \(\mathrm{Enu}_{k}\) nos dice que \(s_{i}^{\mathbf{A}_{\mathcal{U}}}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}]=s_{i}(t_{1},...,t_{n})/\mathrm{\bowtie}\), para \(i=1,...,m\). Tenemos entonces que \[\begin{aligned} t^{\mathbf{A}_{\mathcal{U}}}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}] & =f^{\mathbf{A}_{\mathcal{U}}}(s_{1}^{\mathbf{A}_{\mathcal{U}}}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}],...,s_{m}^{\mathbf{A}_{\mathcal{U}}}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}])\\ & =f^{\mathbf{A}_{\mathcal{U}}}(s_{1}(t_{1},...,t_{n})/\mathrm{\bowtie},...,s_{m}(t_{1},...,t_{n})/\mathrm{\bowtie})\\ & =f(s_{1}(t_{1},...,t_{n}),...,s_{m}(t_{1},...,t_{n}))/\mathrm{\bowtie}\\ & =t(t_{1},...,t_{n})/\mathrm{\bowtie} \end{aligned}\]

Para probar (5) tambien usaremos la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:

1. adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Para cada \(\varphi=_{d}\varphi(v_{1},...,v_{n})\in F_{k}^{\tau}\), \(t_{1},...,t_{n}\in T_{c}^{\tau}\), tenemos que \[\mathbf{A}_{\mathcal{U}}\models\varphi[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}]\text{ si y solo si }[\varphi(t_{1},...,t_{n})]_{T}\in\mathcal{U}.\]

Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).

Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Dejada al lector.

Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Supongamos \(\varphi=_{d}\varphi(v_{1},...,v_{n})\in F_{k+1}^{\tau}\) y \(t_{1},...,t_{n}\in T_{c}^{\tau}\). Por el Lema de Lectura Única de Fórmulas Declaradas hay varios casos:

Caso \(\varphi=\left(\varphi_{1}\vee\varphi_{2}\right)\), con \(\varphi_{1},\varphi_{2}\in F_{k}^{\tau}\). Nótese que por la Convención Notacional 6, tenemos que \(\varphi_{i}=_{d}\varphi_{i}(v_{1},...,v_{n})\), \(i=1,2\). Ya que \(\mathrm{Enu}_{k}\) es verdadero tenemos que \[\mathbf{A}_{\mathcal{U}}\models\varphi_{i}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}]\text{ si y solo si }[\varphi_{i}(t_{1},...,t_{n})]_{T}\in\mathcal{U}\] para \(i=1,2\). Tenemos entonces \[\begin{array}{c} \mathbf{A}_{\mathcal{U}}\models\varphi[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}]\\ \Updownarrow\\ \mathbf{A}_{\mathcal{U}}\models\varphi_{1}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}]\text{ o }\mathbf{A}_{\mathcal{U}}\models\varphi_{2}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}]\\ \Updownarrow\\{} [\varphi_{1}(t_{1},...,t_{n})]_{T}\in\mathcal{U}\text{ o }[\varphi_{2}(t_{1},...,t_{n})]_{T}\in\mathcal{U}\\ \Updownarrow\\{} [\varphi_{1}(t_{1},...,t_{n})]_{T}\ \mathsf{s}^{T}\mathsf{\ }[\varphi_{2}(t_{1},...,t_{n})]_{T}\in\mathcal{U}\\ \Updownarrow\\{} [\left(\varphi_{1}(t_{1},...,t_{n})\vee\varphi_{2}(t_{1},...,t_{n})\right)]_{T}\in\mathcal{U}\\ \Updownarrow\\{} [\varphi(t_{1},...,t_{n})]_{T}\in\mathcal{U}. \end{array}\] Caso \(\varphi=\forall v\varphi_{1}\), con \(\varphi_{1}\in F_{k}^{\tau}\) y \(v\in Var-\{v_{1},...,v_{n}\}\). Nótese que por la Convención Notacional 6, tenemos que \(\varphi_{1}=_{d}\varphi_{1}(v_{1},...,v_{n},v)\). Ya que \(\mathrm{Enu}_{k}\) es verdadero tenemos que para cada \(t\in T_{c}^{\tau}\) \[\mathbf{A}_{\mathcal{U}}\models\varphi_{1}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie},t/\mathrm{\bowtie}]\text{ si y solo si }[\varphi_{1}(t_{1},...,t_{n},t)]_{T}\in\mathcal{U}\] Tenemos entonces \[\begin{array}{c} \mathbf{A}_{\mathcal{U}}\models\varphi[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}]\\ \Updownarrow\\ \mathbf{A}_{\mathcal{U}}\models\varphi_{1}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie},t/\mathrm{\bowtie}]\text{, para todo }t\in T_{c}^{\tau}\\ \Updownarrow\\{} [\varphi_{1}(t_{1},...,t_{n},t)]_{T}\in\mathcal{U}\text{, para todo }t\in T_{c}^{\tau}\\ \Updownarrow\\{} [\forall v\varphi_{1}(t_{1},...,t_{n},v)]_{T}\in\mathcal{U}\\ \Updownarrow\\{} [\varphi(t_{1},...,t_{n})]_{T}\in\mathcal{U}. \end{array}\] Caso \(\varphi=\exists v\varphi_{1}\), con \(\varphi_{1}\in F_{k}^{\tau}\) y \(v\in Var-\{v_{1},...,v_{n}\}\). Nótese que por la Convención Notacional 6, tenemos que \(\varphi_{1}=_{d}\varphi_{1}(v_{1},...,v_{n},v)\). Ya que \(\mathrm{Enu}_{k}\) es verdadero tenemos que para cada \(t\in T_{c}^{\tau}\) \[\mathbf{A}_{\mathcal{U}}\models\varphi_{1}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie},t/\mathrm{\bowtie}]\text{ si y solo si }[\varphi_{1}(t_{1},...,t_{n},t)]_{T}\in\mathcal{U}\] Tenemos entonces \[\begin{array}{c} \mathbf{A}_{\mathcal{U}}\models\varphi[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie}]\\ \Updownarrow\\ \mathbf{A}_{\mathcal{U}}\models\varphi_{1}[t_{1}/\mathrm{\bowtie},...,t_{n}/\mathrm{\bowtie},t/\mathrm{\bowtie}]\text{, para algún }t\in T_{c}^{\tau}\\ \Updownarrow\\{} [\varphi_{1}(t_{1},...,t_{n},t)]_{T}\in\mathcal{U}\text{, para algún }t\in T_{c}^{\tau}\\ \Updownarrow\\ ([\varphi_{1}(t_{1},...,t_{n},t)]_{T})^{\mathsf{c}^{T}}\not\in\mathcal{U}\text{, para algún }t\in T_{c}^{\tau}\\ \Updownarrow\\{} [\lnot\varphi_{1}(t_{1},...,t_{n},t)]_{T}\not\in\mathcal{U}\text{, para algún }t\in T_{c}^{\tau}\\ \Updownarrow\\{} [\forall v\;\lnot\varphi_{1}(t_{1},...,t_{n},v)]_{T}\not\in\mathcal{U}\\ \Updownarrow\\ ([\forall v\;\lnot\varphi_{1}(t_{1},...,t_{n},v)]_{T})^{\mathsf{c}^{T}}\in\mathcal{U}\\ \Updownarrow\\{} [\lnot\forall v\;\lnot\varphi_{1}(t_{1},...,t_{n},v)]_{T}\in\mathcal{U}\\ \Updownarrow\\{} [\varphi(t_{1},...,t_{n})]_{T}\in\mathcal{U}. \end{array}\] Los otros casos son dejados al lector.

Pero ahora nótese que (5) en particular nos dice que para cada sentencia \(\psi\in S^{\tau}\), \(\mathbf{A}_{\mathcal{U}}\models\psi\) si y solo si \([\psi]_{T}\in\mathcal{U}.\) De esta forma llegamos a que \(\mathbf{A}_{\mathcal{U}}\models\Sigma\) y \(\mathbf{A}_{\mathcal{U}}\models\lnot\varphi_{0}\), lo cual contradice la suposición de que \(T\models\varphi_{0}.\)

Ahora supongamos que \(\tau\) es cualquier tipo. Sean \(s_{1}\) y \(s_{2}\) un par de símbolos no pertenecientes a la lista \[\forall\ \ \exists\ \ \lnot\ \ \vee\ \ \wedge\ \ \rightarrow\ \ \leftrightarrow\ \ (\ \ )\ \ ,\ \equiv\ \ \mathsf{X}\ \ \mathit{0}\ \ \mathit{1}\ \ ...\ \ \mathit{9}\ \ \mathbf{0}\ \ \mathbf{1}\ \ ...\ \ \mathbf{9}\] y tales que ninguno ocurra en alguna palabra de \(\mathcal{C}\cup\mathcal{F}\cup\mathcal{R}.\) Si \(T\models\varphi\), entonces usando el Lema de Coincidencia se puede ver que \((\Sigma,(\mathcal{C}\cup\{s_{1}s_{2}s_{1},s_{1}s_{2}s_{2}s_{1},...\},\mathcal{F},\mathcal{R},a))\models\varphi\), por lo cual \[(\Sigma,(\mathcal{C}\cup\{s_{1}s_{2}s_{1},s_{1}s_{2}s_{2}s_{1},...\},\mathcal{F},\mathcal{R},a))\vdash\varphi.\] Pero por Lema 7.50, tenemos que \(T\vdash\varphi.\)  

Veamos algunas consecuencias del Teorema de Completitud.

Proof. Supongamos \((\Sigma,\tau)\) es consistente y no tiene modelos. Ya que no tiene modelos, se da trivialmente que \((\Sigma,\tau)\models\varphi\), para cada \(\varphi\in S^{\tau}\). Obviamente esto dice que \((\Sigma,\tau)\) es inconsistente, lo cual es absurdo.  

Proof. (a) Veamos que \((\Sigma,\tau)\) es consistente. Supongamos lo contrario, es decir supongamos \((\Sigma,\tau)\vdash\left(\varphi\wedge\lnot\varphi\right)\), para alguna sentencia \(\varphi\). Nótese que entonces hay un subconjunto finito \(\Sigma_{0}\subseteq\Sigma\) tal que la teoría \((\Sigma_{0},\tau)\vdash\left(\varphi\wedge\lnot\varphi\right)\) (\(\Sigma_{0}\) puede ser formado con los axiomas de \(\Sigma\) usados en una prueba formal que atestigüe que \((\Sigma,\tau)\vdash\left(\varphi\wedge\lnot\varphi\right)\)). Pero esto es absurdo ya que por hipótesis dicha teoría \((\Sigma_{0},\tau)\) tiene un modelo (use Corrección). O sea que \((\Sigma,\tau)\) es consistente y entonces el corolario anterior nos dice que tiene un modelo

(b) Si \((\Sigma,\tau)\models\varphi\), entonces por Completitud, \((\Sigma,\tau)\vdash\varphi\). Pero entonces hay un subconjunto finito \(\Sigma_{0}\subseteq\Sigma\) tal que \((\Sigma_{0},\tau)\vdash\varphi\), es decir tal que \((\Sigma_{0},\tau)\models\varphi\) (Corrección).  

Dejamos al lector entender que es una consecuencia del Teorema de completitud que el criterio NoEsTeorema es completo, es decir que siempre que una sentencia no sea teorema de una teoría hay un modelo de la misma que hace falsa a dicha sentencia.

7.13.10 Interpretación Semántica del Álgebra de Lindenbaum

Usando los teoremas de corrección y completitud podemos dar una representación semántica del álgebra de Lindenbaum. Sea \(T=(\Sigma,\tau)\) una teoría. Dada \(\varphi\in S^{\tau}\) definamos \[\mathrm{Mod}_{T}(\varphi)=\{\mathbf{A}:\mathbf{A}\text{ es modelo de }T\text{ y }\mathbf{A}\vDash\varphi\}\] Por ejemplo \(\mathrm{Mod}_{Po}(\exists x_{1}\forall x_{2}\leq(x_{1},x_{2}))=\{(A,i):(A,i(\leq))\) es un poset con mínimo\(\}\).

Definamos también \[\mathrm{Mod}_{T}=\{\mathbf{A}:\mathbf{A}\text{ es modelo de }T\}\] Dado \(S\subseteq\mathrm{Mod}_{T}\) definamos \[S^{c}=\mathrm{Mod}_{T}-S\]

Proof. Nótese que \[\begin{aligned} \emptyset & =\mathrm{Mod}_{T}(\exists x_{1}\lnot(x_{1}\equiv x_{1}))\\ \mathrm{Mod}_{T} & =\mathrm{Mod}_{T}(\forall x_{1}(x_{1}\equiv x_{1}))\\ \mathrm{Mod}_{T}(\varphi)\cap\mathrm{Mod}_{T}(\psi) & =\mathrm{Mod}_{T}((\varphi\wedge\psi))\\ \mathrm{Mod}_{T}(\varphi)\cup\mathrm{Mod}_{T}(\psi) & =\mathrm{Mod}_{T}((\varphi\vee\psi))\\ \mathrm{Mod}_{T}(\varphi)^{c} & =\mathrm{Mod}_{T}(\lnot\varphi) \end{aligned}\]  

Proof. (1) Dejamos al lector justificar las siguientes equivalencias: \[[\varphi]_{T}\leq^{T}[\psi]_{T}\text{ sii }T\vdash(\varphi\rightarrow\psi)\text{ sii }T\models(\varphi\rightarrow\psi)\text{ sii }\mathrm{Mod}_{T}(\varphi)\subseteq\mathrm{Mod}_{T}(\psi)\] (2) y (3) siguen de (1)  

Ya que \(\{\mathrm{Mod}_{T}(\varphi):\varphi\in S^{\tau}\}\) es un subuniverso de \((\mathcal{P}(\mathrm{Mod}_{T}),\cup,\cap,^{c},\emptyset,\mathrm{Mod}_{T})\), tenemos que \((\{\mathrm{Mod}_{T}(\varphi):\varphi\in S^{\tau}\},\cup,\cap,^{c},\emptyset,\mathrm{Mod}_{T})\) es un álgebra de Boole. Nótese que (2) del lema anterior nos asegura que \[\begin{array}{rcl} S^{\tau}/\mathrm{\dashv\vdash}_{T} & \rightarrow & \{\mathrm{Mod}_{T}(\varphi):\varphi\in S^{\tau}\}\\{} [\varphi]_{T} & \rightarrow & \mathrm{Mod}_{T}(\varphi) \end{array}\] define en forma inambigua una función. Tenemos entonces el siguiente

Proof. Llamémosle \(f\) a la función del enunciado. Es claro que \(f\) es suryectiva. Además (2) del lema anterior nos dice que \(f\) es inyectiva. Además usando las igualdades de la prueba del Lema 7.53, fácilmente podemos ver que \(f\) es un homomorfismo por lo cual es un isomorfismo.  

7.13.11 Teorías Completas

Una teoría \((\Sigma,\tau)\) será llamada completa cuando para cada \(\varphi\in S^{\tau}\) se dé que \((\Sigma,\tau)\vdash\varphi\) o \((\Sigma,\tau)\vdash\lnot\varphi\). Es poco frecuente que una teoría consistente sea completa y esto lo veremos claro después del siguiente resultado. Necesitaremos la siguiente definición. Sean \(\mathbf{A}\) y \(\mathbf{B}\) dos estructuras de tipo \(\tau\). Diremos que \(\mathbf{A}\) y \(\mathbf{B}\) son elementalmente equivalentes si para cada \(\varphi\in S^{\tau}\) se da que \(\mathbf{A}\models\varphi\) sii \(\mathbf{B}\models\varphi\).

Proof. Supongamos vale (1). Probaremos (2). Supongamos \(\mathbf{A},\mathbf{B}\) son modelos de \((\Sigma,\tau)\) y supongamos \(\mathbf{A}\models\varphi\). Entonces no puede darse \((\Sigma,\tau)\vdash\lnot\varphi\) (use corrección) por lo cual tenemos que \((\Sigma,\tau)\vdash\varphi\). Ya que \(\mathbf{B}\) es modelo de \((\Sigma,\tau)\) tenemos entonces que \(\mathbf{B}\models\varphi\). Esto prueba que \(\mathbf{A}\) y \(\mathbf{B}\) son elementalmente equivalentes.

Ahora supongamos vale (2). Probaremos (3). Ya que \((\Sigma,\tau)\) es consistente, tiene al menos un modelo. Sea \(\mathbf{A}\) uno de ellos. Por corrección todo teorema es verdadero en \(\mathbf{A}\). Recíprocamente si \(\mathbf{A}\models\varphi\), entonces, por (2), todo modelo de \((\Sigma,\tau)\) satisface \(\varphi\), lo cual nos dice que \(\varphi\) es un teorema.

Obviamente (3) implica que toda sentencia es o un teorema o refutable y esto nos dice que \(0^{(\Sigma,\tau)}\cup1^{(\Sigma,\tau)}=S^{\tau}\). Ya que \(0^{(\Sigma,\tau)}\cap1^{(\Sigma,\tau)}=\emptyset\) puesto que \((\Sigma,\tau)\) es consistente, tenemos que vale (4).

Es trivial que (4) implica (1).  

Ya que lo mas común es que una teoría tenga un par de modelos no elementalmente equivalentes, la mayoría de las teorías no son completas.

7.13.12 La Aritmética de Peano

En esta sección desarrollaremos las propiedades básicas de \(Arit\), una teoría de primer orden la cual modeliza a la aritmética. Esta teoría ha sido paradigmática en el desarrollo de la lógica.

Sea \(\tau_{A}=(\{0,1\},\{+^{2},.^{2}\},\{\leq^{2}\},a)\). Denotemos con \(\mathbf{\boldsymbol{\omega}}\) a la estructura de tipo \(\tau_{A}\) que tiene a \(\omega\) como universo e interpreta los nombres de \(\tau_{A}\) en la manera usual, es decir \[\begin{array}{l} 0^{\mathbf{\boldsymbol{\omega}}}=0\\ 1^{\mathbf{\boldsymbol{\omega}}}=1\\ \leq^{\mathbf{\boldsymbol{\omega}}}=\{(n,m)\in\omega^{2}:n\leq m\}\\ +^{\mathbf{\boldsymbol{\omega}}}(n,m)=n+m\text{, para cada }n,m\in\omega\\ .^{\mathbf{\boldsymbol{\omega}}}(n,m)=n.m\text{, para cada }n,m\in\omega \end{array}\] Para facilitar la lectura, si \(t,s\in T^{\tau_{A}}\), escribiremos \(t\leq s\) en lugar de \(\mathrm{\leq}(t,s)\), \(t+s\) en lugar de \(+(t,s)\) y \(t.s\) en lugar de \(.(t,s)\). Tambien escribiremos \(t<s\) en lugar de \((t\leq s\wedge\neg(t\equiv s))\).

Sea \(\Sigma\) el conjunto formado por las siguientes sentencias:

1. adhocprefixadhocsufix \(\forall x_{1}\forall x_{2}\forall x_{3}\;x_{1}+(x_{2}+x_{3})\equiv(x_{1}+x_{2})+x_{3}\)

2. adhocprefixadhocsufix \(\forall x_{1}\forall x_{2}\;x_{1}+x_{2}\equiv x_{2}+x_{1}\)

3. adhocprefixadhocsufix \(\forall x_{1}\forall x_{2}\forall x_{3}\;x_{1}.(x_{2}.x_{3})\equiv(x_{1}.x_{2}).x_{3}\)

4. adhocprefixadhocsufix \(\forall x_{1}\forall x_{2}\;x_{1}.x_{2}\equiv x_{2}.x_{1}\)

5. adhocprefixadhocsufix \(\forall x_{1}\;x_{1}+0\equiv x_{1}\)

6. adhocprefixadhocsufix \(\forall x_{1}\;x_{1}.0\equiv0\)

7. adhocprefixadhocsufix \(\forall x_{1}\;x_{1}.1\equiv x_{1}\)

8. adhocprefixadhocsufix \(\forall x_{1}\forall x_{2}\forall x_{3}\;x_{1}.(x_{2}+x_{3})\equiv(x_{1}.x_{2})+(x_{1}.x_{3})\)

9. adhocprefixadhocsufix \(\forall x_{1}\forall x_{2}\forall x_{3}\;(x_{1}+x_{3}\equiv x_{2}+x_{3}\rightarrow x_{1}\equiv x_{2})\)

10. adhocprefixadhocsufix \(\forall x_{1}\;x_{1}\leq x_{1}\)

11. adhocprefixadhocsufix \(\forall x_{1}\forall x_{2}\forall x_{3}\;((x_{1}\leq x_{2}\wedge x_{2}\leq x_{3})\rightarrow x_{1}\leq x_{3})\)

12. adhocprefixadhocsufix \(\forall x_{1}\forall x_{2}\;((x_{1}\leq x_{2}\wedge x_{2}\leq x_{1})\rightarrow x_{1}\equiv x_{2})\)

13. adhocprefixadhocsufix \(\forall x_{1}\forall x_{2}\;(x_{1}\leq x_{2}\vee x_{2}\leq x_{1})\)

14. adhocprefixadhocsufix \(\forall x_{1}\forall x_{2}\;(x_{1}\leq x_{2}\leftrightarrow\exists x_{3}\;x_{2}\equiv x_{1}+x_{3})\)

15. adhocprefixadhocsufix \(0<1\)

Es fácil ver que todas estas sentencias son satisfechas por \(\mathbf{\boldsymbol{\omega}}\) por lo cual \(\mathbf{\boldsymbol{\omega}}\) es un modelo de la teoría \((\Sigma,\tau_{A})\). Definamos \[Verd_{\mathbf{\boldsymbol{\omega}}}=\{\varphi\in S^{\tau_{A}}:\mathbf{\boldsymbol{\omega}}\models\varphi\}\] Es claro que todo teorema de \((\Sigma,\tau_{A})\) pertenece a \(Verd_{\mathbf{\boldsymbol{\omega}}}\) (por que?). Un pregunta interesante es si toda sentencia \(\varphi\in Verd_{\mathbf{\boldsymbol{\omega}}}\) es un teorema de \((\Sigma,\tau_{A})\), es decir puede ser probada en forma elemental partiendo de los axiomas de \(\Sigma\). La respuesta es no y lo explicaremos a continuación. Sea \(\mathbf{Q}^{\geq0}\) la estructura de tipo \(\tau_{A}\) que tiene a \(\{r\in\mathbf{Q}:r\geq0\}\) como universo e interpreta los nombres de \(\tau_{A}\) en la manera usual. Note que \(\mathbf{Q}^{\geq0}\) también es un modelo de \((\Sigma,\tau_{A})\). Pero entonces todo teorema de \((\Sigma,\tau_{A})\) debe ser verdadero en \(\mathbf{Q}^{\geq0}\). Pero la sentencia \(\forall x\ (x\leq1\rightarrow(x\equiv0\vee x\equiv1))\) es falsa en \(\mathbf{Q}^{\geq0}\) por lo cual no es un teorema de \((\Sigma,\tau_{A})\) y sin embargo pertenece a \(Verd_{\mathbf{\boldsymbol{\omega}}}\). Es decir los axiomas de \(\Sigma\) son demasiado generales y deberíamos agregarle axiomas que sean mas característicos de la estructura particular de \(\mathbf{\boldsymbol{\omega}}\). En esa dirección, a continuación extenderemos el conjunto \(\Sigma\) con axiomas que nos permitirán hacer pruebas por inducción tal como se lo hace en la aritmética básica.

Dada una fórmula \(\psi\in F^{\tau_{A}}\) y variables \(v_{1},...,v_{n+1}\), con \(n\geq0\), tales que \(Li(\psi)\subseteq\{v_{1},...,v_{n+1}\}\) y \(v_{i}\neq v_{j}\) siempre que \(i\neq j\), denotaremos con \(Ind_{\psi,v_{1},...,v_{n+1}}\) a la siguiente sentencia de tipo \(\tau_{A}\) \[\forall v_{1}...\forall v_{n}\ ((\psi(\vec{v},0)\wedge\forall v_{n+1}\ (\psi(\vec{v},v_{n+1})\rightarrow\psi(\vec{v},+(v_{n+1},1))))\rightarrow\forall v_{n+1}\ \psi(\vec{v},v_{n+1}))\] donde suponemos que hemos declarado \(\psi=_{d}\psi(v_{1},...,v_{n+1})\). Nótese que si por ejemplo \(Li(\psi)\subseteq\{x_{1},x_{2},x_{3}\}\), entonces las seis sentencias \[Ind_{\psi,x_{1},x_{2},x_{3}}\ \ Ind_{\psi,x_{1},x_{3},x_{2}}\ \ Ind_{\psi,x_{2},x_{1},x_{3}}\ \ Ind_{\psi,x_{2},x_{3},x_{1}}\ \ Ind_{\psi,x_{3},x_{1},x_{2}}\ \ Ind_{\psi,x_{3},x_{2},x_{1}}\] son todas distintas.

Sea \(\Sigma_{A}\) el conjunto que resulta de agregarle a \(\Sigma\) todas las sentencias de la forma \(Ind_{\psi,v_{1},...,v_{n+1}}\). Nótese que el conjunto \(\Sigma_{A}\) es infinito.

La teoría \((\Sigma_{A},\tau_{A})\) será llamada Aritmética de Peano y la denotaremos con \(Arit\). Es intuitivamente claro que

Proof. Sean \(\psi\in F^{\tau_{A}}\) y \(v_{1},...,v_{n+1}\), con \(n\geq0\), tales que \(Li(\psi)\subseteq\{v_{1},...,v_{n+1}\}\) y \(v_{i}\neq v_{j}\) siempre que \(i\neq j\). Veremos que \(\mathbf{\boldsymbol{\omega}}\vDash Ind_{\psi,v_{1},...,v_{n+1}}\). Declaremos \(\psi=_{d}\psi(v_{1},...,v_{n},v_{n+1})\). Sea \[\varphi=((\psi(\vec{v},0)\wedge\forall v_{n+1}\ (\psi(\vec{v},v_{n+1})\rightarrow\psi(\vec{v},+(v_{n+1},1)))\rightarrow\forall v_{n+1}\ \psi(\vec{v},v_{n+1}))\] Declaremos \(\varphi=_{d}\varphi(v_{1},...,v_{n})\). Nótese que \(\mathbf{\boldsymbol{\omega}}\vDash Ind_{\psi,v_{1},...,v_{n+1}}\) si y solo si para cada \(a_{1},...,a_{n}\in\omega\) se tiene que \(\mathbf{\boldsymbol{\omega}}\vDash\varphi[\vec{a}]\). Sean \(a_{1},...,a_{n}\in\omega\) fijos. Probaremos que \(\mathbf{\boldsymbol{\omega}}\vDash\varphi[\vec{a}]\). Notar que si \[\mathbf{\boldsymbol{\omega}}\nvDash(\psi(\vec{v},0)\wedge\forall v_{n+1}\ (\psi(\vec{v},v_{n+1})\rightarrow\psi(\vec{v},+(v_{n+1},1)))[\vec{a}]\] entonces \(\mathbf{\boldsymbol{\omega}}\vDash\varphi[\vec{a}]\) por lo cual podemos hacer solo el caso en que \[\mathbf{\boldsymbol{\omega}}\vDash(\psi(\vec{v},0)\wedge\forall v_{n+1}\ (\psi(\vec{v},v_{n+1})\rightarrow\psi(\vec{v},+(v_{n+1},1)))[\vec{a}]\] Para probar que \(\mathbf{\boldsymbol{\omega}}\vDash\varphi[\vec{a}]\), deberemos probar entonces que \(\mathbf{\boldsymbol{\omega}}\vDash\forall v_{n+1}\ \psi(\vec{v},v_{n+1})[\vec{a}]\). Sea \(S=\{a\in\omega:\mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a]\}\). Ya que \(\mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},0)[\vec{a}]\), es fácil ver usando el Teorema de Reemplazo para Fórmulas que \(\mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},0]\), lo cual nos dice que \(0\in S\). Ya que \(\mathbf{\boldsymbol{\omega}}\vDash\forall v_{n+1}\ (\psi(\vec{v},v_{n+1})\rightarrow\psi(\vec{v},+(v_{n+1},1))[\vec{a}]\), tenemos que

1. adhocprefix(1)adhocsufix Para cada \(a\in\omega\), si \(\mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a]\), entonces \(\mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},+(v_{n+1},1))[\vec{a},a]\).

Pero por el Teorema de Reemplazo para Fórmulas, tenemos que \(\mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},+(v_{n+1},1))[\vec{a},a]\) sii \(\mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a+1]\), lo cual nos dice que

1. adhocprefix(2)adhocsufix Para cada \(a\in\omega\), si \(\mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a]\), entonces \(\mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a+1]\).

Ya que \(0\in S\) y (2) nos dice que \(a\in S\) implica \(a+1\in S\), tenemos que \(S=\omega\). Es decir que para cada \(a\in\omega\), se da que \(\mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a]\) lo cual nos dice que \(\mathbf{\boldsymbol{\omega}}\vDash\forall v_{n+1}\ \psi(\vec{v},v_{n+1})[\vec{a}]\).

Es rutina probar que \(\mathbf{\boldsymbol{\omega}}\) satisface los otros 15 axiomas de \(Arit\).  

El modelo \(\mathbf{\boldsymbol{\omega}}\) es llamado el modelo estándar de \(Arit\).

1. adhocprefixEjercicio:adhocsufix Pruebe que \(\mathbf{Q}^{\geq0}\) no es un modelo de \(Arit\), dando una "propiedad inductiva que no cumpla"

Definamos el mapeo \(\widehat{\ \ \ }:\omega\rightarrow\{(\;)\;,\;+\;0\;1\}^{\ast}\) de la siguiente manera \[\begin{aligned} \widehat{0} & =0\\ \widehat{1} & =1\\ \widehat{n+1} & =+(\widehat{n},1)\text{, para cada }n\geq1 \end{aligned}\]

Proof. Sea \(\tau=(\{0,1,\blacktriangle\},\{+^{2},.^{2}\},\{\leq^{2}\},a)\) y sea \(\Sigma=\Sigma_{A}\cup\{\lnot(\widehat{n}\equiv\blacktriangle):n\in\omega\}\). Por el Teorema de Compacidad la teoría \((\Sigma,\tau)\) tiene un modelo \(\mathbf{A}=(A,i)\). Ya que \[\mathbf{A}\vDash\lnot(\widehat{n}\equiv\blacktriangle)\text{, para cada }n\in\omega\] tenemos que \[i(\blacktriangle)\neq\widehat{n}^{\mathbf{A}}\text{, para cada }n\in\omega\] Por el Lema de Coincidencia la estructura \(\mathbf{B}=(A,i|_{\{0,1,+,.,\leq\}})\) es un modelo de \(Arit\). Además dicho lema nos garantiza que \(\widehat{n}^{\mathbf{B}}=\widehat{n}^{\mathbf{A}}\), para cada \(n\in\omega\), por lo cual tenemos que \[i(\blacktriangle)\neq\widehat{n}^{\mathbf{B}}\text{, para cada }n\in\omega\] Veamos que \(\mathbf{B}\) no es isomorfo a \(\mathbf{\boldsymbol{\omega}}\). Supongamos \(F:\omega\rightarrow A\) es un isomorfismo de \(\mathbf{\boldsymbol{\omega}}\) en \(\mathbf{B}\). Es fácil de probar usando la Regla de Inducción a desde \(0\) que \(F(n)=\widehat{n}^{\mathbf{B}}\), para cada \(n\in\omega\). Pero esto produce un absurdo ya que nos dice que \(i(\blacktriangle)\) no esta en la imagen de \(F\).  

1. adhocprefixEjercicio:adhocsufix Dado un modelo \(\mathbf{A}\) de \(Arit\) y elementos \(a,b\in A\), diremos que \(a\) divide a \(b\) en \(\mathbf{A}\) cuando haya un \(c\in A\) tal que \(b=.^{\mathbf{A}}(c,a).\) Un elemento \(a\in A\) será llamado primo en \(\mathbf{A}\) si \(a\neq1^{\mathbf{A}}\) y sus únicos divisores son \(1^{\mathbf{A}}\) y \(a\). Pruebe que hay un modelo de \(Arit\), \(\mathbf{A}\), en el cual hay infinitos primos no pertenecientes a \(\{\widehat{n}^{\mathbf{A}}:n\in\omega\}\).

Proof. (1) es dejada al lector.

(2) \[\begin{array}{lllll} \;1. & x_{0}\leq0 & & & \text{HIPOTESIS}1\\ \;2. & \forall x\;0\leq x & & & \text{TEOREMA}\\ \;3. & 0\leq x_{0} & & & \text{PARTICULARIZACION}(2)\\ \;4. & x_{0}\leq0\wedge0\leq x_{0} & & & \text{CONJUNCIONINTRODUCCION}(1,3)\\ \;5. & \forall x_{1}\forall x_{2}\;((x_{1}\leq x_{2}\wedge x_{2}\leq x_{1})\rightarrow x_{1}\equiv x_{2}) & & & \text{AXIOMAPROPIO}\\ \;6. & \forall x_{2}\;((x_{0}\leq x_{2}\wedge x_{2}\leq x_{0})\rightarrow x_{0}\equiv x_{2}) & & & \text{PARTICULARIZACION}(5)\\ \;7. & ((x_{0}\leq0\wedge0\leq x_{0})\rightarrow x_{0}\equiv0) & & & \text{PARTICULARIZACION}(6)\\ \;8. & x_{0}\equiv0 & & & \text{TESIS}1\text{MODUSPONENS}(4,7)\\ \;9. & x_{0}\leq0\rightarrow x_{0}\equiv0 & & & \text{CONCLUSION}\\ 10. & \forall x\ (x\leq0\rightarrow x\equiv0) & & & \text{GENERALIZACION}(9) \end{array}\]

(3) \[\begin{array}{lllll} \;1. & x_{0}+y_{0}\equiv0 & & & \text{HIPOTESIS}1\\ \;2. & 0\equiv x_{0}+y_{0} & & & \text{COMMUTATIVIDAD}(1)\\ \;3. & \exists x_{3}\ (0\equiv x_{0}+x_{3}) & & & \text{EXISTENCIAL}(2)\\ \;4. & \forall x_{1}\forall x_{2}\;(x_{1}\leq x_{2}\leftrightarrow\exists x_{3}\;x_{2}\equiv x_{1}+x_{3}) & & & \text{AXIOMAPROPIO}\\ \;5. & x_{0}\leq0\leftrightarrow\exists x_{3}\;0\equiv x_{0}+x_{3}) & & & \text{PARTICULARIZACION}^{2}(4)\\ \;6. & x_{0}\leq0 & & & \text{REEMPLAZO}(5,3)\\ \;7. & \forall x\ 0\leq x & & & \text{TEOREMA}\\ \;8. & 0\leq x_{0} & & & \text{PARTICULARIZACION}(7)\\ \;9. & x_{0}\leq0\wedge0\leq x_{0} & & & \text{CONJUNCIONINTRODUCCION}(6,8)\\ 10. & \forall x_{1}\forall x_{2}\;((x_{1}\leq x_{2}\wedge x_{2}\leq x_{1})\rightarrow x_{1}\equiv x_{2}) & & & \text{AXIOMAPROPIO}\\ 11. & ((x_{0}\leq0\wedge0\leq x_{0})\rightarrow x_{0}\equiv0) & & & \text{PARTICULARIZACION}^{2}(10)\\ 12. & x_{0}\equiv0 & & & \text{MODUSPONENS}(9,11)\\ 13. & 0+y_{0}\equiv0 & & & \text{REEMPLAZO}(12,1)\\ 14. & \forall y\ y\equiv0+y & & & \text{TEOREMA}\\ 15. & y_{0}\equiv0+y_{0} & & & \text{PARTICULARIZACION}(14)\\ 16. & y_{0}\equiv0 & & & \text{TRANSITIVIDAD}(15,13)\\ 17. & x_{0}\equiv0\wedge y_{0}\equiv0 & & & \text{TESIS}1\text{CONJUNCIONINTRODUCCION}(12,16)\\ 18. & x_{0}+y_{0}\equiv0\rightarrow(x_{0}\equiv0\wedge y_{0}\equiv0) & & & \text{CONCLUSION}\\ 19. & \forall x\forall y\;(x+y\equiv0\rightarrow(x\equiv0\wedge y\equiv0)) & & & \text{GENERALIZACION}^{2}(18) \end{array}\]  

Proof. Hay cuatro casos.

Caso \(\varphi=(t\equiv s)\), con \(t,s\) términos cerrados.

Ya que \(\mathbf{\boldsymbol{\omega}}\models\varphi\), tenemos que \(t^{\mathbf{\boldsymbol{\omega}}}=s^{\mathbf{\boldsymbol{\omega}}}\) y por lo tanto \(\widehat{t^{\mathbf{\boldsymbol{\omega}}}}=\widehat{s^{\mathbf{\boldsymbol{\omega}}}}\). Por el lema anterior tenemos que \(Arit\vdash(t\equiv\widehat{t^{\mathbf{\boldsymbol{\omega}}}}),(s\equiv\widehat{s^{\mathbf{\boldsymbol{\omega}}}})\) lo cual, ya que \(\widehat{t^{\mathbf{\boldsymbol{\omega}}}}\) y \(\widehat{s^{\mathbf{\boldsymbol{\omega}}}}\) son el mismo término nos dice por la regla de transitividad que \(Arit\vdash(t\equiv s)\).

Caso \(\varphi=(t\leq s)\), con \(t,s\) términos cerrados.

Ya que \(\mathbf{\boldsymbol{\omega}}\models\varphi\), tenemos que \(t^{\mathbf{\boldsymbol{\omega}}}\leq s^{\mathbf{\boldsymbol{\omega}}}\) y por lo tanto hay un \(k\in\omega\) tal que \(t^{\mathbf{\boldsymbol{\omega}}}+k=s^{\mathbf{\boldsymbol{\omega}}}\). Se tiene entonces que \(\widehat{t^{\mathbf{\boldsymbol{\omega}}}+k}=\widehat{s^{\mathbf{\boldsymbol{\omega}}}}\). Por el lema anterior tenemos que \(Arit\vdash+(\widehat{t^{\mathbf{\boldsymbol{\omega}}}},\widehat{k})\equiv\widehat{t^{\mathbf{\boldsymbol{\omega}}}+k}\) lo cual nos dice que \[Arit\vdash+(\widehat{t^{\mathbf{\boldsymbol{\omega}}}},\widehat{k})\equiv\widehat{s^{\mathbf{\boldsymbol{\omega}}}}\] Pero el lema anterior nos dice que \[Arit\vdash(t\equiv\widehat{t^{\mathbf{\boldsymbol{\omega}}}}),(s\equiv\widehat{s^{\mathbf{\boldsymbol{\omega}}}})\] y por lo tanto la regla de reemplazo nos asegura que \(Arit\vdash+(t,\widehat{k})\equiv s\). Ya que \[\forall x_{1}\forall x_{2}\;(x_{1}\leq x_{2}\leftrightarrow\exists x_{3}\;x_{2}\equiv x_{1}+x_{3})\] es un axioma de \(Arit\), tenemos que \(Arit\vdash(t\leq s)\).

Caso \(\varphi=\lnot(t\equiv s)\), con \(t,s\) términos cerrados.

Caso \(\varphi=\lnot(t\leq s)\), con \(t,s\) términos cerrados.  

El siguiente lema muestra que en \(Arit\) se pueden probar ciertas sentencias las cuales nos servirán para emular la Regla de Inducción Completa.

Proof. Sea \(\tilde{\varphi}=\forall w(w\leq v\rightarrow\varphi(\vec{v},w))\). Notar que \(Li(\tilde{\varphi})\subseteq\{v_{1},...,v_{n},v\}\). Declaremos \(\tilde{\varphi}=_{d}\tilde{\varphi}(\vec{v},v)\). Para hacer la prueba formal usaremos el axioma \(Ind_{\tilde{\varphi},v_{1},...,v_{n},v}\). Salvo por el uso de algunos teoremas simples y el uso simultaneo de las reglas de particularización y generalización, la siguiente es la prueba formal buscada. \[\begin{array}{lllll} \;1. & (\varphi(\vec{c},0)\wedge\forall v(\forall w(w<v\rightarrow\varphi(\vec{c},w))\rightarrow\varphi(\vec{c},v)) & & & \text{HIPOTESIS}1\\ \;2. & \;\;\;w_{0}\leq0 & & & \text{HIPOTESIS}2\\ \;3. & \;\;\;\forall x\;(x\leq0\rightarrow x\equiv0) & & & \text{TEOREMA}\\ \;4. & \;\;\;w_{0}\leq0\rightarrow w_{0}\equiv0 & & & \text{PARTICULARIZACION}(3)\\ \;5. & \;\;\;w_{0}\equiv0 & & & \text{MODUSPONENS}(2,4)\\ \;6. & \;\;\;\varphi(\vec{c},0) & & & \text{CONJUNCIONELIMINACION}(1)\\ \;7. & \;\;\;\varphi(\vec{c},w_{0}) & & & \text{TESIS}2\text{REEMPLAZO}(5,6)\\ \;8. & w_{0}\leq0\rightarrow\varphi(\vec{c},w_{0}) & & & \text{CONCLUSION}\\ \;9. & \tilde{\varphi}(\vec{c},0) & & & \text{GENERALIZACION}(8)\\ 10. & \;\;\;\tilde{\varphi}(\vec{c},v_{0}) & & & \text{HIPOTESIS}3\\ 11. & \;\;\;\;\;\;w_{0}<v_{0}+1 & & & \text{HIPOTESIS}4\\ 12. & \;\;\;\;\;\;\forall x,y\;x<y+1\rightarrow x\leq y & & & \text{TEOREMA}\\ 13. & \;\;\;\;\;\;w_{0}<v_{0}+1\rightarrow w_{0}\leq v_{0} & & & \text{PARTICULARIZACION}(12)\\ 14. & \;\;\;\;\;\;w_{0}\leq v_{0} & & & \text{MODUSPONENS}(11,13)\\ 15. & \;\;\;\;\;\;w_{0}\leq v_{0}\rightarrow\varphi(\vec{c},w_{0}) & & & \text{PARTICULARIZACION}(10)\\ 16. & \;\;\;\;\;\;\varphi(\vec{c},w_{0}) & & & \text{TESIS}4\text{MODUSPONENS}(14,15)\\ 17. & \;\;\;w_{0}<v_{0}+1\rightarrow\varphi(\vec{c},w_{0}) & & & \text{CONCLUSION}\\ 18. & \;\;\;\forall w\;w<v_{0}+1\rightarrow\varphi(\vec{c},w) & & & \text{GENERALIZACION}(17)\\ 19. & \;\;\;\forall v(\forall w(w<v\rightarrow\varphi(\vec{c},w))\rightarrow\varphi(\vec{c},v)) & & & \text{CONJUNCIONELIMINACION}(1)\\ 20. & \;\;\;(\forall w(w<v_{0}+1\rightarrow\varphi(\vec{c},w))\rightarrow\varphi(\vec{c},v_{0}+1)) & & & \text{PARTICULARIZACION}(19)\\ 21. & \;\;\;\varphi(\vec{c},v_{0}+1) & & & \text{MODUSPONENS}(18,20)\\ 22. & \;\;\;\;\;\;w_{0}\leq v_{0}+1 & & & \text{HIPOTESIS}5\\ 23. & \;\;\;\;\;\;\forall x,y\;x\leq y+1\rightarrow(x\leq y\vee x\equiv y+1) & & & \text{TEOREMA}\\ 24. & \;\;\;\;\;\;w_{0}\leq v_{0}+1\rightarrow(w_{0}\leq v_{0}\vee w_{0}\equiv v_{0}+1) & & & \text{PARTICULARIZACION}(23)\\ 25. & \;\;\;\;\;\;(w_{0}\leq v_{0}\vee w_{0}\equiv v_{0}+1) & & & \text{MODUSPONENS}(22,24)\\ 26. & \;\;\;\;\;\;w_{0}\leq v_{0}\rightarrow\varphi(\vec{c},w_{0}) & & & \text{PARTICULARIZACION}(10)\\ 27. & \;\;\;\;\;\;\;\;\;w_{0}\equiv v_{0}+1 & & & \text{HIPOTESIS}6\\ 28. & \;\;\;\;\;\;\;\;\;\varphi(\vec{c},w_{0}) & & & \text{TESIS}6\text{REEMPLAZO}(21,27)\\ 29. & \;\;\;w_{0}\equiv v_{0}+1\rightarrow\varphi(\vec{c},w_{0}) & & & \text{CONCLUSION}\\ 30. & \;\;\;\;\;\;\varphi(\vec{c},w_{0}) & & & \text{TESIS}5\text{DISJUNCIONELIM}(25,26,29)\\ 31. & \;\;\;w_{0}\leq v_{0}+1\rightarrow\varphi(\vec{c},w_{0}) & & & \text{CONCLUSION}\\ 32. & \;\;\;\tilde{\varphi}(\vec{c},v_{0}+1) & & & \text{TESIS}3\text{GENERALIZACION}(31)\\ 33. & \tilde{\varphi}(\vec{c},v_{0})\rightarrow\tilde{\varphi}(\vec{c},v_{0}+1) & & & \text{CONCLUSION}\\ 34. & \forall v\tilde{\varphi}(\vec{c},v)\rightarrow\tilde{\varphi}(\vec{c},v+1) & & & \text{GENERALIZACION}(33)\\ 35. & \tilde{\varphi}(\vec{c},0)\wedge\forall v\tilde{\varphi}(\vec{c},v)\rightarrow\tilde{\varphi}(\vec{c},v+1) & & & \text{CONJUNCIONINTRODUCCION}(9,34)\\ 36. & Ind_{\tilde{\varphi},v_{1},...,v_{n},v} & & & \text{AXIOMAPROPIO}\\ 37. & (\tilde{\varphi}(\vec{c},0)\wedge\forall v(\tilde{\varphi}(\vec{c},v)\rightarrow\tilde{\varphi}(\vec{c},v+1))\rightarrow\forall v\tilde{\varphi}(\vec{c},v) & & & \text{PARTICULARIZACION}(36)\\ 38. & \forall v\tilde{\varphi}(\vec{c},v) & & & \text{MODUSPONENS}(35,37)\\ 39. & \tilde{\varphi}(\vec{c},v_{0}) & & & \text{PARTICULARIZACION}(38)\\ 40. & v_{0}\leq v_{0}\rightarrow\varphi(\vec{c},v_{0}) & & & \text{PARTICULARIZACION}(39)\\ 41. & \forall x\;x\leq x & & & \text{AXIOMAPROPIO}\\ 42. & v_{0}\leq v_{0} & & & \text{PARTICULARIZACION}(41)\\ 43. & \varphi(\vec{c},v_{0}) & & & \text{MODUSPONENS}(40,42)\\ 44. & \forall v\varphi(\vec{c},v) & & & \text{TESIS}1\text{GENERALIZACION}(43)\\ 45. & (\varphi(\vec{c},0)\wedge\forall v(\forall w(w<v\rightarrow\varphi(\vec{c},w))\rightarrow\varphi(\vec{c},v)))\rightarrow\forall v\varphi(\vec{c},v) & & & \text{CONCLUSION}\\ 46. & \forall\vec{v}((\varphi(\vec{v},0)\wedge\forall v(\forall w(w<v\rightarrow\varphi(\vec{v},w))\rightarrow\varphi(\vec{v},v)))\rightarrow\forall v\varphi(\vec{v},v)) & & & \text{GENERALIZACION}(45) \end{array}\]