Nivel 7 · Completitud en Lean (experto)

NaturalDeduction.lean: el cálculo

Esta página define el objeto central del módulo: el cálculo de deducción natural $\Gamma \Provnd \varphi$ , primero como sistema de reglas y después, sin cambios, como tipo inductivo ND en Lean.

Codificar la falsedad dentro del fragmento

Como el lenguaje objeto no tiene un $\bot$ primitivo, se representa la falsedad mediante una fórmula canónica que es falsa bajo toda valuación.

Definición 11.6 (Falsedad objeto)

Se fija un átomo distinguido $p_0$ (en el código, la cadena "⊥"). Se define

\bot \;:=\; \neg(p_0 \to p_0).

Lema 11.7 (⊥ es semánticamente falsa)

Para toda valuación $v$ , $\;\llbracket \bot \rrbracket_v \leftrightarrow \mathrm{Falso}$ .

Demostración.

A probar: $\llbracket \bot \rrbracket_v \leftrightarrow \mathrm{Falso}$ para toda $v$ , donde $\bot \equiv \neg(p_0 \to p_0)$ .

( $\Rightarrow$ ) $\llbracket p_0 \to p_0 \rrbracket_v = (v(p_0) \to v(p_0))$ es verdadero para cualquier valor de $v(p_0)$ (la implicación identidad). Por tanto $\llbracket \bot \rrbracket_v = \llbracket \neg(p_0 \to p_0) \rrbracket_v = \neg\,\mathrm{Verdadero} = \mathrm{Falso}$ .
( $\Leftarrow$ ) $\mathrm{Falso}$ implica cualquier proposición; en particular $\llbracket \bot \rrbracket_v$ .

Extracto de NaturalDeduction.lean.

def Bot : Formula := ~(.atom "⊥" ⟶ .atom "⊥")

theorem eval_Bot (v : Valuation) : eval v Bot ↔ False := by
  constructor
  · intro h
    have hp : eval v (.atom "⊥" ⟶ .atom "⊥") := by intro hP; exact hP
    exact h hp
  · intro h; exact False.elim h

Matemática: las reglas

El juicio es $\Gamma \Provnd \varphi$ , donde $\Gamma$ es un conjunto de fórmulas. Se escribe $\Gamma, \varphi$ por $\Gamma \cup \{\varphi\}$ (en Lean, insert φ Γ). Son las reglas de deducción natural del módulo 3, restringidas al fragmento $\{\neg,\to\}$ : al núcleo intuicionista se le añade una única regla clásica, la reducción al absurdo. En la subsección siguiente cada una de estas siete reglas reaparece, sin cambios, como un constructor del tipo inductivo ND: es el mismo cálculo, leído ahora como tipo de datos. Los constructores conservan los nombres (en inglés) que tienen en Lean, de modo que la etiqueta del árbol y el constructor del código denotan la misma regla.

\frac{\varphi \in \Gamma}{\Gamma \Provnd \varphi}\ \texttt{hyp} \qquad \frac{\Gamma, \varphi \Provnd \psi}{\Gamma \Provnd \varphi \to \psi}\ \texttt{impI} \qquad \frac{\Gamma \Provnd \varphi \to \psi \quad \Gamma \Provnd \varphi}{\Gamma \Provnd \psi}\ \texttt{impE}

\frac{\Gamma, \varphi \Provnd \bot}{\Gamma \Provnd \neg\varphi}\ \texttt{negI} \qquad \frac{\Gamma \Provnd \neg\varphi \quad \Gamma \Provnd \varphi}{\Gamma \Provnd \bot}\ \texttt{negE} \qquad \frac{\Gamma \Provnd \bot}{\Gamma \Provnd \varphi}\ \texttt{botE} \qquad \frac{\Gamma, \neg\varphi \Provnd \bot}{\Gamma \Provnd \varphi}\ \texttt{classical}

Nota (El núcleo intuicionista y la regla clásica)

Las seis primeras reglas son el núcleo intuicionista; la última (reductio ad absurdum, llamada classical en el código) es lo que hace clásico al cálculo, tal como se anticipó en la Nota 9.5, y es exactamente lo que se necesita para la completitud respecto de la semántica clásica de tablas de verdad.

Código de Lean (tal como se implementa)

Extracto de NaturalDeduction.lean.

inductive ND : Set Formula → Formula → Prop
| hyp {Γ φ} : φ ∈ Γ → ND Γ φ
| impI {Γ φ ψ} : ND (insert φ Γ) ψ → ND Γ (φ ⟶ ψ)
| impE {Γ φ ψ} : ND Γ (φ ⟶ ψ) → ND Γ φ → ND Γ ψ
| negI {Γ φ} : ND (insert φ Γ) Bot → ND Γ (~φ)
| negE {Γ φ} : ND Γ (~φ) → ND Γ φ → ND Γ Bot
| botE {Γ φ} : ND Γ Bot → ND Γ φ
| classical {Γ φ} : ND (insert (~φ) Γ) Bot → ND Γ φ

Cada constructor es una de las reglas anteriores, leída de arriba abajo como «premisas $\to$ conclusión». La descarga de hipótesis es implícita en el uso de insert: una premisa ND (insert φ Γ) … es una subderivación en la que $\varphi$ está disponible como supuesto, y formar la conclusión lo elimina del contexto. Crucialmente, no hay constructor oráculo: toda forma de construir una derivación es una de estas siete reglas genuinas.

Vista interna (CIC). Esta declaración extiende el entorno del núcleo con la familia ND, los siete constructores ND.hyp, …, ND.classical y el eliminador ND.rec, cuyo tipo (omitiendo los contextos implícitos) es el principio de inducción para derivaciones:

ND.rec :
  (C : (Γ : Set Formula) → (φ : Formula) → ND Γ φ → Prop) →   -- el motivo
  (case_hyp : …) → (case_impI : …) → … → (case_classical : …) → -- una por regla
  ∀ {Γ φ} (d : ND Γ φ), C Γ φ d

Esto es «inducción sobre la altura de una derivación» por dos razones: ND es la menor familia cerrada bajo sus constructores, de modo que sus únicos habitantes son árboles finitos de constructores (fijar el motivo $C$ en cada constructor lo fija para todas las derivaciones); y eliminar un inductivo de $\mathsf{Prop}$ hacia $\mathsf{Prop}$ siempre está permitido, que es el caso de todos los motivos de este módulo. Por tanto «por inducción sobre la derivación» es ND.rec (e induction d with | hyp … su azúcar sintáctico). Dicho como un hecho que el lector no familiarizado con Lean puede retener: existe una derivación de $\varphi$ a partir de $\Gamma$ en deducción natural si y solo si el tipo ND Γ φ está habitado. El tipo no es una codificación aproximada de las pruebas: es el conjunto de las pruebas. La ausencia de un octavo constructor «oráculo» no es, por tanto, una elección estilística sino un hecho estructural sobre el tipo: nada puede habitar ND Γ φ salvo una derivación genuina.