Loading [MathJax]/jax/output/CommonHTML/jax.js

7.13 Logica ecuacional

Dados t,sTτ, con ts denotaremos la siguiente sentencia de tipo τ: x1...xn(ts) 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 ts denota a la sentencia (ts), cuando t,sTτc. Las sentencias ts, con t,sTτ, seran llamadas identidades de tipo τ. Notese que Ats sii tA[a]=sA[a], para cada aAN. Tambien, si t=dt(x1,...,xm) y s=ds(x1,...,xm), entonces dado una τ-algebra A, tenemos que Ats 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 Tts, entonces hay una prueba formal de ts en T. Sin envargo, en dicha prueba formal puede haber sentencias las cuales no sean identidades. Una pregunta interesante es la siguiente:

  1. Pregunta: ¿Hay una nocion de "prueba ecuacional" la cual sea:

  2. - Correcta: si hay una prueba ecuacional de ts en T, entonces ts es verdadera en cada modelo de T

  3. - Completa: si Tts, entonces hay una prueba ecuacional de ts 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.

7.13.1 Pruebas ecuacionales

Primero introducimos una serie de conjuntos los cuales poseen informacion deductiva ecuacional basica. Sea TransEcτ={(ts,sp,tp):t,s,pTτ} Diremos que φ se deduce de ψ1y ψ2 por la regla de transitividad ecuacional, respecto a τ para expresar que (ψ1,ψ2,φ)TransEcτ. Sea SimEcτ={(ts,st):t,sTτ} Diremos que φ se deduce de ψ1 por la regla de simetria ecuacional, respecto a τ para expresar que (ψ1,φ)SimEcτ. Sea SubsEcτ={(ts,t(p1,...,pn)s(p1,...,pn)):t=dt(x1,...,xn)s=ds(x1,...,xn) y p1,...,pnTτ} Diremos que φ se deduce de ψ1 por la regla de substitucion ecuacional, respecto a τ para expresar que (ψ1,φ)SubsEcτ. Sea ReempEcτ={(ts,r˜r):t,s,rTτ \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 x1x1 sera llamada axioma logico ecuacional de tipo τ. Notese que dicha identidad no es ni mas ni menos que la sentencia x1(x1x1) la cual es universalmente valida.

7.13.1.1 Definicion de prueba ecuacional

Dada una teoria ecuacional (Σ,τ) y una identidad pq de tipo τ, una prueba ecuacional de pq en (Σ,τ) sera una palabra φSτ+ tal que

  1. (1) Cada φk, con k=1,...,n(φ), es una identidad de tipo τ y φn(φ)=pq

  2. (2) Para cada k=1,...,n(φ), se da alguna de las siguientes

    1. (a) φk=x1x1

    2. (b) φkΣ

    3. (c) hay i,j<k tales que φk se deduce por la regla de transitividad ecuacional a partir de φi y φj

    4. (d) hay i<k tal que φk se deduce por la regla de simetria ecuacional a partir de φi

    5. (e) hay i<k tal que φk se deduce por la regla de substitucion ecuacional a partir de φi

    6. (f) hay i<k tal que φk se deduce por la regla de reemplazo ecuacional a partir de φi

Escribiremos (Σ,τ)ecpq cuando haya una prueba ecuacional de pq en (Σ,τ).

7.13.2 Correccion ecuacional

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

  1. - Teok: Sean t,sTτ, rTτk y sea A una τ-algebra tal que tA[a]=sA[a], para cada aAN. Entonces rA[a]=˜rA[a], para cada aAN, 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,sTτ, rTτk+1Tτk y sea A una τ-algebra tal que tA[a]=sA[a], para cada aAN. Sea ˜r el resultado de reemplazar algunas ocurrencias de t en r por s. El caso t=r es trivial. Supongamos entonces que tr. Supongamos r=f(r1,...,rn), con r1,...,rnTτk y fFn. 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 aAN 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 Ats, con t=dt(x1,...,xn) y s=ds(x1,...,xn). Veremos que entonces At(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 aAm. 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 At(p1,...,pn)s(p1,...,pn)  


7.10 (Teorema de Correccion de pruebas ecuacionales ). Si (Σ,τ)ecpq, entonces (Σ,τ)pq.

Proof. Sea φ una prueba ecuacional de pq en (Σ,τ). Usando el lema anterior se puede probar facilmente por induccion en i que (Σ,τ)φi, por lo cual (Σ,τ)pq  


7.13.3 Completitud ecuacional

Para probar que el concepto de prueba ecuacional es completo nos haran falta algunos resultados basicos que tienen interes por si mismos.

7.13.3.1 El algebra de terminos

Dado un tipo algebraico τ, hay una forma natural de definir un algebra Tτ cuyo universo es Tτ, de la siguiente manera

  1. (1) cTτ=c, para cada cC

  2. (2) fTτ(t1,...,tn)=f(t1,...,tn), para todo t1,...,tnTτ, fFn.

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 k0, sea

  1. - Teok: Dados t1,...,tnTτ 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)=cC.

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,...,tnTτ y t=dt(x1,...,xn)Tτk+1Tτk. Hay fFm, con m1, y terminos s1,...,smTτ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:VarA, 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 cC, tenemos que ˉF(cTτ)=ˉF(c)=cA[(F(x1),F(x2),...)]=cA Dados fFn, t1,...,tnTτ 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 (Σ,τ)pq, entonces (Σ,τ)ecpq.

Proof. Supongamos (Σ,τ)pq. Sea θ la siguiente relacion binaria sobre Tτ: θ={(t,s):(Σ,τ)ects}. Dejamos al lector probar que θ es una congruencia de Tτ. Veamos que

  1. (*) 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 ts un elemento de Σ, con t=dt(x1,...,xn) y s=ds(x1,...,xn). Veremos que Tτ/θts, 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 ts.

Ya que Tτ/θΣ, por hipotesis tenemos que Tτ/θpq. Es decir que si p=dp(x1,...,xn) y q=dq(x1,...,xn) tenemos que pTτ/θ[t1/θ,...,tn/θ]=qTτ/θ[t1/θ,...,tn/θ], para todo t1,...,tnTτ. 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 (Σ,τ)ecpq.  


7.6. Sea (Σ,τ) una teoria ecuacional. Si (Σ,τ)pq, entonces (Σ,τ)ecpq.