Nivel 7 · Completitud en Lean (experto)

La auditoría de axiomas

Una formalización es tan honesta como sus dependencias. Deben excluirse dos modos de fallo: una laguna admitida (sorry) y una regla postulada ad hoc (un «oráculo»). El comando #print axioms de Lean informa el conjunto completo de axiomas lógicos de los que depende transitivamente un teorema; un sorry aflora como el pseudoaxioma sorryAx, y cualquier constante postulada aparecería por su nombre. Ejecutarlo sobre los resultados principales arroja lo siguiente. Extracto de Audit.lean.

#print axioms completeness_ND
-- 'completeness_ND' depends on axioms: [propext, Classical.choice, Quot.sound]
#print axioms soundComplete
-- 'soundComplete' depends on axioms: [propext, Classical.choice, Quot.sound]
#print axioms soundness
-- 'soundness' depends on axioms: [propext, Classical.choice, Quot.sound]
#print axioms ex_id
-- 'ex_id' does not depend on any axioms
#print axioms ex_dne
-- 'ex_dne' does not depend on any axioms

Qué es cada axioma

Los tres axiomas reportados son los fundamentos clásicos estándar sobre los que se construye todo Mathlib de Lean; no son específicos de este desarrollo.

propext (extensionalidad proposicional): dos proposiciones lógicamente equivalentes son iguales como términos de $\mathsf{Prop}$ .
Classical.choice (el axioma de elección): de la existencia no vacía de un tipo se extrae un habitante; de él se derivan el tercero excluido y Classical.propDecidable.
Quot.sound (corrección de los cocientes): elementos relacionados tienen la misma clase en el tipo cociente.

En particular:

No aparece ningún sorryAx: no hay lagunas admitidas.
No aparece ninguna constante llamada oracle (ni ningún teorema de completitud de biblioteca): la completitud es genuinamente interna.
Las derivaciones construidas a mano ex_id y ex_dne no dependen de ningún axioma, pues son términos de prueba finitos del tipo inductivo ND.

Dónde entra la lógica clásica

Los dos primeros axiomas no son decorativos: rastrean usos concretos del razonamiento clásico, todos en pasos ya señalados en las páginas anteriores.

En la corrección (Teorema 11.12), el caso de la RAA valida $\neg\neg\varphi \to \varphi$ en el metanivel mediante by_contra (bivalencia); por eso soundness depende de Classical.choice/propext.
En el lema de Kalmár (Lema 11.18), el caso de la negación usa la eliminación de la doble negación (not_not) y el de la implicación la equivalencia $\neg(P \to Q) \Leftrightarrow P \wedge \neg Q$ ; ambos son clásicos.
La semántica eval sobre Prop y el condicional de lit se deciden con Classical.propDecidable, que reposa en Classical.choice.
Quot.sound proviene de las estructuras de cociente de Mathlib (conjuntos, listas), no de un paso clásico del propio argumento.

Es decir, los tres axiomas marcan exactamente los puntos donde el contenido clásico de un teorema clásico se hace explícito; no hay clasicidad oculta en ningún otro lugar. Este es el certificado formal de que el

Teorema 11.22

es exactamente lo que afirma ser.

Validación cruzada con la biblioteca Foundation

El teorema de completitud de las páginas anteriores se sostiene por sí solo. De forma independiente, se verifica la misma adecuación semántica a través de la biblioteca Foundation (FormalizedFormalLogic) (FormalizedFormalLogic, 2024) , que ya contiene un teorema de completitud para un cálculo proposicional clásico. Deliberadamente no se importa en el desarrollo principal: la clausura completa de Mathlib usada por el núcleo y la usada por Foundation chocan en una declaración duplicada de Matrix.map, de modo que el apéndice se compila como un objetivo separado de Lake (Thesis.Prop.CompletenessViaFoundation). Nada del desarrollo principal depende de él.

Traducción a la sintaxis de Foundation

El cálculo clásico de Foundation se presenta sobre fórmulas en forma normal de negación, así que se traduce la sintaxis de superficie usando la identidad clásica $(\varphi \to \psi) \equiv (\neg\varphi \lor \psi)$ :

t(p) = p, \qquad t(\neg\varphi) = \neg\,t(\varphi), \qquad t(\varphi \to \psi) = \neg\,t(\varphi) \lor t(\psi).

Extracto de BridgeToFoundation.lean.

abbrev F : Type := LO.Propositional.NNFormula String

def tr : Formula → F
| .atom s   => LO.Propositional.NNFormula.atom s
| .neg p    => (∼ (tr p))
| .impl p q => (∼ (tr p)) ⋎ (tr q)

abbrev Sat (v : Valuation) (ψ : F) : Prop := v ⊧ ψ

El lema puente

