Download El teorema de correctud-completud fuerte: un enfoque semántico

El teorema de correctud-completud fuerte:
un enfoque semántico
José Alfredo Amor
[email protected]
RESUMEN
El objetivo de este artículo es exponer dos cosas. En primer lugar, lo que entendemos
por una prueba de tipo semántico del teorema de correctud-completud fuerte de la lógica
clásica. En segundo lugar presentar una prueba de ese estilo, usando el teorema de
compacidad y otros resultados semánticos. Los elementos usados son conocidos, sin embargo
la prueba es original, elegante y sencilla porque evita la manipulación sintáctica en un sistema
axiomático dado. Usaré la lógica clásica de primer orden y el concepto de sistema axiomático
en una concepción ligeramente diferente a la tradicional, donde la definición de derivación
formal incluye la posibilidad de establecer restricciones a la aplicación de las reglas de
inferencia.
Palabras clave: semántica, compacidad, correctud, completud, teorema de la deducción.
I. NOCIONES BÁSICAS
Suponemos que las nociones de lenguaje de primer orden con igualdad y de interpretación
para ellos -como se presentan en los libros de lógica matemática - son bien conocidas. En esta
sección revisaremos algunas nociones básicas como “consecuencia lógica”, “derivación
formal en un sistema axiomático” y los teoremas relacionados de correctud-completud fuerte
y de compacidad, para aclarar conceptos o simplemente para refrescar la memoria del lector.
Definiremos también el significado de “un sistema satisface Modus Ponens” y de “un sistema
satisface el Metateorema de la Deducción”.
En la sección 2 se mostrarán las principales ideas sobre el teorema de correctud-completud.
En la sección 3, introducimos los teoremas semánticos de compacidad, Skolem y Herbrand;
explicaremos qué entendemos por una prueba con enfoque semántico, con especial énfasis en
la diferencia entre la heurística semántica y la sintáctica, para el teorema de completud.
Entonces generalizamos una prueba de J. Malitz [Malitz 1979], que consideramos como una
prueba con enfoque semántico del teorema de correctud-completud débil (o restringido), pero
que no prueba la forma fuerte. Con la idea de la prueba de Malitz, usamos dos resultados
metalógicos que presentaremos previamente, para definir -con un enfoque semántico- un
sistema axiomático para obtener la versión fuerte (o extendida) de correctud y completud. A
nuestro sistema lo llamaremos MA, y es una modificación y extensión del de Malitz, y lo
definiremos formalmente en la sección 4. En nuestra noción de derivabilidad en MA está la
contribución más interesante, ya que no era obvio cómo adaptar la noción de derivabilidad
1
para obtener la prueba de correctud fuerte. En la sección 5 resumimos las ideas heurísticas
relacionadas y damos algunas conclusiones.
El concepto básico semántico de la relación de ser forzado a ser verdad por otras
verdades, se conoce como “consecuencia lógica”.
DEFINICIÓN 1.1 φ es una consecuencia lógica de Σ o Σ implica lógicamente a φ (Σ ϕ) si
y sólo si para toda interpretación A, toda asignación de variables s que satisface α para toda
α∈ Σ, también satisface ϕ.
Nótese que la definición de “ϕ es una consecuencia lógica de Σ” significa que es imposible
tener una interpretación y una asignación donde todas las fórmulas del conjunto Σ son
satisfechas y la fórmula φ no.
El caso particular Σ = ∅ denotado ϕ en vez de ∅ϕ, significa de acuerdo a la definición
anterior, que en toda interpretación A, toda asignación de variables s satisface ϕ. En este caso
decimos que ϕ es lógicamente válida.
El concepto sintáctico básico de obtener una fórmula a partir de un conjunto de
fórmulas en un sistema axiomático S se conoce como derivación formal en el sistema S.
Decimos que una fórmula α es derivable de un conjunto de fórmulas Σ en un sistema
axiomático S, si hay una derivación formal de α a partir de Σ en S.
DEFINICIÓN 1.2
a) Un sistema axiomático S está definido por la siguientes dos condiciones:
1. Un conjunto decidible ∆ de fórmulas1. Las fórmulas de ∆ se llaman los
axiomas de S.
2. Un conjunto finito decidible de reglas de inferencia2 de S.
b) Una derivación formal de una fórmula α a partir de un conjunto de fórmulas Σ en
un sistema axiomático S es una lista finita de n fórmulas α1, . . . ,αn, con n≥1, tal
que αn=α y para toda i (1≤ i ≤ n) αi es o un axioma de S, o αi es una fórmula de Σ3
o αi es obtenida de fórmulas anteriores de la lista por medio de alguna regla de
inferencia de S. Puede establecerse previamente alguna restricción a la aplicación
de una regla, pero dicha restricción debe ser efectivamente decidible4. Si tal
derivación existe, se denota por Σ├sα y se lee como “α es derivable de Σ en el
sistema S”.
El caso particular Σ = Ø denotado ├sϕ, en vez de Ø├sϕ, se define como “α es un teorema
formal en el sistema S”. La única diferencia es que no hay hipótesis.
1
Para cada fórmula debe haber un procedimiento efectivo para decidir si es un elemento de ∆ o no lo es.
Para cada regla de inferencia debe haber un procedimiento efectivo para decidir si una fórmula se sigue o no de
otras fórmulas usando esa regla.
3
En este caso decimos que αi es una hipótesis de Σ.
4
De hecho, si tal a restricción existe debe ser parte de la definición misma de derivación formal. [Amor 2004].
2
2
DEFINICIÓN 1.3
a) Un sistema axiomático S satisface correctud fuerte si y sólo si toda fórmula obtenida
con el proceso de derivación a partir de un conjunto de fórmulas Σ, es una
consecuencia lógica del mismo conjunto Σ. En símbolos:
Si Σ├s α entonces Σ╞ α
b) Un sistema axiomático S satisface correctud débil si y sólo si todo teorema formal es
una fórmula lógicamente válida. Este es el caso particular Σ = Ø. En símbolos:
Si ├s α entonces ╞ α.
c) Un sistema axiomático S satisface completud fuerte si y sólo si todas las
consecuencias lógicas de Σ pueden obtenerse con el proceso de derivación a partir de
Σ en S. En símbolos:
Si Σ╞ α entonces Σ├s α
d) Un sistema axiomático S satisface completud débil si y sólo si todas las fórmulas
lógicamente válidas son teoremas formales en S. Este es también el caso particular Σ =
Ø. En símbolos:
Si ╞ α entonces ├s α
DEFINICIÓN 1.4 Dado un sistema axiomático S, definimos lo siguiente:
i) El sistema S satisface Modus Ponens (MP) si y sólo si para todo conjunto de fórmulas
Σ∪{α, β},
Σ, α, (α→β)├ S β
ii) El sistema S satisface el Metateorema de la Deducción (MTD) si y sólo si para todo
conjunto de fórmulas Σ ∪ {α, β}:
Si Σ, α├S β entonces Σ├S (α→β)
iii) Sea Σ un conjunto de fórmulas, entonces: Σ es S-consistente si y sólo si no hay fórmula α
tal que Σ├ S α y Σ├ S (¬α). Véase [Amor 2003].
II. EL TEOREMA DE CORRECTUD-COMPLETUD FUERTE
Imaginar si había o no una prueba con enfoque semántico para el teorema de
correctud-completud fuerte, usando el teorema de compacidad, fue el origen de este trabajo.
Ahora podemos decir que sí es posible definir un sistema axiomático desde una perspectiva
semántica, de modo tal que todas las consecuencia lógicas son exactamente sus derivaciones
formales. En otras palabras, podemos decir que la prueba que buscábamos existe y, como
mostraremos más adelante, puede llevarse a cabo sin trabajar dentro del sistema dado, sino
usando las propiedades semánticas del sistema y algunos otros resultados semánticos como el
teorema de compacidad, una versión semántica del teorema de Skolem y una versión
semántica del teorema de Herbrand.5 Desde luego que necesitamos definir algunos conceptos
5
Este trabajo es parte del presentado en [Amor 2001].
3
sintácticos elementales, porque el teorema mismo los involucra y necesitamos usar algunos
resultados sintácticos elementales que se siguen trivialmente de las definiciones, y se cumplen
en cualquier sistema axiomático. Sin embargo los argumentos que daremos durante la prueba
son puramente semánticos.
Este artículo presenta no sólo la prueba con enfoque semántico mencionada antes, sino
también una manera general de entender y formular el teorema de correctud-completud fuerte,
como un resultado sobre la existencia de ciertos sistemas axiomáticos y no como un teorema
que se refiere a propiedades particulares de un sistema particular.
Debe notarse que dentro de la formulación del teorema de correctud-completud fuerte,
el sistema axiomático mencionado juega un papel fundamental (usualmente no explícito). Así
desde un punto de vista metalógico, nuestro objetivo es enfatizar la existencia de un sistema
axiomático en la afirmación del teorema, relativo al cual las propiedades de correctud y
completud se cumplen. Consideremos las siguientes dos formulaciones equivalentes del
teorema:
TEOREMA 2.1 Teorema de correctud-completud fuerte (Primera forma)
Existe un sistema axiomático formal S tal que para todo conjunto de fórmulas Σ U {α},
Σ ╞ α si y sólo si Σ├S α
TEOREMA 2.2 Teorema de correctud-completud fuerte (Segunda forma)
Existe un sistema axiomático formal S tal que:
i) S satisface MP
ii) Para todas las fórmulas β y γ, ├s (β →(¬β →γ))
iii) Para toda fórmula α, ├S [(¬α→α)→α]
iv) S satisface MTD
v) Para todo conjunto de fórmulas Γ,
Γ es S-consistente si y sólo si Γ es satisfacible.
En este artículo daremos la prueba con un enfoque semántico de la primera forma del
teorema. Nótese que la propiedad v) de la segunda forma incluye el teorema de Henkin6.
Debemos decir que para tener la equivalencia entre esas dos formas, las propiedades i) a iv)
de la segunda forma son necesarias.
TEOREMA 2.3 La dos formas del teorema de correctud-completud fuerte son equivalentes
Prueba (esquema):
Supongamos la primera forma y sea S el sistema dado. Es claro que para todo conjunto de
fórmulas ΣU{α,β}: Σ, α, (α→β)╞ β; para todas las fórmulas β y γ: ╞ (β →(¬β →γ)); para toda
fórmula α: ╞[(¬α→α)→α]. Además para toda conjunto de fórmulas ΣU{α, β}: Si Σ, α╞ β
6
Corresponde a un lado de la doble implicación: Si Γ es s-consistente entonces Γ es satisfacible. [Henkin 1949].
4
entonces Σ╞(α→β). Ahora usando la primera forma tenemos i), ii), iii), iv). Para v) sea Γ un
conjunto de fórmulas. Supongamos que Γ es insatisfacible, entonces Γ╞α para toda fórmula
α, entonces (por la primera forma) Γ├S α para toda fórmula α, entonces Γ es S-inconsistente.
Por otro lado, supongamos que Γ es S-inconsistente, entonces hay una fórmula β tal que Γ├S β
y Γ├S¬β. Entonces (por la primera forma) tenemos que Γ╞ β y Γ╞ ¬β, por lo tanto Γ es
insatisfacible.
Ahora supongamos la segunda forma y sea S el sistema dado. Sea ΣU{α} cualquier conjunto
de fórmulas. Para el “sólo si”, supongamos que Σ S α. Entonces ΣU{¬α} es S-consistente
porque si no, habría una fórmula β tal que ΣU{¬α}├S β y ΣU{¬α}├S ¬β, pero entonces por
ii) y i) de la segunda forma tenemos que ΣU{¬α}├S γ para toda fórmula γ; en particular
ΣU{¬α}├S α. Ahora por iv) tenemos que Σ├S(¬α→α) y por iii) y i) tenemos Σ├S α. Así
ΣU{¬α} es S-consistente. Finalmente por v) tenemos que ΣU{¬α} es satisfacible y por lo
tanto Σ α.
Para el “si”, supongamos que Σ α. Entonces ΣU{¬α} es satisfacible y por v) ΣU{¬α} es Sconsistente. Entonces Σ S α, porque si Σ├S α entonces ΣU{¬α}├S α por monotonía de
cualquier sistema formal y ΣU{¬α}├S¬α es inmediato; contra la S-consistencia de ΣU{¬α}.
Para la prueba de la equivalencia de esta dos formas, véase [Amor 2006] pp.140-141. La
primera forma, con el caso particular Σ = ∅, es la correctud-completud débil.
TEOREMA 2.4 Teorema de correctud-completud débil
Existe un sistema formal axiomático S tal que para toda fórmula α,
╞ α si y sólo si ├S α
Es claro que correctud-completud fuerte trivialmente implica correctud-completud
débil, porque esta última es el caso particular Σ = ∅ del primero. Por otro lado, correctudcompletud débil junto con Modus Ponens (MP) y el Metateorema de la Deducción en el
sistema (MTD) y junto con el teorema de compacidad, implica correctud-completud fuerte.
III. UN ENFOQUE SEMÁNTICO PARA CORRECTUD-COMPLETUD FUERTE
Una prueba directa del teorema de correctud-completud fuerte, consiste en definir un
sistema axiomático y probar que satisface correctud y completud. Esta prueba se hace
usualmente trabajando dentro del sistema axiomático y haciendo muchas derivaciones
formales hasta mostrar que el sistema cumple ambas propiedades.
Hay un modo alternativo: una prueba con enfoque semántico, que consiste en definir,
de un modo ad hoc y con una perspectiva semántica, un sistema cuyos axiomas y reglas tienen
fundamento semántico y que satisface correctud y completud. En este caso la justificación es
semántica y evita trabajar dentro del sistema definido, excepto para usar algunas propiedades
generales de todos los sistemas. Esta prueba es una extensión y modificación esencial de una
prueba de Malitz, quien presenta un sistema y prueba que satisface correctud-completud débil,
pero que no satisface ni correctud ni completud fuerte.
5
En nuestra prueba usamos el teorema de compacidad, una versión semántica del
teorema de Skolem y una versión semántica del teorema de Herbrand, el cual dicho sea de
paso, se demuestra usando el teorema de compacidad. Las pruebas de esos teoremas son
semánticas y aparecen en el libro de Malitz [Malitz 1979] y también en [Amor 2006].
Presentamos ahora el teorema de compacidad, el cual es un teorema puramente semántico
probado también por Gödel en 1930. Damos aquí dos versiones equivalentes del teorema.
TEOREMA 3.1 Teorema de compacidad Primer forma
Dado un conjunto de fórmulas Σ de un lenguaje de primer orden con igualdad, si cada
subconjunto finito Γ⊆Σ, Γ es satisfacible, entonces Σ es satisfacible.
PRUEBA (esquema):
Sea un conjunto infinito de fórmulas Σ tal que cada subconjunto finito suyo es satisfacible
(llamamos a esta propiedad “ser finitamente satisfacible”). Necesitamos probar dos resultados,
el primero consiste en obtener conjunto Γ tal que Σ⊆Γ y Γ es un conjunto maximal finitamente
satisfacible de fórmulas, usando el Lema de Zorn. El segundo resultado consiste en obtener un
conjunto Ω tal que Σ⊆Ω, y Ω es cerrado bajo “testigos” existenciales y sea finitamente
satisfacible. Entonces estos dos resultados se iteran por recursión y la unión de todos esos
conjuntos es un conjunto Σ* tal que Σ⊆Σ* y Σ* es un conjunto de fórmulas maximal cerrado
bajo “testigos” y finitamente satisfacible. Entonces construimos una estructura interpretación
para el lenguaje y una asignación para las variables, que satisface todas las fórmulas de Σ*. Esa
interpretación y asignación obviamente satisface a todas las fórmulas de Σ y así podemos
concluir que Σ es satisfacible. De hecho Σ* es igual al conjunto de todas las fórmulas
satisfechas por esa asignación en esa estructura.
TEOREMA 3.2 Teorema de compacidad Segunda forma
Si Σ U {φ} es un conjunto de fórmulas de un lenguaje de primer orden con igualdad y
Σφ, entonces hay a subconjunto finito Γ⊆Σ, tal que Γφ.
PRUEBA:
Supongamos que Σφ. Entonces Σ U{¬φ} es insatisfacible, y entonces por la primera forma,
hay un ∆ finito, ∆⊆ΣU{¬φ} que es insatisfacible. Pero entonces ∆\{¬φ}U{¬φ} es también
insatisfacible y por lo tanto hay Γ =∆\{¬φ} finito, ∆\{¬φ}⊆Σ tal que ∆\{¬φ}φ.
Esta segunda forma es la que usaremos en nuestro resultado principal. Nótese que el
teorema de compacidad es una afirmación puramente semántica; no involucra deducciones en
absoluto, pues se refiere sólo a nociones semánticas y existen varias pruebas de él, puramente
semánticas.
Lo que hemos llamado “teorema de Skolem” no debe confundirse con el famoso
teorema de Skolem sobre la existencia de modelos numerables para conjuntos de fórmulas.
6
Aquí nos referimos a un teorema sobre una forma especial de fórmula que puede asociarse
con cada fórmula, conocida como su Forma de Skolem de Validez (FSV).
DEFINICIÓN 3.1 Sean φ, ψ, fórmulas. Decimos que φ y ψ son fórmulas equiválidas si y
sólo si se cumple que: φ si y sólo si ψ.
La relación entre una fórmula y su forma de Skolem de validez asociada, es lo que
hemos llamado equivalidez y es una relación estrictamente más débil que la de equivalencia
lógica, pero es muy útil, ya que establece una “equivalencia” en términos de validez lógica,
como veremos después con el teorema de Skolem.
Un enunciado puede transformarse por medio de un algoritmo a su “forma de Skolem
de validez”, FSV(φ). Este algoritmo genera siempre una cuantificación existencial “pura” (sin
cuantificadores universales) que afecta a una fórmula matriz sin cuantificadores. En otras
palabras, para toda enunciado φ, FSV(φ) = (∃x1…∃xkψ), donde ψ = ψ( x1,…,xk) es una
fórmula sin cuantificadores.
En seguida mostraremos cómo obtener esta forma de Skolem. Dado cualquier
enunciado φ, la FSV(φ) se obtiene con el siguiente proceso algorítmico: el primer paso es (1)
reemplazar condicionales (α→β) con (¬α∨β), y bicondicionales (α↔β) con
((¬α∨β)∧(¬β∨α)), así obtenemos un enunciado bien conocido que es lógicamente
equivalente al original y que incluye sólo los conectivos ¬, ∨, ∧. En seguida (2) introducir
negaciones por medio de las bien conocidas leyes lógicas de negación. En seguida (3)
renombrar todas las variables acotadas, para evitar variables repetidas en cuantificaciones
diferentes. Luego (4) transformar la fórmula para obtener la Forma Prenex (FP). Finalmente
(5) eliminar de izquierda a derecha, uno a uno, todos los cuantificadores universales
introduciendo “testigos” que son nuevas constantes o funciones Skolem 7.
Podemos resumir y nombrar los pasos de este procedimiento (que muestra cómo
obtener FSV(φ) a partir de φ) del siguiente modo: reemplazar condicionales (RC), reemplazar
bicondicionales (RB), introducir negaciones (IN), renombrar variables cuantificadas (RV),
prenexar todos los cuantificadores (FP)8, Skolemización dual (D(x, t)) donde “x” es la variable
universal eliminada y “t ” es la nueva constante o función de Skolem que la substituye.
Finalmente obtenemos FSV(φ)9.
La equivalencia lógica se denota con “≡”. Es importante tener en mente que el paso de
Skolemización dual, consistente en la eliminación de los cuantificadores universales y difiere
7
Estas funciones (llamadas “de Skolem”) dependen de las variables de los cuantificadores existenciales previos
al cuantificador universal que se está eliminando. En el caso de que no haya cuantificadores existenciales previos
al cuantificador universal que se está eliminando, la sustitución se hace por una nueva constante (llamada “de
Skolem”). [Amor 2004].
8
Hasta este punto, todos los enunciados obtenidos en el proceso son lógicamente equivalentes entre sí.
9
La forma de Skolem de validez FSV se puede obtener de otro modo, en términos de la llamada Forma de
Skolem de Satisfacción, denotada FSS. Lo siguiente establece, para el lector interesado, la relación dual entre las
dos formas de Skolem mencionadas: Si φ es una fórmula, entonces FSV(φ) = FP[¬(FSS(¬φ))] así como FSS(φ)
= FP[¬(FSV(¬φ))].
7
de los otros pasos, en que no se preserva la equivalencia lógica. Para ilustrar este proceso,
damos un ejemplo de la aplicación de este algoritmo usando las abreviaturas introducidas
antes:
φ = [∃y∀x P(x,y) ∧ ¬∃z∀x∀y Q(z,x,f(y))]
≡ [∃y∀x P(x,y) ∧ ∀z∃x∃y ¬Q(z, x,f(y))]
IN
≡ [∃y∀x P(x,y) ∧ ∀z∃v∃w ¬Q(z, v,f(w))]
RV
≡ ∃y∀x∀z∃v∃w [P(x,y) ∧ ¬Q(z,v,f(w))]
FP
FP(φ) = ∃y∀x∀z∃v∃w [P(x,y) ∧ ¬Q(z,v,f(w))]
Sk1 = ∃y∀z∃v∃w [P(g(y),y) ∧ ¬Q(z,v,f(w))]
D(x, g(y))
Sk2 = ∃y∃v∃w [P(g(y),y) ∧ ¬Q(h(y),v,f(w))]
D(z, h(y))
FSV(φ) = ∃y∃v∃w[P(g(y),y) ∧ ¬Q(h(y),v,f(w))]
El teorema de Skolem establece que una fórmula ϕ es lógicamente válida si y sólo si la Forma
de Skolem para Validez de ϕ (FSV(ϕ)) es lógicamente válida. Decimos que φ y FSV(φ) son
fórmulas equiválidas. Formalmente:
TEOREMA 3.3 Teorema de Skolem
Para toda fórmula φ:
i) φ
si y sólo si
FSV(φ).
ii) [φ→FSV(φ)].
iii) Hay fórmulas ψ tales que [FSV(ψ)→ ψ].
Para una prueba del teorema de Skolem, véase [Malitz 1979] p.157 o [Amor 2006], p.92.
Como otro ejemplo, aplicaremos el algoritmo a una fórmula que usaremos en la sección IV:
Sea φ = [∃x∀y P(x,y) → ∀y∃x P(x,y)]. Entonces:
≡ [¬∃x∀y P(x,y) ∨ ∀y∃x P(x,y)]
RC
≡ [∀x∃y ¬P(x,y) ∨ ∀y∃x P(x,y)]
IN
≡ [∀x∃y ¬P(x,y) ∨ ∀z∃w P(w,z)]
RV
≡ ∀x∃y ∀z∃w [¬P(x,y) ∨ P(w,z)]
FP
FP(φ) = ∀x∃y ∀z∃w [¬P(x,y) ∨ P(w,z)]
Sk1 = ∃y ∀z∃w [¬P(c,y) ∨ P(w,z)]
D(x, c)
Sk2 = ∃y ∃w [¬P(c,y) ∨ P(w, f(y)]
D(z, f(y))
FSV(φ) = ∃y ∃w [¬P(c,y) ∨ P(w, f(y)]
DEFINICIÓN 3.2 Un término básico es un término sin variables. Sea ψ una fórmula sin
cuantificadores, entonces una instancia básica de ψ es la fórmula obtenida al substituir todas
las variables (libres) de ψ por términos básicos.
8
TEOREMA 3.4 Teorema de Herbrand
Si ψ(x1,…, xn) es una fórmula sin cuantificadores, entonces:
(∃x1…∃xnψ) si y sólo si existe una sucesión finita ψ1,…,ψm, de instancias básicas de ψ,
tal que (ψ1∨…∨ψm).
Nótese que la parte “si” es realmente una consecuencia directa del siguiente resultado
elemental: si ψ(x1,…,xn) es una fórmula sin cuantificadores y ψ1,…,ψm es una sucesión finita
de instancias básicas de ψ, entonces (ψ1∨…∨ψm)(∃x1…∃xnψ). Este resultado será usado
más tarde. La parte “sólo si” del teorema de Herbrand es la parte fuerte y se prueba usando el
teorema de compacidad. Para una prueba, véase [Malitz 1979], p.185 o [Amor 2006], p.95.
Ahora vayamos a la prueba con enfoque semántico del teorema de correctud-completud
fuerte. Sea ∑φ una consecuencia lógica de una fórmula φ a partir de un conjunto de
fórmulas Σ. Entonces por el teorema de compacidad existe un Γ⊆∑, Γ finito, tal que Γφ.
Sea Γ={α1,…,αm}. Como sabemos, esto es equivalente a que α1,…, αm φ. Así, aplicando m
veces la propiedad semántica elemental:
∑, α φ
si y sólo si
∑ (α→ φ).
Observamos que α1,…, αm φ es equivalente a:
(α1→ (α2→… → (αm →φ)…))
Ahora, sea γ = (α1→ (α2→… → (αm →φ)…)) la fórmula lógicamente válida anterior. El
enunciado denotado ∀γ es la cerradura universal de la fórmula γ, tal que si γ = γ(x1,…,xn)
donde x1,…,xn son todas las variables libres en γ, entonces ∀γ = ∀(γ(x1,…,xn)) =
∀x1….∀xnγ(x1,…,xn). Como γ es equivalente en términos de validez lógica (o equiválida) a su
cerradura universal ∀γ, el enunciado ∀γ es también lógicamente válido.
Por otro lado, por el teorema de Skolem, la validez lógica del enunciado ∀γ es equivalente a
la validez lógica de FSV(∀γ)10, y esta es a su vez equivalente, por el teorema de Herbrand, a
la existencia de una sucesión de instancias básicas de la matriz ψ de FSV(∀γ), cuya
disyunción es lógicamente válida. En otras palabras, tenemos el siguiente argumento
semántico, donde abreviaremos “si y sólo si” con la expresión “sii”:
∑φ sii {α1, …, αm} φ, para algún {α1,…, αm}⊆∑ y m∈
sii (α1→(α2→… → (αm →φ)…))
sii γ
pues γ = (α1→(α2→… → (αm →φ)…))
sii ∀γ
10
Obsérvese que ∀γ es un enunciado, y entonces FSV(∀γ) es también un enunciado. Esto es importante para
poder usar el teorema de Herbrand, si se aplica al enunciado FSV(∀γ) que es de la forma (∃x1…∃xkψ).
9
sii FSV(∀γ)
sii (∃x1…∃xkψ) con FSV(∀γ)=(∃x1…∃xkψ) y ψ=ψ(x1,…,xk) sin cuantificadores
sii hay instancias básicas ψ1,…,ψn de ψ, tales que (ψ1∨…∨ψn)
Tenemos que expandir el lenguaje original con un número infinito numerable de
nuevos símbolos de constante y de nuevos símbolos de función para cada aridad. Esto es
necesario para tener suficientes instancias básicas de fórmulas sin cuantificadores.
Empecemos por definir nuestro sistema de tal modo que sus axiomas sean
precisamente todas la fórmulas que comparten las propiedades de la fórmula (ψ1∨…∨ψn)
obtenida con el argumento semántico presentado antes. En otras palabras, los axiomas serán
todas las disyunciones lógicamente válidas de instancias básicas de fórmulas sin
cuantificadores.
Debemos decir que los axiomas definidos de esta manera no son instancias de
esquemas de axiomas, pero sí hay un número infinito de ellos. Por otro lado, ya que un
axioma es por definición lógicamente válido, entonces debe ser efectivamente decidible si una
fórmula de la forma propuesta es o no es un axioma. Pero este es el caso, porque las
disyunciones de instancias básicas de fórmulas sin cuantificadores son fórmulas
proposicionales, y entonces su validez lógica es efectivamente decidible en la lógica
proposicional.
Ahora, iremos a la inversa en el argumento semántico previo. Definimos como la
primera regla de inferencia, el paso inverso en el Teorema de Herbrand. Sin embargo lo
haremos en la forma general (ψ1∨…∨ψn) (∃x1…∃xkψ) presentada en la observación
posterior al Teorema de Herbrand. Entonces, de cualquier disyunción de instancias básicas de
sustitución de una fórmula ψ(x1,…,xk) sin cuantificadores, obtenemos la cuantificación
existencial de ψ. Esta cuantificación existencial de ψ es precisamente FSV(∀γ). Esta regla,
cuya premisa puede ser lógicamente válida (axioma) o no, la llamaremos regla de Herbrand o
HB:
(ψ1∨…∨ψn)
(∃x1…∃xkψ)
Donde ψ= ψ(x1,…,xk) no tiene cuantificadores y toda ψi (1≤i≤n) es una instancia básica de ψ.
Definamos ahora, como la segunda regla de inferencia, el paso inverso del teorema de
Skolem: de FSV(∀γ), obtenemos ∀γ. A esta regla la llamaremos regla de Skolem o SK:
FSV(∀γ)
∀γ
Definamos ahora, como la tercera regla de inferencia, el paso inverso de la propiedad
de equivalidez de la cerradura universal “ γ si y sólo si ∀γ”. Pero lo haremos en la forma
más general ∀γ γ, así que de ∀γ obtenemos la instanciación con variables γ. Esta regla
aplicada a cualquier enunciado de la forma ∀γ, lógicamente válido o no, la llamaremos regla
de Instanciación de Variables o IV:
∀γ
γ
10
Obsérvese que (∀γ→γ) y entonces ∀γγ, pero que generalmente (γ→∀γ). Sin embargo,
otra vez, nos referimos a dos fórmulas equiválidas: ∀γ sii γ.
Recordar que γ = (α1→(α2→…→ (αm →φ)…)). Ahora definimos, como la cuarta regla de
inferencia, el paso inverso en la propiedad semántica elemental “Γ, αiφ sii Γ(αi → φ)”
que se aplicó m veces en nuestro argumento semántico. Cada vez ese paso inverso será una
aplicación de la siguiente regla: de α y (α→ φ) obtenemos φ, con α y φ cualesquiera fórmulas.
Esta regla se llama Modus Ponens o MP:
α, (α→ φ)
φ
Nótese que hasta aquí tenemos, por definición, un esquema de derivación formal de la
fórmula φ a partir del conjunto de fórmulas ∑. Todo está dentro del sistema axiomático que
hemos definido, motivados por nuestro argumento semántico previo. La siguiente lista de
4+2m fórmulas, con m≥0, muestra la derivación formal de la fórmula φ a partir del conjunto
de fórmulas ∑:
1. (ψ1∨… ∨ψn)
Axioma
2. (∃x1… ∃xk ψ)
Regla HB a 1
3. ∀γ
4. γ
4. (α1→(α2→… → (αm →φ)…))
4+1. α1
….
4+m. αm
4+m+1. α2→… → (αm →φ)…))
….
4+m+(m-1). αm →φ
4+2m. φ
Regla SK a 2 (∃x1…∃xkψ)=FSV(∀γ)
Regla IV a 3
Esta es la misma fórmula γ
Hipótesis
….
Hipótesis
Regla MP a 4+1,4
….
….
Regla MP a 4+m, 4+m+(m-1)
Por tanto α1, …,αm├ φ
Por definición, de 1 a 4+2m
Por tanto
∑├ φ
Propiedad sintáctica elemental de monotonía
Debe ser claro ahora que el teorema de compacidad, la propiedad semántica elemental
“Γ,αiφ sii Γ(αi → φ)”, la propiedad semántica de la cerradura universal y los teoremas
semánticos de Skolem y de Herbrand, justifican la completud fuerte y la correctud débil del
sistema definido, en el caso Σ=∅, m=0, γ=φ y en sólo cuatro pasos. Ya que decidibilidad es
una característica esencial de los sistemas axiomáticos, es muy importante señalar que los
axiomas y reglas de inferencia que definimos son de hecho decidibles.
11
Llamemos S al sistema axiomático de Malitz donde los axiomas son los mismos que los que
hemos definido, pero las reglas de inferencia son sólo HB y SK y la definición de derivación
es la tradicional, sin restricción en la aplicación de reglas. Este sistema satisface correctudcompletud débil sólo para enunciados. Sin embargo no satisface la versión fuerte. Para
mostrar esto tenemos los siguientes dos ejemplos:
1) Consideremos la fórmula ∀xP(x). Como FSV(∀xP(x)) = P(c), usando la regla SK
obtenemos P(c)S∀xP(x). Sin embargo P(c) ∀xP(x). Esto muestra que S no satisface
correctud fuerte.
2) Por otro lado, tenemos que ∀xP(x)P(c) lo cual es inmediato. Sin embargo un análisis de
todas las posibles pruebas formales en S muestra que ∀xP(x) SP(c), porque si
∀xP(x)SP(c), entonces hay una derivación de P(c) a partir de ∀xP(x) en S, donde ∀xP(x) es
una hipótesis que no puede ser un teorema formal porque ∀xP(x). HB o SK no pueden ser
aplicadas a ∀xP(x) por su forma y con IV sólo obtenemos P(x). Así, podemos eliminar
∀xP(x) de la derivación pues no se usa y obtenemos S P(c). Pero P(c), contradiciendo la
correctud débil de S. Véase [Amor 2001] pp.64-66. Esto significa que S no satisface
completud fuerte.
Parece natural preguntarse cómo podríamos modificar el sistema S de modo que satisfaga el
teorema fuerte. La respuesta a esta pregunta se obtuvo con dos resultados metalógicos
generales acerca de sistema axiomáticos que ya satisfacen la propiedad de correctudcompletud débil. Debemos mencionar aquí que esos resultados se prueban usando el teorema
de compacidad. El primer resultado se refiere a la relación metalógica entre completud fuerte
y Modus Ponens (MP):
TEOREMA 3.5 Si S es un sistema axiomático que satisface completud débil, entonces:
S satisface completud fuerte si y sólo si S satisface MP.
El segundo resultado se refiere a la relación metalógica entre correctud fuerte y el
Metateorema de la deducción (MTD):
TEOREMA 3.6 Si S es un sistema axiomático que satisface correctud y completud débil,
entonces:
S satisface correctud fuerte si y sólo si S satisface el MTD.
COROLARIO 3.7 Si S es un sistema axiomático que satisface correctud-completud débil,
entonces:
S satisface correctud-completud fuerte si y sólo si S satisface MP y MTD.
Para una demostración de estos resultados, véase [Amor 2003].
Estas relaciones metalógicas generales muestran claramente que dado un sistema que
satisface correctud-completud débil, para que satisfaga el teorema de correctud-completud
12
fuerte, el sistema debe también satisfacer ambos, Modus Ponens y el metateorema de la
deducción. Nótese entonces que el sistema S de Malitz no puede satisfacer MP y MTD. Así
pues, esas dos propiedades no son cuestión de preferencia personal o conveniencia práctica.
De hecho, pueden considerarse propiedades estructurales intrínsecas de la lógica de primer
orden, que juegan un papel fundamental en la correctud y completud fuerte.
Recordemos que en general (FSV(∀γ)→ ∀γ) pero sí tenemos que (∀γ→FSV(∀γ)). Sin
embargo estas dos fórmulas son equiválidas: FSV(∀γ) sii ∀γ. Ahora imponemos una
restricción a la aplicación de la segunda regla de inferencia llamada regla de Skolem (o regla
SK). En este caso, la restricción impuesta es que la regla de inferencia SK no puede ser
aplicada a hipótesis o a fórmulas que dependen de hipótesis. Esta restricción es motivada por
la restricción semántica señalada justo antes del Teorema de Skolem y es precisamente la
restricción a la regla de Skolem que garantiza que la consecuencia lógica se preserve. Con
esta restricción como parte de nuestra definición de derivación, nuestro sistema axiomático
satisfará correctud fuerte y equivalentemente el metateorema de la deducción.
IV. EL SISTEMA AXIOMÁTICO MA
Siguiendo todo lo dicho antes, podemos dar nuestro sistema MA (por Malitz-Amor) que
cumple correctud-completud fuerte. El lenguaje fue expandido con una cantidad infinita
numerable de símbolos de nuevas constantes y funciones de cada aridad.
DEFINICIÓN 4.1. Damos el sistema axiomático MA como sigue:
i) Axiomas de MA
Todas las disyunciones lógicamente válidas (ψ1∨…∨ψn) de instancias básicas de fórmulas ψ
sin cuantificadores, son axiomas de MA. Todos los términos del lenguaje expandido se usan
aquí.
ii) Reglas de inferencia de MA
a) Regla de Herbrand, HB:
(ψ1∨…∨ψm)
(∃x1… ∃xkψ)
Donde ψ(x1,…,xk) es una fórmula sin cuantificadores, y cada ψi es una instancia básica de ψ.
b) Regla de Skolem, SK:
FSV(∀φ)
si ├MA FSV(∀φ)
∀φ
donde FSV(∀φ) = (∃x1…∃xkψ) es la forma de Skolem de validez para ∀ϕ, donde
ψ=ψ(x1,…,xk) es una fórmula sin cuantificadores.
c) Instanciación de Variables, IV:
∀ϕ
ϕ
Para ϕ cualquier fórmula.
d) Modus Ponens, MP:
α , (α→ φ)
13
φ
Para α y φ fórmulas.
La definición de derivación en MA11
Una derivación de una fórmula α a partir de un conjunto de fórmulas Σ en MA, es una lista
finita de n fórmulas α1,…,αn, con n ≥1; tal que αn = α y para toda i (1≤i≤n), o αi es un axioma
de MA o αi es una hipótesis (fórmula de Σ), o αi es obtenida de fórmulas anteriores en la lista
por medio de una de las reglas de inferencia HB, IV, MP, de MA, o existe una lista de
fórmulas δ1,….,δm tal que δm = αi y tal que:
1) Para toda i (1≤i≤m) δi = αk para algún k (1≤k≤n).
2) Si 1≤k≤j≤m y δk = αs y δj = αp entonces 1≤s≤p≤n.
3) La lista δ1,…., δm es una prueba formal de MA, que usa sólo los axiomas y las cuatro reglas
HB, SK, IV, MP, pero sin hipótesis.
Si tal a derivación existe, se denota Σ├MAα y se lee “α es derivable de Σ en el sistema MA”.
Obsérvese que la sucesión δ1,….,δm es parte de la sucesión original guardando su orden y que
no son ni fórmulas de Σ que no son axiomas, ni fórmulas obtenidas de fórmulas de Σ que no
son axiomas, porque es una prueba formal. Esta definición de derivación recupera
rigorosamente nuestra idea intuitiva original de la restricción: no aplicar la regla SK a
hipótesis ni a fórmulas que dependen de hipótesis.
Para aclarar más la definición del sistema MA, damos un ejemplo de derivación en MA:
∃x∀y Pxy ├MA∀y∃x Pxy
Primero, obsérvese que ψ1 = [¬P(c,f(c))∨P(c,f(f(c)))] es la instancia básica {y/f(c), w/c} de la
fórmula ψ = [¬P(c,y) ∨ P(w,f(y))]. Segundo, que ψ2 = [¬P(c,c) ∨ P(c,f(c))] es la instancia
básica {y/c, w/c} de la misma fórmula ψ. Finalmente, la disyunción de esas dos instancias
básicas [¬P(c,f(c))∨P(c,f(f(c)))]∨[¬P(c,c) ∨P(c,f(c))] es lógicamente válida pues es una
tautología de la forma proposicional (¬A∨B∨¬C∨A). Así ψ1∨ψ2 es un axioma de MA.
Sea ϕ = (∃x∀yP(x,y)→∀y∃xP(x,y) entonces FSV(ϕ) = ∃y∃w(¬P(c,y) ∨ P(w,f(y))).12 Entonces
la derivación es la siguiente:
1. [¬P(c,f(c))∨P(c,f(f(c)))]∨ [¬P(c,c)∨P(c,f(c))]
Axioma de MA (ψ1∨ψ2)
2. ∃y∃w(¬P(c,y) ∨ P(w,f(y)))
Regla HB a 1 (FSV(ϕ))
3. [∃x∀yP(x,y) → ∀y∃xP(x,y)]
Regla SK a 2 (ϕ)
4. ∃x∀yP(x,y)
Hipótesis
5. ∀y∃xP(x,y)
MP a 4, 3
LEMA 4.1 Correctud-completud débil del sistema MA
Para toda fórmula φ:
11
φ
si y sólo si
MA φ.
Agradezco al dictaminador anónimo quien me sugirió esta definición, que corresponde con la idea original, y
es más precisa.
14
PRUEBA: Usaremos compacidad y el teorema de Skolem. La prueba surge directamente de
la definición del sistema MA, basada en el argumento semántico de la sección III. Sea φ una
fórmula y supongamos que φ. Entonces ∀φ por la propiedad semántica de la cerradura
universal, entonces FSV(∀φ) por el teorema de Skolem, entonces (∃x1…∃xkψ) donde
FSV(∀φ) = (∃x1…∃xkψ) para alguna ψ= ψ(x1,…,xk) sin cuantificadores. Entonces hay
instancias básicas ψ1,…,ψn de ψ, tales que (ψ1∨…∨ψn) por el teorema de Herbrand. Así,
por definición, (ψ1∨…∨ψn) es un axioma de MA y la sucesión de cuatro fórmulas
((ψ1∨…∨ψn), ∃x1…∃xkψ, ∀φ, φ) es por definición una prueba formal de φ en MA,
justificada respectivamente por “axioma”, “regla HB”, “regla SK” y “regla IV”, por lo tanto
MA φ.
Por otro lado, supongamos MA φ y sea (α1, α2,…, αm=φ) una prueba formal de φ en MA.
Mostramos por inducción matemática sobre i que para toda i ≤ m, αi. En el caso i=m
terminamos. Supongamos αj para toda j< i ≤ m. Hay cinco casos para αi: αi es un axioma,
αi se obtiene por HB, αi se obtiene por SK, αi se obtiene por IV y αi se obtiene por MP. Como
no hay hipótesis, la restricción a la aplicación de regla SK no se necesita.
a) Si αi es un axioma entonces αi.
b) Si αi se obtiene por HB de αj = (ψ1∨…∨ψm) con j<i y αi=(∃x1… ∃xkψ) entonces por hipótesis
inductiva (ψ1∨…∨ψm). Entonces por el teorema de Herbrand (∃x1… ∃xkψ), que es αi.
c) Si αi se obtiene por SK aplicada a αj= FSV(αi) con j<i, entonces por hipótesis inductiva
FSV(αi). Entonces por el teorema de Skolem, αi.
d) Si αi se obtiene por IV aplicada a αj= ∀αi con j<i entonces por hipótesis inductiva ∀αi.
Entonces por la propiedad semántica de la cerradura universal, αi.
e) Si αi se obtiene por MP aplicado a αj y αk=(αj→αi) con j, k<i entonces por hipótesis inductiva
αj y (αj→αi). Entonces concluimos que αi.
Mostraremos ahora que MA satisface correctud-completud fuerte. Nótese que todo lo
anterior se probó de modo semántico, usando sólo las definiciones sintácticas necesarias y las
propiedades semánticas elementales que satisfacen por definición, todos los sistemas
axiomáticos.
TEOREMA 4.2 Hay un sistema axiomático (MA), tal que para todo conjunto de fórmulas
∑∪{φ}, satisface:
∑φ
12
si y sólo si
∑MA φ
Véase el segundo ejemplo, después del teorema 3.3, en la sección III.
15
PRUEBA: Usaremos los teoremas de compacidad y de Skolem. Sea MA el sistema que
definimos y sea ∑ ∪ {φ} cualquier conjunto de fórmulas.
i) ∑φ ⇒ ∑MA φ.
Supongamos que ∑φ
⇒ Hay Γ⊆∑, Γ finito, tal que Γφ
Por teorema de compacidad
⇒ α1, …,αm φ
Con Γ={α1,…,αm}
⇒ (α1→(α2→… → (αm →φ)…))
Propiedad semántica m veces
⇒ MA (α1→(α2→… → (αm →φ)…))
Completud débil, por Lema 4.1
⇒ α1, …,αm MA φ
Por MP, m veces
⇒ Hay Γ⊆∑, Γ finito, tal que ΓMA φ
Con Γ = {α1, …,αm}
⇒ ∑MA φ
Propiedad sintáctica de monotonía
ii) ∑MA φ ⇒ ∑φ.
Supongamos ∑MA φ. Entonces por definición hay una lista finita α1,α2,…,αn=φ, que es una
derivación formal de φ a partir de ∑ en MA. Mostraremos por inducción matemática sobre i que
para toda i ≤ n, ∑ αi. En el caso i =n terminamos.
Suponemos ∑ αj para toda j< i ≤ n. Mostramos para αi. Hay seis casos: αi es un axioma, αi es
una hipótesis de ∑, αi se obtiene por HB, αi se obtiene por SK, αi se obtiene por IV y αi se
obtiene por MP.
a) Si αi es un axioma de MA entonces αi y entonces ∑ αi.
b) Si αi es una hipótesis de ∑, entonces obviamente ∑ αi.
c) Si αi se obtiene por HB de αj = (ψ1∨…∨ψm) con j<i y αi=(∃x1… ∃xkψ) entonces por hipótesis
inductiva ∑(ψ1∨…∨ψm). Pero tenemos (ψ1∨…∨ψm) (∃x1… ∃xkψ), así ∑(∃x1… ∃xkψ),
que es ∑ αi.
d) Si αi se obtiene por SK aplicada a αj= FSV(αi) con j<i, entonces por la definición de
derivación (restricción a la aplicación de la regla SK a FSV(αi) en la deducción dada), sabemos
que FSV(αi) no es una hipótesis y fue obtenida sin usar hipótesis. Así, por definición sabemos
que MA FSV(αi) y entonces por correctud débil, del Lema 4.1, tenemos FSV(αi). Ahora
usando el teorema de Skolem, tenemos que αi y finalmente podemos concluir que ∑ αi.
e) Si αi se obtiene por IV aplicada a αj= ∀αi con j<i entonces por hipótesis inductiva ∑∀αi.
Pero sabemos que ∀αi αi, y concluimos que ∑αi.
16
f) Si αi se obtiene por MP aplicada a αj y αk=(αj→αi) con j, k<i entonces por hipótesis inductiva
∑ αj y ∑ (αj→αi). Pero αj, (αj→αi)αi y concluimos ∑ αi.
Nótese que la restricción en la definición de derivación, introducida para la aplicación de la
regla SK, fue fundamental en el caso d).
COROLLARY 4.3 Metateorema de la deducción para el sistema MA
Para todo Σ ∪ {α, β} conjunto de fórmulas:
Si Σ, α ├MA β entonces Σ├MA (α→β)
Es una consecuencia inmediata del teorema anterior y los resultados metalógicos presentados
en la sección III.
V. HEURÍSTICA Y CONCLUSIONES
En esta sección damos un breve resumen de las ideas intuitivas y la heurística que nos
ayudó a obtener este sistema axiomático. La definición de nuestro sistema axiomático MA
surgió como un sistema ad hoc, desde un punto de vista semántico, porque sus axiomas y
reglas de inferencia no responden a objetivos sintácticos. Más bien responden a invertir un
proceso semántico que resumimos a continuación, para toda fórmula φ y cualquier conjunto
de fórmulas Σ:
Empezamos con una consecuencia lógica de φ a partir de Σ. Por el teorema de
compacidad, esta puede ser pensada como una fórmula de forma implicativa, digamos A,
donde A = (α1→(α2→…→(αm→φ)…)) que es lógicamente válida. Así, el enunciado
∀A=∀(α1→(α2→…→(αm→φ)…)) es también lógicamente válido. Por otro lado, a partir de
∀A se obtiene algorítmicamente una forma especial de Skolem B = FSV(∀A). Entonces B es
también un enunciado lógicamente válido, por el teorema de Skolem. De aquí obtenemos por
el teorema de Herbrand, un enunciado lógicamente válido C, sin variables libres y sin
cuantificadores, cuya validez lógica es decidible porque es un enunciado proposicional. Los
axiomas serán esos enunciados C y las reglas serán los inversos de los teoremas semánticos
usados. Una vez que tenemos este sistema ad hoc probamos directamente la correctud por
inducción matemática y obtenemos el metateorema de la deducción como corolario, aún
cuando la construcción del sistema fue en mucho inspirada por él. De hecho, debe notarse que
la restricción a la aplicación de la regla de Skolem, es precisamente lo que garantiza que las
consecuencias lógicas se preserven.
Por lo anterior tenemos una respuesta afirmativa al problema de establecer una prueba
con enfoque semántico para el teorema de correctud-completud fuerte que puede pensarse
como un corolario de los teoremas de compacidad y de Skolem. Finalmente puede decirse que
hemos mostrado que las ideas semánticas son tan básicas y poderosas, como para probar
importantes resultados sintácticos.
17
REFERENCIAS
AMOR J.A. (2001), Relaciones metalógicas entre compacidad y completud: una prueba
semántica de completud en lógica clásica, tesis doctoral, UNAM, México.
__________ (2003), A structural characterization of extended correctness-completeness in
classical logic, Crítica Revista Hispanoamericana de Filosofía, Vol.35 No.103, pp.69-82.
___________ (2004), Un refinamiento del concepto de sistema axiomático, Signos Filosóficos
Vol.IV, No.11, p. 35-54, México.
___________ (2006), Compacidad en Lógica de Primer Orden y su relación con el teorema de
Completud, 2a edición, Coordinación de Servicios Editoriales, Facultad de Ciencias, UNAM.
GÖDEL K. (1930), The completeness of the axioms of the functional calculus of logic, en Kurt
Gödel Collected Works, Vol. I, Oxford University Press, Oxford, 1986. Ed. Solomon
Feferman, p. 103-123.
HENKIN L. (1949), The completeness of the first-order functional calculus, Leon Henkin,
The Journal of Symbolic Logic, Vol.14, No.3, (pp. 159-166).
MALCEV A. I. (1971), The Metamathematics de Algebraic Systems: Collected Papers 19361967, North Holland, Amsterdam.
MALITZ J. (1979), Introduction to Mathematical Logic, Part III Model Theory, SpringerVerlag, New York.
Departamento de Matemáticas, Facultad de Ciencias, UNAM
Ciudad Universitaria, México D. F. 04510, México
E-mail: [email protected]
18