7.12 Teorias de primer orden

En esta seccion nos avocaremos a dar una solucion al punto (3) de nuestro Programa de Logica Matematica. O sea nos abocaremos al siguiente problema:

1. adhocprefix(3)adhocsufix Dar un modelo matematico del concepto de prueba elemental en una teoria elemental de tipo \(\tau\).

Este problema involucra el concepto de teoria elemental definido en la Seccion [seccion teorias elementales y pruebas elementales], el cual es intuitivo y no fue definido en forma precisa ya que depende del concepto de sentencia elemental de tipo \(\tau\). O sea que un primer paso en la resolucion de (3) sera dar un modelo matematico del concepto de teoria elemental. Recordemos que una teoria elemental es por definicion 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 matematico para las sentencias elementales puras de tipo \(\tau\) (i.e. las sentencias de tipo \(\tau\)), podemos dar el siguiente modelo matematico del concepto de teoria elemental:

Una teoria (de primer orden) sera 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 resolucion del punto (3) pero aun nos queda por hacer lo mas complicado.

Dada una teoria de primer orden \((\Sigma,\tau)\), los elementos de \(\Sigma\) seran llamados axiomas propios de \((\Sigma,\tau)\). Un modelo de \((\Sigma,\tau)\) sera una estructura de tipo \(\tau\) la cual satisfaga todos los axiomas propios de \((\Sigma,\tau)\).

Algunos ejemplos de teorias de primer orden:

La teoria \(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}\] Notese 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 vacio e \(i\) es una funcion 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 vacio y \(R\) es un orden parcial sobre \(A\). De todas maneras deberia quedar claro que en esencia un poset y un modelo de \(Po\) son la misma cosa por lo cual llamaremos a \(Po\) la teoria 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 biyeccion natural entre la clase de los modelos de \(Po\) y la clase de los posets.

La teoria \(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 teoria 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 teoria de los reticulados cuaterna y muchas veces nos referiremos a los modelos de \(RetCua\) como si fueran reticulados cuaterna.

7.12.1 Definicion del concepto de prueba formal

Recomendamos al lector repasar el concepto de prueba elemental en una teoria elemental, dado en el capitulo Estructuras y su Lenguaje Elemental. Aqui daremos un modelo matematico del concepto de prueba elemental en una teoria \((\Sigma,\tau)\). Tal como lo hemos visto en numerosos ejemplos, una prueba es una sucecion de sentencias junto con una sucesion de "justificaciones" las cuales van explicando o justificando por que es licito que cada una de dichas sentencias aparezca en la sucesion. Por supuesto nuestra definicion sera precisa y matematica por lo que deberemos trabajar bastante para poder escribirla correctamente. Como objeto matematico una prueba resultara ser un par ordenado de palabras cuya primera coordenada codificara en forma natural la sucesion de sentencias y su segunda coordenada codificara la sucesion de justificaciones.

La formalizacion matematica 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 elejimos bien la teoria, las pruebas elementales no son ni mas ni menos que las pruebas de la matematica misma por lo cual se tiene una definicion matematica de la deduccion matematica real!

7.12.1.1 Reglas

Definiremos una serie de conjuntos los cuales poseen informacion deductiva basica, es decir representan las reglas usuales con las que los matematicos dan pasos dentro de una demostracion (aunque muchas veces ellos lo hacen sin avisar debido a la obviedad de dichas reglas).

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

Sean \[\begin{aligned} 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}\}\\ 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}\] 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}\] 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 particularizacion (resp. existencia, evocacion, conjuncion-eliminacion, equivalencia-eliminacion, disjuncion-introduccion, absurdo, conmutatividad), con respecto a \(\tau\) para expresar que \((\psi,\varphi)\in Partic^{\tau}\) (resp. \((\psi,\varphi)\in Exist^{\tau}\), \((\psi,\varphi)\in Evoc^{\tau}\), \((\psi,\varphi)\in ConjElim^{\tau}\), \((\psi,\varphi)\in EquivElim^{\tau}\), \((\psi,\varphi)\in DisjInt^{\tau}\), \((\psi,\varphi)\in Absur^{\tau}\), \((\psi,\varphi)\in Commut^{\tau}\)).

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. conjuncion-introduccion, equivalencia-introduccion, disjuncion-eliminacion), 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}\)). 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 division por casos, con respecto a \(\tau\) para expresar que \((\psi_{1},\psi_{2},\psi_{3},\varphi)\in DivPorCas^{\tau}\). Sea \[Reemp^{\tau}=Reemp1^{\tau}\cup Reemp2^{\tau}\] donde

\(Reemp1^{\tau}=\{((t\equiv s),\gamma,\tilde{\gamma}):s,t\in T_{c}^{\tau},\)

\(\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \gamma\in S^{\tau}\ \mathrm{y\ }\tilde{\gamma}=\mathrm{resultado\ de\ reemplazar\ en\ }\gamma\ \mathrm{una\ ocurrencia\ 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)=Li(\psi)=\{v_{1},...,v_{n}\}\),

\(\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ n\geq0,\) \(\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}\). 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}\). Sea \[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. Notese que \(c\) es el unico nombre de constante que ocurre en \(\varphi_{1}\) y no ocurre en \(\varphi_{2}\)  

Escribiremos \((\varphi_{1},\varphi_{2})\in Generaliz^{\tau}\) via \(c\) para expresar que \((\varphi_{1},\varphi_{2})\in Generaliz^{\tau}\) y que \(c\) es el unico 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 generalizacion con nombre de constante \(c\), con respecto a \(\tau\), para expresar que \((\varphi_{1},\varphi_{2})\in Generaliz^{\tau}\) via \(c\)

Sea \[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. Notese que \(e\) es el unico nombre de constante que ocurre en \(\varphi_{2}\) y no ocurre en \(\varphi_{1}\).  

Escribiremos \((\varphi_{1},\varphi_{2})\in Elec^{\tau}\) via \(e\) para expresar que \((\varphi_{1},\varphi_{2})\in Elec^{\tau}\) y que \(e\) es el unico 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 eleccion con nombre de constante \(e\), con respecto a \(\tau\) para expresar que \((\varphi_{1},\varphi_{2})\in Elec^{\tau}\) via \(e\).

Como se puede notar hay muchas reglas y todas modelizan en forma muy natural fragmentos deductivos usuales de las pruebas elementales.

Reglas universales

Una regla \(R\) sera llamada universal cuando se de 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 valida.

Proof. Veamos que la regla de existencia es universal. Por definicion, 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)\). Sea \(t^{\mathbf{A}}\) el valor que toma \(t\) en \(\mathbf{A}\). Por el Lema 7.5 tenemos que \(\mathbf{A}\models\varphi\left[t^{\mathbf{A}}\right]\), por lo cual tenemos que \(\mathbf{A}\models\exists v\varphi(v)\).