Lema 11.24 (Preservación de la semántica)

Para toda valuación $v$ y toda fórmula de superficie $\varphi$ , $\;\llbracket \varphi \rrbracket_v \leftrightarrow \mathrm{Sat}(v, t(\varphi))$ .

Demostración.

A probar: $\llbracket \varphi \rrbracket_v \leftrightarrow \mathrm{Sat}(v, t(\varphi))$ , para toda $v$ y toda fórmula de superficie $\varphi$ . Por inducción estructural sobre $\varphi$ .

Átomo $\varphi = s$ . $t(s)$ es la variable correspondiente, y por definición de $\mathrm{Sat}$ , $\;\mathrm{Sat}(v, t(s)) = v(s) = \llbracket s \rrbracket_v$ .
Negación $\varphi = \neg p$ . Como $t(\neg p)$ es la negación de $t(p)$ , $\mathrm{Sat}(v, t(\neg p)) = \neg\,\mathrm{Sat}(v, t(p))$ . Por la hipótesis de inducción $\llbracket p \rrbracket_v \leftrightarrow \mathrm{Sat}(v, t(p))$ , se sigue $\llbracket \neg p \rrbracket_v \leftrightarrow \mathrm{Sat}(v, t(\neg p))$ .
Implicación $\varphi = p \to q$ . La traducción codifica la implicación como $t(p \to q) = (\neg\,t(p)) \lor t(q)$ , de modo que $\mathrm{Sat}(v, t(p \to q)) = \neg\,\mathrm{Sat}(v, t(p)) \lor \mathrm{Sat}(v, t(q))$ . Usando las hipótesis de inducción y la tautología clásica $(P \to Q) \leftrightarrow (\neg P \lor Q)$ : $\llbracket p \to q \rrbracket_v = (\llbracket p \rrbracket_v \to \llbracket q \rrbracket_v) \leftrightarrow (\neg\llbracket p \rrbracket_v \lor \llbracket q \rrbracket_v) \leftrightarrow (\neg\,\mathrm{Sat}(v, t(p)) \lor \mathrm{Sat}(v, t(q))) = \mathrm{Sat}(v, t(p \to q)).$

theorem eval_tr (v : Valuation) : ∀ φ : Formula, eval v φ ↔ Sat v (tr φ) := by
  intro φ
  induction φ with
  | atom s => simp [eval, tr, Sat]
  | neg p ih => simp [eval, tr, Sat, ih]
  | impl p q ihp ihq => simp [eval, tr, Sat, ihp, ihq]; tauto

Importación de la completitud de Foundation

Componer el lema puente con el teorema de completitud de la biblioteca proporciona, para toda tautología de superficie $\varphi$ , una demostración de Foundation de $t(\varphi)$ a partir de la teoría vacía. Esto suministra una confirmación independiente de que la noción de superficie de tautología coincide con la de la biblioteca y, por tanto, una corroboración externa de la adecuación. Extracto de CompletenessViaFoundation.lean.

theorem provable_tr_of_tautology (φ : Formula) :
    IsTautology φ → Provable (∅ : Theory) (tr φ) := by
  intro hTaut
  apply LO.Propositional.ClassicalSemantics.completeness!
  intro v hvT
  have : eval v φ := hTaut v
  exact (eval_tr v φ).1 this

Reproducir la auditoría

El desarrollo completo se compila con lake build desde la raíz del repositorio; las instrucciones detalladas están en su README. Los comandos #print axioms de Audit.lean se ejecutan durante la compilación, de modo que la auditoría de axiomas se reproduce con la misma orden; cualquier lector puede verificar por sí mismo que la salida es la reportada arriba.

Cierre: la completitud como programa

Se ha dado una demostración completa, verificada por el núcleo, de la adecuación de la deducción natural proposicional clásica:

\mathrm{Taut}(\varphi) \;\Longleftrightarrow\; \emptyset \Provnd \varphi.

La corrección es una inducción sobre reglas rutinaria; la completitud es el argumento de Kalmár llevado a cabo enteramente con las propias reglas de inferencia del sistema, mediante una construcción por valuación y un paso finito de descarga de átomos impulsado por un análisis por casos clásico derivado. La auditoría de axiomas certifica que la demostración está libre de lagunas admitidas y de toda regla de completitud postulada.

Conceptualmente, el desarrollo realiza el lema de Stansifer («la completitud como un programa») (Stansifer, 2001) en el marco de la deducción natural: la demostración del lema de Kalmár es un procedimiento efectivo que, dada la tabla de verdad de $\varphi$ , ensambla una derivación concreta, que el paso de descarga pliega luego en una derivación a partir del contexto vacío. La validación cruzada con Foundation refuerza la confianza en que la semántica de superficie es la pretendida.