Nivel 7 · Completitud en Lean (experto)

Reglas estructurales y derivadas

Antes de la corrección y la completitud se registran tres lemas que se usan repetidamente. Cada uno es un metateorema demostrado por inducción sobre reglas o exhibiendo una derivación.

Debilitamiento (monotonía en el contexto)

Lema 11.8 (Debilitamiento)

Si Γ⊢NDφ\Gamma \Provnd \varphi y Γ⊆Δ\Gamma \subseteq \Delta, entonces Δ⊢NDφ\Delta \Provnd \varphi.

Demostración.

A probar: Δ⊢NDφ\Delta \Provnd \varphi, bajo las hipótesis Γ⊢NDφ\Gamma \Provnd \varphi y Γ⊆Δ\Gamma \subseteq \Delta.

Por inducción sobre la derivación de Γ⊢NDφ\Gamma \Provnd \varphi, generalizando sobre Δ\Delta (la hipótesis de inducción, abreviada HI, queda disponible para cualquier contexto que incluya al de la premisa). En todos los casos se dispone de Γ⊆Δ\Gamma \subseteq \Delta y, por monotonía de la inserción, de Γ,ψ⊆Δ,ψ\Gamma, \psi \subseteq \Delta, \psi para toda fórmula ψ\psi. Se tratan uno por uno los siete constructores; en cada caso la última regla de la derivación se reaplica sobre Δ\Delta. Se muestran completos tres casos representativos; los cuatro restantes (→\toE, ¬\negE, ⊥\botE y RAA) siguen exactamente el mismo patrón que su análogo mostrado (reaplicar la regla sobre las conclusiones de las HI, con la misma inclusión o su versión insertada), y están escritos en su totalidad en la tesis.

  1. hipótesis. La derivación es φ∈ΓΓ⊢NDφ\dfrac{\varphi \in \Gamma}{\Gamma \Provnd \varphi}. De φ∈Γ\varphi \in \Gamma y Γ⊆Δ\Gamma \subseteq \Delta se sigue φ∈Δ\varphi \in \Delta, y: φ∈ΔΔ⊢NDφ (hipoˊtesis).\frac{\varphi \in \Delta}{\Delta \Provnd \varphi}\ \text{(hipótesis).}
  2. →\toI. Termina en Γ,φ⊢NDψΓ⊢NDφ→ψ\dfrac{\Gamma, \varphi \Provnd \psi}{\Gamma \Provnd \varphi \to \psi}. La HI aplicada a la premisa con Γ,φ⊆Δ,φ\Gamma, \varphi \subseteq \Delta, \varphi da Δ,φ⊢NDψ\Delta, \varphi \Provnd \psi, y: Δ,φ⊢NDψΔ⊢NDφ→ψ (→I).\frac{\Delta, \varphi \Provnd \psi}{\Delta \Provnd \varphi \to \psi}\ (\to\mathrm{I}).
  3. ¬\negI. Termina en Γ,φ⊢ND⊥Γ⊢ND¬φ\dfrac{\Gamma, \varphi \Provnd \bot}{\Gamma \Provnd \neg\varphi}. La HI con Γ,φ⊆Δ,φ\Gamma, \varphi \subseteq \Delta, \varphi da Δ,φ⊢ND⊥\Delta, \varphi \Provnd \bot, y: Δ,φ⊢ND⊥Δ⊢ND¬φ (¬I).\frac{\Delta, \varphi \Provnd \bot}{\Delta \Provnd \neg\varphi}\ (\neg\mathrm{I}).

En cada caso la conclusión es la requerida sobre Δ\Delta, lo que cierra la inducción.

Extracto de NaturalDeduction.lean.

theorem weakening {Γ φ} (d : ND Γ φ) : ∀ {Δ}, Γ ⊆ Δ → ND Δ φ := by
  induction d with
  | hyp hmem => intro Δ hsub; exact ND.hyp (hsub hmem)
  | impI _ ih => intro Δ hsub; exact ND.impI (ih (insert_subset_insert hsub))
  | impE _ _ ih1 ih2 => intro Δ hsub; exact ND.impE (ih1 hsub) (ih2 hsub)
  | negI _ ih => intro Δ hsub; exact ND.negI (ih (insert_subset_insert hsub))
  | negE _ _ ih1 ih2 => intro Δ hsub; exact ND.negE (ih1 hsub) (ih2 hsub)
  | botE _ ih => intro Δ hsub; exact ND.botE (ih hsub)
  | classical _ ih => intro Δ hsub; exact ND.classical (ih (insert_subset_insert hsub))

Las siete ramas | reflejan exactamente los siete casos de la demostración; insert_subset_insert es el lema de Mathlib Γ⊆Δ⇒(Γ,χ)⊆(Δ,χ)\Gamma \subseteq \Delta \Rightarrow (\Gamma, \chi) \subseteq (\Delta, \chi) usado en los tres casos con descarga.

Vista interna (CIC). induction d se elabora a ND.rec aplicado con el motivo

C Γ φ (_:ND Γ φ)  :=  ∀ Δ, Γ⊆Δ→ND Δ φ.C\,\Gamma\,\varphi\,(\_ : \texttt{ND}\ \Gamma\ \varphi) \;:=\; \forall\,\Delta,\ \Gamma \subseteq \Delta \to \texttt{ND}\ \Delta\ \varphi.

Obsérvese que el motivo es a su vez un tipo Π\Pi (cuantifica sobre Δ\Delta); por eso la demostración «generaliza sobre Δ\Delta» antes de inducir. Cada rama proporciona la premisa menor correspondiente de ND.rec y, al poder usar las hipótesis de inducción ih, reconstruye la conclusión con el mismo constructor sobre el contexto mayor. Todo el bloque de tácticas se elabora a un único término cerrado de tipo ∀ {Γ φ}, ND Γ φ → ∀ {Δ}, Γ ⊆ Δ → ND Δ φ.

