Nivel 3 · Lógica y deducción natural

La perspectiva constructiva: BHK y NJ

La equivalencia $\Gamma \vdash \psi \iff \Gamma \vDash \psi$ de las páginas anteriores agota la lógica clásica, pero la correspondencia de Curry–Howard no se aplica a ella, sino a su núcleo constructivo: la lógica intuicionista. La diferencia es filosófica. La lógica clásica descansa en la verdad absoluta y en la ley del medio excluido ( $p \vee \neg p$ ), que obliga a aceptar como ciertos enunciados cuya verdad quizá nunca pueda exhibirse. La lógica intuicionista reemplaza la pregunta «¿es verdadera?» por «¿qué cuenta como una prueba?». Esta página sigue a Sørensen y Urzyczyn (2006) .

Semántica intuitiva: la interpretación BHK

La interpretación de Brouwer–Heyting–Kolmogorov (BHK) define el significado de cada conectivo en términos de la construcción que lo prueba.

Definición 9.17 (Interpretación BHK)

Una construcción (o prueba) de una fórmula se define por recursión:

de $\phi_1 \land \phi_2$ : un par formado por una prueba de $\phi_1$ y una de $\phi_2$ ;
de $\phi_1 \lor \phi_2$ : un índice $i \in \{1, 2\}$ junto con una prueba de $\phi_i$ (debe especificarse cuál caso se prueba);
de $\phi_1 \to \phi_2$ : un método (función) que transforma toda prueba de $\phi_1$ en una de $\phi_2$ ;
de $\bot$ : no existe ninguna.

La negación $\neg\phi$ abrevia $\phi \to \bot$ ; así, una prueba de $\neg\phi$ es un método que transforma toda prueba de $\phi$ en una de $\bot$ .

El carácter algorítmico de esta lectura es la base de Curry–Howard: la prueba deja de ser una derivación estática y se vuelve un objeto computacional.

Ejemplo 9.18 (Tautologías clásicas bajo BHK)

Muchas tautologías clásicas no son teoremas intuicionistas por carecer de contenido constructivo.

$p \to \neg\neg p$ (válida). Su forma es $p \to ((p \to \bot) \to \bot)$ : dada una prueba de $p$ y un método de $p \to \bot$ , se aplica el método a la prueba para obtener $\bot$ .
$\neg\neg p \to p$ (inválida). Requeriría un método universal que extraiga una prueba de $p$ de una prueba de $\neg\neg p$ , que en general no existe.
$p \lor \neg p$ (inválida). Probarla exigiría un procedimiento general que, para cualquier $p$ , decida y aporte una prueba de $p$ o una de $\neg p$ ; tal procedimiento no existe en general.

Deducción natural intuicionista: el sistema NJ

El sistema de deducción natural intuicionista de Gentzen, denotado NJ (la «J» indica intuicionista), es una restricción del clásico: el núcleo de reglas sin RAA ni LEM (módulo la abreviatura $\neg\varphi := \varphi\to\bot$ que NJ adopta, bajo la cual $\neg\mathrm{i}$ y $\neg\mathrm{e}$ son instancias de $\to$ I y $\to$ E).

Definición 9.19 (Lenguaje proposicional intuicionista)

El conjunto $\Phi$ de fórmulas se define por la gramática $\Phi ::= \bot \mid PV \mid (\Phi \to \Phi) \mid (\Phi \lor \Phi) \mid (\Phi \land \Phi),$ con $PV$ el conjunto de variables proposicionales. La negación $\neg \varphi$ abrevia $\varphi \to \bot$ , y $\varphi \leftrightarrow \psi$ abrevia $(\varphi \to \psi) \land (\psi \to \varphi)$ .

El sistema opera sobre secuentes $\Gamma \vdash \varphi$ , donde $\Gamma$ es un contexto (conjunto finito de fórmulas). La derivabilidad $\vdash$ es la menor relación cerrada bajo el siguiente axioma y reglas.

Axioma.

$\Gamma, \varphi \vdash \varphi \quad (\mathrm{Ax})$

Conjunción.

