| Autor(es) | Kurt Gödel (1906–1978); Martin H. Löb (1921–2006); Krister Segerberg (n. 1936); Robert M. Solovay (n. 1938) |
| Fecha / periodo | 1933–1976 · Siglo XX · Europa y Estados Unidos |
| Tipo | Formal |
| Deriva de | Lógica intuicionista · Lógica modal · Lógica de primer orden clásica · Formalismo y programa de Hilbert |
| Derivan de ella | Lógica de la justificación |
| Tres leyes | Identidad: ✓ (base clásica; \(\Box(A \to A)\) es teorema) · No contradicción: matizado (\(\neg(A \land \neg A)\) es teorema, pero la consistencia \(\neg\Box\bot\) no lo es) · Tercio excluso: ✓ para \(A\); no para la demostrabilidad (\(\Box A \lor \Box\neg A\) no es teorema) |
La lógica GL estudia qué leyes cumple el predicado de demostrabilidad de una teoría aritmética cuando se lo trata como un operador modal. Si \(\Box A\) significa «\(A\) es demostrable en la aritmética de Peano», ¿qué fórmulas modales son demostrables en la aritmética para toda interpretación de sus letras? La respuesta es sorprendentemente limpia: exactamente los teoremas de una lógica modal decidible con un único axioma característico, el de Löb. El gesto distintivo es convertir los teoremas de incompletitud de Gödel, que parecían resultados aislados y difíciles, en consecuencias de un cálculo proposicional. La demostrabilidad resulta ser una modalidad muy distinta de la necesidad metafísica: no satisface la reflexión \(\Box A \to A\).
Axiomas de GL.
Reglas. Modus ponens y necesitación (si \(\vdash A\), entonces \(\vdash \Box A\)).
El axioma 4, \(\Box A \to \Box\Box A\), es derivable (de Jongh, Kripke y Sambin, independientemente). El axioma T, \(\Box A \to A\), no lo es: con \(A = \bot\) daría \(\neg\Box\bot\), la consistencia.
Condiciones de derivabilidad (Hilbert y Bernays 1939, simplificadas por Löb 1955). Para el predicado de demostrabilidad \(\mathrm{Pr}\) de PA:
Corresponden a la necesitación, K y 4. Teorema de Löb (1955): si \(PA \vdash \mathrm{Pr}(\ulcorner A \urcorner) \to A\), entonces \(PA \vdash A\). Su formalización es el axioma de Löb.
Semántica de Kripke (Segerberg 1971). GL es correcta y completa respecto de los marcos transitivos y conversamente bien fundados (sin cadenas ascendentes infinitas de accesibilidad), y también respecto de los árboles finitos transitivos e irreflexivos. Tiene la propiedad del modelo finito, es decidible (PSPACE-completa) y no es compacta. No es canónica: el marco canónico no es conversamente bien fundado.
Completitud aritmética (Solovay, 1976). Una realización \(*\) asigna a cada letra un enunciado aritmético y traduce \(\Box\) por \(\mathrm{Pr}\).
Teorema del punto fijo (de Jongh y Sambin, 1975). Si \(p\) solo aparece bajo \(\Box\) en \(A(p)\), existe una fórmula \(B\) sin \(p\) tal que GL \(\vdash \Box(p \leftrightarrow A(p)) \leftrightarrow \Box(p \leftrightarrow B)\). Los enunciados autorreferentes tienen soluciones únicas y explícitas.
Ejemplos trabajados.
Relación con S4. Gödel (1933) tradujo la lógica intuicionista a S4 leyendo \(\Box\) como «demostrable», pero observó que el predicado formal de demostrabilidad no satisface \(\Box A \to A\) en la aritmética. GL es la respuesta a qué lógica obedece realmente. La lógica de Grzegorczyk (Grz), extensión de S4, corresponde a «demostrable y verdadero».
GL procede de cuatro fuentes. De la lógica intuicionista, a través de la traducción de Gödel (1933) a S4, recibe la idea de leer la necesidad como demostrabilidad. De la lógica modal toma el lenguaje, la axiomática normal y, con Segerberg, la semántica de Kripke. De la lógica de primer orden clásica y de la aritmética formalizada en ella toma el predicado de demostrabilidad con el que se interpreta \(\Box\). Del programa de Hilbert procede el análisis de las condiciones de derivabilidad: Hilbert y Bernays las formularon en Grundlagen der Mathematik II (1939) para demostrar con detalle el segundo teorema de incompletitud, y Löb (1955) las usó para su teorema. La formulación modal explícita llegó en los años setenta, con Macintyre y Simmons, Magari y su escuela en Siena y Boolos.
De la escuela rusa de la lógica de la demostrabilidad, en la que trabajaba Artemov, surge la lógica de la justificación, que plantea la misma pregunta para pruebas explícitas en lugar de la demostrabilidad existencial.
El libro de Boolos The Unprovability of Consistency (1979) difundió la disciplina; The Logic of Provability (1993) la resumió. Después se estudiaron lógicas de interpretabilidad, de demostrabilidad para teorías más fuertes y la lógica polimodal GLP de Japaridze, con aplicaciones al análisis ordinal. Para la pregunta «¿una lógica o muchas?» GL es un ejemplo de lógica no rival sino temática: la base es clásica, pero la modalidad se fija con exactitud por el objeto que interpreta. Muestra también que «necesario» no tiene una única lógica: la necesidad metafísica, la epistémica y la demostrabilidad aritmética obedecen principios distintos.