feat(Logics/Propositional): further API for manipulating theories in natural deduction

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,61 @@ 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⟩
+/-- 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)
 
-instance instIsClassicalCPL [Bot Atom] : IsClassical (Atom := Atom) CPL where
-  dne A := Set.mem_range.mpr ⟨A, rfl⟩
+/-- 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 instIsIntuitionisticExtention [Bot Atom] {T T' : Theory Atom} [IsIntuitionistic T]
-    (h : T ⊆ T') : IsIntuitionistic T' := by grind
+lemma dne_mem_cpl [Bot Atom] (A : Proposition Atom) : (¬¬A → A) ∈ CPL Atom := ⟨A, rfl⟩
 
-omit [DecidableEq Atom] in
-@[scoped grind →]
-theorem instIsClassicalExtention [Bot Atom] {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') :
-    IsClassical T' := by grind
+open InferenceSystem
 
-/-- 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
+/-- 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)
+
+-- should this be proof-relevant?
+/-- A theory is inconsistent if it derives every proposition. -/
+@[mk_iff]
+class IsInconsistent (Atom : Type u) (S : Type*) [InferenceSystem S (Proposition Atom)] where
+  /-- Every proposition is derivable. -/
+  forall_derivableIn (A : Proposition Atom) : DerivableIn S A
+
+/-- A theory is consistent is there is a non-derivable proposition. -/
+@[mk_iff]
+class IsConsistent (Atom : Type u) (S : Type*) [InferenceSystem S (Proposition Atom)] where
+  /-- Some proposition is not derivable. -/
+  exists_not_derivableIn : ∃ A : Proposition Atom, ¬ DerivableIn S A
 
-instance instIsIntuitionisticIntuitionisticCompletion (T : Theory Atom) :
-    IsIntuitionistic T.intuitionisticCompletion := by grind
+omit [DecidableEq Atom] in
+lemma isInconsistent_iff_not_isConsistent {S : Type*} [InferenceSystem S (Proposition Atom)] :
+    IsInconsistent Atom S ↔ ¬ IsConsistent Atom S := by
+  simp [isInconsistent_iff, isConsistent_iff]
 
 end Cslib.Logic.PL.Theory

Cslib/Logics/Propositional/NaturalDeduction/Basic.lean

@@ -11,8 +11,6 @@ public import Mathlib.Data.Finset.Insert
 public import Mathlib.Data.Finset.SDiff
 public import Mathlib.Data.Finset.Image
 
-@[expose] public section
-
 /-! # Natural deduction for propositional logic
 
 We define, for minimal logic, deduction trees (a `Type`) and derivability (a `Prop`) relative to a
@@ -61,6 +59,8 @@ in §2.2 of Sorensen & Urzyczyn's *Lectures on the Curry-Howard Isomorphism*. (S
 references welcome!)
 -/
 
+@[expose] public section
+
 universe u
 
 namespace Cslib.Logic.PL
@@ -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