lean4-logic

Formalizing Logic in Lean4

https://iehality.github.io/lean4-logic/

Table of Contents

• lean4-logic
  • Table of Contents
  • Usage
  • Structure
  • Classical Propositional Logic
    • Definition
    • Theorem
  • Intuitionistic Propositional Logic
    • Definitions
    • Kripkean Semantics
      • Defininitions
      • Theorems
  • First-Order Logic
    • Definition
    • Theorem
  • Normal Modal Logic
    • Definition
    • Theorem
  • References

Usage

Add following to lakefile.lean.

require logic from git "https://github.com/iehality/lean4-logic"

Structure

The key results are summarised in Logic/Summary.lean.

• Logic
  • Vorspiel: Supplementary definitions and theorems for Mathlib
  • Logic
  • AutoProver: Automated theorem proving based on proof search
  • Propositional: Propositional logic
    • Classical: Classical propositional logic
      • Basic
    • Intuitionistic: Intuitionistic propositional logic
      • Kriple: Kripke semantics
  • FirstOrder: First-order logic
    • Basic
    • Computability: encodeing, computability
    • Completeness: Completeness theorem
    • Arith: Arithmetic
    • Incompleteness: Incompleteness theorem
  • Modal: Variants of modal logics
    • Normal: Normal propositional modal logic

Classical Propositional Logic

Definition

		Definition	Notation
$(\rm Cut)\vdash_\mathrm{T} \Gamma$	Derivation in Tait-Calculus + Cut	LO.Propositional.Classical.Derivation	⊢¹ Γ
$v \models p$	Tarski's truth definition condition	LO.Propositional.Classical.semantics	v ⊧ p

Theorem

• Soundness theorem

  theorem LO.Propositional.Classical.soundness
    {α : Type u_1}
    {T : LO.Propositional.Theory α}
    {p : LO.Propositional.Formula α} :
    T ⊢ p → T ⊨ p

• Completeness theorem

  noncomputable def LO.Propositional.Classical.completeness
      {α : Type u_1}
      {T : LO.Propositional.Theory α}
      {p : LO.Propositional.Formula α} :
      T ⊨ p → T ⊢ p

Intuitionistic Propositional Logic

Definitions

		Definition	Notation
$\Gamma \vdash \varphi$	Deduction	LO.Propositional.Intuitionistic.Deduction	Γ ⊢ᴵ p
	Deductive (Exists deduction)	LO.Propositional.Intuitionistic.Deductive	Γ ⊢ᴵ! p

Kripkean Semantics

Defininitions

		Definition	Notation
$w \Vdash^M \varphi$	Satisfy on Kripkean Model $M$ and its world $w$	LO.Propositional.Intuitionistic.Formula.KripkeSatisfies	w ⊩[M] p
$M \vDash \varphi$	Models	LO.Propositional.Intuitionistic.Formula.KripkeModels	M ⊧ p
$\Gamma \models \varphi$	Conequences	LO.Propositional.Intuitionistic.Formula.KripkeConsequence	Γ ⊨ᴵ p

Theorems

• Soundness

  theorem Kripke.sounds {Γ : Theory β} {p : Formula β} : (Γ ⊢ᴵ! p) → (Γ ⊨ᴵ p)

• Completeness

  theorem Kripke.completes
    [DecidableEq β] [Encodable β]
    {Γ : Theory β} {p : Formula β} : (Γ ⊨ᴵ p) → (Γ ⊢ᴵ! p)

• Disjunction Property

  theorem Deduction.disjunctive
    [DecidableEq β] [Encodable β]
    {p q : Formula β} : (∅ ⊢ᴵ! p ⋎ q) → (∅ ⊢ᴵ! p) ∨ (∅ ⊢ᴵ! q)

First-Order Logic

Definition

		Definition	Notation
