refactor(Logics/Propositional): classical and intuitionistic inference systems

Cslib.lean

@@ -131,3 +131,4 @@ public import Cslib.Logics.LinearLogic.CLL.MLL
 public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
 public import Cslib.Logics.Propositional.Defs
 public import Cslib.Logics.Propositional.NaturalDeduction.Basic
+public import Cslib.Logics.Propositional.NaturalDeduction.Theory

Cslib/Computability/Automata/NA/Concat.lean

@@ -177,7 +177,7 @@ theorem finConcat_language_eq [Inhabited Symbol] :
     obtain ⟨ss, ⟨_, h_ωtr⟩, _⟩ := concat_run_exists h_xl1 h_run2
     #adaptation_note
     /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
-    have h_mtr := LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (xl1.length + xl2.length))
+    have h_mtr := LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (a := xl1.length + xl2.length))
     simp [← append_append_ωSequence, extract_eq_drop_take,
       take_append_of_le_length, ← List.length_append] at h_mtr
     have : ss (xl1.length + xl2.length) = (ss.drop xl1.length) xl2.length := by grind

Cslib/Logics/Propositional/Defs.lean

@@ -6,7 +6,7 @@ Authors: Thomas Waring
 
 module
 
-public import Cslib.Init
+public import Cslib.Foundations.Logic.InferenceSystem
 public import Mathlib.Data.FunLike.Basic
 public import Mathlib.Data.Set.Image
 public import Mathlib.Order.TypeTags
@@ -99,56 +99,43 @@ instance : Functor Theory where
   map f := Set.image (f <$> ·)
 
 /-- The empty theory corresponds to minimal propositional logic. -/
-abbrev MPL : Theory (Atom) := ∅
+abbrev MPL (Atom : Type u) : Theory (Atom) := ∅
 
 /-- Intuitionistic propositional logic adds the principle of explosion (ex falso quodlibet). -/
-abbrev IPL [Bot Atom] : Theory Atom :=
-  Set.range (⊥ → ·)
-
-/-- Classical logic further adds double negation elimination. -/
-abbrev CPL [Bot Atom] : Theory Atom :=
-  Set.range (fun (A : Proposition Atom) ↦ ¬¬A → A)
-
-/-- A theory is intuitionistic if it validates ex falso quodlibet. -/
-@[scoped grind]
-class IsIntuitionistic [Bot Atom] (T : Theory Atom) where
-  efq (A : Proposition Atom) : (⊥ → A) ∈ T
-
-omit [DecidableEq Atom] in
-@[scoped grind =]
-theorem isIntuitionisticIff [Bot Atom] (T : Theory Atom) : IsIntuitionistic T ↔ IPL ⊆ T := by grind
-
-/-- A theory is classical if it validates double-negation elimination. -/
-@[scoped grind]
-class IsClassical [Bot Atom] (T : Theory Atom) where
-  dne (A : Proposition Atom) : (¬¬A → A) ∈ T
+abbrev IPL (Atom : Type u) [Bot Atom] : Theory Atom := {⊥ → A | A : Proposition Atom}
 
 omit [DecidableEq Atom] in
-@[scoped grind =]
-theorem isClassicalIff [Bot Atom] (T : Theory Atom) : IsClassical T ↔ CPL ⊆ T := by grind
+lemma efq_mem_ipl [Bot Atom] (A : Proposition Atom) : (⊥ → A) ∈ IPL Atom := ⟨A, rfl⟩
 
-instance instIsIntuitionisticIPL [Bot Atom] : IsIntuitionistic (Atom := Atom) IPL where
-  efq A := Set.mem_range.mpr ⟨A, rfl⟩
-
-instance instIsClassicalCPL [Bot Atom] : IsClassical (Atom := Atom) CPL where
-  dne A := Set.mem_range.mpr ⟨A, rfl⟩
+/-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/
+@[reducible]
+def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) :=
+  (WithBot.some <$> T) ∪ IPL (WithBot Atom)
 
