Download 3.5 Comparando cálculos y modelos

Comparando cálculos y modelos
La idea de comparar cálculos y modelos hace referencia al estudio de la
relación existente entre las dos nociones fundamentales de la Lógica, la consecuencia
semántica y la derivabilidad formal. Como ya sabemos, tanto una como otra
constituyen definiciones alternativas de la misma relación, la de consecuencia. Se trata
pues, de determinar de manera efectiva si realmente estamos ante dos definiciones
alternativas de la misma entidad, o ante dos relaciones distintas aunque emparentadas
de un cierto modo. Indirectamente, obtendremos un análisis de los recursos formales y
cognitivos que se ponen un funcionamiento en cada caso.
La comparación entre la derivabilidad formal y la consecuencia semántica se
resuelve en el estudio de dos propiedades que ya hemos introducido al discutir la
Lógica de Enunciados Clásica –cfr.: cap. 2.8-. Se trata de
[1]
i. Corrección: Un cálculo S es correcto en relación a una clase M de
modelos o estructuras syss para cada conjunto X de fórmulas y para
cada fórmula A sucede que:
-
Si X|S A, entonces X√ M A.
ii. Completitud (fuerte): Un cálculo S es completo en relación a una
clase M de modelos o estructuras syss para cada conjunto X de
fórmulas y para cada fórmula A sucede que:
-
Si X√ M A, entonces X|S A.
La referencia a estructuras no debe provocar aquí especiales problemas. Por
estructura, o incluso por sistema, no se entiende en este contexto nada muy distinto de
Lógica de Primer Orden
lo que aquí hemos denominado modelo. He querido introducir algo más de
terminología porque no es infrecuente encontrar obras en las que estas expresiones
son sistemáticamente empleadas.
A diferencia de lo que sucedía en el capítulo anterior, en el que analizábamos
resultados que no guardan entre sí una relación aparente, lo que nos proponemos en
este nuevo capítulo sí parece estar dotado de una cierta unidad. Nuestro objetivo
parece estar claro esta vez: se trata de resolver todas nuestras dudas acerca del
equilibrio existente entre el cálculo –la derivabilidad formal- y los modelos –la
consecuencia semántica-. Esto no debe servir para suponer una conexión entre las
demostraciones de una y otra propiedad, demostraciones que ciertamente son
bastante independientes entre sí.
La formulación de la corrección y la completitud –más adelante quedará claro
por qué añado el adjetivo fuerte- ofrecida en [1] hace especial hincapié en citar de
manera explícita los dos elementos que se requieren para definir las relaciones que se
están comparando. Me refiero a un cálculo S y a una clase de modelos M. De este
modo, nunca estaremos tentados a atribuir sólo a una de las clases de recursos
involucrados la posesión de una de esas propiedad. Esta aclaración es necesaria en la
medida en que es muy común afirmar que tal o cual cálculo es correcto o completo sin
citar de forma explícita la clase de modelos con respecto a la cual se establecen esas
propiedades. El resultado indirecto de esta manera de actuar es la concesión de una
primacía, epistemológica, al menos, a la construcción de la clase de modelos M con
respecto a los cuales se mide después la adecuación del cálculo. Así las cosas,
corrección y completitud serían propiedades que establecen, prima facie, la
adecuación de un cálculo con respecto a una clase de modelos ya existente. Esa clase
de modelos debería gozar, entonces, de una motivación independiente capaz de
aportar la adecuación del análisis que ofrece de las constantes lógicas del lenguaje y,
presumiblemente, del comportamiento de la noción de verdad. Esta observación
desencadenó hace unos años una cierta polémica que, muy posiblemente, no es sino
un nuevo episodio en el continuo debate acerca de qué es primero, si los recursos del
cálculo o los empleados en los modelos.
322
Comparando cálculos y modelos
La forma de proceder adoptada en [1] pretende ser neutral en esta polémica
admitiendo que existen buenos ejemplos de prioridad epistemológica tanto en el
terreno de los sistemas deductivos como en el de los modelos. Por tanto, es posible
hallar lógicas –en el sentido del término que aquí se ha discutido en [22] cap.2.8- en
las que la corrección y la completitud evalúan la adecuación del cálculo y otras en las
que es posible entender que lo que se analiza es la adecuación de los modelos.
La discusión de la corrección y la completitud muestra siempre un balance muy
desequilibrado a favor de la segunda de ellas. La demostración de la completitud es
considerablemente más compleja y prolija que la de la corrección. Esto aconseja, por
si sólo discutir en primer lugar la corrección para pasar a continuación a la completitud.
Pero existe, además, otra razón que suele influir en que se proceda de esa forma: no
hay sistemas deductivos incorrectos. Dicho de otra forma, la comprobación de la
corrección de un cálculo con respecto a una clase de modelos previamente
seleccionada es condición necesaria para considerar que estamos ante un genuino
producto lógico y no ante un ensayo fallido.
Corrección del Cálculo Clásico para la Lógica de Primer Orden. La corrección es una
propiedad que, como ya he advertido en más de una ocasión suele asimilarse con otra
que ya ha sido establecida para LPO: la consistencia. Es frecuente afirmar, por
ejemplo, que un cierto cálculo es consistente porque no prueba ninguna fórmula falsa
–se entiende que respecto a una cierta clase de modelos o interpretaciones-.
Seguramente hay razones que justifican esta forma de hablar que aquí, pero tampoco
es raro ver en ello una confusión fácil de deshacer.
La consistencia analiza el carácter no trivial de un cálculo. Hemos visto que,
bajo los supuestos que aquí se han asumido, esto es algo que equivale a afirmar que
un cálculo nunca demuestra una fórmula y su negación. Pero esos mismos supuestos
permiten afirmar en este caso que si un sistema deductivo es inconsistente, entonces
323
Lógica de Primer Orden
es incorrecto. Pero es más, podemos expresar esta tesis en forma de un teorema
trivial:
[2]
Teorema: Si la derivabilidad formal caracterizada para LPO por un
sistema S resulta ser correcta con respecto a la clase de todos los
modelos M para LC , entonces esa misma relación es (simplemente)
consistente.
Esquema de la demostración. Sea S el cálculo elegido para representar
la derivabilidad formal en LPO. Si S es simplemente inconsistente
entonces existe una fórmula A tal que |S A y |S ¬A. Ahora bien, sea como
sea A, la definición del negador garantiza que bajo tales circunstancias
existe siempre un modelo µ tal que [A] µ =F. Por tanto, A no es una
verdad lógica con respecto a la clase de modelos de la que se extrae µ.
La afirmación inversa no se puede establecer del mismo modo. Es decir, que
un cálculo no pruebe nunca una fórmula y su negación no basta para garantizar un
equilibrio idóneo entre sus teoremas y las verdades lógicas de una cierta clase de
modelos.
¿De qué forma puede un sistema deductivo probar fórmulas que no son
verdades lógicas o, en general, argumentos que no son válidos? Parece evidente que
algo semejante sólo puede tener lugar cuando las reglas de que dispone el cálculo
permiten obtener alguna construcción que da lugar a un argumento inválido. Para que
esto se produzca bastará, en general, que las reglas muestren alguna divergencia
apreciable a la hora de interpretar el comportamiento modelista de las constantes
lógicas que manipulan o, también en la forma de tener en cuenta el contexto en el que
se define la consecuencia semántica. Este comentario es la mejor pista que se puede
pedir para organizar una demostración rigurosa de este resultado. Sólo queda elegir
un cálculo que actúe ahora como representante de la derivabilidad formal para LPO.
Una buena elección puede ser Sqc. Esto obliga a aclarar una serie de aspectos
324
Comparando cálculos y modelos
de la construcción de dicho cálculo interesantes para ver el modo en que es posible
concebir la definición de cada una de las reglas. Como ya he dicho en más de una
ocasión, la consideración del formato de las reglas que corresponden a una
determinada constante lógica no es algo que pueda darse sin tener en cuenta si existe
o no alguna definición previa de dicha constante lógica. Si no existen convenciones
previas de ningún tipo acerca del significado de una cierta constante lógica, o estas no
son en todo caso independientes de su función dentro del cálculo, entonces sí
podremos afirmar que el par de reglas ofrecido define por completo esa constante.
Este sería un ejemplo claro de cálculo primero, semántica después. Es obvio, en
cualquier caso, que esta no es la estrategia que cabe seguir en el caso de LPO. Todas
sus constantes lógicas tienen un significado previo que ni siquiera es formal, pertenece
incluso o un nivel puramente intuitivo.
Cada regla debe responder a ese significado, y en definitiva, a la conducta
modelista de la correspondiente constante. Para poner en conexión esta conducta y el
formato de una regla es preciso establecer una especie de interfaz entre los recursos
empleados en el cálculo y las convenciones que implícita o explícitamente se asumen
en el tratamiento de la consecuencia semántica. Es cierto que el uso secuentes lleva a
pensar en la existencia de una directa conexión entre cada uno de ellos y una
afirmación acerca de la derivabilidad de una fórmula a partir de un conjunto de
premisas. Dicho de otra forma, cada secuente sería visto como una afirmación acerca
de la derivabilidad de algo a partir de otra cosa. La única diferencia sería así simbólica:
en un caso aparecería “⇒” mientras que en otro lo que figuraría sería “|”. Sin embargo,
esta forma de entender la conexión entre secuentes y la descripción de la derivabilidad
es inadecuada. Los secuentes admiten la presencia de conjuntos de fórmulas a ambos
lados del símbolo “⇒”, mientras que eso mismo no se da para “|” –al menos en el caso
que ahora nos ocupa-. A la hora de evaluar la forma en que una regla recoge el
significado de una constante, deberemos establecer alguna convención que permita
dotar de un significado modelista aceptable a la presencia de conjuntos de fórmulas a
la derecha de “⇒”. Esta convención se deduce claramente de la combinación de un
par de factores presentes en el diseño general de Sqc. La introducción de constante
325
Lógica de Primer Orden
en el lado derecho de un secuente obliga a considerar en ciertas ocasiones la
presencia de más de una fórmula en esa parte del secuente. En muchas ocasiones
esa presencia sólo se obtiene mediante el uso de la regla de monotonía por la
derecha. Así las cosas, si un secuente debe tener un significado modelista aceptable,
es decir, si un secuente tiene que poder ser interpretado una afirmación acerca de la
consecuencia semántica de las fórmulas que se hallan presentes en cada caso, la
convención o interfaz que es preciso añadir será el siguiente:
[3]
Interpretación modelista de un secuente: Dado el secuente X,A⇒B,Y
admitiremos en lo sucesivo que la situación que este expresa se traduce
en términos de modelos como sigue:
- Para todo modelo µ sucede que si para toda fórmula x i∈X, [x i]µ =V y
[A]µ =V, entonces existe al menos una fórmula yj∈Y tal que [yj]µ =V o
[B]µ =V.
Para mayor claridad es frecuente expresar esta convención afirmando que las
fórmulas en el lado izquierdo de un secuente han de interpretarse de forma conjuntiva,
mientras que las fórmulas en el lado derecho lo harán de forma disyuntiva. Esto da
lugar a que un secuente como el anterior, pueda ser traducido como un secuente
idealizado del tipo: (x1&x2&...xi&...)&A⇒(y1 vy2v...yiv...)vB. Este interfaz puede ser visto
como el resultado de una sutil combinación entre el tipo de estructura básica en que
consiste un secuente y el tipo de manipulaciones que se desea hacer con ellos.
Esto permite que demostremos ya lo que es el resultado sobre el que pivota la
defensa de la corrección de Sqc con respecto a la clase M de todos los modelos para
LC . Lo dividiré en dos partes, aunque sólo por razones de claridad. La primera analiza
el caso de las reglas estructurales y la segunda la de las reglas lógicas.
326
Comparando cálculos y modelos
[4]
Teorema: Cada una de las reglas estructurales de Sqc preserva la
corrección.
Esquema de la demostración. La estrategia consiste, básicamente, en
analizar cada caso. El sistema considerado es, recuérdese, la reunión
de [16] cap. 2.6 y [24] cap. 3.3. Considerada cada regla, se probará que
si los secuentes que figuran en la cabecera –uno o más- son válidos
bajo la convención de lectura asumida en [3], entonces el secuente
resultante también lo es.
Caso 1: Monotonía.
Izquierda. Partimos de X⇒Y. Supongamos, no obstante, que el
secuente resultante X,A⇒Y no preserva la corrección. Entonces habrá
de existir en modelo µ tal que [X] µ =[A] µ =V mientras que todas y cada
una de las yj∈Y son tales que [yj]µ =F. Pero en tal caso, ese mismo
modelo serviría para rechazar X⇒Y.
Derecha. Similar al caso anterior.
Caso 2: Contracción. Es trivial en ambos casos.
Caso 3: Permutación. También trivial.
Caso 4: Corte. Los secuentes en la cabecera de la Regla son X⇒Y,A y
W,A⇒Z. Supongamos que esta regla no preserva la corrección. Existe,
entonces un modelo µ tal que verifica a un tiempo todas las fórmulas en
X y W y hace falsas a todas las fórmulas en Y y Z. Por hipótesis, tanto
X⇒Y,A como W,A⇒Z han de dar lugar a consecuencias válidas.
Puesto que bajo µ todas las fórmulas en X son verdaderas y todas las
fórmulas en Y son falsas, la única opción de que X⇒Y,A de lugar a una
consecuencia válida es que [A] µ =V. Pero en ese caso es el secuente
W,A⇒Z el que resulta inválido, contradiciendo así la hipótesis. Si
327
Lógica de Primer Orden
hubiéramos razonado partiendo de W y Z el resultado habría sido el
mismo.
Quizá sea una buena ocasión para recordar el papel que desempeña la Regla
de Corte en un sistema como Sqc, sobre todo a la vista de la discusión de su
eliminabilidad.
[5]
Teorema: Cada una de las reglas lógicas de Sqc preserva la corrección.
Esquema de la demostración: Limitaremos nuestra atención a las reglas
para el negador, el condicional y el cuantor existencial. Los casos
restantes tienen un tratamiento muy similar y quedan como ejercicio.
Caso 1. Negación.
Izquierda. El secuente que forma la cabecera es X⇒A,Y. Supongamos,
como hemos venido haciendo, que la regla no preserva la corrección.
Eso supone la existencia de un modelo µ que verifica todas las fórmulas
en X y ¬A y que hace falsas todas las fórmulas en Y. Ahora bien, por la
cláusula correspondiente al negador eso supone que µ verifica todas las
fórmulas en X al tiempo que hace falsa a A y a todas las fórmulas en Y.
Pero entonces el secuente que forma la cabecera no es válido
contrariamente a lo que habíamos supuesto.
Derecha. Se argumenta de forma prácticamente idéntica
Caso 2. Condicional.
Izquierda. Los secuentes que forman la cabecera son X,B⇒Y y X⇒A,Y.
Consideraremos que son válidos para suponer a continuación que
X,A→B⇒Y no lo es. Según esto hay un modelo µ tal que [X] µ =V y
[A→B]µ =V, mientras que para todas las fórmulas yj∈Y sucede que [yj]=F.
Ahora bien, por la cláusula correspondiente al condicional eso supone
que ese modelo µ es tal que o bien [A] µ =F, o bien [B]µ =V.
328
Comparando cálculos y modelos
Subcaso 1: Supongamos que [A] µ =F. Entonces el secuente X⇒A,Y no
es válido ya que µ verifica todas las fórmulas en X al tiempo que hace
falsas todas las fórmulas en Y y a A.
Subcaso 2: Supongamos que [B]µ=V. Entonces es el secuente X,B⇒Y
el que no resulta válido.
Derecha. El secuente que forma la cabecera de la regla es X,A⇒B,Y.
Asumiremos que es válido para suponer a continuación que X⇒A→B,Y
no lo es. Eso supone la existencia de un modelo µ que verifica todas las
fórmulas en X, al tiempo que hace falsas todas las fórmulas en Y y a
A→B. Por la cláusula correspondiente al condicional eso implica que µ
verifica A y hace falsa a B. Pero entonces µ invalida el secuente de la
cabecera de la regla, contra lo que habíamos supuesto inicialmente.
Caso 3: Cuantor existencial.
Izquierda. El secuente que forma la cabecera es X,A(x/ui)⇒Y, donde u i
es además un parámetro que no ocurre en el secuente que resulta de
introducir el cuantor, esto es, no ocurre en X,∃xA⇒Y. Supongamos que
este último secuente no es válido. Eso supone la existencia de un
modelo µ que verifica todas las fórmulas en X, que verifica ∃xA al
tiempo que hace falsas todas las fórmulas en Y. Por la cláusula
correspondiente al cuantor existencial eso implica la existencia de una
función gx de asignación tal que g(x)=ui –confundiendo el parámetro ui
con un elemento del dominio U del modelo µ- tal que [A] gx =V. Ahora
bien, puesto que por la restricción impuesta sobre ui este parámetro no
ocurre en Y, podemos suponer que esa misma asignación permite
afirmar que todas las fórmulas en X son verdaderas, que [A]gx =V,
mientras que todas las fórmulas en Y son falsas.
Derecha. El secuente que forma la cabecera es X⇒A(x/ui),Y. La
inexistencia de restricciones sobre el parámetro hacen que el resultado
se siga de forma trivial.
329
Lógica de Primer Orden
La reunión de estos dos teoremas da como resultado la corrección de Sqc.
[6]
Teorema: Para todo conjunto X de fórmulas y toda fórmula A, sucede
que si X|Sqc A, entonces X√ c A con respecto a la clase M de todos los
modelos para LC .
Esquema de la demostración. Por la definición de |Sqc sabemos que X|Sqc
A es derivable en Sqc syss el secuente X⇒A puede ser obtenido a
partir del axioma y del uso de las reglas de Sqc. Sabemos que las
reglas de Sqc preservan la corrección, teoremas [4] y [5], así que sólo
resta demostrar que el axioma también lo hace. Pero esto es trivial, ya
que su formato garantiza la existencia de al menos una fórmula común
a cada lado del símbolo “⇒”, impidiendo que exista así un modelo que
verifique todas las fórmulas en el lado izquierdo del axioma al tiempo
que hace falsas todas las fórmulas en el lado derecho.
Aunque el uso de adjetivos como “fuerte” y “débil” suele reservarse para hablar
sólo de la completitud, también es posible aplicarlos al caso que nos ocupa. El
resultado anterior correspondería entonces a la corrección fuerte, siendo la corrección
débil un caso especial de la anterior:
[7]
Corolario: Para toda fórmula A de LC sucede que si |Sqc A, entonces √ C A.
Puesto que Sqc ha actuado aquí como representante de la derivabilidad en
LPO, [6] y [7] se deberán hacerse extensivos a esa relación de derivabilidad dando
lugar a
330
Comparando cálculos y modelos
[8]
Corrección:
i.
X|A ⇒ X√ C A
ii.
|A ⇒ √ C A
Para finalizar ofreceré un teorema que es consecuencia inmediata de todo lo
anterior.
[9]
Teorema: Si X es satisfecho por algún modelo µ∈M, entonces X es
consistente.
Esquema de la demostración: Supongamos que X tiene un modelo –es
satisfecho por un modelo-. Supongamos no obstante que no es
consistente. Existe entonces una fórmula A –consistencia simple- tal
que X|A y X|¬A. Por el teorema de corrección se puede afirmar ahora
tanto que X√ C A como X√ C ¬A. Puesto que X es satisfacible eso significa
que existe un modelo en el cual tanto A como ¬A son verdaderos, lo que
es imposible por la cláusula del negador.
La propiedad de consistencia no debería confundirse aquí con la de corrección.
Este restado recibe también a veces el nombre de test de consistencia.
331
Lógica de Primer Orden
Completitud del Cálculo Clásico para la Lógica de Primer Orden. Nos toca abordar el
problema inverso. Se trata de saber si un argumento válido es demostrable o, si por el
contrario, podrían hallarse argumentos válidos para los que no existe ninguna
construcción del tipo que aquí hemos admitido como derivaciones o pruebas.
La principal novedad del problema es que en este caso el punto de partida
viene dado por una afirmación no constructiva: X√ C A, mientras que el punto de llegada
es una afirmación que garantiza la existencia de una cierta construcción. X|A. El
primero que halla un modo de superar este problema es K. Gödel en el año 1930. Sus
ideas se basan en resultados previos aportados por Löwenheim acerca de la
normalización de las fórmulas de LC –cfr. cap. 2.5-. Las expresiones que permiten
dotar de un teorema de forma normal al lenguaje LC se conocen por el nombre de
formas normales de Skolem, y tendremos ocasión de hablar de ellas en capítulos
posteriores, aunque en un contexto algo distinto.
Es evidente que esta estrategia no es la que vamos a seguir aquí. De hecho,
es sumamente raro acercarse a la demostración original de Gödel si no es por
motivaciones de carácter histórico. La técnica que ha venido a reemplazar la que
Gödel adoptara en su día se debe a L. Henkin y a su teorema del año 1949 en el que
se vuelve a establecer esa completitud mediante un método que, a partir de entonces,
se denomina método de Henkin.
Como toda herramienta que acaba por formar parte del equipamiento básico de
una disciplina su reformulación ha sido muy intensa y el parecido con el original es ya
poco. Este proceso se ha visto favorecido, además, por la flexibilidad del este método,
la cual seguramente es consecuencia de un sólido fundamento intuitivo. Esta es la
razón que hace posible que se presenten un gran número de modificaciones
contextuales que no llegan a afectar al resultado final. El método de Henkin es, por
tanto, un método de trabajo más que una demostración concreta dotada de un mayor
o menor número de pasos. Un dato a favor de esta tesis lo ofrecen numerosos
desarrollos dentro de las llamadas lógicas no-clásicas, las cuales, difiriendo a veces
332
Comparando cálculos y modelos
mucho del modelo ilustrado en LPO hacen uso, no obstante, de las mismas técnicas
que Henkin usara para establecer la completitud de LPO. Mi objetivo será hacer
entender los pasos básicos de este método.
La solidez de las intuiciones básicas del método de Henkin se basa en un
razonamiento sumamente simple y al que pocas veces se presta la debida atención.
Concebir una forma de poner en conexión la condición relativa a los modelos de M que
se expresa al afirmar que X√ C A con una prueba de A a partir de X no es, ciertamente,
tarea fácil. Pero como sucede tantas veces en Lógica, lo que a veces no se aprecia de
forma directa puede resultar relativamente fácil de entender si se mira de otro modo.
Supongamos que XúA. Lo que la completitud de LPO tendría que afirmar en tal caso
es que XûC A. Simplemente hemos invertido –dado la vuelta- la presentación habitual
de la propiedad de completitud (fuerte). Decir que XûC A supone tanto como sostener la
existencia de un modelo µ en M tal que [X] µ =V y para el cual sucede, además, que
[A]µ =F. Esta afirmación sitúa la prueba del teorema de completitud en un camino que
parece conducir directamente a la construcción de ese modelo a partir de la
información que quepa extraer de XúA. Mantener que A no es derivable a partir de X
no es, sin embargo, una afirmación más fácil de manejar que aquella que sostiene que
X√ C A, lo cual nos deja en una situación no mucho mejor que la anterior. Cosa muy
distinta sería si en vez de considerar como punto de partida algo tan débil como XúA
dispusiéramos de algo considerablemente más fuerte como pudiera ser Y|¬A. En tal
caso podríamos pensar en utilizar la información codificada en la existencia de dicha
prueba para analizar la posible construcción del modelo µ mencionado líneas atrás.
Aún estaríamos a tiempo de reconducir nuestra estrategia si fuésemos capaces de
demostrar que siempre que XúA, entonces existe un conjunto Y tal que X⊆Y dándose,
además, que Y|¬A. Logrado este paso, habría que mostrar entonces que en la
afirmación Y|¬A sí hay suficiente información como para construir el modelo requerido.
333
Lógica de Primer Orden
No pretendo que sea fácil entender el proceso, me conformo con que no
parezca puro arte de magia. Voy a resumir lo dicho en términos de un esquema
informal:
[10]
Planteamiento heurístico de la demostración del Teorema de
Completitud:
1. Inversión del enunciado del teorema: Si XúA, entonces XûC A
2. Reforzamiento de la afirmación XúA: Si XúA, entonces existe un Y
tal que X⊆Y, y Y|¬A.
3. Análisis modelista de Y|¬A: Si Y|¬A, entonces existe un modelo µ,
cuya construcción se ofrece, basado es esa afirmación y para el
cual sucede que [X] µ =V mientras que [A]µ =F.
Si tomamos el antecedente de la tesis que se sostiene en [10.1] y procedemos
a encadenarla con las restantes afirmaciones de [10] –viejo método conocido como
silogismo hipotético- llegamos finalmente a la tesis según la cual existe un modelo µ tal
que [X]µ =V y [A] µ =F, es decir, habremos llegado a probar que XûC A a partir de XúA.
Una demostración de completitud tipo Henkin consta básicamente de tres
etapas que no corresponden exactamente a las descritas en [10], aunque el efecto es,
obviamente, el mismo. De hecho, será conveniente que interpretemos estas fases
como los puntos críticos de los que dependen luego la satisfacción de los pasos que
acabamos de comentar. Los fases a las que hago ahora referencia son:
[11]
Fases de la demostración de completitud por el procedimiento de
Henkin :
1. Lema de Lindenbaum. Se muestra de qué modo conectar una
afirmación del tipo XúA con la existencia de un superconjunto Y de X
de muy especial factura que garantiza que Y|¬A.
334
Comparando cálculos y modelos
2. Teorema de Henkin. Se aprovechan las propiedades genuinas de
los conjuntos del tipo al que pertenece el conjunto Y anterior para
construir un modelo que satisface exactamente las fórmulas en ese
conjunto.
3. Teorema de Completitud. Se reúnen las piezas anteriores mediante
un razonamiento lógico elemental que da como resultado la
conexión de XúA con XûC A y por tanto, el establecimiento definitivo
de la tesis por la cual si X√ C A, entonces X|A.
La primera de estas etapas tiene como objeto analizar las condiciones bajo las
cuales un conjunto de fórmulas puede llegar constituir una forma de representar el
contenido de un modelo. El teorema [9] establece una condición necesaria para que tal
cosa pueda darse. Ningún conjunto inconsistente puede representar un modelo ya que
los modelos no pueden, por definición, verificar simultáneamente una fórmula y su
negación. Por tanto, hemos de partir siempre de conjuntos consistentes. Un conjunto
consistente puede contener muchas fórmulas, pero, desde luego deja de contener
muchas otras. De hecho, un conjunto de fórmulas X del cual solo sabemos que es
consistente puede dejar de contener tanto A como ¬A, para multitud de fórmulas de
LC . Eso introduce también una cierto obstáculo en los derechos que un conjunto
consistente puede tener a representar en el lenguaje un cierto modelo, ya que todo
modelo es tal que, por definición, siempre verifica, o bien A, o bien ¬A.
Si sumamos las dos dificultades identificadas, pronto veremos que para que un
conjunto de fórmulas pueda ser un buen candidato a la representación de un modelo
hay que conseguir añadirle tantas fórmulas como sea posible sin perder en ningún
momento la consistencia. Una forma de aproximarnos a ese objetivo puede ser añadir
al conjunto de partida todas aquellas fórmulas que son derivables a partir de él. Dado
un conjunto X, lo que se obtendría entonces es la teoría generada por X, esto es,
Th(X). Una teoría Th(X) es un conjunto que incluye a X y que, por definición, es
335
Lógica de Primer Orden
consistente. Sin embargo, queda aún muy lejos de lo que se necesita. De hecho, no
hay nada que pueda ocupar el lugar de la siguiente noción fundamental:
[12]
Un conjunto máximamente consistente es todo conjunto X que satisface
las siguientes condiciones:
i.
X es consistente y
ii.
Para cada fórmula A, o bien A∈X o bien ¬A∈X.
De esta definición y de la equivalencia de las nociones de consistencia simple
absoluta se sigue que
[13]
Teorema: Si X es un conjunto máximamente consistente entonces para
toda fórmula A sucede que si A∉X, entonces XW{A} es inconsistente.
Esquema de la demostración. Si A∉X, entonces por maximalidad ¬A∈X.
Así pues X,A|¬A, pero por reflexividad X,A|A, y por tanto XW{A} es
inconsistente.
Un conjunto máximamente consistente resulta ser, por tanto, un conjunto al que
no es posible añadirle ninguna fórmula sin romper esa consistencia. Por otra parte, es
evidente que un conjunto de estas características retiene las buenas propiedades de
las teorías. En concreto,
[14]
Teorema: Si X es un conjunto máximamente consistente, entonces para
toda fórmula A sucede que X|A syss A∈X.
Esquema de la demostración. La parte no trivial es aquella en que se
establece que si X es máximamente consistente, entonces si X|A,
336
Comparando cálculos y modelos
sucede que A∈X. Supongamos que A∉X. Por maximalidad, sucede
entonces que ¬A∈X. Pero entonces X|¬A y X|A, y por tanto X no es
consistente, contrariamente a lo que se había afirmado en principio.
Si analizamos [12] observamos que las condiciones impuestas sobre un
conjunto de fórmulas para ser máximamente consistente son, ni más ni menos,
aquellas que se precisan para poder considerarlo como un buen candidato a la
representación lingüística de un modelo. No estoy diciendo que lo sea, sino que
cumple ciertas condiciones que son necesarias en todo conjunto de fórmulas que
aspire a comportarse de ese modo. Por otra parte, y como queda de manifiesto en el
teorema [14], los criterios empleados en esta definición proceden del cálculo. Es decir,
un conjunto máximo es un tipo especial de teoría que aspira a representar un modelo.
De hecho, es el tipo de conjunto Y cuya existencia se reclama en [10.2]. No obstante,
al hablar en esa ocasión de un cierto conjunto Y se exigía, además, que fuese posible
mostrar que dado un conjunto consistente cualquiera –no necesariamente máximoX⊆Y. No sabemos cuan peculiares son los conjuntos máximamente consistentes, de
hecho, no sabemos si existen. El Lema de Lindenbaum resuelve este problema
mostrando que todo conjunto consistente está incluido en algún conjunto consistente
máximo, y lo hace estableciendo una construcción inductiva de un conjunto máximo a
partir de un conjunto consistente cualquiera.
El siguiente resultado no desempeña un papel de gran relevancia en la
demostración del Lema de Lindenbaum pero actúa como superestructura del proceso
facilitando en alguna ocasión las cosas.
[15]
Teorema: Si X es un conjunto consistente de fórmulas, entonces para
cualquier fórmula A, o bien XW{A} es consistente, o bien XW{¬A} es
consistente.
337
Lógica de Primer Orden
Esquema de la demostración. Este resultado pasa por demostrar que
para cualquier conjunto X y cualquier fórmula A sucede que X|A syss
XW{¬A} es inconsistente. La parte no trivial de este resultado es aquella
en la que se pasa de la afirmación de que XW{¬A} es inconsistente a
X|A. Si ese conjunto es inconsistente, entonces X,¬A|B y X,¬A|¬B. Es
trivial demostrar en tal caso –queda como ejercicio- que X|A.
Supongamos ahora que tanto XW{A} como XW{¬A} son inconsistentes.
Según lo visto eso implica que X|A y X|¬A, contradiciendo la
consistencia de X.
Para establecer los términos de la construcción de Lindenbaum necesitamos
antes fijar unas condiciones dentro de las cuales actuar. En primer lugar vamos a
definir un lenguaje L* C a partir de LC el cual resulta de añadir a las constantes
individuales del vocabulario básico de LC todos los parámetros {u1,...ui...} empleados
en la presentación de los cálculos anteriores. Además, asumiremos que en ese
lenguaje el cuantor universal se introduce por definición. Esto permitirá prescindir de él
en la práctica abreviando algunas consideraciones. A continuación vamos asumir la
existencia de una función de enumeración para las fórmulas cerradas de ese nuevo
lenguaje. Esta función, sea ε, asocia a cada entero positivo una fórmula de L* C . La
existencia de esta función necesita ser establecida de manera efectiva. Podemos
obviar el paso ya que enumerar las fórmulas de un lenguaje como L* C es tarea trivial.
No lo sería tanto si en lugar de considerar un conjunto enumerable de parámetros –o
testigos, como también se conocen en los contextos modelistas- hubiéramos
precisado una cantidad mayor de ellos. Una que resultase no enumerable. En la
medida en que no nos vamos a ocupar de considerar modelos con universos no
enumerables esa necesidad, y las complicaciones que de ella se derivan, resulta
prescindible. Sí quiero advertir, no obstante, de la existencia de técnicas que permiten
extender el formato general que ahora discutimos a lenguajes de cualquier cardinal –
tamaño-. La existencia de una función enumerante se justifica entonces haciendo uso
de un teorema de teoría de conjuntos de carácter menos elemental que lo visto hasta
338
Comparando cálculos y modelos
ahora. Se trata del teorema del buen orden cuya exposición va un poco más allá de los
objetivos de este curso.
Una vez establecidas estas condiciones vamos a mostrar sin más dilación en
qué consiste una construcción de Lindenbaum.
[16]
Construcción de Lindenbaum. Sea X un conjunto consistente cualquiera
de fórmulas pertenecientes a LC y sea ε una enumeración de L* C . A
partir de ahí se procede a construir la siguiente cadena de conjuntos de
fórmulas:
1. X0=X
Xi, si XiW{Ai} es inconsistente, siendo Ai es la i-ésima
fórmula de la enumeración
2. Xi+1=
XiW{Ai} si dicho conjunto es consistente y Ai no es de la
forma ∃xB para alguna fórmula B
XiW{Ai, B(x/ui)} si dicho conjunto es consistente y Ai es de
la forma ∃xB para alguna fórmula B, siendo ui el primer
parámetro que no figura en XiW{Ai}.
3
X*=WXi, i∈.
Lo que el Lema de Lindenbaum hace ahora es establecer que X* es
efectivamente un conjunto máximamente consistente y que, además, para cualquier
conjunto X consistente existe un X* tal para el cual se cumple que X⊆X*. Esto suele
expresarse afirmando que todo conjunto consistente de fórmulas se extiende a uno
máximamente consistente.
339
Lógica de Primer Orden
Antes de pasar a ese punto convendría explicar algún detalle de la
construcción que tal vez haya podido quedar menos claro. Puede extrañar, por
ejemplo, la exigencia de que cada fórmula existencial sea acompañada de una
instancia de substitución que garantice que realmente existe en ese conjunto un
parámetro que reemplaza a la variable bajo el alcance del cuantor. La razón para ello
consiste en impedir que se puedan formar conjuntos en los que se encuentra una
cierta fórmula A del tipo ∃xB al tiempo que para cada constante individual en L* C
¬B(x/c) pertenece igualmente a ese conjunto. Cualquier mecanismo deductivo que
empleemos permite dar lugar a esa situación simplemente añadiendo parámetros
nuevos. La idea de ejemplificar mediante un parámetro o testigo la presencia de
fórmulas existenciales provoca que en algún punto de la enumeración nos veamos
obligados a excluir alguna fórmula del tipo ¬B(x/c), si queremos preservar la
consistencia del resultado. Si hubiéramos admitido la presencia de cuantores
universales, nos habríamos visto en la necesidad de admitir algo parecido para el caso
de fórmulas del tipo ¬∀xB.
[17]
Lema de Lindenbaum. Todo conjunto consistente de fórmulas X se
extiende a uno máximamente consistente X*.
Esquema de la demostración. La demostración consta de tres partes. La
primera de ellas establece que X⊆X*, lo cual es obvio por la
construcción anterior, así que prescindiremos de más detalles. La
segunda establece que X* es consistente, y la tercera que es máximo.
X* es consistente: Supongamos, no obstante, que existe una fórmula A
tal que X*|A y X*|¬A. Por el teorema [14] eso implica que tanto A como
¬A pertenecen a X*. Puesto que existe una enumeración ε de todas las
fórmulas en L* C , podemos suponer que A es Bi bajo esa enumeración
mientras que ¬A es Bj. Puesto que no afecta en nada al razonamiento
supondremos que i<j. Por la construcción de X* eso supone que
340
Comparando cálculos y modelos
Xi+1=XiW{Bi}. Ahora bien, esa misma construcción garantizará que Xj=Xi,
ya que al haber añadido antes Bi, y ser Bj su negación, nunca llegará a
añadirse Bj.
X* es máximo: Supongamos que hay una fórmula A tal que ni ella ni su
negación pertenecen a X*. Al igual que antes podemos suponer que por
la enumeración ε A=Bi, ¬A=Bj y que i<j. Puesto que Bi no pertenece a
X*, podemos suponer por la construcción de X* que XiW{Bi} es
inconsistente, pero entonces por el teorema [15] XjW{Bj} es consistente y
entonces la construcción de X* garantiza que Xj+1=Xj W{Bj}, y por tanto,
Bj∈X*, contrariamente a lo que se había supuesto.
Con este resultado hemos mostrado que la idea vertida en [10.2] responde a
una construcción formal perfectamente coherente. Todo conjunto consistente puede
ser extendido a uno máximamente consistente siguiendo para ello las reglas
establecidas por el cálculo. Obsérvese que el criterio que determina si una fórmula ha
de ser añadida o no en una etapa de la construcción de X* es la existencia de pruebas
que hagan del conjunto considerado un conjunto trivial –inconsistente- desde el punto
de vista del cálculo. No se trata de considerar en este punto la propia conducta
modelista de las constantes lógicas, sino las reglas del propio cálculo. Cuánto se
parezcan un conjunto máximo y un modelo dependerá en parte de lo bien que cada
sistema de reglas represente la conducta modelista de cada constante. Pero este es
un asunto en el que aún no hemos entrado. Corresponde, en definitiva, analizar el
tercer paso de los que han sido mencionados en [10].
De lo que se trata ahora es de analizar si la información vertida en un conjunto
máximamente consistente basta o no para construir un modelo. Si realmente es
suficiente como para dar lugar a un modelo adecuado para LC , es decir, un modelo en
M, entonces estaremos realmente muy cerca de lograr nuestro objetivo.
341
Lógica de Primer Orden
Lo primero que hay que abordar es la construcción de un dominio adecuado a
ese modelo, pero por fortuna esta es tarea fácil. La adición de los parámetros
empleados en el cálculo al conjunto de las constantes de L* C permite establecer un
interfaz entre los conjuntos máximos obtenidos por la construcción de Lindenbaum y el
dominio del modelo µ que se desea construir. Teniendo eso en cuenta, parece claro
que lo que corresponde es considerar un dominio sobre el cual proyectar el conjunto
formado por la unión de las constantes en {a1,...ai,...} y los parámetros en {u1,...ui,...}.
Sólo merece la pena hacer notar que la unión de ambos conjuntos no contiene más
elementos que los que pueda haber en un conjunto de cardinal enumerable. En otras
palabras, la unión de dos conjuntos enumerables cualesquiera sólo genera un
conjunto de cardinal enumerable. El paso siguiente es la construcción de la función I
de interpretación que, junto con el dominio U forma el par µ=<U,I>.
[18]
Construcción del modelo canónico µ* de un conjunto consistente
máximo X*.
1. Dominio. U* un conjunto cualquiera de cardinal enumerable.
2. Función I*.
i.
Para cada término t en L* C I*(t)∈U* con la única condición
de que para cualesquiera dos términos distintos t, t’
sucede que I*(t)≠I*(t’).
ii.
-
Para cada letra relacional n-aria Rin,
<[t1]µ*,g,...[tn]µ*,g>∈I*(Rin) syss Rint1,...tn∈X*, donde g es una
función arbitraria de asignación definida sobre U*.
Como se puede ver, el modelo generado a partir de X*, al cual se suele añadir
el calificativo de “canónico”, establece la imagen de la función I* de interpretación
tomando en cuenta la información atómica presente en X*. Puesto que X* es un
342
Comparando cálculos y modelos
conjunto consiste y máximo sabemos que para cada letra relacional y cada n-tupla
existe información disponible capaz de generar una función de interpretación
aceptable. La razón de exigir que cada término en L* C quede asociado a un elemento
distinto en U* se debe a la necesidad de evitar posibles conflictos en la interpretación
que no existen en el conjunto X*. Puesto que disponemos de suficientes elementos en
U* como para evitar este tipo de problema, lo suyo es no provocarlo de forma artificial.
La función de asignación g no desempeña aquí papel alguno, ya que en X* no existen
fórmulas con variables libres, pero es necesaria para construir luego la función [.]µ*,g
que permite dar un valor a cada fórmula en L* C.
El paso dado en [18] es importante al mostrar la forma de generar un modelo a
partir de la información atómica contenida en X*, pero no garantiza en absoluto que la
función modelo [.]µ* verifique exactamente las fórmulas en X*. Este punto es el que
resulta realmente crucial porque es ahí donde vamos a comprobar si el criterio seguido
para construir X*, las reglas del cálculo, y el que permite generar [.]µ* a partir de µ*, las
clásulas semánticas, coinciden del modo deseado. Esto nos lleva discutir el siguiente
enunciado:
[19]
Lema : Para toda fórmula A de L* C y todo conjunto máximamente
consistente X* sucede que A∈X* syss [A] µ* =V.
Esquema de la demostración. La demostración procede por inducción
sobre el grado lógico.
Base: Fórmulas atómicas. Por la construcción del modelo canónico µ*
sabemos que <[t1]µ*,g,...[tn]µ*,g>∈I*(Rin) syss Rint1,...tn∈X*. Ahora bien,
esos supone tanto como admitir que [Rint1,...tn]µ*,g=V.
Hipótesis de inducción: Supongamos que el resultado se cumple para
fórmulas de grado lógico n. A continuación vamos a probar que se
cumple para fórmulas de grado lógico n+1. Consideraremos sólo tres
casos.
Caso 1. A=¬B.
343
Lógica de Primer Orden
i.
¬B∈X*. Por la consistencia de X* sabemos que B∉X*. Puesto
que B es a lo sumo de grado n, sabemos que el teorema se
cumple. Eso significa que [B]µ*,g=F. Por la cláusula
correspondiente al negador tenemos entonces que [¬B]µ*,g=V.
ii.
[¬B]µ*,g=V. Por la cláusula, [B]µ*,g=F. Por hipótesis de inducción
se tiene entonces que B∉X*. Por la condición de maximalidad se
tiene entonces que ¬B∈X*.
Caso 2. A=B→C.
i.
B→C∈X*. Si B→C∈X*, entonces o bien B∉X*, o bien C∈X*.
Supongamos que no es así. En tal caso, B∈X* y C∉X*. Es
inmediato comprobar que todo conjunto máximamente
consistente es cerrado bajo la siguiente regla: si A→B∈X* y
A∈X*, entonces B∈X*. En este caso eso supone que C∈X*. Por
tanto podemos dar por sentado que si B→C∈X*, entonces o
bien B∉X*, o bien C∈X*. Por hipótesis de inducción, y puesto
que tanto B como C son de grado lógico menor o igual que n,
tenemos que [B]µ*,g=F o [C]µ*,g=V. Pero eso supone tanto como
afirmar que [B→C]µ*,g=V.
ii.
[B→C]µ*,g=V. Por la cláusula del condicional se tiene que
[B]µ*,g=F o [C]µ*,g=V. Puesto que tanto B como C son de grado
menor que n, podemos asumir que el resultado se cumple para
ambas. Hay dos casos:
a) B∉X*. Por maximalidad, ¬B∈X*. Queda como ejercicio
mostrar que todo conjunto máximamente consistente es
cerrado bajo la regla siguiente: si A∈X* entonces AvB∈X*.
En nuestro caso eso supone afirmar que ¬BvC∈X* y de ahí
aplicando la definición del condicional, B→C∈X*.
b) C∈X*. Similar al caso anterior, pero aplicando en este caso la
clausura bajo la regla: si B∈X*, entonces AvB∈X*.
344
Comparando cálculos y modelos
Caso 3. A=∃xB
i.
∃xB∈X*. Puesto que X* dispone, por construcción, de al menos
un tesigo –parámetro- ui para instanciar ∃xB, podemos afirmar
que si ∃xB∈X*, entonces existe un parámetro ui tal que
B(x/ui)∈X*. Puesto que B(x/ui) es de grado lógico a lo sumo n, se
puede aplicar la hipótesis de inducción y afirmar que
[B(x/ui)]µ*,g=V. De ahí por la clásula del cuantor pasamos sin más
a [∃xB]µ*,g=V.
ii.
[∃xB]µ*,g=V. Aplicando la clásula correspondiente y la hipótesis
de inducción llegamos a que B(x/ui)∈X* para algún parámetro ui.
Es obvio que X*W{¬∃xB} es inconsistente, y por tanto, por la
maximalidad de X*, ∃xB∈X*.
Aunque largo y algo tedioso, este lema constituye realmente la piedra
angular de una demostración de completitud tipo Henkin. A parte del uso
especialmente claro de la hipótesis inducción, que permite descender y
cambiar de plano –del cálculo a los modelos y viceversa- para ascender
posteriormente, merece la pena llamar la atención sobre el papel que
desempeña la presencia de testigos en el tratamiento del cuantor existencial. Si
no hubiésemos hecho uso de este recurso, la presencia de una fórmula del tipo
∃xB en un conjunto X* no permitiría afirmar que existe en ese mismo conjunto
una instancia de substitución adecuada, y por tanto, no podríamos servirnos del
mecanismo que apela a la hipótesis de inducción para llegar a la cláusula
semántica correspondiente. Pero con independencia de este hecho, que muy
bien podría ser interpretado como una simple maniobra técnica, existen
razones profundas para hacer uso de testigos de la forma en que se ha hecho.
Un conjunto máximo que contuviera una fórmula del tipo ∃xB y ninguna de sus
instancias de substitución tendría que contener todas las fórmulas del tipo
¬B(x/ui) para cada parámetro en L* C . Estos conjuntos, consistentes, no
obstante, reciben en ocasiones el nombre de conjuntos ω-inconsistentes. Es
345
Lógica de Primer Orden
obvio que un conjunto ω-inconsistente con respecto al cuantor existencial no
captura el significado modelista de dicha constante lógica, violando, además,
elementos contextuales relativos al manejo de este cuantor en un cálculo.
El último elemento relevante de esta demostración es el que se refiere a la
ausencia de referencias concretas a algún mecanismo particular de cálculo. Es obvio
que apelamos al cálculo constantemente, pero no se hace preciso en ningún momento
tener en cuenta los recursos específicos de alguno de ellos. A lo sumo hemos tenido
que invocar alguna regla cuya clausura se comprueba sobre cualquier conjunto X*
mediante cualquier sistema particular de reglas. Esta es la razón por la cual se suele
afirmar que el método de Henkin es especialmente independiente de las
especificidades de cada cálculo.
Lo siguiente resume por fin buena parte de la discusión.
[20]
Teorema (Teorema de Henkin). Todo conjunto consistente de fórmulas
tiene un modelo de cardinal enumerable.
Esquema de la demostración. Por el lema de Lindenbaum, todo
conjunto consistente X se extiende a un conjunto consistente máximo.
El lema anterior muestra que el modelo canónico µ* es un modelo de
X*, y por tanto, del propio X. Que µ* tiene un universo de cardinal
enumerable se sigue inmediatamente de la enumerabilidad de las
fórmulas en L* C y del modo en que se ha construido dicho modelo.
Estamos ya muy cerca de alcanzar el tercer paso del planteamiento heurístico
expuesto en [10] y con ello la formulación completa del Teorema de completitud para
LPO. Todo lo que resta es la correcta colocación de todas las piezas junto con un poco
de lo que se suele denominar razonamiento lógico elemental. Véase si no.
346
Comparando cálculos y modelos
[21]
Teorema de Completitud (fuerte): Para cualquier conjunto X de fórmulas
y cualquier fórmula A de LC se cumple lo siguiente:
-
si X√A entonces X|A
Esquema de la demostración. Supongamos que XúA. Sabemos que si A
no es derivable a partir de un conjunto X, entonces XW{¬A} es un
conjunto consistente. Por el Teorema de Henkin, todo conjunto
consistente tiene un modelo, y este en particular verifica de manera
simultánea todas las fórmulas en X y ¬A. Es decir, verifica las fórmulas
en X y hace falsa a A, lo cual basta para establecer que XûA.
Como es obvio, la completitud débil se sigue como un corolario inmediato de lo
anterior.
[22]
Corolario (Completitud débil): Para cualquier fórmula A sucede que
-
si √A, entonces |A
Esquema de la demostración. Considerando en [21] X=∅.
Hay un aspecto de este tipo de técnica que no hemos comentado aquí. Se trata
del efecto que sobre ella tiene la adición del símbolo de identidad “=” como constante
347
Lógica de Primer Orden
lógica en Vb. No es la primera vez que procedemos a añadir la identidad –cfr.: [6], cap.
3.3- como recurso extra al final de la exposición de un cierto sistema. En todos los
casos en que se ha efectuado esta maniobra hemos sido conscientes de que la
presencia de esta nueva constante no iba a afectar de manera sustancial a la
conducta de los sistemas en que se incorpora. Esto mismo no se puede afirmar de
manera tan inmediata en el contexto de una demostración de completitud. Podría
suceder que este incremento en la capacidad expresiva explícitamente reconocida en
el lenguaje tuviera como efecto la pérdida de propiedades. Ya hemos avisado en más
de una ocasión de que la incorporación de nuevos recursos en un lenguaje formal
suele se causa de la pérdida de propiedades metateóricas elementales.
Por fortuna, la Lógica de Primer Orden con identidad es tan completa con
respecto a sus modelos como lo era antes el fragmento sin identidad. Lo que sí es
cierto, no obstante, es que para establecer este extremo es preciso superar algunas
dificultades de cierto interés. Incorporar expresiones del tipo t=t’ al lenguaje L* C no
ofrece especial dificultad. Tampoco obtener los correspondientes conjuntos máximos
del tipo X*. La dificultad se presenta en la construcción del modelo canónico que antes
tenía lugar en [18] y que empleábamos luego en la demostración del lema central que
se enuncia en [19]. Supongamos, como en [18], que cada constante individual en L* C
queda asociada a un elemento distinto del dominio U* de µ* por medio de I*. Es obvio
que en tal caso cualquier fórmula del tipo t=t’ resulta falsa en µ*, aunque pueda
encontrarse en X*. Además, es obvio que la presencia en X* de expresiones de ese
tipo habrá tenido un efecto a través cálculo sobre los parámetros que incorporamos en
ciertas fórmulas, efecto al cual no parece sensible el modelo. La menear de resolver
este problema es mediante el paso de U* a un dominio cociente U/u obtenido al definir
la equivalencia “u” del modo que se indica:
[23]
tut’ syss t=t’∈X*
Si empleamos esta relación para generar clases de equivalencia sobre U*/u lo
que obtenemos finalmente, es fácil comprobarlo, es una partición en clases de
348
Comparando cálculos y modelos
equivalencia del conjunto U*, es decir, obtenemos un dominio formado por los
representantes canónicos de las clases de equivalencia obtenidos. Por cierto, es aquí
donde en cierto modo entran en juego las propiedades genuinas de la identidad tal y el
hecho de que sus leyes características, reflexividad, simetría y transitividad, puedan
ser demostradas en el cálculo. Así, donde antes teníamos elementos ui en U* ahora
tenemos sus representantes canónicos [ui]u. Basta reemplazar en [18] U* por U*/u y
asociar mediante I* las nuevas constantes individuales en L* C a elementos en U*/u. Es
inmediato comprobar que bajo estas estipulaciones la identidad se comporta ya de
forma correcta, pudiendo incorporar a la demostración del lema central [19] la parte
correspondiente a la identidad. Esto es, aquel paso en el que se establece que t=t’∈X*
syss [t=t’]µ*,g=V. El detalle se deja como ejercicio. Esto permite afirmar finalmente que
[24]
Teorema de Completitud (fuerte) para LPO=: Para cualquier conjunto X
de fórmulas y cualquier fórmula A de LC = se cumple lo siguiente:
-
si X√A entonces X|A
La discusión de todo lo relativo a la completitud nos ha enseñado a entender
mejor cómo funciona la relación conjuntos de fórmulas y la clase de los modelos que
las verifican. La existencia de modelos canónicos del tipo de µ* muestra hasta qué
punto es posible ajustar esa relación en un contexto en el que no hay significado
material propiamente dicho. Es decir, las razones por las que un modelo lo es de un
conjunto residen en última instancia en el significado de las constantes lógicas y de los
átomos eventualmente presentes en ese conjunto. Una vez que hemos comprobado
que LPO es completa y correcta, no parece que podamos esperar de sus fórmulas y
de los modelos que las satisfacen la identificación de peculiaridades dignas de tener
en cuenta. Dicho de otra forma, dos conjuntos consistentes de fórmulas sólo difieren
en sus hechos atómicos, lo cual, en un contexto puramente formal es irrelevante. No
parece que podamos servirnos con provecho del lenguaje LC para expresar diferencias
349
Lógica de Primer Orden
notables acerca de los modelos que satisfacen una fórmula –o conjunto de ellas- y los
que satisfacen otra sin salirnos por completo del dominio de las ciencias formales. Sin
embargo, existe toda una rama de la Lógica contemporánea, la Teoría de modelos,
dedicada precisamente, a estudiar cómo se pueden emplear fórmulas para expresar
propiedades formales notables de clases de modelos. El siguiente capítulo está
dedicado a comentar algunos de los resultados más elementales de esta parte de la
Lógica.
Orientación bibliográfica.
De nuevo se puede empezar consultando el libro de [Hunter, 1969], secc. 29,
32 y 46. La descripción que se hace de una demostración tipo Henkin en [Crossley,
1972], cap, 2 tiene la ventaja de presentar un esquema muy claro y elucidador del
procedimiento.
El tratamiento más extenso y profundo de esta técnica, así como de muchas de
sus implicaciones figura en [Manzano, 1989], cap. III. Su lectura es prácticamente
obligada.
[Badesa, Jané y Jansana, 1998], cap. 17 presenta el acierto de emplear el
concepto de “modelo canónico”, uso que he adoptado en este capítulo.
350