Veamos que la regla de reemplazo es universal. Debemos probar que si \((\psi_{1},\psi_{2},\varphi)\in Reemp^{\tau}=Reemp1^{\tau}\cup Reemp2^{\tau}\), entonces \(\left((\psi_{1}\wedge\psi_{2})\rightarrow\varphi\right)\) es una sentencia universalmente valida. El caso en el que \((\psi_{1},\psi_{2},\varphi)\in Reemp1^{\tau}\) es facil y lo dejaremos al lector. Para el caso en el que \((\psi_{1},\psi_{2},\varphi)\in Reemp2^{\tau}\) nos hara falta un resultado un poco mas general. Veamos por induccion en \(k\) que si se dan las siguientes condiciones

\(\alpha\in F_{k}^{\tau}\) y \(\varphi,\psi\in F^{\tau}\)

\(\mathbf{A}\) es una estructura de tipo \(\tau\)

\(\overline{\alpha}=\) resultado de reemplazar en \(\alpha\) una ocurrencia de \(\varphi\) por \(\psi\),

\(\mathbf{A}\models\varphi\left[\vec{a}\right]\) si y solo si \(\mathbf{A}\models\psi\left[\vec{a}\right]\), para cada \(\vec{a}\in A^{\mathbf{N}}\)

entonces se da 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}}\).

CASO \(k=0.\)

Entonces \(\alpha\) es atomica y por lo tanto ya que \(\alpha\) es la unica subformula de \(\alpha\), la situacion es facil de probar.

CASO \(\alpha=\forall x_{i}\alpha_{1}.\)

Si \(\varphi=\alpha\), entonces la situacion es facil de probar. Si \(\varphi\neq\alpha\), entonces la ocurrencia de \(\varphi\) a reemplazar sucede en \(\alpha_{1}\) y por lo tanto \(\overline{\alpha}=\forall x_{i}\overline{\alpha_{1}}.\) Se tiene entonces que para un \(\vec{a}\) dado, \[\begin{array}{c} \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\\ \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})\).

Si \(\varphi=\alpha\), entonces la situacion es facil de probar. Supongamos \(\varphi\neq\alpha\) y supongamos que la ocurrencia de \(\varphi\) a reemplazar sucede en \(\alpha_{1}\). Entonces \(\overline{\alpha}=(\overline{\alpha_{1}}\vee\alpha_{2})\) y tenemos que \[\begin{array}{c} \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\\ \mathbf{A}\models\overline{\alpha_{1}}\left[\vec{a}\right]\text{ o }\mathbf{A}\models\alpha_{2}\left[\vec{a}\right]\\ \Updownarrow\\ \mathbf{A}\models\overline{\alpha}\left[\vec{a}\right] \end{array}\] Los demas casos son dejados al lector.

Dejamos al lector el chequeo de la universalidad del resto de las reglas.  

7.12.1.2 Axiomas logicos

Recordemos que dada una teoria \((\Sigma,\tau)\), los elementos de \(\Sigma\) son llamados axiomas propios y en general no son sentencias universalmente validas.

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

1. \((\varphi\leftrightarrow\varphi)\)

2. \((t\equiv t)\)

3. \((\varphi\vee\lnot\varphi)\)

4. \((\varphi\leftrightarrow\lnot\lnot\varphi)\)

5. \((\lnot\forall v\psi\leftrightarrow\exists v\lnot\psi)\)

6. \((\lnot\exists v\psi\leftrightarrow\forall v\lnot\psi)\)

donde \(t\in T_{c}^{\tau}\), \(\varphi\in S^{\tau}\), \(\psi\in F^{\tau}\), \(v\in Var\) y \(Li(\psi)\subseteq\{v\}\). Con \(AxLog^{\tau}\) denotaremos el conjunto \[\{\varphi\in S^{\tau}:\varphi\ \mathrm{es\ un\ axioma\ logico\ de\ tipo\ }\tau\}\] Notese que hay infinitos axiomas logicos de tipo \(\tau\), es decir el conjunto \(AxLog^{\tau}\) es un conjunto infinito de palabras. Por ejemplo, el formato dado en 1. produce una cantidad infinita de axiomas logicos, a saber todas las sentencias de la forma \((\varphi\leftrightarrow\varphi)\), donde \(\varphi\) es cualquier sentencia de tipo \(\tau\).

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

7.12.1.3 Justificaciones

Llamaremos numerales a los siguientes simbolos \[0\ 1\ 2\ 3\ 4\ 5\ 6\ 7\ 8\ 9\] Usaremos \(Num\) para denotar el conjunto de numerales. Notese 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}\] Notese que para \(n\in\mathbf{N}\), la palabra \(Dec(n)\) es la notacion usual decimal de \(n\). Para hacer mas agil la notacion 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 justificacion basica es una palabra perteneciente a la union 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 basicas. Una justificacion es una palabra que ya sea es una justificacion basica o pertenece a la union 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 simbolos \[(\ )\ ,\ 0\ 1\ 2\ 3\ 4\ 5\ 6\ 7\ 8\ 9\ \text{A\ B\ C\ D\ E\ G\ H\ I\ J\ L\ M\ N\ O\ P\ Q\ R\ S\ T\ U\ V\ X Z}\]

7.12.1.4 Concatenaciones balanceadas de justificaciones

Para construir el concepto de prueba elemental deberiamos trabajar con sucesiones finitas de justificaciones pero el siguiente lema nos dice que podemos reemplazarlas por ciertas palabras, i.e. sus concatenaciones, sin perder informacion. 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 lementos 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 facil 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 sucesion \(J_{1},...,J_{n}\) se puede codificar con la palabra \(J_{1}...J_{n}\) sin perder informacion. Dada \(\mathbf{J}\in Just^{+}\), usaremos \(n(\mathbf{J})\) y \(\mathbf{J}_{1},...,\mathbf{J}_{n(\mathbf{J})}\) para denotar los unicos \(n\) y \(J_{1},...,J_{n}\) cuya existencia garantiza el lema anterior.

Dados numeros 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})\text{ y \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ }\\ \exists k\ \mathbf{J}_{i}=\text{HIPOTESIS}\bar{k}\text{ y}\\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \mathbf{J}_{j}=\text{TESIS}\bar{k}\alpha\text{ para algun }\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.12.1.5 Pares adecuados

Para construir el concepto de prueba elemental deberiamos trabajar con sucesiones finitas de sentencias pero el siguiente lema nos dice que podemos reemplazarlas por ciertas palabras, i.e. sus concatenaciones, sin perder informacion.

Proof. Solo hay que probar la unicidad la cual sigue de la Proposicion 7.1.  

