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\). Nótese que este \(n\) es \(0\) cuando \(t\) y \(s\) son término 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}\), serán llamadas identidades de tipo \(\tau\). Nótese 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}}\). También, si \(t=_{d}t(x_{1},...,x_{m})\) y \(s=_{d}s(x_{1},...,x_{m})\), entonces dado una \(\tau\)-álgebra \(\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 teoría de primer orden \((\Sigma,\tau)\) será 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 teoría ecuacional y \(T\vDash t\approx s\), entonces hay una prueba formal de \(t\approx s\) en \(T\). Sin embargo, en dicha prueba formal puede haber sentencias las cuales no sean identidades. Una pregunta interesante es la siguiente:
Pregunta: ¿Hay una noción de "prueba ecuacional" la cual sea:
Correcta: si hay una prueba ecuacional de \(t\approx s\) en \(T\), entonces \(t\approx s\) es verdadera en cada modelo de \(T\)
Completa: si \(T\vDash t\approx s\), entonces hay una prueba ecuacional de \(t\approx s\) en \(T\)?
En esta sección veremos que, tal como lo probo Birkhoff, esto es posible y que la noción de prueba ecuacional que se puede dar es muy natural y simple, es decir si sabemos que en una teoría todos los axiomas son identidades, entonces a los fines de probar identidades las pruebas de primer orden clásicas pueden ser reemplazadas por pruebas con un formato mucho mas amigable.
Primero introducimos una serie de conjuntos los cuales poseen información deductiva ecuacional básica. 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 simetría 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}\] Nótese que si \(t=_{d}t(x_{1},...,x_{n})\in T^{\tau}\) y \(p_{1},...,p_{n}\in T^{\tau}\), el Teorema de Reemplazo para Términos nos garantiza que \(t(p_{1},...,p_{n})\) es un término. Diremos que \(\varphi\) se deduce de \(\psi_{1}\) por la regla de substitución 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}\] Nótese que la definición de \(\tilde{r}\) es inambigua ya que por (e) del Lema de Ocurrencias de Términos en Términos tenemos que las distintas ocurrencias de \(t\) en \(r\) son disjuntas. Además (f) del mismo lema nos garantiza que \(\tilde{r}\) es un término. 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}\) será llamada axioma lógico ecuacional de tipo \(\tau\). Nótese que dicha identidad no es ni mas ni menos que la sentencia \(\forall x_{1}(x_{1}\equiv x_{1})\) la cual es universalmente válida.
Dada una teoría ecuacional \((\Sigma,\tau)\) y una identidad \(p\approx q\) de tipo \(\tau\), una prueba ecuacional de \(p\approx q\) en \((\Sigma,\tau)\) será una palabra \(\boldsymbol{\varphi}\in S^{\tau+}\) tal que
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\)
adhocprefix(2)adhocsufix Para cada \(k=1,...,n(\boldsymbol{\varphi})\), se da alguna de las siguientes
adhocprefix(a)adhocsufix \(\boldsymbol{\varphi}_{k}=x_{1}\approx x_{1}\)
adhocprefix(b)adhocsufix \(\boldsymbol{\varphi}_{k}\in\Sigma\)
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}\)
adhocprefix(d)adhocsufix hay \(i<k\) tal que \(\boldsymbol{\varphi}_{k}\) se deduce por la regla de simetría ecuacional a partir de \(\boldsymbol{\varphi}_{i}\)
adhocprefix(e)adhocsufix hay \(i<k\) tal que \(\boldsymbol{\varphi}_{k}\) se deduce por la regla de substitución ecuacional a partir de \(\boldsymbol{\varphi}_{i}\)
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)\).
Para probar que el concepto de prueba ecuacional es correcto nos hará falta el siguiente lema.
7.60. Todas las reglas introducidas en la sección anterior son universales en el sentido que si \(\varphi\) se deduce de \(\psi_{1},...,\psi_{k}\) por alguna de estas reglas, entonces \(\left((\psi_{1}\wedge...\wedge\psi_{k})\rightarrow\varphi\right)\) es una sentencia universalmente válida.
Proof. Veamos que la regla de reemplazo es universal. Usaremos la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:
adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Sean \(t,s\in T^{\tau}\) y \(r\in T_{k}^{\tau}\). Sea \(\tilde{r}\) el resultado de reemplazar algunas (posiblemente \(0\)) ocurrencias de \(t\) en \(r\) por \(s.\) Sea \(\mathbf{A}\) una \(\tau\)-álgebra 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}}\).
Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).
Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. Supongamos \(t,s\in T^{\tau}\) y \(r\in T_{0}^{\tau}\). Sea \(\tilde{r}\) el resultado de reemplazar algunas (posiblemente \(0\)) ocurrencias de \(t\) en \(r\) por \(s.\) Sea \(\mathbf{A}\) una \(\tau\)-álgebra tal que \(t^{\mathbf{A}}[\vec{a}]=s^{\mathbf{A}}[\vec{a}]\), para cada \(\vec{a}\in A^{\mathbf{N}}\). Si reemplazamos \(0\) ocurrencias de \(t\) en \(r\) para obtener \(\tilde{r}\) es claro que \(\tilde{r}=r\) por lo cual se cumple la conclusión de \(\mathrm{Enu}_{0}\). Si efectivamente reemplazamos alguna ocurrencia de \(t\) en \(r\) para obtener \(\tilde{r}\), los ítems (a) y (b) del Lema de Ocurrencias de Términos en Términos nos dicen que \(t\) debe ser igual a \(r\) por lo cual \(\tilde{r}=s\). Pero entonces es claro que \(r^{\mathbf{A}}[\vec{a}]=\tilde{r}^{\mathbf{A}}[\vec{a}]\), para cada \(\vec{a}\in A^{\mathbf{N}}\) ya que \(r=t\) y por hipótesis \(t^{\mathbf{A}}[\vec{a}]=s^{\mathbf{A}}[\vec{a}]\), para cada \(\vec{a}\in A^{\mathbf{N}}\).
Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Sean \(t,s\in T^{\tau}\) y \(r\in T_{k+1}^{\tau}\). Sea \(\tilde{r}\) el resultado de reemplazar algunas (posiblemente \(0\)) ocurrencias de \(t\) en \(r\) por \(s.\) Sea \(\mathbf{A}\) una \(\tau\)-álgebra tal que \(t^{\mathbf{A}}[\vec{a}]=s^{\mathbf{A}}[\vec{a}]\), para cada \(\vec{a}\in A^{\mathbf{N}}\). Por definición de \(T_{k+1}^{\tau}\) hay dos casos.
Caso \(r\in T_{k}^{\tau}\). Trivial ya que vale \(\mathrm{Enu}_{k}\).
Caso \(r=f(r_{1},...,r_{n})\), con \(r_{1},...,r_{n}\in T_{k}^{\tau}\) y \(f\in\mathcal{F}_{n}\). Si \(t=r\) es claro que vale la conclusón de \(\mathrm{Enu}_{k+1}\). Supongamos entonces que \(t\neq r\). Por (c) del Lema de Ocurrencias de Términos en Términos tenemos que las ocurrencias de \(t\) en \(r\) suceden dentro de los \(r_{i}\). O sea 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 \ensuremath{\mathrm{Enu}_{k}}})\\ & = & f(\tilde{r}_{1},...,\tilde{r}_{n})^{\mathbf{A}}[\vec{a}]\\ & = & \tilde{r}^{\mathbf{A}}[\vec{a}] \end{array}\] lo cual nos dice que \(\mathrm{Enu}_{k+1}\) es verdadero.
Veamos que la regla de substitución 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})\). Sea \(m\) el menor elemento de \(\omega\) tal que podamos hacer las declaraciones \(p_{i}=_{d}p_{i}(x_{1},...,x_{m})\), para cada \(i=1,...,n.\) Notar que \(t(p_{1},...,p_{n})\approx s(p_{1},...,p_{n})\) es la sentencia \[\forall x_{1}...\forall x_{m}(t(p_{1},...,p_{n})\equiv s(p_{1},...,p_{n}))\] Por (b) del Teorema de Reemplazo para Términos, podemos hacer las declaraciones \[\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}\] O sea que \(\mathbf{A}\models t(p_{1},...,p_{n})\approx s(p_{1},...,p_{n})\) si y solo si \(t(p_{1},...,p_{n})^{\mathbf{A}}\left[\vec{a}\right]=s(p_{1},...,p_{n})^{\mathbf{A}}\left[\vec{a}\right]\), para cada \(\vec{a}\in A^{m}\). Pero por (c) del mismo teorema 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}\] para cada \(\vec{a}\in A^{m}\), lo cual nos dice que \(\mathbf{A}\models t(p_{1},...,p_{n})\approx s(p_{1},...,p_{n})\).
7.10 (Teorema de Corrección Ecuacional). Si \((\Sigma,\tau)\vdash_{ec}p\approx q\), entonces \((\Sigma,\tau)\models p\approx q\).
Proof. Sea \(\boldsymbol{\varphi}\) una prueba ecuacional de \(p\approx q\) en \((\Sigma,\tau)\). Probaremos que \((\Sigma,\tau)\models p\approx q\). Sea \(\mathbf{A}\) una \(\tau\)-álgebra la cual es un modelo de \((\Sigma,\tau)\). Probaremos que \(\mathbf{A}\models p\approx q\). Usaremos la Regla de Inducción Completa desde 1 hasta \(n(\boldsymbol{\varphi})\). Para cada \(k\in\{1,...,n(\boldsymbol{\varphi})\}\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:
adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix \(\mathbf{A}\models\boldsymbol{\varphi}_{k}\)
Ya que \(\boldsymbol{\varphi}_{n(\boldsymbol{\varphi})}=p\approx q\) tenemos que \(\mathrm{Enu}_{n(\boldsymbol{\varphi})}=\mathbf{A}\models p\approx q\). Hagamos entonces lo que nos encomienda la Regla de Inducción Completa desde \(1\) hasta \(n(\boldsymbol{\varphi}).\)
Prueba de que \(\mathrm{Enu}_{1}\) es verdadero. Nótese que por la definición de prueba ecuacional, \(\boldsymbol{\varphi}_{1}=x_{1}\approx x_{1}\) o \(\boldsymbol{\varphi}_{1}\in\Sigma\). En los dos casos es claro que \(\mathbf{A}\models\boldsymbol{\varphi}_{1}\) por lo que \(\mathrm{Enu}_{1}\) es verdadero.
Prueba de que para cada \(k\in\{1,...,n(\boldsymbol{\varphi})-1\}\), si \(\mathrm{Enu}_{j}\) es verdadero para \(j\in\{1,...,k\}\), entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que \(\mathrm{Enu}_{j}\) es verdadero para \(j\in\{1,...,k\}\). Probaremos que \(\mathbf{A}\models\boldsymbol{\varphi}_{k+1}\). Por la definición de prueba ecuacional tenemos que se da alguna de las siguientes
adhocprefix(a)adhocsufix \(\boldsymbol{\varphi}_{k+1}=x_{1}\approx x_{1}\)
adhocprefix(b)adhocsufix \(\boldsymbol{\varphi}_{k+1}\in\Sigma\)
adhocprefix(c)adhocsufix hay \(i,j<k+1\) tales que \(\boldsymbol{\varphi}_{k+1}\) se deduce por la regla de transitividad ecuacional a partir de \(\boldsymbol{\varphi}_{i}\) y \(\boldsymbol{\varphi}_{j}\)
adhocprefix(d)adhocsufix hay \(i<k+1\) tal que \(\boldsymbol{\varphi}_{k+1}\) se deduce por la regla de simetría ecuacional a partir de \(\boldsymbol{\varphi}_{i}\)
adhocprefix(e)adhocsufix hay \(i<k+1\) tal que \(\boldsymbol{\varphi}_{k+1}\) se deduce por la regla de substitución ecuacional a partir de \(\boldsymbol{\varphi}_{i}\)
adhocprefix(f)adhocsufix hay \(i<k+1\) tal que \(\boldsymbol{\varphi}_{k+1}\) se deduce por la regla de reemplazo ecuacional a partir de \(\boldsymbol{\varphi}_{i}\)
Supongamos por ejemplo se da (c). Ya que \(i,j\in\{1,...,k\}\) tenemos que \(\mathrm{Enu}_{i}\) y \(\mathrm{Enu}_{j}\) son verdaderos. Es decir \(\mathbf{A}\models\boldsymbol{\varphi}_{i}\) y \(\mathbf{A}\models\boldsymbol{\varphi}_{j}\). El lema anterior entonces nos garantiza que \(\mathbf{A}\models\boldsymbol{\varphi}_{k+1}\). Dejamos al lector los otros casos.
Para probar que el concepto de prueba ecuacional es completo nos harán falta algunos resultados básicos que tienen interés por si mismos.
Dado un tipo algebraico \(\tau\), hay una forma natural de definir un álgebra \(\mathbf{T}^{\tau}\) cuyo universo es \(T^{\tau}\), de la siguiente manera
adhocprefix(1)adhocsufix \(c^{\mathbf{T}^{\tau}}=c\), para cada \(c\in\mathcal{C}\)
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 álgebra de términos de tipo \(\tau\). Veamos un ejemplo. Supongamos \(\tau=(\emptyset,\{f\},\emptyset,\{(f,1)\}).\) Entonces el universo de \(\mathbf{T}^{\tau}\) es \[\{x_{1},f(x_{1}),f(f(x_{1})),...\}\cup\{x_{2},f(x_{2}),f(f(x_{2})),...\}\cup...\]
La función que interpreta a \(f\) en \(\mathbf{T}^{\tau}\) es la que a cada elemento del conjunto anterior le asigna el primer elemento que esta a su derecha. Nótese entonces que \(\mathbf{T}^{\tau}\) resulta isomorfa al álgebra \(\mathbf{A}\) definida por \[\begin{aligned} A & =\mathbf{N}\times\mathbf{N}\\ f^{\mathbf{A}}(n,m) & =(n,m+1) \end{aligned}\]
7.61. Dados \(t_{1},...,t_{n}\in T^{\tau}\), con \(n\in\omega\) y \(t=_{d}t(x_{1},...,x_{n})\in T^{\tau}\), se tiene que \(t^{\mathbf{T}^{\tau}}[t_{1},...,t_{n}]=t(t_{1},...,t_{n})\).
Proof. Usaremos la Regla de Inducción desde 0. Para cada \(k\in\omega\) sea \(\mathrm{Enu}_{k}\) el siguiente enunciado:
adhocprefix\(\mathrm{Enu}_{k}\):adhocsufix Dados \(t_{1},...,t_{n}\in T^{\tau}\), con \(n\in\omega\) 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})\).
Hagamos entonces lo que nos encomienda la Regla de Inducción desde \(0\).
Prueba de que \(\mathrm{Enu}_{0}\) es verdadero. 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 algún \(i\). Entonces tenemos \[\begin{array}{cll} t^{\mathbf{T}^{\tau}}[t_{1},...,t_{n}] & = & t_{i}\\ & = & t(t_{1},...,t_{n}) \end{array}\] Prueba de que si \(\mathrm{Enu}_{k}\) es verdadero entonces \(\mathrm{Enu}_{k+1}\) lo es. Supongamos entonces que vale \(\mathrm{Enu}_{k}\). Sean \(t_{1},...,t_{n}\in T^{\tau}\) y \(t=_{d}t(x_{1},...,x_{n})\in T_{k+1}^{\tau}\). Por definicion de \(T_{k+1}^{\tau}\) hay dos casos.
Caso \(t=_{d}t(x_{1},...,x_{n})\in T_{k}^{\tau}\). Trivial ya que podemos aplicar \(\mathrm{Enu}_{k}\).
Caso \(t=f(s_{1},...,s_{m})\), con \(f\in\mathcal{F}_{m}\), \(m\geq1\) y \(s_{1},...,s_{m}\in T_{k}^{\tau}\). Por la Convención Notacional 3, tenemos declarados también \(s_{1}=_{d}s_{1}(x_{1},...,x_{n}),...,s_{m}=_{d}s_{m}(x_{1},...,x_{n})\). O sea que \(\mathrm{Enu}_{k}\) nos dice que \[s_{i}^{\mathbf{T}^{\tau}}[t_{1},...,t_{n}]=s_{i}(t_{1},...,t_{n}),\text{ }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}\] por lo cual vale \(\mathrm{Enu}_{k+1}\).
El álgebra de términos tiene la siguiente propiedad fundamental:
7.62 (Universal Mapping Property). Si \(\mathbf{A}\) es cualquier \(\tau\)-álgebra y \(F:Var\rightarrow A\), es una función cualquiera, entonces \(F\) puede ser extendida a un homomorfismo \(\bar{F}:\mathbf{T}^{\tau}\rightarrow\mathbf{A}\).
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
7.11 (Teorema de Completitud Ecuacional). Sea \((\Sigma,\tau)\) una teoría ecuacional. Si \((\Sigma,\tau)\models p\approx q\), entonces \((\Sigma,\tau)\vdash_{ec}p\approx q.\)
Proof. Supongamos \((\Sigma,\tau)\models p\approx q.\) Sea \(\theta\) la siguiente relación 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
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.61 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\). Nótese 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 hipótesis 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\).
7.9. Sea \((\Sigma,\tau)\) una teoría ecuacional. Si \((\Sigma,\tau)\vdash p\approx q\), entonces \((\Sigma,\tau)\vdash_{ec}p\approx q\).