$(\rm Cut)\vdash_\mathrm{T} \Gamma$	Derivation in Tait-Calculus + Cut	LO.FirstOrder.Derivation	⊢¹ Γ
$M \models \sigma$	Tarski's truth definition condition	LO.FirstOrder.Models	M ⊧ₘ σ
$T \triangleright U$	Theory interpretation	LO.FirstOrder.TheoryInterpretation	T ⊳ U
$\mathbf{EQ}$	Axiom of equality	LO.FirstOrder.Theory.eqAxiom	𝐄𝐐
$\mathbf{PA^-}$	Finitely axiomatized fragment of $\mathbf{PA}$	LO.FirstOrder.Arith.Theory.peanoMinus	𝐏𝐀⁻
$\mathbf{I}_\mathrm{open}$	Induction of open formula	LO.FirstOrder.Arith.Theory.iOpen	𝐈open
$\mathbf{I\Sigma}_n$	Induction of $\Sigma_n$ formula	LO.FirstOrder.Arith.Theory.iSigma	𝐈𝚺
$\mathbf{PA}$	Peano arithmetic	LO.FirstOrder.Arith.Theory.peano	𝐏𝐀
$\mathbf{EA}$	elementary arithmetic	LO.FirstOrder.Arith.Theory.elementaryArithmetic	𝐄𝐀

Theorem

