Dados t,s∈Tτ, con t≈s denotaremos la siguiente sentencia de tipo τ: ∀x1...∀xn(t≡s) donde n es el menor j tal que {x1,...,xj} contiene a todas las variables que ocurren en t y s. Notese que este n es 0 cuando t y s son terminos cerrados, es decir que t≈s denota a la sentencia (t≡s), cuando t,s∈Tτc. Las sentencias t≈s, con t,s∈Tτ, seran llamadas identidades de tipo τ. Notese que A⊨t≈s sii tA[→a]=sA[→a], para cada →a∈AN. Tambien, si t=dt(x1,...,xm) y s=ds(x1,...,xm), entonces dado una τ-algebra A, tenemos que A⊨t≈s sii tA[a1,...,am]=sA[a1,...,am], para cada (a1,...,am)∈Am. (Independientemente de que m sea el menor j tal que {x1,...,xj} contiene a las variables que ocurren en t y s.)
Una teoria de primer orden (Σ,τ) sera llamada ecuacional si τ es un tipo algebraico y cada elemento de Σ es una identidad de tipo τ. Por supuesto, el Teorema de Completitud de Godel nos garantiza que si T es una teoria ecuacional y T⊨t≈s, entonces hay una prueba formal de t≈s en T. Sin envargo, en dicha prueba formal puede haber sentencias las cuales no sean identidades. Una pregunta interesante es la siguiente:
Pregunta: ¿Hay una nocion de "prueba ecuacional" la cual sea:
- Correcta: si hay una prueba ecuacional de t≈s en T, entonces t≈s es verdadera en cada modelo de T
- Completa: si T⊨t≈s, entonces hay una prueba ecuacional de t≈s en T?
En esta seccion veremos que, tal como lo probo Birkhoff, esto es posible y que la nocion de prueba ecuacional que se puede dar es muy natural y simple, es decir si sabemos que en una teoria todos los axiomas son identidades, entonces a los fines de probar identidades las pruebas de primer orden clasicas pueden ser reemplazadas por pruebas con un formato mucho mas amigable.
Primero introducimos una serie de conjuntos los cuales poseen informacion deductiva ecuacional basica. Sea TransEcτ={(t≈s,s≈p,t≈p):t,s,p∈Tτ} Diremos que φ se deduce de ψ1y ψ2 por la regla de transitividad ecuacional, respecto a τ para expresar que (ψ1,ψ2,φ)∈TransEcτ. Sea SimEcτ={(t≈s,s≈t):t,s∈Tτ} Diremos que φ se deduce de ψ1 por la regla de simetria ecuacional, respecto a τ para expresar que (ψ1,φ)∈SimEcτ. Sea SubsEcτ={(t≈s,t(p1,...,pn)≈s(p1,...,pn)):t=dt(x1,...,xn)s=ds(x1,...,xn) y p1,...,pn∈Tτ} Diremos que φ se deduce de ψ1 por la regla de substitucion ecuacional, respecto a τ para expresar que (ψ1,φ)∈SubsEcτ. Sea ReempEcτ={(t≈s,r≈˜r):t,s,r∈Tτ \textrm{y} ˜r=resultadode reemplazar algunas ocurrencias de t en r por s} Diremos que φ se deduce de ψ1 por la regla de reemplazo ecuacional, respecto a τ para expresar que (ψ1,φ)∈ReempEcτ.
La identidad x1≈x1 sera llamada axioma logico ecuacional de tipo τ. Notese que dicha identidad no es ni mas ni menos que la sentencia ∀x1(x1≡x1) la cual es universalmente valida.
Dada una teoria ecuacional (Σ,τ) y una identidad p≈q de tipo τ, una prueba ecuacional de p≈q en (Σ,τ) sera una palabra φ∈Sτ+ tal que
(1) Cada φk, con k=1,...,n(φ), es una identidad de tipo τ y φn(φ)=p≈q
(2) Para cada k=1,...,n(φ), se da alguna de las siguientes
(a) φk=x1≈x1
(b) φk∈Σ
(c) hay i,j<k tales que φk se deduce por la regla de transitividad ecuacional a partir de φi y φj
(d) hay i<k tal que φk se deduce por la regla de simetria ecuacional a partir de φi
(e) hay i<k tal que φk se deduce por la regla de substitucion ecuacional a partir de φi
(f) hay i<k tal que φk se deduce por la regla de reemplazo ecuacional a partir de φi
Escribiremos (Σ,τ)⊢ecp≈q cuando haya una prueba ecuacional de p≈q en (Σ,τ).
Para probar que el concepto de prueba ecuacional es correcto nos hara falta el siguiente lema.
7.53. Todas las reglas introducidas en la seccion anterior son universales en el sentido que si φ se deduce de ψ1,...,ψk por alguna de estas reglas, entonces ((ψ1∧...∧ψk)→φ) es una sentencia universalmente valida.
Proof. Veamos que la regla de reemplazo es universal. Basta con ver por induccion en k que
- Teok: Sean t,s∈Tτ, r∈Tτk y sea A una τ-algebra tal que tA[→a]=sA[→a], para cada →a∈AN. Entonces rA[→a]=˜rA[→a], para cada →a∈AN, donde ˜r es el resultado de reemplazar algunas ocurrencias de t en r por s.
La prueba de Teo0 es dejada al lector. Asumamos que vale Teok y probemos que vale Teok+1. Sean t,s∈Tτ, r∈Tτk+1−Tτk y sea A una τ-algebra tal que tA[→a]=sA[→a], para cada →a∈AN. Sea ˜r el resultado de reemplazar algunas ocurrencias de t en r por s. El caso t=r es trivial. Supongamos entonces que t≠r. Supongamos r=f(r1,...,rn), con r1,...,rn∈Tτk y f∈Fn. Notese que por Lema 7.6 tenemos que ˜r=f(˜r1,...,˜rn), donde cada ˜ri es el resultado de reemplazar algunas ocurrencias de t en ri por s. Para →a∈AN se tiene que rA[→a]=f(r1,...,rn)A[→a]=fA(rA1[→a],...,rAn[→a])=fA(˜rA1[→a],...,˜rAn[→a])por Teok=f(˜r1,...,˜rn)A[→a]=˜rA[→a] lo cual prueba Teok+1
Veamos que la regla de substitucion es universal. Supongamos A⊨t≈s, con t=dt(x1,...,xn) y s=ds(x1,...,xn). Veremos que entonces A⊨t(p1,...,pn)≈s(p1,...,pn). Supongamos que pi=dpi(x1,...,xm), para cada i=1,...,n. Por (a) del Lema 7.4, tenemos que t(p1,...,pn)=dt(p1,...,pn)(x1,...,xm)s(p1,...,pn)=ds(p1,...,pn)(x1,...,xm) Sea →a∈Am. Tenemos que t(p1,...,pn)A[→a]=tA[pA1[→a],...,pAn[→a]]=sA[pA1[→a],...,pAn[→a]]=s(p1,...,pn)A[→a] lo cual nos dice que A⊨t(p1,...,pn)≈s(p1,...,pn)
7.10 (Teorema de Correccion de pruebas ecuacionales ). Si (Σ,τ)⊢ecp≈q, entonces (Σ,τ)⊨p≈q.
Proof. Sea φ una prueba ecuacional de p≈q en (Σ,τ). Usando el lema anterior se puede probar facilmente por induccion en i que (Σ,τ)⊨φi, por lo cual (Σ,τ)⊨p≈q
Para probar que el concepto de prueba ecuacional es completo nos haran falta algunos resultados basicos que tienen interes por si mismos.
Dado un tipo algebraico τ, hay una forma natural de definir un algebra Tτ cuyo universo es Tτ, de la siguiente manera
(1) cTτ=c, para cada c∈C
(2) fTτ(t1,...,tn)=f(t1,...,tn), para todo t1,...,tn∈Tτ, f∈Fn.
Llamaremos a Tτ el algebra de terminos de tipo τ.
7.1. Supongamos τ=(∅,{f},∅,{(f,1)}). Entonces el universo de Tτ es
{x1,f(x1),f(f(x1)),...}∪
{x2,f(x2),f(f(x2)),...}∪
{x3,f(x3),f(f(x3)),...}∪
⋮
La funcion que interpreta a f en Tτ es la que a cada elemento del conjunto anterior le asigna el primer elemento que esta a su derecha. Notese entonces que Tτ resulta isomorfa al algebra A definida por A=N×NfA((n,m))=(n,m+1)
7.54. Dados t1,...,tn,t=dt(x1,...,xn)∈Tτ, se tiene que tTτ[t1,...,tn]=t(t1,...,tn).
Proof. Para cada k≥0, sea
- Teok: Dados t1,...,tn∈Tτ y t=dt(x1,...,xn)∈Tτk, se tiene que tTτ[t1,...,tn]=t(t1,...,tn).
Veamos que es cierto Teo0. Hay dos casos
Caso t=dt(x1,...,xn)=c∈C.
Entonces tenemos tTτ[t1,...,tn]=cTτ=c=t(t1,...,tn)
Caso t=dt(x1,...,xn)=xi, para algun i.
Entonces tenemos tTτ[t1,...,tn]=ti=t(t1,...,tn) Veamos que Teok implica Teok+1. Supongamos que vale Teok. Sean t1,...,tn∈Tτ y t=dt(x1,...,xn)∈Tτk+1−Tτk. Hay f∈Fm, con m≥1, y terminos s1,...,sm∈Tτk tales que t=f(s1,...,sm). Notese que si=dsi(x1,...,xn), i=1,...,m. Tenemos entonces que tTτ[t1,...,tn]=f(s1,...,sm)Tτ[t1,...,tn]=fTτ(sTτ1[t1,...,tn],...,sTτm[t1,...,tn])=fTτ(s1(t1,...,tn),...,sm(t1,...,tn))=f(s1(t1,...,tn),...,sm(t1,...,tn))=t(t1,...,tn) con lo cual vale Teok+1
El algebra de terminos tiene la siguiente propiedad fundamental:
7.55 (Universal Maping Property). Si A es cualquier τ-algebra y F:Var→A, es una funcion cualquiera, entonces F puede ser extendida a un homomorfismo ˉF:Tτ→A.
Proof. Definamos ˉF de la siguiente manera: ˉF(t)=tA[(F(x1),F(x2),...)] Es claro que ˉF extiende a F. Veamos que es un homomorfismo. Dada c∈C, tenemos que ˉF(cTτ)=ˉF(c)=cA[(F(x1),F(x2),...)]=cA Dados f∈Fn, t1,...,tn∈Tτ tenemos que ˉF(fTτ(t1,...,tn))=ˉF(f(t1,...,tn))=f(t1,...,tn)A[(F(x1),F(x2),...)]=fA(tA1[(F(x1),F(x2),...)],...,tAn[(F(x1),F(x2),...)])=fA(ˉF(t1),...,ˉF(tn)) con lo cual hemos probado que ˉF es un homomorfismo
7.11 (Teorema de Completitud Ecuacional). Sea (Σ,τ) una teoria ecuacional. Si (Σ,τ)⊨p≈q, entonces (Σ,τ)⊢ecp≈q.
Proof. Supongamos (Σ,τ)⊨p≈q. Sea θ la siguiente relacion binaria sobre Tτ: θ={(t,s):(Σ,τ)⊢ect≈s}. Dejamos al lector probar que θ es una congruencia de Tτ. Veamos que
(*) tTτ/θ[t1/θ,...,tn/θ]=t(t1,...,tn)/θ, para todo t1,...,tn, t=dt(x1,...,xn)
Por Corolario 7.2 tenemos que tTτ/θ[t1/θ,...,tn/θ]=tTτ[t1,...,tn]/θ Pero por Lema 7.54 tenemos que tTτ[t1,...,tn]=t(t1,...,tn) por lo cual (*) es verdadera.
Veamos que Tτ/θ⊨Σ. Sea t≈s un elemento de Σ, con t=dt(x1,...,xn) y s=ds(x1,...,xn). Veremos que Tτ/θ⊨t≈s, es decir veremos que tTτ/θ[t1/θ,...,tn/θ]=sTτ/θ[t1/θ,...,tn/θ] para todo t1/θ,...,tn/θ∈Tτ/θ. Notese que (Σ,τ)⊢ect(t1,...,tn)≈s(t1,...,tn) por lo cual t(t1,...,tn)/θ=s(t1,...,tn)/θ. Por (*) tenemos entonces tTτ/θ[t1/θ,...,tn/θ]=t(t1,...,tn)/θ=s(t1,...,tn)/θ=sTτ/θ[t1/θ,...,tn/θ], lo cual nos dice que Tτ/θ satisface la identidad t≈s.
Ya que Tτ/θ⊨Σ, por hipotesis tenemos que Tτ/θ⊨p≈q. Es decir que si p=dp(x1,...,xn) y q=dq(x1,...,xn) tenemos que pTτ/θ[t1/θ,...,tn/θ]=qTτ/θ[t1/θ,...,tn/θ], para todo t1,...,tn∈Tτ. En particular, tomando ti=xi, i=1,...,n tenemos que pTτ/θ[x1/θ,...,xn/θ]=qTτ/θ[x1/θ,...,xn/θ] lo cual por (*) nos dice que p/θ=q/θ, produciendo (Σ,τ)⊢ecp≈q.
7.6. Sea (Σ,τ) una teoria ecuacional. Si (Σ,τ)⊢p≈q, entonces (Σ,τ)⊢ecp≈q.