| Autor(es) | Sergei N. Artemov (n. 1951); Melvin Fitting (n. 1942) |
| Fecha / periodo | 1995–2005 · Siglo XX–XXI · Rusia y Estados Unidos |
| Tipo | Formal |
| Deriva de | Lógica intuicionista · Lógica modal · Lógica epistémica · Lógica de la demostrabilidad |
| Derivan de ella | — |
| Tres leyes | Identidad: ✓ (base clásica; hay término \(t\) con \(t{:}(A \to A)\)) · No contradicción: ✓ (base clásica; por reflexión ningún \(t{:}\bot\) es verdadero) · Tercio excluso: ✓ en la base, aunque LP sirve para dar semántica de pruebas a una lógica que lo rechaza |
La lógica de la justificación sustituye la modalidad implícita \(\Box A\), «\(A\) es demostrable» o «\(A\) se sabe», por un enunciado explícito \(t{:}A\), «\(t\) es una prueba (o justificación) de \(A\)». Los términos \(t\) tienen estructura y se combinan con operaciones que reflejan cómo se construyen las pruebas. El problema de fondo es antiguo: Gödel (1933) interpretó la lógica intuicionista en S4 leyendo \(\Box\) como demostrabilidad, pero la demostrabilidad formal en la aritmética no obedece S4, sino la lógica GL, porque la reflexión \(\Box A \to A\) no es demostrable. Faltaba, pues, una semántica de pruebas exacta para S4 y, con ella, para la interpretación BHK. El gesto de Artemov fue cambiar la demostrabilidad existencial («hay una prueba») por pruebas explícitas, con las que la reflexión sí vale. Con ello también se abre una epistemología formal en la que las razones son objetos del lenguaje.
Lenguaje de LP (Artemov, «Explicit provability and constructive semantics», Bulletin of Symbolic Logic, 2001). Términos de prueba: variables \(x, y, \dots\), constantes \(c\) y operaciones \(t \cdot s\) (aplicación), \(t + s\) (suma) y \(!t\) (verificación). Fórmulas: las proposicionales y \(t{:}F\).
Axiomas.
Reglas. Modus ponens y necesitación de axiomas: si \(A\) es un axioma, \(\vdash c{:}A\) para una constante \(c\). Una especificación de constantes fija qué constantes justifican qué axiomas.
Internalización. Si \(\vdash F\), existe un término \(p\) tal que \(\vdash p{:}F\). Es la versión explícita de la regla de necesitación.
Teorema de realización (Artemov 1995, 2001). Si se borran los términos y se sustituye cada \(t{:}F\) por \(\Box F\), los teoremas de LP son exactamente los de S4; y todo teorema de S4 puede «realizarse» sustituyendo cada \(\Box\) por un término adecuado. Se obtuvieron teoremas análogos para K (lógica J), T (JT), K4 (J4), S5 (JT45) y otras.
Completitud aritmética. LP es correcta y completa respecto de la interpretación en la aritmética de Peano en la que \(t{:}F\) se lee «\(t\) es el código de una prueba de \(F\)» con operaciones recursivas sobre pruebas. Resulta la cadena: lógica intuicionista \(\hookrightarrow\) S4 (Gödel) \(\hookrightarrow\) LP (realización) \(\hookrightarrow\) pruebas en PA. Es la formalización de la interpretación BHK que Gödel había esbozado en su conferencia de Zilsel (1938), publicada en 1995.
Semántica. Mkrtychev (1997) dio modelos de un solo mundo. Fitting («The logic of proofs, semantically», Annals of Pure and Applied Logic, 2005) dio modelos de Kripke con una función de evidencia \(\mathcal{E}(t, F)\), el conjunto de mundos en que \(t\) es evidencia admisible para \(F\). \(t{:}F\) es verdadero en \(w\) si y solo si \(w \in \mathcal{E}(t, F)\) y \(F\) vale en todos los mundos accesibles desde \(w\). Hay corrección y completitud.
Complejidad. La derivabilidad en LP está en \(\Pi^p_2\) (Kuznets 2000), por debajo de la PSPACE-completitud de S4.
Ejemplo de realización. En S4 vale \(\Box(A \land B) \to \Box A\). Su realización en LP es \(x{:}(A \land B) \to (c \cdot x){:}A\), donde \(c{:}(A \land B \to A)\) por necesitación de axiomas. El término \(c \cdot x\) registra cómo se obtiene la justificación de \(A\) a partir de la de \(A \land B\).
La lógica de la justificación nace de la escuela rusa de lógica de la demostrabilidad, a la que Artemov pertenecía en Moscú: el problema de qué modalidad corresponde a la demostrabilidad aritmética, resuelto para la demostrabilidad existencial por la lógica GL de Solovay, se plantea ahora para las pruebas explícitas. De la lógica modal recibe su forma: LP es la versión explícita de S4, y el programa se extendió a otras lógicas modales mediante teoremas de realización. De la lógica intuicionista toma su motivación principal: dar a la interpretación BHK, que dice que una prueba de \(A \to B\) es una construcción que transforma pruebas de \(A\) en pruebas de \(B\), una semántica exacta en términos de pruebas.
Con la lógica epistémica la relación es de reinterpretación: Artemov y Fitting leyeron \(K_a A\) como la forma implícita de «\(A\) está justificado por alguna razón» y usaron los términos para tratar la omnisciencia lógica y los casos de Gettier, en los que se cree algo verdadero por una razón equivocada.
El informe técnico de Cornell «Operational modal logic» (1995) presentó el sistema; la publicación de referencia es de 2001, y la semántica de Fitting de 2005 lo abrió a la epistemología. Desde entonces la lógica de la justificación se ha desarrollado como un campo propio, con lógicas multiagente, versiones de primer orden y aplicaciones a la teoría de la argumentación. Para la pregunta «¿una lógica o muchas?» es un ejemplo de reconciliación: una lógica clásica con términos de prueba explica con exactitud la lógica intuicionista y la modal S4, que parecían rivales o incomparables. Las distintas lógicas aparecen como niveles de explicitud sobre un mismo fenómeno: la prueba.