refactor: Proposition type to bot/imp primitives

Cslib.lean

@@ -69,6 +69,7 @@ public import Cslib.Foundations.Data.Relation
 public import Cslib.Foundations.Data.Set.Saturation
 public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
+public import Cslib.Foundations.Logic.Connectives
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Cslib.Foundations.Logic.LogicalEquivalence
 public import Cslib.Foundations.Semantics.FLTS.Basic

Cslib/Foundations/Logic/Connectives.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Benjamin Brast-McKie
+-/
+
+module
+
+import Cslib.Init
+
+/-! # Connective Typeclasses for Composable Logics
+
+This module defines a typeclass hierarchy for logical connectives, shared across the four
+logic levels (Propositional, Modal, Temporal, Bimodal). Each formula type registers itself
+as an instance of the appropriate connective class, enabling polymorphic axiom definitions
+and notation.
+
+## Design
+
+The hierarchy follows the Foundation pattern (FormalizedFormalLogic/Foundation):
+- **Atomic classes**: `HasBot`, `HasImp`, `HasBox`, `HasUntil`, `HasSince`
+- **Bundled classes**: `PropositionalConnectives`, `ModalConnectives`,
+  `TemporalConnectives`, `BimodalConnectives`
+- **Derived connectives**: `ImpBotDerived` for `neg`, `top`, `or`, `and` from `bot`/`imp`
+
+Each concrete formula type duplicates its constructors (Lean 4 cannot extend inductives)
+and registers as an instance of the appropriate bundled class.
+
+Falsum and implication are taken as the only propositional primitives because `{imp, bot}`
+is functionally complete for classical logic: every other connective is definable, so it can
+be a derived `abbrev` rather than a constructor. This keeps the inductive formula types as
+small as possible -- minimising the case count in every recursion and induction over formulas
+-- and lets the derived connectives unfold to `imp`/`bot` definitionally, so reasoning about
+`¬`, `∧`, `∨`, and `↔` needs no separate axioms or bridging lemmas.
+
+## References
+
+* [A. Church, *Introduction to Mathematical Logic*][Church1956]
+* [A. Heyting, *Die formalen Regeln der intuitionistischen Logik*][Heyting1930]
+* [G. Gentzen, *Untersuchungen über das logische Schließen*][Gentzen1935]
+* [A. Chagrov, M. Zakharyaschev, *Modal Logic*][ChagrovZakharyaschev1997], Chapter 1
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- A type has a falsum (bottom) connective. -/
+class HasBot (F : Type*) where
+  /-- The falsum/bottom connective. -/
+  bot : F
+
+/-- A type has an implication connective. -/
+class HasImp (F : Type*) where
+  /-- The implication connective. -/
+  imp : F → F → F
+
+/-- A type has a necessity (box) modality. -/
+class HasBox (F : Type*) where
+  /-- The necessity/box modality. -/
+  box : F → F
+
+/-- A type has an until temporal operator. -/
+class HasUntil (F : Type*) where
+  /-- The until temporal operator. -/
+  untl : F → F → F
+
+/-- A type has a since temporal operator. -/
+class HasSince (F : Type*) where
+  /-- The since temporal operator. -/
+  snce : F → F → F
+
+/-- Propositional connectives: falsum and implication. -/
+class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F
+
+/-- Modal connectives: propositional connectives plus necessity. -/
+class ModalConnectives (F : Type*) extends PropositionalConnectives F, HasBox F
+
+/-- Temporal connectives: propositional connectives plus until and since. -/
+class TemporalConnectives (F : Type*) extends PropositionalConnectives F, HasUntil F, HasSince F
+
+/-- Bimodal connectives: modal connectives plus until and since.
+    Note: we extend `ModalConnectives` and add `HasUntil`/`HasSince` directly
+    rather than extending `TemporalConnectives`, to avoid a typeclass diamond. -/
+class BimodalConnectives (F : Type*) extends ModalConnectives F, HasUntil F, HasSince F
+
+/-- Derived connectives definable from `bot` and `imp` alone.
+
+Provides `neg`, `top`, `or`, `and` as abbreviations: negation is implication to falsum
+(`neg φ := imp φ bot`), verum is `imp bot bot`, disjunction is `imp (neg φ) ψ`, and conjunction
+is `neg (imp φ (neg ψ))`. These are forced once `{imp, bot}` is fixed as the primitive basis --
+each is the truth-functional definition of the connective in terms of implication and falsum --
+so the choice carries no information beyond the basis itself.
+
+**Status**: This class is intentionally uninstantiated. Each concrete formula type
+(PL.Proposition, Modal.Proposition, Temporal.Formula, Bimodal.Formula) defines its
+own `abbrev` connectives directly on the inductive constructors, which are
+definitionally equal to these defaults. Registering typeclass instances would add
+resolution overhead at every use site with no benefit, since the `abbrev` definitions
+already compute. The class is retained as a specification artifact and for potential
+future use in polymorphic proof-system abstractions that need to quantify over derived
+connectives generically. -/
+class ImpBotDerived (F : Type*) [HasBot F] [HasImp F] where
+  /-- Negation: `neg φ := imp φ bot` -/
+  neg : F → F := fun φ => HasImp.imp φ HasBot.bot
+  /-- Top/verum: `top := imp bot bot` -/
+  top : F := HasImp.imp HasBot.bot HasBot.bot
+  /-- Disjunction: `or φ ψ := imp (neg φ) ψ` where `neg φ := imp φ bot` -/
+  or : F → F → F := fun φ ψ => HasImp.imp (HasImp.imp φ HasBot.bot) ψ
+  /-- Conjunction: `and φ ψ := neg (imp φ (neg ψ))` -/
+  and : F → F → F := fun φ ψ =>
+    HasImp.imp (HasImp.imp φ (HasImp.imp ψ HasBot.bot)) HasBot.bot
+
+end Cslib.Logic