• Cut-elimination

  def LO.FirstOrder.Derivation.hauptsatz
      {L : LO.FirstOrder.Language}
      [(k : ℕ) → DecidableEq (LO.FirstOrder.Language.Func L k)]
      [(k : ℕ) → DecidableEq (LO.FirstOrder.Language.Rel L k)]
      {Δ : LO.FirstOrder.Sequent L} :
      ⊢¹ Δ → { d : ⊢¹ Δ // LO.FirstOrder.Derivation.CutFree d }

• Soundness theorem

  theorem LO.FirstOrder.soundness
      {L : LO.FirstOrder.Language}
      {T : Set (LO.FirstOrder.Sentence L)}
      {σ : LO.FirstOrder.Sentence L} :
      T ⊢ σ → T ⊨ σ

• Completeness theorem

  noncomputable def LO.FirstOrder.completeness
      {L : LO.FirstOrder.Language}
      {T : LO.FirstOrder.Theory L}
      {σ : LO.FirstOrder.Sentence L} :
      T ⊨ σ → T ⊢ σ

• Gödel's first incompleteness theorem

  theorem LO.FirstOrder.Arith.first_incompleteness
      (T : LO.FirstOrder.Theory ℒₒᵣ)
      [DecidablePred T]
      [𝐄𝐐 ≾ T]
      [𝐏𝐀⁻ ≾ T]
      [LO.FirstOrder.Arith.SigmaOneSound T]
      [LO.FirstOrder.Theory.Computable T] :
      ¬LO.System.Complete T

  • undecidable sentence

    theorem LO.FirstOrder.Arith.undecidable
        (T : LO.FirstOrder.Theory ℒₒᵣ)
        [DecidablePred T]
        [𝐄𝐐 ≾ T]
        [𝐏𝐀⁻ ≾ T]
        [LO.FirstOrder.Arith.SigmaOneSound T]
        [LO.FirstOrder.Theory.Computable T] :
        T ⊬ LO.FirstOrder.Arith.FirstIncompleteness.undecidable T ∧
        T ⊬ ~LO.FirstOrder.Arith.FirstIncompleteness.undecidable T

Normal Modal Logic

Definition

In this formalization, (Modal) Logic means set of axioms.

Logic	Definition	Notation	Remarks
$\mathbf{K}$	LO.Modal.Normal.AxiomSet.K	𝐊
$\mathbf{KD}$	LO.Modal.Normal.AxiomSet.KD	𝐊𝐃
$\mathbf{S4}$	LO.Modal.Normal.AxiomSet.S4	𝐒𝟒	Alias of 𝐊𝐓𝟒.
$\mathbf{S4.2}$	LO.Modal.Normal.AxiomSet.S4Dot2	𝐒𝟒.𝟐
$\mathbf{S4.3}$	LO.Modal.Normal.AxiomSet.S4Dot3	𝐒𝟒.𝟑
$\mathbf{S4Grz}$	LO.Modal.Normal.AxiomSet.S4Grz	𝐒𝟒𝐆𝐫𝐳
$\mathbf{S5}$	LO.Modal.Normal.AxiomSet.S5	𝐒𝟓	Alias of 𝐊𝐓𝟓.
$\mathbf{GL}$	LO.Modal.Normal.AxiomSet.GL	𝐆𝐋

		Definition	Notation
$M, w \models \varphi$	Satisfy	LO.Modal.Normal.Formula.Satisfies	w ⊧ᴹˢ[M] φ
$M \models \varphi$	Valid on model (Models)	LO.Modal.Normal.Formula.Models	⊧ᴹᵐ[M] φ
$F \models \varphi$	Valid on frame (Frames)	LO.Modal.Normal.Formula.Frames	⊧ᴹᶠ[F] φ
$\Gamma \models^F \varphi$	Consequence on frame	LO.Modal.Normal.Formula.FrameConsequence	Γ ⊨ᴹᶠ[F] φ
$\Gamma \vdash_{\Lambda} \varphi$	Hilbert-style Deduction on logic $\Lambda$	LO.Modal.Normal.Deduction	Γ ⊢ᴹ[Λ] φ

Theorem

• Soundness of Hilbert-style deduction for 𝐊 extend 𝐓, 𝐁, 𝐃, 𝟒, 𝟓 Extensions (i.e. 𝐊𝐃, 𝐒𝟒, 𝐒𝟓, etc.)

  theorem LO.Modal.Normal.Logic.Hilbert.sounds
      {α : Type u} [Inhabited α]
      {β : Type u} [Inhabited β]
      (Λ : AxiomSet α)
      (f : Frame β) (hf : f ∈ (FrameClass β α Λ))
      {p : LO.Modal.Normal.Formula α}
      (h : ⊢ᴹ[Λ] p) :
      ⊧ᴹᶠ[f] p

  • Consistency

    theorem LO.Modal.Normal.Logic.Hilbert.consistency
        {α : Type u}
        {β : Type u}
        (Λ : AxiomSet α)
        (hf : ∃ f, f ∈ (FrameClass β α Λ)) :
        ⊬ᴹ[Λ]! ⊥

  • WIP: Currently, these theorems was proved where only Λ is 𝐊, 𝐊𝐃, 𝐒𝟒, 𝐒𝟓.
• Strong Completeness of Hilbert-style deduction for 𝐊 extend 𝐓, 𝐁, 𝐃, 𝟒, 𝟓 Extensions

  def Completeness
    {α β : Type u}
    (Λ : AxiomSet β)
    (𝔽 : FrameClass α)
    := ∀ (Γ : Theory β) (p : Formula β), (Γ ⊨ᴹ[𝔽] p) → (Γ ⊢ᴹ[Λ]! p)
  
  theorem LogicK.Hilbert.completes
    {β : Type u} [inst✝ : DecidableEq β] :
    Completeness
      (𝐊 : AxiomSet β)
      (𝔽((𝐊 : AxiomSet β)) : FrameClass (MaximalConsistentTheory (𝐊 : AxiomSet β)))

• Gödel-McKensey-Tarski Theorem

  def GTranslation : Intuitionistic.Formula α → Formula α
  postfix:75 "ᵍ" => GTranslation
  
  theorem companion_Int_S4
    [DecidableEq α] [Encodable α] [Inhabited α]
    {p : Intuitionistic.Formula β} : (∅ ⊢! p) ↔ (∅ ⊢ᴹ[𝐒𝟒]! pᵍ)

References

• J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis
• W. Pohlers, Proof Theory: The First Step into Impredicativity
• P. Hájek, P. Pudlák, Metamathematics of First-Order Arithmetic
• R. Kaye, Models of Peano arithmetic
• 田中 一之, ゲーデルと20世紀の論理学
• 菊池 誠 (編者), 『数学における証明と真理 ─ 様相論理と数学基礎論』
• P. Blackburn, M. de Rijke, Y. Venema, "Modal Logic"
• Open Logic Project, "The Open Logic Text"
• R. Hakli, S. Negri, "Does the deduction theorem fail for modal logic?"
• G. Boolos, "The Logic of Provability"
• Huayu Guo, Dongheng Chen, Bruno Bentzen, "Verified completeness in Henkin-style for intuitionistic propositional logic"
  • https://arxiv.org/abs/2310.01916
  • https://github.com/bbentzen/ipl