Nivel 7 · Completitud en Lean (experto)

Panorama y estrategia

Este módulo presenta una demostración completa, verificada por máquina, del teorema de completitud de la deducción natural clásica proposicional, formalizada en Lean 4 y comprobada de modo que no depende de ningún supuesto no demostrado más allá de los fundamentos clásicos estándar del ecosistema Lean/Mathlib. Se fija un lenguaje de superficie con átomos, negación e implicación; se lo dota de la semántica clásica usual (tablas de verdad); y se define un cálculo genuino de deducción natural $\Gamma \Provnd \varphi$ con contextos, descarga de hipótesis y una regla de reducción al absurdo clásica. Después se demuestra la corrección (toda fórmula derivable es una tautología ) y la completitud (toda tautología es derivable a partir del contexto vacío), esta última mediante una realización constructiva del lema de Kalmár . La demostración no usa ningún «oráculo» externo ni ningún teorema de completitud de biblioteca, y se cierra con una auditoría de axiomas con #print axioms.

Alcance. Lo que se verifica por máquina es la corrección y la completitud del cálculo clásico sobre el fragmento $\{\neg,\to\}$ y a partir del contexto vacío. Aquí y en todo el módulo, $\neg$ y $\to$ dentro de un juicio $\Gamma \Provnd \varphi$ denotan los conectivos objeto, y fuera de él los conectivos meta de Lean; el contexto desambigua siempre. El enunciado matemático que se formaliza es exactamente el

del módulo 3, y la regla clásica que hace posible el argumento es la de la Nota 9.5.

La completitud como programa (Stansifer, 2001)

La inspiración rectora del capítulo es el artículo de Ryan Stansifer Completeness of Propositional Logic as a Program (Stansifer, 2001) . Stansifer subraya un punto de vista que se ha vuelto central en el razonamiento mecanizado moderno: una demostración constructiva de completitud puede ejecutarse como un programa que toma una tautología $\varphi$ y devuelve una derivación de $\varphi$ en un sistema de pruebas fijo. En su desarrollo, las fórmulas usan solo $\neg$ y $\to$ y las pruebas son árboles explícitos en un sistema de Hilbert (los axiomas de Łukasiewicz más modus ponens); el programa produce objetos de prueba y es correcto por construcción. El fundamento conceptual es el de toda la teoría de la demostración: los objetos de prueba son artefactos computacionales y pueden manipularse sistemáticamente.

Lean proporciona un marco donde esta idea se vuelve precisa: las pruebas son términos tipados, y la verificación de su corrección se delega a un núcleo pequeño y de confianza. Este módulo adopta la perspectiva de Stansifer, pero en el marco de la deducción natural en lugar de un cálculo de Hilbert, y lleva a cabo el argumento de forma interna: la derivación de cada tautología se construye a partir de las reglas genuinas de introducción/eliminación, sin recurrir a un procedimiento de decisión externo ni a un teorema de completitud importado. La estrategia es el argumento clásico de Kalmár (Kalmár, 1935) , que es naturalmente «ejecutable» en el sentido de Stansifer: dada la tabla de verdad de $\varphi$, produce una derivación concreta.

Dos niveles de lógica

La nota siguiente es la clave de lectura de todo el módulo; conviene tenerla presente en cada página.

El diccionario CIC

La distinción anterior se vuelve exacta en términos del CIC , la teoría de tipos que implementa el núcleo de Lean (Coquand y Huet, 1988) (Coquand y Paulin, 1990) (Carneiro, 2019) . La correspondencia entre las nociones lógicas de este módulo y las operaciones del núcleo es la siguiente.

La línea decisiva es la cuarta: una derivación es un término. Una prueba a nivel objeto no se describe, ni se afirma, ni se importa: se construye, como una estructura de datos finita, y el núcleo comprueba que tiene el tipo declarado. Un metateorema como la completitud es asimismo un término, del tipo $\Pi$ mostrado; construir ese término y verificar su tipo es demostrar el teorema.

Cómo leer este módulo

Cada página sigue el mismo formato del capítulo: cada pieza aparece primero como matemática ordinaria con su demostración completa, y luego como su realización en Lean línea por línea, con extractos transcritos de los archivos fuente del repositorio. Además, las secciones incluyen una breve nota Vista interna (CIC) que nombra el mecanismo que usa el código de Lean (aplicación de constructores, ND.rec, Formula.rec o el término $\Pi$ que habita el tipo). Estas notas permiten verificar, en cada paso, que el código construye exactamente el objeto que describe la matemática, sin laguna oculta ni apelación a una autoridad externa.

Un desarrollo en Lean es fiable en la medida en que (i) el núcleo acepta cada término, y (ii) el enunciado que uno lee es el enunciado que uno quiere decir. El punto (i) se garantiza automáticamente; el punto (ii) es responsabilidad humana, y es la razón de que cada declaración de Lean venga acompañada de su enunciado matemático.

Anticipo: la auditoría de axiomas

Lean rastrea de qué axiomas lógicos depende en definitiva un teorema; la orden #print axioms los reporta. La última página del módulo usa esto para certificar que el teorema de completitud no usa ningún sorry (ninguna laguna admitida) ni ninguna regla «oráculo» ad hoc: se reduce exactamente a tres axiomas,

#print axioms completeness_ND
-- 'completeness_ND' depends on axioms: [propext, Classical.choice, Quot.sound]

propext (extensionalidad proposicional), Classical.choice (el axioma de elección) y Quot.sound (corrección de los cocientes): los fundamentos clásicos estándar sobre los que se construye todo Mathlib, no supuestos específicos de este desarrollo. Los principios clásicos que el argumento usa (el tercero excluido en los análisis por casos y una elección al definir el literal lit) se reducen exactamente a esos tres axiomas; dónde entra cada uno se señala en el punto preciso en que ocurre.