-omit [DecidableEq Atom] in
-@[scoped grind →]
-theorem instIsIntuitionisticExtention [Bot Atom] {T T' : Theory Atom} [IsIntuitionistic T]
-    (h : T ⊆ T') : IsIntuitionistic T' := by grind
+/-- Classical logic further adds double negation elimination. -/
+abbrev CPL (Atom : Type u) [Bot Atom] : Theory Atom := {¬¬A → A | A : Proposition Atom}
 
 omit [DecidableEq Atom] in
-@[scoped grind →]
-theorem instIsClassicalExtention [Bot Atom] {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') :
-    IsClassical T' := by grind
+lemma dne_mem_cpl [Bot Atom] (A : Proposition Atom) : (¬¬A → A) ∈ CPL Atom := ⟨A, rfl⟩
 
-/-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/
-@[reducible]
-def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) :=
-  (WithBot.some <$> T) ∪ IPL
+open InferenceSystem
 
-instance instIsIntuitionisticIntuitionisticCompletion (T : Theory Atom) :
-    IsIntuitionistic T.intuitionisticCompletion := by grind
+/-- An inference system is intuitionistic if it derives ex falso quodlibet. TODO: this should be
+generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an
+implication connective. -/
+@[scoped grind]
+class IsIntuitionistic (Atom : Type u) [Bot Atom] (S : Type*)
+    [InferenceSystem S (Proposition Atom)] where
+  /-- The principle of explosion (ex falso quolibet). -/
+  efq (A : Proposition Atom) : S⇓(⊥ → A)
+
+/-- An inference system is classical if it validates double-negation elimination. TODO: this should
+be generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an
+implication connective. -/
+@[scoped grind]
+class IsClassical (Atom : Type u) [Bot Atom] (S : Type*)
+    [InferenceSystem S (Proposition Atom)] where
+  /-- Double-negation elimination. -/
+  dne (A : Proposition Atom) : S⇓(¬¬A → A)
 
 end Cslib.Logic.PL.Theory

Cslib/Logics/Propositional/NaturalDeduction/Basic.lean

@@ -156,7 +156,7 @@ theorem Theory.equiv_iff {A B : Proposition Atom} :
     exact ⟨D, E⟩
 
 /-- Minimally equivalent propositions. -/
-abbrev Equiv : Proposition Atom → Proposition Atom → Prop := MPL.Equiv
+abbrev Equiv : Proposition Atom → Proposition Atom → Prop := (MPL Atom).Equiv
 
 @[inherit_doc]
 scoped infix:29 " ≡ " => Equiv

Cslib/Logics/Propositional/NaturalDeduction/Theory.lean

@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2025 Thomas Waring. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Waring
+-/
+module
+
+public import Cslib.Logics.Propositional.NaturalDeduction.Basic
+
+/-! # Results on propositional theories
+
+In this file we prove the expected results that `IPL Atom` is an intuitionistic theory, and
+`CPL Atom` is a classical theory. We provide derived rules for common intuitionistic and classical
+proof patterns.
+-/
+
+@[expose] public section
+
+universe u
+
+namespace Cslib.Logic.PL
+
+open Proposition Theory InferenceSystem DerivableIn Derivation IsIntuitionistic IsClassical
+
+variable {Atom : Type u} [DecidableEq Atom] [Bot Atom] {T : Theory Atom}
+
+namespace Theory
+
+instance instIsIntuitionisticIPL : IsIntuitionistic Atom (IPL Atom) where
+  efq A := ax (efq_mem_ipl A)
+
+/-- Derivation of efq in an arbitrary context. -/
+def IsIntuitionistic.efqCtx [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Proposition Atom)
+    : T⇓(Γ ⊢ ⊥ → A) := (efq A : T⇓(⊥ → A)).weak_ctx (Finset.empty_subset Γ)
+
+/-- Efq as a derived rule. -/
+def IsIntuitionistic.efqRule [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Proposition Atom)
+    (D : T⇓(Γ ⊢ ⊥)) : T⇓(Γ ⊢ A) :=
+  implE (A := ⊥) (efqCtx Γ A) D
+
+/-- Prove any proposition from contradictory hypotheses. -/
+def IsIntuitionistic.contra [IsIntuitionistic Atom T] {Γ : Ctx Atom} (A B : Proposition Atom)
+    (hΓ : A ∈ Γ) (hΓ' : (¬A) ∈ Γ) : T⇓(Γ ⊢ B) :=
+  efqRule Γ B <| implE (ass hΓ') (ass hΓ)
+
+instance instIsClassicalCPL : IsClassical Atom (CPL Atom) where
+  dne A := ax (dne_mem_cpl A)
+
+/-- Proof by contradiction as a derived rule. -/
+def IsClassical.byContra [IsClassical Atom T] {Γ : Ctx Atom} {A : Proposition Atom}
+    (D : T⇓(insert (¬ A) Γ ⊢ ⊥)) : T⇓(Γ ⊢ A) :=
+  implE (A := ¬¬A) ((dne A : T⇓(¬¬A → A)) |>.weak_ctx <| Finset.empty_subset ..) D.implI
+
+instance instIsIntuitionisticOfIsClassical [IsClassical Atom T] : IsIntuitionistic Atom T where
+  efq A := implI _ <| byContra <| ass (by grind)
+
+/-- Law of excluded middle in a classical theory. -/
+def IsClassical.lem [IsClassical Atom T] (A : Proposition Atom) : T⇓(A ∨ ¬ A) := by
+  apply byContra
+  apply implE (ass <| Finset.mem_insert_self ..)
+  apply orI₂; apply implI
+  apply implE (A := A ∨ ¬ A) (ass <| by grind)
+  exact orI₁ <| ass <| Finset.mem_insert_self ..
+
+/-- Pierce's law in a classical theory. -/
+def IsClassical.pierce [IsClassical Atom T] (A B : Proposition Atom) : T⇓(((A → B) → A) → A) := by
+  apply implI; apply byContra
+  apply implE (ass <| Finset.mem_insert_self ..)
+  apply implE (A := A → B) (ass <| by grind); apply implI
+  apply contra A B <;> grind
+
+/-- The axiom system consisting of instances of LEM. -/
+def LEM (Atom : Type u) [Bot Atom] : Theory Atom := {A ∨ ¬ A | A : Proposition Atom}
+
+omit [DecidableEq Atom] in
+lemma lem_mem_lem (A : Proposition Atom) : (A ∨ ¬ A) ∈ LEM Atom := ⟨A, rfl⟩
+
+/-- The axiom system consisting of instances of Pierce's law. -/
+def Pierce (Atom : Type u) : Theory Atom :=
+  {((A → B) → A) → A | (A : Proposition Atom) (B : Proposition Atom)}
+
+omit [DecidableEq Atom] [Bot Atom] in
+lemma pierce_mem_pierce (A B : Proposition Atom) : (((A → B) → A) → A) ∈ Pierce Atom := ⟨A, B, rfl⟩
+
+instance instIsClassicalLEM : IsClassical Atom (LEM Atom ∪ IPL Atom : Theory Atom) where
+  dne A := by
+    apply implI
+    apply orE (ax <| Set.mem_union_left _ <| lem_mem_lem A)
+    · exact ass (Finset.mem_insert_self A _)
+    · apply implE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A))
+      apply implE (A := ¬ A) <;> exact ass (by grind)
+
+instance instIsClassicalPierce : IsClassical Atom (Pierce Atom ∪ IPL Atom : Theory Atom) where
+  dne A := by
+    apply implI
+    apply implE (A := (A → ⊥) → A) (ax <| Set.mem_union_left _ <| pierce_mem_pierce A ⊥)
+    apply implI
+    apply implE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A))
+    apply implE (A := ¬ A) <;> exact ass (by grind)
+
+end Cslib.Logic.PL.Theory