Es decir el lema anterior nos dice que la sucesion \(\varphi_{1},...,\varphi_{n}\) se puede codificar con la palabra \(\varphi_{1}...\varphi_{n}\) sin perder informacion. Dada \(\boldsymbol{\varphi}\in S^{\tau+}\), usaremos \(n(\boldsymbol{\varphi})\) y \(\boldsymbol{\varphi}_{1},...,\boldsymbol{\varphi}_{n(\boldsymbol{\varphi})}\) para denotar los unicos \(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}\) sera la hipotesis del bloque \(\left\langle i,j\right\rangle\) en \((\boldsymbol{\varphi},\mathbf{J})\) y \(\boldsymbol{\varphi}_{j}\) sera la tesis del bloque \(\left\langle i,j\right\rangle\) en \((\boldsymbol{\varphi},\mathbf{J})\). Diremos que \(\boldsymbol{\varphi}_{i}\) esta bajo la hipotesis \(\boldsymbol{\varphi}_{l}\) en \((\boldsymbol{\varphi},\mathbf{J})\) o que \(\boldsymbol{\varphi}_{l}\) es una hipotesis 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 ademas para todo \(B\in\mathcal{B}^{\mathbf{J}}\) se tiene que \(i\in B\Rightarrow j\in B\).

7.12.1.6 Dependencia de constantes 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 numeros \(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}\) via \(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.12.1.7 Definicion de prueba formal

Ahora si estamos en condiciones de definir el concepto de prueba formal en una teoria de primer orden. Sea \((\Sigma,\tau)\) una teoria de primer orden. Sea \(\varphi\) una sentencia de tipo \(\tau\). Una prueba formal de \(\varphi\) en \((\Sigma,\tau)\) sera un par adecuado \((\boldsymbol{\varphi},\mathbf{J})\) de algun 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 algun \(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 logico 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\) 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\) 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\) 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\) 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\) 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\) 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\) 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\) 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\) 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\) 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\) 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\) 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\) 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\) 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\) y 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\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Elec^{\tau_{1}}\) via 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\) y \((\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Generaliz^{\tau_{1}}\) via 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 ocurra en \(\boldsymbol{\varphi}\) el cual sea introducido por la aplicacion de la regla de eleccion; 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}\}\), entonces no se da que \((\boldsymbol{\varphi}_{v},\boldsymbol{\varphi}_{u})\in Elec^{\tau_{1}}\) via \(c\).

       3. adhocprefix(iii)adhocsufix \(c\) no ocurre en ninguna hipotesis de \(\boldsymbol{\varphi}_{l}\).

       4. adhocprefix(iv)adhocsufix Ningun nombre de constante que ocurra en \(\boldsymbol{\varphi}_{l}\) o en sus hipotesis, depende de \(c.\)

7.12.2 El concepto de teorema

Cuando haya una prueba de \(\varphi\) en \((\Sigma,\tau)\), diremos que \(\varphi\) es un teorema de la teoria \((\Sigma,\tau)\) y escribiremos \((\Sigma,\tau)\vdash\varphi\). A continuacion daremos algunos ejemplos de teoremas exibiendo sus pruebas formales.

En la teoria \(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 Subseccion [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)) & & \text{\textrm{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 concatenacion de la secuencia de sentencias de arriba y \(\mathbf{J}\) es la concatenacion de la secuencia de justificaciones de arriba. Notese 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 definicion de prueba es el conjunto \(\{a,b\}\).

En la teoria \((\emptyset,\tau)\)

Veamos algunos teoremas con sus pruebas formales de esta teoria.

1. adhocprefix-adhocsufix 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}\]

2. adhocprefix-adhocsufix Cualesquiera sean las sentencias \(\varphi_{1},\varphi_{2}\text{ y }\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}\]

3. 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}\]

4. 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}\]

5. 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}\]

6. 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}\]

A continuacion damos varias sentencias para que el lector de pruebas formales en \(RetCua\). La forma mas facil de hacer esto es primero dar la prueba elemental tal como se lo hizo en la seccion 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 mecanicamente para obtener la prueba formal. Todo lo contrario el debe volver a la seccion de reticulados cuaterna y hacer la respectiva prueba elemental imaginando como matematico la “novela” de su prueba elemental para luego dedicarse a traducirla a una formal. Reescribimos aqui los consejos dados en la seccion de reticulados cuaterna para realizar pruebas elementales de reticulados cuaterna:

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

   1. Cuando queramos hacer una prueba elemental de alguna sentencia elemental pura es importante no perder nuestro roll de matematicos y creer que porque debemos realizar la prueba escribiendo las cosas con sentencias elementales debemos dejar de pensar como matematicos y volvernos escarabajos sintacticos mecanicos 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 matematica involucrada la escribamos usando sentencias elementales.

   2. Una buena manera de hacer una prueba elemental de una sentencia elemental pura \(\varphi\) es primero hacer la prueba matematica sin fijarse demaciado si es elemental o no. Es decir partir de la suposicion de que tenemos un reticulado cuaterna \((L,\mathsf{s},\mathsf{i},\leq)\) fijo (pero arbitrario) e intentar (como matematicos) probar que entonces en \((L,\mathsf{s},\mathsf{i},\leq)\) se cumple \(\varphi\). Muchas ideas para esto las podra obtener de las pruebas dadas en la seccion de reticulados par. Una ves que hayamos hecho nuestra prueba como matematicos, intentar tunearla para que se vuelva una prueba elemental.

   3. Es decir debemos ser el mismo matematico de siempre solo que haciendo pruebas de un estilo muy particular.

Cabe destacar que dar una prueba formal concreta en este caso no es ni mas ni menos que dar una formalizacion matematicamente perfecta de la matematica informal existente en la respectiva prueba elemental. Es decir estamos formalizando “porciones de matematica 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.12.2.1 Azuquita para escarabajo

Las pruebas formales modelizan nuestras pruebas elementales y hemos hecho las cosas para que la modelizacion 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 definicion de prueba formal es que las pruebas (elementales) hechas por un matematico sean traducibles a una formal de la forma mas natural posible. A continuacion daremos algunas de las mecanicas mas comunes de los matematicos cuando prueban.

Mecanicas de intentar probar una implicacion

Cuando un matematico intenta probar una sentencia de la forma \((\varphi\rightarrow\psi)\) suele asumir \(\varphi\) y luego probar \(\psi\). Esto claramente puede ser emulado en nuestras pruebas formales.

Mecanicas de intentar probar una disjuncion

Cuando un matematico intenta probar una sentencia de la forma \((\varphi\vee\psi)\) suele:

1. 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 disjuncion-introduccion (caso 3)

2. Asumir \((\lnot\varphi\wedge\lnot\psi)\) y llegar a un absurdo para concluir que vale \((\varphi\vee\psi)\)

Mecanica de intentar probar un \(\forall\)

