feat(Logics/Propositional): five-primitive formula type with primitive bot

Cslib.lean

@@ -69,6 +69,7 @@ public import Cslib.Foundations.Data.RelatesInSteps
 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.Relation.Attr

Cslib/Foundations/Logic/Connectives.lean

@@ -0,0 +1,71 @@
+/-
+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 Propositional Logic
+
+This module defines a typeclass hierarchy for propositional logical connectives. Each formula
+type registers itself as an instance of the appropriate connective class, enabling polymorphic
+axiom definitions and notation that work uniformly across different formula types.
+
+## Design
+
+The hierarchy adopts five constructors `{atom, bot, imp, and, or}`,
+following the operator-typeclass direction of fmontesi's PR #607 (one class per operator):
+- **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr`
+- **Bundled class**: `PropositionalConnectives` (extends `HasBot` and `HasImp`)
+
+Conjunction (`HasAnd`) and disjunction (`HasOr`) are treated as independent primitives rather
+than Łukasiewicz-derived connectives. The classical encodings `φ ∧ ψ := ¬(φ → ¬ψ)` and
+`φ ∨ ψ := ¬φ → ψ` are only propositionally equivalent to `∧` and `∨` in classical logic
+([Avigad2022]); they fail in intuitionistic and minimal logic. Making `and`
+and `or` primitive via `HasAnd`/`HasOr` supports all three logic strengths with a single
+typeclass hierarchy.
+
+Negation and verum stay derived: each concrete formula type defines `neg φ := φ → ⊥` and
+`top := ⊥ → ⊥` as `abbrev`s, which are valid in minimal, intuitionistic, and classical logic
+alike, so no typeclass machinery is needed for them.
+
+## References
+
+* [J. Avigad, *Mathematical Logic and Computation*][Avigad2022]
+-/
+
+@[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 conjunction connective. -/
+class HasAnd (F : Type*) where
+  /-- The conjunction connective. -/
+  and : F → F → F
+
+/-- A type has a disjunction connective. -/
+class HasOr (F : Type*) where
+  /-- The disjunction connective. -/
+  or : F → F → F
+
+/-- Propositional connectives: falsum and implication.
+
+`HasAnd` and `HasOr` are defined as standalone atomic classes in this module.
+When all four connectives are needed, use
+`[PropositionalConnectives F] [HasAnd F] [HasOr F]`. -/
+class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F
+
+end Cslib.Logic

Cslib/Logics/Propositional/Defs.lean

@@ -1,37 +1,47 @@
 /-
-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
 
+import Cslib.Init
+public import Cslib.Foundations.Logic.Connectives
 public import Cslib.Foundations.Logic.InferenceSystem
 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), `imp` (implication), `and` (conjunction), and `or` (disjunction). Negation
+  (`neg`), verum (`top`), and biconditional (`iff`) are derived connectives (`abbrev`s). This
+  follows the natural deduction tradition ([Avigad2022]) in which `neg A` abbreviates `A → ⊥`
+  rather than being taken as primitive.
 - `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
-elimination.
+- `IsIntuitionistic` : an inference system is intuitionistic if it derives the principle of
+  explosion.
+- `IsClassical` : an inference system is classical if it further derives double negation
+  elimination.
 - `Proposition.subst` : replace `atom x` in a `A : Proposition Atom` with `f x`, for a function
   `f : Atom → Proposition Atom'`. This induces a monad structure on `Proposition`, with
   `pure := Proposition.atom`. `Theory` is a functor, by mapping each proposition `A ∈ T` to
   `f <$> A`.
 - `Theory.intuitionisticCompletion` : the freely generated intuitionistic theory extending a given
-theory.
+  theory.
 
 ## Notation
 
 We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum,
 conjunction, disjunction, implication and negation.
+
+## References
+
+* [J. Avigad, *Mathematical Logic and Computation*][Avigad2022]
 -/
 
 @[expose] public section
@@ -42,44 +52,61 @@ variable {Atom : Type u} [DecidableEq Atom]
 
 namespace Cslib.Logic.PL
 
