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:
(3) Dar un modelo matematico del concepto de prueba elemental en una teoria elemental.
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 τ. 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 (Σ,τ) tal que τ es un tipo cualquiera y Σ es un conjunto de sentencias elementales puras de tipo τ. Dado que ya tenemos nuestro modelo matematico para las sentencias elementales puras de tipo τ (i.e. las sentencias de tipo τ), podemos dar el siguiente modelo matematico del concepto de teoria elemental:
Una teoria (de primer orden) sera un par (Σ,τ), donde τ es un tipo y Σ es un conjunto de sentencias de tipo τ. 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 (Σ,τ), los elementos de Σ seran llamados axiomas propios de (Σ,τ). Un modelo de (Σ,τ) sera una estructura de tipo τ la cual satisfaga todos los axiomas propios de (Σ,τ).
Algunos ejemplos de teorias de primer orden:
La teoria Po. Sea Po=({A≤R,A≤T,A≤A},τPo) donde τPo es el tipo de los posets, es decir (∅,∅,{≤},{(≤,2)}) y A≤R=∀x1≤(x1,x1)A≤T=∀x1∀x2∀x3((≤(x1,x2)∧≤(x2,x3))→≤(x1,x3))A≤A=∀x1∀x2((≤(x1,x2)∧≤(x2,x1))→(x1≡x2)) Notese que una estructura A de tipo τPo es un modelo de Po si y solo si ≤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 {≤} tal que i(≤) es un orden parcial sobre A. Es decir, un modelo de Po es un par (A,{(≤,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 τRetCua=(∅,{s2,i2},{≤2},a) y sea ΣRetCua el siguiente conjunto de sentencias: A≤R=∀x1≤(x1,x1)A≤T=∀x1∀x2∀x3((≤(x1,x2)∧≤(x2,x3))→≤(x1,x3))A≤A=∀x1∀x2((≤(x1,x2)∧≤(x2,x1))→(x1≡x2))AsesC=∀x1∀x2(≤(x1,s(x1,x2))∧≤(x2,s(x1,x2)))As≤C=∀x1∀x2∀x3((≤(x1,x3)∧≤(x2,x3))→≤(s(x1,x2),x3))AiesC=∀x1∀x2(≤(i(x1,x2),x1)∧≤(i(x1,x2),x2))Ai≥C=∀x1∀x2∀x3((≤(x3,x1)∧≤(x3,x2))→≤(x3,i(x1,x2))) Definamos RetCua=(ΣRetCua,τRetCua). Obviamente los modelos de esta teoria son esencialmente reticulados cuaterna en el sentido que una estructura A de tipo τRetCua es un modelo de RetCua si y solo si (A,sA,iA,≤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.
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 (Σ,τ). 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 que modeliza a la deduccion matematica real!
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 τ es un tipo cualquiera, un termino t∈Tτ es llamado cerrado si ninguna variable es subtermino de t. Con Tτc denotamos el conjunto formado por todos los terminos cerrados.
Sean Particτ={(∀vφ(v),φ(t)):φ=dφ(v)∈Fτ y t∈Tτc}Existτ={(φ(t),∃vφ(v)):φ=dφ(v)∈Fτ y t∈Tτc}Evocτ={(φ,φ):φ∈Sτ}ConjElimτ={((φ∧ψ),φ):φ,ψ∈Sτ}∪{((φ∧ψ),ψ):φ,ψ∈Sτ}EquivElimτ={((φ↔ψ),(φ→ψ)):φ,ψ∈Sτ}∪{((φ↔ψ),(ψ→φ)):φ,ψ∈Sτ}DisjIntτ={(φ,(φ∨ψ)):φ,ψ∈Sτ}∪{(ψ,(φ∨ψ)):φ,ψ∈Sτ}∪{((¬φ→ψ),(φ∨ψ)):φ,ψ∈Sτ} Sea Absurτ=Absur1τ∪Absur2τ∪Absur3τ donde Absur1τ={((¬φ→(ψ∧¬ψ)),φ):φ,ψ∈Sτ}Absur2τ={((φ→(ψ∧¬ψ)),¬φ):φ,ψ∈Sτ}Absur3τ={((ψ∧¬ψ),φ):φ,ψ∈Sτ} Sea Commutτ=Commut1τ∪Commut2τ donde Commut1τ={((t≡s),(s≡t)):s,t∈Tτc}Commut2τ={((φ↔ψ),(ψ↔φ)):φ,ψ∈Sτ} Diremos que φ se deduce de ψ por la regla de particularizacion (resp. existencia, evocacion, conjuncion-eliminacion, equivalencia-eliminacion, disjuncion-introduccion, absurdo, conmutatividad), con respecto a τ para expresar que (ψ,φ)∈Particτ (resp. (ψ,φ)∈Existτ, (ψ,φ)∈Evocτ, (ψ,φ)∈ConjElimτ, (ψ,φ)∈EquivElimτ, (ψ,φ)∈DisjIntτ, (ψ,φ)∈Absurτ, (ψ,φ)∈Commutτ).
Sean ModPonτ={(φ,(φ→ψ),ψ):φ,ψ∈Sτ}ConjIntτ={(φ,ψ,(φ∧ψ)):φ,ψ∈Sτ}EquivIntτ={((φ→ψ),(ψ→φ),(φ↔ψ)):φ,ψ∈Sτ}DisjElimτ={(¬φ,(φ∨ψ),ψ):φ,ψ∈Sτ}∪{(¬ψ,(φ∨ψ),φ):φ,ψ∈Sτ} Diremos que φ se deduce de ψ1 y ψ2 por la regla de Modus Ponens (resp. conjuncion-introduccion, equivalencia-introduccion, disjuncion-eliminacion), con respecto a τ para expresar que (ψ1,ψ2,φ)∈ModPonτ (resp. (ψ1,ψ2,φ)∈ConjIntτ, (ψ1,ψ2,φ)∈EquivIntτ, (ψ1,ψ2,φ)∈DisjElimτ). Sea DivPorCasτ={((φ1∨φ2),(φ1→ψ),(φ2→ψ),ψ):φ1,φ2,ψ∈Sτ} Diremos que φ se deduce de ψ1, ψ2 y ψ3 por la regla de division por casos, con respecto a τ para expresar que (ψ1,ψ2,ψ3,φ)∈DivPorCasτ. Sea Reempτ=Reemp1τ∪Reemp2τ donde
Reemp1τ={(∀v1...∀vn(t≡s),γ,˜γ):s,t∈Tτ, Li((t≡s))⊆{v1,...,vn},
n≥0, γ,˜γ∈Sτ y ˜γ=resultado de reemplazar en γ una ocurrencia de t por s}
Reemp2τ={(∀v1...∀vn(φ↔ψ),γ,˜γ):φ,ψ∈Fτ, Li(φ)∪Li(ψ)⊆{v1,...,vn},
n≥0, γ,˜γ∈Sτ y ˜γ=resultado de reemplazar en γ una ocurrencia de φ por ψ}
Diremos que φ se deduce de ψ1y ψ2 por la regla de reemplazo, con respecto a τ, para expresar que (ψ1,ψ2,φ)∈Reempτ.
Sea
Transτ=Trans1τ∪Trans2τ∪Trans3τ donde Trans1τ={((t≡s),(s≡u),(t≡u)):t,s,u∈Tτc}Trans2τ={((φ→ψ),(ψ→Φ),(φ→Φ)):φ,ψ,Φ∈Sτ}Trans3τ={((φ↔ψ),(ψ↔Φ),(φ↔Φ)):φ,ψ,Φ∈Sτ} Diremos que φ se deduce de ψ1y ψ2 por la regla de transitividad, con respecto a τ para expresar que (ψ1,ψ2,φ)∈Transτ. Sea Generalizτ={(φ(c),∀vφ(v)):φ=dφ(v)∈Fτ, Li(φ)={v} y c∈C no ocurre en φ} Es importante el siguiente
7.30. Si (φ1,φ2)∈Generalizτ, entonces el nombre de constante c del cual habla la definicion de Generalizτ esta univocamente determinado por el par (φ1,φ2).
Proof. Notese que c es el unico nombre de constante que ocurre en φ1 y no ocurre en φ2
Escribiremos (φ1,φ2)∈Generalizτ via c para expresar que (φ1,φ2)∈Generalizτ y que c es el unico nombre de constante que ocurre en φ1 y no ocurre en φ2. Diremos que φ2 se deduce de φ1 por la regla de generalizacion con nombre de constante c, con respecto a τ, para expresar que (φ1,φ2)∈Generalizτ via c
Sea Elecτ={(∃vφ(v),φ(e)):φ=dφ(v)∈Fτ, Li(φ)={v} y e∈C no ocurre en φ} Es importante el siguiente
7.31. Si (φ1,φ2)∈Elecτ, entonces el nombre de constante e del cual habla la definicion de Elecτ esta univocamente determinado por el par (φ1,φ2).
Proof. Notese que e es el unico nombre de constante que ocurre en φ2 y no ocurre en φ1.
Escribiremos (φ1,φ2)∈Elecτ via e para expresar que (φ1,φ2)∈Elecτ y que e es el unico nombre de constante que ocurre en φ2 y no ocurre en φ1. Diremos que φ2 se deduce de φ1 por la regla de eleccion con nombre de constante e, con respecto a τ para expresar que (φ1,φ2)∈Elecτ via e.
Como se puede notar hay muchas reglas y todas modelizan en forma muy natural fragmentos deductivos usuales de las pruebas elementales.
Una regla R sera llamada universal cuando se de que si φ se deduce de ψ1,...,ψk por R, entonces ((ψ1∧...∧ψk)→φ) es una sentencia universalmente valida.
7.32. Sea τ un tipo. Todas las reglas exepto las reglas de eleccion y generalizacion son universales.
Proof. Veamos que la regla de existencia es universal. Por definicion, un par de Existτ es siempre de la forma (φ(t),∃vφ(v)), con φ=dφ(v) y t∈Tτc. Sea A una estructura de tipo τ tal que A⊨φ(t). Sea tA el valor que toma t en A. Por el Lema 7.5 tenemos que A⊨φ[tA], por lo cual tenemos que A⊨∃vφ(v).
Veamos que la regla de reemplazo es universal. Debemos probar que si (ψ1,ψ2,φ)∈Reempτ=Reemp1τ∪Reemp2τ, entonces ((ψ1∧ψ2)→φ) es una sentencia universalmente valida. El caso en el que (ψ1,ψ2,φ)∈Reemp1τ es facil y lo dejaremos al lector. Para el caso en el que (ψ1,ψ2,φ)∈Reemp2τ nos hara falta un resultado un poco mas general. Veamos por induccion en k que si se dan las siguientes condiciones
- α∈Fτk y φ,ψ∈Fτ
- A es una estructura de tipo τ
- ¯α= resultado de reemplazar en α una ocurrencia de φ por ψ,
- A⊨φ[→a] si y solo si A⊨ψ[→a], para cada →a∈AN
entonces se da que
- A⊨α[→a] si y solo si A⊨¯α[→a], para cada →a∈AN.
CASO k=0.
Entonces α es atomica y por lo tanto ya que α es la unica subformula de α, la situacion es facil de probar.
CASO α=∀xiα1.
Si φ=α, entonces la situacion es facil de probar. Si φ≠α, entonces la ocurrencia de φ a reemplazar sucede en α1 y por lo tanto ¯α=∀xi¯α1. Se tiene entonces que para un →a dado, A⊨α[→a]⇕A⊨α1[↓ai→a], para cada a∈A⇕A⊨¯α1[↓ai→a], para cada a∈A⇕A⊨¯α[→a] CASO α=(α1∨α2).
Si φ=α, entonces la situacion es facil de probar. Supongamos φ≠α y supongamos que la ocurrencia de φ a reemplazar sucede en α1. Entonces ¯α=(¯α1∨α2) y tenemos que A⊨α[→a]⇕A⊨α1[→a] o A⊨α2[→a]⇕A⊨¯α1[→a] o A⊨α2[→a]⇕A⊨¯α[→a] Los demas casos son dejados al lector.
Dejamos al lector el chequeo de la universalidad del resto de las reglas.
Recordemos que dada una teoria (Σ,τ), los elementos de Σ 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 τ a todas las sentencias de alguna de las siguientes formas.
(t≡t), con t∈Tτc
(Qvφ↔φ), con Q∈{∀,∃}, v∈Var y φ∈Sτ
(¬(φ∨ψ)↔(¬φ∧¬ψ)), con φ,ψ∈Sτ
(¬(φ∧ψ)↔(¬φ∨¬ψ)), con φ,ψ∈Sτ
(¬(φ→ψ)↔(φ∧¬ψ)), con φ,ψ∈Sτ
(¬(φ↔ψ)↔((φ∧¬ψ)∨(¬φ∧ψ))), con φ,ψ∈Sτ
(¬¬φ↔φ), con φ∈Sτ
(¬∀vγ↔∃v¬γ), con v∈Var, γ∈Fτ y Li(γ)⊆{v}
(¬∃vγ↔∀v¬γ), con v∈Var, γ∈Fτ y Li(γ)⊆{v}
Con AxLogτ denotaremos el conjunto {φ∈Sτ:φ es un axioma logico de tipo τ} Notese que hay infinitos axiomas logicos de tipo τ, es decir el conjunto AxLogτ es un conjunto infinito de palabras. Por ejemplo, el formato dado en (5) produce una cantidad infinita de axiomas logicos, a saber todas las sentencias de la forma (¬(φ∧ψ)↔(¬φ∨¬ψ)), donde φ y ψ son cualquier par de sentencias de tipo τ. O sea que cada renglon de arriva corresponde no a un axioma sino a una cantidad infinita de axiomas, todos con un formato determinado. Se le suelen llamar Axiomas Esquema a este tipo de formatos que describen una morfologia de cierta familia de axiomas.
El axioma esquema dado en (1) sin dudas describe la familia de axiomas mas basicos que uno puede imaginar. Llamaremos a este axioma esquema el Axioma Esquema de Identidad.
Al axioma esquema dado en (2) lo llamaremos el Axioma Esquema de Cuantificacion Vacua.
Al axioma esquema dado en (3) lo llamaremos el Axioma Esquema Negacion del ∨.
Al dado en (4) lo llamaremos el Axioma Esquema Negacion del ∧.
Al dado en (7) lo llamaremos el Axioma Esquema Negacion de ¬.
Al dado en (8) lo llamaremos el Axioma Esquema Negacion del ∀.
Al resto el lector ya se habra dado cuenta como los llamaremos.... Notese que los 7 ultimos axiomas esquema nos dan formas equivalentes a las negaciones de cada uno de los formatos posibles de formulas no atomicas dados en el Lema Menu de Formulas. Ya veremos en Mecanicas de negacion como estos axiomas se pueden usar para simular los comiensos de pruebas por el absurdo que usualmente hacen los matematicos.
Ejercicio: Pruebe que cada sentencia de AxLogτ es universalmente valida
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∩ω=∅. Sea Sig:Num∗→Num∗ definida de la siguiente manera Sig(ε)=1Sig(α0)=α1Sig(α1)=α2Sig(α2)=α3Sig(α3)=α4Sig(α4)=α5Sig(α5)=α6Sig(α6)=α7Sig(α7)=α8Sig(α8)=α9Sig(α9)=Sig(α)0 Definamos Dec:ω→Num∗ de la siguiente manera Dec(0)=εDec(n+1)=Sig(Dec(n)) Notese que para n∈N, la palabra Dec(n) es la notacion usual decimal de n. Para hacer mas agil la notacion escribiremos ˉn en lugar de Dec(n).
Sea Nombres1 el conjunto formado por las siguientes palabras EXISTENCIACOMMUTATIVIDADPARTICULARIZACIONABSURDOEVOCACIONCONJUNCIONELIMINACIONEQUIVALENCIAELIMINACIONDISJUNCIONINTRODUCCIONELECCIONGENERALIZACION Sea Nombres2 el conjunto formado por las siguientes palabras MODUSPONENSTRANSITIVIDADCONJUNCIONINTRODUCCIONEQUIVALENCIAINTRODUCCIONDISJUNCIONELIMINACIONREEMPLAZO Una justificacion basica es una palabra perteneciente a la union de los siguientes conjuntos de palabras {CONCLUSION,AXIOMAPROPIO,AXIOMALOGICO} {α(ˉk):k∈N y α∈Nombres1} {α(ˉj,ˉk):j,k∈N y α∈Nombres2} {DIVISIONPORCASOS(ˉj,ˉk,ˉl):j,k,l∈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 {HIPOTESISˉk:k∈N} {TESISˉjα:j∈N y α∈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 A\ B\ C\ D\ E\ G\ H\ I\ J\ L\ M\ N\ O\ P\ Q\ R\ S\ T\ U\ V\ X Z
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+={α1...αn:α1,...,αn∈L y n≥1}
7.33. Sea J∈Just+. Hay unicos n≥1 y J1,...,Jn∈Just tales que J=J1...Jn.
Proof. Supongamos J1,...,Jn, J′1,...,J′m, con n,m≥1, son justificaciones tales que J1...Jn=J′1...J′m. Es facil ver que entonces tenemos J1=J′1, por lo cual J2...Jn=J′2...J′m. Un argumento inductivo nos dice que entonces n=m y Ji=J′i, i=1,...,n
Es decir el lema anterior nos dice que la sucesion J1,...,Jn se puede codificar con la palabra J1...Jn sin perder informacion. Dada J∈Just+, usaremos n(J) y J1,...,Jn(J) para denotar los unicos n y J1,...,Jn cuya existencia garantiza el lema anterior.
Dados numeros naturales i≤j, usaremos ⟨i,j⟩ para denotar el conjunto {i,i+1,...,j}. A los conjuntos de la forma ⟨i,j⟩ los llamaremos bloques.
Dada J∈Just+ definamos BJ={⟨i,j⟩:1≤i≤j≤n(J) y \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ∃k Ji=HIPOTESISˉk y Jj=TESISˉkα para algun α∈JustBas} Diremos que J∈Just+ es balanceada si se dan las siguientes
(1) Por cada k∈N a lo sumo hay un i tal que Ji= HIPOTESISˉk y a lo sumo hay un i tal que Ji= TESISˉkα, con α∈JustBas
(2) Si Ji=HIPOTESISˉk entonces hay un l>i tal que Jl=TESISˉkα, con α∈JustBas
(3) Si Ji=TESISˉkα, con α∈JustBas, entonces hay un l<i tal que Jl=HIPOTESISˉk
(4) Si B1,B2∈BJ, entonces B1∩B2=∅ o B1⊆B2 o B2⊆B1
Ejercicio: Supongamos J∈Just+ es balanceada. Entonces
Si ⟨i,j⟩∈BJ, entonces i<j
Si ⟨i,j⟩,⟨i′,j′⟩∈BJ y i=i′, entonces j=j′
Si ⟨i,j⟩,⟨i′,j′⟩∈BJ y j=j′, entonces i=i′
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.
7.34. Sea φ∈Sτ+. Hay unicos n≥1 y φ1,...,φn∈Sτ tales que φ=φ1...φn.
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 φ1,...,φn se puede codificar con la palabra φ1...φn sin perder informacion. Dada φ∈Sτ+, usaremos n(φ) y φ1,...,φn(φ) para denotar los unicos n y φ1,...,φn cuya existencia garantiza el lema anterior.
Un par adecuado de tipo τ es un par (φ,J)∈Sτ+×Just+ tal que n(φ)=n(J) y J es balanceada.
Sea (φ,J) un par adecuado de tipo τ. Si ⟨i,j⟩∈BJ, entonces φi sera la hipotesis del bloque ⟨i,j⟩ en (φ,J) y φj sera la tesis del bloque ⟨i,j⟩ en (φ,J). Diremos que φi esta bajo la hipotesis φl en (φ,J) o que φl es una hipotesis de φi en (φ,J) cuando haya en BJ un bloque de la forma ⟨l,j⟩ el cual contenga a i. Sean i,j∈⟨1,n(φ)⟩. Diremos que i es anterior a j en (φ,J) si i<j y ademas para todo B∈BJ se tiene que i∈B⇒j∈B.
Sea (φ,J) un par adecuado de tipo τ. Dadas e,d∈C, diremos que e depende directamente de d en (φ,J) si hay numeros 1≤l<j≤n(φ) tales que
(1) l es anterior a j en (φ,J)
(2) Jj=αELECCION(ˉl), con α∈{ε}∪{TESISˉk:k∈N} y (φl,φj)∈Elecτ via e
(3) d ocurre en φl.
Dados e,d∈C, diremos que e depende de d en (φ,J) si existen e0,...,ek+1∈C, con k≥0, tales que
(1) e0=e y ek+1=d
(2) ei depende directamente de ei+1 en (φ,J), para i=0,...,k.
Ahora si estamos en condiciones de definir el concepto de prueba formal en una teoria de primer orden. Sea (Σ,τ) una teoria de primer orden. Sea φ una sentencia de tipo τ. Una prueba formal de φ en (Σ,τ) sera un par adecuado (φ,J) de algun tipo τ1=(C∪C1,F,R,a), con C1 finito y disjunto con C, tal que
(1) Cada φi es una sentencia de tipo τ1
(2) φn(φ)=φ
(3) Si ⟨i,j⟩∈BJ, entonces φj+1=(φi→φj) y Jj+1=αCONCLUSION, con α∈{ε}∪{TESISˉk:k∈N}
(4) Para cada i=1,...,n(φ), se da una de las siguientes
(a) Ji=HIPOTESISˉk para algun k∈N
(b) Ji=αCONCLUSION, con α∈{ε}∪{TESISˉk:k∈N} y hay un j tal que ⟨j,i−1⟩∈BJ y φi=(φj→φi−1)
(c) Ji=αAXIOMALOGICO, con α∈{ε}∪{TESISˉk:k∈N} y φi es un axioma logico de tipo τ1
(d) Ji=αAXIOMAPROPIO, con α∈{ε}∪{TESISˉk:k∈N} y φi∈Σ
(e) Ji=αPARTICULARIZACION(ˉl), con α∈{ε}∪{TESISˉk:k∈N}, l anterior a i en (φ,J) y (φl,φi)∈Particτ1
(f) Ji=αCOMMUTATIVIDAD(ˉl), con α∈{ε}∪{TESISˉk:k∈N}, l anterior a i en (φ,J) y (φl,φi)∈Commutτ1
(g) Ji=αABSURDO(ˉl), con α∈{ε}∪{TESISˉk:k∈N}, l anterior a i en (φ,J) y (φl,φi)∈Absurτ1
(h) Ji=αEVOCACION(ˉl), con α∈{ε}∪{TESISˉk:k∈N}, l anterior a i en (φ,J) y (φl,φi)∈Evocτ1
(i) Ji=αEXISTENCIA(ˉl), con α∈{ε}∪{TESISˉk:k∈N}, l anterior a i en (φ,J) y (φl,φi)∈Existτ1
(j) Ji=αCONJUNCIONELIMINACION(ˉl), con α∈{ε}∪{TESISˉk:k∈N}, l anterior a i en (φ,J) y (φl,φi)∈ConjElimτ1
(k) Ji=αDISJUNCIONINTRODUCCION(ˉl), con α∈{ε}∪{TESISˉk:k∈N}, l anterior a i en (φ,J) y (φl,φi)∈DisjIntτ1
(l) Ji=αEQUIVALENCIAELIMINACION(ˉl), con α∈{ε}∪{TESISˉk:k∈N}, l anterior a i en (φ,J) y (φl,φi)∈EquivElimτ1
(m) Ji=αMODUSPONENS(¯l1,¯l2), con α∈{ε}∪{TESISˉk:k∈N}, l1 y l2 anteriores a i en (φ,J) y (φl1,φl2,φi)∈ModPonτ1
(n) Ji=αCONJUNCIONINTRODUCCION(¯l1,¯l2), con α∈{ε}∪{TESISˉk:k∈N}, l1 y l2 anteriores a i en (φ,J) y (φl1,φl2,φi)∈ConjIntτ1
(o) Ji=αEQUIVALENCIAINTRODUCCION(¯l1,¯l2), con α∈{ε}∪{TESISˉk:k∈N}, l1 y l2 anteriores a i en (φ,J) y (φl1,φl2,φi)∈EquivIntτ1
(p) Ji=αDISJUNCIONELIMINACION(¯l1,¯l2), con α∈{ε}∪{TESISˉk:k∈N}, l1 y l2 anteriores a i en (φ,J) y (φl1,φl2,φi)∈DisjElimτ1
(q) Ji=αREEMPLAZO(¯l1,¯l2), con α∈{ε}∪{TESISˉk:k∈N}, l1 y l2 anteriores a i en (φ,J) y (φl1,φl2,φi)∈Reempτ1
(r) Ji=αTRANSITIVIDAD(¯l1,¯l2), con α∈{ε}∪{TESISˉk:k∈N}, l1 y l2 anteriores a i en (φ,J) y (φl1,φl2,φi)∈Transτ1
(s) Ji=αDIVISIONPORCASOS(¯l1,¯l2,¯l3), con α∈{ε}∪{TESISˉk:k∈N}, l1,l2 y l3 anteriores a i en (φ,J) y (φl1,φl2,φl3,φi)∈DivPorCasτ1
(t) Ji=αELECCION(ˉl), con α∈{ε}∪{TESISˉk:k∈N}, l anterior a i en (φ,J) y (φl,φi)∈Elecτ1 via un nombre de cte e, el cual no pertenece a C y no ocurre en φ1,...,φi−1.
(u) Ji=αGENERALIZACION(ˉl), con α∈{ε}∪{TESISˉk:k∈N}, l anterior a i en (φ,J) y (φl,φi)∈Generalizτ1 via un nombre de cte c el cual cumple:
(i) c∉C
(ii) c no es un nombre de cte que sea introducido en (φ,J) por la aplicacion de la regla de eleccion; es decir para cada u∈{1,...,n(φ)}, si Ju=αELECCION(ˉv), con α∈{ε}∪{TESISˉk:k∈N} y v anterior a u en (φ,J), entonces no se da que (φv,φu)∈Elecτ1 via c.
(iii) Para cada u∈{1,...,n(φ)}, si φu es hipotesis de φl en (φ,J), entonces c no ocurre en φu
(iv) Ningun nombre de constante que ocurra en φl depende de c en (φ,J)
(v) Para cada u∈{1,...,n(φ)}, si φu es hipotesis de φl en (φ,J), entonces ningun nombre de constante que ocurra en φu depende de c en (φ,J)
Los nombres de constante de C1 que ocurran en φ seran llamados los nombres de constante auxiliares de (φ,J). Notese que los nombres de constante auxiliares de (φ,J) son la version formalizada de los nombres de elementos fijos usados en una prueba elemental. Al tipo (C∪{nombres de cte auxiliares de (φ,J)},F,R,a) lo llamaremos el tipo ambiente de (φ,J).
Cuando haya una prueba de φ en (Σ,τ), diremos que φ es un teorema de la teoria (Σ,τ) y escribiremos (Σ,τ)⊢φ. A continuacion daremos algunos ejemplos de teoremas exibiendo sus pruebas formales.
Sea μ=∀x1∀x2((∀x3≤(x3,x1)∧∀x3≤(x3,x2))→(x1≡x2)). Veamos que μ es un teorema de Po. La idea para hacer la prueba formal es ir copiando la estructura de la prueba elemental de μ dada la Subseccion [pruebas elementales de posets]. Para facilitar la lectura la escribiremos secuencialmente 1.(∀x3≤(x3,a)∧∀x3≤(x3,b))HIPOTESIS12.∀x3≤(x3,a)CONJUNCIONELIMINACION(1)3.≤(b,a)PARTICULARIZACION(2)4.∀x3≤(x3,b)CONJUNCIONELIMINACION(1)5.≤(a,b)PARTICULARIZACION(4)6.(≤(a,b)∧≤(b,a))CONJUNCIONINTRODUCCION(5,3)7.∀x1∀x2((≤(x1,x2)∧≤(x2,x1))→(x1≡x2))AXIOMAPROPIO8.∀x2((≤(a,x2)∧≤(x2,a))→(a≡x2))PARTICULARIZACION(7)9.((≤(a,b)∧≤(b,a))→(a≡b))PARTICULARIZACION(8)10.(a≡b)TESIS1MODUSPONENS(6,9)11.((∀x3≤(x3,a)∧∀x3≤(x3,b))→(a≡b))CONCLUSION12.∀x2((∀x3≤(x3,a)∧∀x3≤(x3,x2))→(a≡x2))GENERALIZACION(11)13.∀x1∀x2((∀x3≤(x3,x1)∧∀x3≤(x3,x2))→(x1≡x2))GENERALIZACION(12) Pero por supuesto, nuestra prueba formal es en realidad el par (φ,J) donde φ es la concatenacion de la secuencia de sentencias de arriba y J es la concatenacion de la secuencia de justificaciones de arriba. Notese que las sentencias de esta prueba formal son de tipo ({a,b},∅,{≤},{(≤,2)}) es decir extendimos τ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 C1 al que se refiere la definicion de prueba es el conjunto {a,b}. Es decir las palabras a y b son los nombres de constante auxiliares de (φ,J) y el tipo ambiente de (φ,J) es ({a,b},∅,{≤},{(≤,2)}).
Veamos algunos teoremas con sus pruebas formales de esta teoria.
- ∀x1(x1≡x1) es un teorema de (∅,τ), atestiguado por la prueba formal 1.c≡cAXIOMALOGICO2.∀x1(x1≡x1)GENERALIZACION(1) (c es un nombre de cte no perteneciente a C y tal que (C∪{c},F,R,a) es un tipo).
- Cualesquiera sea la sentencia φ de tipo τ se tiene que (φ→φ) es un teorema de (∅,τ). Una prueba formal: 1.φHIPOTESIS12.φTESIS1EVOCACION(1)3.(φ→φ)CONCLUSION
- Cualesquiera sea la sentencia φ de tipo τ se tiene que (φ↔φ) es un teorema de (∅,τ). Una prueba formal: 1.φHIPOTESIS12.φTESIS1EVOCACION(1)3.(φ→φ)CONCLUSION4.(φ→φ)EVOCACION(3)5.(φ↔φ)EQUIVALENCIAINTRODUCCION(3,4) Cualesquiera sea la sentencias φ de tipo τ se tiene que (φ∨¬φ) es un teorema de (∅,τ). Una prueba formal: 1.¬φHIPOTESIS12.¬φTESIS1EVOCACION(1)3.(¬φ→¬φ)CONCLUSION4.(φ∨¬φ)DISJUNCIONINTRODUCCION(3) Cualesquiera sea la sentencias φ de tipo τ se tiene que ¬(φ∧¬φ) es un teorema de (∅,τ). Una prueba formal: 1.(φ∧¬φ)HIPOTESIS12.(φ∧¬φ)TESIS1EVOCACION(1)3.((φ∧¬φ)→(φ∧¬φ))CONCLUSION4.¬(φ∧¬φ)ABSURDO(3) Cualesquiera sean las sentencias φ1 y φ2 de tipo τ se tiene que ((φ1∨φ2)→(φ2∨φ1)) es un teorema de (∅,τ). Una prueba formal: 1.(φ1∨φ2)HIPOTESIS12.φ1HIPOTESIS23.(φ2∨φ1)TESIS2DISJUNCIONINTRODUCCION(2)4.(φ1→(φ2∨φ1))CONCLUSION5.φ2HIPOTESIS36.(φ2∨φ1)TESIS3DISJUNCIONINTRODUCCION(5)7.φ2→(φ2∨φ1)CONCLUSION8.(φ2∨φ1)TESIS1DIVISIONPORCASOS(1,4,7)9.((φ1∨φ2)→(φ2∨φ1))CONCLUSION
- Cualesquiera sean las sentencias φ1,φ2,φ3 de tipo τ se tiene que ((φ1∨(φ2∨φ3))→((φ1∨φ2)∨φ3)) es un teorema de (∅,τ). Una prueba formal: 1.(φ1∨(φ2∨φ3))HIPOTESIS12.φ1HIPOTESIS23.(φ1∨φ2)DISJUNCIONINTRODUCCION(2)4.((φ1∨φ2)∨φ3)TESIS2DISJUNCIONINTRODUCCION(3)5.(φ1→((φ1∨φ2)∨φ3))CONCLUSION6.(φ2∨φ3)HIPOTESIS37.φ2HIPOTESIS48.(φ1∨φ2)DISJUNCIONINTRODUCCION(7)9.((φ1∨φ2)∨φ3)TESIS4DISJUNCIONINTRODUCCION(8)10.(φ2→((φ1∨φ2)∨φ3))CONCLUSION11.φ3HIPOTESIS512.((φ1∨φ2)∨φ3)TESIS5DISJUNCIONINTRODUCCION(11)13.(φ3→((φ1∨φ2)∨φ3))CONCLUSION14.((φ1∨φ2)∨φ3)TESIS3DIVISIONPORCASOS(6,10,13)15.((φ2∨φ3)→((φ1∨φ2)∨φ3))CONCLUSION16.((φ1∨φ2)∨φ3)TESIS1DIVISIONPORCASOS(1,5,15)17.((φ1∨(φ2∨φ3))→((φ1∨φ2)∨φ3))CONCLUSION
- Cualesquiera sean las sentencias φ y ψ la sentencia ((φ∧(φ∨ψ))↔φ) es un teorema de (∅,τ). Una prueba formal: 1.(φ∧(φ∨ψ))HIPOTESIS12.φTESIS1CONJUNCIONELIMINACION(1)3.((φ∧(φ∨ψ))→φ)CONCLUSION4.φHIPOTESIS25.(φ∨ψ)DISJUNCIONINTRODUCCION(4)6.(φ∧(φ∨ψ))TESIS2CONJUNCIONINTRODUCCION(4,5)7.(φ→(φ∧(φ∨ψ)))CONCLUSION8.((φ∧(φ∨ψ))↔φ)EQUIVALENCIAINTRODUCCION(3,7)
- Cualesquiera sean las sentencias φ y ψ la sentencia ((φ∨(φ∧ψ))↔φ) es un teorema de (∅,τ). Una prueba formal: 1.(φ∨(φ∧ψ))HIPOTESIS12.φHIPOTESIS23.φTESIS2EVOCACION(2)4.(φ→φ)CONCLUSION5.(φ∧ψ)HIPOTESIS36.φTESIS3CONJUNCIONELIMINACION(5)7.((φ∧ψ)→φ)CONCLUSION8.φTESIS1DIVISIONPORCASOS(1,4,7)9.((φ∨(φ∧ψ))→φ)CONCLUSION10.φHIPOTESIS411.(φ∨(φ∧ψ))TESIS4DISJUNCIONINTRODUCCION(10)12.(φ→(φ∨(φ∧ψ)))CONCLUSION13.((φ∨(φ∧ψ))↔φ)EQUIVALENCIAINTRODUCCION(9,12)
- Cualesquiera sean las sentencias φ1,φ2 y φ la sentencia ((φ∧(φ1∨φ2))→((φ∧φ1)∨(φ∧φ2))) es un teorema de (∅,τ). Una prueba formal: 1.(φ∧(φ1∨φ2))HIPOTESIS12.φCONJUNCIONELIMINACION(1)3.(φ1∨φ2)CONJUNCIONELIMINACION(1)4.φ1HIPOTESIS25.(φ∧φ1)CONJUNCIONINTRODUCCION(2,4)6.((φ∧φ1)∨(φ∧φ2))TESIS2DISJUNCIONINTRODUCCION(5)7.(φ1→((φ∧φ1)∨(φ∧φ2)))CONCLUSION8.φ2HIPOTESIS39.(φ∧φ2)CONJUNCIONINTRODUCCION(2,8)10.((φ∧φ1)∨(φ∧φ2))TESIS3DISJUNCIONINTRODUCCION(9)11.(φ2→((φ∧φ1)∨(φ∧φ2)))CONCLUSION12.((φ∧φ1)∨(φ∧φ2))TESIS1DIVISIONPORCASOS(3,7,11)13.((φ∧(φ1∨φ2))→((φ∧φ1)∨(φ∧φ2)))CONCLUSION
- Cualesquiera sean las sentencias φ1,φ2 y φ la sentencia (((φ∧φ1)∨(φ∧φ2))→(φ∧(φ1∨φ2))) es un teorema de (∅,τ). Una prueba formal: 1.((φ∧φ1)∨(φ∧φ2))HIPOTESIS12.(φ∧φ1)HIPOTESIS23.φCONJUNCIONELIMINACION(2)4.φ1CONJUNCIONELIMINACION(2)5.(φ1∨φ2)DISJUNCIONINTRODUCCION(4)6.(φ∧(φ1∨φ2))TESIS2CONJUNCIONINTRODUCCION(3,5)7.((φ∧φ1)→(φ∧(φ1∨φ2)))CONCLUSION8.(φ∧φ2)HIPOTESIS39.φCONJUNCIONELIMINACION(8)10.φ2CONJUNCIONELIMINACION(8)11.(φ1∨φ2)DISJUNCIONINTRODUCCION(10)12.(φ∧(φ1∨φ2))TESIS3CONJUNCIONINTRODUCCION(9,11)13.((φ∧φ2)→(φ∧(φ1∨φ2)))CONCLUSION14.(φ∧(φ1∨φ2))TESIS1DIVISIONPORCASOS(1,7,13)15.(((φ∧φ1)∨(φ∧φ2))→(φ∧(φ1∨φ2)))CONCLUSION
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:
Consejos importantes: Por favor contengan a su escarabajo interior...
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.
Una buena manera de hacer una prueba elemental de una sentencia elemental pura φ 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,s,i,≤) fijo (pero arbitrario) e intentar (como matematicos) probar que entonces en (L,s,i,≤) se cumple φ. 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.
Es decir debemos ser el mismo matematico de siempre solo que haciendo pruebas de un estilo muy particular.
Ademas es un sano consejo que cuando hagamos la prueba matematica y tambien la elemental, no llenemos de “basura logica”. Es decir, debemos ser fieles a que en tales pruebas nuestro roll es el de un matematico comun y corriente (que hasta podria odiar la logica como disciplina!) por lo cual no tiene sentido ahi hacer referencia a las reglas y mecanicas que constituyen una prueba formal. Por ejemplo poner en la prueba matematica o en la prueba elemental: Por Modus Ponens se tiene que....., es obviamente algo que un matematico no haria! Otro ejemplo: Usar ≡ en lugar del =. Es decir todas estas cosas distraen y nos alejan de las ideas (por eso enojan en algun sentido a los matematicos) en momentos donde la concentracion e imaginacion matematicas son cruciales. Consejo: guarde para la prueba formal todos esos impulsos.
Cabe destacar que dar una prueba formal concreta no es ni mas ni menos que dar una formalizacion matematicamente perfecta de la matematica informal existente en la respectiva prueba elemental. Es decir estamos formalizando “porciones de matematica real”.
Ejercicio: De una prueba formal de ∀x1(s(x1,x1)≡x1) en RetCua
Ejercicio: De una prueba formal de ∀x1∀x2(s(x1,x2)≡s(x2,x1)) en RetCua
Ejercicio: De una prueba formal de ∀x1∀x2(i(s(x1,x2),x1)≡x1) en RetCua
Ejercicio: De una prueba formal de ∀x1∀x2(≤(x1,x2)↔(s(x1,x2)≡x2)) en RetCua
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 y para cada caso daremos la forma en la que podemos “copiar” esto dentro de una prueba formal.
Es muy comun que el matematico deduzca la sentencia ψ a partir de sentencias (φ↔ψ) y φ. Esto formalmente se puede hacer exactamente igual ya que ψ se deduce por la regla de reemplazo de (φ↔ψ) y φ (es justo el caso n=0 y γ=φ).
Cuando un matematico en el contexto de una prueba intenta probar una sentencia de la forma (φ→ψ) suele asumir como hipotesis φ, luego sigue razonando y prueba ψ para entonces concluir que vale (φ→ψ). Esto formalmente lo podemos hacer de la misma manera: ⋮⋮⋮k.φHIPOTESIS1⋮⋮⋮j.ψTESIS1...j+1.(φ→ψ)CONCLUSION⋮⋮⋮
Cuando un matematico en el contexto de una prueba intenta probar una sentencia de la forma (φ∨ψ) suele probar (¬φ→ψ) y entonces concluir que vale (φ∨ψ). Esto claramente puede emularse en nuestras pruebas formales usando la regla de disjuncion-introduccion (caso 3)
Cuando un matematico en el contexto de una prueba intenta probar una sentencia de la forma (φ↔ψ) suele probar (φ→ψ) y (ψ→φ) y entonces concluir que vale (φ↔ψ). Esto claramente puede emularse en nuestras pruebas formales usando la regla de equivalencia-introduccion
Cuando un matematico ya sabe que es cierta una disjuncion (φ∨ψ) e intenta probar una sentencia γ suele probar (φ→γ) y (ψ→γ) y entonces concluir que vale γ. Esto claramente puede emularse en nuestras pruebas formales usando la regla de division por casos
Cuando un matematico intenta probar una sentencia por el absurdo asume su negacion pero muchas veces se saltea un paso y pone directamente algo equivalente a la negacion de dicha sentencia. Por ejemplo: El matematico va a probar por el absurdo una sentencia de la forma (φ∨ψ). Para esto asume (¬φ∧¬ψ) y luego de cierto razonamiento llega a una contradiccion de la forma (γ∧¬γ). Concluye entonces (φ∨ψ). Formalmente haremos: 1.¬(φ∨ψ)HIPOTESIS12.(¬(φ∨ψ)↔(¬φ∧¬ψ))AXIOMALOGICO3.(¬φ∧¬ψ)REEMPLAZO(1,2)⋮⋮⋮k.(γ∧¬γ)TESIS1...k+1.(¬(φ∨ψ)→(γ∧¬γ))CONCLUSIONk+2.(φ∨ψ)ABSURDO(k+1) Es decir hacemos exactamente lo mismo pero sin saltearnos el paso de negar la sentencia que queremos probar (i.e. (φ∨ψ)). Otro ejemplo: El matematico va a probar por el absurdo una sentencia de la forma ∀vφ. Para esto asume ∃v¬φ(v) y luego de cierto razonamiento llega a una contradiccion de la forma (γ∧¬γ). Concluye entonces ∀vφ(v). Formalmente haremos: 1.¬∀vφHIPOTESIS12.(¬∀vφ↔∃v¬φ)AXIOMALOGICO3.∃v¬φREEMPLAZO(1,2)⋮⋮⋮k.(γ∧¬γ)TESIS1...k+1.(¬∀vφ→(γ∧¬γ))CONCLUSIONk+2.∀vφABSURDO(k+1) Un ultimo ejemplo: El matematico va a probar por el absurdo una sentencia de la forma (φ→ψ). Para esto asume (φ∧¬ψ) y luego de cierto razonamiento llega a una contradiccion de la forma (γ∧¬γ). Concluye entonces (φ→ψ). Formalmente haremos: 1.¬(φ→ψ)HIPOTESIS12.(¬(φ→ψ)↔(φ∧¬ψ))AXIOMALOGICO3.(φ∧¬ψ)REEMPLAZO(1,2)⋮⋮⋮k.(γ∧¬γ)TESIS1...k+1.(¬(φ→ψ)→(γ∧¬γ))CONCLUSIONk+2.(φ→ψ)ABSURDO(k+1) Notese que este tipo de situaciones se dan para los 7 distintos tipos de formulas no atomicas dados en el Lema Menu de Formulas. En cada caso para formalizar usamos el respectivo axioma esquema de negacion junto con la regla de reemplazo. Dejamos al lector hacer lo mismo con los conectivos restantes (i.e. ∧,↔,¬,∃).
Si bien acabamos de dar muchas mecanicas de deduccion, cabe destacar que han sido dadas para mostrar como emular a los matematicos en determinadas situaciones cotidianas y no para que el alumno suelte a su escarabajo y que cuando intente dar una prueba formal se saltee la prueba matematica, se olvide de su roll matematico y se dedique a aplicar estas reglas mecanicamente sin pensar!!! Es decir, es importante que se olvide de estas mecanicas (y de todas las baratijas logicas) y primero intente dar una prueba como matematico, luego tunee esta prueba a una elemental y recien cuando empiece a traducir esta prueba elemental a una formal se fije en como estas mecanicas ayudan a emular ciertas partes de la prueba matematica.
Ya que nuestra definicion de prueba formal esta hecha intentando que las pruebas (elementales) hechas por un matematico sean traducibles a una formal de la forma mas natural posible, muchas veces habra “redundancia deductiva”. Algunos ejemplos de redundancia deductiva:
- Se podran probar algunos axiomas logicos usando solo los otros, es decir algunos axiomas logicos podrian sacarse y el concepto de prueba resultante tendria la misma “potencia” (i.e. se podrian seguir probando los mismos teoremas). Por ejemplo el lector no tendra problemas en dar una prueba de (¬∃vφ↔∀v¬φ) (por supuesto sin usarlo a el como axioma). Sin envargo se lo incluye como axioma dado que interviene naturalmente cuando un matematico quiere probar por el absurdo una sentencia de la forma ∃vφ (ver arriva en Mecanicas de negacion)
- Muchas de las reglas podrian sacarse y se podrian seguir probando los mismos teoremas, por ejemplo la regla de eleccion.
De todas maneras esta redundancia es anecdotica ya que lo importante es que nuestro concepto de prueba formal sea un modelo lo mas natural posible. Cuando quitamos redundancia puede volverse muy ingenioso probar alguna sentencia obviamente cierta. Veamos un ejemplo: Sea φ=dφ(v) una formula de tipo τ. Ya que (¬∀vφ↔∃v¬φ) es un axioma logico, tenemos que ((¬∀vφ↔∃v¬φ),AXIOMALOGICO) es una prueba formal de (¬∀vφ↔∃v¬φ) en la teoria (∅,τ). A continuacion se da una prueba formal en la teoria (∅,τ) de la sentencia (¬∀vφ↔∃v¬φ) la cual no usa el hecho de que (¬∀vφ↔∃v¬φ) sea un axioma logico. Notar que en las primeras 10 lineas se prueba (¬∃v¬φ→¬¬∀vφ), es decir el contraresiproco de (¬∀vφ→∃v¬φ). De la linea 11 hasta la 17 se prueba (¬∀vφ→∃v¬φ). En las lineas restantes se prueba la implicacion reciproca de (¬∀vφ→∃v¬φ), es decir (∃v¬φ→¬∀vφ) y en el ultimo paso se obtiene (¬∀vφ↔∃v¬φ) por la regla de equivalencia-introduccion. Cabe observar que esta prueba formal no es natural u obvia, mas bien es dificil de encontrar. 1.¬∃v¬φHIPOTESIS12.¬φ(c)HIPOTESIS23.∃v¬φEXISTENCIAL(2)4.(∃v¬φ∧¬∃v¬φ)TESIS2CONJUNCIONINTRODUCCION(3,1)5.¬φ(c)→(∃v¬φ∧¬∃v¬φ)CONCLUSION6.φ(c)ABSURDO(5)7.∀vφGENERALIZACION(6)8.(∀vφ↔¬¬∀vφ)AXIOMALOGICO9.¬¬∀vφTESIS1REEMPLAZO(7,8)10.(¬∃v¬φ→¬¬∀vφ)CONCLUSION11.¬∀vφHIPOTESIS312.¬∃v¬φHIPOTESIS413.¬¬∀vφMODUSPONENS(12,10)14.(¬∀vφ∧¬¬∀vφ)TESIS4CONJUNCIONINTRODUCCION(11,13)15.¬∃v¬φ→(¬∀vφ∧¬¬∀vφ)CONCLUSION16.∃v¬φTESIS3ABSURDO(15)17.(¬∀vφ→∃v¬φ)CONCLUSION18.∃v¬φHIPOTESIS519.¬φ(e)ELECCION(18)20.∀vφHIPOTESIS621.φ(e)PARTICULARIZACION(20)22.(φ(e)∧¬φ(e))TESIS6CONJUNCIONINTRODUCCION(21,19)23.∀vφ→(φ(e)∧¬φ(e))CONCLUSION24.¬∀vφTESIS5ABSURDO(23)25.(∃v¬φ→¬∀vφ)CONCLUSION26.(¬∀vφ↔∃v¬φ)EQUIVALENCIAINTRODUCCION(17,25)
Como detalle sorprendente de cuanto mas minimal se puede hacer la definicion de prueba, el concepto de prueba dado en el libro de Mendelson, Introduction to mathematical logic (sexta edicion) solo usa cinco axiomas esquema y dos reglas, (Modus Ponens y generalizacion) y prueba los mismos teoremas que el nuestro ya que tambien en dicho texto se prueba el Teorema de Completitud relativo a tal definicion de prueba. Por supuesto esta simplificacion del concepto de prueba hace mucho mas dificil y tecnico el desarrollo.
Por supuesto los numeros asociados a las hipotesis en una prueba son completamente arbitrarios y pueden cambiarse, es decir:
7.35 (Cambio de indice de hipotesis). Sea (φ,J) una prueba formal de φ en (Σ,τ). Sea m∈N tal que Ji≠ HIPOTESISˉm, para cada i=1,...,n(φ). Supongamos que Ji= HIPOTESISˉk y que Jj= TESISˉkα, con [α]1∉Num. Sea ˜J el resultado de reemplazar en J la justificacion Ji por HIPOTESISˉm y reemplazar la justificacion Jj por TESISˉmα. Entonces (φ,˜J) es una prueba formal de φ en (Σ,τ).
Proof. Es un chequeo largo pero trivial.
Tambien podemos cambiar los nombres de cte auxiliares
7.36 (Cambio de nombres de constante auxiliares). Sea (φ,J) una prueba formal de φ en (Σ,τ). Sea C1 el conjunto de nombres de constante auxiliares de (φ,J). Sea e∈C1. Sea ˜e∉C∪C1 tal que (C∪(C1−{e})∪{˜e},F,R,a) es un tipo. Sea ˜φi= resultado de reemplazar en φi cada ocurrencia de e por ˜e. Entonces (˜φ1...˜φn(φ),J) es una prueba formal de φ en (Σ,τ).
Proof. Sean τ1=(C∪C1,F,R,a)τ2=(C∪(C1−{e})∪{˜e},F,R,a) Para cada c∈C∪(C1−{e}) definamos ˜c=c. Notese que el mapeo c→˜c es una biyeccion entre el conjunto de nombres de constante de τ1 y el conjunto de nombres de cte de τ2. Para cada t∈Tτ1 sea ˜t= resultado de reemplazar en t cada ocurrencia de c por ˜c, para cada c∈C∪C1. Analogamente para una formula ψ∈Fτ1, sea ˜ψ= resultado de reemplazar en ψ cada ocurrencia de c por ˜c, para cada c∈C∪C1. Notese que los mapeos t→˜t y ψ→˜ψ son biyecciones naturales entre Tτ1 y Tτ2 y entre Fτ1 y Fτ2, respectivamente. Notese que cualesquiera sean ψ1,ψ2∈Fτ1, tenemos que ψ1 se deduce de ψ2 por la regla de generalizacion con constante c sii ˜ψ1 se deduce de ˜ψ2 por la regla de generalizacion con constante ˜c. Para las otras reglas sucede lo mismo. Notese tambien que c ocurre en ψ sii ˜c ocurre en ˜ψ. Mas aun notese que c depende de d en (φ,J) sii ˜c depende de ˜d en (˜φ,J), donde ˜φ=~φ1...~φn(φ). Ahora es facil chequear que (˜φ,J) es una prueba formal de φ en (Σ,τ) basandose en que (φ,J) es una prueba formal de φ en (Σ,τ).
7.37 (Propiedades basicas de ⊢). Sea (Σ,τ) una teoria.
(1) (Uso de Teoremas) Si (Σ,τ)⊢φ1,...,φn y (Σ∪{φ1,...,φn},τ)⊢φ, entonces (Σ,τ)⊢φ.
(2) Supongamos (Σ,τ)⊢φ1,...,φn. Si R es una regla distinta de GENERALIZACION y ELECCION y φ se deduce de φ1,...,φn por la regla R, entonces (Σ,τ)⊢φ.
(3) (Σ,τ)⊢(φ→ψ) si y solo si (Σ∪{φ},τ)⊢ψ.
Proof. (1) Notese que basta con hacer el caso n=1. El caso con n≥2 se obtiene aplicando n veces el caso n=1. Supongamos entonces que (Σ,τ)⊢φ1 y (Σ∪{φ1},τ)⊢φ. Sea (α1...αh,I1...Ih) una prueba formal de φ1 en (Σ,τ). Sea (ψ1...ψm,J1...Jm) una prueba formal de φ en (Σ∪{φ1},τ). Notese que por los Lemas 7.35 y 7.36 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 ~Ji de la siguiente manera.
- Si Ji=αAXIOMAPROPIO, con α∈{ε}∪{TESISˉk:k∈N} y ψi=φ1, entonces ~Ji=αEVOCACION(¯h)
- Si Ji=αAXIOMAPROPIO, con α∈{ε}∪{TESISˉk:k∈N} y ψi∉{φ1}, entonces ~Ji=αAXIOMAPROPIO.
- Si Ji=αAXIOMALOGICO, con α∈{ε}∪{TESISˉk:k∈N}, entonces ~Ji=αAXIOMALOGICO
- Si Ji=αCONCLUSION, con α∈{ε}∪{TESISˉk:k∈N}, entonces ~Ji=αCONCLUSION.
- Si Ji=HIPOTESISˉk, entonces ~Ji=HIPOTESISˉk
- Si Ji=αR(¯l1,...,¯lk), con α∈{ε}∪{TESISˉk:k∈N}, entonces ~Ji=αR(¯l1+h,...,¯lk+h)
Es facil chequear que (α1...αhψ1...ψm,I1...Ih~J1...~Jm) es una prueba formal de φ en (Σ,τ)
(2) Notese que 1.φ1AXIOMAPROPIO2.φ2AXIOMAPROPIO⋮⋮⋮n.φnAXIOMAPROPIOn+1.φR(ˉ1,...,ˉn) es una prueba formal de φ en (Σ∪{φ1,...,φn},τ), lo cual por (1) nos dice que (Σ,τ)⊢φ.
(3) Supongamos (Σ,τ)⊢(φ→ψ). Entonces tenemos que (Σ∪{φ},τ)⊢(φ→ψ),φ, lo cual por (2) nos dice que (Σ∪{φ},τ)⊢ψ. Supongamos ahora que (Σ∪{φ},τ)⊢ψ. Sea (φ1...φn,J1...,Jn) una prueba formal de ψ en (Σ∪{φ},τ). Para cada i=1,...,n, definamos ~Ji de la siguiente manera.
- Si φi=φ y Ji=αAXIOMAPROPIO, con α∈{ε}∪{TESISˉk:k∈N}, entonces ~Ji=αEVOCACION(1)
- Si φi≠φ y Ji=αAXIOMAPROPIO, con α∈{ε}∪{TESISˉk:k∈N}, entonces ~Ji=αAXIOMAPROPIO
- Si Ji=αAXIOMALOGICO, con α∈{ε}∪{TESISˉk:k∈N}, entonces ~Ji=αAXIOMALOGICO
- Si Ji=αCONCLUSION, con α∈{ε}∪{TESISˉk:k∈N}, entonces ~Ji=αCONCLUSION
- Si Ji=HIPOTESISˉk, entonces ~Ji=HIPOTESISˉk
- Si Ji=αR(¯l1,...,¯lk), con α∈{ε}∪{TESISˉk:k∈N}, entonces ~Ji=αR(¯l1+1,...,¯lk+1)
Sea m tal que ninguna Ji es igual a HIPOTESISˉm. Notese que ~Jn no es de la forma TESISˉkβ ni de la forma HIPOTESISˉk (por que?) por lo cual TESISˉm~Jn es una justificacion. Es facil chequear que (φφ1...φn(φ→ψ),HIPOTESISˉm~J1...~Jn−1TESISˉm~JnCONCLUSION) es una prueba formal de (φ→ψ) en (Σ,τ)
Una teoria (Σ,τ) sera inconsistente cuando haya una sentencia φ tal que (Σ,τ)⊢(φ∧¬φ). Una teoria (Σ,τ) sera consistente cuando no sea inconsistente.
7.38 (Propiedades basicas de la consistencia). Sea (Σ,τ) una teoria.
(1) Si (Σ,τ) es inconsistente, entonces (Σ,τ)⊢φ, para toda sentencia φ.
(2) Si (Σ,τ) es consistente y (Σ,τ)⊢φ, entonces (Σ∪{φ},τ) es consistente.
(3) Si (Σ,τ)⊬, entonces (\Sigma\cup\{\varphi\},\tau) es consistente.
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.37 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.37 nos diria que (\Sigma,\tau)\vdash\psi\wedge\lnot\psi, es decir nos diria que (\Sigma,\tau) es inconsistente.
(3) es dejada al lector.
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).
7.6 (Teorema de Correccion). (\Sigma,\tau)\vdash\varphi implica (\Sigma,\tau)\models\varphi.
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.
7.3. Si (\Sigma,\tau) tiene un modelo, entonces (\Sigma,\tau) es consistente.
Proof. Supongamos \mathbf{A} es un modelo de (\Sigma,\tau). Si (\Sigma,\tau) fuera inconsistente, entonces toda sentencia de tipo \tau seria un teorema de (\Sigma,\tau), en particular tendriamos que \exists x_{1}\lnot(x_{1}\equiv x_{1}) seria un teorema de (\Sigma,\tau), lo cual por el Teorema de Correccion nos diria que \mathbf{A}\models\exists x_{1}\lnot(x_{1}\equiv x_{1}), lo cual no es cierto. O sea que (\Sigma,\tau) es consistente
El Teorema de Correccion es muy util para asegurar que una sentencia no es un teorema de una teoria dada. Mas concretamente tenemos el siguiente criterio:
NoEsTeorema 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.
Dejamos al lector justificar este criterio usando el Teorema de Correccion. Podemos usarlo, por ejemplo, para ver que ni la sentencia Dis_{1}=\forall x_{1}\forall x_{2}(\mathsf{i}(x_{1},\mathsf{s}(x_{2},x_{3}))\equiv\mathsf{s}(\mathsf{i}(x_{1},x_{2}),\mathsf{i}(x_{1},x_{3}))) ni su negacion son teoremas de RetCua 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, es decir ya no vale el Teorema de Correccion.
Ejemplo 1: 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.
Ejemplo 2: 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.
Ejemplo 3: 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}
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)\}
7.39. \dashv\vdash_{T} es una relacion de equivalencia.
Proof. La relacion es reflexiva ya que cualquiera sea la \varphi\in S^{\tau} tenemos que \begin{array}{llll} 1. & \varphi & & \text{HIPOTESIS}1\\ 2. & \varphi & & \text{TESIS}1\text{EVOCACION}(1)\\ 3. & (\varphi\rightarrow\varphi) & & \text{CONCLUSION}\\ 4. & (\varphi\rightarrow\varphi) & & \text{EVOCACION}(3)\\ 5. & (\varphi\leftrightarrow\varphi) & & \text{EQUIVALENCIAINTRODUCCION}(3,4) \end{array} es una prueba formal de ((\varphi\leftrightarrow\varphi) en T. Veamos que es 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.37 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.
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}. Una sentencia \varphi se dice refutable en T si T\vdash\lnot\varphi.
7.40. Dada una teoria T=(\Sigma,\tau), se tiene que:
(1) [\forall x_{1}(x_{1}\equiv x_{1})]_{T}=\{\varphi\in S^{\tau}:\varphi\text{ es un teorema de \ensuremath{T}}\}
(2) [\exists x_{1}\neg(x_{1}\equiv x_{1})]_{T}=\{\varphi\in S^{\tau}:\varphi\text{ es refutable en \ensuremath{T}}\}
Proof. Haremos la prueba de (2) y dejaremos la prueba de (1) como ejercicio. Notese que \exists x_{1}\neg(x_{1}\equiv x_{1}) es refutable en T ya que \begin{array}{llll} 1.\; & \exists x_{1}\neg(x_{1}\equiv x_{1}) & & \text{HIPOTESIS1}\\ 2.\; & \neg(e\equiv e) & & \text{ELECCION\ensuremath{(1)}}\\ 3.\; & (e\equiv e) & & \text{AXIOMALOGICO}\\ 4.\; & ((e\equiv e)\wedge\neg(e\equiv e)) & & \text{TESIS1CONJUNCIONINTRODUCCION}(3,2)\\ 5.\; & (\exists x_{1}\neg(x_{1}\equiv x_{1})\rightarrow((e\equiv e)\wedge\neg(e\equiv e))) & & \text{CONCLUSION}\\ 6.\; & \neg\exists x_{1}\neg(x_{1}\equiv x_{1}) & & \text{ABSURDO\ensuremath{(5)}} \end{array} es una prueba de \neg\exists x_{1}\neg(x_{1}\equiv x_{1}) en T. Ahora veamos que si \varphi es refutable en T y \varphi\dashv\vdash_{T}\psi, entonces \psi es refutable en T. Notese que \begin{array}{llll} 1.\; & \lnot\varphi & & \text{AXIOMAPROPIO}\\ 2.\; & (\varphi\leftrightarrow\psi) & & \text{AXIOMAPROPIO}\\ 3.\; & \lnot\psi & & \text{REEMPLAZO}(2,1) \end{array} es una prueba de \lnot\psi en (\Sigma\cup\{\lnot\varphi,(\varphi\leftrightarrow\psi)\},\tau), lo cual por (1) del Lema 7.37 nos dice que \psi es refutable en T. Ya que \exists x_{1}\neg(x_{1}\equiv x_{1}) es refutable en T, lo anterior nos dice que [\exists x_{1}\neg(x_{1}\equiv x_{1})]_{T}\subseteq\{\varphi\in S^{\tau}:\varphi\text{ es refutable en \ensuremath{T}}\} Para terminar la prueba de (2) notese que basta con probar que si \varphi\text{ y }\psi son refutables en T, entonces \varphi\dashv\vdash_{T}\psi. Pero \begin{array}{llll} 1.\; & \varphi & & \text{HIPOTESIS}1\\ 2.\; & \lnot\varphi & & \text{AXIOMAPROPIO}\\ 3.\; & (\varphi\wedge\lnot\varphi) & & \text{CONJUNCIONINTRODUCCION}(1,3)\\ 4. & \psi & & \text{TESIS}1\text{ABSURDO}(3)\\ 5. & (\varphi\rightarrow\psi) & & \text{CONCLUSION}\\ 6. & \psi & & \text{HIPOTESIS}2\\ 7. & \lnot\psi & & \text{AXIOMAPROPIO}\\ 8. & (\psi\wedge\lnot\psi) & & \text{CONJUNCIONINTRODUCCION}(6,7)\\ 9. & \varphi & & \text{TESIS}2\text{ABSURDO}(8)\\ 10. & (\psi\rightarrow\varphi) & & \text{CONCLUSION}\\ 11. & (\varphi\leftrightarrow\psi) & & \text{EQUIVALENCIAINTRODUCCION}(5,10) \end{array} justifica que (\Sigma\cup\{\lnot\varphi,\lnot\psi\},\tau)\vdash(\varphi\leftrightarrow\psi) por lo cual si \varphi\text{ y }\psi son refutables en T, se puede aplicar (1) del Lema 7.37 y obtener que \varphi\dashv\vdash_{T}\psi.
Definiremos sobre S^{\tau}/\mathrm{\dashv\vdash}_{T} la 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
- Si [\varphi]_{T}=[\varphi^{\prime}]_{T} y [\psi]_{T}=[\psi^{\prime}]_{T} entonces [(\varphi\vee\psi)]_{T}=[(\varphi^{\prime}\vee\psi^{\prime})]_{T}
Es decir debemos probar que si T\vdash\left(\varphi\leftrightarrow\varphi^{\prime}\right) y T\vdash\left(\psi\leftrightarrow\psi^{\prime}\right), entonces T\vdash((\varphi\vee\psi)\leftrightarrow(\varphi^{\prime}\vee\psi^{\prime})). Supongamos que T\vdash\left(\varphi\leftrightarrow\varphi^{\prime}\right) y T\vdash\left(\psi\leftrightarrow\psi^{\prime}\right). Notese que tambien T\vdash((\varphi\vee\psi)\leftrightarrow(\varphi\vee\psi)) (ya probamos que \dashv\vdash_{T} es reflexiva). Ademas tenemos que \begin{array}{llll} 1.\; & \left(\varphi\leftrightarrow\varphi^{\prime}\right) & & \text{AXIOMAPROPIO}\\ 2.\; & \left(\psi\leftrightarrow\psi^{\prime}\right) & & \text{AXIOMAPROPIO}\\ 3.\; & ((\varphi\vee\psi)\leftrightarrow(\varphi\vee\psi)) & & \text{AXIOMALOGICO}\\ 4.\; & ((\varphi\vee\psi)\leftrightarrow(\varphi^{\prime}\vee\psi)) & & \text{REEMPLAZO}(1,3)\\ 5.\; & ((\varphi\vee\psi)\leftrightarrow(\varphi^{\prime}\vee\psi^{\prime})) & & \text{REEMPLAZO}(2,4) \end{array} atestigua que (\Sigma\cup\{\left(\varphi\leftrightarrow\varphi^{\prime}\right),\left(\psi\leftrightarrow\psi^{\prime}\right),((\varphi\vee\psi)\leftrightarrow(\varphi\vee\psi))\},\tau)\vdash((\varphi\vee\psi)\leftrightarrow(\varphi^{\prime}\vee\psi^{\prime})) lo cual nos dice por (1) del Lema 7.37 que T\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.
7.7. Sea T=(\Sigma,\tau) una teoria. Entonces (S^{\tau}/\mathrm{\dashv\vdash}_{T},\mathsf{s}^{T},\mathsf{i}^{T},^{\mathsf{c}^{T}},0^{T},1^{T}) es un algebra de Boole.
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) [\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{1}]_{T}=[\varphi_{1}]_{T}
(2) [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{1}]_{T}=[\varphi_{1}]_{T}
(3) [\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{2}]_{T}=[\varphi_{2}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{1}]_{T}
(4) [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{2}]_{T}=[\varphi_{2}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{1}]_{T}
(5) [\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) [\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) [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{2}]_{T})=[\varphi_{1}]_{T}
(8) [\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{2}]_{T})=[\varphi_{1}]_{T}
(9) 0^{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{1}]_{T}=[\varphi_{1}]_{T}
(10) [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}1^{T}=1^{T}
(11) [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}([\varphi_{1}]_{T})^{\mathsf{c}^{T}}=1^{T}
(12) [\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}([\varphi_{1}]_{T})^{\mathsf{c}^{T}}=0^{T}
(13) [\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}([\varphi_{2}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T})=([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{2}]_{T})\;\mathsf{s}^{T}\mathsf{\;}([\varphi_{1}]_{T}\;\mathsf{i}^{T}\mathsf{\;}[\varphi_{3}]_{T})
Veamos por ejemplo que se da (10), es decir probaremos que [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}1^{T}=1^{T}, cualesquiera sea la sentencia \varphi_{1}. Por el Lema 7.40 debemos probar que para cualquier \varphi_{1}\in S^{\tau}, se da que [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\forall x_{1}(x_{1}\equiv x_{1})]_{T}=[\forall x_{1}(x_{1}\equiv x_{1})]_{T} Ya que [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\forall x_{1}(x_{1}\equiv x_{1})]_{T}=[(\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1}))]_{T}, debemos probar que [(\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1}))]_{T}=[\forall x_{1}(x_{1}\equiv x_{1})]_{T} o equivalentemente T\vdash((\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1}))\leftrightarrow\forall x_{1}(x_{1}\equiv x_{1})) Notese que por (2) del Lema 7.37, basta con probar que \begin{aligned} T & \vdash((\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1}))\rightarrow\forall x_{1}(x_{1}\equiv x_{1}))\\ T & \vdash(\forall x_{1}(x_{1}\equiv x_{1})\rightarrow(\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1}))) \end{aligned} Dejamos la segunda al lector. Para la primera tenemos la siguiente prueba formal \begin{array}{llll} 1.\; & c\equiv c & & \text{AXIOMALOGICO}\\ 2.\; & \forall x_{1}(x_{1}\equiv x_{1}) & & \text{GENERALIZACION}(1)\\ 3. & (\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1})) & & \text{HIPOTESIS1}\\ 4. & \forall x_{1}(x_{1}\equiv x_{1}) & & \text{TESIS1EVOCACION}\text{(2)}\\ 5. & ((\varphi_{1}\vee\forall x_{1}(x_{1}\equiv x_{1}))\rightarrow\forall x_{1}(x_{1}\equiv x_{1})) & & \text{CONCLUSION} \end{array} (c es un nombre de cte no perteneciente a \mathcal{C} y tal que (\mathcal{C}\cup\{c\},\mathcal{F},\mathcal{R},a) es un tipo).
Veamos ahora que se da (6), es decir veamos que [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}([\varphi_{2}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T})=([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{2}]_{T})\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T} cualesquiera sean \varphi_{1},\varphi_{2},\varphi_{3}\in S^{\tau}. Sean \varphi_{1},\varphi_{2},\varphi_{3}\in S^{\tau} fijas. Por la definicion de la operacion \mathsf{s}^{T} tenemos que \begin{array}{llll} [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}([\varphi_{2}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T}) & = & [\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[(\varphi_{2}\vee\varphi_{3})]_{T}\\ & = & [(\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3}))]_{T}\\ \\([\varphi_{1}]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{2}]_{T})\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T} & = & [(\varphi_{1}\vee\varphi_{2})]_{T}\;\mathsf{s}^{T}\mathsf{\;}[\varphi_{3}]_{T}\\ & = & [((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3})]_{T} \end{array} O sea que debemos probar que [(\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3}))]_{T}=[((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3})]_{T} es decir, debemos probar que T\vdash((\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3}))\leftrightarrow((\varphi_{1}\vee\varphi_{2})\vee\varphi_{3})) Notese que por (2) del Lema 7.37, 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}.
7.41. Sea T una teoria. Se tiene que [\varphi]_{T}\leq^{T}[\psi]_{T}\text{ si y solo si }T\vdash\left(\varphi\rightarrow\psi\right)
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}
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 aparezca un matematico que realice 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 Matematica dado en la Seccion [programa de logica matematica].
Para probar el Teorema de Completitud necesitaremos algunos resultados.
7.42 (Lema de Coincidencia). Sean \tau y \tau^{\prime} dos tipos cualesquiera y sea \tau_{\cap}=(\mathcal{C}_{\cap},\mathcal{F}_{\cap},\mathcal{R}_{\cap},a_{\cap}), donde \begin{aligned} \mathcal{C}_{\cap} & =\mathcal{C}\cap\mathcal{C}^{\prime}\\ \mathcal{F}_{\cap} & =\{f\in\mathcal{F}\cap\mathcal{F}^{\prime}:a(f)=a^{\prime}(f)\}\\ \mathcal{R}_{\cap} & =\{r\in\mathcal{R}\cap\mathcal{R}^{\prime}:a(r)=a^{\prime}(r)\}\\ a_{\cap} & =a|_{\mathcal{F}_{\cap}\cup\mathcal{R}_{\cap}} \end{aligned} Entonces \tau_{\cap} es un tipo tal que T^{\tau_{\cap}}=T^{\tau}\cap T^{\tau^{\prime}} y F^{\tau_{\cap}}=F^{\tau}\cap F^{\tau^{\prime}}. Sean \mathbf{A} y \mathbf{A}^{\prime} modelos de tipo \tau y \tau^{\prime} respectivamente. Supongamos que A=A^{\prime} y que c^{\mathbf{A}}=c^{\mathbf{A}^{\prime}}, para cada c\in\mathcal{C}_{\cap}, f^{\mathbf{A}}=f^{\mathbf{A}^{\prime}}, para cada f\in\mathcal{F}_{\cap} y r^{\mathbf{A}}=r^{\mathbf{A}^{\prime}}, para cada r\in\mathcal{R}_{\cap}.
(a) Para cada t=_{d}t(\vec{v})\in T^{\tau_{\cap}} se tiene que t^{\mathbf{A}}[\vec{a}]=t^{\mathbf{A}^{\prime}}[\vec{a}], para cada \vec{a}\in A^{n}
(b) Para cada \varphi=_{d}\varphi(\vec{v})\in F^{\tau_{\cap}} se tiene que \mathbf{A}\models\varphi[\vec{a}]\text{ si y solo si }\mathbf{A}^{\prime}\models\varphi[\vec{a}] para cada \vec{a}\in A^{n}
(c) Si \Sigma\cup\{\varphi\}\subseteq S^{\tau_{\cap}}, entonces (\Sigma,\tau)\models\varphi\text{ sii }(\Sigma,\tau^{\prime})\models\varphi\text{.}
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
- universo de \mathbf{A}= A^{\prime}
- c^{\mathbf{A}}=c^{\mathbf{A}^{\prime}}, para cada c\in\mathcal{C}_{\cap},
- f^{\mathbf{A}}=f^{\mathbf{A}^{\prime}}, para cada f\in\mathcal{F}_{\cap}
- r^{\mathbf{A}}=r^{\mathbf{A}^{\prime}}, para cada r\in\mathcal{R}_{\cap}
- c^{\mathbf{A}}=a, para cada c\in\mathcal{C}-\mathcal{C}_{\cap}
- 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}
- 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
7.43 (Tipos parecidos). Sean \tau=(\mathcal{C},\mathcal{F},\mathcal{R},a) y \tau^{\prime}=(\mathcal{C}^{\prime},\mathcal{F}^{\prime},\mathcal{R}^{\prime},a^{\prime}) tipos.
(1) Si \mathcal{C}\subseteq\mathcal{C}^{\prime}, \mathcal{F}\subseteq\mathcal{F}^{\prime}, \mathcal{R}\subseteq\mathcal{R}^{\prime} y a^{\prime}|_{\mathcal{F}\cup\mathcal{R}}=a, entonces (\Sigma,\tau)\vdash\varphi implica (\Sigma,\tau^{\prime})\vdash\varphi
(2) Si \mathcal{C}\subseteq\mathcal{C}^{\prime}, \mathcal{F}=\mathcal{F}^{\prime}, \mathcal{R}=\mathcal{R}^{\prime} y a^{\prime}=a, entonces (\Sigma,\tau^{\prime})\vdash\varphi implica (\Sigma,\tau)\vdash\varphi, cada vez que \Sigma\cup\{\varphi\}\subseteq S^{\tau}.
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.36 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:
- \mathcal{C}_{2}\cap\mathcal{C}^{\prime}=\emptyset
- (\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}.
7.44 (Lema del Infimo). Sea T=(\Sigma,\tau) una teoria y supongamos que \tau tiene una cantidad infinita de nombres de cte que no ocurren en las sentencias de \Sigma. Entonces para cada formula \varphi=_{d}\varphi(v), se tiene que en el algebra de Lindenbaum \mathcal{A}_{T}: [\forall v\varphi(v)]_{T}=\inf(\{[\varphi(t)]_{T}:t\in T_{c}^{\tau}\}).
Proof. Haremos primero el caso en que v no ocurre libremente en \varphi, es decir cuando \varphi es una sentencia. En este caso tenemos que \{[\varphi(t)]_{T}:t\in T_{c}^{\tau}\}=\{[\varphi]_{T}\}, por lo cual \inf(\{[\varphi(t)]_{T}:t\in T_{c}^{\tau}\})=[\varphi]_{T}. Es decir que debemos probar que [\forall v\varphi(v)]_{T}=[\varphi]_{T}. Pero el Axioma Esquema de Cuantificacion Vacua nos dice que (\forall v\varphi\leftrightarrow\varphi) es un axioma logico por lo cual T\vdash(\forall v\varphi\leftrightarrow\varphi)), obteniendo que [\forall v\varphi(v)]_{T}=[\varphi]_{T}.
Hagamos ahora el caso en el que Li(\varphi)=\{v\}. Primero veamos que [\forall v\varphi(v)]_{T} es cota inferior del conjunto \{[\varphi(t)]_{T}:t\in T_{c}^{\tau}\}. Por el Lema 7.41 debemos probar que para todo termino cerrado t, se da que T\vdash(\forall v\varphi(v)\rightarrow\varphi(t)). Pero esto es facil ya que \begin{array}{cllll} 1. & \forall v\varphi(v) & & & \text{HIPOTESIS}1\\ 2. & \varphi(t) & & & \text{TESIS}1\text{PARTICULARIZACION}(1)\\ 3. & (\forall v\varphi(v)\rightarrow\varphi(t)) & & & \text{CONCLUSION} \end{array} es una prueba formal de (\forall v\varphi(v)\rightarrow\varphi(t)) en T. Supongamos ahora que [\psi]_{T}\leq^{T}[\varphi(t)]_{T}, para todo termino cerrado t. Probaremos que [\psi]_{T}\leq^{T}[\forall v\varphi(v)]_{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 (\boldsymbol{\varphi},\mathbf{J})=(\boldsymbol{\varphi}_{1}...\boldsymbol{\varphi}_{n},\mathbf{J}_{1}...\mathbf{J}_{n}) de \left(\psi\rightarrow\varphi(c)\right) en T. Sean c_{1},...,c_{k} los nombres de constante auxiliares de (\boldsymbol{\varphi},\mathbf{J}) (es decir, (\mathcal{C}\cup\{c_{1},...,c_{k}\},\mathcal{F},\mathcal{R},a)) es el tipo ambiente de (\boldsymbol{\varphi},\mathbf{J})). Sea m\in\mathbf{N} tal que J_{i}\neq\text{HIPOTESIS}\bar{m} para cada i=1,...,n. Notese que (\mathcal{C}-\{c\},\mathcal{F},\mathcal{R},a)) es un tipo y los elementos de \Sigma son sentencias de este tipo ya que c no ocurre en las sentencias de \Sigma. O sea que T_{r}=(\Sigma,\mathcal{C}-\{c\},\mathcal{F},\mathcal{R},a)) es una teoria. Veamos que la siguiente es una prueba formal en T_{r} de \left(\psi\rightarrow\forall v\varphi(v)\right): \begin{array}{rlcl} 1. & \boldsymbol{\varphi}_{1} & & \mathbf{J}_{1}\\ 2. & \boldsymbol{\varphi}_{2} & & \mathbf{J}_{2}\\ \vdots & \vdots & & \vdots\\ n. & \boldsymbol{\varphi}_{n}=\left(\psi\rightarrow\varphi(c)\right) & & \mathbf{J}_{n}\\ n+1. & \psi & & \text{HIPOTESIS}\bar{m}\\ n+2. & \varphi(c) & & \text{MODUSPONENS}(\overline{n+1},\bar{n})\\ n+3. & \forall v\varphi(v) & & \text{TESIS}\bar{m}\text{GENERALIZACION}(\overline{n+2})\\ n+4. & \left(\psi\rightarrow\forall v\varphi(v)\right) & & \text{CONCLUSION} \end{array} Notese que nuestra candidata a prueba formal, como objeto matematico es el par (\boldsymbol{\gamma},\mathbf{K}) donde \boldsymbol{\gamma} es la palabra \boldsymbol{\varphi}\psi\varphi(c)\forall v\varphi(v)\left(\psi\rightarrow\forall v\varphi(v)\right) y \mathbf{K} es la palabra \mathbf{J}\text{HIPOTESIS}\bar{m}\text{MODUSPONENS}(\overline{n+1},\bar{n})\text{TESIS}\bar{m}\text{GENERALIZACION}(\overline{n+2})\text{CONCLUSION} Notese que
(I) n(\boldsymbol{\gamma})=n+4=n(\mathbf{K})
(II) \boldsymbol{\gamma}_{i}=\boldsymbol{\varphi}_{i}, para i\in\{1,...,n\}, \boldsymbol{\gamma}_{n+1}=\psi, \boldsymbol{\gamma}_{n+2}=\varphi(c), \boldsymbol{\gamma}_{n+3}=\forall v\varphi(v) y \boldsymbol{\gamma}_{n+4}=(\psi\rightarrow\forall v\varphi(v))
(III) \boldsymbol{\mathbf{K}}_{i}=\mathbf{J}_{i}, para i\in\{1,...,n\}, \mathbf{J}_{n+1}=\text{HIPOTESIS}\bar{m}, \mathbf{J}_{n+2}=\text{MODUSPONENS}(\overline{n+1},\bar{n}), \mathbf{J}_{n+3}=\text{TESIS}\bar{m}\text{GENERALIZACION}(\overline{n+2}) y \mathbf{J}_{n+4}=\text{CONCLUSION}
(IV) \mathbf{K} es balanceada ya que \mathbf{J} lo es y \mathcal{B}^{\mathbf{K}}=\mathcal{B}^{\mathbf{J}}\cup\{\left\langle n+1,n+3\right\rangle \}
Notese que el tipo \tau_{1} de la definicion de prueba para (\boldsymbol{\gamma},\mathbf{K}) puede ser \tau_{1}=((\mathcal{C}-\{c\})\cup\{c,c_{1},...,c_{k}\},\mathcal{F},\mathcal{R},a)=(\mathcal{C}\cup\{c_{1},...,c_{k}\},\mathcal{F},\mathcal{R},a)) (i.e. el tipo ambiente de (\boldsymbol{\gamma},\mathbf{K})). O sea justamente es el tipo ambiente de (\boldsymbol{\varphi},\mathbf{J}) pero en (\boldsymbol{\varphi},\mathbf{J}) el nombre de cte c no es auxiliar ya que esta en el tipo de la teoria T y en cambio c es un nombre de constante auxiliar de (\boldsymbol{\gamma},\mathbf{K}) ya que no pertenece al tipo de la teoria T_{r}. O sea los nombres de constante auxiliares de (\boldsymbol{\gamma},\mathbf{K}) son c,c_{1},...,c_{k}. O sea que I y IV nos dicen que (\boldsymbol{\gamma},\mathbf{K}) es un par adecuado de tipo \tau_{1}.
Solo nos falta ver que se cumplen (3) y (4) de la definicion de prueba formal. Dejamos al lector verificar que se cumple (3). Para chequear que se cumple (4) primero notemos que:
(V) Para i,j\in\{1,...,n\} se tiene que i es anterior a j en (\boldsymbol{\gamma},\mathbf{K}) si y solo si i es anterior a j en (\boldsymbol{\varphi},\mathbf{J}) (esto es directo de IV)
(VI) Si i,j\in\{1,...,n\} entonces \boldsymbol{\gamma}_{i} es hipotesis de \boldsymbol{\gamma}_{j} en (\boldsymbol{\gamma},\mathbf{K}) si y solo si \boldsymbol{\varphi}_{i} es hipotesis de \boldsymbol{\varphi}_{i} en (\boldsymbol{\varphi},\mathbf{J}) (esto es directo de IV)
(VII) Dadas e,d\in\mathcal{C}\cup\{c_{1},...,c_{k}\} se tiene que e depende de d en (\boldsymbol{\gamma},\mathbf{K}) si y solo si e depende de d en (\boldsymbol{\varphi},\mathbf{J})
Probemos VII. Sean e,d\in\mathcal{C}\cup\{c_{1},...,c_{k}\} tales que e depende directamente de d en (\boldsymbol{\gamma},\mathbf{K}). O sea que hay numeros 1\leq l<j\leq n(\boldsymbol{\gamma})=n+4 tales que
- l es anterior a j en (\boldsymbol{\gamma},\mathbf{K})
- \mathbf{K}_{j}=\alpha\mathrm{ELECCION}(\bar{l}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\} y (\boldsymbol{\gamma}_{l},\boldsymbol{\gamma}_{j})\in Elec^{\tau_{1}} via e
- d ocurre en \boldsymbol{\gamma}_{l}.
Ya que \mathbf{K}_{j}=\alpha\mathrm{ELECCION}(\bar{l}), III nos dice que j\leq n y por lo tanto l\leq n. Usando V, III y II obtenemos que
- l es anterior a j en (\boldsymbol{\varphi},\mathbf{J})
- \mathbf{J}_{j}=\alpha\mathrm{ELECCION}(\bar{l}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\} y (\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{j})\in Elec^{\tau_{1}} via e
- d ocurre en \boldsymbol{\varphi}_{l}.
lo cual nos dice que e depende directamente de d en (\boldsymbol{\varphi},\mathbf{J}). Similarmente podemos probar que si e depende directamente de d en (\boldsymbol{\varphi},\mathbf{J}), entonces e depende directamente de d en (\boldsymbol{\gamma},\mathbf{K}). Por supuesto esto ya alcanza para probar VII.
Ahora si, veamos que se cumple (4) de la definicion de prueba formal. Para cada i=1,...,n+4 debemos probar que se cumple alguna de las propiedades (a), (b), (c), ..., (u) de (4) de la definicion de prueba. Primero supongamos i\in\{1,...,n\}. Ya que (\boldsymbol{\varphi},\mathbf{J}) cumple (4) tenemos que se cumple alguna de las propiedades (a), (b), (c), ...., (u), con respecto a la prueba (\boldsymbol{\varphi},\mathbf{J}). Por ejemplo supongamos se cumple (f) con respecto a la prueba (\boldsymbol{\varphi},\mathbf{J}). Entonces tenemos que \mathbf{J}_{i}=\alpha\mathrm{COMMUTATIVIDAD}(\bar{l}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}, l anterior a i en (\boldsymbol{\varphi},\mathbf{J}) y (\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Commut^{\tau_{1}}. Pero ya que \mathbf{K}_{i}=\mathbf{J}_{i}, \boldsymbol{\varphi}_{l}=\boldsymbol{\gamma}_{l}\text{ y }\boldsymbol{\varphi}_{i}=\boldsymbol{\gamma}_{i}, V nos dice que
- \mathbf{K}_{i}=\alpha\mathrm{COMMUTATIVIDAD}(\bar{l}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}, l anterior a i en (\boldsymbol{\gamma},\mathbf{K}) y (\boldsymbol{\gamma}_{l},\boldsymbol{\gamma}_{i})\in Commut^{\tau_{1}}(recordar que \tau_{1} es el tipo ambiente de (\boldsymbol{\varphi},\mathbf{J}) y (\boldsymbol{\gamma},\mathbf{K}))
lo cual nos dice que se cumple (f) con respecto a (\boldsymbol{\gamma},\mathbf{K}). Supongamos ahora se cumple (t) respecto de la prueba (\boldsymbol{\varphi},\mathbf{J}). Es decir \mathbf{J}_{i}=\alpha\mathrm{ELECCION}(\bar{l}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}, l anterior a i en (\boldsymbol{\varphi},\mathbf{J}) y (\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Elec^{\tau_{1}} via un nombre de cte e, el cual no pertenece a \mathcal{C} y no ocurre en \boldsymbol{\varphi}_{1},...,\boldsymbol{\varphi}_{i-1}. Ya que \mathbf{K}_{i}=\mathbf{J}_{i} y \boldsymbol{\gamma}_{j}=\boldsymbol{\varphi}_{j}, para j\in\{1,...,n\}, V nos dice que
- \mathbf{K}_{i}=\alpha\mathrm{ELECCION}(\bar{l}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}, l anterior a i en (\boldsymbol{\gamma},\mathbf{K}) y (\boldsymbol{\gamma}_{l},\boldsymbol{\gamma}_{i})\in Elec^{\tau_{1}} via un nombre de cte e, el cual no pertenece a \mathcal{C}-\{c\} y no ocurre en \boldsymbol{\gamma}_{1},...,\boldsymbol{\gamma}_{i-1}.
O sea que se cumple (t) con respecto a (\boldsymbol{\gamma},\mathbf{K}). La prueba de los otros casos es similar, salvo el caso (u). Supongamos entonces que se cumple (u) respecto de la prueba (\boldsymbol{\varphi},\mathbf{J}) y veamos que entonces tambien se cumple (u) respecto de (\boldsymbol{\gamma},\mathbf{K}). O sea que sabemos que \mathbf{J}_{i}=\alpha\mathrm{GENERALIZACION}(\bar{l}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}, l anterior a i en (\boldsymbol{\varphi},\mathbf{J}) y (\boldsymbol{\varphi}_{l},\boldsymbol{\varphi}_{i})\in Generaliz^{\tau_{1}} via un nombre de cte d el cual cumple:
(i) d\not\in\mathcal{C}
(ii) Para cada u\in\{1,...,n\}, si \mathbf{J}_{u}=\alpha\mathrm{ELECCION}(\bar{v}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\} y v anterior a u en (\boldsymbol{\varphi},\mathbf{J}), entonces no se da que (\boldsymbol{\varphi}_{v},\boldsymbol{\varphi}_{u})\in Elec^{\tau_{1}} via d.
(iii) Para cada u\in\{1,...,n\}, si \boldsymbol{\varphi}_{u} es hipotesis de \boldsymbol{\varphi}_{l} en (\boldsymbol{\varphi},\mathbf{J}), entonces d no ocurre en \boldsymbol{\varphi}_{u}
(iv) Ningun nombre de constante que ocurra en \boldsymbol{\varphi}_{l} depende de d en (\boldsymbol{\varphi},\mathbf{J})
(v) Para cada u\in\{1,...,n\}, si \boldsymbol{\varphi}_{u} es hipotesis de \boldsymbol{\varphi}_{l} en (\boldsymbol{\varphi},\mathbf{J}), entonces ningun nombre de constante que ocurra en \boldsymbol{\varphi}_{u} depende de d en (\boldsymbol{\varphi},\mathbf{J})
Usando entonces las propiedades ya probadas es facil ver que \mathbf{K}_{i}=\alpha\mathrm{GENERALIZACION}(\bar{l}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}, l anterior a i en (\boldsymbol{\gamma},\mathbf{K}) y (\boldsymbol{\gamma}_{l},\boldsymbol{\gamma}_{i})\in Generaliz^{\tau_{1}} via un nombre de cte d el cual cumple:
(i)’ d\not\in\mathcal{C}-\{c\}
(ii)’ Para cada u\in\{1,...,n\}, si \mathbf{K}_{u}=\alpha\mathrm{ELECCION}(\bar{v}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\} y v anterior a u en (\boldsymbol{\gamma},\mathbf{K}), entonces no se da que (\boldsymbol{\gamma}_{v},\boldsymbol{\gamma}_{u})\in Elec^{\tau_{1}} via d.
(iii)’ Para cada u\in\{1,...,n\}, si \boldsymbol{\gamma}_{u} es hipotesis de \boldsymbol{\gamma}_{l} en (\boldsymbol{\gamma},\mathbf{K}), entonces d no ocurre en \boldsymbol{\gamma}_{u}
(iv)’ Ningun nombre de constante que ocurra en \boldsymbol{\gamma}_{l} depende de d en (\boldsymbol{\gamma},\mathbf{K})
(v)’ Para cada u\in\{1,...,n\}, si \boldsymbol{\gamma}_{u} es hipotesis de \boldsymbol{\gamma}_{l} en (\boldsymbol{\gamma},\mathbf{K}), entonces ningun nombre de constante que ocurra en \boldsymbol{\gamma}_{u} depende de d en (\boldsymbol{\gamma},\mathbf{K})
Notese que hemos “casi” probado que se cumple (u) respecto de (\boldsymbol{\gamma},\mathbf{K}) ya que deberiamos tener n+4 en lugar de n en las propiedades (ii)’, (iii)’ y (v)’. Pero notese que podemos poner n+4 en lugar de n en dichas propiedades y se seguiran cumpliendo. Por ejemplo si \mathbf{K}_{u}=\alpha\mathrm{ELECCION}(\bar{v}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\}, entonces u\leq n (por como son \mathbf{K}_{n+1},...,\mathbf{K}_{n+4}) y por lo tanto en (ii)’ es irrelevante reemplazar n por n+4. Ademas si \boldsymbol{\gamma}_{u} es hipotesis de \boldsymbol{\gamma}_{l} en (\boldsymbol{\gamma},\mathbf{K}), entonces u\leq l<i\leq n por lo cual en (iii)’ y (v)’ es irrelevante reemplazar n por n+4. Ahora si hemos probado que se cumple (u) respecto de (\boldsymbol{\gamma},\mathbf{K}).
Nos falta ver que para i\in\{n+1,n+2,n+3,n+4\} se cumple alguna de las propiedades (a), (b), (c), ..., (u) de (4) de la definicion de prueba, respecto de (\boldsymbol{\gamma},\mathbf{K}). Cuando i\in\{n+1,n+2,n+4\} es facil y dejado al lector. Veamos el caso i=n+3. Veremos que se da (u). Es claro que \mathbf{K}_{i}=\text{TESIS}\bar{m}\text{GENERALIZACION}(\overline{n+2}), que n+2 es anterior a i en (\boldsymbol{\gamma},\mathbf{K}) y que (\boldsymbol{\gamma}_{n+2},\boldsymbol{\gamma}_{i})\in Generaliz^{\tau_{1}} via el nombre de cte c. Nos faltaria ver entonces que:
(i)” c\not\in\mathcal{C}-\{c\}
(ii)” Para cada u\in\{1,...,n+4\}, si \mathbf{K}_{u}=\alpha\mathrm{ELECCION}(\bar{v}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\} y v anterior a u en (\boldsymbol{\gamma},\mathbf{K}), entonces no se da que (\boldsymbol{\gamma}_{v},\boldsymbol{\gamma}_{u})\in Elec^{\tau_{1}} via c.
(iii)” Para cada u\in\{1,...,n+4\}, si \boldsymbol{\gamma}_{u} es hipotesis de \boldsymbol{\gamma}_{n+2} en (\boldsymbol{\gamma},\mathbf{K}), entonces c no ocurre en \boldsymbol{\gamma}_{u}
(iv)” Ningun nombre de constante que ocurra en \boldsymbol{\gamma}_{n+2} depende de c en (\boldsymbol{\gamma},\mathbf{K})
(v)” Para cada u\in\{1,...,n+4\}, si \boldsymbol{\gamma}_{u} es hipotesis de \boldsymbol{\gamma}_{n+2} en (\boldsymbol{\gamma},\mathbf{K}), entonces ningun nombre de constante que ocurra en \boldsymbol{\gamma}_{u} depende de c en (\boldsymbol{\gamma},\mathbf{K})
Obviamente se cumple (i)”. Veamos que se cumple (ii)”. Supongamos entonces \mathbf{K}_{u}=\alpha\mathrm{ELECCION}(\bar{v}), con u\in\{1,...,n+4\}, \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\} y v anterior a u en (\boldsymbol{\gamma},\mathbf{K}). Note que u\leq n por lo cual tambien v\leq n. O sea que por las propiedades ya probadas tenemos que \mathbf{J}_{u}=\alpha\mathrm{ELECCION}(\bar{v}), con \alpha\in\{\varepsilon\}\cup\{\mathrm{TESIS}\bar{k}:k\in\mathbf{N}\} y v anterior a u en (\boldsymbol{\varphi},\mathbf{J}). Pero entonces ya que (\boldsymbol{\varphi},\mathbf{J}) es una prueba formal, debe darse que (\boldsymbol{\varphi}_{v},\boldsymbol{\varphi}_{u})\in Elec^{\tau_{1}} via un nombre de cte e, el cual no pertenece a \mathcal{C} y no ocurre en \boldsymbol{\varphi}_{1},...,\boldsymbol{\varphi}_{u-1}. Ya que c no es igual a e, tenemos que no se da (\boldsymbol{\varphi}_{v},\boldsymbol{\varphi}_{u})\in Elec^{\tau_{1}} via c, por lo cual no se da (\boldsymbol{\gamma}_{v},\boldsymbol{\gamma}_{u})\in Elec^{\tau_{1}} via c. Para probar (iii)” note que si \boldsymbol{\gamma}_{u} es hipotesis de \boldsymbol{\gamma}_{n+2} en (\boldsymbol{\gamma},\mathbf{K}), entonces u=n+1. O sea que \boldsymbol{\gamma}_{u}=\psi y claramente entonces c no ocurre en \boldsymbol{\gamma}_{u}. Para probar (iv)” y (v)” notese que los nombres de cte que ocurren en \boldsymbol{\gamma}_{n+2} o en hipotesis de \boldsymbol{\gamma}_{n+2} en (\boldsymbol{\gamma},\mathbf{K}) pertenecen todos a \mathcal{C}, por lo cual no dependen de ningun otro nombre de cte en (\boldsymbol{\gamma},\mathbf{K}) ya que no dependen de ningun nombre de cte en (\boldsymbol{\varphi},\mathbf{J}).
O sea que ya probamos que (\boldsymbol{\gamma},\mathbf{K}) es una prueba por lo cual tenemos que T_{r}\vdash\left(\psi\rightarrow\forall v\varphi(v)\right). Por el Lema 7.43 tenemos entonces que T\vdash\left(\psi\rightarrow\forall v\varphi(v)\right), lo cual nos dice que [\psi]_{T}\leq^{T}[\forall v\varphi(v)]_{T}.
Para entender la prueba del siguiente resultado es conveniente que el lector repase el final de la Seccion [ordenes naturales sobre sigma estrella] donde dado un orden total \leq para un alfabeto \Sigma se define un orden total sobre \Sigma^{*} el cual extiende a \leq (y es llamado el orden total de \Sigma^{*} inducido por \leq).
7.45 (Lema de enumeracion). Sea \tau un tipo. Hay una infinitupla (\gamma_{1},\gamma_{2},...)\in F^{\tau\mathbf{N}} tal que:
(1) \left\vert Li(\gamma_{j})\right\vert \leq1, para cada j=1,2,...
(2) Si \left\vert Li(\gamma)\right\vert \leq1, entonces \gamma=\gamma_{j}, para algun j\in\mathbf{N}
Proof. Notese que las formulas de tipo \tau son palabras de algun alfabeto finito A. Sea \leq un orden total sobre A. Sea L=\{\alpha\in F^{\tau}:\left\vert Li(\alpha)\right\vert \leq1\}. Definamos para t\in\mathbf{N}, \gamma_{t}=t\mathrm{\text{-}esimo}\text{ }\mathrm{elemento\text{ }de}\text{ }L\text{ }\mathrm{con\text{ }respecto\text{ }al\text{ }orden\text{ }total\text{ }de\text{ }}A^{\ast}\text{ }\mathrm{inducido\text{ }por}\text{ }\leq Notese que \begin{aligned} \gamma_{1} & =\text{menor }\alpha\in F^{\tau}\text{ tal que }\left\vert Li(\alpha)\right\vert \leq1\\ \gamma_{t+1} & =\text{menor }\alpha\in F^{\tau}\text{ tal que }\left\vert Li(\alpha)\right\vert \leq1\text{ y }\alpha\notin\{\gamma_{1},...,\gamma_{t}\} \end{aligned} Claramente entonces la infinitupla (\gamma_{1},\gamma_{2},...) cumple (1) y (2).
Observacion: Ya hemos observado que F^{\tau} es un conjunto A-efectivamente computable y por supuesto tambien lo es \{\alpha\in F^{\tau}:\left\vert Li(\alpha)\right\vert \leq1\}. Dejamos al lector convencerse que la funcion f:\mathbf{N}\rightarrow F^{\tau}dada por f(t)=\gamma_{t} es A-efectivamente computable. Por supuesto tambien se podria probar que f es A-recursiva primitiva usando las tecnicas dadas en el analisis de recursividad del lenguaje de primer orden hecho en la Subseccion [analisis de recursividad del lenguaje de primer orden].
Ahora si, el famoso resultado de Godel.
7.8 (Teorema de Completitud). Sea T=(\Sigma,\tau) una teoria de primer orden. Si T\models\varphi, entonces T\vdash\varphi.
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 [\varphi_{0}]_{T}\neq1^{T}=\{\varphi\in S^{\tau}:T\vdash\varphi\}. O sea que [\lnot\varphi_{0}]_{T}\not=0^{T}. Por el lema anterior hay una infinitupla (\gamma_{1},\gamma_{2},...)\in F^{\tau\mathbf{N}} tal que:
- \left\vert Li(\gamma_{j})\right\vert \leq1, para cada j=1,2,...
- 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.44 tenemos que \inf\{[\gamma_{j}(t)]_{T}:t\in T_{c}^{\tau}\}=[\forall w_{j}\gamma_{j}(w_{j})]_{T}, para cada j=1,2,.... Por el Teorema de Rasiowa y Sikorski tenemos que hay un filtro primo \mathcal{U} de \mathcal{A}_{T}, el cual cumple:
(a) [\lnot\varphi_{0}]_{T}\in\mathcal{U}
(b) 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
(b)^{\prime} 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) \bowtie es de equivalencia.
(2) 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) 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:
- Universo de \mathbf{A}_{\mathcal{U}}=T_{c}^{\tau}/\mathrm{\bowtie}
- c^{\mathbf{A}_{\mathcal{U}}}=c/\mathrm{\bowtie}, para cada c\in\mathcal{C}.
- 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}\;
- 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:
(4) 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}
(5) 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.43, tenemos que T\vdash\varphi.
Veamos algunas consecuencias del Teorema de Completitud.
7.4. Toda teoria consistente tiene un modelo.
Proof. Supongamos (\Sigma,\tau) es consistente y no tiene modelos. Ya que no tiene modelos, se da trivialmente que (\Sigma,\tau)\models\varphi, para cada \varphi\in S^{\tau}. Obviamente esto dice que (\Sigma,\tau) es inconsistente, lo cual es absurdo.
7.5 (Teorema de Compacidad). Sea (\Sigma,\tau) una teoria.
(a) Si (\Sigma,\tau) es tal que (\Sigma_{0},\tau) tiene un modelo, para cada subconjunto finito \Sigma_{0}\subseteq\Sigma, entonces (\Sigma,\tau) tiene un modelo
(b) Si (\Sigma,\tau)\models\varphi, entonces hay un subconjunto finito \Sigma_{0}\subseteq\Sigma tal que (\Sigma_{0},\tau)\models\varphi.
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 (use Correccion). O sea que (\Sigma,\tau) es consistente y entonces el corolario anterior nos dice que tiene un modelo
(b) Si (\Sigma,\tau)\models\varphi, entonces por Completitud, (\Sigma,\tau)\vdash\varphi. Pero entonces hay un subconjunto finito \Sigma_{0}\subseteq\Sigma tal que (\Sigma_{0},\tau)\vdash\varphi, es decir tal que (\Sigma_{0},\tau)\models\varphi (Correccion).
Dejamos al lector entender que es una consecuencia del Teorema de completitud que el criterio NoEsTeorema es completo, es decir que siempre que una sentecia no sea teorema de una teoria hay un modelo de la misma que hace falsa a dicha sentencia.
Usando los teoremas de correccion y completitud podemos dar una representacion semantica del algebra de Lindenbaum. 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
7.46. \{\mathrm{Mod}_{T}(\varphi):\varphi\in S^{\tau}\} es un subuniverso del algebra de Boole (\mathcal{P}(\mathrm{Mod}_{T}),\cup,\cap,^{c},\emptyset,\mathrm{Mod}_{T})
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}
7.47. Dadas \varphi,\psi\in S^{\tau} se tiene:
(1) [\varphi]_{T}\leq^{T}[\psi]_{T} sii \mathrm{Mod}_{T}(\varphi)\subseteq\mathrm{Mod}_{T}(\psi)
(2) [\varphi]_{T}=[\psi]_{T} sii \mathrm{Mod}_{T}(\varphi)=\mathrm{Mod}_{T}(\psi)
(3) [\varphi]_{T}<^{T}[\psi]_{T} sii \mathrm{Mod}_{T}(\varphi)\subsetneqq\mathrm{Mod}_{T}(\psi)
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
7.9 (Representacion semantica del algebra de Lindenbaum). La funcion \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} es un isomorfismo de \mathcal{A}_{T} en (\{\mathrm{Mod}_{T}(\varphi):\varphi\in S^{\tau}\},\cup,\cap,^{c},\emptyset,\mathrm{Mod}_{T}).
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.46, facilmente podemos ver que f es un homomorfismo por lo cual es un isomorfismo.
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. Necesitaremos la siguiente definicion. Sean \mathbf{A} y \mathbf{B} dos estructuras de tipo \tau. Diremos que \mathbf{A} y \mathbf{B} son elementalmente equivalentes si para cada \varphi\in S^{\tau} se da que \mathbf{A}\models\varphi sii \mathbf{B}\models\varphi.
7.2. Sea (\Sigma,\tau) una teoria consistente. Son equivalentes
(1) (\Sigma,\tau) es completa
(2) Todos los modelos de (\Sigma,\tau) son elementalmente equivalentes
(3) Hay una estructura \mathbf{A} tal que los teoremas de (\Sigma,\tau) son exactamente las sentencias verdaderas en \mathbf{A}
(4) \mathcal{A}_{(\Sigma,\tau)} tiene exactamente dos elementos
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.
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{\boldsymbol{\omega}} a la estructura de tipo \tau_{A} que tiene a \omega como universo e interpreta los nombres de \tau_{A} en la manera usual, es decir \begin{array}{l} 0^{\mathbf{\boldsymbol{\omega}}}=0\\ 1^{\mathbf{\boldsymbol{\omega}}}=1\\ \leq^{\mathbf{\boldsymbol{\omega}}}=\{(n,m)\in\omega^{2}:n\leq m\}\\ +^{\mathbf{\boldsymbol{\omega}}}(n,m)=n+m\text{, para cada }n,m\in\omega\\ .^{\mathbf{\boldsymbol{\omega}}}(n,m)=n.m\text{, para cada }n,m\in\omega \end{array} Sea \Sigma el conjunto formado por las siguientes sentencias:
\forall x_{1}\forall x_{2}\forall x_{3}\;x_{1}+(x_{2}+x_{3})\equiv(x_{1}+x_{2})+x_{3}
\forall x_{1}\forall x_{2}\;x_{1}+x_{2}\equiv x_{2}+x_{1}
\forall x_{1}\forall x_{2}\forall x_{3}\;x_{1}.(x_{2}.x_{3})\equiv(x_{1}.x_{2}).x_{3}
\forall x_{1}\forall x_{2}\;x_{1}.x_{2}\equiv x_{2}.x_{1}
\forall x_{1}\;x_{1}+0\equiv x_{1}
\forall x_{1}\;x_{1}.0\equiv0
\forall x_{1}\;x_{1}.1\equiv x_{1}
\forall x_{1}\forall x_{2}\forall x_{3}\;x_{1}.(x_{2}+x_{3})\equiv(x_{1}.x_{2})+(x_{1}.x_{3})
\forall x_{1}\forall x_{2}\forall x_{3}\;(x_{1}+x_{3}\equiv x_{2}+x_{3}\rightarrow x_{1}\equiv x_{2})
\forall x_{1}\;x_{1}\leq x_{1}
\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})
\forall x_{1}\forall x_{2}\;((x_{1}\leq x_{2}\wedge x_{2}\leq x_{1})\rightarrow x_{1}\equiv x_{2})
\forall x_{1}\forall x_{2}\;(x_{1}\leq x_{2}\vee x_{2}\leq x_{1})
\forall x_{1}\forall x_{2}\;(x_{1}\leq x_{2}\leftrightarrow\exists x_{3}\;x_{2}\equiv x_{1}+x_{3})
0<1
Es facil ver que todas estas sentencias son satisfechas por \mathbf{\boldsymbol{\omega}} por lo cual \mathbf{\boldsymbol{\omega}} es un modelo de la teoria (\Sigma,\tau_{A}). Definamos Verd_{\mathbf{\boldsymbol{\omega}}}=\{\varphi\in S^{\tau_{A}}:\mathbf{\boldsymbol{\omega}}\models\varphi\} Es claro que todo teorema de (\Sigma,\tau_{A}) pertenece a Verd_{\mathbf{\boldsymbol{\omega}}} (por que?). Un pregunta interesante es si toda sentencia \varphi\in Verd_{\mathbf{\boldsymbol{\omega}}} es un teorema de (\Sigma,\tau_{A}), es decir puede ser probada en forma elemental partiendo de los axiomas de \Sigma. La respuesta es no y lo explicaremos a 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{\boldsymbol{\omega}}}. Es decir los axiomas de \Sigma son demaciado generales y deberiamos agregarle axiomas que sean mas caracteristicos de la estructura particular de \mathbf{\boldsymbol{\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
7.48. \mathbf{\boldsymbol{\omega}} es un modelo de Arit
Proof. Sean \psi\in F^{\tau_{A}} y v_{1},...,v_{n+1}, con n\geq0, tales que Li(\psi)\subseteq\{v_{1},...,v_{n+1}\} y v_{i}\neq v_{j} siempre que i\neq j. Veremos que \mathbf{\boldsymbol{\omega}}\vDash Ind_{\psi,v_{1},...,v_{n+1}}. Declaremos \psi=_{d}\psi(v_{1},...,v_{n},v_{n+1}). Sea \varphi=((\psi(\vec{v},0)\wedge\forall v_{n+1}\ (\psi(\vec{v},v_{n+1})\rightarrow\psi(\vec{v},+(v_{n+1},1)))\rightarrow\forall v_{n+1}\ \psi(\vec{v},v_{n+1})) Declaremos \varphi=_{d}\varphi(v_{1},...,v_{n}). Notese que \mathbf{\boldsymbol{\omega}}\vDash Ind_{\psi,v_{1},...,v_{n+1}} si y solo si para cada a_{1},...,a_{n}\in\omega se tiene que \mathbf{\boldsymbol{\omega}}\vDash\varphi[\vec{a}]. Sean a_{1},...,a_{n}\in\omega fijos. Probaremos que \mathbf{\boldsymbol{\omega}}\vDash\varphi[\vec{a}]. Notar que si \mathbf{\boldsymbol{\omega}}\nvDash(\psi(\vec{v},0)\wedge\forall v_{n+1}\ (\psi(\vec{v},v_{n+1})\rightarrow\psi(\vec{v},+(v_{n+1},1)))[\vec{a}] entonces \mathbf{\boldsymbol{\omega}}\vDash\varphi[\vec{a}] por lo cual podemos hacer solo el caso en que \mathbf{\boldsymbol{\omega}}\vDash(\psi(\vec{v},0)\wedge\forall v_{n+1}\ (\psi(\vec{v},v_{n+1})\rightarrow\psi(\vec{v},+(v_{n+1},1)))[\vec{a}] Para probar que \mathbf{\boldsymbol{\omega}}\vDash\varphi[\vec{a}], deberemos probar entonces que \mathbf{\boldsymbol{\omega}}\vDash\forall v_{n+1}\ \psi(\vec{v},v_{n+1})[\vec{a}]. Sea S=\{a\in\omega:\mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a]\}. Ya que \mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},0)[\vec{a}], es facil ver usando el lema de reemplazo que \mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},0], lo cual nos dice que 0\in S. Ya que \mathbf{\boldsymbol{\omega}}\vDash\forall v_{n+1}\ (\psi(\vec{v},v_{n+1})\rightarrow\psi(\vec{v},+(v_{n+1},1))[\vec{a}], tenemos que
(1) Para cada a\in\omega, si \mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a], entonces \mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},+(v_{n+1},1))[\vec{a},a].
Pero por el lema de reemplazo, tenemos que \mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},+(v_{n+1},1))[\vec{a},a] sii \mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a+1], lo cual nos dice que
(2) Para cada a\in\omega, si \mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a], entonces \mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a+1].
Ya que 0\in S y (2) nos dice que a\in S implica a+1\in S, tenemos que S=\omega. Es decir que para cada a\in\omega, se da que \mathbf{\boldsymbol{\omega}}\vDash\psi(\vec{v},v_{n+1})[\vec{a},a] lo cual nos dice que \mathbf{\boldsymbol{\omega}}\vDash\forall v_{n+1}\ \psi(\vec{v},v_{n+1})[\vec{a}].
Es rutina probar que \mathbf{\boldsymbol{\omega}} satisface los otros 15 axiomas de Arit.
El modelo \mathbf{\boldsymbol{\omega}} es llamado el modelo standard de Arit.
Ejercicio: 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}
7.3. Hay un modelo de Arit el cual no es isomorfo a \mathbf{\boldsymbol{\omega}}
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{\boldsymbol{\omega}}. Supongamos F:\omega\rightarrow A es un isomorfismo de \mathbf{\boldsymbol{\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.
Ejercicio: 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\}.
7.49. Las siguientes sentencias son teoremas de la aritmetica de Peano:
(1) \forall x\;0\leq x
(2) \forall x\;(x\leq0\rightarrow x\equiv0)
(3) \forall x\forall y\;(x+y\equiv0\rightarrow(x\equiv0\wedge y\equiv0))
(4) \forall x\;(\lnot(x\equiv0)\rightarrow\exists z\ (x\equiv z+1))
(5) \forall x\forall y\;(x<y\rightarrow x+1\leq y)
(6) \forall x\forall y\;(x<y+1\rightarrow x\leq y)
(7) \forall x\forall y\;(x\leq y+1\rightarrow(x\leq y\vee x\equiv y+1))
(8) \forall x\forall y\;((x\leq y\wedge y\leq x+1)\rightarrow(x\equiv y\vee x\equiv y+1)) (use (7))
(9) \forall x\forall y\;(\lnot y\equiv0\rightarrow\exists q\exists r\;x\equiv q.y+r\wedge r<y)
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}
7.50. Sean n,m\in\omega y sea t\in T_{c}^{\tau_{A}}. Las siguientes sentencias son teoremas de la aritmetica de Peano:
(a) (+(\widehat{n},\widehat{m})\equiv\widehat{n+m})
(b) (.(\widehat{n},\widehat{m})\equiv\widehat{n.m})
(c) \forall x\;(x\leq\widehat{n}\rightarrow(x\equiv\widehat{0}\vee x\equiv\widehat{1}\vee...\vee x\equiv\widehat{n}))
(d) (t\equiv\widehat{t^{\mathbf{\boldsymbol{\omega}}}})
7.51. Si \varphi es una sentencia atomica o negacion de atomica y \mathbf{\boldsymbol{\omega}}\models\varphi, entonces Arit\vdash\varphi.
Proof. Hay cuatro casos.
Caso \varphi=(t\equiv s), con t,s terminos cerrados.
Ya que \mathbf{\boldsymbol{\omega}}\models\varphi, tenemos que t^{\mathbf{\boldsymbol{\omega}}}=s^{\mathbf{\boldsymbol{\omega}}} y por lo tanto \widehat{t^{\mathbf{\boldsymbol{\omega}}}}=\widehat{s^{\mathbf{\boldsymbol{\omega}}}}. Por el lema anterior tenemos que Arit\vdash(t\equiv\widehat{t^{\mathbf{\boldsymbol{\omega}}}}),(s\equiv\widehat{s^{\mathbf{\boldsymbol{\omega}}}}) lo cual, ya que \widehat{t^{\mathbf{\boldsymbol{\omega}}}} y \widehat{s^{\mathbf{\boldsymbol{\omega}}}} son el mismo 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{\boldsymbol{\omega}}\models\varphi, tenemos que t^{\mathbf{\boldsymbol{\omega}}}\leq s^{\mathbf{\boldsymbol{\omega}}} y por lo tanto hay un k\in\omega tal que t^{\mathbf{\boldsymbol{\omega}}}+k=s^{\mathbf{\boldsymbol{\omega}}}. Se tiene entonces que \widehat{t^{\mathbf{\boldsymbol{\omega}}}+k}=\widehat{s^{\mathbf{\boldsymbol{\omega}}}}. Por el lema anterior tenemos que Arit\vdash+(\widehat{t^{\mathbf{\boldsymbol{\omega}}}},\widehat{k})\equiv\widehat{t^{\mathbf{\boldsymbol{\omega}}}+k} lo cual nos dice que Arit\vdash+(\widehat{t^{\mathbf{\boldsymbol{\omega}}}},\widehat{k})\equiv\widehat{s^{\mathbf{\boldsymbol{\omega}}}} Pero el lema anterior nos dice que Arit\vdash(t\equiv\widehat{t^{\mathbf{\boldsymbol{\omega}}}}),(s\equiv\widehat{s^{\mathbf{\boldsymbol{\omega}}}}) y por lo tanto la regla de reemplazo nos asegura que Arit\vdash+(t,\widehat{k})\equiv s. Ya que \forall x_{1}\forall x_{2}\;(x_{1}\leq x_{2}\leftrightarrow\exists x_{3}\;x_{2}\equiv x_{1}+x_{3}) es un axioma de Arit, tenemos que Arit\vdash(t\leq s).
Caso \varphi=\lnot(t\equiv s), con t,s 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.
7.52. Sea \varphi=_{d}\varphi(\vec{v},v)\in F^{\tau_{A}}. Supongamos v es sustituible por w en \varphi y w\notin\{v_{1},...,v_{n}\}. Entonces: Arit\vdash\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))
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}