Cuando un matematico intenta probar una sentencia de la forma \(\forall v\varphi(v)\) suele:

1. Fijar un elemento \(a\) del cual supone que ademas es arbitrario, i.e. no tiene nada de particular, solo es un elemento del universo de la estructura generica en la cual el esta pensando. Luego prueba \(\varphi(a)\), y concluye que vale \(\forall v\varphi(v)\) ya que \(a\) era arbitrario.

2. Asumir que \(\exists v\lnot\varphi(v)\) y llegar a un absurdo para concluir que vale \((\varphi\vee\psi)\)

Cuando

Las pruebas formales modelizan nuestras pruebas elementales y en la mayoria de los casos la modelizacion es tan natural que el pasaje de la prueba elemental a la formal es rutinario y obvio. Sin envargo hay ciertos casos en los que la modelizacion es un poco mas burocratica y puede suceder que a uno no se le ocurra como "formalizar" (i.e. ir haciendo la prueba formal) cierta parte de una prueba elemental.

1. Sea \(\tau\) un tipo cualquiera y sea \(\varphi=_{d}\varphi(v)\) una formula de tipo \(\tau\). Ya que \((\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi)\) es un axioma logico, 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 teoria \((\emptyset,\tau)\). A continuacion se da una prueba formal en la teoria \((\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 logico. Notar que en las primeras 10 lineas se prueba \((\lnot\exists v\lnot\varphi\rightarrow\lnot\lnot\forall v\varphi)\), es decir el contraresiproco 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 implicacion 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 ultimo paso se obtiene \((\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi)\) por la regla de equivalencia-introduccion. Cabe observar que esta prueba formal no es natural u obvia, mas bien es dificil 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}\]

   En virtud de la prueba formal anterior se tiene que si redujeramos la lista de axiomas logicos sacando las sentencias de la forma \((\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi)\), el concepto de prueba formal resultante seria equivalente al dado. La razon por la cual se incluyen las sentencias de la forma \((\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi)\) como axiomas logicos es que nuestra definicion de prueba formal en una teoria intenta modelizar o describir en forma matematica a las pruebas reales de los matematicos y la sentencia \((\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi)\) es obviamente cierta para un matematico por lo cual seria un detalle artificioso de nuestra definicion si dicha sentencia resultara dificil de probar con el concepto de prueba formalizado. Dicho de otra forma, nuestro concepto de prueba formal no modelizaria en forma natural a las pruebas matematicas reales. No sucede lo mismo con los axiomas de la forma \((\lnot\exists v\varphi\leftrightarrow\forall v\lnot\varphi)\) los cuales se pueden probar formalmente en forma directa (y sin usar axiomas de las ultimas dos formas de axiomas logicos) tal como lo haria un matematico. Sin envargo hemos elejido incluir a las sentencias de la forma \((\lnot\exists v\varphi\leftrightarrow\forall v\lnot\varphi)\) como axiomas logicos por una cuestion estetica y mnemotecnica ya que ambos axiomas \((\lnot\forall v\varphi\leftrightarrow\exists v\lnot\varphi)\) y \((\lnot\exists v\varphi\leftrightarrow\forall v\lnot\varphi)\) estan muy emparentados ya que nos dicen como "eliminar la negacion de un cuantificador".

7.12.3 Propiedades basicas de pruebas y teoremas

Por supuesto los numeros asociados a las hipotesis en una prueba son completamente arbitrarios y pueden cambiarse, es decir:

Tambien 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\). Notese que el mapeo \(c\rightarrow\tilde{c}\) es una biyeccion 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}\). Analogamente para una formula \(\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}\). Notese 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. Notese que cualesquiera sean \(\psi_{1},\psi_{2}\in F^{\tau_{1}}\), tenemos que \(\psi_{1}\) se deduce de \(\psi_{2}\) por la regla de generalizacion con constante \(c\) sii \(\tilde{\psi}_{1}\) se deduce de \(\tilde{\psi}_{2}\) por la regla de generalizacion con constante \(\tilde{c}\). Para las otras reglas sucede lo mismo. Notese tambien que \(c\) ocurre en \(\psi\) sii \(\tilde{c}\) ocurre en \(\tilde{\psi}.\) Mas aun notese 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 facil chequear que \((\mathbf{\tilde{\boldsymbol{\varphi}}},\mathbf{J})\) es una prueba formal de \(\varphi\) en \((\Sigma,\tau)\) basandose en que \((\boldsymbol{\varphi},\mathbf{J})\) es una prueba formal de \(\varphi\) en \((\Sigma,\tau)\).  

Proof. (1) Notese 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)\). Notese que por los Lemas 7.34 y 7.35 podemos suponer que estas dos pruebas no comparten ningun nombre de constante auxiliar y que tampoco comparten numeros asociados a hipotesis 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 facil 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) Notese 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 P(\overline{l_{1}+1},...,\overline{l_{k}+1})\)

Sea \(m\) tal que ninguna \(J_{i}\) es igual a \(\mathrm{HIPOTESIS}\bar{m}\). Notese 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 justificacion. Es facil 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.12.4 Consistencia

Una teoria \((\Sigma,\tau)\) sera inconsistente cuando haya una sentencia \(\varphi\) tal que \((\Sigma,\tau)\vdash(\varphi\wedge\lnot\varphi).\) Una teoria \((\Sigma,\tau)\) sera consistente cuando no sea inconsistente.

Proof. (1) Si \((\Sigma,\tau)\) es inconsistente, entonces por definicion 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.36 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.36 nos diria que \((\Sigma,\tau)\vdash\psi\wedge\lnot\psi\), es decir nos diria que \((\Sigma,\tau)\) es inconsistente.

(3) es dejada al lector.  

7.12.5 El Teorema de Correccion

Como ya vimos en las secciones anteriores, el concepto matematico de prueba formal en una teoria \((\Sigma,\tau)\) fue hecho como un intento de modelizar ciertas pruebas que realizan los matematicos profecionales, a las que llamamos pruebas elementales. Es claro que cuando un matematico hace una prueba elemental de una setencia \(\varphi\) en una teoria \((\Sigma,\tau)\), comienza imaginando una estructura \(\mathbf{A}\) de tipo \(\tau\) de la cual lo unico que sabe es que ella satisface todas las sentencias de \(\Sigma\), y luego al finalizar la prueba concluye que dicho modelo imaginario satisface la ultima sentencia de la prueba, i.e. \(\varphi\). En algun sentido la mision de una prueba es justamente eso: justificar con solidez que la sentencia a probar vale en todos los modelos de la teoria.

