refactor

Logic/FirstOrder/Incompleteness/FirstIncompleteness.lean

@@ -191,8 +191,6 @@ end representation
 
 namespace FirstIncompleteness
 
-attribute [instance] Classical.propDecidable
-
 variable (T)
 
 private lemma diagRefutation_re : RePred (fun σ => T ⊢! ~σ&[⸢σ⸣]) := by
@@ -220,24 +218,22 @@ lemma diagRefutation_spec (σ : FormulaFin ℒₒᵣ 1) :
 
 lemma independent : System.Independent T γ := by
   have h : T ⊢! γ ↔ T ⊢! ~γ := by simpa using diagRefutation_spec T ρ
-  constructor
-  · intro b
-    exact inconsistent_of_provable_and_refutable' b (h.mp b) (consistent_of_sigmaOneSound T)
-  · intro b
-    exact inconsistent_of_provable_and_refutable' (h.mpr b) b (consistent_of_sigmaOneSound T)
+  exact
+    ⟨System.unprovable_iff_not_provable.mpr
+       (fun b => inconsistent_of_provable_and_refutable' b (h.mp b) (consistent_of_sigmaOneSound T)),
+     System.unprovable_iff_not_provable.mpr
+       (fun b => inconsistent_of_provable_and_refutable' (h.mpr b) b (consistent_of_sigmaOneSound T))⟩
 
 theorem main : ¬System.Complete T := System.incomplete_iff_exists_independent.mpr ⟨γ, independent T⟩
 
 end FirstIncompleteness
 
-attribute [-instance] Classical.propDecidable
-
 variable (T : Theory ℒₒᵣ) [DecidablePred T] [EqTheory T] [PAminus T] [SigmaOneSound T] [Theory.Computable T]
 
 theorem first_incompleteness : ¬System.Complete T := FirstIncompleteness.main T
 
 lemma undecidable :
-    ¬T ⊢! FirstIncompleteness.undecidableSentence T ∧ ¬T ⊢! ~FirstIncompleteness.undecidableSentence T :=
+    T ⊬ FirstIncompleteness.undecidableSentence T ∧ T ⊬ ~FirstIncompleteness.undecidableSentence T :=
   FirstIncompleteness.independent T
 
 end Arith

Logic/Logic/LogicSymbol.lean

@@ -9,31 +9,62 @@ section logicNotation
 @[notation_class] class Tilde (α : Sort _) where
   tilde : α → α
 
-prefix:75 "~" => Tilde.tilde
-
 @[notation_class] class Arrow (α : Sort _) where
   arrow : α → α → α
 
-infixr:60 " ⟶ " => Arrow.arrow
-
 @[notation_class] class Wedge (α : Sort _) where
   wedge : α → α → α
 
-infixr:69 " ⋏ " => Wedge.wedge
-
 @[notation_class] class Vee (α : Sort _) where
   vee : α → α → α
 
-infixr:68 " ⋎ " => Vee.vee
-
 class LogicSymbol (α : Sort _)
   extends Top α, Bot α, Tilde α, Arrow α, Wedge α, Vee α
 
 @[notation_class] class UnivQuantifier (α : ℕ → Sort _) where
   univ : ∀ {n}, α (n + 1) → α n
 
+@[notation_class] class ExQuantifier (α : ℕ → Sort _) where
+  ex : ∀ {n}, α (n + 1) → α n
+
+@[notation_class] class UnivQuantifier₂ (α : ℕ → ℕ → Sort _) where
+  univ₂₁ : ∀ {m n}, α (m + 1) n → α m n
+  univ₂₂ : ∀ {m n}, α m (n + 1) → α m n
+
+@[notation_class] class ExQuantifier₂ (α : ℕ → ℕ → Sort _) where
+  ex₂₁ : ∀ {m n}, α (m + 1) n → α m n
+  ex₂₂ : ∀ {m n}, α m (n + 1) → α m n
+
+prefix:75 "~" => Tilde.tilde
+
+infixr:60 " ⟶ " => Arrow.arrow
+
+infixr:69 " ⋏ " => Wedge.wedge
+
+infixr:68 " ⋎ " => Vee.vee
+
 prefix:64 "∀' " => UnivQuantifier.univ
 
+prefix:64 "∃' " => ExQuantifier.ex
+
+prefix:64 "∀¹ " => UnivQuantifier₂.univ₂₁
+prefix:64 "∀² " => UnivQuantifier₂.univ₂₂
+
+prefix:64 "∃¹ " => ExQuantifier₂.ex₂₁
+prefix:64 "∃² " => ExQuantifier₂.ex₂₂
+
+attribute [match_pattern]
+  Tilde.tilde
+  Arrow.arrow
+  Wedge.wedge
+  Vee.vee
+  UnivQuantifier.univ
+  ExQuantifier.ex
+  UnivQuantifier₂.univ₂₁
+  UnivQuantifier₂.univ₂₂
+  ExQuantifier₂.ex₂₁
+  ExQuantifier₂.ex₂₂
+
 section UnivQuantifier
 
 variable {α : ℕ → Sort u} [UnivQuantifier α]
@@ -42,17 +73,12 @@ def univClosure : {n : ℕ} → α n → α 0
   | 0,     a => a
   | _ + 1, a => univClosure (∀' a)
 
-@[simp] lemma univ_closure_zero (a : α 0) : univClosure a = a := rfl
+@[simp] lemma univClosure_zero (a : α 0) : univClosure a = a := rfl
 
-@[simp] lemma univ_closure_succ {n} (a : α (n + 1)) : univClosure a = univClosure (∀' a) := rfl
+@[simp] lemma univClosure_succ {n} (a : α (n + 1)) : univClosure a = univClosure (∀' a) := rfl
 
 end UnivQuantifier
 
-@[notation_class] class ExQuantifier (α : ℕ → Sort _) where
-  ex : ∀ {n}, α (n + 1) → α n
-
-prefix:64 "∃' " => ExQuantifier.ex
-
 section ExQuantifier
 
 variable {α : ℕ → Sort u} [ExQuantifier α]
@@ -61,13 +87,55 @@ def exClosure : {n : ℕ} → α n → α 0
   | 0,     a => a
   | _ + 1, a => exClosure (∃' a)
 
-@[simp] lemma ex_closure_zero (a : α 0) : exClosure a = a := rfl
+@[simp] lemma exClosure_zero (a : α 0) : exClosure a = a := rfl
 
-@[simp] lemma ex_closure_succ {n} (a : α (n + 1)) : exClosure a = exClosure (∃' a) := rfl
+@[simp] lemma exClosure_succ {n} (a : α (n + 1)) : exClosure a = exClosure (∃' a) := rfl
 
 end ExQuantifier
 
-attribute [match_pattern] Tilde.tilde Arrow.arrow Wedge.wedge Vee.vee UnivQuantifier.univ ExQuantifier.ex
+section UnivQuantifier₂
+
+variable {α : ℕ → ℕ → Sort u} [UnivQuantifier₂ α]
+
+def univClosure₂₁ : {m n : ℕ} → α m n → α 0 n
+  | 0,     _, a => a
+  | _ + 1, _, a => univClosure₂₁ (∀¹ a)
+
+def univClosure₂₂ : {m n : ℕ} → α m n → α m 0
+  | _, 0,     a => a
+  | _, _ + 1, a => univClosure₂₂ (∀² a)
+
+@[simp] lemma univClosure₂₁_zero {n} (a : α 0 n) : univClosure₂₁ a = a := rfl
+
+@[simp] lemma univClosure₂₁_succ {m n} (a : α (m + 1) n) : univClosure₂₁ a = univClosure₂₁ (∀¹ a) := rfl
+
+@[simp] lemma univClosure₂₂_zero {m} (a : α m 0) : univClosure₂₂ a = a := rfl
+
+@[simp] lemma univClosure₂₂_succ {m n} (a : α m (n + 1)) : univClosure₂₂ a = univClosure₂₂ (∀² a) := rfl
+
+end UnivQuantifier₂
+
+section ExQuantifier₂
+
+variable {α : ℕ → ℕ → Sort u} [ExQuantifier₂ α]
+
+def exClosure₂₁ : {m n : ℕ} → α m n → α 0 n
+  | 0,     _, a => a
+  | _ + 1, _, a => exClosure₂₁ (∃¹ a)
+
+def exClosure₂₂ : {m n : ℕ} → α m n → α m 0
+  | _, 0,     a => a
+  | _, _ + 1, a => exClosure₂₂ (∃² a)
+
+@[simp] lemma exClosure₂₁_zero {n} (a : α 0 n) : exClosure₂₁ a = a := rfl
+
+@[simp] lemma exClosure₂₁_succ {m n} (a : α (m + 1) n) : exClosure₂₁ a = exClosure₂₁ (∃¹ a) := rfl
+
+@[simp] lemma exClosure₂₂_zero {m} (a : α m 0) : exClosure₂₂ a = a := rfl
+
+@[simp] lemma exClosure₂₂_succ {m n} (a : α m (n + 1)) : exClosure₂₂ a = exClosure₂₂ (∃² a) := rfl
+
+end ExQuantifier₂
 
 @[notation_class] class HasTurnstile (α : Sort _) (β : Sort _) where
   turnstile : Set α → α → β
@@ -216,6 +284,16 @@ notation:64 "∃[" p "] " q => bex p q
 
 end quantifier
 
+class AndOrClosed {F} [LogicSymbol F] (C : F → Prop) where
+  verum  : C ⊤
+  falsum : C ⊥
+  and {f g : F} : C f → C g → C (f ⋏ g)
+  or  {f g : F} : C f → C g → C (f ⋎ g)
+
+class Closed {F} [LogicSymbol F] (C : F → Prop) extends AndOrClosed C where
+  not {f : F} : C f → C (~f)
+  imply {f g : F} : C f → C g → C (f ⟶ g)
+
 end LogicSymbol
 
 end LO

Logic/Logic/System.lean

@@ -38,9 +38,15 @@ abbrev Provable (T : Set F) (f : F) : Prop := Nonempty (T ⊢ f)
 
 infix:45 " ⊢! " => System.Provable
 
+abbrev Unprovable (T : Set F) (f : F) : Prop := IsEmpty (T ⊢ f)
+
+infix:45 " ⊬ " => System.Unprovable
+
+lemma unprovable_iff_not_provable {T : Set F} {f : F} : T ⊬ f ↔ ¬T ⊢! f := by simp[System.Unprovable]
+
 protected def Complete (T : Set F) : Prop := ∀ f, (T ⊢! f) ∨ (T ⊢! ~f)
 
-def Independent (T : Set F) (f : F) : Prop := ¬T ⊢! f ∧ ¬T ⊢! ~f
+def Independent (T : Set F) (f : F) : Prop := T ⊬ f ∧ T ⊬ ~f
 
 lemma incomplete_iff_exists_independent {T : Set F} :
     ¬System.Complete T ↔ ∃ f, Independent T f := by simp[System.Complete, not_or, Independent]

Logic/Summary.lean

@@ -9,21 +9,25 @@ open LO.FirstOrder
 
 variable {L : Language} [∀ k, DecidableEq (L.func k)] [∀ k, DecidableEq (L.rel k)] {T : Theory L}
 
+/- Cut elimination for Tait-calculus -/
 theorem cut_elimination {Δ : Sequent L} : ⊢ᶜ Δ → ⊢ᵀ Δ := DerivationCR.hauptsatz
 
+/- Soundness theorem -/
 theorem soundness_theorem {σ : Sentence L} : T ⊢ σ → T ⊨ σ := FirstOrder.soundness
 
+/- Completeness theorem -/
 theorem completeness_theorem {σ : Sentence L} : T ⊨ σ → T ⊢ σ := FirstOrder.completeness
 
 open Arith FirstIncompleteness
 
-variable (T : Theory ℒₒᵣ) [EqTheory T] [PAminus T] [DecidablePred T] [SigmaOneSound T] [Theory.Computable T]
+variable (T : Theory ℒₒᵣ) [DecidablePred T] [EqTheory T] [PAminus T] [SigmaOneSound T] [Theory.Computable T]
 
+/- Gödel's first incompleteness theorem -/
 theorem first_incompleteness_theorem : ¬System.Complete T :=
   FirstOrder.Arith.first_incompleteness T
 
-theorem undecidable_sentence :
-    ¬T ⊢! undecidableSentence T ∧ ¬T ⊢! ~undecidableSentence T :=
+/- Undecidable sentence  -/
+theorem undecidable_sentence : T ⊬ undecidableSentence T ∧ T ⊬ ~undecidableSentence T :=
   FirstOrder.Arith.undecidable T
 
 end LO.Summary.FirstOrder

README.md

@@ -28,14 +28,34 @@ Formalizing Logic in Lean4
 | $T \vdash \sigma$                   | Proof, Provability                  |  `LO.FirstOrder.Proof`          | `T ⊢ σ`, `T ⊢! σ` |
 
 ## Theorem
+
 ### First-Order logic
 
-|                                | Proof                                    | 
-| ----                           | ----                                     |
-| Soundness theorem              | `@soundness : ∀ {L : Language} [inst : (k : ℕ) → DecidableEq (Language.func L k)] [inst_1 : (k : ℕ) → DecidableEq (Language.rel L k)] {T : Set (Sentence L)} {σ : Sentence L}, T ⊢ σ → T ⊨ σ` |
-| Completeness theorem           | `@completeness : {L : Language} → [inst : (k : ℕ) → DecidableEq (Language.func L k)] → [inst_1 : (k : ℕ) → DecidableEq (Language.rel L k)] → {T : Theory L} → {σ : Sentence L} → T ⊨ σ → T ⊢ σ` |
-| Cut-elimination                | `@DerivationCR.hauptsatz : {L : Language} → [inst : (k : ℕ) → DecidableEq (Language.func L k)] → [inst_1 : (k : ℕ) → DecidableEq (Language.rel L k)] → {Δ : Sequent L} → ⊢ᶜ Δ → ⊢ᵀ Δ` |
-| First incompleteness theorem   | `@Arith.first_incompleteness : ∀ (T : Theory Language.oRing) [inst : DecidablePred T] [inst_1 : EqTheory T] [inst_2 : Arith.PAminus T] [inst_3 : Arith.SigmaOneSound T] [inst : Theory.Computable T], ¬System.Complete T` |
+- Cut-elimination
+```lean
+theorem cut_elimination {Δ : Sequent L} : ⊢ᶜ Δ → ⊢ᵀ Δ := DerivationCR.hauptsatz
+```
+
+- Soundness theorem
+```lean
+theorem soundness_theorem {σ : Sentence L} : T ⊢ σ → T ⊨ σ := FirstOrder.soundness
+```
+
+- Completeness theorem
+```lean
+theorem completeness_theorem {σ : Sentence L} : T ⊨ σ → T ⊢ σ := FirstOrder.completeness
+```
+
+- Gödel's first incompleteness theorem
+```lean
+theorem first_incompleteness_theorem :
+    ¬System.Complete T := FirstOrder.Arith.first_incompleteness T
+```
+
+```lean
+theorem undecidable_sentence :
+    T ⊬ undecidableSentence T ∧ T ⊬ ~undecidableSentence T := FirstOrder.Arith.undecidable T
+```
 
 ## References
 - J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis