Preámbulo · Lean desde cero

Ya puedes leer la tesis

Esta página no introduce ningún concepto nuevo. Propone un único ejercicio: leer el enunciado de un teorema real, copiado sin retoques del repositorio lean_execution, el código que acompaña a la tesis. Es el teorema principal:

theorem completeness_ND (φ : Formula) (h : IsTautology φ) :
    ND (∅ : Set Formula) φ

Hace ocho páginas, esta línea era ruido tipográfico. Ahora cada pieza tiene nombre. Léase despacio, de izquierda a derecha.

El enunciado, símbolo por símbolo

theorem completeness_ND. La declaración de la página 6: un teorema con nombre, para poder citarlo después. Lo que sigue, hasta los últimos dos puntos, son las hipótesis; lo que viene tras ellos es el enunciado, que es un tipo.

(φ : Formula). Un binder, con la misma forma que (x : Nat) en la página 2: introduce un argumento llamado φ y declara su tipo. Aquí el tipo no es Nat sino Formula, el tipo inductivo de las fórmulas proposicionales que la tesis define constructor por constructor (un átomo es una fórmula; si $\varphi$ y $\psi$ son fórmulas, $\varphi \to \psi$ es una fórmula). En prosa: «para toda fórmula $\varphi$».

(h : IsTautology φ). Otro binder, pero su tipo es una proposición, como en las páginas 5 y 6: h es una hipótesis con nombre, una prueba de que φ es tautología (verdadera bajo toda valuación). En prosa: «si $\varphi$ es tautología».

ND (∅ : Set Formula) φ. La conclusión. ND es el tipo inductivo del tercer guion de la página 7: sus constructores son las reglas de inferencia de la deducción natural , y ND Γ φ es el tipo de las derivaciones de φ a partir del contexto Γ. Aquí el contexto es ∅, con una ascripción como la de la página 1 ((∅ : Set Formula)) para decirle a Lean de qué tipo es ese conjunto vacío. Un habitante de este tipo es, por tanto, una derivación de φ sin hipótesis.

Juntando las piezas, el teorema se lee así: para toda fórmula $\varphi$, si $\varphi$ es tautología, entonces existe una derivación de $\varphi$ sin hipótesis. Es el teorema de completitud de la lógica proposicional, el resultado central de la tesis, el mismo que la ruta teórica enuncia como Teorema 9.12.

Esto es lo que el preámbulo quería lograr: que un enunciado formalizado real se lea con la misma naturalidad que su versión de pizarra, sabiendo qué es cada símbolo y por qué está ahí.

Tu mapa desde aquí

El preámbulo enseñó el lenguaje; el resto de la guía enseña por qué funciona y cómo se usa a fondo. Tres caminos, según el interés:

• La motivación y la ruta completa. El nivel 0, ¿por qué verificar?, cuenta qué problema resuelven los asistentes de pruebas y presenta el itinerario entero: del cálculo lambda (nivel 1) a la teoría de tipos de Lean (niveles 2 a 6), construyendo con rigor cada idea que aquí se dio por intuición.
• Directo al teorema. El módulo 7 recorre la formalización de la completitud línea por línea: la sintaxis de Formula, las reglas de ND, el lema de Kalmár y la demostración de completeness_ND tal como está en el código. Se puede leer ya, con solo este preámbulo; las referencias a la ruta teórica están enlazadas donde hagan falta.
• Las manos en el código. El repositorio lean_execution contiene la formalización completa. Abrirlo en un editor con Lean instalado regala lo que ninguna página estática puede: el infoview de verdad, respondiendo en vivo a cada táctica.

Ocho páginas atrás, Lean era una calculadora con una manía. Ahora es un lenguaje legible: tipos que se juzgan antes que los valores, funciones que son demostraciones, tácticas que escriben términos y reglas de inferencia que son constructores. Nada de esto sustituye a la tesis ni a la ruta; las vuelve legibles. Ese era el trato, y está cumplido.