feat(Logics/Modal): refactor formula primitives to {atom, bot, imp, box}

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: benbrastmckie

Cslib/Foundations/Logic/Connectives.lean

@@ -8,18 +8,18 @@ module
 
 import Cslib.Init
 
-/-! # Connective Typeclasses for Propositional Logic
+/-! # Connective Typeclasses for Composable Logics
 
-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.
+This module defines a typeclass hierarchy for logical connectives, shared across propositional
+and modal logic levels. Each formula type registers itself as an instance of the appropriate
+connective class, enabling polymorphic axiom definitions and notation.
 
 ## Design
 
-The hierarchy adopts five constructors `{atom, bot, imp, and, or}`,
+The hierarchy adopts a hybrid design,
 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`)
+- **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr`, `HasBox`
+- **Bundled classes**: `PropositionalConnectives`, `ModalConnectives`
 
 Conjunction (`HasAnd`) and disjunction (`HasOr`) are treated as independent primitives rather
 than Łukasiewicz-derived connectives. The classical encodings `φ ∧ ψ := ¬(φ → ¬ψ)` and
@@ -51,6 +51,18 @@ class HasImp (F : Type*) where
   /-- The implication connective. -/
   imp : F → F → F
 
+/-- A type has a necessity/box modality.
+
+Box represents universal quantification over accessible worlds (`∀ w', r w w' → φ`),
+distributes over implication (axiom K), and is the subject of the necessitation rule.
+In classical systems,
+diamond (possibility) is derived as `¬□¬φ`. Non-classical modal logics (intuitionistic,
+minimal) require a separate `HasDia` typeclass, since `□` and `◇` become independent
+operators in those settings. -/
+class HasBox (F : Type*) where
+  /-- The necessity/box modality. -/
+  box : F → F
+
 /-- A type has a conjunction connective. -/
 class HasAnd (F : Type*) where
   /-- The conjunction connective. -/
@@ -68,4 +80,12 @@ When all four connectives are needed, use
 `[PropositionalConnectives F] [HasAnd F] [HasOr F]`. -/
 class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F
 
+/-- Modal connectives: propositional connectives plus box (necessity).
+
+Diamond (possibility) is derivable from box and propositional connectives via
+classical negation (`◇φ := ¬□¬φ`) and need not appear in the typeclass. Non-classical modal
+logics (intuitionistic, minimal) require extending this class with a primitive `HasDia` once
+those formula types are formalized. -/
+class ModalConnectives (F : Type*) extends PropositionalConnectives F, HasBox F
+
 end Cslib.Logic