7.13 Logica ecuacional

Dados \(t,s\in T^{\tau}\), con \(t\approx s\) denotaremos la siguiente sentencia de tipo \(\tau\): \[\forall x_{1}...\forall x_{n}\;(t\equiv s)\] donde \(n\) es el menor \(j\) tal que \(\{x_{1},...,x_{j}\}\) 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\approx s\) denota a la sentencia \((t\equiv s)\), cuando \(t,s\in T_{c}^{\tau}\). Las sentencias \(t\approx s\), con \(t,s\in T^{\tau}\), seran llamadas identidades de tipo \(\tau\). Notese que \(\mathbf{A}\models t\approx s\) sii \(t^{\mathbf{A}}[\vec{a}]=s^{\mathbf{A}}[\vec{a}]\), para cada \(\vec{a}\in A^{\mathbf{N}}\). Tambien, si \(t=_{d}t(x_{1},...,x_{m})\) y \(s=_{d}s(x_{1},...,x_{m})\), entonces dado una \(\tau\)-algebra \(\mathbf{A}\), tenemos que \(\mathbf{A}\models t\approx s\) sii \(t^{\mathbf{A}}\left[a_{1},...,a_{m}\right]=s^{\mathbf{A}}\left[a_{1},...,a_{m}\right]\), para cada \((a_{1},...,a_{m})\in A^{m}\). (Independientemente de que \(m\) sea el menor \(j\) tal que \(\{x_{1},...,x_{j}\}\) contiene a las variables que ocurren en \(t\) y \(s\).)

Una teoria de primer orden \((\Sigma,\tau)\) sera llamada ecuacional si \(\tau\) es un tipo algebraico y cada elemento de \(\Sigma\) es una identidad de tipo \(\tau\). Por supuesto, el teorema de completitud de Godel nos garantiza que si \(T\) es una teoria ecuacional y \(T\vDash t\approx s\), entonces hay una prueba formal de \(t\approx s\) en \(T\). Sin envargo, en dicha prueba formal puede haber sentencias las cuales no sean identidades. Una pregunta interesante es la siguiente:

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

2. adhocprefix-adhocsufix Correcta: si hay una prueba ecuacional de \(t\approx s\) en \(T\), entonces \(t\approx s\) es verdadera en cada modelo de \(T\)

