Nivel 7 · Completitud en Lean (experto)

Corrección y consistencia

La corrección es la mitad fácil de la adecuación: toda fórmula derivable es semánticamente válida. Su demostración es la inducción sobre reglas por excelencia, y conviene subrayar desde el principio en qué nivel vive: es un teorema meta acerca del cálculo objeto (Nota 11.1), demostrado con los conectivos y las tácticas de Lean, no con las reglas de ND.

Matemática

Se escribe $v \models \Gamma$ por « $\llbracket \psi \rrbracket_v$ se cumple para toda $\psi \in \Gamma$ ».

Lema 11.11 (Satisfacción de un contexto extendido)

Si $\llbracket \chi \rrbracket_v$ se cumple y $v \models \Gamma$ , entonces $v \models \Gamma, \chi$ .

Demostración.

A probar: $v \models \Gamma, \chi$ , es decir, $\llbracket \psi \rrbracket_v$ para toda $\psi \in \Gamma, \chi$ , bajo las hipótesis $\llbracket \chi \rrbracket_v$ y $v \models \Gamma$ . Sea $\psi \in \Gamma, \chi = \{\chi\} \cup \Gamma$ . Hay dos casos:

$\psi = \chi$ : entonces $\llbracket \psi \rrbracket_v = \llbracket \chi \rrbracket_v$ se cumple por la primera hipótesis.
$\psi \in \Gamma$ : entonces $\llbracket \psi \rrbracket_v$ se cumple porque $v \models \Gamma$ (segunda hipótesis).

En ambos casos $\llbracket \psi \rrbracket_v$ , luego $v \models \Gamma, \chi$ .

Teorema 11.12 (Corrección)

Si $\Gamma \Provnd \varphi$ , entonces para toda valuación $v$ con $v \models \Gamma$ se cumple $\llbracket \varphi \rrbracket_v$ .

Demostración.

A probar: para toda valuación $v$ con $v \models \Gamma$ se cumple $\llbracket \varphi \rrbracket_v$ .

Por inducción sobre la derivación de $\Gamma \Provnd \varphi$ . Se fija $v$ con $v \models \Gamma$ y se analiza la última regla aplicada; «HI» abrevia la hipótesis de inducción sobre la(s) subderivación(es). Toda la demostración transcurre a nivel meta: cada caso convierte una regla del cálculo objeto en el paso lógico correspondiente de Lean. Se muestran completos cuatro casos representativos, incluidos los dos delicados ( $\neg$ I y RAA); los tres restantes son análogos y están escritos en su totalidad en la tesis: $\to$ E es el modus ponens a nivel meta aplicado a las dos HI, $\neg$ E combina las dos HI en $\mathrm{Falso} = \llbracket \bot \rrbracket_v$ , y $\bot$ E obtiene $\mathrm{Falso}$ de su HI y de ahí cualquier meta.

hipótesis ( $\varphi \in \Gamma$ ). Meta: $\llbracket \varphi \rrbracket_v$ . Como $v \models \Gamma$ y $\varphi \in \Gamma$ , se cumple $\llbracket \varphi \rrbracket_v$ por definición de $v \models \Gamma$ .
$\to$ I (premisa $\Gamma, \varphi \Provnd \psi$ ). Meta: $\llbracket \varphi \to \psi \rrbracket_v$ , que por definición es $\llbracket \varphi \rrbracket_v \to \llbracket \psi \rrbracket_v$ . Se supone $\llbracket \varphi \rrbracket_v$ ; por el Lema 11.11, $v \models \Gamma, \varphi$ , y la HI sobre la premisa da $\llbracket \psi \rrbracket_v$ .
$\neg$ I (premisa $\Gamma, \varphi \Provnd \bot$ ). Meta: $\llbracket \neg\varphi \rrbracket_v = \neg\llbracket \varphi \rrbracket_v$ . Se supone $\llbracket \varphi \rrbracket_v$ ; entonces $v \models \Gamma, \varphi$ (Lema 11.11) y la HI da $\llbracket \bot \rrbracket_v$ , que es $\mathrm{Falso}$ (Lema 11.7). La suposición es insostenible, luego $\neg\llbracket \varphi \rrbracket_v$ .
RAA (premisa $\Gamma, \neg\varphi \Provnd \bot$ ). Meta: $\llbracket \varphi \rrbracket_v$ . Supóngase, por contradicción, $\neg\llbracket \varphi \rrbracket_v$ ; entonces $\llbracket \neg\varphi \rrbracket_v$ se cumple, así que $v \models \Gamma, \neg\varphi$ , y la HI da $\llbracket \bot \rrbracket_v = \mathrm{Falso}$ : contradicción. Luego $\llbracket \varphi \rrbracket_v$ . (Único caso que apela al principio clásico a nivel meta.)