O sea que si nuestro concepto de prueba formal permitiera probar sentencias que no sean verdaderas en todos los modelos de la teoria, 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 teoria se llama Teorema de Correccion. Lo enunciaremos fomalmente a continuacion aunque no daremos la prueba ya que es dificultosa. Antes una definicion. Dada \((\Sigma,\tau)\) una teoria, escribiremos \((\Sigma,\tau)\models\varphi\) cuando \(\varphi\) sea verdadera en todo modelo de \((\Sigma,\tau)\).

Cabe destacar que el Teorema de Correccion hace parte de la tarea encomendada en el punto (4) del programa de logica dado en la Seccion [programa de logica matematica] ya que asegura que nuestro concepto de prueba formal no es demaciado permisivo como para permitir probar sentencias que son falsas en algun modelo de la teoria. Pero dicho concepto podria ser incorrecto en el sentido que podria haber pruebas elementales dadas por matematicos la cuales no puedan ser simuladas por pruebas formales. Por ejemplo podria pasar que mañana un matematico diera una prueba elemental de una sentencia \(\varphi\) en una teoria \((\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 erroneo del concepto de prueba elemental, por ser incompleto. Por supuesto en ese caso podriamos mejorarlo viendo la prueba elemental dada por dicho matematico y enrriquesiendo a la luz de dicha prueba nuestra definicion de prueba formal. De todas maneras nos quedaria la duda de que aun esta nueva definicion 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 Correccion es el siguiente.

Proof. Supongamos \(\mathbf{A}\) es un modelo de \((\Sigma,\tau).\) Si \((\Sigma,\tau)\) fuera inconsistente, tendriamos que hay una \(\varphi\in S^{t}\) tal que \((\Sigma,\tau)\vdash(\varphi\wedge\lnot\varphi)\), lo cual por el Teorema de Correccion nos diria que \(\mathbf{A}\models(\varphi\wedge\lnot\varphi)\)  

El teorema de correccion es muy util para asegurar que una sentencia no es un teorema de una teoria 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 teoria \((\Sigma,\tau)\) basta con encontrar un modelo de \((\Sigma,\tau)\) para el cual \(\varphi\) sea falsa.

Por ejemplo, usando este criterio podemos ver que ni la sentencia \[Dis1=\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 negacion son teoremas de \(RetCua\). Obviamente esto es ya que hay reticulados cuaterna distributivos y tambien hay reticulados cuaterna no distributivos.

Concluimos la subseccion dando algunos ejemplos que muestran que si hacemos mas permisiva la definicion de prueba formal, esta ya no resulta correcta.

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)\). Notese que una estructura \(\mathbf{A}\) de tipo \(\tau\) es modelo de \(T\) sii \(f^{\mathbf{A}}\) es una funcion 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 permitieramos que lo anterior fuera una prueba formal, dejaria de valer el teorema de correccion 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 hipotesis de la sentencia a la cual se le aplica la generalizacion. 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 permitieramos que lo anterior fuera una prueba formal, dejaria de valer el Teorema de Correccion 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 hipotesis 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.12.6 El algebra 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 teoria. Podemos definir la siguiente relacion 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}:T\vdash\left(\varphi\leftrightarrow\psi\right)\}\]

Proof. La relacion es reflexiva ya que \((\varphi\leftrightarrow\varphi)\) es un axioma logico y por lo tanto \(((\varphi\leftrightarrow\varphi),\)AXIOMALOGICO\()\) es una prueba formal de \((\varphi\leftrightarrow\varphi)\) en \(T\). Veamos que es simetrica. 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 commutatividad, (2) del Lema 7.36 nos dice que \(T\vdash\left(\psi\leftrightarrow\varphi\right)\).

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

Una sentencia \(\varphi\) se dice refutable en \((\Sigma,\tau)\) si \((\Sigma,\tau)\vdash\lnot\varphi\).

Proof. Haremos la prueba de (2) y dejaremos la prueba de (1) como ejercicio. Sean \(\varphi,\psi\) refutables en \(T\), veremos que \(\varphi\dashv\vdash_{T}\psi\). Notese que \[\begin{array}{llll} 1.\; & \varphi & & \text{HIPOTESIS}1\\ 2.\; & \lnot\psi & & \text{HIPOTESIS}2\\ 3.\; & \lnot\varphi & & \text{AXIOMAPROPIO}\\ 4.\; & (\varphi\wedge\lnot\varphi) & & \text{TESIS}2\text{CONJUNCIONINTRODUCCION}(1,3)\\ 5. & \lnot\psi\rightarrow(\varphi\wedge\lnot\varphi) & & \text{CONCLUSION}\\ 6. & \psi & & \text{TESIS}1\text{ABSURDO}(5)\\ 7. & (\varphi\rightarrow\psi) & & \text{CONCLUSION}\\ 8. & \psi & & \text{HIPOTESIS}3\\ 9. & \lnot\varphi & & \text{HIPOTESIS}4\\ 10. & \lnot\psi & & \text{AXIOMAPROPIO}\\ 11. & (\psi\wedge\lnot\psi) & & \text{TESIS}4\text{CONJUNCIONINTRODUCCION}(8,10)\\ 12. & \lnot\varphi\rightarrow(\psi\wedge\lnot\psi) & & \text{CONCLUSION}\\ 13. & \varphi & & \text{TESIS}3\text{ABSURDO}(12)\\ 14. & (\psi\rightarrow\varphi) & & \text{CONCLUSION}\\ 15. & (\varphi\leftrightarrow\psi) & & \text{EQUIVALENCIAINTRODUCCION}(7,14) \end{array}\] justifica que \((\Sigma\cup\{\lnot\varphi,\lnot\psi\},\tau)\vdash(\varphi\leftrightarrow\psi)\) lo cual por (1) del Lema 7.36 nos dice que \((\Sigma,\tau)\vdash(\varphi\leftrightarrow\psi)\), obteniendo que \(\varphi\dashv\vdash_{T}\psi\). Para terminar de probar (2) faltaria ver que si \(\varphi\) es refutable en \(T\) y \(\varphi\dashv\vdash_{T}\psi\), entonces \(\psi\) es refutable en \(T\). Dejamos al lector la prueba.  

