hmonroe/lean4-logic2

Lean4 Logic Formalization

lean4-logic

Formalizing Logic in Lean4

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

Table of Contents

• lean4-logic
  • Table of Contents
  • Usage
  • Structure
  • Propositional Logic
    • Definition
    • Theorem
  • 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
    • Basic
  • ManySorted: Many-sorted logic
    • Basic
  • FirstOrder: First-order logic
    • Basic
    • Computability: encodeing, computability
    • Completeness: Completeness theorem
    • Arith: Arithmetic
    • Incompleteness: Incompleteness theorem
  • SecondOrder: Monadic second-order logic
  • Modal: Variants of modal logics
    • Normal: Normal propositional modal logic

Propositional Logic

Definition

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

Theorem

• Soundness theorem

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

• Completeness theorem

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

First-Order Logic

$\mathbf{PA^-}$ is not to be included in $\mathbf{I\Sigma}_n$ or $\mathbf{PA}$ for simplicity in this formalization.

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 ⊧ₘ σ
$\mathbf{Eq}$	Axiom of equality	LO.FirstOrder.Theory.Eq	𝐄𝐪
$\mathbf{PA^-}$	Finitely axiomatized fragment of $\mathbf{PA}$	LO.FirstOrder.Arith.Theory.PAminus	𝐏𝐀⁻
$\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	𝐏𝐀

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.LogicK	𝐊
$\mathbf{KD}$	LO.Modal.Normal.LogicKD	𝐊𝐃
$\mathbf{S4}$	LO.Modal.Normal.LogicS4	𝐒𝟒	Alias of 𝐊𝐓𝟒.
$\mathbf{S4.2}$	LO.Modal.Normal.LogicS4Dot2	𝐒𝟒.𝟐
$\mathbf{S4.3}$	LO.Modal.Normal.LogicS4Dot3	𝐒𝟒.𝟑
$\mathbf{S4Grz}$	LO.Modal.Normal.LogicS4Grz	𝐒𝟒𝐆𝐫𝐳
$\mathbf{S5}$	LO.Modal.Normal.LogicS5	𝐒𝟓	Alias of 𝐊𝐓𝟓.
$\mathbf{GL}$	LO.Modal.Normal.LogicGL	𝐆𝐋

		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 β)))
  

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"