Corolario 11.13 (Los teoremas son tautologías)

Si $\emptyset \Provnd \varphi$ entonces $\mathrm{Taut}(\varphi)$ .

Demostración.

A probar: $\mathrm{Taut}(\varphi)$ , es decir, $\llbracket \varphi \rrbracket_v$ para toda $v$ . Se aplica el Teorema 11.12 con $\Gamma = \emptyset$ : para cualquier $v$ , la hipótesis $v \models \emptyset$ se cumple de forma vacua (no hay fórmulas en $\emptyset$ ), de modo que el teorema entrega $\llbracket \varphi \rrbracket_v$ . Como $v$ es arbitraria, $\mathrm{Taut}(\varphi)$ .

Corolario 11.14 (Consistencia)

$\bot$ no es derivable a partir del contexto vacío: $\;\neg(\emptyset \Provnd \bot)$ .

Demostración.

A probar: $\neg(\emptyset \Provnd \bot)$ . Supóngase, por contradicción, que $\emptyset \Provnd \bot$ . Por el Corolario 11.13, $\bot$ sería una tautología, es decir, $\llbracket \bot \rrbracket_v$ para toda $v$ . Pero por el Lema 11.7, $\llbracket \bot \rrbracket_v = \mathrm{Falso}$ para toda $v$ : contradicción. Por tanto $\neg(\emptyset \Provnd \bot)$ .

Código de Lean (tal como se implementa)

Extracto de NaturalDeduction.lean.

theorem sat_insert {v : Valuation} {Γ : Set Formula} {χ : Formula}
    (hχ : eval v χ) (hΓ : ∀ ψ ∈ Γ, eval v ψ) :
    ∀ ψ ∈ insert χ Γ, eval v ψ := by
  intro ψ hψ
  rcases Set.mem_insert_iff.1 hψ with h | h
  · subst h; exact hχ
  · exact hΓ ψ h

theorem soundness {Γ φ} (d : ND Γ φ) :
    ∀ v, (∀ ψ ∈ Γ, eval v ψ) → eval v φ := by
  induction d with
  | hyp hmem => intro v hv; exact hv _ hmem
  | impI _ ih => intro v hv hp; exact ih v (sat_insert hp hv)
  | impE _ _ ih1 ih2 => intro v hv; exact (ih1 v hv) (ih2 v hv)
  | negI _ ih => intro v hv hp; exact (eval_Bot v).1 (ih v (sat_insert hp hv))
  | negE _ _ ih1 ih2 => intro v hv; exact (eval_Bot v).2 ((ih1 v hv) (ih2 v hv))
  | botE _ ih => intro v hv; exact ((eval_Bot v).1 (ih v hv)).elim
  | classical _ ih =>
      intro v hv
      by_contra hnp
      exact (eval_Bot v).1 (ih v (sat_insert hnp hv))

theorem isTautology_of_provable {φ} (d : ND (∅ : Set Formula) φ) : IsTautology φ := by
  intro v; refine soundness d v ?_; intro ψ hψ; simp at hψ

theorem not_provable_Bot : ¬ ND (∅ : Set Formula) Bot := by
  intro d
  exact (eval_Bot (fun _ => True)).1 (isTautology_of_provable d (fun _ => True))

Las siete ramas de soundness son los siete casos anteriores; (eval_Bot v).1 y .2 son las dos direcciones del Lema 11.7; el by_contra de la rama classical es el único paso clásico.

Vista interna (CIC). De nuevo induction d es ND.rec, ahora con el motivo valuado en $\mathsf{Prop}$

C\,\Gamma\,\varphi\,(\_) \;:=\; \forall v,\ \big(\forall \psi \in \Gamma,\ \texttt{eval}\ v\ \psi\big) \to \texttt{eval}\ v\ \varphi.

La corrección y la completitud eliminan el mismo inductivo ND hacia dos motivos $\mathsf{Prop}$ distintos: la validez semántica aquí y, dentro de Kalmár, la derivabilidad desde contextos de literales allá. Ambas eliminaciones son legítimas porque los blancos son proposiciones. El paso by_contra es donde el nivel meta usa Classical.choice/propext, razón por la cual soundness aparece en la auditoría de axiomas con esas constantes.