Dada una teoria \(T=(\Sigma,\tau)\) y \(\varphi\in S^{\tau}\), \([\varphi]_{T}\) denotara la clase de \(\varphi\) con respecto a la relacion de equivalencia \(\dashv\vdash_{T}\). Definiremos sobre \(S^{\tau}/\mathrm{\dashv\vdash}_{T}\) las siguiente operacion binaria \(\mathsf{s}^{T}\): \[[\varphi]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\psi]_{T}=[(\varphi\vee\psi)]_{T}\] Una observacion importante es que para que la definicion anterior de la operacion \(\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}))\). Pero esto sigue de (1) del Lema 7.36 ya 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)\},\tau)\vdash((\varphi\vee\psi)\leftrightarrow(\varphi^{\prime}\vee\psi^{\prime}))\). En forma analoga se puede ver que las siguientes igualdades definen en forma inambigua una operacion binaria \(\mathsf{i}^{T}\) sobre \(S^{\tau}/\mathrm{\dashv\vdash}_{T}\) y una operacion 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 teoria \(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 clasica de Boole para el calculo proposicional.

Proof. Por definicion de algebra 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}\). Ya que \(\forall x_{1}(x_{1}\equiv x_{1})\) es un teorema de \(T\), 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), tenemos que el Lema 7.39 nos dice que \(1^{T}=\{\varphi\in S^{\tau}:\varphi\) es un teorema de \(T\}=[\forall x_{1}(x_{1}\equiv x_{1})]_{T}\). Es decir que para probar (10) 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}=\{\varphi\in S^{\tau}:\varphi\text{ }\mathrm{es\ un\ teorema\ de\ }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})\) es un teorema de \(T\), lo cual es atestiguado por 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{DISJUNCIONINTRODUCCION}(2) \end{array}\] 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 definicion de la operacion \(\mathsf{s}^{T}\) 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}))\] Notese que por (2) del Lema 7.36, 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}(6)\\ 9. & ((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3}) & & \text{TESIS}4\text{DISJUNCIONINTRODUCCION}(7)\\ 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 definicion de prueba formal  

Dada una teoria \(T=(\Sigma,\tau)\), denotaremos con \(\mathcal{A}_{T}\) al algebra de Boole \((S^{\tau}/\mathrm{\dashv\vdash}_{T},\mathsf{s}^{T},\mathsf{i}^{T},^{\mathsf{c}^{T}},0^{T},1^{T})\). El algebra \(\mathcal{A}_{T}\) sera llamada el algebra de Lindenbaum de la teoria \(T\). Denotaremos con \(\leq^{T}\) al orden parcial asociado al algebra 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 descripcion 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 definicion de \(\mathsf{s}^{T}\) tenemos que \([(\varphi\vee\psi)]_{T}=[\psi]_{T}\), es decir \(T\vdash((\varphi\vee\psi)\leftrightarrow\psi)\). Es facil ver entonces que \(T\vdash\left(\varphi\rightarrow\psi\right)\). Reciprocamente si \(T\vdash\left(\varphi\rightarrow\psi\right)\), entonces facilmente podemos probar que \(T\vdash((\varphi\vee\psi)\leftrightarrow\psi)\), lo cual nos dice que \([(\varphi\vee\psi)]_{T}=[\psi]_{T}\). Por la definicion 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.12.7 Teorema de Completitud

Hasta el momento tenemos una definicion matematica de prueba formal que modeliza el concepto intuitivo de prueba elemental, el cual corresponde al mundo real de los matematicos profecionales. Ahora bien, nada nos asegura que no aparesca un matematico que realize una prueba elemental de una sentencia \(\varphi\) en una teoria \((\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 podria pasar por ejemplo si nos hubiesemos olvidado de incluir en nuestra definicion de prueba formal alguna regla o accion que el matematico usara para probar dicha \(\varphi\), es decir nos podria pasar que no podamos "traducir" dicha prueba elemental a una prueba formal. Parese dificil 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 empirico puesto que depende de las acciones de la comunidad matematica profecional y ademas no tiene una formulacion precisa. Por otra parte nada nos asegura que los matematicos profecionales no vayan a descubrir en el futuro algun nuevo "truco" elemental y que nuestro concepto que era completo pase a ser incompleto.

Fue un verdadero desafio cientifico (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 razon 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 matematico (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) habra una prueba formal que pruebe la misma sentencia!

Por supuesto queda la posibilidad de que una prueba elemental dada por algun matematico (ahora o en el futuro) no sea traducible en forma natural a una prueba formal que pruebe lo mismo (mas alla de que sepamos que hay una gracias a Godel). Sin envargo el lector se ira convenciendo que esto es improbable que suceda, a medida que vaya formalizando distintas pruebas elementales clasicas dadas por los matematicos a lo largo de la historia.

Cabe destacar que entonces el Teorema de Correccion junto con el Teorema de Completitud resuelven el punto (4) del Programa de Logica Matematicadado en la Seccion [programa de logica matematica].

Para probar el teorema de completitud necesitaremos algunos resultados.

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)\). Notese que aplicando varias veces el Lema 7.35 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})\). Notese 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 definicion de prueba formal en \((\Sigma,\tau)\). Todos los otros puntos se cumplen en forma directa, exepto 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 acotadamente en \(\varphi\). Primero notese que \([\forall v\varphi(v)]_{T}\leq^{T}[\varphi(t)]_{T}\), para todo termino cerrado \(t\), ya que podemos dar la siguiente prueba formal: \[\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}\] Supongamos ahora que \([\psi]_{T}\leq^{T}[\varphi(t)]_{T}\), para todo termino cerrado \(t.\) Por hipotesis 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 \((\varphi_{1}...\varphi_{n},J_{1}...J_{n})\) de \(\left(\psi\rightarrow\varphi(c)\right)\) en \(T\). Pero entonces es facil de chequear que la siguiente es una prueba formal en \((\Sigma,(\mathcal{C}-\{c\},\mathcal{F},\mathcal{R},a))\) de \(\left(\psi\rightarrow\forall v\varphi(v)\right)\): \[\begin{array}{rlcl} 1. & \varphi_{1} & & J_{1}\\ 2. & \varphi_{2} & & J_{2}\\ \vdots & \vdots & & \vdots\\ n. & \varphi_{n}=\left(\psi\rightarrow\varphi(c)\right) & & 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}\] (con \(m\) elejido suficientemente grande y \(\tau_{1}=\tau\) en la definicion de prueba, es decir con \(c\) como el unico nombre de cte auxiliar de la prueba). Por el Lema 7.41 tenemos entonces que \(T\vdash\left(\psi\rightarrow\forall v\varphi(v)\right)\). Cabe destacar que es necesaria la asumsion de que \(v\) no ocurra acotadamente en \(\varphi\) para que \((\varphi(c),\forall v\varphi(v))\in Generaliz^{\tau}\) (por que?).