Cslib/Foundations/Logic/InferenceSystem.lean

@@ -6,9 +6,9 @@ Authors: Fabrizio Montesi
 
 module
 
-public import Cslib.Init
+import Cslib.Init
 
-/-! -/
+/-! # Inference System Typeclass -/
 
 @[expose] public section
 

Cslib/Logics/Propositional/Defs.lean

@@ -1,22 +1,25 @@
 /-
-Copyright (c) 2025 Thomas Waring. All rights reserved.
+Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Thomas Waring
+Authors: Thomas Waring, Benjamin Brast-McKie
 -/
 
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Logic.Connectives
 public import Mathlib.Data.FunLike.Basic
-public import Mathlib.Data.Set.Image
+public import Mathlib.Data.Set.Basic
 public import Mathlib.Order.TypeTags
 
 /-! # Propositions and theories
 
 ## Main definitions
 
-- `Proposition` : the type of propositions over a given type of atom. This type has a `Bot`
-instance whenever `Atom` does, and a `Top` whenever `Atom` is inhabited.
+- `Proposition` : the type of propositions over a given type of atom. Primitives are `atom`,
+  `bot` (falsum), and `imp` (implication); since `{imp, bot}` is functionally complete for
+  classical logic, conjunction, disjunction, negation, and verum are derived connectives
+  (`abbrev`s) rather than constructors, keeping the inductive minimal.
 - `Theory` : set of `Proposition`.
 - `IsIntuitionistic` : a theory is intuitionistic if it contains the principle of explosion.
 - `IsClassical` : an intuitionistic theory is classical if it further contains double negation
@@ -32,6 +35,11 @@ theory.
 
 We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum,
 conjunction, disjunction, implication and negation.
+
+## References
+
+* [A. Church, *Introduction to Mathematical Logic*][Church1956]
+* [A. Chagrov, M. Zakharyaschev, *Modal Logic*][ChagrovZakharyaschev1997], Chapter 1
 -/
 
 @[expose] public section
@@ -42,44 +50,54 @@ variable {Atom : Type u} [DecidableEq Atom]
 
 namespace Cslib.Logic.PL
 
-/-- Propositions. -/
+/-- Propositions. Primitives are atoms, falsum, and implication. -/
 inductive Proposition (Atom : Type u) : Type u where
   /-- Propositional atoms -/
   | atom (x : Atom)
-  /-- Conjunction -/
-  | and (a b : Proposition Atom)
-  /-- Disjunction -/
-  | or (a b : Proposition Atom)
+  /-- Falsum / bottom -/
+  | bot
   /-- Implication -/
-  | impl (a b : Proposition Atom)
+  | imp (a b : Proposition Atom)
 deriving DecidableEq, BEq
 
-instance instBotProposition [Bot Atom] : Bot (Proposition Atom) := ⟨.atom ⊥⟩
-instance instInhabitedOfBot [Bot Atom] : Inhabited Atom := ⟨⊥⟩
+/-- Negation as a derived connective: ¬A := A → ⊥ -/
+abbrev Proposition.neg : Proposition Atom → Proposition Atom := (Proposition.imp · .bot)
 
-/-- We view negation as a defined connective ~A := A → ⊥ -/
-abbrev Proposition.neg [Bot Atom] : Proposition Atom → Proposition Atom := (Proposition.impl · ⊥)
+/-- Verum / top as a derived connective: ⊤ := ⊥ → ⊥ -/
+abbrev Proposition.top : Proposition Atom := .imp .bot .bot
 
