Download Los teoremas de completud María Manzano Universidad de

Los teoremas de completud
María Manzano
Universidad de Salamanca
mara@usal.es
Reconciliar las definiciones y los planteamientos sintácticos y semánticos de
consecuencia constituye el núcleo de toda lógica -esto es, tanto de las lógicas
puras y aplicadas, como de las clásicas y no clásicas-, incluso del de la que
podemos denominar lógica universal.
El teorema de completud, junto con el de corrección, establecen la equivalencia
entre la noción sintáctica y la semántica de consecuencia, para un cierto
lenguaje. Podemos plantear la cuestión así: la noción semántica de verdad
sirve para seleccionar del conjunto de todas las sentencias de un cierto
lenguaje, a las que son verdaderas en todos las estructuras o modelos
adecuados (las llamamos fórmulas lógicamente válidas, VAL). Por otra parte, a
nuestro lenguaje formal, que es de naturaleza puramente sintáctica, podemos
incorporarle un cálculo deductivo. Dicho cálculo permitirá deducir unas fórmulas
de otras, y nos servirá para generar el conjunto de las sentencias del lenguaje
que se pueden deducir sin premisas en el cálculo, a las que llamamos
teoremas lógicos (TEO)
¿Coinciden esos conjuntos?
Demostrar que VAL⊆TEO es el objetivo del teorema de completud débil, que
TEO⊆VAL lo es del de correción. La demostración del teorema de corrección
suele ser mucho más fácil que el de completud y es frecuente denominar
teorema de completud a la igualdad entre los conjuntos VAL y TEO, esto es, a
VAL=TEO.
La demostración de completud proporciona además información sobre la
estructura de la clase de los modelos de una determinada lógica. Por ejemplo,
La demostración de completud de Henkin para la teoría de tipos demuestra que
el conjunto TEO de los teoremas del cálculo coincide con el conjunto VAL de
las sentencias verdaderas en la clase de estructuras generales, que es un
subconjunto propio del de las válidas en estructuras estándar. De hecho,
cuanto más restrictiva sea la clase de modelos más amplia será la de las
fórmulas en ella válida y a la inversa.
Relevancia teórica y práctica del teorema de completud
Importancia teórica: No sabemos qué es una lógica hasta que no hemos
identificado al conjunto de sus fórmulas válidas; esto es la logicidad reside en
ese conjunto. Me explico. Cada interpretación selecciona del conjunto de todas
las fórmulas a las sentencias verdaderas en ella, que constituyen lo que
denominamos teoría de una estructura, y que en principio será distinta para
cada interpretación o modelo. Sin embargo, todas las teorías tienen un núcleo
común, el de las fórmulas válidas, VAL. Por ser verdaderas en toda estructura
estas sentencias no describen a ninguna estructura en particular, sino a aquello
que es común a todas ellas.
¿Caracterizan algo estas sentencias?
La respuesta es que sí, que describen a la propia lógica. Por consiguiente, si
logramos generarlas con facilidad habremos captado la esencia de la lógica.
Importancia práctica: Aunque contemos con la noción semántica de verdad
es frecuentemente muy difícil manejarla apelando simplemente a las
condiciones de la definición. Mucho más difícil todavía lo es el determinar si
una fórmula es consecuencia de un conjunto de ellas que tomamos como
hipótesis; esto es, si toda interpretación en la que las hipótesis sean
verdaderas la conclusión también. La razón es que en principio sería necesario
comprobarlo en toda interpretación, modelo a modelo. Por fortuna hay otro
modo de determinar si es una fórmula es consecuencia de otras que no es la
mera verificación directa de sus especificaciones semánticas: se trata de inferir
o deducir la fórmula en un cálculo deductivo utilizando las hipótesis; esto es, de
establecer una cadena de razonamiento entre premisas y conclusión. De
hecho, esta forma de definir el concepto de consecuencia es incluso más
adecuada a la noción intuitiva, ya que refleja el carácter discursivo del
razonamiento.
Si el cálculo deductivo nos va a resultar útil es porque nos ayudará a no
equivocarnos; no nos conducirá de hipótesis verdaderas a conclusiones falsas:
será un cálculo correcto. Además sus reglas permitirán obtener como teoremas
a todas las consecuencias de un conjunto dado de hipótesis; esto es, será de
aplicabilidad general, lo que denominamos un cálculo completo.
La historia de las demostraciones de completud
Hay tres ejes básicos en este estudio de la completud, que son:
1. Origen: ¿Cuándo y cómo nace la necesidad de demostración del teorema
de completud?. ¿Cuándo se deslinda del teorema de decidibilidad? Nuestra
hipótesis es que separar el concepto de completud del de decidibilidad no
debió resultar fácil puesto que la primera prueba de completud se hizo para
la lógica proposicional, que es completa y decidible; esto es, para ella existe
un algoritmo que en un número finito de pasos te dice si la fórmula es válida
o nó.
2. Evolución de la prueba de completud de Henkin: La demostración que
hizo Henkin del teorema de completud resultó ser muy versátil y se pudo
modificar para otras lógicas. ¿Cuál es la relación entre esa demostración y
las pruebas de completud posteriores?. Nos parece especialmente
interesante establecer la relación con las demostraciones que emplean
Conjuntos de Hintikka, con las de naturaleza netamente algebraicas que
emplean álgebras booleanas, filtros o ultrafiltros, las que construyen
modelos canónicos para lógicas modales y temporales, o las que se valen
de la introducción de designadores rígidos para lógicas híbridas.
3. Pruebas alternativas de completud: También en la historia de la lógica
hay numerosos ejemplos de demostraciones indirectas de completud; por
ejemplo, completud vía interpolación, completud vía compacidad, completud
vía traducción a una lógica marco que sea completa, completud mediante
modelos no estándar para lógicas incompletas. Será interesante incluir
estas demostraciones en nuestra concepción general del concepto de
completud para saber cómo y cuando debemos aplicar cada una de ellas.
Nociones ligadas a la de completud
Hay lógicas clásicas, proposicionales y de primer orden, también de orden
superior. Hay una gran variedad dentro de la categoría de las lógicas
denominadas
no
clásicas:
abductivas,
algebraicas,
condicionales,
combinatorias, categoriales, constructivas, cuánticas, deónticas, descriptivas,
difusas, epistémicas, ecuacionales, estoicas, generales, libres, híbridas,
infinitarias,
intensionales,
intuicionistas,
lineales,
multimodales,
no
monotónicas, paraconsistentes, polivalentes, de la relevancia, subestructurales
y en general, una extensa clase de lógicas no-estándar. Claramente esta
enumeración no es una buena clasificación ya que no es exhaustiva y es
solapante (por ejemplo, hay lógicas modales que son intuicionistas y nomonotónicas). De hecho, la mayoría de los lógicos actuales piensan que la
división entre lógica clásica y no clásica carece de sentido y sólo preserva una
cierta connotación histórica.
Hemos seleccionado algunos sistemas lógicos cuyo estudio nos parece de
interés:
1. Incluimos la lógica clásica, tanto la proposicional (LP), como la de
primer orden (LPO) y la de orden superio (LOS). Su estudio no sólo es
históricamente relevante, además nos proporcionan ejemplos de un
comportamiento muy variado respecto al tema que nos ocupa :
• para LP hay cálculos correctos y completos y normalmente
terminan (esto es, proporcionan un procedimiento efectivo que
permite listar todos los elementos del conjunto de teoremas lógicos,
TEO);
• hay cálculos correctos y completos para LPO, pero ninguno termina
ya que el problema de la satisfacilbilidad para la lógica de primer
orden es indecidible.
•
LOS es incompleta con la semántica estándar, pero se pueden
definir cálculos completos cuando las fórmulas se interpretan en
modelos generales.
2. Mencionaremos algunos sistemas lógicos no clásicos porque la
variedad de demostraciones del teorema de completud es muy rica e
interesante:
• Las lógicas multimodales normalmente emplean la construcción del
modelo canónico para obtener resultados de completud de carácter
general, tales como los teoremas de Sahlqvist.
• Las lógicas descriptivas proporcionan buenos ejemplos de
resultados de completud (que terminan) para cálculos de tableaux
usando la cosntrucción de conjuntos máximamente consistentes.
• En lógicas híbridas normalmente se emplea la « construcción de
Henkin » para obtener resultados de completud tales como el Pure
Formulas Theorem.
3. También en la historia de la lógica hay numerosos ejemplos de
demostraciones indirectas de completud; por ejemplo, completud vía
interpolación, completud vía compacidad, completud vía traducción a una
lógica marco que sea completa, completud mediante modelos no estándar
para lógicas incompletas.
En la mayoría de los casos se cita la demostración de Henkin de 1950 o la de
1949.
Resultado universal de completud
¿Qué sentido tiene hablar de un resultado universal de completud?
Tenemos dos hipótesis de trabajo: La primera es que un resultado universal
podría alcanzarse generalizando la idea de Henkin para elaborar su
demostración de completud de primer orden a partir de su prueba de completud
para teoría de tipos. De hecho pensamos que la demostración de completud de
Blackburn para lógicas híbridas mediante designadores rígidos está en esa
línea.
La segunda sospecha, aunque no contamos con demasiados indicios, es que
una prueba de completud para lógicas que sólo poseen reglas estructurales
está directamente ligado al tema de la invariancia. Tarski no se pregunta ¿qué
es la lógica? ni tan siquiera ¿qué es una inferencia lógica? sino, ¿qué
conceptos son lógicos? Usa su propia definición semántica de consecuencia,
en la que sólo aparecen reglas estructurales, e intenta aplicar un programa que
había dado grandes resultados en matemáticas: definir conceptos utilizando
invariancias bajo ciertos grupos de transformaciones. De manera que un
concepto es lógico si podemos definir transformaciones pertinentes en el
universo que idealmente representa al de conjuntos del que extraemos las
estructuras y demostrar la invariancia del concepto bajo las transformaciones.
La jerarquía de tipos finitos es la idealización del universo más frecuentemente
empleada y las transformaciones pueden ser permutaciones, biyecciones,
isomorfismos, etc., según los distintos autores.
Bibliografía
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
Blackburn, Patrick; de Rijke, Maarten; Venema, Yde. [2001]. Modal
Logic. Cambridge University Press, Cambridge (UK),.
P. Blackburn, J. van Benthem and F. Wolter (eds). [2007]. Handbook of
Modal Logic. Elsevier.
ten Cate, Balder: Model theory for extended modal languages, ILLC
Dissertation Series DS-2005-01, University of Amsterdam, 2005.
van Benthem, J.F.A.K. [1979]. "Some Kinds of Modal Completeness".
Studia Logica
van Benthem, J.F.A.K. [2009]. Modal Logic for Open Minds. (in print)
Fine, Kit. [1978, 81]. "Model Theory for Modal Logic", Partes I-III. Part I y
II en Journal of Philosophical Logic 7, 1978, 125-156, 277-306; Parte III
en Journal of Philosophical Logic 10, 1981, 293-307.
Gabbay, Dov and Guenthner, Franz (eds.). [2001]. Handbook of
Philosophical Logic, Second Edition. Kluwer Academic Publishers.
Goldblatt, R. [1993]. “An Anstract Setting for Henkin’s Proofs” en
Mathematics of Modality. CSLI Lecture Notes Number 43
Henkin, Leon. [1950]. "Completeness in the theory of types". JSL. vol.
15. pp. 81-91.
Henkin, Leon. [1963]. "En Extension of the Craig-Lyndon Interpolation
Theorem". JSL. vol. 28, n. 3. pp. 201-216
Henkin, Leon. [1996]. "The discovery of my completeness proofs. Bulletin
of Symbolic Logic, vol. 2, Number 2, June 1996. (presentado el 24 de
Agosto de 1993 en el XIX International Congress of History of Science,
Zaragoza, Spain).
Kripke, Saul A. [1959]. "A completeness theorem in modal logic". JSL.
24, 1-14.
Manzano, María. [1996]. Extensions of first order logic. Number 19 in
Cambridge Tracts in Theoretical Computer Science. Cambridge
University Press. Cambridge. U.K. a 44. 25-37.
Manzano, M. [1999]. Model Theory. OUP. London
Sahlqvist, H. 1975"Completeness and Correspondence in the First and
Second Order Semantics for Modal Logic." In Proceedings of the 3rd
Scandinavian Logic Symposium, 110-143: North-Holland.
•
Tarski, A. [1986] "What are logical notions". History and Philosophy of
Logic. vol 7 (texto de la conferencia de Tarski del mismo título, editado
por Corcoran.)