Ahora supongamos el caso mas general donde \(v\) puede ocurrir acotadamente en \(\varphi\). Sea \(\gamma=\varphi(w)\), donde \(w\) es una variable que no ocurre en \(\varphi\). Claramente \(Li(\gamma)\subseteq\{w\}\). Declaremos \(\gamma=_{d}\gamma(w)\). Notese que \(w\) no ocurre acotadamente en \(\gamma\). Por lo ya probado tenemos que \[[\forall w\gamma(w)]_{T}=\inf(\{[\gamma(t)]_{T}:t\in T_{c}^{\tau}\})\] Pero \([\forall v\varphi(v)]_{T}=[\forall w\gamma(w)]_{T}\) ya que \[\begin{array}{rlcl} 1. & \forall v\varphi(v) & & \text{HIPOTESIS}1\\ 2. & \varphi(c)\text{ (es igual a }\gamma(c)\text{)} & & \text{PARTICULARIZACION}(1)\\ 3. & \forall w\gamma(w) & & \text{TESIS}1\text{GENERALIZACION}(2)\\ 4. & (\forall v\varphi(v)\rightarrow\forall w\gamma(w)) & & \text{CONCLUSION} \end{array}\] y \[\begin{array}{rlcl} 1. & \forall w\gamma(w) & & \text{HIPOTESIS}1\\ 2. & \varphi(c)\text{ (es igual a }\gamma(c)\text{)} & & \text{PARTICULARIZACION}(1)\\ 3. & & & \text{TESIS}1\text{GENERALIZACION}(2)\\ 4. & (\forall v\varphi(v)\rightarrow\forall w\gamma(w)) & & \text{CONCLUSION} \end{array}\]

es claro que \[\begin{aligned} _{T} & =[\forall w\gamma(w)]_{T}\\{} [\varphi(t)]_{T} & =[\gamma(t)]_{T}\text{ para cada }t\in T_{c}^{\tau}\}) \end{aligned}\] por lo cual obtenemos que \[[\forall v\varphi(v)]_{T}=\inf(\{[\varphi(t)]_{T}:t\in T_{c}^{\tau}\}).\]  

Proof. Dejamos al lector probar que \(\tau_{\cap}\) es un tipo, \(T^{\tau_{\cap}}=T^{\tau}\cap T^{\tau^{\prime}}\) y \(F^{\tau_{\cap}}=F^{\tau}\cap F^{\tau^{\prime}}\).

(a) y (b) son directos por induccion.

(c) Supongamos que \((\Sigma,\tau)\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\)  

Proof. Notese que las formulas de tipo \(\tau\) son palabras de algun alfabeto finito \(A\). Dado un orden total \(\leq\) para \(A\), podemos definir \[\begin{aligned} \gamma_{1} & =\min\nolimits_{\alpha}^{\leq}\left(\alpha\in F^{\tau}\wedge\left\vert Li(\alpha)\right\vert \leq1\right)\\ \gamma_{t+1} & =\min\nolimits_{\alpha}^{\leq}\left(\alpha\in F^{\tau}\wedge\left\vert Li(\alpha)\right\vert \leq1\wedge(\forall i\in\omega)_{i\leq t}\alpha\neq\gamma_{i}\right) \end{aligned}\] Notese que para \(t\in\mathbf{N}\), tenemos que \(\gamma_{t}=t\)-esimo elemento de \(\{\alpha\in F^{\tau}:\left\vert Li(\alpha)\right\vert \leq1\}\), con respecto al orden total de \(A^{\ast}\) inducido por \(\leq\). Claramente entonces la infinitupla \((\gamma_{1},\gamma_{2},...)\) cumple (1) y (2).  

Ahora si, 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}\). Notese que ya que \(T\not\vdash\varphi_{0}\), tenemos 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 algun \(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})\). Notese que por el Lema 7.42 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 Rasiova 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 formulas 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 relacion: \[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). Notese 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 implicacion es analoga.

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}\).

Notese que la definicion de \(f^{\mathbf{A}_{\mathcal{U}}}\) es inambigua por (3). Probaremos las siguientes propiedades basicas:

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}.\]

La prueba de (4) es directa por induccion. Probaremos (5) por induccion en el \(k\) tal que \(\varphi\in F_{k}^{\tau}\). El caso \(k=0\) es dejado al lector. Supongamos (5) vale para \(\varphi\in F_{k}^{\tau}\). Sea \(\varphi=_{d}\varphi(v_{1},...,v_{n})\in F_{k+1}^{\tau}-F_{k}^{\tau}\). Hay varios casos:

CASO \(\varphi=\left(\varphi_{1}\vee\varphi_{2}\right)\).

Notese que por la Convencion Notacional 6, tenemos que \(\varphi_{i}=_{d}\varphi_{i}(v_{1},...,v_{n})\). 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 \(v\in Var-\{v_{1},...,v_{n}\}\). Notese que por la Convencion Notacional 6, tenemos que \(\varphi_{1}=_{d}\varphi_{1}(v_{1},...,v_{n},v)\). 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 \(v\in Var-\{v_{1},...,v_{n}\}\). Notese que por la Convencion Notacional 6, tenemos que \(\varphi_{1}=_{d}\varphi_{1}(v_{1},...,v_{n},v)\). 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 algun }t\in T_{c}^{\tau}\\ \Updownarrow\\{} [\varphi_{1}(t_{1},...,t_{n},t)]_{T}\in\mathcal{U}\text{, para algun }t\in T_{c}^{\tau}\\ \Updownarrow\\ ([\varphi_{1}(t_{1},...,t_{n},t)]_{T})^{\mathsf{c}^{T}}\not\in\mathcal{U}\text{, para algun }t\in T_{c}^{\tau}\\ \Updownarrow\\{} [\lnot\varphi_{1}(t_{1},...,t_{n},t)]_{T}\not\in\mathcal{U}\text{, para algun }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}\] Pero ahora notese 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 suposicion de que \(T\models\varphi_{0}.\)

Ahora supongamos que \(\tau\) es cualquier tipo. Sean \(s_{1}\) y \(s_{2}\) un par de simbolos 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.41, tenemos que \(T\vdash\varphi.\)  

Proof. Supongamos \((\Sigma,\tau)\) es consistente y no tiene modelos. Entonces \((\Sigma,\tau)\models\left(\varphi\wedge\lnot\varphi\right)\), con lo cual por completitud \((\Sigma,\tau)\vdash\left(\varphi\wedge\lnot\varphi\right)\), 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\). Notese que entonces hay un subconjunto finito \(\Sigma_{0}\subseteq\Sigma\) tal que la teoria \((\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 atestigue que \((\Sigma,\tau)\vdash\left(\varphi\wedge\lnot\varphi\right)\)). Pero esto es absurdo ya que por hypotesis dicha teoria \((\Sigma_{0},\tau)\) tiene un modelo. O sea que \((\Sigma,\tau)\) es consistente por lo cual 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\) (correccion).  

7.12.8 Interpretacion semantica del algebra de Lindembaum

Usando lo teoremas de correccion y completitud podemos dar una representacion semantica del algebra de Lindembaum. Sea \(T=(\Sigma,\tau)\) una teoria. 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 minimo\(\}\).