3. adhocprefix-adhocsufix Completa: si \(T\vDash t\approx s\), entonces hay una prueba ecuacional de \(t\approx 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.

7.13.1 Pruebas ecuacionales

Primero introducimos una serie de conjuntos los cuales poseen informacion deductiva ecuacional basica. Sea \[TransEc^{\tau}=\{(t\approx s,s\approx p,t\approx p):t,s,p\in T^{\tau}\}\] Diremos que \(\varphi\) se deduce de \(\psi_{1}\)y \(\psi_{2}\) por la regla de transitividad ecuacional, respecto a \(\tau\) para expresar que \((\psi_{1},\psi_{2},\varphi)\in TransEc^{\tau}\). Sea \[SimEc^{\tau}=\{(t\approx s,s\approx t):t,s\in T^{\tau}\}\] Diremos que \(\varphi\) se deduce de \(\psi_{1}\) por la regla de simetria ecuacional, respecto a \(\tau\) para expresar que \((\psi_{1},\varphi)\in SimEc^{\tau}\). Sea \[\begin{array}{c} SubsEc^{\tau}=\{(t\approx s,t(p_{1},...,p_{n})\approx s(p_{1},...,p_{n})):t=_{d}t(x_{1},...,x_{n})\\ s=_{d}s(x_{1},...,x_{n})\ \mathrm{y}\ p_{1},...,p_{n}\in T^{\tau}\} \end{array}\] Diremos que \(\varphi\) se deduce de \(\psi_{1}\) por la regla de substitucion ecuacional, respecto a \(\tau\) para expresar que \((\psi_{1},\varphi)\in SubsEc^{\tau}\). Sea \[\begin{array}{c} ReempEc^{\tau}=\{(t\approx s,r\approx\tilde{r}):t,s,r\in T^{\tau}\ \text{\textrm{y}}\ \tilde{r}=\mathrm{resultado}\\ \mathrm{de\ reemplazar\ algunas\ ocurrencias\ de\ }t\ \mathrm{en\ }r\ \mathrm{por\ }s\} \end{array}\] Diremos que \(\varphi\) se deduce de \(\psi_{1}\) por la regla de reemplazo ecuacional, respecto a \(\tau\) para expresar que \((\psi_{1},\varphi)\in ReempEc^{\tau}\).

La identidad \(x_{1}\approx x_{1}\) sera llamada axioma logico ecuacional de tipo \(\tau\). Notese que dicha identidad no es ni mas ni menos que la sentencia \(\forall x_{1}(x_{1}\equiv x_{1})\) la cual es universalmente valida.

7.13.1.1 Definicion de prueba ecuacional

Dada una teoria ecuacional \((\Sigma,\tau)\) y una identidad \(p\approx q\) de tipo \(\tau\), una prueba ecuacional de \(p\approx q\) en \((\Sigma,\tau)\) sera una palabra \(\boldsymbol{\varphi}\in S^{\tau+}\) tal que

1. adhocprefix(1)adhocsufix Cada \(\boldsymbol{\varphi}_{k}\), con \(k=1,...,n(\boldsymbol{\varphi})\), es una identidad de tipo \(\tau\) y \(\boldsymbol{\varphi}_{n(\boldsymbol{\varphi})}=p\approx q\)

2. adhocprefix(2)adhocsufix Para cada \(k=1,...,n(\boldsymbol{\varphi})\), se da alguna de las siguientes

   1. adhocprefix(a)adhocsufix \(\boldsymbol{\varphi}_{k}=x_{1}\approx x_{1}\)

   2. adhocprefix(b)adhocsufix \(\boldsymbol{\varphi}_{k}\in\Sigma\)

   3. adhocprefix(c)adhocsufix hay \(i,j<k\) tales que \(\boldsymbol{\varphi}_{k}\) se deduce por la regla de transitividad ecuacional a partir de \(\boldsymbol{\varphi}_{i}\) y \(\boldsymbol{\varphi}_{j}\)

   4. adhocprefix(d)adhocsufix hay \(i<k\) tal que \(\boldsymbol{\varphi}_{k}\) se deduce por la regla de simetria ecuacional a partir de \(\boldsymbol{\varphi}_{i}\)

   5. adhocprefix(e)adhocsufix hay \(i<k\) tal que \(\boldsymbol{\varphi}_{k}\) se deduce por la regla de substitucion ecuacional a partir de \(\boldsymbol{\varphi}_{i}\)

   6. adhocprefix(f)adhocsufix hay \(i<k\) tal que \(\boldsymbol{\varphi}_{k}\) se deduce por la regla de reemplazo ecuacional a partir de \(\boldsymbol{\varphi}_{i}\)

Escribiremos \((\Sigma,\tau)\vdash_{ec}p\approx q\) cuando haya una prueba ecuacional de \(p\approx q\) en \((\Sigma,\tau)\).

7.13.2 Correccion ecuacional

Para probar que el concepto de prueba ecuacional es correcto nos hara falta el siguiente lema.

Proof. Veamos que la regla de reemplazo es universal. Basta con ver por induccion en \(k\) que

1. adhocprefix-adhocsufix Teo\(_{k}\): Sean \(t,s\in T^{\tau}\), \(r\in T_{k}^{\tau}\) y sea \(\mathbf{A}\) una \(\tau\)-algebra tal que \(t^{\mathbf{A}}[\vec{a}]=s^{\mathbf{A}}[\vec{a}]\), para cada \(\vec{a}\in A^{\mathbf{N}}\). Entonces \(r^{\mathbf{A}}[\vec{a}]=\tilde{r}^{\mathbf{A}}[\vec{a}]\), para cada \(\vec{a}\in A^{\mathbf{N}}\), donde \(\tilde{r}\) es el resultado de reemplazar algunas ocurrencias de \(t\) en \(r\) por \(s.\)

La prueba de Teo\(_{0}\) es dejada al lector. Asumamos que vale Teo\(_{k}\) y probemos que vale Teo\(_{k+1}\). Sean \(t,s\in T^{\tau}\), \(r\in T_{k+1}^{\tau}-T_{k}^{\tau}\) y sea \(\mathbf{A}\) una \(\tau\)-algebra tal que \(t^{\mathbf{A}}[\vec{a}]=s^{\mathbf{A}}[\vec{a}]\), para cada \(\vec{a}\in A^{\mathbf{N}}\). Sea \(\tilde{r}\) el resultado de reemplazar algunas ocurrencias de \(t\) en \(r\) por \(s\). El caso \(t=r\) es trivial. Supongamos entonces que \(t\neq r\). Supongamos \(r=f(r_{1},...,r_{n})\), con \(r_{1},...,r_{n}\in T_{k}^{\tau}\) y \(f\in\mathcal{F}_{n}\). Notese que por Lema 7.7 tenemos que \(\tilde{r}=f(\tilde{r}_{1},...,\tilde{r}_{n})\), donde cada \(\tilde{r}_{i}\) es el resultado de reemplazar algunas ocurrencias de \(t\) en \(r_{i}\) por \(s\). Para \(\vec{a}\in A^{\mathbf{N}}\) se tiene que \[\begin{array}{cclll} r^{\mathbf{A}}[\vec{a}] & = & f(r_{1},...,r_{n})^{\mathbf{A}}[\vec{a}]\\ & = & f^{\mathbf{A}}(r_{1}^{\mathbf{A}}[\vec{a}],...,r_{n}^{\mathbf{A}}[\vec{a}])\\ & = & f^{\mathbf{A}}(\tilde{r}_{1}^{\mathbf{A}}[\vec{a}],...,\tilde{r}_{n}^{\mathbf{A}}[\vec{a}]) & & \text{por Teo}_{k}\\ & = & f(\tilde{r}_{1},...,\tilde{r}_{n})^{\mathbf{A}}[\vec{a}]\\ & = & \tilde{r}^{\mathbf{A}}[\vec{a}] \end{array}\] lo cual prueba Teo\(_{k+1}\)

Veamos que la regla de substitucion es universal. Supongamos \(\mathbf{A}\models t\approx s\), con \(t=_{d}t(x_{1},...,x_{n})\) y \(s=_{d}s(x_{1},...,x_{n})\). Veremos que entonces \(\mathbf{A}\models t(p_{1},...,p_{n})\approx s(p_{1},...,p_{n}).\) Supongamos que \(p_{i}=_{d}p_{i}(x_{1},...,x_{m})\), para cada \(i=1,...,n.\) Por (a) del Lema 7.4, tenemos que \[\begin{aligned} t(p_{1},...,p_{n}) & =_{d}t(p_{1},...,p_{n})(x_{1},...,x_{m})\\ s(p_{1},...,p_{n}) & =_{d}s(p_{1},...,p_{n})(x_{1},...,x_{m}) \end{aligned}\] Sea \(\vec{a}\in A^{m}\). Tenemos que \[\begin{array}{rcl} t(p_{1},...,p_{n})^{\mathbf{A}}\left[\vec{a}\right] & = & t^{\mathbf{A}}\left[p_{1}^{\mathbf{A}}\left[\vec{a}\right],...,p_{n}^{\mathbf{A}}\left[\vec{a}\right]\right]\\ & = & s^{\mathbf{A}}\left[p_{1}^{\mathbf{A}}\left[\vec{a}\right],...,p_{n}^{\mathbf{A}}\left[\vec{a}\right]\right]\\ & = & s(p_{1},...,p_{n})^{\mathbf{A}}\left[\vec{a}\right] \end{array}\] lo cual nos dice que \(\mathbf{A}\models t(p_{1},...,p_{n})\approx s(p_{1},...,p_{n})\)  

Proof. Sea \(\boldsymbol{\varphi}\) una prueba ecuacional de \(p\approx q\) en \((\Sigma,\tau)\). Usando el lema anterior se puede probar facilmente por induccion en \(i\) que \((\Sigma,\tau)\models\boldsymbol{\varphi}_{i}\), por lo cual \((\Sigma,\tau)\models p\approx q\)  

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 \(\tau\), hay una forma natural de definir un algebra \(\mathbf{T}^{\tau}\) cuyo universo es \(T^{\tau}\), de la siguiente manera

1. adhocprefix(1)adhocsufix \(c^{\mathbf{T}^{\tau}}=c\), para cada \(c\in\mathcal{C}\)

2. adhocprefix(2)adhocsufix \(f^{\mathbf{T}^{\tau}}(t_{1},...,t_{n})=f(t_{1},...,t_{n})\), para todo \(t_{1},...,t_{n}\in T^{\tau}\), \(f\in\mathcal{F}_{n}\).

Llamaremos a \(\mathbf{T}^{\tau}\) el algebra de terminos de tipo \(\tau\).

Proof. Para cada \(k\geq0\), sea

1. adhocprefix-adhocsufix Teo\(_{k}\): Dados \(t_{1},...,t_{n}\in T^{\tau}\) y \(t=_{d}t(x_{1},...,x_{n})\in T_{k}^{\tau}\), se tiene que \(t^{\mathbf{T}^{\tau}}[t_{1},...,t_{n}]=t(t_{1},...,t_{n})\).

Veamos que es cierto Teo\(_{0}\). Hay dos casos

Caso \(t=_{d}t(x_{1},...,x_{n})=c\in\mathcal{C}\).

Entonces tenemos \[\begin{array}{cll} t^{\mathbf{T}^{\tau}}[t_{1},...,t_{n}] & = & c^{\mathbf{T}^{\tau}}\\ & = & c\\ & = & t(t_{1},...,t_{n}) \end{array}\]

Caso \(t=_{d}t(x_{1},...,x_{n})=x_{i}\), para algun \(i\).

Entonces tenemos \[\begin{array}{cll} t^{\mathbf{T}^{\tau}}[t_{1},...,t_{n}] & = & t_{i}\\ & = & t(t_{1},...,t_{n}) \end{array}\] Veamos que Teo\(_{k}\) implica Teo\(_{k+1}\). Supongamos que vale Teo\(_{k}\). Sean \(t_{1},...,t_{n}\in T^{\tau}\) y \(t=_{d}t(x_{1},...,x_{n})\in T_{k+1}^{\tau}-T_{k}^{\tau}\). Hay \(f\in\mathcal{F}_{m}\), con \(m\geq1\), y terminos \(s_{1},...,s_{m}\in T_{k}^{\tau}\) tales que \(t=f(s_{1},...,s_{m})\). Notese que \(s_{i}=_{d}s_{i}(x_{1},...,x_{n})\), \(i=1,...,m\). Tenemos entonces que \[\begin{array}{lll} t^{\mathbf{T}^{\tau}}[t_{1},...,t_{n}] & = & f(s_{1},...,s_{m})^{\mathbf{T}^{\tau}}[t_{1},...,t_{n}]\\ & = & f^{\mathbf{T}^{\tau}}(s_{1}^{\mathbf{T}^{\tau}}[t_{1},...,t_{n}],...,s_{m}^{\mathbf{T}^{\tau}}[t_{1},...,t_{n}])\\ & = & f^{\mathbf{T}^{\tau}}(s_{1}(t_{1},...,t_{n}),...,s_{m}(t_{1},...,t_{n}))\\ & = & f(s_{1}(t_{1},...,t_{n}),...,s_{m}(t_{1},...,t_{n}))\\ & = & t(t_{1},...,t_{n}) \end{array}\] con lo cual vale Teo\(_{k+1}\)  

El algebra de terminos tiene la siguiente propiedad fundamental:

Proof. Definamos \(\bar{F}\) de la siguiente manera: \[\bar{F}(t)=t^{\mathbf{A}}[(F(x_{1}),F(x_{2}),...)]\] Es claro que \(\bar{F}\) extiende a \(F\). Veamos que es un homomorfismo. Dada \(c\in\mathcal{C}\), tenemos que \[\begin{array}{lll} \bar{F}(c^{\mathbf{T}^{\tau}}) & = & \bar{F}(c)\\ & = & c^{\mathbf{A}}[(F(x_{1}),F(x_{2}),...)]\\ & = & c^{\mathbf{A}} \end{array}\] Dados \(f\in\mathcal{F}_{n}\), \(t_{1},...,t_{n}\in T^{\tau}\) tenemos que \[\begin{array}{lll} \bar{F}(f^{\mathbf{T}^{\tau}}(t_{1},...,t_{n})) & = & \bar{F}(f(t_{1},...,t_{n}))\\ & = & f(t_{1},...,t_{n})^{\mathbf{A}}[(F(x_{1}),F(x_{2}),...)]\\ & = & f^{\mathbf{A}}(t_{1}^{\mathbf{A}}[(F(x_{1}),F(x_{2}),...)],...,t_{n}^{\mathbf{A}}[(F(x_{1}),F(x_{2}),...)])\\ & = & f^{\mathbf{A}}(\bar{F}(t_{1}),...,\bar{F}(t_{n})) \end{array}\] con lo cual hemos probado que \(\bar{F}\) es un homomorfismo  

Proof. Supongamos \((\Sigma,\tau)\models p\approx q.\) Sea \(\theta\) la siguiente relacion binaria sobre \(T^{\tau}\): \[\theta=\{(t,s):(\Sigma,\tau)\vdash_{ec}t\approx s\}.\] Dejamos al lector probar que \(\theta\) es una congruencia de \(\mathbf{T}^{\tau}\). Veamos que

1. adhocprefix(*)adhocsufix \(t^{\mathbf{T}^{\tau}/\theta}[t_{1}/\theta,...,t_{n}/\theta]=t(t_{1},...,t_{n})/\theta\), para todo \(t_{1},...,t_{n}\), \(t=_{d}t(x_{1},...,x_{n})\)

Por Corolario 7.2 tenemos que \[t^{\mathbf{T}^{\tau}/\theta}[t_{1}/\theta,...,t_{n}/\theta]=t^{\mathbf{T}^{\tau}}[t_{1},...,t_{n}]/\theta\] Pero por Lema 7.53 tenemos que \(t^{\mathbf{T}^{\tau}}[t_{1},...,t_{n}]=t(t_{1},...,t_{n})\) por lo cual (*) es verdadera.

Veamos que \(\mathbf{T}^{\tau}/\theta\models\Sigma.\) Sea \(t\approx s\) un elemento de \(\Sigma\), con \(t=_{d}t(x_{1},...,x_{n})\) y \(s=_{d}s(x_{1},...,x_{n}).\) Veremos que \(\mathbf{T}^{\tau}/\theta\models t\approx s\), es decir veremos que \[t^{\mathbf{T}^{\tau}/\theta}[t_{1}/\theta,...,t_{n}/\theta]=s^{\mathbf{T}^{\tau}/\theta}[t_{1}/\theta,...,t_{n}/\theta]\] para todo \(t_{1}/\theta,...,t_{n}/\theta\in T^{\tau}/\theta\). Notese que \[(\Sigma,\tau)\vdash_{ec}t(t_{1},...,t_{n})\approx s(t_{1},...,t_{n})\] por lo cual \(t(t_{1},...,t_{n})/\theta=s(t_{1},...,t_{n})/\theta.\) Por (*) tenemos entonces \[t^{\mathbf{T}^{\tau}/\theta}[t_{1}/\theta,...,t_{n}/\theta]=t(t_{1},...,t_{n})/\theta=s(t_{1},...,t_{n})/\theta=s^{\mathbf{T}^{\tau}/\theta}[t_{1}/\theta,...,t_{n}/\theta],\] lo cual nos dice que \(\mathbf{T}^{\tau}/\theta\) satisface la identidad \(t\approx s.\)

Ya que \(\mathbf{T}^{\tau}/\theta\models\Sigma\), por hipotesis tenemos que \(\mathbf{T}^{\tau}/\theta\models p\approx q.\) Es decir que si \(p=_{d}p(x_{1},...,x_{n})\) y \(q=_{d}q(x_{1},...,x_{n})\) tenemos que \(p^{\mathbf{T}^{\tau}/\theta}[t_{1}/\theta,...,t_{n}/\theta]=q^{\mathbf{T}^{\tau}/\theta}[t_{1}/\theta,...,t_{n}/\theta]\), para todo \(t_{1},...,t_{n}\in T^{\tau}\). En particular, tomando \(t_{i}=x_{i}\), \(i=1,...,n\) tenemos que \[p^{\mathbf{T}^{\tau}/\theta}[x_{1}/\theta,...,x_{n}/\theta]=q^{\mathbf{T}^{\tau}/\theta}[x_{1}/\theta,...,x_{n}/\theta]\] lo cual por (*) nos dice que \(p/\theta=q/\theta\), produciendo \((\Sigma,\tau)\vdash_{ec}p\approx q\).