\dfrac{\Gamma \vdash \varphi \quad \Gamma \vdash \psi}{\Gamma \vdash \varphi \land \psi}\ (\land\mathrm{I}) \qquad \dfrac{\Gamma \vdash \varphi \land \psi}{\Gamma \vdash \varphi}\ (\land\mathrm{E}_1) \qquad \dfrac{\Gamma \vdash \varphi \land \psi}{\Gamma \vdash \psi}\ (\land\mathrm{E}_2)

Disyunción.

\dfrac{\Gamma \vdash \varphi}{\Gamma \vdash \varphi \lor \psi}\ (\lor\mathrm{I}_1) \qquad \dfrac{\Gamma \vdash \psi}{\Gamma \vdash \varphi \lor \psi}\ (\lor\mathrm{I}_2) \qquad \dfrac{\Gamma \vdash \varphi \lor \psi \quad \Gamma, \varphi \vdash \rho \quad \Gamma, \psi \vdash \rho}{\Gamma \vdash \rho}\ (\lor\mathrm{E})

Implicación.

\dfrac{\Gamma, \varphi \vdash \psi}{\Gamma \vdash \varphi \to \psi}\ (\to\mathrm{I}) \qquad \dfrac{\Gamma \vdash \varphi \to \psi \quad \Gamma \vdash \varphi}{\Gamma \vdash \psi}\ (\to\mathrm{E})

Contradicción. No hay regla de introducción para $\bot$ ; solo la eliminación (principio de explosión):

$\dfrac{\Gamma \vdash \bot}{\Gamma \vdash \varphi}\ (\bot\mathrm{E})$

La solidez y la completitud de NJ se demuestran en la literatura con la semántica de Kripke (Sørensen y Urzyczyn, 2006) . Lo esencial aquí es que añadir RAA (o LEM) a NJ recupera la lógica clásica de las páginas anteriores: NJ es su corazón constructivo.

Incompleta respecto de las tablas de verdad

La fórmula $p \vee \neg p$ es una tautología : es verdadera bajo toda valuación (Definición 9.10). Sin embargo, el punto 3 del Ejemplo 9.18 muestra que carece de prueba constructiva: no es derivable en NJ. La lógica intuicionista es, por tanto, incompleta respecto de la semántica de tablas de verdad: existen fórmulas válidas en toda valuación que NJ no demuestra. Cada sistema es sólido y completo respecto de su semántica (NJ respecto de la de Kripke, el cálculo clásico respecto de las tablas), y ya se vio el fenómeno recíproco: RAA y LEM dejan de ser sólidas para la semántica de Kripke (Teorema 9.11).

Nota 9.16 (Lo clásico y lo constructivo en esta tesis)

Vale la pena anticipar cómo encajan los dos mundos, porque el resto del recorrido vive en ambos. El teorema de completitud que se formaliza en Lean (nivel 7, próximamente) es clásico: su cálculo objeto admite la reducción al absurdo. Pero la herramienta que lo verifica (la teoría de tipos regida por Curry–Howard, que se construye en los niveles siguientes) es de raíz constructiva. Por eso este recorrido por la lógica intuicionista no es un desvío: es el fundamento del asistente de pruebas en el que, más adelante, una derivación clásica se construye y se comprueba como un término. Vale la pena además recordar por qué el teorema objeto debe ser clásico: la lógica intuicionista es incompleta respecto de las tablas de verdad ( $p\vee\neg p$ es válida en toda valuación pero no es teorema intuicionista), y es esa laguna la que el argumento de Kalmár (Teorema 9.12) salva apelando al medio excluido. La completitud respecto de tablas de verdad es, en este sentido, un fenómeno clásico.

Hacia Curry–Howard

Según BHK, una prueba de $\phi_1 \to \phi_2$ es un método que transforma pruebas; el lenguaje preciso para describir tales métodos es el cálculo lambda del nivel 1. La correspondencia exacta entre las derivaciones de NJ y los términos tipados, proposiciones como tipos y pruebas como programas, es el isomorfismo de Curry–Howard (Wadler, 2015) : el tema del nivel 4 (próximamente), y la razón última de que en Lean una derivación sea un término.