-/-- A fixed choice of a derivable proposition (of course any two are equivalent). -/
-abbrev Proposition.top [Inhabited Atom] : Proposition Atom := impl (.atom default) (.atom default)
+/-- Disjunction as a derived connective: A ∨ B := ¬A → B -/
+abbrev Proposition.or (A B : Proposition Atom) : Proposition Atom :=
+  .imp (.imp A .bot) B
 
-instance instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top⟩
+/-- Conjunction as a derived connective: A ∧ B := ¬(A → ¬B) -/
+abbrev Proposition.and (A B : Proposition Atom) : Proposition Atom :=
+  .imp (.imp A (.imp B .bot)) .bot
 
-example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl
+/-- Biconditional as a derived connective: A ↔ B := (A → B) ∧ (B → A) -/
+abbrev Proposition.iff (A B : Proposition Atom) : Proposition Atom :=
+  (A.imp B).and (B.imp A)
+
+instance : Bot (Proposition Atom) := ⟨.bot⟩
+instance : Top (Proposition Atom) := ⟨.top⟩
 
 @[inherit_doc] scoped infix:36 " ∧ " => Proposition.and
 @[inherit_doc] scoped infix:35 " ∨ " => Proposition.or
-@[inherit_doc] scoped infix:30 " → " => Proposition.impl
+@[inherit_doc] scoped infix:30 " → " => Proposition.imp
 @[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg
 
+/-- Register `Proposition` as an instance of `PropositionalConnectives`. -/
+instance : PropositionalConnectives (Proposition Atom) where
+  bot := .bot
+  imp := .imp
+
 /-- Substitute each atom in a proposition for a proposition, possibly changing the atomic
 language. -/
 def Proposition.subst {Atom Atom' : Type u} (f : Atom → Proposition Atom') :
     Proposition Atom → Proposition Atom'
   | atom x => f x
-  | and A B => (A.subst f) ∧ (B.subst f)
-  | or A B => (A.subst f) ∨ (B.subst f)
-  | impl A B => (A.subst f) → (B.subst f)
+  | bot => .bot
+  | imp A B => .imp (A.subst f) (B.subst f)
 
 -- This is probably a lawful monad, but that doesn't seem to be important.
 instance : Monad Proposition where
@@ -102,45 +120,45 @@ instance : Functor Theory where
 abbrev MPL : Theory (Atom) := ∅
 
 /-- Intuitionistic propositional logic adds the principle of explosion (ex falso quodlibet). -/
-abbrev IPL [Bot Atom] : Theory Atom :=
-  Set.range (⊥ → ·)
+abbrev IPL : Theory Atom :=
+  Set.range (Proposition.imp ⊥ ·)
 
 /-- Classical logic further adds double negation elimination. -/
-abbrev CPL [Bot Atom] : Theory Atom :=
+abbrev CPL : 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
+class IsIntuitionistic (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
+theorem isIntuitionisticIff (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
+class IsClassical (T : Theory Atom) where
   dne (A : Proposition Atom) : (¬¬A → A) ∈ T
 
 omit [DecidableEq Atom] in
 @[scoped grind =]
-theorem isClassicalIff [Bot Atom] (T : Theory Atom) : IsClassical T ↔ CPL ⊆ T := by grind
+theorem isClassicalIff (T : Theory Atom) : IsClassical T ↔ CPL ⊆ T := by grind
 
-instance instIsIntuitionisticIPL [Bot Atom] : IsIntuitionistic (Atom := Atom) IPL where
+instance instIsIntuitionisticIPL : IsIntuitionistic (Atom := Atom) IPL where
   efq A := Set.mem_range.mpr ⟨A, rfl⟩
 
-instance instIsClassicalCPL [Bot Atom] : IsClassical (Atom := Atom) CPL where
+instance instIsClassicalCPL : IsClassical (Atom := Atom) CPL where
   dne A := Set.mem_range.mpr ⟨A, rfl⟩
 
 omit [DecidableEq Atom] in
 @[scoped grind →]
-theorem instIsIntuitionisticExtention [Bot Atom] {T T' : Theory Atom} [IsIntuitionistic T]
+theorem instIsIntuitionisticExtention {T T' : Theory Atom} [IsIntuitionistic T]
     (h : T ⊆ T') : IsIntuitionistic T' := by grind
 
 omit [DecidableEq Atom] in
 @[scoped grind →]
-theorem instIsClassicalExtention [Bot Atom] {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') :
+theorem instIsClassicalExtention {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') :
     IsClassical T' := by grind
 
 /-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/