Definamos tambien \[\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. Notese 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 algebra de Boole. Notese 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 inhambigua una funcion. Tenemos entonces el siguiente

Proof. Llamemosle \(f\) a la funcion del enunciado. Es claro que \(f\) es suryectiva. Ademas (2) del lema anterior nos dice que \(f\) es inyectiva. Ademas usando las igualdades de la prueba del Lema 7.45, facilmente podemos ver que \(f\) es un homomorfismo por lo cual es un isomorfismo.  

7.12.9 Teorias completas

Una teoria \((\Sigma,\tau)\) sera llamada completa cuando para cada \(\varphi\in S^{\tau}\) se de que \((\Sigma,\tau)\vdash\varphi\) o \((\Sigma,\tau)\vdash\lnot\varphi\). Es poco frecuente que una teoria consistente sea completa y esto lo veremos claro despues del siguiente resultado.

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 correccion) 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 correccion todo teorema es verdadero en \(\mathbf{A}\). Reciprocamente 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) impica 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 comun es que una teoria tenga un par de modelos no elementalmente equivalentes, la mayoria de las teorias no son completas.

7.12.10 La aritmetica de Peano

En esta seccion desarrollaremos las propiedades basicas de \(Arit\), una teoria de primer orden la cual modeliza a la aritmetica. Esta teoria ha sido paradigmatica en el desarrollo de la logica.

Sea \(\tau_{A}=(\{0,1\},\{+^{2},.^{2}\},\{\leq^{2}\},a)\). Denotemos con \(\mathbf{\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{\omega}}=0\\ 1^{\mathbf{\omega}}=1\\ \leq^{\mathbf{\omega}}=\{(n,m)\in\omega^{2}:n\leq m\}\\ +^{\mathbf{\omega}}(n,m)=n+m\text{, para cada }n,m\in\omega\\ .^{\mathbf{\omega}}(n,m)=n.m\text{, para cada }n,m\in\omega \end{array}\] Sea \(\Sigma\) el conjunto formado por las siguientes sentencias:

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

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

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

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

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

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

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

8. \(\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. \(\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. \(\forall x_{1}\;x_{1}\leq x_{1}\)

11. \(\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. \(\forall x_{1}\forall x_{2}\;((x_{1}\leq x_{2}\wedge x_{2}\leq x_{1})\rightarrow x_{1}\equiv x_{2})\)

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

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

15. \(0<1\)

Es facil ver que todas estas sentencias son satisfechas por \(\mathbf{\omega}\) por lo cual \(\mathbf{\omega}\) es un modelo de la teoria \((\Sigma,\tau_{A})\). Definamos \[Verd_{\mathbf{\omega}}=\{\varphi\in S^{\tau_{A}}:\mathbf{\omega}\models\varphi\}\] Es claro que todo teorema de \((\Sigma,\tau_{A})\) pertenece a \(Verd_{\mathbf{\omega}}\) (por que?). Un pregunta interesante es si toda sentencia \(\varphi\in Verd_{\mathbf{\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 continuacion. 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}\) tambien 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 envargo pertenece a \(Verd_{\mathbf{\omega}}\). Es decir los axiomas de \(\Sigma\) son demaciado generales y deberiamos agregarle axiomas que sean mas caracteristicos de la estructura particular de \(\mathbf{\omega}\). En esa direccion, a continuacion extenderemos el conjunto \(\Sigma\) con axiomas que nos permitiran hacer pruebas por induccion tal como se lo hace en la aritmetica basica.

Dada una formula \(\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})\). Notese 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}}\). Notese que el conjunto \(\Sigma_{A}\) es infinito.

La teoria \((\Sigma_{A},\tau_{A})\) sera llamada Aritmetica 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{\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})\). Notese que \(\mathbf{\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{\omega}\vDash\varphi[\vec{a}]\). Sean \(a_{1},...,a_{n}\in\omega\) fijos. Probaremos que \(\mathbf{\omega}\vDash\varphi[\vec{a}]\). Notar que si \[\mathbf{\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{\omega}\vDash\varphi[\vec{a}]\) por lo cual podemos hacer solo el caso en que \[\mathbf{\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{\omega}\vDash\varphi[\vec{a}]\), deberemos probar entonces que \(\mathbf{\omega}\vDash\forall v_{n+1}\ \psi(\vec{v},v_{n+1})[\vec{a}]\). Sea \(S=\{a\in\omega:\mathbf{\omega}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a]\}\). Ya que \(\mathbf{\omega}\vDash\psi(\vec{v},0)[\vec{a}]\), es facil ver usando el lema de reemplazo que \(\mathbf{\omega}\vDash\psi(\vec{v},v_{n+1})[\vec{a},0]\), lo cual nos dice que \(0\in S\). Ya que \(\mathbf{\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{\omega}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a]\), entonces \(\mathbf{\omega}\vDash\psi(\vec{v},+(v_{n+1},1))[\vec{a},a]\).

Pero por el lema de reemplazo, tenemos que \(\mathbf{\omega}\vDash\psi(\vec{v},+(v_{n+1},1))[\vec{a},a]\) sii \(\mathbf{\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{\omega}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a]\), entonces \(\mathbf{\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{\omega}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a]\) lo cual nos dice que \(\mathbf{\omega}\vDash\forall v_{n+1}\ \psi(\vec{v},v_{n+1})[\vec{a}]\).

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

El modelo \(\mathbf{\omega}\) es llamado el modelo standard 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 teoria \((\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\). Ademas 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{\omega}\). Supongamos \(F:\omega\rightarrow A\) es un isomorfismo de \(\mathbf{\omega}\) en \(\mathbf{B}\). Es facil de probar por induccion en \(n\) 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\) sera llamado primo en \(\mathbf{A}\) si \(a\neq1^{\mathbf{A}}\) y sus unicos 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}(5)\\ \;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\) terminos cerrados.

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

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

Ya que \(\mathbf{\omega}\models\varphi\), tenemos que \(t^{\mathbf{\omega}}\leq s^{\mathbf{\omega}}\) y por lo tanto hay un \(k\in\omega\) tal que \(t^{\mathbf{\omega}}+k=s^{\mathbf{\omega}}\). Se tiene entonces que \(\widehat{t^{\mathbf{\omega}}+k}=\widehat{s^{\mathbf{\omega}}}\). Por el lema anterior tenemos que \(Arit\vdash+(\widehat{t^{\mathbf{\omega}}},\widehat{k})\equiv\widehat{t^{\mathbf{\omega}}+k}\) lo cual nos dice que \[Arit\vdash+(\widehat{t^{\mathbf{\omega}}},\widehat{k})\equiv\widehat{s^{\mathbf{\omega}}}\] Pero el lema anterior nos dice que \[Arit\vdash(t\equiv\widehat{t^{\mathbf{\omega}}}),(s\equiv\widehat{s^{\mathbf{\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\) terminos cerrados.

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

El siguiente lema muestra que en \(Arit\) se pueden probar ciertas sentencias las cuales emulan el principio de induccion 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 particularizacion y generalizacion, 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}\]