Introducción de doble negación

Lema 11.9 (Introducción de doble negación)

Si Γ⊢NDφ\Gamma \Provnd \varphi entonces Γ⊢ND¬¬φ\Gamma \Provnd \neg\neg\varphi.

Demostración.

A probar: Γ⊢ND¬¬φ\Gamma \Provnd \neg\neg\varphi, bajo la hipótesis d:Γ⊢NDφd : \Gamma \Provnd \varphi. Se construye la derivación paso a paso.

  1. Como ¬φ∈Γ,¬φ\neg\varphi \in \Gamma, \neg\varphi, la regla de hipótesis da Γ,¬φ⊢ND¬φ\Gamma, \neg\varphi \Provnd \neg\varphi (1).
  2. Por debilitamiento (Lema 11.8) de dd con Γ⊆Γ,¬φ\Gamma \subseteq \Gamma, \neg\varphi: Γ,¬φ⊢NDφ\Gamma, \neg\varphi \Provnd \varphi (2).
  3. ¬\negE sobre (1) y (2): Γ,¬φ⊢ND⊥\Gamma, \neg\varphi \Provnd \bot (3).
  4. ¬\negI descargando ¬φ\neg\varphi en (3): Γ⊢ND¬¬φ\Gamma \Provnd \neg\neg\varphi.

El árbol completo es:

Extracto de NaturalDeduction.lean.

theorem dni {Γ φ} (d : ND Γ φ) : ND Γ (~~φ) := by
  apply ND.negI
  exact ND.negE (ND.hyp (Set.mem_insert _ _)) (weakening d (Set.subset_insert _ _))

Demostración por casos clásica

El siguiente lema es el motor del paso de descarga de átomos de la página 7. Es «la ley del tercero excluido, usada en silencio»: nunca se forma un objeto disyunción, simplemente se divide la prueba.

Lema 11.10 (Análisis por casos derivado)

Si Γ,φ⊢NDχ\Gamma, \varphi \Provnd \chi y Γ,¬φ⊢NDχ\Gamma, \neg\varphi \Provnd \chi, entonces Γ⊢NDχ\Gamma \Provnd \chi.

Demostración.

A probar: Γ⊢NDχ\Gamma \Provnd \chi, bajo las hipótesis d1:Γ,φ⊢NDχd_1 : \Gamma, \varphi \Provnd \chi y d2:Γ,¬φ⊢NDχd_2 : \Gamma, \neg\varphi \Provnd \chi.

Estrategia. Se aplica RAA; basta derivar Γ,¬χ⊢ND⊥\Gamma, \neg\chi \Provnd \bot. Para ello se construyen dos subderivaciones, (i)(i) y (ii)(ii), y se combinan con ¬\negE.

Subderivación (i)(i): Γ,¬χ⊢ND¬φ\Gamma, \neg\chi \Provnd \neg\varphi.

Subderivación (ii)(ii): Γ,¬χ⊢ND¬¬φ\Gamma, \neg\chi \Provnd \neg\neg\varphi.

Combinación. Con (ii)(ii) como ¬ψ\neg\psi y (i)(i) como ψ\psi (tomando ψ=¬φ\psi = \neg\varphi), la regla ¬\negE y luego RAA cierran la prueba:

Γ,¬χ⊢ND¬¬φΓ,¬χ⊢ND¬φΓ,¬χ⊢ND⊥ (¬E)Γ,¬χ⊢ND⊥Γ⊢NDχ (RAA).\frac{\Gamma, \neg\chi \Provnd \neg\neg\varphi \quad \Gamma, \neg\chi \Provnd \neg\varphi} {\Gamma, \neg\chi \Provnd \bot}\ (\neg\mathrm{E}) \qquad \frac{\Gamma, \neg\chi \Provnd \bot}{\Gamma \Provnd \chi}\ (\text{RAA}).

Extracto de NaturalDeduction.lean.

theorem byCases {Γ φ χ} (d1 : ND (insert φ Γ) χ) (d2 : ND (insert (~φ) Γ) χ) :
    ND Γ χ := by
  apply ND.classical
  have e1 : ND (insert (~χ) Γ) (~φ) := by
    apply ND.negI
    refine ND.negE (ND.hyp ?_) (weakening d1 ?_)
    · exact Set.mem_insert_of_mem _ (Set.mem_insert _ _)
    · exact Set.insert_subset_insert (Set.subset_insert _ _)
  have e2 : ND (insert (~χ) Γ) (~~φ) := by
    apply ND.negI
    refine ND.negE (ND.hyp ?_) (weakening d2 ?_)
    · exact Set.mem_insert_of_mem _ (Set.mem_insert _ _)
    · exact Set.insert_subset_insert (Set.subset_insert _ _)
  exact ND.negE e2 e1

Vista interna (CIC). dni y byCases no son inducciones: cada uno ensambla directamente un término ND a partir de constructores. Por ejemplo, dni d se elabora a

ND.negI (ND.negE (ND.hyp … ) (weakening d … )),\texttt{ND.negI}\ \big(\texttt{ND.negE}\ (\texttt{ND.hyp}\ \dots)\ (\texttt{weakening}\ d\ \dots)\big),

un árbol de constructores cuyas hojas son la hipótesis y el debilitamiento (construido recursivamente) de dd. Los bloques have e1 … := by … en byCases construyen las dos subderivaciones como subtérminos nombrados, y exact ND.negE e2 e1 los inserta en el constructor ¬\negE. Así, estas «reglas derivadas» son admisibles por construcción: cada una es una función que devuelve una derivación genuina, no una nueva primitiva del cálculo.