-/-- Propositions. -/
+/-- Propositions. Primitives are atoms, falsum, implication, conjunction, and disjunction. -/
 inductive Proposition (Atom : Type u) : Type u where
   /-- Propositional atoms -/
   | atom (x : Atom)
+  /-- Falsum / bottom -/
+  | bot
+  /-- Implication -/
+  | imp (a b : Proposition Atom)
   /-- Conjunction -/
   | and (a b : Proposition Atom)
   /-- Disjunction -/
   | or (a b : Proposition Atom)
-  /-- Implication -/
-  | impl (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)
+/-- 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 instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top⟩
-
-example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl
+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 infix:20 " ↔ " => Proposition.iff
 @[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg
 
+/-- Register `Proposition` as an instance of `PropositionalConnectives`. -/
+instance : PropositionalConnectives (Proposition Atom) where
+  bot := .bot
+  imp := .imp
+
+/-- Register `HasAnd` instance for `Proposition`. -/
+instance : HasAnd (Proposition Atom) where
+  and := .and
+
+/-- Register `HasOr` instance for `Proposition`. -/
+instance : HasOr (Proposition Atom) where
+  or := .or
+
 /-- 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)
+  | and A B => .and (A.subst f) (B.subst f)
+  | or A B => .or (A.subst f) (B.subst f)
 
 -- This is probably a lawful monad, but that doesn't seem to be important.
 instance : Monad Proposition where
@@ -99,41 +126,45 @@ instance : Functor Theory where
   map f := Set.image (f <$> ·)
 
 /-- The empty theory corresponds to minimal propositional logic. -/
-abbrev MPL (Atom : Type u) : Theory (Atom) := ∅
+abbrev MPL : Theory (Atom) := ∅
 
 /-- Intuitionistic propositional logic adds the principle of explosion (ex falso quodlibet). -/
-abbrev IPL (Atom : Type u) [Bot Atom] : Theory Atom := {⊥ → A | A : Proposition Atom}
+abbrev IPL : Theory Atom :=
+  Set.range (Proposition.imp ⊥ ·)
 
 omit [DecidableEq Atom] in
-lemma efq_mem_ipl [Bot Atom] (A : Proposition Atom) : (⊥ → A) ∈ IPL 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 (WithBot Atom)
+lemma efq_mem_ipl (A : Proposition Atom) : (⊥ → A) ∈ IPL (Atom := Atom) := ⟨A, rfl⟩
 
 /-- Classical logic further adds double negation elimination. -/
-abbrev CPL (Atom : Type u) [Bot Atom] : Theory Atom := {¬¬A → A | A : Proposition Atom}
+abbrev CPL : Theory Atom :=
+  Set.range (fun (A : Proposition Atom) ↦ ¬¬A → A)
 
 omit [DecidableEq Atom] in
-lemma dne_mem_cpl [Bot Atom] (A : Proposition Atom) : (¬¬A → A) ∈ CPL Atom := ⟨A, rfl⟩
+lemma dne_mem_cpl (A : Proposition Atom) : (¬¬A → A) ∈ CPL (Atom := Atom) := ⟨A, rfl⟩
+
+/-- Extend a theory `T` to an intuitionistic theory over a larger atom type by adding the principle
+of explosion. The atom type is extended with `WithBot` to ensure the result is over a strictly
+larger language. -/
+@[reducible]
+def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) :=
+  (WithBot.some <$> T) ∪ IPL
 
 open InferenceSystem
 
 /-- 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*)
+class IsIntuitionistic (Atom : Type u) (S : Type*)
     [InferenceSystem S (Proposition Atom)] where
-  /-- The principle of explosion (ex falso quolibet). -/
+  /-- The principle of explosion (ex falso quodlibet). -/
   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*)
+class IsClassical (Atom : Type u) (S : Type*)
     [InferenceSystem S (Proposition Atom)] where
   /-- Double-negation elimination. -/
   dne (A : Proposition Atom) : S⇓(¬¬A → A)