diff --git a/Cslib.lean b/Cslib.lean
index 657d106c2..40fc03a0c 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -58,6 +58,7 @@ public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
 public import Cslib.Foundations.Data.FinFun.Update
 public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Data.ListHelpers
 public import Cslib.Foundations.Data.Nat.Segment
 public import Cslib.Foundations.Data.OmegaSequence.Defs
 public import Cslib.Foundations.Data.OmegaSequence.Flatten
@@ -69,8 +70,22 @@ 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.Axioms
+public import Cslib.Foundations.Logic.Connectives
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Cslib.Foundations.Logic.LogicalEquivalence
+public import Cslib.Foundations.Logic.Metalogic.Consistency
+public import Cslib.Foundations.Logic.Metalogic.DeductionHelpers
+public import Cslib.Foundations.Logic.ProofSystem
+public import Cslib.Foundations.Logic.Theorems
+public import Cslib.Foundations.Logic.Theorems.BigConj
+public import Cslib.Foundations.Logic.Theorems.Combinators
+public import Cslib.Foundations.Logic.Theorems.Modal.Basic
+public import Cslib.Foundations.Logic.Theorems.Modal.S5
+public import Cslib.Foundations.Logic.Theorems.Propositional.Connectives
+public import Cslib.Foundations.Logic.Theorems.Propositional.Core
+public import Cslib.Foundations.Logic.Theorems.Temporal.FrameConditions
+public import Cslib.Foundations.Logic.Theorems.Temporal.TemporalDerived
 public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
 public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
@@ -140,7 +155,13 @@ public import Cslib.Logics.Modal.Basic
 public import Cslib.Logics.Modal.Cube
 public import Cslib.Logics.Modal.Denotation
 public import Cslib.Logics.Propositional.Defs
+public import Cslib.Logics.Propositional.Metalogic.DeductionTheorem
+public import Cslib.Logics.Propositional.Metalogic.MCS
 public import Cslib.Logics.Propositional.NaturalDeduction.Basic
+public import Cslib.Logics.Propositional.NaturalDeduction.FromHilbert
+public import Cslib.Logics.Propositional.ProofSystem.Axioms
+public import Cslib.Logics.Propositional.ProofSystem.Derivation
+public import Cslib.Logics.Propositional.ProofSystem.Instances
 public import Cslib.MachineLearning.PACLearning.Defs
 public import Cslib.MachineLearning.PACLearning.VCDimension
 public import Cslib.MachineLearning.PACLearning.VersionSpace
diff --git a/Cslib/Foundations/Data/ListHelpers.lean b/Cslib/Foundations/Data/ListHelpers.lean
new file mode 100644
index 000000000..513e24ae4
--- /dev/null
+++ b/Cslib/Foundations/Data/ListHelpers.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
+public import Cslib.Init
+
+/-! # Shared List Helper Utilities
+
+Shared `removeAll` definition and supporting lemmas used by all DeductionTheorem
+files (Propositional, Modal, Temporal, Bimodal). Extracted to avoid duplication.
+
+## Main Definitions
+
+- `removeAll`: Remove all occurrences of an element from a list
+- `removeAll_subset_of_subset`: If `A in Gamma'` and `Gamma' subs A :: Delta`,
+  then `removeAll Gamma' A subs Delta`
+- `mem_removeAll_of_mem_of_ne`: Membership in removeAll from membership and inequality
+- `removeAll_subset_removeAll`: removeAll preserves subset relationships
+
+## Aliases
+
+- `removeAll_sub_of_sub`: Alias for `removeAll_subset_of_subset` using `List.Subset`
+- `removeAll_sub_removeAll`: Alias for `removeAll_subset_removeAll` using `List.Subset`
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Helpers
+
+/-- Remove all occurrences of `a` from a list. -/
+def removeAll [DecidableEq α] (l : List α) (a : α) : List α :=
+  l.filter (· ≠ a)
+
+theorem removeAll_subset_of_subset [DecidableEq α] {A : α} {Γ' Δ : List α}
+    (h_sub : ∀ x ∈ Γ', x ∈ A :: Δ) (h_mem : A ∈ Γ') :
+    ∀ x ∈ removeAll Γ' A, x ∈ Δ := by
+  intro x hx
+  simp [removeAll, List.mem_filter] at hx
+  obtain ⟨hx_in, hx_ne⟩ := hx
+  have := h_sub x hx_in
+  simp [List.mem_cons] at this
+  rcases this with rfl | h
+  · exact absurd rfl hx_ne
+  · exact h
+
+theorem mem_removeAll_of_mem_of_ne [DecidableEq α] {a x : α} {l : List α}
+    (h_mem : x ∈ l) (h_ne : x ≠ a) : x ∈ removeAll l a := by
+  simp [removeAll, List.mem_filter]
+  exact ⟨h_mem, h_ne⟩
+
+theorem removeAll_subset_removeAll [DecidableEq α] {a : α} {l₁ l₂ : List α}
+    (h : ∀ x ∈ l₁, x ∈ l₂) : ∀ x ∈ removeAll l₁ a, x ∈ removeAll l₂ a := by
+  intro x hx
+  simp [removeAll, List.mem_filter] at hx ⊢
+  exact ⟨h x hx.1, hx.2⟩
+
+/-- Alias using `List.Subset` notation for `removeAll_subset_of_subset`. -/
+theorem removeAll_sub_of_sub [DecidableEq α] {A : α} {Γ' Δ : List α}
+    (h_sub : Γ' ⊆ A :: Δ) (h_mem : A ∈ Γ') :
+    removeAll Γ' A ⊆ Δ :=
+  removeAll_subset_of_subset h_sub h_mem
+
+/-- Alias using `List.Subset` notation for `removeAll_subset_removeAll`. -/
+theorem removeAll_sub_removeAll [DecidableEq α] {a : α} {l₁ l₂ : List α}
+    (h : l₁ ⊆ l₂) : removeAll l₁ a ⊆ removeAll l₂ a :=
+  removeAll_subset_removeAll h
+
+end Cslib.Logic.Helpers
diff --git a/Cslib/Foundations/Logic/Axioms.lean b/Cslib/Foundations/Logic/Axioms.lean
new file mode 100644
index 000000000..b404b8691
--- /dev/null
+++ b/Cslib/Foundations/Logic/Axioms.lean
@@ -0,0 +1,298 @@
+/-
+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
+public import Cslib.Foundations.Logic.Connectives
+
+/-! # Polymorphic Axiom Definitions
+
+This module defines axiom formulas as polymorphic `abbrev`s parameterized over the connective
+typeclasses. Each axiom is defined once and can be instantiated at any formula type with the
+appropriate connectives.
+
+## Organization
+
+- **Propositional axioms**: `ImplyK`, `ImplyS`, `EFQ`, `Peirce`
+  (require `HasBot`, `HasImp`)
+- **Modal axioms**: `AxiomK`, `AxiomT`, `Axiom4`, `AxiomB`, `Axiom5`, `AxiomD`
+  (require additionally `HasBox`)
+- **Temporal axioms**: `SerialFuture`, `ConnectFuture`, etc.
+  (require `HasUntil`, `HasSince`)
+- **Interaction axiom**: `ModalFuture`
+  (requires both `HasBox` and `HasUntil`)
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Axioms
+
+variable {F : Type*}
+
+/-! ### Shared Abbreviations -/
+
+section Abbreviations
+variable [HasBot F] [HasImp F]
+
+/-- Top formula: ⊥ → ⊥ -/
+abbrev top' : F := HasImp.imp (HasBot.bot : F) HasBot.bot
+
+/-- Negation: φ → ⊥ -/
+abbrev neg' (x : F) : F := HasImp.imp x HasBot.bot
+
+/-- Lukasiewicz conjunction: ¬(φ → ¬ψ) -/
+abbrev conj' (a b : F) : F :=
+  HasImp.imp (HasImp.imp a (neg' b)) HasBot.bot
+
+/-- Lukasiewicz disjunction: ¬φ → ψ -/
+abbrev disj' (a b : F) : F :=
+  HasImp.imp (neg' a) b
+
+end Abbreviations
+
+/-! ### Propositional Axioms -/
+
+section Propositional
+variable [HasBot F] [HasImp F]
+
+/-- K axiom for implication: φ → (ψ → φ) -/
+protected abbrev ImplyK (φ ψ : F) : F :=
+  HasImp.imp φ (HasImp.imp ψ φ)
+
+/-- S axiom for implication: (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)) -/
+protected abbrev ImplyS (φ ψ χ : F) : F :=
+  HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ))
+    (HasImp.imp (HasImp.imp φ ψ) (HasImp.imp φ χ))
+
+/-- Ex falso quodlibet: ⊥ → φ -/
+protected abbrev EFQ (φ : F) : F :=
+  HasImp.imp HasBot.bot φ
+
+/-- Peirce's law (classical): ((φ → ψ) → φ) → φ -/
+protected abbrev Peirce (φ ψ : F) : F :=
+  HasImp.imp (HasImp.imp (HasImp.imp φ ψ) φ) φ
+
+/-- Double negation elimination: ¬¬φ → φ
+    where ¬φ = φ → ⊥ -/
+protected abbrev DNE (φ : F) : F :=
+  HasImp.imp (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot) φ
+
+end Propositional
+
+/-! ### Modal Axioms -/
+
+section Modal
+variable [HasBot F] [HasImp F] [HasBox F]
+
+/-- Distribution axiom K: □(φ → ψ) → (□φ → □ψ) -/
+protected abbrev AxiomK (φ ψ : F) : F :=
+  HasImp.imp (HasBox.box (HasImp.imp φ ψ))
+    (HasImp.imp (HasBox.box φ) (HasBox.box ψ))
+
+/-- Reflexivity axiom T: □φ → φ -/
+protected abbrev AxiomT (φ : F) : F :=
+  HasImp.imp (HasBox.box φ) φ
+
+/-- Transitivity axiom 4: □φ → □□φ -/
+protected abbrev Axiom4 (φ : F) : F :=
+  HasImp.imp (HasBox.box φ) (HasBox.box (HasBox.box φ))
+
+/-- Symmetry axiom B: φ → □◇φ
+    where ◇φ = ¬□¬φ = (□(φ → ⊥)) → ⊥ -/
+protected abbrev AxiomB (φ : F) : F :=
+  HasImp.imp φ (HasBox.box
+    (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot))
+
+/-- Euclidean axiom 5: ◇φ → □◇φ
+    where ◇φ = (□(φ → ⊥)) → ⊥ -/
+protected abbrev Axiom5 (φ : F) : F :=
+  HasImp.imp
+    (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+    (HasBox.box (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot))
+
+/-- Seriality axiom D: □φ → ◇φ
+    where ◇φ = (□(φ → ⊥)) → ⊥ -/
+protected abbrev AxiomD (φ : F) : F :=
+  HasImp.imp (HasBox.box φ)
+    (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+
+end Modal
+
+/-! ### Temporal Axioms -/
+
+section Temporal
+variable [HasBot F] [HasImp F] [HasUntil F] [HasSince F]
+
+/-- Serial future (BX1): ⊤ → F ⊤
+    where ⊤ = ⊥ → ⊥, F φ = ⊤ U φ -/
+protected abbrev SerialFuture : F :=
+  HasImp.imp top' (HasUntil.untl top' top')
+
+/-- Serial past (BX1'): ⊤ → P ⊤
+    where P φ = ⊤ S φ -/
+protected abbrev SerialPast : F :=
+  HasImp.imp top' (HasSince.snce top' top')
+
+/-- Guard monotonicity of Until under G (BX2G):
+    G(φ → ψ) → (χ U φ → χ U ψ)
+    where G(α) = ¬(⊤ U ¬α) -/
+protected abbrev LeftMonoUntilG (φ ψ χ : F) : F :=
+  let G_imp := HasImp.imp (HasUntil.untl (neg' (HasImp.imp φ ψ)) top') HasBot.bot
+  HasImp.imp G_imp
+    (HasImp.imp (HasUntil.untl χ φ) (HasUntil.untl χ ψ))
+
+/-- Guard monotonicity of Since under H (BX2H):
+    H(φ → ψ) → (χ S φ → χ S ψ)
+    where H(α) = ¬(⊤ S ¬α) -/
+protected abbrev LeftMonoSinceH (φ ψ χ : F) : F :=
+  let H_imp := HasImp.imp (HasSince.snce (neg' (HasImp.imp φ ψ)) top') HasBot.bot
+  HasImp.imp H_imp
+    (HasImp.imp (HasSince.snce χ φ) (HasSince.snce χ ψ))
+
+/-- Event monotonicity of Until (BX3):
+    G(φ → ψ) → (φ U χ → ψ U χ)
+    where G(α) = ¬(⊤ U ¬α) -/
+protected abbrev RightMonoUntil (φ ψ χ : F) : F :=
+  let G_imp := HasImp.imp (HasUntil.untl (neg' (HasImp.imp φ ψ)) top') HasBot.bot
+  HasImp.imp G_imp
+    (HasImp.imp (HasUntil.untl φ χ) (HasUntil.untl ψ χ))
+
+/-- Event monotonicity of Since (BX3'):
+    H(φ → ψ) → (φ S χ → ψ S χ)
+    where H(α) = ¬(⊤ S ¬α) -/
+protected abbrev RightMonoSince (φ ψ χ : F) : F :=
+  let H_imp := HasImp.imp (HasSince.snce (neg' (HasImp.imp φ ψ)) top') HasBot.bot
+  HasImp.imp H_imp
+    (HasImp.imp (HasSince.snce φ χ) (HasSince.snce ψ χ))
+
+/-- Temporal connectedness future (BX4): φ → G(P(φ))
+    where P(α) = ⊤ S α, G(α) = ¬(⊤ U ¬α) -/
+protected abbrev ConnectFuture (φ : F) : F :=
+  let P_φ := HasSince.snce φ top'
+  let G_P_φ := HasImp.imp (HasUntil.untl (neg' P_φ) top') HasBot.bot
+  HasImp.imp φ G_P_φ
+
+/-- Temporal connectedness past (BX4'): φ → H(F(φ))
+    where F(α) = ⊤ U α, H(α) = ¬(⊤ S ¬α) -/
+protected abbrev ConnectPast (φ : F) : F :=
+  let F_φ := HasUntil.untl φ top'
+  let H_F_φ := HasImp.imp (HasSince.snce (neg' F_φ) top') HasBot.bot
+  HasImp.imp φ H_F_φ
+
+/-- Until-Since enrichment (BX13):
+    p ∧ (ψ U φ) → (ψ ∧ S(p, φ)) U φ
+    where ∧ is Lukasiewicz conjunction -/
+protected abbrev EnrichmentUntil (φ ψ p : F) : F :=
+  HasImp.imp (conj' p (HasUntil.untl ψ φ))
+    (HasUntil.untl (conj' ψ (HasSince.snce p φ)) φ)
+
+/-- Since-Until enrichment (BX13'):
+    p ∧ (ψ S φ) → (ψ ∧ U(p, φ)) S φ -/
+protected abbrev EnrichmentSince (φ ψ p : F) : F :=
+  HasImp.imp (conj' p (HasSince.snce ψ φ))
+    (HasSince.snce (conj' ψ (HasUntil.untl p φ)) φ)
+
+/-- Self-accumulation of Until (BX5):
+    U(ψ, φ) → U(ψ, φ ∧ U(ψ, φ)) -/
+protected abbrev SelfAccumUntil (φ ψ : F) : F :=
+  HasImp.imp (HasUntil.untl ψ φ)
+    (HasUntil.untl ψ (conj' φ (HasUntil.untl ψ φ)))
+
+/-- Self-accumulation of Since (BX5'):
+    S(ψ, φ) → S(ψ, φ ∧ S(ψ, φ)) -/
+protected abbrev SelfAccumSince (φ ψ : F) : F :=
+  HasImp.imp (HasSince.snce ψ φ)
+    (HasSince.snce ψ (conj' φ (HasSince.snce ψ φ)))
+
+/-- Absorption of Until (BX6):
+    U(φ ∧ U(ψ, φ), φ) → U(ψ, φ) -/
+protected abbrev AbsorbUntil (φ ψ : F) : F :=
+  HasImp.imp (HasUntil.untl (conj' φ (HasUntil.untl ψ φ)) φ)
+    (HasUntil.untl ψ φ)
+
+/-- Absorption of Since (BX6'):
+    S(φ ∧ S(ψ, φ), φ) → S(ψ, φ) -/
+protected abbrev AbsorbSince (φ ψ : F) : F :=
+  HasImp.imp (HasSince.snce (conj' φ (HasSince.snce ψ φ)) φ)
+    (HasSince.snce ψ φ)
+
+/-- Linearity of Until (BX7):
+    U(ψ,φ) ∧ U(θ,χ) → U(ψ∧θ, φ∧χ) ∨ U(ψ∧χ, φ∧χ) ∨ U(φ∧θ, φ∧χ) -/
+protected abbrev LinearUntil (φ ψ χ θ : F) : F :=
+  HasImp.imp (conj' (HasUntil.untl ψ φ) (HasUntil.untl θ χ))
+    (disj' (disj' (HasUntil.untl (conj' ψ θ) (conj' φ χ))
+                  (HasUntil.untl (conj' ψ χ) (conj' φ χ)))
+           (HasUntil.untl (conj' φ θ) (conj' φ χ)))
+
+/-- Linearity of Since (BX7'):
+    S(ψ,φ) ∧ S(θ,χ) → S(ψ∧θ, φ∧χ) ∨ S(ψ∧χ, φ∧χ) ∨ S(φ∧θ, φ∧χ) -/
+protected abbrev LinearSince (φ ψ χ θ : F) : F :=
+  HasImp.imp (conj' (HasSince.snce ψ φ) (HasSince.snce θ χ))
+    (disj' (disj' (HasSince.snce (conj' ψ θ) (conj' φ χ))
+                  (HasSince.snce (conj' ψ χ) (conj' φ χ)))
+           (HasSince.snce (conj' φ θ) (conj' φ χ)))
+
+/-- Until implies eventuality (BX10):
+    U(ψ, φ) → F(ψ)
+    where F(α) = ⊤ U α -/
+protected abbrev UntilF (φ ψ : F) : F :=
+  HasImp.imp (HasUntil.untl ψ φ) (HasUntil.untl ψ top')
+
+/-- Since implies past eventuality (BX10'):
+    S(ψ, φ) → P(ψ)
+    where P(α) = α S ⊤ -/
+protected abbrev SinceP (φ ψ : F) : F :=
+  HasImp.imp (HasSince.snce ψ φ) (HasSince.snce ψ top')
+
+/-- Temporal linearity (BX11):
+    F(φ) ∧ F(ψ) → F(φ ∧ ψ) ∨ F(φ ∧ F(ψ)) ∨ F(F(φ) ∧ ψ) -/
+protected abbrev TempLinearity (φ ψ : F) : F :=
+  let F' := fun (x : F) => HasUntil.untl x top'
+  HasImp.imp (conj' (F' φ) (F' ψ))
+    (disj' (F' (conj' φ ψ))
+      (disj' (F' (conj' φ (F' ψ)))
+             (F' (conj' (F' φ) ψ))))
+
+/-- Temporal linearity past (BX11'):
+    P(φ) ∧ P(ψ) → P(φ ∧ ψ) ∨ P(φ ∧ P(ψ)) ∨ P(P(φ) ∧ ψ) -/
+protected abbrev TempLinearityPast (φ ψ : F) : F :=
+  let P' := fun (x : F) => HasSince.snce x top'
+  HasImp.imp (conj' (P' φ) (P' ψ))
+    (disj' (P' (conj' φ ψ))
+      (disj' (P' (conj' φ (P' ψ)))
+             (P' (conj' (P' φ) ψ))))
+
+/-- F-Until equivalence (BX12):
+    F(φ) → U(φ, ⊤)
+    where F(α) = ⊤ U α.
+    Note: Under the Burgess 1982 convention, this is trivially F(φ) → F(φ). -/
+protected abbrev FUntilEquiv (φ : F) : F :=
+  HasImp.imp (HasUntil.untl φ top') (HasUntil.untl φ top')
+
+/-- P-Since equivalence (BX12'):
+    P(φ) → S(φ, ⊤)
+    Note: Under the Burgess 1982 convention, this is trivially P(φ) → P(φ). -/
+protected abbrev PSinceEquiv (φ : F) : F :=
+  HasImp.imp (HasSince.snce φ top') (HasSince.snce φ top')
+
+end Temporal
+
+/-! ### Interaction Axioms -/
+
+section Interaction
+variable [HasBot F] [HasImp F] [HasBox F] [HasUntil F]
+
+/-- Modal-future interaction axiom MF: □φ → □(Gφ)
+    where G φ = ¬F(¬φ) = ¬(⊤ U ¬φ)
+    Necessary truths remain necessary in the future. -/
+protected abbrev ModalFuture (φ : F) : F :=
+  let G_φ := HasImp.imp (HasUntil.untl (neg' φ) top') HasBot.bot
+  HasImp.imp (HasBox.box φ) (HasBox.box G_φ)
+
+end Interaction
+
+end Cslib.Logic.Axioms
diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean
new file mode 100644
index 000000000..dc43451ed
--- /dev/null
+++ b/Cslib/Foundations/Logic/Connectives.lean
@@ -0,0 +1,98 @@
+/-
+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**: `LukasiewiczDerived` 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.
+-/
+
+@[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
+
+/-- Lukasiewicz-style derived connectives from `bot` and `imp`.
+
+Provides `neg`, `top`, `or`, `and` as abbreviations following the standard Lukasiewicz
+encoding: negation is implication to falsum, verum is `bot → bot`, disjunction is
+`¬φ → ψ`, and conjunction is `¬(φ → ¬ψ)`.
+
+**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 LukasiewiczDerived (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
diff --git a/Cslib/Foundations/Logic/InferenceSystem.lean b/Cslib/Foundations/Logic/InferenceSystem.lean
index 854b8deb1..3a111589f 100644
--- a/Cslib/Foundations/Logic/InferenceSystem.lean
+++ b/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
 
diff --git a/Cslib/Foundations/Logic/Metalogic/Consistency.lean b/Cslib/Foundations/Logic/Metalogic/Consistency.lean
new file mode 100644
index 000000000..247d687ed
--- /dev/null
+++ b/Cslib/Foundations/Logic/Metalogic/Consistency.lean
@@ -0,0 +1,278 @@
+/-
+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
+public import Mathlib.Order.Zorn
+public import Cslib.Foundations.Logic.Connectives
+
+/-! # Generic Maximal Consistent Set (MCS) Foundations
+
+This module provides a generic framework for maximal consistent set (MCS) theory,
+parameterized over an abstract derivation relation. The key components are:
+
+- `DerivationSystem`: A structure bundling a context-based derivability predicate with
+  weakening, assumption, and modus ponens properties.
+- `SetConsistent`, `SetMaximalConsistent`: Set-based consistency predicates.
+- `consistent_chain_union`: Chain unions preserve set-consistency (input to Zorn's lemma).
+- `set_lindenbaum`: Lindenbaum's lemma -- every consistent set extends to a maximally
+  consistent set (via Zorn's lemma).
+- `HasDeductionTheorem`: A separate hypothesis type for the deduction theorem.
+- Closure properties (`closed_under_derivation`, `implication_property`,
+  `negation_complete`) conditional on the deduction theorem.
+
+Downstream modal (task 30) and temporal (task 31) metalogic tasks instantiate
+`DerivationSystem` from their concrete `DerivationTree` types and supply deduction
+theorem proofs.
+-/
+
+@[expose] public section
+
+open Cslib.Logic
+
+namespace Cslib.Logic.Metalogic
+
+variable {F : Type*} [HasBot F] [HasImp F]
+
+/-- A derivation system abstracts over logic-specific proof systems.
+
+`F` is the formula type with bottom and implication.
+`Deriv` maps a context (list of assumptions) and a conclusion to a `Prop`.
+
+Required properties:
+- `weakening`: derivations can be extended with additional assumptions
+- `assumption`: any formula in the context is derivable from it
+- `mp`: modus ponens is admissible -/
+structure DerivationSystem (F : Type*) [HasBot F] [HasImp F] where
+  /-- Context-based derivability: `Deriv Γ φ` means `φ` is derivable from `Γ`. -/
+  Deriv : List F → F → Prop
+  /-- Weakening: if `Γ ⊢ φ` and `Γ ⊆ Δ`, then `Δ ⊢ φ`. -/
+  weakening : ∀ {Γ Δ : List F} {φ : F}, Deriv Γ φ → (∀ x ∈ Γ, x ∈ Δ) → Deriv Δ φ
+  /-- Assumption: if `φ ∈ Γ`, then `Γ ⊢ φ`. -/
+  assumption : ∀ {Γ : List F} {φ : F}, φ ∈ Γ → Deriv Γ φ
+  /-- Modus ponens: from `Γ ⊢ φ → ψ` and `Γ ⊢ φ`, derive `Γ ⊢ ψ`. -/
+  mp : ∀ {Γ : List F} {φ ψ : F}, Deriv Γ (HasImp.imp φ ψ) → Deriv Γ φ → Deriv Γ ψ
+
+/-! ## Consistency Definitions -/
+
+/-- List-based consistency: `Γ` is consistent iff `Γ` does not derive `⊥`. -/
+def Consistent (D : DerivationSystem F) (Γ : List F) : Prop :=
+  ¬ D.Deriv Γ HasBot.bot
+
+/-- Set-based consistency: `S` is set-consistent iff every finite subset is consistent. -/
+def SetConsistent (D : DerivationSystem F) (S : Set F) : Prop :=
+  ∀ L : List F, (∀ φ ∈ L, φ ∈ S) → Consistent D L
+
+/-- Set-based maximal consistency: `S` is maximally consistent iff it is set-consistent
+and adding any formula not in `S` makes it inconsistent. -/
+def SetMaximalConsistent (D : DerivationSystem F) (S : Set F) : Prop :=
+  SetConsistent D S ∧ ∀ φ : F, φ ∉ S → ¬ SetConsistent D (insert φ S)
+
+/-- The collection of consistent supersets of `S`. Used as the domain for Zorn's lemma
+in Lindenbaum's lemma. -/
+def ConsistentSupersets (D : DerivationSystem F) (S : Set F) : Set (Set F) :=
+  {T | S ⊆ T ∧ SetConsistent D T}
+
+/-- In a set-consistent set, `φ` and `φ → ⊥` cannot both be members. -/
+theorem set_consistent_not_both (D : DerivationSystem F) {S : Set F}
+    (hcons : SetConsistent D S) {φ : F} (hφ : φ ∈ S)
+    (hneg : HasImp.imp φ HasBot.bot ∈ S) : False := by
+  have h := hcons [HasImp.imp φ HasBot.bot, φ] (by
+    intro ψ hψ
+    rw [List.mem_cons] at hψ
+    rcases hψ with rfl | hψ
+    · exact hneg
+    · rw [List.mem_cons] at hψ; rcases hψ with rfl | hψ
+      · exact hφ
+      · simp at hψ)
+  apply h
+  exact D.mp (D.assumption (List.mem_cons.mpr (Or.inl rfl)))
+    (D.assumption (List.mem_cons.mpr (Or.inr (List.mem_cons.mpr (Or.inl rfl)))))
+
+/-- A set-consistent set `S` is in its own collection of consistent supersets. -/
+theorem base_mem_consistent_supersets (D : DerivationSystem F) {S : Set F}
+    (hS : SetConsistent D S) : S ∈ ConsistentSupersets D S :=
+  ⟨Set.Subset.refl S, hS⟩
+
+/-! ## Chain Union Lemmas -/
+
+/-- Any finite list whose elements all belong to `⋃₀ C` (a chain union) has all its
+elements in some single chain member. Proved by induction on the list. -/
+lemma finite_list_in_chain_member {F' : Type*} {C : Set (Set F')}
+    (hchain : IsChain (· ⊆ ·) C) (hCne : C.Nonempty)
+    (L : List F') (h : ∀ φ ∈ L, φ ∈ ⋃₀ C) :
+    ∃ S ∈ C, ∀ φ ∈ L, φ ∈ S := by
+  induction L with
+  | nil =>
+    obtain ⟨S, hS⟩ := hCne
+    exact ⟨S, hS, fun _ h => by simp at h⟩
+  | cons a L ih =>
+    have ha := h a (List.mem_cons.mpr (Or.inl rfl))
+    obtain ⟨S₁, hS₁C, haS₁⟩ := Set.mem_sUnion.mp ha
+    have hL : ∀ φ ∈ L, φ ∈ ⋃₀ C := fun φ hφ => h φ (List.mem_cons.mpr (Or.inr hφ))
+    obtain ⟨S₂, hS₂C, hLS₂⟩ := ih hL
+    rcases hchain.total hS₁C hS₂C with hsub | hsub
+    · exact ⟨S₂, hS₂C, fun φ hφ => by
+        rw [List.mem_cons] at hφ
+        rcases hφ with rfl | hφ
+        · exact hsub haS₁
+        · exact hLS₂ φ hφ⟩
+    · exact ⟨S₁, hS₁C, fun φ hφ => by
+        rw [List.mem_cons] at hφ
+        rcases hφ with rfl | hφ
+        · exact haS₁
+        · exact hsub (hLS₂ φ hφ)⟩
+
+/-- The union of a nonempty chain of set-consistent sets is set-consistent.
+This is the key input to Zorn's lemma in Lindenbaum's lemma. -/
+theorem consistent_chain_union (D : DerivationSystem F)
+    {C : Set (Set F)} (hchain : IsChain (· ⊆ ·) C) (hCne : C.Nonempty)
+    (hcons : ∀ S ∈ C, SetConsistent D S) :
+    SetConsistent D (⋃₀ C) := by
+  intro L hL
+  obtain ⟨S, hSC, hLS⟩ := finite_list_in_chain_member hchain hCne L hL
+  exact hcons S hSC L hLS
+
+/-! ## Lindenbaum's Lemma -/
+
+/-- **Lindenbaum's Lemma**: Every set-consistent set can be extended to a maximally
+consistent set. The proof applies `zorn_subset_nonempty` to the collection of consistent
+supersets, using `consistent_chain_union` to verify the chain condition. -/
+theorem set_lindenbaum (D : DerivationSystem F) {S : Set F}
+    (hS : SetConsistent D S) :
+    ∃ M : Set F, S ⊆ M ∧ SetMaximalConsistent D M := by
+  -- Apply Zorn's lemma to the consistent supersets of S
+  have ⟨M, hSM, hmax⟩ := zorn_subset_nonempty (ConsistentSupersets D S)
+    (fun C hCsub hchain hCne => by
+      -- The chain union is a consistent superset
+      refine ⟨⋃₀ C, ⟨?_, ?_⟩, fun s hs => Set.subset_sUnion_of_mem hs⟩
+      -- S ⊆ ⋃₀ C: S is contained in every chain member
+      · intro x hx
+        obtain ⟨T, hT⟩ := hCne
+        exact Set.mem_sUnion.mpr ⟨T, hT, (hCsub hT).1 hx⟩
+      -- ⋃₀ C is set-consistent
+      · exact consistent_chain_union D hchain hCne (fun T hT => (hCsub hT).2))
+    S (base_mem_consistent_supersets D hS)
+  refine ⟨M, hSM, hmax.prop.2, fun φ hφ hcons => ?_⟩
+  -- If φ ∉ M, then insert φ M strictly extends M in ConsistentSupersets
+  have hins : insert φ M ∈ ConsistentSupersets D S :=
+    ⟨Set.Subset.trans hSM (Set.subset_insert φ M), hcons⟩
+  -- But M is maximal, so insert φ M = M
+  have := hmax.eq_of_ge hins (Set.subset_insert φ M)
+  -- This contradicts φ ∉ M since φ ∈ insert φ M = M
+  exact hφ (this ▸ Set.mem_insert φ M)
+
+/-! ## Deduction Theorem and Closure Properties -/
+
+/-- The deduction theorem hypothesis for a derivation system. States that if
+`φ :: Γ ⊢ ψ` then `Γ ⊢ φ → ψ`. This is NOT bundled into `DerivationSystem` because
+the base MCS theory (consistency, chain union, Lindenbaum) does not require it.
+Each logic supplies its own proof of this property. -/
+def HasDeductionTheorem (D : DerivationSystem F) : Prop :=
+  ∀ {Γ : List F} {φ ψ : F}, D.Deriv (φ :: Γ) ψ → D.Deriv Γ (HasImp.imp φ ψ)
+
+/-- Helper: given a derivation `L ⊢ ψ` where `L ⊆ insert φ S`, produce a derivation
+from `φ :: L_S ⊢ ψ` where `L_S` contains only elements of `S`. Uses classical
+decidability for list filtering. -/
+private lemma derives_from_insert_to_cons (D : DerivationSystem F)
+    {S : Set F} {φ : F} {L : List F} {ψ : F}
+    (hL : ∀ x ∈ L, x ∈ insert φ S) (hd : D.Deriv L ψ) :
+    ∃ L_S : List F, (∀ x ∈ L_S, x ∈ S) ∧ D.Deriv (φ :: L_S) ψ := by
+  classical
+  let L_S := L.filter (fun x => decide (x ≠ φ) = true)
+  refine ⟨L_S, ?_, ?_⟩
+  · intro x hx
+    simp only [L_S, List.mem_filter, decide_eq_true_eq] at hx
+    rcases Set.mem_insert_iff.mp (hL x hx.1) with rfl | hxS
+    · exact absurd rfl hx.2
+    · exact hxS
+  · exact D.weakening hd (fun x hx => by
+      by_cases hxφ : x = φ
+      · exact List.mem_cons.mpr (Or.inl hxφ)
+      · exact List.mem_cons.mpr (Or.inr (by
+          simp only [L_S, List.mem_filter, decide_eq_true_eq]; exact ⟨hx, hxφ⟩)))
+
+/-- A maximally consistent set is closed under derivation, given the deduction theorem.
+
+If `L ⊆ S` and `L ⊢ φ`, then `φ ∈ S`. Proof: assume `φ ∉ S`. By maximality,
+`insert φ S` is inconsistent, so some `L' ⊆ insert φ S` derives `⊥`. Extract a
+derivation `φ :: L_S ⊢ ⊥` where `L_S ⊆ S`, apply the deduction theorem to get
+`L_S ⊢ φ → ⊥`. Combined with the weakened `L_S ++ L ⊢ φ` and `L_S ++ L ⊢ φ → ⊥`,
+we get `L_S ++ L ⊢ ⊥` from `S`, contradicting set-consistency. -/
+theorem SetMaximalConsistent.closed_under_derivation
+    (D : DerivationSystem F) (hdt : HasDeductionTheorem D)
+    {S : Set F} (h_mcs : SetMaximalConsistent D S)
+    {L : List F} (h_sub : ∀ ψ ∈ L, ψ ∈ S)
+    {φ : F} (h_deriv : D.Deriv L φ) : φ ∈ S := by
+  by_contra hφ
+  -- By maximality, insert φ S is inconsistent
+  have hinc := h_mcs.2 φ hφ
+  unfold SetConsistent Consistent at hinc
+  push Not at hinc
+  obtain ⟨L', hL'sub, hL'bot⟩ := hinc
+  -- Extract derivation from φ :: L_S where L_S ⊆ S
+  obtain ⟨L_S, hL_S_sub, hcons_deriv⟩ := derives_from_insert_to_cons D hL'sub hL'bot
+  -- Apply DT: L_S ⊢ φ → ⊥
+  have h_neg : D.Deriv L_S (HasImp.imp φ HasBot.bot) := hdt hcons_deriv
+  -- Weaken both to L_S ++ L
+  have h_neg' : D.Deriv (L_S ++ L) (HasImp.imp φ HasBot.bot) :=
+    D.weakening h_neg (fun x hx => List.mem_append.mpr (Or.inl hx))
+  have h_phi : D.Deriv (L_S ++ L) φ :=
+    D.weakening h_deriv (fun x hx => List.mem_append.mpr (Or.inr hx))
+  -- MP: L_S ++ L ⊢ ⊥
+  have h_bot : D.Deriv (L_S ++ L) HasBot.bot := D.mp h_neg' h_phi
+  -- All elements of L_S ++ L are in S
+  have h_all_S : ∀ ψ ∈ L_S ++ L, ψ ∈ S := by
+    intro ψ hψ
+    rcases List.mem_append.mp hψ with h | h
+    · exact hL_S_sub ψ h
+    · exact h_sub ψ h
+  -- Contradiction with set-consistency
+  exact h_mcs.1 (L_S ++ L) h_all_S h_bot
+
+/-- Implication property: if `φ → ψ ∈ S` and `φ ∈ S`, then `ψ ∈ S`.
+Follows directly from `closed_under_derivation` via modus ponens. -/
+theorem SetMaximalConsistent.implication_property
+    (D : DerivationSystem F) (hdt : HasDeductionTheorem D)
+    {S : Set F} (h_mcs : SetMaximalConsistent D S)
+    {φ ψ : F} (h_imp : HasImp.imp φ ψ ∈ S) (h_phi : φ ∈ S) : ψ ∈ S :=
+  closed_under_derivation D hdt h_mcs
+    (L := [HasImp.imp φ ψ, φ])
+    (fun x hx => by
+      rw [List.mem_cons] at hx
+      rcases hx with rfl | hx
+      · exact h_imp
+      · rw [List.mem_cons] at hx; rcases hx with rfl | hx
+        · exact h_phi
+        · simp at hx)
+    (D.mp (D.assumption (List.mem_cons.mpr (Or.inl rfl)))
+      (D.assumption (List.mem_cons.mpr (Or.inr (List.mem_cons.mpr (Or.inl rfl))))))
+
+/-- Negation completeness: for any formula `φ`, either `φ ∈ S` or `(φ → ⊥) ∈ S`.
+Uses the deduction theorem and maximality. -/
+theorem SetMaximalConsistent.negation_complete
+    (D : DerivationSystem F) (hdt : HasDeductionTheorem D)
+    {S : Set F} (h_mcs : SetMaximalConsistent D S)
+    (φ : F) : φ ∈ S ∨ HasImp.imp φ HasBot.bot ∈ S := by
+  by_contra h
+  push Not at h
+  obtain ⟨hφ, hneg⟩ := h
+  -- φ ∉ S, so insert φ S is inconsistent
+  have hinc := h_mcs.2 φ hφ
+  unfold SetConsistent Consistent at hinc
+  push Not at hinc
+  obtain ⟨L', hL'sub, hL'bot⟩ := hinc
+  -- Extract derivation from φ :: L_S where L_S ⊆ S
+  obtain ⟨L_S, hL_S_sub, hcons_deriv⟩ := derives_from_insert_to_cons D hL'sub hL'bot
+  -- Apply DT: L_S ⊢ φ → ⊥
+  have h_neg : D.Deriv L_S (HasImp.imp φ HasBot.bot) := hdt hcons_deriv
+  -- (φ → ⊥) ∈ S by closed_under_derivation
+  have : HasImp.imp φ HasBot.bot ∈ S :=
+    closed_under_derivation D hdt h_mcs hL_S_sub h_neg
+  exact hneg this
+
+end Cslib.Logic.Metalogic
diff --git a/Cslib/Foundations/Logic/Metalogic/DeductionHelpers.lean b/Cslib/Foundations/Logic/Metalogic/DeductionHelpers.lean
new file mode 100644
index 000000000..9b96e1657
--- /dev/null
+++ b/Cslib/Foundations/Logic/Metalogic/DeductionHelpers.lean
@@ -0,0 +1,120 @@
+/-
+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
+public import Cslib.Foundations.Logic.Connectives
+
+/-! # Generic Deduction Theorem Helpers
+
+This module defines a `HasHilbertTree` typeclass abstracting the common structure
+needed by the 4 deduction theorem helper lemmas across PL, Modal, Temporal, and
+Bimodal logics. Each logic instantiates this typeclass, and the 4 generic helpers
+(`deductionAxiom`, `deductionImpSelf`, `deductionAssumptionOther`,
+`deductionMpUnderImp`) are proven once here.
+
+The per-logic `deduction_with_mem` and `deduction_theorem` remain concrete in each
+logic because they require pattern matching on concrete `DerivationTree` constructors
+and use `termination_by` on concrete height functions.
+
+## Design
+
+The typeclass provides 6 fields:
+- `Tree`: The derivation tree type `List F → F → Type*`
+- `implyK`: Produces `[] ⊢ φ → (ψ → φ)` (K/weakening axiom)
+- `implyS`: Produces `[] ⊢ (φ→(ψ→χ)) → ((φ→ψ) → (φ→χ))` (S/distribution axiom)
+- `assumption`: From `φ ∈ Γ`, produces `Γ ⊢ φ`
+- `mp`: From `Γ ⊢ φ → ψ` and `Γ ⊢ φ`, produces `Γ ⊢ ψ`
+- `weakening`: From `Γ ⊢ φ` and `∀ x ∈ Γ, x ∈ Δ`, produces `Δ ⊢ φ`
+
+The `implyK`/`implyS` fields produce trees from the empty context, already
+incorporating any axiom-type or frame-class proofs. This allows the generic
+helpers to work uniformly across logics with different axiom systems.
+
+## References
+
+* Cslib/Logics/Propositional/Metalogic/DeductionTheorem.lean
+* Cslib/Logics/Modal/Metalogic/DeductionTheorem.lean
+* Cslib/Logics/Temporal/Metalogic/DeductionTheorem.lean
+* Cslib/Logics/Bimodal/Metalogic/Core/DeductionTheorem.lean
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+open Cslib.Logic
+
+variable {F : Type*} [HasImp F]
+
+/-- Typeclass abstracting the Hilbert-style derivation tree operations needed
+by the deduction theorem helper lemmas.
+
+Each logic (PL, Modal, Temporal, Bimodal) instantiates this with its own
+`DerivationTree` type and axiom constructors. The `implyK` and `implyS` fields
+produce trees from the empty context, encapsulating logic-specific axiom
+constructors and frame-class proofs. -/
+class HasHilbertTree (F : Type*) [HasImp F] where
+  /-- The derivation tree type, parameterized by context and conclusion. -/
+  Tree : List F → F → Type*
+  /-- K axiom (weakening): `[] ⊢ φ → (ψ → φ)` -/
+  implyK : (φ ψ : F) → Tree [] (HasImp.imp φ (HasImp.imp ψ φ))
+  /-- S axiom (distribution): `[] ⊢ (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))` -/
+  implyS : (φ ψ χ : F) → Tree []
+    (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ))
+      (HasImp.imp (HasImp.imp φ ψ) (HasImp.imp φ χ)))
+  /-- Assumption rule: from `φ ∈ Γ`, derive `Γ ⊢ φ`. -/
+  assumption : {Γ : List F} → {φ : F} → φ ∈ Γ → Tree Γ φ
+  /-- Modus ponens: from `Γ ⊢ φ → ψ` and `Γ ⊢ φ`, derive `Γ ⊢ ψ`. -/
+  mp : {Γ : List F} → {φ ψ : F} → Tree Γ (HasImp.imp φ ψ) → Tree Γ φ → Tree Γ ψ
+  /-- Weakening: from `Γ ⊢ φ` and `∀ x ∈ Γ, x ∈ Δ`, derive `Δ ⊢ φ`. -/
+  weakening : {Γ Δ : List F} → {φ : F} → Tree Γ φ → (∀ x ∈ Γ, x ∈ Δ) → Tree Δ φ
+
+variable [HasHilbertTree F]
+
+/-! ## Generic Deduction Helpers -/
+
+/-- If `d` is a derivation of `φ` from empty context, then `Γ ⊢ A → φ`.
+This is the axiom case of the deduction theorem. -/
+noncomputable def deductionAxiom (Γ : List F) (A : F)
+    (d_empty : HasHilbertTree.Tree (F := F) [] φ) :
+    HasHilbertTree.Tree Γ (HasImp.imp A φ) :=
+  let k := HasHilbertTree.implyK (F := F) φ A
+  let step := HasHilbertTree.mp k d_empty
+  HasHilbertTree.weakening step (fun _ h => nomatch h)
+
+/-- `Γ ⊢ A → A` (identity / self-implication).
+Built from S, K, K axioms. -/
+noncomputable def deductionImpSelf (Γ : List F) (A : F) :
+    HasHilbertTree.Tree Γ (HasImp.imp A A) :=
+  let s := HasHilbertTree.implyS (F := F) A (HasImp.imp A A) A
+  let k1 := HasHilbertTree.implyK (F := F) A (HasImp.imp A A)
+  let k2 := HasHilbertTree.implyK (F := F) A A
+  let step1 := HasHilbertTree.mp s k1
+  let result := HasHilbertTree.mp step1 k2
+  HasHilbertTree.weakening result (fun _ h => nomatch h)
+
+/-- If `B ∈ Γ`, then `Γ ⊢ A → B`. Uses the K axiom. -/
+noncomputable def deductionAssumptionOther (Γ : List F) (A B : F)
+    (h_mem : B ∈ Γ) : HasHilbertTree.Tree Γ (HasImp.imp A B) :=
+  let b_deriv := HasHilbertTree.assumption (F := F) h_mem
+  let k := HasHilbertTree.implyK (F := F) B A
+  let k_weak := HasHilbertTree.weakening k (fun _ h => nomatch h)
+  HasHilbertTree.mp k_weak b_deriv
+
+/-- Modus ponens under implication: from `Γ ⊢ A → (C → D)` and `Γ ⊢ A → C`,
+derive `Γ ⊢ A → D`. Uses the S axiom. -/
+noncomputable def deductionMpUnderImp (Γ : List F) (A C D : F)
+    (h₁ : HasHilbertTree.Tree Γ (HasImp.imp A (HasImp.imp C D)))
+    (h₂ : HasHilbertTree.Tree Γ (HasImp.imp A C)) :
+    HasHilbertTree.Tree Γ (HasImp.imp A D) :=
+  let s := HasHilbertTree.implyS (F := F) A C D
+  let s_weak := HasHilbertTree.weakening s (fun _ h => nomatch h)
+  let step1 := HasHilbertTree.mp s_weak h₁
+  HasHilbertTree.mp step1 h₂
+
+end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/ProofSystem.lean b/Cslib/Foundations/Logic/ProofSystem.lean
new file mode 100644
index 000000000..1e8dee48a
--- /dev/null
+++ b/Cslib/Foundations/Logic/ProofSystem.lean
@@ -0,0 +1,353 @@
+/-
+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
+public import Cslib.Foundations.Logic.InferenceSystem
+public import Cslib.Foundations.Logic.Axioms
+
+/-! # Proof System Typeclasses
+
+This module defines the typeclass hierarchy for Hilbert-style proof systems.
+Each axiom gets a `HasAxiom*` typeclass, and bundled proof system classes
+compose these via `extends`.
+
+## Architecture
+
+### Layer 1: Individual Axiom Typeclasses
+
+Each `HasAxiom*` typeclass states that a particular proof system tag `S`
+proves the corresponding axiom for all formula instantiations.
+
+### Layer 2: Inference Rule Typeclasses
+
+`ModusPonens`, `Necessitation` state that the proof system is closed
+under the corresponding rule.
+
+### Layer 3: Bundled Proof System Classes
+
+`PropositionalHilbert`, `ModalHilbert`, `ModalS5Hilbert`, etc. compose
+the individual axiom and rule typeclasses via `extends`.
+
+### Layer 4: Tag Types
+
+Opaque tag types (`Propositional.HilbertCl`, `Modal.HilbertK`, etc.)
+serve as proof system identifiers. Concrete `InferenceSystem` and
+`HasAxiom*` instances will be registered when derivation trees are defined.
+
+## Note
+
+This module defines the **interface** only. Concrete instances require
+derivation trees (not yet ported) and are future work.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+variable {F : Type*}
+
+/-! ### Inference Rule Typeclasses -/
+
+/-- A proof system has modus ponens: from `S ⊢ φ → ψ` and `S ⊢ φ`,
+    derive `S ⊢ ψ`. -/
+class ModusPonens (S : Type*) [HasImp F] [InferenceSystem S F] where
+  /-- Modus ponens rule. -/
+  mp {φ ψ : F} : InferenceSystem.DerivableIn S (HasImp.imp φ ψ) →
+    InferenceSystem.DerivableIn S φ → InferenceSystem.DerivableIn S ψ
+
+/-- A proof system has necessitation: from `S ⊢ φ`, derive `S ⊢ □φ`. -/
+class Necessitation (S : Type*) [HasBox F] [InferenceSystem S F] where
+  /-- Necessitation rule. -/
+  nec {φ : F} :
+    InferenceSystem.DerivableIn S φ →
+    InferenceSystem.DerivableIn S (HasBox.box φ)
+
+/-- The proof system has temporal necessitation: from `S ⊢ φ`, derive `S ⊢ G(φ)`
+    and `S ⊢ H(φ)`.
+    G(φ) = ¬F(¬φ) = (⊤ U (φ → ⊥)) → ⊥
+    H(φ) = ¬P(¬φ) = (⊤ S (φ → ⊥)) → ⊥ -/
+class TemporalNecessitation (S : Type*) [HasBot F] [HasImp F]
+    [HasUntil F] [HasSince F] [InferenceSystem S F] where
+  /-- Temporal necessitation (G-necessitation): from `S ⊢ φ`, derive `S ⊢ G(φ)`. -/
+  tempNec {φ : F} :
+    InferenceSystem.DerivableIn S φ →
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasUntil.untl (HasImp.imp φ HasBot.bot)
+          (HasImp.imp (HasBot.bot : F) HasBot.bot))
+        HasBot.bot)
+  /-- Past temporal necessitation (H-necessitation): from `S ⊢ φ`, derive `S ⊢ H(φ)`. -/
+  tempNecPast {φ : F} :
+    InferenceSystem.DerivableIn S φ →
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasSince.snce (HasImp.imp φ HasBot.bot)
+          (HasImp.imp (HasBot.bot : F) HasBot.bot))
+        HasBot.bot)
+
+/-! ### Individual Axiom Typeclasses -/
+
+section AxiomClasses
+
+variable (S : Type*) [HasBot F] [HasImp F] [InferenceSystem S F]
+
+/-- The proof system proves ImplyK: φ → (ψ → φ). -/
+class HasAxiomImplyK where
+  implyK {φ ψ : F} : InferenceSystem.DerivableIn S (Axioms.ImplyK φ ψ)
+
+/-- The proof system proves ImplyS. -/
+class HasAxiomImplyS where
+  implyS {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S (Axioms.ImplyS φ ψ χ)
+
+/-- The proof system proves EFQ: ⊥ → φ. -/
+class HasAxiomEFQ where
+  efq {φ : F} : InferenceSystem.DerivableIn S (Axioms.EFQ φ)
+
+/-- The proof system proves Peirce's law. -/
+class HasAxiomPeirce where
+  peirce {φ ψ : F} :
+    InferenceSystem.DerivableIn S (Axioms.Peirce φ ψ)
+
+/-- The proof system proves DNE: ¬¬φ → φ. -/
+class HasAxiomDNE where
+  dne {φ : F} : InferenceSystem.DerivableIn S (Axioms.DNE φ)
+
+variable [HasBox F]
+
+/-- The proof system proves axiom K: □(φ → ψ) → (□φ → □ψ). -/
+class HasAxiomK where
+  K {φ ψ : F} : InferenceSystem.DerivableIn S (Axioms.AxiomK φ ψ)
+
+/-- The proof system proves axiom T: □φ → φ. -/
+class HasAxiomT where
+  T {φ : F} : InferenceSystem.DerivableIn S (Axioms.AxiomT φ)
+
+/-- The proof system proves axiom 4: □φ → □□φ. -/
+class HasAxiom4 where
+  four {φ : F} : InferenceSystem.DerivableIn S (Axioms.Axiom4 φ)
+
+/-- The proof system proves axiom B: φ → □◇φ. -/
+class HasAxiomB where
+  B {φ : F} : InferenceSystem.DerivableIn S (Axioms.AxiomB φ)
+
+/-- The proof system proves axiom 5: ◇φ → □◇φ. -/
+class HasAxiom5 where
+  five {φ : F} : InferenceSystem.DerivableIn S (Axioms.Axiom5 φ)
+
+/-- The proof system proves axiom D: □φ → ◇φ. -/
+class HasAxiomD where
+  D {φ : F} : InferenceSystem.DerivableIn S (Axioms.AxiomD φ)
+
+variable [HasUntil F]
+
+/-- The proof system proves the modal-future interaction axiom. -/
+class HasAxiomMF where
+  MF {φ : F} :
+    InferenceSystem.DerivableIn S (Axioms.ModalFuture φ)
+
+end AxiomClasses
+
+/-! ### Temporal Axiom Typeclasses -/
+
+section TemporalAxiomClasses
+
+variable (S : Type*) [HasBot F] [HasImp F] [HasUntil F] [HasSince F]
+  [InferenceSystem S F]
+
+/-- The proof system proves serial future (BX1): ⊤ → F ⊤. -/
+class HasAxiomSerialFuture where
+  serialFuture : InferenceSystem.DerivableIn S (Axioms.SerialFuture (F := F))
+
+/-- The proof system proves serial past (BX1'): ⊤ → P ⊤. -/
+class HasAxiomSerialPast where
+  serialPast : InferenceSystem.DerivableIn S (Axioms.SerialPast (F := F))
+
+/-- The proof system proves guard monotonicity of Until under G (BX2G). -/
+class HasAxiomLeftMonoUntilG where
+  leftMonoUntilG {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S (Axioms.LeftMonoUntilG φ ψ χ)
+
+/-- The proof system proves guard monotonicity of Since under H (BX2H). -/
+class HasAxiomLeftMonoSinceH where
+  leftMonoSinceH {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S (Axioms.LeftMonoSinceH φ ψ χ)
+
+/-- The proof system proves event monotonicity of Until (BX3). -/
+class HasAxiomRightMonoUntil where
+  rightMonoUntil {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S (Axioms.RightMonoUntil φ ψ χ)
+
+/-- The proof system proves event monotonicity of Since (BX3'). -/
+class HasAxiomRightMonoSince where
+  rightMonoSince {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S (Axioms.RightMonoSince φ ψ χ)
+
+/-- The proof system proves temporal connectedness future (BX4). -/
+class HasAxiomConnectFuture where
+  connectFuture {φ : F} :
+    InferenceSystem.DerivableIn S (Axioms.ConnectFuture φ)
+
+/-- The proof system proves temporal connectedness past (BX4'). -/
+class HasAxiomConnectPast where
+  connectPast {φ : F} :
+    InferenceSystem.DerivableIn S (Axioms.ConnectPast φ)
+
+/-- The proof system proves Until-Since enrichment (BX13). -/
+class HasAxiomEnrichmentUntil where
+  enrichmentUntil {φ ψ p : F} :
+    InferenceSystem.DerivableIn S (Axioms.EnrichmentUntil φ ψ p)
+
+/-- The proof system proves Since-Until enrichment (BX13'). -/
+class HasAxiomEnrichmentSince where
+  enrichmentSince {φ ψ p : F} :
+    InferenceSystem.DerivableIn S (Axioms.EnrichmentSince φ ψ p)
+
+/-- The proof system proves self-accumulation of Until (BX5). -/
+class HasAxiomSelfAccumUntil where
+  selfAccumUntil {φ ψ : F} :
+    InferenceSystem.DerivableIn S (Axioms.SelfAccumUntil φ ψ)
+
+/-- The proof system proves self-accumulation of Since (BX5'). -/
+class HasAxiomSelfAccumSince where
+  selfAccumSince {φ ψ : F} :
+    InferenceSystem.DerivableIn S (Axioms.SelfAccumSince φ ψ)
+
+/-- The proof system proves absorption of Until (BX6). -/
+class HasAxiomAbsorbUntil where
+  absorbUntil {φ ψ : F} :
+    InferenceSystem.DerivableIn S (Axioms.AbsorbUntil φ ψ)
+
+/-- The proof system proves absorption of Since (BX6'). -/
+class HasAxiomAbsorbSince where
+  absorbSince {φ ψ : F} :
+    InferenceSystem.DerivableIn S (Axioms.AbsorbSince φ ψ)
+
+/-- The proof system proves linearity of Until (BX7). -/
+class HasAxiomLinearUntil where
+  linearUntil {φ ψ χ θ : F} :
+    InferenceSystem.DerivableIn S (Axioms.LinearUntil φ ψ χ θ)
+
+/-- The proof system proves linearity of Since (BX7'). -/
+class HasAxiomLinearSince where
+  linearSince {φ ψ χ θ : F} :
+    InferenceSystem.DerivableIn S (Axioms.LinearSince φ ψ χ θ)
+
+/-- The proof system proves Until implies eventuality (BX10). -/
+class HasAxiomUntilF where
+  untilF {φ ψ : F} :
+    InferenceSystem.DerivableIn S (Axioms.UntilF φ ψ)
+
+/-- The proof system proves Since implies past eventuality (BX10'). -/
+class HasAxiomSinceP where
+  sinceP {φ ψ : F} :
+    InferenceSystem.DerivableIn S (Axioms.SinceP φ ψ)
+
+/-- The proof system proves temporal linearity (BX11). -/
+class HasAxiomTempLinearity where
+  tempLinearity {φ ψ : F} :
+    InferenceSystem.DerivableIn S (Axioms.TempLinearity φ ψ)
+
+/-- The proof system proves temporal linearity past (BX11'). -/
+class HasAxiomTempLinearityPast where
+  tempLinearityPast {φ ψ : F} :
+    InferenceSystem.DerivableIn S (Axioms.TempLinearityPast φ ψ)
+
+/-- The proof system proves F-Until equivalence (BX12). -/
+class HasAxiomFUntilEquiv where
+  fUntilEquiv {φ : F} :
+    InferenceSystem.DerivableIn S (Axioms.FUntilEquiv φ)
+
+/-- The proof system proves P-Since equivalence (BX12'). -/
+class HasAxiomPSinceEquiv where
+  pSinceEquiv {φ : F} :
+    InferenceSystem.DerivableIn S (Axioms.PSinceEquiv φ)
+
+end TemporalAxiomClasses
+
+/-! ### Bundled Proof System Classes -/
+
+/-- Classical propositional Hilbert system. -/
+class PropositionalHilbert (S : Type*) [HasBot F] [HasImp F]
+    [InferenceSystem S F]
+    extends ModusPonens S (F := F),
+            HasAxiomImplyK S (F := F),
+            HasAxiomImplyS S (F := F),
+            HasAxiomEFQ S (F := F),
+            HasAxiomPeirce S (F := F)
+
+/-- Modal Hilbert system K. -/
+class ModalHilbert (S : Type*) [HasBot F] [HasImp F] [HasBox F]
+    [InferenceSystem S F]
+    extends PropositionalHilbert S (F := F),
+            Necessitation S (F := F),
+            HasAxiomK S (F := F)
+
+/-- Modal Hilbert system S5 (extends K with T, 4, B). -/
+class ModalS5Hilbert (S : Type*) [HasBot F] [HasImp F] [HasBox F]
+    [InferenceSystem S F]
+    extends ModalHilbert S (F := F),
+            HasAxiomT S (F := F),
+            HasAxiom4 S (F := F),
+            HasAxiomB S (F := F)
+
+/-- Temporal Hilbert system BX: extends propositional logic with temporal
+    necessitation and all 22 BX temporal axiom typeclasses. -/
+class TemporalBXHilbert (S : Type*) [HasBot F] [HasImp F] [HasUntil F]
+    [HasSince F] [InferenceSystem S F]
+    extends PropositionalHilbert S (F := F),
+            TemporalNecessitation S (F := F),
+            HasAxiomSerialFuture S (F := F),
+            HasAxiomSerialPast S (F := F),
+            HasAxiomLeftMonoUntilG S (F := F),
+            HasAxiomLeftMonoSinceH S (F := F),
+            HasAxiomRightMonoUntil S (F := F),
+            HasAxiomRightMonoSince S (F := F),
+            HasAxiomConnectFuture S (F := F),
+            HasAxiomConnectPast S (F := F),
+            HasAxiomEnrichmentUntil S (F := F),
+            HasAxiomEnrichmentSince S (F := F),
+            HasAxiomSelfAccumUntil S (F := F),
+            HasAxiomSelfAccumSince S (F := F),
+            HasAxiomAbsorbUntil S (F := F),
+            HasAxiomAbsorbSince S (F := F),
+            HasAxiomLinearUntil S (F := F),
+            HasAxiomLinearSince S (F := F),
+            HasAxiomUntilF S (F := F),
+            HasAxiomSinceP S (F := F),
+            HasAxiomTempLinearity S (F := F),
+            HasAxiomTempLinearityPast S (F := F),
+            HasAxiomFUntilEquiv S (F := F),
+            HasAxiomPSinceEquiv S (F := F)
+
+/-- Bimodal Hilbert system TM: extends S5 modal logic and BX temporal logic
+    with the modal-future interaction axiom. -/
+class BimodalTMHilbert (S : Type*) [HasBot F] [HasImp F] [HasBox F]
+    [HasUntil F] [HasSince F] [InferenceSystem S F]
+    extends ModalS5Hilbert S (F := F),
+            TemporalBXHilbert S (F := F),
+            HasAxiomMF S (F := F)
+
+/-! ### Tag Types -/
+
+/-- Tag type for classical propositional Hilbert system. -/
+opaque Propositional.HilbertCl : Type := Empty
+
+/-- Tag type for modal logic K. -/
+opaque Modal.HilbertK : Type := Empty
+
+/-- Tag type for modal logic S5. -/
+opaque Modal.HilbertS5 : Type := Empty
+
+/-- Tag type for temporal logic BX. -/
+opaque Temporal.HilbertBX : Type := Empty
+
+/-- Tag type for bimodal logic TM. -/
+opaque Bimodal.HilbertTM : Type := Empty
+
+end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/Theorems.lean b/Cslib/Foundations/Logic/Theorems.lean
new file mode 100644
index 000000000..e7f899c1a
--- /dev/null
+++ b/Cslib/Foundations/Logic/Theorems.lean
@@ -0,0 +1,48 @@
+/-
+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
+public import Cslib.Foundations.Logic.Theorems.Combinators
+public import Cslib.Foundations.Logic.Theorems.Propositional.Core
+public import Cslib.Foundations.Logic.Theorems.Propositional.Connectives
+public import Cslib.Foundations.Logic.Theorems.BigConj
+public import Cslib.Foundations.Logic.Theorems.Modal.Basic
+public import Cslib.Foundations.Logic.Theorems.Modal.S5
+public import Cslib.Foundations.Logic.Theorems.Temporal.TemporalDerived
+public import Cslib.Foundations.Logic.Theorems.Temporal.FrameConditions
+
+/-! # Hilbert-Style Theorems
+
+Module aggregator for all theorems derived in the generic typeclass framework.
+
+## Submodules
+
+### Propositional (`[PropositionalHilbert S]`)
+
+- `Combinators`: I/B/C/S combinators, imp_trans, pairing, dni
+- `Propositional.Core`: LEM, DNE, raa, efq_neg, rcp, lce_imp, rce_imp
+- `Propositional.Connectives`: classical_merge, iff ops, contraposition,
+  De Morgan laws
+- `BigConj`: bigconj syntax and derivability lemmas
+
+### Modal (`[ModalHilbert S]` / `[ModalS5Hilbert S]`)
+
+- `Modal.Basic`: K-level theorems (box_mono, diamond_mono, k_dist_diamond,
+  box_contrapose, modal duality, box_iff_intro)
+- `Modal.S5`: S5-level theorems (axiom 5 derivation, t_box_to_diamond,
+  box_conj_iff, diamond_disj_iff, s5_diamond_box collapse, nested
+  modality theorems)
+
+### Temporal (`[TemporalBXHilbert S]`)
+
+- `Temporal.TemporalDerived`: BX-system derived theorems (guard/event monotonicity
+  wrappers, future/past operators, enrichment, self-accumulation, absorption,
+  linearity)
+- `Temporal.FrameConditions`: Frame condition typeclasses (LinearTemporalFrame,
+  SerialFrame, DenseTemporalFrame, DiscreteTemporalFrame)
+-/
diff --git a/Cslib/Foundations/Logic/Theorems/BigConj.lean b/Cslib/Foundations/Logic/Theorems/BigConj.lean
new file mode 100644
index 000000000..f9e7981e2
--- /dev/null
+++ b/Cslib/Foundations/Logic/Theorems/BigConj.lean
@@ -0,0 +1,142 @@
+/-
+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
+public import Cslib.Foundations.Logic.Theorems.Propositional.Core
+
+/-! # Big Conjunction over Lists of Formulas
+
+Defines `bigconj : List F → F` as a generic fold using
+`HasBot.bot` and `HasImp.imp` (Lukasiewicz encoding of conjunction),
+plus derivability lemmas for `[PropositionalHilbert S]`.
+
+## Main Definitions
+
+- `bigconj`: Big conjunction (`⊤` for empty, identity for singleton,
+  nested conjunction for longer lists)
+- `negBigconj`: Negation of big conjunction
+
+## Main Results
+
+- `bigconj_nil`, `bigconj_singleton`, `bigconj_cons_cons`: Simp lemmas
+- `bigconj_mem_derivable`: If `φ ∈ L` and `⊢ bigconj L`,
+  then `⊢ φ`
+- `bigconj_derivable_intro`: If all members of `L` are derivable,
+  then `⊢ bigconj L`
+
+## Encoding
+
+Conjunction uses the Lukasiewicz encoding:
+`φ ∧ ψ := (φ → (ψ → ⊥)) → ⊥`
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Theorems.BigConj
+
+open Cslib.Logic
+
+variable {F : Type*} [HasBot F] [HasImp F]
+
+/-! ### Syntactic Definitions -/
+
+/-- Big conjunction over a list of formulas.
+    Base case: empty list folds to `⊤ := ⊥ → ⊥`.
+    Singleton: just the formula.
+    Longer: nested conjunction. -/
+def bigconj : List F → F
+  | [] => HasImp.imp HasBot.bot HasBot.bot
+  | [φ] => φ
+  | φ :: ψ :: rest =>
+    HasImp.imp
+      (HasImp.imp φ
+        (HasImp.imp (bigconj (ψ :: rest)) HasBot.bot))
+      HasBot.bot
+
+/-- Negated big conjunction. -/
+def negBigconj (L : List F) : F :=
+  HasImp.imp (bigconj L) HasBot.bot
+
+@[simp] theorem bigconj_nil :
+    bigconj (F := F) [] =
+      HasImp.imp HasBot.bot HasBot.bot := rfl
+
+@[simp] theorem bigconj_singleton (φ : F) :
+    bigconj [φ] = φ := rfl
+
+@[simp] theorem bigconj_cons_cons (φ ψ : F)
+    (rest : List F) :
+    bigconj (φ :: ψ :: rest) =
+      HasImp.imp
+        (HasImp.imp φ
+          (HasImp.imp (bigconj (ψ :: rest)) HasBot.bot))
+        HasBot.bot := rfl
+
+@[simp] theorem negBigconj_def (L : List F) :
+    negBigconj L = HasImp.imp (bigconj L) HasBot.bot :=
+  rfl
+
+/-! ### Derivability Lemmas -/
+
+variable {S : Type*} [InferenceSystem S F]
+variable [PropositionalHilbert S (F := F)]
+
+open Cslib.Logic.Theorems.Combinators
+open Cslib.Logic.Theorems.Propositional.Core
+
+section BigConj
+
+/-- If `φ ∈ L` and `⊢ bigconj L`, then `⊢ φ`. -/
+theorem bigconj_mem_derivable {L : List F} {φ : F}
+    (hmem : φ ∈ L)
+    (hconj : InferenceSystem.DerivableIn S (bigconj L)) :
+    InferenceSystem.DerivableIn S φ := by
+  induction L with
+  | nil => simp only [List.not_mem_nil] at hmem
+  | cons a rest ih =>
+    cases rest with
+    | nil =>
+      simp only [bigconj_singleton] at hconj
+      simp only [List.mem_singleton] at hmem
+      rw [hmem]; exact hconj
+    | cons b tail =>
+      simp only [bigconj_cons_cons] at hconj
+      cases hmem with
+      | head => exact ModusPonens.mp lce_imp hconj
+      | tail _ hmem' =>
+        have := ModusPonens.mp rce_imp hconj
+        exact ih hmem' this
+
+/-- If all members of `L` are derivable, then `⊢ bigconj L`. -/
+theorem bigconj_derivable_intro {L : List F}
+    (h : ∀ φ ∈ L, InferenceSystem.DerivableIn S φ) :
+    InferenceSystem.DerivableIn S (bigconj L) := by
+  induction L with
+  | nil =>
+    simp only [bigconj_nil]
+    exact identity (S := S) HasBot.bot
+  | cons a rest ih =>
+    cases rest with
+    | nil =>
+      simp only [bigconj_singleton]
+      exact h a (by simp)
+    | cons b tail =>
+      simp only [bigconj_cons_cons]
+      have ha := h a (by simp)
+      have hrest : ∀ φ ∈ (b :: tail),
+          InferenceSystem.DerivableIn S φ := by
+        intro φ hmem
+        exact h φ (by simp [hmem])
+      have ih_result := ih hrest
+      have pair := pairing (S := S) a (bigconj (b :: tail))
+      exact ModusPonens.mp
+        (ModusPonens.mp pair ha) ih_result
+
+end BigConj
+
+end Cslib.Logic.Theorems.BigConj
diff --git a/Cslib/Foundations/Logic/Theorems/Combinators.lean b/Cslib/Foundations/Logic/Theorems/Combinators.lean
new file mode 100644
index 000000000..ac101c39a
--- /dev/null
+++ b/Cslib/Foundations/Logic/Theorems/Combinators.lean
@@ -0,0 +1,339 @@
+/-
+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
+public import Cslib.Foundations.Logic.ProofSystem
+
+/-! # Propositional Reasoning Combinators
+
+This module defines fundamental propositional reasoning combinators derived from
+the ImplyK and ImplyS axioms. These combinators provide the foundation for all
+propositional theorems in the Hilbert-style proof system.
+
+All theorems are generic over `[PropositionalHilbert S]`.
+
+## Main Combinators
+
+- `imp_trans`: Transitivity of implication (hypothetical syllogism)
+- `identity`: Identity combinator (SKK construction)
+- `b_combinator`: B combinator (function composition)
+- `flip`: C combinator (argument flip)
+- `app1`: Single application lemma
+- `app2`: Double application lemma (Vireo combinator)
+- `pairing`: Conjunction introduction combinator
+- `dni`: Double negation introduction
+- `combine_imp_conj`: Combine implications into conjunction
+- `combine_imp_conj_3`: Combine three implications into conjunction
+
+## Naming Convention
+
+BimodalLogic's `Axiom.prop_s` (weakening: φ → (ψ → φ)) maps to cslib's
+`ImplyK`. BimodalLogic's `Axiom.prop_k` (distribution) maps to cslib's
+`ImplyS`.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Theorems.Combinators
+
+open Cslib.Logic
+
+variable {F : Type*} [HasBot F] [HasImp F]
+variable {S : Type*} [InferenceSystem S F]
+variable [PropositionalHilbert S (F := F)]
+
+section Combinators
+
+/-- Transitivity of implication: from `⊢ φ → ψ` and `⊢ ψ → χ`,
+    derive `⊢ φ → χ`. -/
+theorem imp_trans {φ ψ χ : F}
+    (h1 : InferenceSystem.DerivableIn S (HasImp.imp φ ψ))
+    (h2 : InferenceSystem.DerivableIn S (HasImp.imp ψ χ)) :
+    InferenceSystem.DerivableIn S (HasImp.imp φ χ) := by
+  have h3 := ModusPonens.mp
+    (HasAxiomImplyK.implyK
+      (S := S) (φ := HasImp.imp ψ χ) (ψ := φ)) h2
+  have h4 := ModusPonens.mp
+    (HasAxiomImplyS.implyS
+      (S := S) (φ := φ) (ψ := ψ) (χ := χ)) h3
+  exact ModusPonens.mp h4 h1
+
+/-- Identity combinator: `⊢ φ → φ` (SKK construction). -/
+theorem identity (φ : F) :
+    InferenceSystem.DerivableIn S (HasImp.imp φ φ) := by
+  have k1 : InferenceSystem.DerivableIn S
+      (HasImp.imp φ (HasImp.imp (HasImp.imp φ φ) φ)) :=
+    HasAxiomImplyK.implyK
+  have k2 : InferenceSystem.DerivableIn S
+      (HasImp.imp φ (HasImp.imp φ φ)) :=
+    HasAxiomImplyK.implyK
+  have s1 := HasAxiomImplyS.implyS
+    (S := S) (φ := φ) (ψ := HasImp.imp φ φ) (χ := φ)
+  exact ModusPonens.mp (ModusPonens.mp s1 k1) k2
+
+/-- B combinator (composition):
+    `⊢ (ψ → χ) → (φ → ψ) → (φ → χ)`. -/
+theorem b_combinator {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp ψ χ)
+        (HasImp.imp (HasImp.imp φ ψ)
+          (HasImp.imp φ χ))) :=
+  imp_trans HasAxiomImplyK.implyK HasAxiomImplyS.implyS
+
+/-- C combinator (flip):
+    `⊢ (φ → ψ → χ) → (ψ → φ → χ)`. -/
+theorem flip {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ))
+        (HasImp.imp ψ (HasImp.imp φ χ))) := by
+  have step1 := HasAxiomImplyK.implyK (S := S)
+    (φ := HasImp.imp φ (HasImp.imp ψ χ)) (ψ := ψ)
+  have k_abc := HasAxiomImplyS.implyS (S := S)
+    (φ := φ) (ψ := ψ) (χ := χ)
+  have step2 := ModusPonens.mp
+    (HasAxiomImplyK.implyK (S := S)
+      (φ := HasImp.imp
+        (HasImp.imp φ (HasImp.imp ψ χ))
+        (HasImp.imp (HasImp.imp φ ψ) (HasImp.imp φ χ)))
+      (ψ := ψ))
+    k_abc
+  have step3 := ModusPonens.mp
+    (HasAxiomImplyS.implyS (S := S) (φ := ψ)
+      (ψ := HasImp.imp φ (HasImp.imp ψ χ))
+      (χ := HasImp.imp (HasImp.imp φ ψ) (HasImp.imp φ χ)))
+    step2
+  have step4 := imp_trans step1 step3
+  have s_ab := HasAxiomImplyK.implyK (S := S)
+    (φ := ψ) (ψ := φ)
+  have k_final := HasAxiomImplyS.implyS (S := S) (φ := ψ)
+    (ψ := HasImp.imp φ ψ) (χ := HasImp.imp φ χ)
+  have step5 := imp_trans step4 k_final
+  have step6 := ModusPonens.mp
+    (HasAxiomImplyK.implyK (S := S)
+      (φ := HasImp.imp ψ (HasImp.imp φ ψ))
+      (ψ := HasImp.imp φ (HasImp.imp ψ χ)))
+    s_ab
+  have k_combine := HasAxiomImplyS.implyS (S := S)
+    (φ := HasImp.imp φ (HasImp.imp ψ χ))
+    (ψ := HasImp.imp ψ (HasImp.imp φ ψ))
+    (χ := HasImp.imp ψ (HasImp.imp φ χ))
+  exact ModusPonens.mp
+    (ModusPonens.mp k_combine step5) step6
+
+/-- Single application lemma: `⊢ φ → (φ → ψ) → ψ`. -/
+theorem app1 {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp φ
+        (HasImp.imp (HasImp.imp φ ψ) ψ)) := by
+  have id_ab := identity (S := S) (HasImp.imp φ ψ)
+  exact ModusPonens.mp
+    (@flip F _ _ S _ _
+      (HasImp.imp φ ψ) φ ψ) id_ab
+
+/-- Double application (Vireo):
+    `⊢ φ → ψ → (φ → ψ → χ) → χ`. -/
+theorem app2 {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp φ (HasImp.imp ψ
+        (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ))
+          χ))) := by
+  -- Stage 1: Build the two app1 base lemmas
+  have step_a : InferenceSystem.DerivableIn S
+      (HasImp.imp φ (HasImp.imp
+        (HasImp.imp φ (HasImp.imp ψ χ))
+        (HasImp.imp ψ χ))) :=
+    app1
+  have step_b : InferenceSystem.DerivableIn S
+      (HasImp.imp ψ (HasImp.imp (HasImp.imp ψ χ) χ)) :=
+    app1
+  -- Stage 2: Weaken and flip to get both under ψ scope
+  have a_b_bc_c := ModusPonens.mp
+    (HasAxiomImplyK.implyK (S := S)
+      (φ := HasImp.imp ψ (HasImp.imp (HasImp.imp ψ χ) χ))
+      (ψ := φ))
+    step_b
+  have b_a := ModusPonens.mp
+    (HasAxiomImplyK.implyK (S := S)
+      (φ := HasImp.imp φ (HasImp.imp
+        (HasImp.imp φ (HasImp.imp ψ χ))
+        (HasImp.imp ψ χ)))
+      (ψ := ψ))
+    step_a
+  have a_b_abc_bc := ModusPonens.mp
+    (@flip F _ _ S _ _
+      ψ φ (HasImp.imp
+        (HasImp.imp φ (HasImp.imp ψ χ))
+        (HasImp.imp ψ χ)))
+    b_a
+  -- Stage 3: B-combinator composition for (ψ→χ)→χ chain
+  have b_comp : InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp (HasImp.imp ψ χ) χ)
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ))
+            (HasImp.imp ψ χ))
+          (HasImp.imp
+            (HasImp.imp φ (HasImp.imp ψ χ)) χ))) :=
+    b_combinator
+  have b_b_comp := ModusPonens.mp
+    (HasAxiomImplyK.implyK (S := S)
+      (φ := HasImp.imp
+        (HasImp.imp (HasImp.imp ψ χ) χ)
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ))
+            (HasImp.imp ψ χ))
+          (HasImp.imp
+            (HasImp.imp φ (HasImp.imp ψ χ)) χ)))
+      (ψ := ψ))
+    b_comp
+  have k_b := HasAxiomImplyS.implyS (S := S) (φ := ψ)
+    (ψ := HasImp.imp (HasImp.imp ψ χ) χ)
+    (χ := HasImp.imp
+      (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ))
+        (HasImp.imp ψ χ))
+      (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ)) χ))
+  have step7_b := ModusPonens.mp k_b b_b_comp
+  -- Stage 4: Lift composition under φ scope via S and K
+  have weak_step7 := ModusPonens.mp
+    (HasAxiomImplyK.implyK (S := S)
+      (φ := HasImp.imp
+        (HasImp.imp ψ (HasImp.imp (HasImp.imp ψ χ) χ))
+        (HasImp.imp ψ
+          (HasImp.imp
+            (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ))
+              (HasImp.imp ψ χ))
+            (HasImp.imp
+              (HasImp.imp φ (HasImp.imp ψ χ)) χ))))
+      (ψ := φ))
+    step7_b
+  have k_a := HasAxiomImplyS.implyS (S := S) (φ := φ)
+    (ψ := HasImp.imp ψ (HasImp.imp (HasImp.imp ψ χ) χ))
+    (χ := HasImp.imp ψ
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ))
+          (HasImp.imp ψ χ))
+        (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ)) χ)))
+  have step8 := ModusPonens.mp k_a weak_step7
+  have step9 := ModusPonens.mp step8 a_b_bc_c
+  -- Stage 5: Final composition — collapse to φ → ψ → (φ→ψ→χ) → χ
+  have k_b_final := HasAxiomImplyS.implyS (S := S)
+    (φ := ψ)
+    (ψ := HasImp.imp
+      (HasImp.imp φ (HasImp.imp ψ χ))
+      (HasImp.imp ψ χ))
+    (χ := HasImp.imp
+      (HasImp.imp φ (HasImp.imp ψ χ)) χ)
+  have weak_k_b := ModusPonens.mp
+    (HasAxiomImplyK.implyK (S := S)
+      (φ := HasImp.imp
+        (HasImp.imp ψ
+          (HasImp.imp
+            (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ))
+              (HasImp.imp ψ χ))
+            (HasImp.imp
+              (HasImp.imp φ (HasImp.imp ψ χ)) χ)))
+        (HasImp.imp
+          (HasImp.imp ψ (HasImp.imp
+            (HasImp.imp φ (HasImp.imp ψ χ))
+            (HasImp.imp ψ χ)))
+          (HasImp.imp ψ
+            (HasImp.imp
+              (HasImp.imp φ (HasImp.imp ψ χ)) χ))))
+      (ψ := φ))
+    k_b_final
+  have k_a_outer := HasAxiomImplyS.implyS (S := S)
+    (φ := φ)
+    (ψ := HasImp.imp ψ
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ))
+          (HasImp.imp ψ χ))
+        (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ)) χ)))
+    (χ := HasImp.imp
+      (HasImp.imp ψ (HasImp.imp
+        (HasImp.imp φ (HasImp.imp ψ χ))
+        (HasImp.imp ψ χ)))
+      (HasImp.imp ψ
+        (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ)) χ)))
+  have step10_a := ModusPonens.mp k_a_outer weak_k_b
+  have step10 := ModusPonens.mp step10_a step9
+  have k_a_final := HasAxiomImplyS.implyS (S := S)
+    (φ := φ)
+    (ψ := HasImp.imp ψ (HasImp.imp
+      (HasImp.imp φ (HasImp.imp ψ χ))
+      (HasImp.imp ψ χ)))
+    (χ := HasImp.imp ψ
+      (HasImp.imp (HasImp.imp φ (HasImp.imp ψ χ)) χ))
+  have step11 := ModusPonens.mp k_a_final step10
+  exact ModusPonens.mp step11 a_b_abc_bc
+
+/-- Pairing combinator: `⊢ φ → ψ → ¬(φ → ¬ψ)`.
+    This is conjunction introduction where
+    `φ ∧ ψ := (φ → (ψ → ⊥)) → ⊥`. -/
+theorem pairing (φ ψ : F) :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp φ (HasImp.imp ψ
+        (HasImp.imp
+          (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+          HasBot.bot))) :=
+  @app2 F _ _ S _ _ φ ψ HasBot.bot
+
+/-- Double negation introduction: `⊢ φ → ¬¬φ`
+    where `¬φ := φ → ⊥`. -/
+theorem dni (φ : F) :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp φ
+        (HasImp.imp (HasImp.imp φ HasBot.bot)
+          HasBot.bot)) :=
+  @app1 F _ _ S _ _ (φ := φ) (ψ := HasBot.bot)
+
+/-- Combine two implications into conjunction:
+    from `⊢ P → A` and `⊢ P → B`,
+    derive `⊢ P → ¬(A → ¬B)`. -/
+theorem combine_imp_conj {P A₁ B₁ : F}
+    (hA : InferenceSystem.DerivableIn S
+      (HasImp.imp P A₁))
+    (hB : InferenceSystem.DerivableIn S
+      (HasImp.imp P B₁)) :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp P
+        (HasImp.imp
+          (HasImp.imp A₁ (HasImp.imp B₁ HasBot.bot))
+          HasBot.bot)) := by
+  have h1 := imp_trans hA (pairing A₁ B₁)
+  have s1 := HasAxiomImplyS.implyS (S := S)
+    (φ := P) (ψ := B₁)
+    (χ := HasImp.imp
+      (HasImp.imp A₁ (HasImp.imp B₁ HasBot.bot))
+      HasBot.bot)
+  exact ModusPonens.mp (ModusPonens.mp s1 h1) hB
+
+/-- Combine three implications into nested conjunction:
+    from `⊢ P → A`, `⊢ P → B`, `⊢ P → C`,
+    derive `⊢ P → ¬(A → ¬(¬(B → ¬C)))`. -/
+theorem combine_imp_conj_3 {P A₁ B₁ C₁ : F}
+    (hA : InferenceSystem.DerivableIn S
+      (HasImp.imp P A₁))
+    (hB : InferenceSystem.DerivableIn S
+      (HasImp.imp P B₁))
+    (hC : InferenceSystem.DerivableIn S
+      (HasImp.imp P C₁)) :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp P
+        (HasImp.imp
+          (HasImp.imp A₁
+            (HasImp.imp
+              (HasImp.imp
+                (HasImp.imp B₁
+                  (HasImp.imp C₁ HasBot.bot))
+                HasBot.bot)
+              HasBot.bot))
+          HasBot.bot)) :=
+  combine_imp_conj hA (combine_imp_conj hB hC)
+
+end Combinators
+
+end Cslib.Logic.Theorems.Combinators
diff --git a/Cslib/Foundations/Logic/Theorems/Modal/Basic.lean b/Cslib/Foundations/Logic/Theorems/Modal/Basic.lean
new file mode 100644
index 000000000..2ec38aa9e
--- /dev/null
+++ b/Cslib/Foundations/Logic/Theorems/Modal/Basic.lean
@@ -0,0 +1,203 @@
+/-
+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
+public import Cslib.Foundations.Logic.Theorems.Combinators
+public import Cslib.Foundations.Logic.Theorems.Propositional.Core
+public import Cslib.Foundations.Logic.Theorems.Propositional.Connectives
+
+/-! # K-Level Modal Theorems
+
+This module defines modal theorems that are derivable in any proof system
+satisfying `[ModalHilbert S]`, i.e., using only the K distribution axiom
+and necessitation rule (plus propositional axioms).
+
+All theorems are generic over `[ModalHilbert S]` with formula type `F`
+carrying `HasBot`, `HasImp`, and `HasBox` instances.
+
+## Main Results
+
+- `box_mono`: Box monotonicity (meta-rule): from `⊢ φ → ψ`, derive `⊢ □φ → □ψ`
+- `diamond_mono`: Diamond monotonicity (meta-rule): from `⊢ φ → ψ`, derive `⊢ ◇φ → ◇ψ`
+- `box_contrapose`: `⊢ □(φ → ψ) → □(¬ψ → ¬φ)` (box preserves contraposition)
+- `k_dist_diamond`: `⊢ □(φ → ψ) → (◇φ → ◇ψ)` (K distribution for diamond)
+- `modal_duality_neg`: `⊢ ◇¬φ → ¬□φ` (modal duality forward)
+- `modal_duality_neg_rev`: `⊢ ¬□φ → ◇¬φ` (modal duality reverse)
+- `box_iff_intro`: From `⊢ φ ↔ ψ`, derive `⊢ □φ ↔ □ψ`
+
+## Encoding
+
+- `¬φ = φ → ⊥`
+- `◇φ = ¬□¬φ = (□(φ → ⊥)) → ⊥`
+- `φ ∧ ψ = (φ → (ψ → ⊥)) → ⊥`
+- `φ ↔ ψ = (φ → ψ) ∧ (ψ → φ)`
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Theorems.Modal.Basic
+
+open Cslib.Logic
+open Cslib.Logic.Theorems.Combinators
+open Cslib.Logic.Theorems.Propositional.Core
+open Cslib.Logic.Theorems.Propositional.Connectives
+
+variable {F : Type*} [HasBot F] [HasImp F] [HasBox F]
+variable {S : Type*} [InferenceSystem S F]
+variable [ModalHilbert S (F := F)]
+
+section Basic
+
+/-- Box monotonicity (meta-rule): from `⊢ φ → ψ`, derive `⊢ □φ → □ψ`.
+
+Uses necessitation to box the implication, then K axiom to distribute. -/
+theorem box_mono {φ ψ : F}
+    (h : InferenceSystem.DerivableIn S (HasImp.imp φ ψ)) :
+    InferenceSystem.DerivableIn S (HasImp.imp (HasBox.box φ) (HasBox.box ψ)) := by
+  have box_h := Necessitation.nec h
+  have mk := HasAxiomK.K (S := S) (φ := φ) (ψ := ψ)
+  exact ModusPonens.mp mk box_h
+
+/-- Diamond monotonicity (meta-rule): from `⊢ φ → ψ`, derive `⊢ ◇φ → ◇ψ`.
+
+Derived via contraposition of box_mono applied to the negated implication.
+Since ◇φ = ¬□¬φ, from φ → ψ we get ¬ψ → ¬φ (contraposition),
+then □¬ψ → □¬φ (box_mono), then ¬□¬φ → ¬□¬ψ (contraposition again). -/
+theorem diamond_mono {φ ψ : F}
+    (h : InferenceSystem.DerivableIn S (HasImp.imp φ ψ)) :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+        (HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) HasBot.bot)) := by
+  have contra : InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp ψ HasBot.bot) (HasImp.imp φ HasBot.bot)) :=
+    contraposition h
+  have box_contra : InferenceSystem.DerivableIn S
+      (HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) (HasBox.box (HasImp.imp φ HasBot.bot))) :=
+    box_mono contra
+  exact contraposition box_contra
+
+/-- Box preserves contraposition: `⊢ □(φ → ψ) → □(¬ψ → ¬φ)`.
+
+Uses box_mono on the contrapose_imp theorem. -/
+theorem box_contrapose {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasBox.box (HasImp.imp φ ψ))
+        (HasBox.box (HasImp.imp (HasImp.imp ψ HasBot.bot) (HasImp.imp φ HasBot.bot)))) := by
+  -- contrapose_imp: (φ → ψ) → (¬ψ → ¬φ)
+  have contra_thm : InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp φ ψ)
+        (HasImp.imp (HasImp.imp ψ HasBot.bot)
+          (HasImp.imp φ HasBot.bot))) :=
+    contrapose_imp
+  exact box_mono contra_thm
+
+/-- K distribution for diamond: `⊢ □(φ → ψ) → (◇φ → ◇ψ)`.
+
+This is the valid form of "diamond monotonicity as implication".
+Note: `(φ → ψ) → (◇φ → ◇ψ)` is NOT valid; the implication must be boxed.
+
+Proof:
+1. box_contrapose: □(φ → ψ) → □(¬ψ → ¬φ)
+2. K axiom: □(¬ψ → ¬φ) → (□¬ψ → □¬φ)
+3. Compose: □(φ → ψ) → (□¬ψ → □¬φ)
+4. contrapose_imp on consequent: (□¬ψ → □¬φ) → (¬□¬φ → ¬□¬ψ)
+5. Compose: □(φ → ψ) → (◇φ → ◇ψ) -/
+theorem k_dist_diamond {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasBox.box (HasImp.imp φ ψ))
+        (HasImp.imp
+          (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+          (HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) HasBot.bot))) := by
+  -- Step 1: box_contrapose: □(φ → ψ) → □(¬ψ → ¬φ)
+  have box_contra := @box_contrapose F _ _ _ S _ _ (φ := φ) (ψ := ψ)
+  -- K axiom: □(¬ψ → ¬φ) → (□¬ψ → □¬φ)
+  have k_inst := HasAxiomK.K (S := S)
+    (φ := HasImp.imp ψ HasBot.bot)
+    (ψ := HasImp.imp φ HasBot.bot)
+  -- Compose: □(φ → ψ) → (□¬ψ → □¬φ)
+  have step1 := imp_trans box_contra k_inst
+  -- contrapose_imp: (□¬ψ → □¬φ) → (¬□¬φ → ¬□¬ψ)
+  have contra_cons : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) (HasBox.box (HasImp.imp φ HasBot.bot)))
+        (HasImp.imp
+          (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+          (HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) HasBot.bot))) :=
+    contrapose_imp
+  -- Compose: □(φ → ψ) → (◇φ → ◇ψ)
+  exact imp_trans step1 contra_cons
+
+/-- Modal duality (forward): `⊢ ◇¬φ → ¬□φ`.
+
+Since ◇¬φ = ¬□¬¬φ, we need ¬□¬¬φ → ¬□φ.
+From DNI (φ → ¬¬φ), apply box_mono (□φ → □¬¬φ),
+then contrapose (¬□¬¬φ → ¬□φ). -/
+theorem modal_duality_neg {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasBox.box (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot))
+          HasBot.bot)
+        (HasImp.imp (HasBox.box φ) HasBot.bot)) := by
+  -- DNI: φ → ¬¬φ
+  have dni_phi := dni (S := S) φ
+  -- box_mono: □φ → □¬¬φ
+  have forward := box_mono dni_phi
+  -- contrapose: ¬□¬¬φ → ¬□φ
+  exact contraposition forward
+
+/-- Modal duality (reverse): `⊢ ¬□φ → ◇¬φ`.
+
+Since ◇¬φ = ¬□¬¬φ, we need ¬□φ → ¬□¬¬φ.
+From DNE (¬¬φ → φ), apply box_mono (□¬¬φ → □φ),
+then contrapose (¬□φ → ¬□¬¬φ). -/
+theorem modal_duality_neg_rev {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasBox.box φ) HasBot.bot)
+        (HasImp.imp
+          (HasBox.box (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot))
+          HasBot.bot)) := by
+  -- DNE: ¬¬φ → φ
+  have dne_phi := @double_negation F _ _ S _ _ (φ := φ)
+  -- box_mono: □¬¬φ → □φ
+  have forward := box_mono dne_phi
+  -- contrapose: ¬□φ → ¬□¬¬φ
+  exact contraposition forward
+
+/-- Box preserves biconditionals: from `⊢ φ ↔ ψ`, derive `⊢ □φ ↔ □ψ`.
+
+Extracts both directions using lce_imp and rce_imp, applies box_mono
+to each, then combines with iff_intro. -/
+theorem box_iff_intro {φ ψ : F}
+    (h : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp φ ψ)
+          (HasImp.imp (HasImp.imp ψ φ) HasBot.bot))
+        HasBot.bot)) :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp (HasBox.box φ) (HasBox.box ψ))
+          (HasImp.imp (HasImp.imp (HasBox.box ψ) (HasBox.box φ)) HasBot.bot))
+        HasBot.bot) := by
+  -- Extract φ → ψ from biconditional
+  have ab := ModusPonens.mp lce_imp h
+  -- Extract ψ → φ from biconditional
+  have ba := ModusPonens.mp rce_imp h
+  -- Apply box_mono to both directions
+  have box_ab := box_mono ab
+  have box_ba := box_mono ba
+  -- Combine into biconditional
+  exact iff_intro box_ab box_ba
+
+end Basic
+
+end Cslib.Logic.Theorems.Modal.Basic
diff --git a/Cslib/Foundations/Logic/Theorems/Modal/S5.lean b/Cslib/Foundations/Logic/Theorems/Modal/S5.lean
new file mode 100644
index 000000000..28701a9eb
--- /dev/null
+++ b/Cslib/Foundations/Logic/Theorems/Modal/S5.lean
@@ -0,0 +1,533 @@
+/-
+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
+public import Cslib.Foundations.Logic.Theorems.Modal.Basic
+
+/-! # S5-Level Modal Theorems
+
+This module defines modal theorems that are derivable in any proof system
+satisfying `[ModalS5Hilbert S]`, i.e., using the K distribution axiom,
+necessitation rule, plus axioms T (□φ → φ), 4 (□φ → □□φ), and B (φ → □◇φ).
+
+All theorems are generic over `[ModalS5Hilbert S]` with formula type `F`
+carrying `HasBot`, `HasImp`, and `HasBox` instances.
+
+## Main Results
+
+### Axiom 5 Derivation
+- `diamond_4`: `⊢ ◇◇φ → ◇φ`
+- `axiom5_derived`: `⊢ ◇φ → □◇φ`
+- `axiom5_collapse_derived`: `⊢ ◇□φ → □φ`
+
+### Core S5 Theorems
+- `t_box_to_diamond`: `⊢ □φ → ◇φ`
+- `t_box_consistency`: `⊢ ¬□(φ ∧ ¬φ)`
+- `box_disj_intro`: `⊢ (□φ ∨ □ψ) → □(φ ∨ ψ)`
+- `box_conj_iff`: `⊢ □(φ ∧ ψ) ↔ (□φ ∧ □ψ)`
+- `diamond_disj_iff`: `⊢ ◇(φ ∨ ψ) ↔ (◇φ ∨ ◇ψ)`
+
+### S5 Collapse and Diamond-Box Theorems
+- `s5_diamond_box`: `⊢ ◇□φ ↔ □φ`
+- `s5_diamond_box_to_truth`: `⊢ ◇□φ → φ`
+
+### S4-Level Nested Modality Theorems
+- `s4_diamond_box_conj`: `⊢ (◇φ ∧ □ψ) → ◇(φ ∧ □ψ)`
+- `s4_box_diamond_box`: `⊢ □φ → □(◇□φ)`
+- `s4_diamond_box_diamond`: `⊢ ◇(□(◇φ)) ↔ ◇φ`
+- `s5_diamond_conj_diamond`: `⊢ ◇(φ ∧ ◇ψ) ↔ (◇φ ∧ ◇ψ)`
+
+## Encoding
+- `¬φ = φ → ⊥`; `◇φ = (□(φ → ⊥)) → ⊥`
+- `φ ∧ ψ = (φ → (ψ → ⊥)) → ⊥`; `φ ∨ ψ = (φ → ⊥) → ψ`
+- `φ ↔ ψ = ((φ → ψ) → ((ψ → φ) → ⊥)) → ⊥`
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Theorems.Modal.S5
+
+open Cslib.Logic
+open Cslib.Logic.Axioms
+open Cslib.Logic.Theorems.Combinators
+open Cslib.Logic.Theorems.Propositional.Core
+open Cslib.Logic.Theorems.Propositional.Connectives
+open Cslib.Logic.Theorems.Modal.Basic
+
+variable {F : Type*} [HasBot F] [HasImp F] [HasBox F]
+variable {S : Type*} [InferenceSystem S F]
+variable [ModalS5Hilbert S (F := F)]
+
+-- Abbreviations from Axioms: neg' φ = φ → ⊥, conj' φ ψ = ¬(φ → ¬ψ),
+-- disj' φ ψ = ¬φ → ψ. Local: diamond' φ = ¬□¬φ, iff' a b
+/-- Diamond as derived connective: `◇φ := ¬□¬φ`. -/
+abbrev diamond' (φ : F) : F :=
+  HasImp.imp (HasBox.box (neg' φ)) HasBot.bot
+/-- Biconditional as derived connective: `φ ↔ ψ := (φ → ψ) ∧ (ψ → φ)`. -/
+abbrev iff' (a b : F) : F :=
+  conj' (HasImp.imp a b) (HasImp.imp b a)
+
+section S5
+
+/-! ## Axiom 5 Derivation Block -/
+
+/-- Diamond 4: `⊢ ◇◇φ → ◇φ` (S4 characteristic for diamond).
+
+Derived from axiom 4 via contraposition and duality. -/
+theorem diamond_4 {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (diamond' (diamond' φ)) (diamond' φ)) := by
+  -- M4 for ¬φ: □¬φ → □□¬φ
+  have m4_neg := HasAxiom4.four (S := S) (φ := HasImp.imp φ HasBot.bot)
+  -- Contrapose: ¬□□¬φ → ¬□¬φ
+  have m4_contraposed := contraposition m4_neg
+  -- DNI on □¬φ: □¬φ → ¬¬□¬φ
+  have dni_box := dni (S := S) (HasBox.box (HasImp.imp φ HasBot.bot))
+  -- DNE on □¬φ: ¬¬□¬φ → □¬φ
+  have dne_box := @double_negation F _ _ S _ _
+    (φ := HasBox.box (HasImp.imp φ HasBot.bot))
+  -- Compose DNE + M4: ¬¬□¬φ → □□¬φ
+  have combined := imp_trans dne_box m4_neg
+  -- Necessitate and distribute: □¬¬□¬φ → □□□¬φ
+  have box_combined := Necessitation.nec combined
+  have mk_dist := HasAxiomK.K (S := S)
+    (φ := HasImp.imp (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot) HasBot.bot)
+    (ψ := HasBox.box (HasBox.box (HasImp.imp φ HasBot.bot)))
+  have distributed := ModusPonens.mp mk_dist box_combined
+  -- DNI on □¬φ necessitated and distributed: □□¬φ → □¬¬□¬φ
+  have box_dni := Necessitation.nec dni_box
+  have mk_dni := HasAxiomK.K (S := S)
+    (φ := HasBox.box (HasImp.imp φ HasBot.bot))
+    (ψ := HasImp.imp (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot) HasBot.bot)
+  have bridge := ModusPonens.mp mk_dni box_dni
+  -- Contrapose bridge: ¬□¬¬□¬φ → ¬□□¬φ
+  have bridge_neg := contraposition bridge
+  -- Compose: ◇◇φ = ¬□¬¬□¬φ → ¬□□¬φ → ¬□¬φ = ◇φ
+  exact imp_trans bridge_neg m4_contraposed
+
+/-- Axiom 5 derived: `⊢ ◇φ → □◇φ` (from B + diamond_4 + box_mono).
+
+1. B on ◇φ: ◇φ → □◇◇φ
+2. box_mono(diamond_4): □◇◇φ → □◇φ
+3. Compose: ◇φ → □◇φ -/
+theorem axiom5_derived {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (diamond' φ) (HasBox.box (diamond' φ))) := by
+  have mb_dia := HasAxiomB.B (S := S)
+    (φ := HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+  have d4 := @diamond_4 F _ _ _ S _ _ (φ := φ)
+  have box_d4 := box_mono d4
+  exact imp_trans mb_dia box_d4
+
+/-- Axiom 5 collapse: `⊢ ◇□φ → □φ` (from axiom5 + duality + DNE).
+
+Chain: ¬□φ →[duality_rev] ◇¬φ →[axiom5] □◇¬φ →[box_mono(duality)] □¬□φ
+Contrapose: ◇□φ = ¬□¬□φ → ¬¬□φ
+DNE: ¬¬□φ → □φ -/
+theorem axiom5_collapse_derived {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (diamond' (HasBox.box φ)) (HasBox.box φ)) := by
+  -- modal_duality_neg_rev: ¬□φ → ◇¬φ
+  have duality_rev := @modal_duality_neg_rev F _ _ _ S _ _ (φ := φ)
+  -- axiom5 on ¬φ: ◇¬φ → □◇¬φ
+  have ax5_negphi := @axiom5_derived F _ _ _ S _ _
+    (φ := HasImp.imp φ HasBot.bot)
+  -- modal_duality_neg: ◇¬φ → ¬□φ
+  have duality_fwd := @modal_duality_neg F _ _ _ S _ _ (φ := φ)
+  -- box_mono on duality_fwd: □◇¬φ → □¬□φ
+  have box_duality_fwd := box_mono duality_fwd
+  -- Chain: ¬□φ → ◇¬φ → □◇¬φ → □¬□φ
+  have chain1 := imp_trans duality_rev ax5_negphi
+  have chain2 := imp_trans chain1 box_duality_fwd
+  -- chain2: (□φ→⊥) → □(□φ→⊥)
+  -- Contrapose: ◇□φ → ¬¬□φ
+  have contra_chain := contraposition chain2
+  -- DNE on □φ
+  have dne_boxphi := @double_negation F _ _ S _ _ (φ := HasBox.box φ)
+  -- Compose: ◇□φ → ¬¬□φ → □φ
+  exact imp_trans contra_chain dne_boxphi
+
+/-! ## Core S5 Theorems -/
+
+/-- T-Box-Diamond: `⊢ □φ → ◇φ` (necessary implies possible). -/
+theorem t_box_to_diamond {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (HasBox.box φ) (diamond' φ)) := by
+  -- T: □φ → φ
+  have mt_a := HasAxiomT.T (S := S) (φ := φ)
+  -- T on ¬φ: □¬φ → ¬φ
+  have mt_neg_a := HasAxiomT.T (S := S) (φ := HasImp.imp φ HasBot.bot)
+  -- RAA: φ → (¬φ → ⊥)
+  have raa_inst := @raa F _ _ S _ _ (φ := φ) (ψ := HasBot.bot)
+  -- Compose □φ → φ → (¬φ → ⊥)
+  have comp1 := imp_trans mt_a raa_inst
+  -- b_combinator: (¬φ→⊥) → (□¬φ→¬φ) → (□¬φ→⊥)
+  have step1 : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+        (HasImp.imp
+          (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) (HasImp.imp φ HasBot.bot))
+          (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot))) :=
+    b_combinator
+  -- flip and apply T on ¬φ
+  have b_flipped := ModusPonens.mp
+    (@flip F _ _ S _ _
+      (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+      (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) (HasImp.imp φ HasBot.bot))
+      (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot))
+    step1
+  have step2 := ModusPonens.mp b_flipped mt_neg_a
+  -- step2: (¬φ→⊥) → (□¬φ→⊥)
+  -- b_combinator to compose
+  have b_outer : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+          (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot))
+        (HasImp.imp
+          (HasImp.imp (HasBox.box φ)
+            (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot))
+          (HasImp.imp (HasBox.box φ)
+            (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot))
+              HasBot.bot)))) :=
+    b_combinator
+  have step3 := ModusPonens.mp b_outer step2
+  exact ModusPonens.mp step3 comp1
+
+/-- T-Box-Consistency: `⊢ ¬□(φ ∧ ¬φ)`. -/
+theorem t_box_consistency {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasBox.box
+          (HasImp.imp
+            (HasImp.imp φ
+              (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot))
+            HasBot.bot))
+        HasBot.bot) := by
+  have mt := HasAxiomT.T (S := S)
+    (φ := HasImp.imp
+      (HasImp.imp φ (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot))
+      HasBot.bot)
+  have dni_phi := dni (S := S) φ
+  have dni_impl := dni (S := S)
+    (HasImp.imp φ (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot))
+  have conj_to_bot := ModusPonens.mp dni_impl dni_phi
+  exact imp_trans mt conj_to_bot
+
+/-- Box-Disjunction Introduction: `⊢ (□φ ∨ □ψ) → □(φ ∨ ψ)`. -/
+theorem box_disj_intro {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp (HasBox.box φ) HasBot.bot) (HasBox.box ψ))
+        (HasBox.box (HasImp.imp (HasImp.imp φ HasBot.bot) ψ))) := by
+  have raa_inst := @raa F _ _ S _ _ (φ := φ) (ψ := ψ)
+  have box_a_case := box_mono raa_inst
+  have weak_b := HasAxiomImplyK.implyK (S := S)
+    (φ := ψ) (ψ := HasImp.imp φ HasBot.bot)
+  have box_b_case := box_mono weak_b
+  have cm := @classical_merge F _ _ S _ _
+    (φ := HasBox.box φ)
+    (ψ := HasBox.box (HasImp.imp (HasImp.imp φ HasBot.bot) ψ))
+  have step1 := ModusPonens.mp cm box_a_case
+  have bc : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasBox.box ψ)
+          (HasBox.box (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)))
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp (HasBox.box φ) HasBot.bot)
+            (HasBox.box ψ))
+          (HasImp.imp (HasImp.imp (HasBox.box φ) HasBot.bot)
+            (HasBox.box
+              (HasImp.imp (HasImp.imp φ HasBot.bot) ψ))))) :=
+    b_combinator
+  have neg_box_case := ModusPonens.mp bc box_b_case
+  exact imp_trans neg_box_case step1
+
+/-- Box-Conjunction Biconditional: `⊢ □(φ ∧ ψ) ↔ (□φ ∧ □ψ)`. -/
+theorem box_conj_iff {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (iff' (HasBox.box (conj' φ ψ)) (conj' (HasBox.box φ) (HasBox.box ψ))) := by
+  -- Forward: □(φ ∧ ψ) → (□φ ∧ □ψ)
+  have lce_a := @lce_imp F _ _ S _ _ (φ := φ) (ψ := ψ)
+  have box_a := box_mono lce_a
+  have rce_b := @rce_imp F _ _ S _ _ (φ := φ) (ψ := ψ)
+  have box_b := box_mono rce_b
+  have forward := combine_imp_conj box_a box_b
+  -- Backward: (□φ ∧ □ψ) → □(φ ∧ ψ)
+  have pair := pairing (S := S) φ ψ
+  have step1 := box_mono pair
+  have modal_k := HasAxiomK.K (S := S) (φ := ψ)
+    (ψ := HasImp.imp (HasImp.imp φ (HasImp.imp ψ HasBot.bot)) HasBot.bot)
+  have comp1 := imp_trans step1 modal_k
+  have lce_box := @lce_imp F _ _ S _ _ (φ := HasBox.box φ) (ψ := HasBox.box ψ)
+  have rce_box := @rce_imp F _ _ S _ _ (φ := HasBox.box φ) (ψ := HasBox.box ψ)
+  have b1 : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasBox.box φ)
+          (HasImp.imp (HasBox.box ψ)
+            (HasBox.box (HasImp.imp
+              (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+              HasBot.bot))))
+        (HasImp.imp
+          (HasImp.imp
+            (HasImp.imp
+              (HasImp.imp (HasBox.box φ)
+                (HasImp.imp (HasBox.box ψ) HasBot.bot))
+              HasBot.bot)
+            (HasBox.box φ))
+          (HasImp.imp
+            (HasImp.imp
+              (HasImp.imp (HasBox.box φ)
+                (HasImp.imp (HasBox.box ψ) HasBot.bot))
+              HasBot.bot)
+            (HasImp.imp (HasBox.box ψ)
+              (HasBox.box (HasImp.imp
+                (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+                HasBot.bot)))))) :=
+    b_combinator
+  have step2 := ModusPonens.mp b1 comp1
+  have step3 := ModusPonens.mp step2 lce_box
+  have s_ax := HasAxiomImplyS.implyS (S := S)
+    (φ := HasImp.imp (HasImp.imp (HasBox.box φ) (HasImp.imp (HasBox.box ψ) HasBot.bot)) HasBot.bot)
+    (ψ := HasBox.box ψ)
+    (χ := HasBox.box (HasImp.imp (HasImp.imp φ (HasImp.imp ψ HasBot.bot)) HasBot.bot))
+  have step4 := ModusPonens.mp s_ax step3
+  have backward := ModusPonens.mp step4 rce_box
+  exact iff_intro forward backward
+
+/-- Diamond-Disjunction Biconditional: `⊢ ◇(φ ∨ ψ) ↔ (◇φ ∨ ◇ψ)`. -/
+theorem diamond_disj_iff {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (iff' (diamond' (disj' φ ψ)) (disj' (diamond' φ) (diamond' ψ))) := by
+  -- Forward: ◇(φ∨ψ) → (◇φ ∨ ◇ψ)
+  -- Get De Morgan biconditionals
+  have demorgan_disj := @demorgan_disj_neg F _ _ S _ _ (φ := φ) (ψ := ψ)
+  -- Extract backward: (¬φ ∧ ¬ψ) → ¬(φ ∨ ψ)
+  have demorgan_back := ModusPonens.mp rce_imp demorgan_disj
+  -- box_iff_intro on demorgan: □¬(φ∨ψ) ↔ □(¬φ∧¬ψ)
+  have box_demorgan := box_iff_intro demorgan_disj
+  -- Extract backward: □(¬φ∧¬ψ) → □¬(φ∨ψ)
+  have box_demorgan_back := ModusPonens.mp rce_imp box_demorgan
+  -- box_conj_iff for ¬φ, ¬ψ
+  have box_conj_neg := @box_conj_iff F _ _ _ S _ _
+    (φ := HasImp.imp φ HasBot.bot) (ψ := HasImp.imp ψ HasBot.bot)
+  -- Extract backward: (□¬φ ∧ □¬ψ) → □(¬φ∧¬ψ)
+  have conj_box_to_box_conj := ModusPonens.mp rce_imp box_conj_neg
+  -- Compose: (□¬φ ∧ □¬ψ) → □¬(φ∨ψ)
+  have conj_box_to_or_box := imp_trans conj_box_to_box_conj box_demorgan_back
+  -- Contrapose: ◇(φ∨ψ) → ¬(□¬φ ∧ □¬ψ)
+  have neg_box_or_to_neg_conj := contraposition conj_box_to_or_box
+  -- De Morgan forward: ¬(□¬φ ∧ □¬ψ) → (◇φ ∨ ◇ψ)
+  have demorgan_conj_fwd := @demorgan_conj_neg_forward F _ _ S _ _
+    (φ := HasBox.box (HasImp.imp φ HasBot.bot))
+    (ψ := HasBox.box (HasImp.imp ψ HasBot.bot))
+  have forward := imp_trans neg_box_or_to_neg_conj demorgan_conj_fwd
+  -- Backward: (◇φ ∨ ◇ψ) → ◇(φ∨ψ)
+  have demorgan_conj_bwd := @demorgan_conj_neg_backward F _ _ S _ _
+    (φ := HasBox.box (HasImp.imp φ HasBot.bot))
+    (ψ := HasBox.box (HasImp.imp ψ HasBot.bot))
+  have box_conj_to_conj_box := ModusPonens.mp lce_imp box_conj_neg
+  have neg_conj_to_neg_box := contraposition box_conj_to_conj_box
+  have box_demorgan_fwd := ModusPonens.mp lce_imp box_demorgan
+  have neg_box_conj_to_neg_box_or := contraposition box_demorgan_fwd
+  have step1 := imp_trans demorgan_conj_bwd neg_conj_to_neg_box
+  have backward := imp_trans step1 neg_box_conj_to_neg_box_or
+  exact iff_intro forward backward
+
+/-! ## S5 Collapse and Diamond-Box Theorems -/
+
+/-- S5-Diamond-Box Collapse: `⊢ ◇□φ ↔ □φ`. -/
+theorem s5_diamond_box {φ : F} :
+    InferenceSystem.DerivableIn S
+      (iff' (diamond' (HasBox.box φ)) (HasBox.box φ)) := by
+  have forward := @axiom5_collapse_derived F _ _ _ S _ _ (φ := φ)
+  have m4_a := HasAxiom4.four (S := S) (φ := φ)
+  have box_box_to_diamond := @t_box_to_diamond F _ _ _ S _ _ (φ := HasBox.box φ)
+  have backward := imp_trans m4_a box_box_to_diamond
+  exact iff_intro forward backward
+
+/-- S5-Diamond-Box-to-Truth: `⊢ ◇□φ → φ`. -/
+theorem s5_diamond_box_to_truth {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (diamond' (HasBox.box φ)) φ) := by
+  have h1 := @axiom5_collapse_derived F _ _ _ S _ _ (φ := φ)
+  have h2 := HasAxiomT.T (S := S) (φ := φ)
+  exact imp_trans h1 h2
+
+/-! ## S4-Level Nested Modality Theorems -/
+
+/-- S4-Diamond-Box-Conjunction: `⊢ (◇φ ∧ □ψ) → ◇(φ ∧ □ψ)`. -/
+theorem s4_diamond_box_conj {φ ψ : F} :
+    let conjPhiBoxPsi := conj' φ (HasBox.box ψ)
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (conj' (diamond' φ) (HasBox.box ψ)) (diamond' conjPhiBoxPsi)) := by
+  -- pairing: φ → □ψ → (φ ∧ □ψ)
+  have pair := pairing (S := S) φ (HasBox.box ψ)
+  -- flip: □ψ → (φ → (φ ∧ □ψ))
+  have flipped := ModusPonens.mp
+    (@flip F _ _ S _ _ φ (HasBox.box ψ)
+      (HasImp.imp (HasImp.imp φ (HasImp.imp (HasBox.box ψ) HasBot.bot)) HasBot.bot))
+    pair
+  -- 4: □ψ → □□ψ
+  have m4_b := HasAxiom4.four (S := S) (φ := ψ)
+  -- box_mono: □□ψ → □(φ → (φ ∧ □ψ))
+  have box_flipped := box_mono flipped
+  -- Compose: □ψ → □(φ → (φ ∧ □ψ))
+  have box_b_to_box_imp := imp_trans m4_b box_flipped
+  -- k_dist_diamond: □(φ → (φ ∧ □ψ)) → (◇φ → ◇(φ ∧ □ψ))
+  have k_dist := @k_dist_diamond F _ _ _ S _ _
+    (φ := φ)
+    (ψ := HasImp.imp (HasImp.imp φ (HasImp.imp (HasBox.box ψ) HasBot.bot)) HasBot.bot)
+  -- Compose: □ψ → (◇φ → ◇(φ ∧ □ψ))
+  have box_b_to_diamond_imp := imp_trans box_b_to_box_imp k_dist
+  -- Extract □ψ: (◇φ ∧ □ψ) → □ψ
+  have rce_conj := @rce_imp F _ _ S _ _
+    (φ := HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+    (ψ := HasBox.box ψ)
+  -- Extract ◇φ: (◇φ ∧ □ψ) → ◇φ
+  have lce_conj := @lce_imp F _ _ S _ _
+    (φ := HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+    (ψ := HasBox.box ψ)
+  -- Compose: (◇φ ∧ □ψ) → □ψ → (◇φ → ◇(φ ∧ □ψ))
+  have conj_to_box_b := imp_trans rce_conj box_b_to_diamond_imp
+  -- Use S axiom
+  have s_ax := HasAxiomImplyS.implyS (S := S)
+    (φ := HasImp.imp
+      (HasImp.imp
+        (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+        (HasImp.imp (HasBox.box ψ) HasBot.bot))
+      HasBot.bot)
+    (ψ := HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+    (χ := HasImp.imp
+      (HasBox.box
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ (HasImp.imp (HasBox.box ψ) HasBot.bot)) HasBot.bot)
+          HasBot.bot))
+      HasBot.bot)
+  have step1 := ModusPonens.mp s_ax conj_to_box_b
+  exact ModusPonens.mp step1 lce_conj
+
+/-- S4-Box-Diamond-Box: `⊢ □φ → □(◇□φ)`.
+
+Direct from axiom B applied to □φ. -/
+theorem s4_box_diamond_box {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (HasBox.box φ) (HasBox.box (diamond' (HasBox.box φ)))) :=
+  HasAxiomB.B (S := S) (φ := HasBox.box φ)
+
+/-- S4-Diamond-Box-Diamond: `⊢ ◇(□(◇φ)) ↔ ◇φ`. -/
+theorem s4_diamond_box_diamond {φ : F} :
+    InferenceSystem.DerivableIn S
+      (iff' (diamond' (HasBox.box (diamond' φ))) (diamond' φ)) := by
+  -- Forward: ◇□◇φ → ◇φ
+  -- axiom5_collapse on ◇φ: ◇□◇φ → □◇φ
+  have m5c := @axiom5_collapse_derived F _ _ _ S _ _
+    (φ := HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+  -- T on ◇φ: □◇φ → ◇φ
+  have t_dia := HasAxiomT.T (S := S)
+    (φ := HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+  have forward := imp_trans m5c t_dia
+  -- Backward: ◇φ → ◇□◇φ
+  -- axiom5 on φ: ◇φ → □◇φ
+  have ax5_a := @axiom5_derived F _ _ _ S _ _ (φ := φ)
+  -- 4 on ◇φ: □◇φ → □□◇φ
+  have m4_dia := HasAxiom4.four (S := S)
+    (φ := HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+  -- t_box_to_diamond on □◇φ: □□◇φ → ◇□◇φ
+  have box_box_to_dia := @t_box_to_diamond F _ _ _ S _ _
+    (φ := HasBox.box (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot))
+  have step1 := imp_trans ax5_a m4_dia
+  have backward := imp_trans step1 box_box_to_dia
+  exact iff_intro forward backward
+
+/-- S5-Diamond-Conjunction-Diamond: `⊢ ◇(φ ∧ ◇ψ) ↔ (◇φ ∧ ◇ψ)`. -/
+theorem s5_diamond_conj_diamond {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (iff' (diamond' (conj' φ (diamond' ψ))) (conj' (diamond' φ) (diamond' ψ))) := by
+  -- Forward: ◇(φ ∧ ◇ψ) → (◇φ ∧ ◇ψ)
+  -- lce: (φ ∧ ◇ψ) → φ
+  have lce := @lce_imp F _ _ S _ _
+    (φ := φ)
+    (ψ := HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) HasBot.bot)
+  have dia_lce := diamond_mono lce
+  -- rce: (φ ∧ ◇ψ) → ◇ψ
+  have rce := @rce_imp F _ _ S _ _
+    (φ := φ)
+    (ψ := HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) HasBot.bot)
+  have dia_rce := diamond_mono rce
+  -- diamond_4: ◇◇ψ → ◇ψ
+  have dia_dia_to_dia := @diamond_4 F _ _ _ S _ _ (φ := ψ)
+  -- Compose: ◇(φ ∧ ◇ψ) → ◇ψ
+  have dia_conj_to_dia_b := imp_trans dia_rce dia_dia_to_dia
+  -- combine: ◇(φ ∧ ◇ψ) → (◇φ ∧ ◇ψ)
+  have forward := combine_imp_conj dia_lce dia_conj_to_dia_b
+  -- Backward: (◇φ ∧ ◇ψ) → ◇(φ ∧ ◇ψ)
+  -- axiom5 on ψ: ◇ψ → □◇ψ
+  have ax5_b := @axiom5_derived F _ _ _ S _ _ (φ := ψ)
+  -- pairing: φ → ◇ψ → (φ ∧ ◇ψ)
+  have pair := pairing (S := S) φ
+    (HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) HasBot.bot)
+  -- flip: ◇ψ → (φ → (φ ∧ ◇ψ))
+  have flipped := ModusPonens.mp
+    (@flip F _ _ S _ _ φ
+      (HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) HasBot.bot)
+      (HasImp.imp
+        (HasImp.imp φ
+          (HasImp.imp (HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) HasBot.bot) HasBot.bot))
+        HasBot.bot))
+    pair
+  -- box_mono: □◇ψ → □(φ → (φ ∧ ◇ψ))
+  have box_flipped := box_mono flipped
+  -- Compose: ◇ψ → □(φ → (φ ∧ ◇ψ))
+  have dia_b_to_box_imp := imp_trans ax5_b box_flipped
+  -- k_dist_diamond: □(φ → (φ ∧ ◇ψ)) → (◇φ → ◇(φ ∧ ◇ψ))
+  have k_dist := @k_dist_diamond F _ _ _ S _ _
+    (φ := φ)
+    (ψ := HasImp.imp
+      (HasImp.imp φ
+        (HasImp.imp (HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) HasBot.bot) HasBot.bot))
+      HasBot.bot)
+  -- Compose: ◇ψ → (◇φ → ◇(φ ∧ ◇ψ))
+  have dia_b_to_imp := imp_trans dia_b_to_box_imp k_dist
+  -- Extract ◇ψ: (◇φ ∧ ◇ψ) → ◇ψ
+  have rce_conj := @rce_imp F _ _ S _ _
+    (φ := HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+    (ψ := HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) HasBot.bot)
+  -- Extract ◇φ: (◇φ ∧ ◇ψ) → ◇φ
+  have lce_conj := @lce_imp F _ _ S _ _
+    (φ := HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+    (ψ := HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) HasBot.bot)
+  -- Compose: (◇φ ∧ ◇ψ) → ◇ψ → (◇φ → ◇(φ ∧ ◇ψ))
+  have conj_to_dia_b := imp_trans rce_conj dia_b_to_imp
+  -- Use S axiom
+  have s_ax := HasAxiomImplyS.implyS (S := S)
+    (φ := HasImp.imp
+      (HasImp.imp
+        (HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+        (HasImp.imp (HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot)) HasBot.bot) HasBot.bot))
+      HasBot.bot)
+    (ψ := HasImp.imp (HasBox.box (HasImp.imp φ HasBot.bot)) HasBot.bot)
+    (χ := HasImp.imp
+      (HasBox.box
+        (HasImp.imp
+          (HasImp.imp
+            (HasImp.imp φ
+              (HasImp.imp
+                (HasImp.imp (HasBox.box (HasImp.imp ψ HasBot.bot))
+                  HasBot.bot)
+                HasBot.bot))
+            HasBot.bot)
+          HasBot.bot))
+      HasBot.bot)
+  have step1 := ModusPonens.mp s_ax conj_to_dia_b
+  have backward := ModusPonens.mp step1 lce_conj
+  exact iff_intro forward backward
+
+end S5
+
+end Cslib.Logic.Theorems.Modal.S5
diff --git a/Cslib/Foundations/Logic/Theorems/Propositional/Connectives.lean b/Cslib/Foundations/Logic/Theorems/Propositional/Connectives.lean
new file mode 100644
index 000000000..ab1d7238c
--- /dev/null
+++ b/Cslib/Foundations/Logic/Theorems/Propositional/Connectives.lean
@@ -0,0 +1,536 @@
+/-
+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
+public import Cslib.Foundations.Logic.Theorems.Propositional.Core
+
+/-! # Derived Connective Theorems
+
+Classical merge, iff introduction, contraposition, and De Morgan laws
+for the Hilbert-style proof system.
+
+All theorems are generic over `[PropositionalHilbert S]`.
+
+## Main Results
+
+- `classical_merge`: `(P → Q) → ((¬P → Q) → Q)` (DT-free)
+- `iff_intro`: From `⊢ A → B` and `⊢ B → A`, derive `⊢ A ↔ B`
+- `contrapose_imp`: `(A → B) → (¬B → ¬A)`
+- `contraposition`: From `⊢ A → B`, derive `⊢ ¬B → ¬A`
+- `contrapose_iff`: From `⊢ A ↔ B`, derive `⊢ ¬A ↔ ¬B`
+- `demorgan_conj_neg_forward`: `¬(A ∧ B) → (¬A ∨ ¬B)`
+- `demorgan_conj_neg_backward`: `(¬A ∨ ¬B) → ¬(A ∧ B)`
+- `demorgan_disj_neg_forward`: `¬(A ∨ B) → (¬A ∧ ¬B)`
+- `demorgan_disj_neg_backward`: `(¬A ∧ ¬B) → ¬(A ∨ B)`
+
+## Encoding
+
+- `¬φ = φ → ⊥`
+- `φ ∧ ψ = (φ → (ψ → ⊥)) → ⊥`
+- `φ ∨ ψ = (φ → ⊥) → ψ`
+- `φ ↔ ψ = (φ → ψ) ∧ (ψ → φ)`
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Theorems.Propositional.Connectives
+
+open Cslib.Logic
+open Cslib.Logic.Theorems.Combinators
+open Cslib.Logic.Theorems.Propositional.Core
+
+variable {F : Type*} [HasBot F] [HasImp F]
+variable {S : Type*} [InferenceSystem S F]
+variable [PropositionalHilbert S (F := F)]
+
+section Connectives
+
+/-- Contraposition (implication form):
+    `⊢ (φ → ψ) → (¬ψ → ¬φ)`. -/
+theorem contrapose_imp {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp φ ψ)
+        (HasImp.imp (HasImp.imp ψ HasBot.bot)
+          (HasImp.imp φ HasBot.bot))) := by
+  -- b: (ψ→⊥) → (φ→ψ) → (φ→⊥)
+  have bc : InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp ψ HasBot.bot)
+        (HasImp.imp (HasImp.imp φ ψ)
+          (HasImp.imp φ HasBot.bot))) :=
+    b_combinator
+  -- flip: (φ→ψ) → (ψ→⊥) → (φ→⊥)
+  exact ModusPonens.mp
+    (@flip F _ _ S _ _
+      (HasImp.imp ψ HasBot.bot)
+      (HasImp.imp φ ψ)
+      (HasImp.imp φ HasBot.bot))
+    bc
+
+/-- Contraposition (meta): from `⊢ φ → ψ`,
+    derive `⊢ ¬ψ → ¬φ`. -/
+theorem contraposition {φ ψ : F}
+    (h : InferenceSystem.DerivableIn S
+      (HasImp.imp φ ψ)) :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp ψ HasBot.bot)
+        (HasImp.imp φ HasBot.bot)) :=
+  ModusPonens.mp contrapose_imp h
+
+/-- Classical merge (DT-free):
+    `⊢ (P → Q) → ((¬P → Q) → Q)`.
+
+    Proof: Contrapose both premises to get
+    (¬Q → ¬P) and (¬Q → ¬¬P), derive ¬¬Q via
+    contradiction, then apply DNE. -/
+theorem classical_merge {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp φ ψ)
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)
+          ψ)) := by
+  -- Strategy: use Peirce(ψ,⊥): ((ψ→⊥)→ψ)→ψ
+  -- We need: (φ→ψ) → ((¬φ→ψ) → ((ψ→⊥)→ψ))
+  -- From (φ→ψ), contrapose: (¬ψ→¬φ)
+  -- From (¬φ→ψ) and (¬ψ→¬φ), compose: (¬ψ→ψ)
+  -- This is: ((ψ→⊥)→ψ), which feeds Peirce.
+  have peirce_inst := HasAxiomPeirce.peirce (S := S)
+    (φ := ψ) (ψ := HasBot.bot)
+  -- Build: (φ→ψ) → ((¬φ→ψ) → ((ψ→⊥)→ψ))
+  -- Step 1: (φ→ψ) gives (¬ψ→¬φ) by contrapose_imp
+  -- Step 2: (¬ψ→¬φ) and (¬φ→ψ) give (¬ψ→ψ) by imp_trans
+  -- So we need: (¬ψ→¬φ) → ((¬φ→ψ) → ((ψ→⊥)→ψ))
+
+  -- b: (¬φ→ψ) → ((ψ→⊥)→¬φ) → ((ψ→⊥)→ψ)
+  -- flip b: ((ψ→⊥)→¬φ) → ((¬φ→ψ) → ((ψ→⊥)→ψ))
+  -- Then compose with contrapose_imp(φ,ψ)
+
+  -- Actually, simpler route using imp_trans:
+  -- b: (¬φ→ψ) → ((ψ→⊥)→¬φ) → ((ψ→⊥)→ψ)
+  have bc : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp ψ HasBot.bot)
+            (HasImp.imp φ HasBot.bot))
+          (HasImp.imp (HasImp.imp ψ HasBot.bot) ψ))) :=
+    b_combinator
+  -- flip: (¬ψ→¬φ) → ((¬φ→ψ) → ((ψ→⊥)→ψ))
+  have flip_bc := ModusPonens.mp
+    (@flip F _ _ S _ _
+      (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)
+      (HasImp.imp (HasImp.imp ψ HasBot.bot)
+        (HasImp.imp φ HasBot.bot))
+      (HasImp.imp (HasImp.imp ψ HasBot.bot) ψ))
+    bc
+  -- Compose: (φ→ψ) → contrapose → (¬ψ→¬φ) →
+  --   flip_bc → ((¬φ→ψ) → ((ψ→⊥)→ψ))
+  have step1 := imp_trans
+    (@contrapose_imp F _ _ S _ _ (φ := φ) (ψ := ψ))
+    flip_bc
+  -- step1: (φ→ψ) → ((¬φ→ψ) → ((ψ→⊥)→ψ))
+
+  -- Now compose inner part with Peirce:
+  -- b: (((ψ→⊥)→ψ)→ψ) → ((¬φ→ψ)→((ψ→⊥)→ψ)) →
+  --    ((¬φ→ψ)→ψ)
+  have bc2 : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp ψ HasBot.bot) ψ) ψ)
+        (HasImp.imp
+          (HasImp.imp
+            (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)
+            (HasImp.imp (HasImp.imp ψ HasBot.bot) ψ))
+          (HasImp.imp
+            (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)
+            ψ))) :=
+    b_combinator
+  have step2 := ModusPonens.mp bc2 peirce_inst
+  -- step2: ((¬φ→ψ)→((ψ→⊥)→ψ)) → ((¬φ→ψ)→ψ)
+
+  -- Compose step1 with step2 at (φ→ψ) level:
+  -- b: ((¬φ→ψ)→((ψ→⊥)→ψ)) → X → ((¬φ→ψ)→ψ)
+  -- But we need to compose step1 and step2 differently:
+  -- step1: (φ→ψ) → ((¬φ→ψ) → ((ψ→⊥)→ψ))
+  -- step2: ((¬φ→ψ) → ((ψ→⊥)→ψ)) → ((¬φ→ψ)→ψ)
+  -- Compose: (φ→ψ) → ((¬φ→ψ)→ψ)
+  exact imp_trans step1 step2
+
+/-- Iff introduction: from `⊢ φ → ψ` and `⊢ ψ → φ`,
+    derive `⊢ (φ → ψ) ∧ (ψ → φ)`.
+    Uses pairing to build the conjunction. -/
+theorem iff_intro {φ ψ : F}
+    (h1 : InferenceSystem.DerivableIn S
+      (HasImp.imp φ ψ))
+    (h2 : InferenceSystem.DerivableIn S
+      (HasImp.imp ψ φ)) :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp φ ψ)
+          (HasImp.imp (HasImp.imp ψ φ) HasBot.bot))
+        HasBot.bot) := by
+  have pair_inst := pairing (S := S) (HasImp.imp φ ψ) (HasImp.imp ψ φ)
+  have step1 := ModusPonens.mp pair_inst h1
+  exact ModusPonens.mp step1 h2
+
+/-- Contrapose iff: from `⊢ φ ↔ ψ`, derive `⊢ ¬φ ↔ ¬ψ`.
+    Uses lce_imp/rce_imp to extract directions. -/
+theorem contrapose_iff {φ ψ : F}
+    (h : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp φ ψ)
+          (HasImp.imp (HasImp.imp ψ φ) HasBot.bot))
+        HasBot.bot)) :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot)
+            (HasImp.imp ψ HasBot.bot))
+          (HasImp.imp
+            (HasImp.imp (HasImp.imp ψ HasBot.bot)
+              (HasImp.imp φ HasBot.bot))
+            HasBot.bot))
+        HasBot.bot) := by
+  -- Extract φ → ψ
+  have ab := ModusPonens.mp lce_imp h
+  -- Extract ψ → φ
+  have ba := ModusPonens.mp rce_imp h
+  -- Contrapose both
+  have nb_na := contraposition ab
+  have na_nb := contraposition ba
+  -- Combine into biconditional
+  exact iff_intro na_nb nb_na
+
+/-- Iff neg intro: from `⊢ ¬φ → ¬ψ` and `⊢ ¬ψ → ¬φ`,
+    derive `⊢ ¬φ ↔ ¬ψ`. -/
+theorem iff_neg_intro {φ ψ : F}
+    (h1 : InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp φ HasBot.bot)
+        (HasImp.imp ψ HasBot.bot)))
+    (h2 : InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp ψ HasBot.bot)
+        (HasImp.imp φ HasBot.bot))) :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot)
+            (HasImp.imp ψ HasBot.bot))
+          (HasImp.imp
+            (HasImp.imp (HasImp.imp ψ HasBot.bot)
+              (HasImp.imp φ HasBot.bot))
+            HasBot.bot))
+        HasBot.bot) :=
+  iff_intro h1 h2
+
+/-- De Morgan 1 forward: `⊢ ¬(φ ∧ ψ) → (¬φ ∨ ¬ψ)`.
+    i.e., `¬¬(φ → ¬ψ) → (¬¬φ → ¬ψ)`.
+    Use DNE on (φ→¬ψ) then compose with DNE on φ. -/
+theorem demorgan_conj_neg_forward {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp
+            (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+            HasBot.bot)
+          HasBot.bot)
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+          (HasImp.imp ψ HasBot.bot))) := by
+  -- DNE on (φ→¬ψ): ¬¬(φ→¬ψ) → (φ→¬ψ)
+  have dne_inner := @double_negation F _ _ S _ _
+    (φ := HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+  -- DNE on φ: ¬¬φ → φ
+  have dne_a := @double_negation F _ _ S _ _ (φ := φ)
+  -- (φ→¬ψ) → (¬¬φ → ¬ψ) by composing with DNE:
+  -- b: (φ→¬ψ) → ((¬¬φ→φ) → (¬¬φ→¬ψ))
+  -- flip: (¬¬φ→φ) → ((φ→¬ψ) → (¬¬φ→¬ψ))
+  -- Apply dne_a: (φ→¬ψ) → (¬¬φ→¬ψ)
+  have bc : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+        (HasImp.imp
+          (HasImp.imp
+            (HasImp.imp (HasImp.imp φ HasBot.bot)
+              HasBot.bot)
+            φ)
+          (HasImp.imp
+            (HasImp.imp (HasImp.imp φ HasBot.bot)
+              HasBot.bot)
+            (HasImp.imp ψ HasBot.bot)))) :=
+    b_combinator
+  have flip_bc := ModusPonens.mp
+    (@flip F _ _ S _ _
+      (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+        φ)
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+        (HasImp.imp ψ HasBot.bot)))
+    bc
+  have step1 := ModusPonens.mp flip_bc dne_a
+  -- step1: (φ→¬ψ) → (¬¬φ → ¬ψ)
+  -- Compose with dne_inner: ¬¬(φ→¬ψ) → (¬¬φ→¬ψ)
+  exact imp_trans dne_inner step1
+
+/-- De Morgan 1 backward: `⊢ (¬φ ∨ ¬ψ) → ¬(φ ∧ ψ)`. -/
+theorem demorgan_conj_neg_backward {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot)
+            HasBot.bot)
+          (HasImp.imp ψ HasBot.bot))
+        (HasImp.imp
+          (HasImp.imp
+            (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+            HasBot.bot)
+          HasBot.bot)) := by
+  -- Strategy: (¬¬φ→¬ψ) → ¬(φ∧ψ)
+  -- We need: (¬¬φ→¬ψ) → ((φ∧ψ) → ⊥)
+  -- i.e.: (¬¬φ→¬ψ) → ((φ→(ψ→⊥))→⊥) → ⊥
+
+  -- From (φ∧ψ), extract φ by lce_imp, get ¬¬φ by dni
+  -- Then from (¬¬φ→¬ψ), get ¬ψ
+  -- From (φ∧ψ), extract ψ by rce_imp
+  -- From ψ and ¬ψ, get ⊥
+
+  -- Build: (φ∧ψ) → ¬¬φ  [lce_imp then dni]
+  have lce := @lce_imp F _ _ S _ _ (φ := φ) (ψ := ψ)
+  have dni_φ := @dni F _ _ S _ _ φ
+  have conj_to_nnφ := imp_trans lce dni_φ
+  -- conj_to_nnφ: (φ∧ψ) → ¬¬φ
+
+  -- Build: (¬¬φ→¬ψ) → ((φ∧ψ)→¬¬φ) → ((φ∧ψ)→¬ψ)
+  have bc1 : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot)
+            HasBot.bot)
+          (HasImp.imp ψ HasBot.bot))
+        (HasImp.imp
+          (HasImp.imp
+            (HasImp.imp
+              (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+              HasBot.bot)
+            (HasImp.imp (HasImp.imp φ HasBot.bot)
+              HasBot.bot))
+          (HasImp.imp
+            (HasImp.imp
+              (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+              HasBot.bot)
+            (HasImp.imp ψ HasBot.bot)))) :=
+    b_combinator
+  have step1 := ModusPonens.mp
+    (@flip F _ _ S _ _
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+        (HasImp.imp ψ HasBot.bot))
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+          HasBot.bot)
+        (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot))
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+          HasBot.bot)
+        (HasImp.imp ψ HasBot.bot)))
+    bc1
+  -- step1: ((φ∧ψ)→¬¬φ) → ((¬¬φ→¬ψ) → ((φ∧ψ)→¬ψ))
+  have step2 := ModusPonens.mp step1 conj_to_nnφ
+  -- step2: (¬¬φ→¬ψ) → ((φ∧ψ)→¬ψ)
+
+  -- Also: (φ∧ψ) → ψ  [rce_imp]
+  have rce := @rce_imp F _ _ S _ _ (φ := φ) (ψ := ψ)
+  -- Now: from ((φ∧ψ)→¬ψ) and ((φ∧ψ)→ψ), get ((φ∧ψ)→⊥)
+  -- i.e., ¬(φ∧ψ)
+  -- app1: ψ → (ψ→⊥) → ⊥  [app1]
+  -- b: ((ψ→⊥)→⊥) → ((φ∧ψ)→(ψ→⊥)) → ((φ∧ψ)→⊥)
+  -- Hmm, the composition is complex. Let me use combine_imp_conj
+  -- pattern:
+  -- ImplyS: ((φ∧ψ)→(¬ψ)) → (((φ∧ψ)→ψ)→((φ∧ψ)→⊥))
+  -- Wait: ¬ψ = ψ→⊥, so we need:
+  -- ((φ∧ψ)→(ψ→⊥)) → (((φ∧ψ)→ψ) → ((φ∧ψ)→⊥))
+  -- This is exactly ImplyS!
+  have s1 := HasAxiomImplyS.implyS (S := S)
+    (φ := HasImp.imp
+      (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+      HasBot.bot)
+    (ψ := ψ) (χ := HasBot.bot)
+  -- s1: ((φ∧ψ)→(ψ→⊥)) → (((φ∧ψ)→ψ)→((φ∧ψ)→⊥))
+
+  -- Compose: (¬¬φ→¬ψ) → step2 → ((φ∧ψ)→¬ψ) →
+  --   s1 → (((φ∧ψ)→ψ)→((φ∧ψ)→⊥))
+  -- Then apply rce to get ((φ∧ψ)→⊥)
+  have step3 := imp_trans step2 s1
+  -- step3: (¬¬φ→¬ψ) → ((φ∧ψ)→ψ) → ((φ∧ψ)→⊥)
+
+  -- Weaken rce into scope, then apply
+  -- ImplyK: ((φ∧ψ)→ψ) → ((¬¬φ→¬ψ) → ((φ∧ψ)→ψ))
+  have k_rce := ModusPonens.mp
+    (HasAxiomImplyK.implyK (S := S)
+      (φ := HasImp.imp
+        (HasImp.imp
+          (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+          HasBot.bot)
+        ψ)
+      (ψ := HasImp.imp
+        (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+        (HasImp.imp ψ HasBot.bot)))
+    rce
+  -- k_rce: (¬¬φ→¬ψ) → ((φ∧ψ)→ψ)
+
+  -- ImplyS: ((¬¬φ→¬ψ) → (X→Y)) → (((¬¬φ→¬ψ)→X) → ((¬¬φ→¬ψ)→Y))
+  have s2 := HasAxiomImplyS.implyS (S := S)
+    (φ := HasImp.imp
+      (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+      (HasImp.imp ψ HasBot.bot))
+    (ψ := HasImp.imp
+      (HasImp.imp
+        (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+        HasBot.bot)
+      ψ)
+    (χ := HasImp.imp
+      (HasImp.imp
+        (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+        HasBot.bot)
+      HasBot.bot)
+  have step4 := ModusPonens.mp s2 step3
+  exact ModusPonens.mp step4 k_rce
+
+/-- De Morgan 1 biconditional:
+    `⊢ ¬(φ ∧ ψ) ↔ (¬φ ∨ ¬ψ)`. -/
+theorem demorgan_conj_neg {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp
+            (HasImp.imp
+              (HasImp.imp
+                (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+                HasBot.bot)
+              HasBot.bot)
+            (HasImp.imp
+              (HasImp.imp (HasImp.imp φ HasBot.bot)
+                HasBot.bot)
+              (HasImp.imp ψ HasBot.bot)))
+          (HasImp.imp
+            (HasImp.imp
+              (HasImp.imp
+                (HasImp.imp (HasImp.imp φ HasBot.bot)
+                  HasBot.bot)
+                (HasImp.imp ψ HasBot.bot))
+              (HasImp.imp
+                (HasImp.imp
+                  (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+                  HasBot.bot)
+                HasBot.bot))
+            HasBot.bot))
+        HasBot.bot) :=
+  iff_intro demorgan_conj_neg_forward
+    demorgan_conj_neg_backward
+
+/-- De Morgan 2 forward: `⊢ ¬(φ ∨ ψ) → (¬φ ∧ ¬ψ)`.
+    i.e., `¬((φ→⊥)→ψ) → ¬((φ→⊥)→((ψ→⊥)→⊥)→⊥)`.
+    Use DNE on B and contraposition. -/
+theorem demorgan_disj_neg_forward {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)
+          HasBot.bot)
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot)
+            (HasImp.imp
+              (HasImp.imp ψ HasBot.bot) HasBot.bot))
+          HasBot.bot)) := by
+  -- (¬φ→¬¬ψ) → (¬φ→ψ) by composing with DNE
+  -- Contrapose: ¬(¬φ→ψ) → ¬(¬φ→¬¬ψ)
+  have dne_ψ := @double_negation F _ _ S _ _ (φ := ψ)
+  -- b: (¬¬ψ→ψ) → ((¬φ→¬¬ψ) → (¬φ→ψ))
+  have bc : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp ψ HasBot.bot) HasBot.bot)
+          ψ)
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot)
+            (HasImp.imp (HasImp.imp ψ HasBot.bot)
+              HasBot.bot))
+          (HasImp.imp (HasImp.imp φ HasBot.bot) ψ))) :=
+    b_combinator
+  have impl := ModusPonens.mp bc dne_ψ
+  -- contrapose: ¬(¬φ→ψ) → ¬(¬φ→¬¬ψ)
+  exact contraposition impl
+
+/-- De Morgan 2 backward: `⊢ (¬φ ∧ ¬ψ) → ¬(φ ∨ ψ)`.
+    i.e., `¬((φ→⊥)→((ψ→⊥)→⊥)→⊥) → ¬((φ→⊥)→ψ)`.
+    Use DNI on B and contraposition. -/
+theorem demorgan_disj_neg_backward {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot)
+            (HasImp.imp
+              (HasImp.imp ψ HasBot.bot) HasBot.bot))
+          HasBot.bot)
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)
+          HasBot.bot)) := by
+  -- (¬φ→ψ) → (¬φ→¬¬ψ) by composing with DNI
+  -- Contrapose: ¬(¬φ→¬¬ψ) → ¬(¬φ→ψ)
+  have dni_ψ := @dni F _ _ S _ _ ψ
+  -- b: (ψ→¬¬ψ) → ((¬φ→ψ) → (¬φ→¬¬ψ))
+  have bc : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp ψ
+          (HasImp.imp (HasImp.imp ψ HasBot.bot)
+            HasBot.bot))
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)
+          (HasImp.imp (HasImp.imp φ HasBot.bot)
+            (HasImp.imp (HasImp.imp ψ HasBot.bot)
+              HasBot.bot)))) :=
+    b_combinator
+  have impl := ModusPonens.mp bc dni_ψ
+  -- contrapose: ¬(¬φ→¬¬ψ) → ¬(¬φ→ψ)
+  exact contraposition impl
+
+/-- De Morgan 2 biconditional:
+    `⊢ ¬(φ ∨ ψ) ↔ (¬φ ∧ ¬ψ)`. -/
+theorem demorgan_disj_neg {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp
+            (HasImp.imp
+              (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)
+              HasBot.bot)
+            (HasImp.imp
+              (HasImp.imp (HasImp.imp φ HasBot.bot)
+                (HasImp.imp
+                  (HasImp.imp ψ HasBot.bot) HasBot.bot))
+              HasBot.bot))
+          (HasImp.imp
+            (HasImp.imp
+              (HasImp.imp
+                (HasImp.imp (HasImp.imp φ HasBot.bot)
+                  (HasImp.imp
+                    (HasImp.imp ψ HasBot.bot) HasBot.bot))
+                HasBot.bot)
+              (HasImp.imp
+                (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)
+                HasBot.bot))
+            HasBot.bot))
+        HasBot.bot) :=
+  iff_intro demorgan_disj_neg_forward
+    demorgan_disj_neg_backward
+
+end Connectives
+
+end Cslib.Logic.Theorems.Propositional.Connectives
diff --git a/Cslib/Foundations/Logic/Theorems/Propositional/Core.lean b/Cslib/Foundations/Logic/Theorems/Propositional/Core.lean
new file mode 100644
index 000000000..847b1ff34
--- /dev/null
+++ b/Cslib/Foundations/Logic/Theorems/Propositional/Core.lean
@@ -0,0 +1,289 @@
+/-
+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
+public import Cslib.Foundations.Logic.Theorems.Combinators
+
+/-! # Core Propositional Theorems
+
+Core propositional theorems for the Hilbert-style proof system, including
+LEM, double negation elimination, reductio ad absurdum, efq for negation,
+reverse contraposition, and conjunction elimination (DT-free proofs).
+
+All theorems are generic over `[PropositionalHilbert S]`.
+
+## Main Results
+
+- `lem`: Law of Excluded Middle (identity on ¬φ)
+- `efq_axiom`: EFQ wrapper (⊥ → φ)
+- `peirce_axiom`: Peirce's law wrapper
+- `double_negation`: DNE derived from EFQ + Peirce + B-combinator
+- `raa`: Reductio ad absurdum (φ → (¬φ → ψ))
+- `efq_neg`: Ex falso for negation (¬φ → (φ → ψ))
+- `rcp`: Reverse contraposition ((¬φ → ¬ψ) → (ψ → φ))
+- `lce_imp`: Left conjunction elimination ((φ ∧ ψ) → φ) -- DT-free
+- `rce_imp`: Right conjunction elimination ((φ ∧ ψ) → ψ) -- DT-free
+
+## Naming Convention
+
+All negation, conjunction, disjunction use raw `HasImp.imp`/`HasBot.bot`
+encoding (Lukasiewicz style):
+- `¬φ := φ → ⊥`
+- `φ ∧ ψ := (φ → (ψ → ⊥)) → ⊥`
+- `φ ∨ ψ := (φ → ⊥) → ψ`
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Theorems.Propositional.Core
+
+open Cslib.Logic
+open Cslib.Logic.Theorems.Combinators
+
+variable {F : Type*} [HasBot F] [HasImp F]
+variable {S : Type*} [InferenceSystem S F]
+variable [PropositionalHilbert S (F := F)]
+
+section Core
+
+-- Abbreviations for readability
+-- neg φ = imp φ bot
+-- and φ ψ = imp (imp φ (imp ψ bot)) bot
+-- or φ ψ = imp (imp φ bot) ψ
+
+/-- EFQ wrapper: `⊢ ⊥ → φ`. -/
+theorem efq_axiom {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp HasBot.bot φ) :=
+  HasAxiomEFQ.efq
+
+/-- Peirce's law wrapper: `⊢ ((φ → ψ) → φ) → φ`. -/
+theorem peirce_axiom {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp φ ψ) φ) φ) :=
+  HasAxiomPeirce.peirce
+
+/-- Double negation elimination (derived):
+    `⊢ ¬¬φ → φ` where `¬φ = φ → ⊥`.
+
+    Proof: Peirce(φ,⊥) gives ((φ→⊥)→φ)→φ.
+    EFQ gives ⊥→φ. B-combinator composes
+    (⊥→φ) with ((φ→⊥)→⊥) to get ((φ→⊥)→φ).
+    Then Peirce gives φ. -/
+theorem double_negation {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+        φ) := by
+  -- Peirce with ψ = ⊥: ((φ→⊥)→φ) → φ
+  have peirce_inst := HasAxiomPeirce.peirce (S := S)
+    (φ := φ) (ψ := HasBot.bot)
+  -- EFQ: ⊥ → φ
+  have efq_inst := HasAxiomEFQ.efq (S := S) (φ := φ)
+  -- B-combinator: (⊥→φ) → ((φ→⊥)→⊥) → ((φ→⊥)→φ)
+  have b_inst : InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp HasBot.bot φ)
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+          (HasImp.imp (HasImp.imp φ HasBot.bot) φ))) :=
+    b_combinator
+  -- MP: ((φ→⊥)→⊥) → ((φ→⊥)→φ)
+  have step1 := ModusPonens.mp b_inst efq_inst
+  -- B-combinator to compose with Peirce
+  have b_final : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp (HasImp.imp φ HasBot.bot) φ) φ)
+        (HasImp.imp
+          (HasImp.imp
+            (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+            (HasImp.imp (HasImp.imp φ HasBot.bot) φ))
+          (HasImp.imp
+            (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+            φ))) :=
+    b_combinator
+  have step2 := ModusPonens.mp b_final peirce_inst
+  exact ModusPonens.mp step2 step1
+
+/-- Reductio ad absurdum: `⊢ φ → (¬φ → ψ)`
+    where `¬φ = φ → ⊥`. -/
+theorem raa {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp φ
+        (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)) := by
+  -- EFQ: ⊥ → ψ
+  have efq_inst := HasAxiomEFQ.efq (S := S) (φ := ψ)
+  -- DNI: φ → ¬¬φ = φ → (φ→⊥) → ⊥
+  have dni_inst := dni (S := S) φ
+  -- B: (⊥→ψ) → ((φ→⊥)→⊥) → ((φ→⊥)→ψ)
+  have b_inner : InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp HasBot.bot ψ)
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+          (HasImp.imp (HasImp.imp φ HasBot.bot) ψ))) :=
+    b_combinator
+  have step1 := ModusPonens.mp b_inner efq_inst
+  -- B: (¬¬φ→(¬φ→ψ)) → (φ→¬¬φ) → (φ→(¬φ→ψ))
+  have b_outer : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot)
+          (HasImp.imp (HasImp.imp φ HasBot.bot) ψ))
+        (HasImp.imp
+          (HasImp.imp φ
+            (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot))
+          (HasImp.imp φ
+            (HasImp.imp (HasImp.imp φ HasBot.bot) ψ)))) :=
+    b_combinator
+  have step2 := ModusPonens.mp b_outer step1
+  exact ModusPonens.mp step2 dni_inst
+
+/-- Ex falso for negation: `⊢ ¬φ → (φ → ψ)`.
+    Flip of RAA. -/
+theorem efq_neg {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp φ HasBot.bot)
+        (HasImp.imp φ ψ)) := by
+  have raa_inst := @raa F _ _ S _ _ (φ := φ) (ψ := ψ)
+  have flip_inst : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp φ
+          (HasImp.imp (HasImp.imp φ HasBot.bot) ψ))
+        (HasImp.imp (HasImp.imp φ HasBot.bot)
+          (HasImp.imp φ ψ))) :=
+    @flip F _ _ S _ _
+      φ (HasImp.imp φ HasBot.bot) ψ
+  exact ModusPonens.mp flip_inst raa_inst
+
+/-- Reverse contraposition: from `⊢ ¬φ → ¬ψ`,
+    derive `⊢ ψ → φ`.
+    Chain: ψ → ¬¬ψ → ¬¬φ → φ. -/
+theorem rcp {φ ψ : F}
+    (h : InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp φ HasBot.bot)
+        (HasImp.imp ψ HasBot.bot))) :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp ψ φ) := by
+  -- DNI for ψ: ψ → ¬¬ψ
+  have dni_b := dni (S := S) ψ
+  -- Contrapose h to get ¬¬ψ → ¬¬φ
+  -- b: (¬ψ→⊥) → ((¬φ→¬ψ) → (¬φ→⊥))
+  have bc : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp (HasImp.imp ψ HasBot.bot)
+          HasBot.bot)
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp φ HasBot.bot)
+            (HasImp.imp ψ HasBot.bot))
+          (HasImp.imp (HasImp.imp φ HasBot.bot)
+            HasBot.bot))) :=
+    b_combinator
+  -- Flip: (¬φ→¬ψ) → (¬¬ψ → ¬¬φ)
+  have flip_bc := ModusPonens.mp
+    (@flip F _ _ S _ _
+      (HasImp.imp (HasImp.imp ψ HasBot.bot) HasBot.bot)
+      (HasImp.imp (HasImp.imp φ HasBot.bot)
+        (HasImp.imp ψ HasBot.bot))
+      (HasImp.imp (HasImp.imp φ HasBot.bot) HasBot.bot))
+    bc
+  -- ¬¬ψ → ¬¬φ
+  have contraposed := ModusPonens.mp flip_bc h
+  -- ψ → ¬¬ψ → ¬¬φ
+  have b_to_nna := imp_trans dni_b contraposed
+  -- DNE for φ: ¬¬φ → φ
+  have dne_a := @double_negation F _ _ S _ _ (φ := φ)
+  -- ψ → ¬¬φ → φ
+  exact imp_trans b_to_nna dne_a
+
+/-- Left conjunction elimination (DT-free):
+    `⊢ (φ ∧ ψ) → φ` where `φ ∧ ψ = (φ→(ψ→⊥))→⊥`.
+
+    Proof: By Peirce with ψ₀ = ψ→⊥:
+    ((φ→(ψ→⊥))→φ)→φ.
+    From efq_neg: ¬(φ→(ψ→⊥)) → ((φ→(ψ→⊥)) → φ).
+    Compose with Peirce to get ¬(φ→(ψ→⊥)) → φ. -/
+theorem lce_imp {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+          HasBot.bot)
+        φ) := by
+  -- Peirce with ψ₀ = (ψ→⊥): ((φ→(ψ→⊥))→φ)→φ
+  have peirce_inst := HasAxiomPeirce.peirce (S := S)
+    (φ := φ) (ψ := HasImp.imp ψ HasBot.bot)
+  -- efq_neg at (φ→(ψ→⊥)): ¬(φ→(ψ→⊥)) → ((φ→(ψ→⊥)) → φ)
+  -- i.e., ((φ→(ψ→⊥))→⊥) → ((φ→(ψ→⊥)) → φ)
+  have efq_inst := @efq_neg F _ _ S _ _
+    (φ := HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+    (ψ := φ)
+  -- Compose with Peirce via imp_trans
+  exact imp_trans efq_inst peirce_inst
+
+/-- Right conjunction elimination (DT-free):
+    `⊢ (φ ∧ ψ) → ψ` where `φ ∧ ψ = (φ→(ψ→⊥))→⊥`.
+
+    Proof: By Peirce with ψ₀ = ⊥: ((ψ→⊥)→ψ)→ψ.
+    We need ¬(φ→(ψ→⊥)) → ((ψ→⊥)→ψ).
+    From ¬(φ→(ψ→⊥)) and (ψ→⊥), derive ⊥ and then ψ.
+    Use ImplyK to weaken: (ψ→⊥) → (φ→(ψ→⊥)).
+    Then compose. -/
+theorem rce_imp {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+          HasBot.bot)
+        ψ) := by
+  -- Peirce(ψ,⊥): ((ψ→⊥)→ψ)→ψ
+  have peirce_inst := HasAxiomPeirce.peirce (S := S)
+    (φ := ψ) (ψ := HasBot.bot)
+  -- efq_neg: ¬(φ→(ψ→⊥)) → ((φ→(ψ→⊥)) → ψ)
+  have efq_inst := @efq_neg F _ _ S _ _
+    (φ := HasImp.imp φ (HasImp.imp ψ HasBot.bot))
+    (ψ := ψ)
+  -- ImplyK: (ψ→⊥) → (φ→(ψ→⊥))
+  have k_inst := HasAxiomImplyK.implyK (S := S)
+    (φ := HasImp.imp ψ HasBot.bot) (ψ := φ)
+  -- b: ((φ→(ψ→⊥))→ψ) → ((ψ→⊥)→(φ→(ψ→⊥))) → ((ψ→⊥)→ψ)
+  have bc2 : InferenceSystem.DerivableIn S
+      (HasImp.imp
+        (HasImp.imp
+          (HasImp.imp φ (HasImp.imp ψ HasBot.bot)) ψ)
+        (HasImp.imp
+          (HasImp.imp (HasImp.imp ψ HasBot.bot)
+            (HasImp.imp φ (HasImp.imp ψ HasBot.bot)))
+          (HasImp.imp (HasImp.imp ψ HasBot.bot) ψ))) :=
+    b_combinator
+  -- flip: K → ((φ→(ψ→⊥))→ψ) → ((ψ→⊥)→ψ)
+  have flip_bc2 := ModusPonens.mp
+    (@flip F _ _ S _ _
+      (HasImp.imp
+        (HasImp.imp φ (HasImp.imp ψ HasBot.bot)) ψ)
+      (HasImp.imp (HasImp.imp ψ HasBot.bot)
+        (HasImp.imp φ (HasImp.imp ψ HasBot.bot)))
+      (HasImp.imp (HasImp.imp ψ HasBot.bot) ψ))
+    bc2
+  -- ((φ→(ψ→⊥))→ψ) → ((ψ→⊥)→ψ)
+  have step1 := ModusPonens.mp flip_bc2 k_inst
+  -- ¬(φ→(ψ→⊥)) → ((ψ→⊥)→ψ)
+  have step2 := imp_trans efq_inst step1
+  -- ¬(φ→(ψ→⊥)) → ψ
+  exact imp_trans step2 peirce_inst
+
+/-- Law of Excluded Middle: `⊢ φ ∨ ¬φ`
+    where `φ ∨ ¬φ = (φ → ⊥) → (φ → ⊥)`. -/
+theorem lem {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (HasImp.imp φ HasBot.bot)
+        (HasImp.imp φ HasBot.bot)) :=
+  identity (HasImp.imp φ HasBot.bot)
+
+end Core
+
+end Cslib.Logic.Theorems.Propositional.Core
diff --git a/Cslib/Foundations/Logic/Theorems/Temporal/FrameConditions.lean b/Cslib/Foundations/Logic/Theorems/Temporal/FrameConditions.lean
new file mode 100644
index 000000000..ca0583e29
--- /dev/null
+++ b/Cslib/Foundations/Logic/Theorems/Temporal/FrameConditions.lean
@@ -0,0 +1,90 @@
+/-
+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
+
+public import Mathlib.Algebra.Order.Group.Defs
+public import Mathlib.Algebra.Order.Group.Int
+public import Mathlib.Data.Int.SuccPred
+public import Mathlib.Data.Finset.Attr
+
+/-! # Frame Condition Typeclasses for Temporal Logic
+
+Marker typeclasses for temporal frame conditions. These bundle the underlying
+Mathlib typeclasses required by temporal logic semantics.
+
+## Hierarchy
+
+```
+LinearTemporalFrame (AddCommGroup + LinearOrder + IsOrderedAddMonoid)
+        |
+   SerialFrame (+ Nontrivial + NoMaxOrder + NoMinOrder)
+      /    \
+DenseTemporalFrame       DiscreteTemporalFrame
+(+ DenselyOrdered)        (+ SuccOrder + PredOrder + IsSuccArchimedean)
+```
+
+## Standard Instances
+
+- `Int` is a `DiscreteTemporalFrame`
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Temporal.FrameConditions
+
+/-! ## Base Typeclass: LinearTemporalFrame -/
+
+/-- Base typeclass for linear temporal frames. -/
+class LinearTemporalFrame (D : Type) [AddCommGroup D] [LinearOrder D]
+    [IsOrderedAddMonoid D] : Prop
+
+/-! ## Serial Frame -/
+
+/-- Serial temporal frame: no maximum or minimum elements. -/
+class SerialFrame (D : Type) [AddCommGroup D] [LinearOrder D]
+    [IsOrderedAddMonoid D] [Nontrivial D] [NoMaxOrder D] [NoMinOrder D] : Prop where
+  toLinearTemporalFrame : LinearTemporalFrame D := {}
+
+instance (D : Type) [AddCommGroup D] [LinearOrder D] [IsOrderedAddMonoid D]
+    [Nontrivial D] [NoMaxOrder D] [NoMinOrder D] [SerialFrame D] :
+    LinearTemporalFrame D :=
+  SerialFrame.toLinearTemporalFrame
+
+/-! ## Dense Temporal Frame -/
+
+/-- Dense temporal frame: densely ordered times. -/
+class DenseTemporalFrame (D : Type) [AddCommGroup D] [LinearOrder D]
+    [IsOrderedAddMonoid D] [Nontrivial D] [NoMaxOrder D] [NoMinOrder D]
+    [DenselyOrdered D] : Prop where
+  toSerialFrame : SerialFrame D := {}
+
+instance (D : Type) [AddCommGroup D] [LinearOrder D] [IsOrderedAddMonoid D]
+    [Nontrivial D] [NoMaxOrder D] [NoMinOrder D] [DenselyOrdered D]
+    [DenseTemporalFrame D] : SerialFrame D :=
+  DenseTemporalFrame.toSerialFrame
+
+/-! ## Discrete Temporal Frame -/
+
+/-- Discrete temporal frame: successor and predecessor structure. -/
+class DiscreteTemporalFrame (D : Type) [AddCommGroup D] [LinearOrder D]
+    [IsOrderedAddMonoid D] [Nontrivial D] [NoMaxOrder D] [NoMinOrder D]
+    [SuccOrder D] [PredOrder D] [IsSuccArchimedean D] : Prop where
+  toSerialFrame : SerialFrame D := {}
+
+instance (D : Type) [AddCommGroup D] [LinearOrder D] [IsOrderedAddMonoid D]
+    [Nontrivial D] [NoMaxOrder D] [NoMinOrder D] [SuccOrder D] [PredOrder D]
+    [IsSuccArchimedean D] [DiscreteTemporalFrame D] : SerialFrame D :=
+  DiscreteTemporalFrame.toSerialFrame
+
+/-! ## Standard Instances for Int -/
+
+instance : LinearTemporalFrame Int := ⟨⟩
+instance : SerialFrame Int := {}
+instance : DiscreteTemporalFrame Int := {}
+
+end Cslib.Logic.Temporal.FrameConditions
diff --git a/Cslib/Foundations/Logic/Theorems/Temporal/TemporalDerived.lean b/Cslib/Foundations/Logic/Theorems/Temporal/TemporalDerived.lean
new file mode 100644
index 000000000..58017e4c7
--- /dev/null
+++ b/Cslib/Foundations/Logic/Theorems/Temporal/TemporalDerived.lean
@@ -0,0 +1,292 @@
+/-
+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
+public import Cslib.Foundations.Logic.Theorems.Propositional.Core
+public import Cslib.Foundations.Logic.Theorems.Propositional.Connectives
+
+/-! # Temporal Derived Theorems (Generic Typeclass Style)
+
+Temporal theorems derived from the BX axiom system, generic over `[TemporalBXHilbert S]`.
+
+## Convention Note
+
+Convention (Burgess 1982): `untl φ₁ φ₂` = `φ₁ U φ₂` with `φ₁` as EVENT and `φ₂` as GUARD.
+`F(φ) = untl(φ, ⊤)` and `G(φ) = ¬F(¬φ)`. This matches BimodalLogic convention.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Theorems.Temporal.TemporalDerived
+
+open Cslib.Logic
+open Cslib.Logic.Axioms
+open Cslib.Logic.Theorems.Combinators
+open Cslib.Logic.Theorems.Propositional.Core
+open Cslib.Logic.Theorems.Propositional.Connectives
+
+variable {F : Type*} [HasBot F] [HasImp F] [HasUntil F] [HasSince F]
+variable {S : Type*} [InferenceSystem S F]
+variable [TemporalBXHilbert S (F := F)]
+
+section TemporalDerived
+
+-- Abbreviations neg'/top' imported from Cslib.Logic.Axioms
+/-- Eventually in the future: `Fφ := φ U ⊤`. -/
+abbrev someFuture (φ : F) : F := HasUntil.untl φ top'
+/-- Always in the future: `Gφ := ¬F¬φ`. -/
+abbrev allFuture (φ : F) : F := neg' (someFuture (neg' φ))
+/-- At some point in the past: `Pφ := φ S ⊤`. -/
+abbrev somePast (φ : F) : F := HasSince.snce φ top'
+/-- Always in the past: `Hφ := ¬P¬φ`. -/
+abbrev allPast (φ : F) : F := neg' (somePast (neg' φ))
+
+/-! ### Level 0: Direct Axiom Wrappers -/
+
+/-- Guard monotonicity of Until under G (BX2G): `⊢ G(φ→ψ) → (χ U φ → χ U ψ)`. -/
+theorem until_mono_guard {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S (Axioms.LeftMonoUntilG φ ψ χ) :=
+  HasAxiomLeftMonoUntilG.leftMonoUntilG
+
+/-- Guard monotonicity of Since under H (BX2H): `⊢ H(φ→ψ) → (χ S φ → χ S ψ)`. -/
+theorem since_mono_guard {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S (Axioms.LeftMonoSinceH φ ψ χ) :=
+  HasAxiomLeftMonoSinceH.leftMonoSinceH
+
+/-- Event monotonicity of Until (BX3): `⊢ G(φ→ψ) → (φ U χ → ψ U χ)`. -/
+theorem until_mono_event {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S (Axioms.RightMonoUntil φ ψ χ) :=
+  HasAxiomRightMonoUntil.rightMonoUntil
+
+/-- Event monotonicity of Since (BX3'): `⊢ H(φ→ψ) → (φ S χ → ψ S χ)`. -/
+theorem since_mono_event {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S (Axioms.RightMonoSince φ ψ χ) :=
+  HasAxiomRightMonoSince.rightMonoSince
+
+/-- Temporal connectedness future (BX4): `⊢ φ → G(P(φ))`. -/
+theorem connect_future_thm {φ : F} :
+    InferenceSystem.DerivableIn S (Axioms.ConnectFuture φ) :=
+  HasAxiomConnectFuture.connectFuture
+
+/-- Temporal connectedness past (BX4'): `⊢ φ → H(F(φ))`. -/
+theorem connect_past_thm {φ : F} :
+    InferenceSystem.DerivableIn S (Axioms.ConnectPast φ) :=
+  HasAxiomConnectPast.connectPast
+
+/-- Until implies F (BX10): `⊢ U(ψ,φ) → F(ψ)`. -/
+theorem until_implies_someFuture {φ ψ : F} :
+    InferenceSystem.DerivableIn S (Axioms.UntilF φ ψ) :=
+  HasAxiomUntilF.untilF
+
+/-- Since implies P (BX10'): `⊢ S(ψ,φ) → P(ψ)`. -/
+theorem since_implies_somePast {φ ψ : F} :
+    InferenceSystem.DerivableIn S (Axioms.SinceP φ ψ) :=
+  HasAxiomSinceP.sinceP
+
+/-! ### F_mono, P_mono
+
+With Burgess convention, F(φ) = untl(φ, ⊤) where the EVENT is φ (first arg).
+So F(A) → F(B) = untl(A,⊤) → untl(B,⊤) changes the event (first arg),
+which is BX3 (RightMonoUntil) with χ := ⊤.
+-/
+
+/-- F is monotone under G: `⊢ G(φ→ψ) → (Fφ → Fψ)`.
+    BX3 with χ := ⊤ (event position changes). -/
+theorem F_mono {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (allFuture (HasImp.imp φ ψ))
+        (HasImp.imp (someFuture φ) (someFuture ψ))) :=
+  HasAxiomRightMonoUntil.rightMonoUntil (S := S) (φ := φ) (ψ := ψ) (χ := top')
+
+/-- P is monotone under H: `⊢ H(φ→ψ) → (Pφ → Pψ)`.
+    BX3' with χ := ⊤ (event position changes). -/
+theorem P_mono {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (allPast (HasImp.imp φ ψ))
+        (HasImp.imp (somePast φ) (somePast ψ))) :=
+  HasAxiomRightMonoSince.rightMonoSince (S := S) (φ := φ) (ψ := ψ) (χ := top')
+
+/-! ### Duality Lemmas (DNI-based) -/
+
+/-- `⊢ F(¬φ) → ¬(Gφ)`: DNI at F(¬φ). -/
+theorem F_neg_G {φ : F} :
+    InferenceSystem.DerivableIn S (HasImp.imp (someFuture (neg' φ)) (neg' (allFuture φ))) :=
+  dni (someFuture (neg' φ))
+
+/-- `⊢ P(¬φ) → ¬(Hφ)`: DNI at P(¬φ). -/
+theorem P_neg_H {φ : F} :
+    InferenceSystem.DerivableIn S (HasImp.imp (somePast (neg' φ)) (neg' (allPast φ))) :=
+  dni (somePast (neg' φ))
+
+/-! ### Level 1: G-distribution -/
+
+/-- Helper: `⊢ ¬(¬ψ→¬φ) → ¬(φ→ψ)`. -/
+private theorem neg_contrapositive_imp_neg {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (neg' (HasImp.imp (neg' ψ) (neg' φ)))
+        (neg' (HasImp.imp φ ψ))) :=
+  ModusPonens.mp
+    (contrapose_imp (S := S) (φ := HasImp.imp φ ψ) (ψ := HasImp.imp (neg' ψ) (neg' φ)))
+    (contrapose_imp (S := S) (φ := φ) (ψ := ψ))
+
+/-- **G-distribution**: `⊢ G(φ→ψ) → (Gφ → Gψ)`.
+    Derived from BX3 and propositional contraposition. -/
+theorem G_distribution {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (allFuture (HasImp.imp φ ψ))
+        (HasImp.imp (allFuture φ) (allFuture ψ))) := by
+  -- Step 1: G(neg_contra) via temporal necessitation
+  have neg_contra := neg_contrapositive_imp_neg (S := S) (φ := φ) (ψ := ψ)
+  have g_nc := TemporalNecessitation.tempNec neg_contra
+  -- Step 2: BX3: G(¬(¬ψ→¬φ) → ¬(φ→ψ)) → (F(¬(¬ψ→¬φ)) → F(¬(φ→ψ)))
+  -- Using F_mono pattern (BX3 with χ := ⊤, event monotonicity)
+  have bx3 := HasAxiomRightMonoUntil.rightMonoUntil (S := S)
+    (φ := neg' (HasImp.imp (neg' ψ) (neg' φ)))
+    (ψ := neg' (HasImp.imp φ ψ))
+    (χ := top')
+  have F_step := ModusPonens.mp bx3 g_nc
+  -- Step 3: Contrapose: G(φ→ψ) → G(¬ψ→¬φ)
+  have G_contra := contraposition F_step
+  -- Step 4: BX3: G(¬ψ→¬φ) → (F(¬ψ) → F(¬φ))
+  have bx3' := HasAxiomRightMonoUntil.rightMonoUntil (S := S)
+    (φ := neg' ψ) (ψ := neg' φ) (χ := top')
+  -- Step 5: Contrapose to get Gφ → Gψ
+  have cp := contrapose_imp (S := S)
+    (φ := someFuture (neg' ψ)) (ψ := someFuture (neg' φ))
+  have GK := imp_trans bx3' cp
+  exact imp_trans G_contra GK
+
+/-- **H-distribution**: `⊢ H(φ→ψ) → (Hφ → Hψ)`.
+    Derived from BX3' and propositional contraposition (uses tempNecPast). -/
+theorem H_distribution {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (allPast (HasImp.imp φ ψ))
+        (HasImp.imp (allPast φ) (allPast ψ))) := by
+  have neg_contra := neg_contrapositive_imp_neg (S := S) (φ := φ) (ψ := ψ)
+  have h_nc := TemporalNecessitation.tempNecPast neg_contra
+  have bx3h := HasAxiomRightMonoSince.rightMonoSince (S := S)
+    (φ := neg' (HasImp.imp (neg' ψ) (neg' φ)))
+    (ψ := neg' (HasImp.imp φ ψ))
+    (χ := top')
+  have P_step := ModusPonens.mp bx3h h_nc
+  have H_contra := contraposition P_step
+  have bx3h' := HasAxiomRightMonoSince.rightMonoSince (S := S)
+    (φ := neg' ψ) (ψ := neg' φ) (χ := top')
+  have cp := contrapose_imp (S := S)
+    (φ := somePast (neg' ψ)) (ψ := somePast (neg' φ))
+  have HK := imp_trans bx3h' cp
+  exact imp_trans H_contra HK
+
+/-! ### G/H Contraposition -/
+
+/-- `⊢ G(φ→ψ) → G(¬ψ→¬φ)`. -/
+theorem G_contrapose {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (allFuture (HasImp.imp φ ψ))
+        (allFuture (HasImp.imp (neg' ψ) (neg' φ)))) := by
+  have neg_contra := neg_contrapositive_imp_neg (S := S) (φ := φ) (ψ := ψ)
+  have g_nc := TemporalNecessitation.tempNec neg_contra
+  have bx3 := HasAxiomRightMonoUntil.rightMonoUntil (S := S)
+    (φ := neg' (HasImp.imp (neg' ψ) (neg' φ)))
+    (ψ := neg' (HasImp.imp φ ψ))
+    (χ := top')
+  exact contraposition (ModusPonens.mp bx3 g_nc)
+
+/-- `⊢ H(φ→ψ) → H(¬ψ→¬φ)`. -/
+theorem H_contrapose {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (allPast (HasImp.imp φ ψ))
+        (allPast (HasImp.imp (neg' ψ) (neg' φ)))) := by
+  have neg_contra := neg_contrapositive_imp_neg (S := S) (φ := φ) (ψ := ψ)
+  have h_nc := TemporalNecessitation.tempNecPast neg_contra
+  have bx3h := HasAxiomRightMonoSince.rightMonoSince (S := S)
+    (φ := neg' (HasImp.imp (neg' ψ) (neg' φ)))
+    (ψ := neg' (HasImp.imp φ ψ))
+    (χ := top')
+  exact contraposition (ModusPonens.mp bx3h h_nc)
+
+/-! ### G/H Conjunction Introduction -/
+
+/-- `⊢ Gφ → Gψ → G(φ∧ψ)`. -/
+theorem G_and_intro {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (allFuture φ)
+        (HasImp.imp (allFuture ψ)
+          (allFuture (HasImp.imp (HasImp.imp φ (neg' ψ))
+            HasBot.bot)))) := by
+  have g_pair := TemporalNecessitation.tempNec (@pairing F _ _ S _ _ φ ψ)
+  have step1 := ModusPonens.mp (G_distribution (S := S)) g_pair
+  exact imp_trans step1 (G_distribution (S := S))
+
+/-- `⊢ Hφ → Hψ → H(φ∧ψ)`. -/
+theorem H_and_intro {φ ψ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (allPast φ)
+        (HasImp.imp (allPast ψ)
+          (allPast (HasImp.imp (HasImp.imp φ (neg' ψ))
+            HasBot.bot)))) := by
+  have h_pair := TemporalNecessitation.tempNecPast (@pairing F _ _ S _ _ φ ψ)
+  have step1 := ModusPonens.mp (H_distribution (S := S)) h_pair
+  exact imp_trans step1 (H_distribution (S := S))
+
+/-! ### G/H Implication Transitivity -/
+
+/-- `⊢ G(φ→ψ) → G(ψ→χ) → G(φ→χ)`. -/
+theorem G_imp_trans {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (allFuture (HasImp.imp φ ψ))
+        (HasImp.imp (allFuture (HasImp.imp ψ χ))
+          (allFuture (HasImp.imp φ χ)))) := by
+  have g_b := TemporalNecessitation.tempNec
+    (@b_combinator F _ _ S _ _ (φ := φ) (ψ := ψ) (χ := χ))
+  have step1 := ModusPonens.mp (G_distribution (S := S)) g_b
+  have step2 := imp_trans step1 (G_distribution (S := S))
+  -- step2 : G(ψ→χ) → G(φ→ψ) → G(φ→χ). Flip to get the right order.
+  exact ModusPonens.mp
+    (@flip F _ _ S _ _
+      (φ := allFuture (HasImp.imp ψ χ))
+      (ψ := allFuture (HasImp.imp φ ψ))
+      (χ := allFuture (HasImp.imp φ χ)))
+    step2
+
+/-- `⊢ H(φ→ψ) → H(ψ→χ) → H(φ→χ)`. -/
+theorem H_imp_trans {φ ψ χ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (allPast (HasImp.imp φ ψ))
+        (HasImp.imp (allPast (HasImp.imp ψ χ))
+          (allPast (HasImp.imp φ χ)))) := by
+  have h_b := TemporalNecessitation.tempNecPast
+    (@b_combinator F _ _ S _ _ (φ := φ) (ψ := ψ) (χ := χ))
+  have step1 := ModusPonens.mp (H_distribution (S := S)) h_b
+  have step2 := imp_trans step1 (H_distribution (S := S))
+  exact ModusPonens.mp
+    (@flip F _ _ S _ _
+      (φ := allPast (HasImp.imp ψ χ))
+      (ψ := allPast (HasImp.imp φ ψ))
+      (χ := allPast (HasImp.imp φ χ)))
+    step2
+
+/-! ### Level 4: Future-Past Interaction Chains -/
+
+/-- `⊢ Gφ → G(G(Pφ))`. -/
+theorem connect_future_G {φ : F} :
+    InferenceSystem.DerivableIn S
+      (HasImp.imp (allFuture φ)
+        (allFuture (allFuture (somePast φ)))) := by
+  have g_conn := TemporalNecessitation.tempNec (@connect_future_thm F _ _ _ _ S _ _ (φ := φ))
+  exact ModusPonens.mp (G_distribution (S := S)) g_conn
+
+/-- `⊢ Hφ → H(H(Fφ))`. -/
+theorem connect_past_H {φ : F} :
+    InferenceSystem.DerivableIn S (HasImp.imp (allPast φ) (allPast (allPast (someFuture φ)))) := by
+  have h_conn := TemporalNecessitation.tempNecPast (@connect_past_thm F _ _ _ _ S _ _ (φ := φ))
+  exact ModusPonens.mp (H_distribution (S := S)) h_conn
+
+end TemporalDerived
+
+end Cslib.Logic.Theorems.Temporal.TemporalDerived
diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean
index fa3caf53e..940d0b2b2 100644
--- a/Cslib/Logics/Propositional/Defs.lean
+++ b/Cslib/Logics/Propositional/Defs.lean
@@ -1,22 +1,24 @@
 /-
-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). Conjunction, disjunction, negation, and verum are
+  derived connectives following the Lukasiewicz convention.
 - `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
@@ -42,44 +44,50 @@ 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
+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 +110,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. -/
diff --git a/Cslib/Logics/Propositional/Metalogic/DeductionTheorem.lean b/Cslib/Logics/Propositional/Metalogic/DeductionTheorem.lean
new file mode 100644
index 000000000..b825599db
--- /dev/null
+++ b/Cslib/Logics/Propositional/Metalogic/DeductionTheorem.lean
@@ -0,0 +1,180 @@
+/-
+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
+
+public import Cslib.Logics.Propositional.ProofSystem.Derivation
+public import Cslib.Foundations.Data.ListHelpers
+public import Cslib.Foundations.Logic.Metalogic.DeductionHelpers
+
+/-! # Deduction Theorem for Propositional Logic
+
+This module proves the deduction theorem for the propositional Hilbert system:
+if `A :: Γ ⊢ B` then `Γ ⊢ A → B`.
+
+## Main Results
+
+- `deductionTheorem`: The core metatheorem, by well-founded recursion on derivation height.
+- `deductionWithMem`: Helper for the weakening case where the deduction hypothesis
+  appears in the middle of the context.
+- `prop_has_deduction_theorem`: The `HasDeductionTheorem` instance for the generic MCS
+  framework.
+
+## Implementation
+
+The proof follows the Modal pattern with well-founded recursion on
+`DerivationTree.height`. The propositional version is simpler than the modal one
+because there are only 4 constructors (no necessitation), eliminating the impossible
+empty-context case entirely.
+
+## References
+
+* Cslib/Logics/Modal/Metalogic/DeductionTheorem.lean -- modal deduction theorem
+* Cslib/Foundations/Logic/Metalogic/Consistency.lean
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL
+
+open Cslib.Logic
+open Cslib.Logic.Helpers
+
+variable {Atom : Type*}
+
+attribute [local instance] Classical.propDecidable
+
+/-! ## HasHilbertTree Instance -/
+
+/-- `HasHilbertTree` instance for propositional logic. Maps PL's `.implyK`/`.implyS`
+axiom constructors to the generic typeclass fields. -/
+noncomputable instance : HasHilbertTree (PL.Proposition Atom) where
+  Tree := fun Γ φ => DerivationTree Γ φ
+  implyK := fun φ ψ => .ax [] _ (.implyK φ ψ)
+  implyS := fun φ ψ χ => .ax [] _ (.implyS φ ψ χ)
+  assumption := fun h => .assumption _ _ h
+  mp := fun d₁ d₂ => .modus_ponens _ _ _ d₁ d₂
+  weakening := fun d h => .weakening _ _ _ d h
+
+/-! ## Core: deductionWithMem -/
+
+/-- The key helper for the weakening case: if `Γ' ⊢ φ` and `A ∈ Γ'`, then
+`removeAll Γ' A ⊢ A → φ`.
+
+This recurses on the derivation structure. All recursive calls are on derivations
+with strictly smaller height, ensuring termination. -/
+noncomputable def deductionWithMem
+    (Γ' : List (PL.Proposition Atom)) (A φ : PL.Proposition Atom)
+    (d : DerivationTree Γ' φ) (hA : A ∈ Γ') :
+    DerivationTree (removeAll Γ' A) (A.imp φ) := by
+  match d with
+  | .ax _ ψ h_ax =>
+    exact deductionAxiom (removeAll Γ' A) A (.ax [] ψ h_ax)
+  | .assumption _ ψ h_mem =>
+    by_cases h_eq : ψ = A
+    · subst h_eq
+      exact deductionImpSelf (removeAll Γ' ψ) ψ
+    · have h_mem' : ψ ∈ removeAll Γ' A := mem_removeAll_of_mem_of_ne h_mem h_eq
+      exact deductionAssumptionOther (removeAll Γ' A) A ψ h_mem'
+  | .modus_ponens _ ψ χ d₁ d₂ =>
+    have ih₁ := deductionWithMem Γ' A (ψ.imp χ) d₁ hA
+    have ih₂ := deductionWithMem Γ' A ψ d₂ hA
+    exact deductionMpUnderImp (removeAll Γ' A) A ψ χ ih₁ ih₂
+  | .weakening Γ'' _ ψ d' h_sub =>
+    by_cases hA' : A ∈ Γ''
+    · have ih := deductionWithMem Γ'' A ψ d' hA'
+      have h_sub' : ∀ x ∈ removeAll Γ'' A, x ∈ removeAll Γ' A :=
+        removeAll_subset_removeAll h_sub
+      exact .weakening (removeAll Γ'' A) (removeAll Γ' A) (A.imp ψ) ih h_sub'
+    · have h_sub' : ∀ x ∈ Γ'', x ∈ removeAll Γ' A := by
+        intro x hx
+        exact mem_removeAll_of_mem_of_ne (h_sub x hx) (fun h_eq => hA' (h_eq ▸ hx))
+      have d_weak := DerivationTree.weakening Γ'' (removeAll Γ' A) ψ d' h_sub'
+      have k_ax : DerivationTree [] (ψ.imp (A.imp ψ)) := .ax [] _ (.implyK ψ A)
+      have k_weak := DerivationTree.weakening [] (removeAll Γ' A) _ k_ax
+        (fun _ h => nomatch h)
+      exact .modus_ponens (removeAll Γ' A) ψ (A.imp ψ) k_weak d_weak
+termination_by d.height
+decreasing_by
+  simp_wf
+  · exact DerivationTree.height_modus_ponens_left d₁ d₂
+  · exact DerivationTree.height_modus_ponens_right d₁ d₂
+  · exact DerivationTree.height_weakening d' h_sub
+
+/-! ## Main Deduction Theorem -/
+
+/-- **Deduction Theorem**: If `A :: Γ ⊢ B` then `Γ ⊢ A → B`.
+
+Proof by well-founded recursion on derivation tree height. Handles all 4 constructors:
+- `ax`: Use `implyK` to weaken the axiom under implication.
+- `assumption` (same): Produce `A → A` via `deductionImpSelf`.
+- `assumption` (other): Use `implyK` with the other assumption.
+- `modus_ponens`: Recurse on both subderivations, combine via `implyS`.
+- `weakening`: Three subcases -- context equality, `A ∈ Γ'` (uses `deductionWithMem`),
+  or `A ∉ Γ'` (uses `implyK`). -/
+noncomputable def deductionTheorem (Γ : List (PL.Proposition Atom)) (A B : PL.Proposition Atom)
+    (d : DerivationTree (A :: Γ) B) :
+    DerivationTree Γ (A.imp B) := by
+  match d with
+  | .ax _ φ h_ax =>
+    exact deductionAxiom Γ A (.ax [] φ h_ax)
+  | .assumption _ φ h_mem =>
+    by_cases h_eq : φ = A
+    · subst h_eq
+      exact deductionImpSelf Γ φ
+    · have h_tail : φ ∈ Γ := by
+        cases h_mem with
+        | head => exact absurd rfl h_eq
+        | tail _ h => exact h
+      exact deductionAssumptionOther Γ A φ h_tail
+  | .modus_ponens _ φ ψ d₁ d₂ =>
+    have ih₁ := deductionTheorem Γ A (φ.imp ψ) d₁
+    have ih₂ := deductionTheorem Γ A φ d₂
+    exact deductionMpUnderImp Γ A φ ψ ih₁ ih₂
+  | .weakening Γ' _ φ d' h_sub =>
+    by_cases h_eq : Γ' = A :: Γ
+    · exact deductionTheorem Γ A φ (h_eq ▸ d')
+    · by_cases hA : A ∈ Γ'
+      · have ih := deductionWithMem Γ' A φ d' hA
+        have h_sub' : ∀ x ∈ removeAll Γ' A, x ∈ Γ :=
+          removeAll_subset_of_subset h_sub hA
+        exact .weakening (removeAll Γ' A) Γ (A.imp φ) ih h_sub'
+      · have h_sub' : ∀ x ∈ Γ', x ∈ Γ := by
+          intro x hx
+          have := h_sub x hx
+          simp [List.mem_cons] at this
+          rcases this with rfl | h
+          · exact absurd hx hA
+          · exact h
+        have d_weak := DerivationTree.weakening Γ' Γ φ d' h_sub'
+        have k_ax : DerivationTree (Atom := Atom) [] (φ.imp (A.imp φ)) := .ax [] _ (.implyK φ A)
+        have k_weak := DerivationTree.weakening [] Γ _ k_ax
+          (fun _ h => nomatch h)
+        exact .modus_ponens Γ φ (A.imp φ) k_weak d_weak
+termination_by d.height
+decreasing_by
+  simp_wf
+  · exact DerivationTree.height_modus_ponens_left d₁ d₂
+  · exact DerivationTree.height_modus_ponens_right d₁ d₂
+  · have : (h_eq ▸ d').height = d'.height := by subst h_eq; rfl
+    simp [this]
+    exact DerivationTree.height_weakening d' h_sub
+
+/-! ## HasDeductionTheorem Instance -/
+
+/-- The deduction theorem wrapped for the generic MCS framework.
+
+`HasDeductionTheorem (@propDerivationSystem Atom)` states that for any
+`Γ`, `φ`, `ψ`, if `φ :: Γ ⊢ ψ` then `Γ ⊢ φ → ψ`. -/
+theorem prop_has_deduction_theorem :
+    Metalogic.HasDeductionTheorem (@propDerivationSystem Atom) := by
+  intro Γ φ ψ h
+  unfold propDerivationSystem Deriv at h ⊢
+  simp at h ⊢
+  obtain ⟨d⟩ := h
+  exact ⟨deductionTheorem Γ φ ψ d⟩
+
+end Cslib.Logic.PL
diff --git a/Cslib/Logics/Propositional/Metalogic/MCS.lean b/Cslib/Logics/Propositional/Metalogic/MCS.lean
new file mode 100644
index 000000000..e9c0424e4
--- /dev/null
+++ b/Cslib/Logics/Propositional/Metalogic/MCS.lean
@@ -0,0 +1,129 @@
+/-
+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
+
+public import Cslib.Logics.Propositional.Metalogic.DeductionTheorem
+
+/-! # Maximal Consistent Sets for Propositional Logic
+
+This module instantiates the generic MCS framework (from `Consistency.lean`) for
+propositional logic and proves propositional-specific MCS properties needed for
+completeness results.
+
+## Main Results
+
+### Generic MCS properties (instantiated from Consistency.lean)
+- `prop_lindenbaum`: Every consistent set extends to a maximally consistent set.
+- `prop_closed_under_derivation`: Derivable formulas are in MCS.
+- `prop_implication_property`: Modus ponens reflected in membership.
+- `prop_negation_complete`: Either `φ` or `¬φ` is in every MCS.
+
+### Propositional-specific properties
+- `prop_mcs_bot_not_mem`: `⊥ ∉ S` for any MCS `S`.
+- `prop_mcs_neg_of_not_mem`: If `φ ∉ S`, then `¬φ ∈ S`.
+- `prop_mcs_not_mem_of_neg`: If `¬φ ∈ S`, then `φ ∉ S`.
+- `prop_mcs_mem_iff_neg_not_mem`: `φ ∈ S ↔ ¬φ ∉ S`.
+
+## References
+
+* Cslib/Logics/Modal/Metalogic/MCS.lean -- modal MCS pattern
+* Cslib/Foundations/Logic/Metalogic/Consistency.lean -- generic MCS framework
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL
+
+open Cslib.Logic
+
+variable {Atom : Type*}
+
+/-! ## Abbreviations for readability -/
+
+/-- Set consistency for the propositional derivation system. -/
+abbrev PropSetConsistent (S : Set (PL.Proposition Atom)) : Prop :=
+  Metalogic.SetConsistent propDerivationSystem S
+
+/-- Set maximal consistency for the propositional derivation system. -/
+abbrev PropSetMaximalConsistent (S : Set (PL.Proposition Atom)) : Prop :=
+  Metalogic.SetMaximalConsistent propDerivationSystem S
+
+/-! ## Generic MCS Properties (instantiated) -/
+
+/-- Lindenbaum's lemma for propositional logic: every consistent set extends
+to an MCS. -/
+theorem prop_lindenbaum {S : Set (PL.Proposition Atom)}
+    (hS : PropSetConsistent S) :
+    ∃ M : Set (PL.Proposition Atom), S ⊆ M ∧ PropSetMaximalConsistent M :=
+  Metalogic.set_lindenbaum propDerivationSystem hS
+
+/-- Derivable formulas are in MCS. -/
+theorem prop_closed_under_derivation
+    {S : Set (PL.Proposition Atom)} (h_mcs : PropSetMaximalConsistent S)
+    {L : List (PL.Proposition Atom)} (h_sub : ∀ ψ ∈ L, ψ ∈ S)
+    {φ : PL.Proposition Atom}
+    (h_deriv : propDerivationSystem.Deriv L φ) : φ ∈ S :=
+  Metalogic.SetMaximalConsistent.closed_under_derivation
+    propDerivationSystem prop_has_deduction_theorem h_mcs h_sub h_deriv
+
+/-- Implication property: if `φ → ψ ∈ S` and `φ ∈ S`, then `ψ ∈ S`. -/
+theorem prop_implication_property
+    {S : Set (PL.Proposition Atom)} (h_mcs : PropSetMaximalConsistent S)
+    {φ ψ : PL.Proposition Atom}
+    (h_imp : Proposition.imp φ ψ ∈ S) (h_phi : φ ∈ S) : ψ ∈ S :=
+  Metalogic.SetMaximalConsistent.implication_property
+    propDerivationSystem prop_has_deduction_theorem h_mcs h_imp h_phi
+
+/-- Negation completeness: for any formula `φ`, either `φ ∈ S` or `¬φ ∈ S`. -/
+theorem prop_negation_complete
+    {S : Set (PL.Proposition Atom)} (h_mcs : PropSetMaximalConsistent S)
+    (φ : PL.Proposition Atom) : φ ∈ S ∨ Proposition.neg φ ∈ S :=
+  Metalogic.SetMaximalConsistent.negation_complete
+    propDerivationSystem prop_has_deduction_theorem h_mcs φ
+
+/-! ## Propositional-Specific MCS Properties -/
+
+/-- `⊥ ∉ S` for any MCS `S`. -/
+theorem prop_mcs_bot_not_mem
+    {S : Set (PL.Proposition Atom)} (h_mcs : PropSetMaximalConsistent S) :
+    Proposition.bot ∉ S := by
+  intro h_bot
+  exact h_mcs.1 [Proposition.bot]
+    (fun x hx => by simp [List.mem_cons] at hx; exact hx ▸ h_bot)
+    (by simp [propDerivationSystem, Deriv]
+        exact ⟨.assumption _ _ (List.mem_cons.mpr (Or.inl rfl))⟩)
+
+/-- If `φ ∉ S` (MCS), then `¬φ ∈ S`. -/
+theorem prop_mcs_neg_of_not_mem
+    {S : Set (PL.Proposition Atom)} (h_mcs : PropSetMaximalConsistent S)
+    {φ : PL.Proposition Atom} (h_not : φ ∉ S) : Proposition.neg φ ∈ S := by
+  rcases prop_negation_complete h_mcs φ with h | h
+  · exact absurd h h_not
+  · exact h
+
+/-- If `¬φ ∈ S` (MCS), then `φ ∉ S`. -/
+theorem prop_mcs_not_mem_of_neg
+    {S : Set (PL.Proposition Atom)} (h_mcs : PropSetMaximalConsistent S)
+    {φ : PL.Proposition Atom} (h_neg : Proposition.neg φ ∈ S) : φ ∉ S := by
+  intro h_phi
+  exact prop_mcs_bot_not_mem h_mcs
+    (prop_implication_property h_mcs h_neg h_phi)
+
+/-- `φ ∈ S ↔ ¬φ ∉ S` for MCS `S`. -/
+theorem prop_mcs_mem_iff_neg_not_mem
+    {S : Set (PL.Proposition Atom)} (h_mcs : PropSetMaximalConsistent S)
+    {φ : PL.Proposition Atom} : φ ∈ S ↔ Proposition.neg φ ∉ S := by
+  constructor
+  · intro h hn
+    exact prop_mcs_bot_not_mem h_mcs
+      (prop_implication_property h_mcs hn h)
+  · intro h
+    rcases prop_negation_complete h_mcs φ with h' | h'
+    · exact h'
+    · exact absurd h' h
+
+end Cslib.Logic.PL
diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
index b1a8947e2..eb3019b17 100644
--- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
+++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
@@ -1,7 +1,7 @@
 /-
-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
 
@@ -42,13 +42,10 @@ abbreviates a derivation of `A` in the empty context: `T⇓(∅ ⊢ A)`.
 
 ## Implementation notes
 
-We formalise here a single type of derivations, meaning there is a single collection of inference
-rules (those for minimal logic). The extension to intuitionistic and classical logic are modelled
-by adding *axioms* --- for instance, intuitionistic derivations are allowed to appeal to axioms of
-the form `⊥ → A` for any proposition `A`. This differs from many on-paper presentations, which add
-that principle as a deduction rule: from `Γ ⊢ ⊥` derive `Γ ⊢ A`. Discussion on proper way to
-capture such developments in cslib is ongoing, see the following
-[zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Logic/with/585843520).
+The primitive inference rules are: axiom (from theory), assumption (from context),
+implication introduction and elimination, and ex falso quodlibet (bottom elimination).
+Conjunction and disjunction rules are derivable from these primitives together with
+the Lukasiewicz definitions of `∧` and `∨` in terms of `→` and `⊥`.
 
 ## References
 
@@ -83,32 +80,22 @@ abbrev Sequent {Atom} := Ctx Atom × Proposition Atom
 scoped notation Γ:60 " ⊢ " A => (⟨Γ, A⟩ : Sequent)
 
 /-- A `T`-derivation of {A₁, ..., Aₙ} ⊢ B demonstrates B using (undischarged) assumptions among Aᵢ,
-possibly appealing to axioms from `T`. -/
+possibly appealing to axioms from `T`. Primitives: axiom, assumption, implication intro/elim,
+and ex falso quodlibet (bottom elimination). -/
 inductive Theory.Derivation {T : Theory Atom} : Ctx Atom → Proposition Atom → Type u where
   /-- Axiom -/
   | ax {Γ : Ctx Atom} {A : Proposition Atom} (_ : A ∈ T) : Derivation Γ A
   /-- Assumption -/
   | ass {Γ : Ctx Atom} {A : Proposition Atom} (_ : A ∈ Γ) : Derivation Γ A
-  /-- Conjunction introduction -/
-  | andI {Γ : Ctx Atom} {A B : Proposition Atom} :
-      Derivation Γ A → Derivation Γ B → Derivation Γ (A ∧ B)
-  /-- Conjunction elimination left -/
-  | andE₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A ∧ B) → Derivation Γ A
-  /-- Conjunction elimination right -/
-  | andE₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A ∧ B) → Derivation Γ B
-  /-- Disjunction introduction left -/
-  | orI₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ A → Derivation Γ (A ∨ B)
-  /-- Disjunction introduction right -/
-  | orI₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ B → Derivation Γ (A ∨ B)
-  /-- Disjunction elimination -/
-  | orE {Γ : Ctx Atom} {A B C : Proposition Atom} : Derivation Γ (A ∨ B) →
-      Derivation (insert A Γ) C → Derivation (insert B Γ) C → Derivation Γ C
   /-- Implication introduction -/
-  | implI {A B : Proposition Atom} (Γ : Ctx Atom) :
+  | impI {A B : Proposition Atom} (Γ : Ctx Atom) :
       Derivation (insert A Γ) B → Derivation Γ (A → B)
-  /-- Implication elimination -/
-  | implE {Γ : Ctx Atom} {A B : Proposition Atom} :
+  /-- Implication elimination (modus ponens) -/
+  | impE {Γ : Ctx Atom} {A B : Proposition Atom} :
       Derivation Γ (A → B) → Derivation Γ A → Derivation Γ B
+  /-- Ex falso quodlibet (bottom elimination) -/
+  | botE {Γ : Ctx Atom} {A : Proposition Atom} :
+      Derivation Γ ⊥ → Derivation Γ A
 
 /-- Inference system for derivations under the theory `T`. -/
 instance (T : Theory Atom) : InferenceSystem T (Sequent (Atom := Atom)) where
@@ -170,17 +157,9 @@ def Theory.Derivation.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposit
     (hTheory : T ⊆ T') (hCtx : Γ ⊆ Δ) : T.Derivation Γ A → T'.Derivation Δ A
   | ax hA => ax <| hTheory hA
   | ass hA => ass <| hCtx hA
-  | andI D D' => andI (D.weak hTheory hCtx) (D'.weak hTheory hCtx)
-  | andE₁ D => andE₁ <| D.weak hTheory hCtx
-  | andE₂ D => andE₂ <| D.weak hTheory hCtx
-  | orI₁ D => orI₁ <| D.weak hTheory hCtx
-  | orI₂ D => orI₂ <| D.weak hTheory hCtx
-  | orE D D' D'' =>
-    orE (D.weak hTheory hCtx)
-      (D'.weak hTheory <| Finset.insert_subset_insert _ hCtx)
-      (D''.weak hTheory <| Finset.insert_subset_insert _ hCtx)
-  | @implI _ _ _ A B Γ D => implI (Δ) <| D.weak hTheory <| Finset.insert_subset_insert _ hCtx
-  | implE D D' => implE (D.weak hTheory hCtx) (D'.weak hTheory hCtx)
+  | @impI _ _ _ A B Γ D => impI (Δ) <| D.weak hTheory <| Finset.insert_subset_insert _ hCtx
+  | impE D D' => impE (D.weak hTheory hCtx) (D'.weak hTheory hCtx)
+  | botE D => botE <| D.weak hTheory hCtx
 
 /-- Weakening the theory only. -/
 def Theory.Derivation.weakTheory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom}
@@ -213,9 +192,9 @@ substitution, which would replace appeals to `A` in `E` by the whole derivation
 -/
 def Theory.Derivation.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom}
     (D : T⇓(Γ ⊢ A)) (E : T⇓(insert A Δ ⊢ B)) : T⇓((Γ ∪ Δ) ⊢ B) := by
-  refine implE (A := A) ?_ (D.weakCtx Finset.subset_union_left)
+  refine impE (A := A) ?_ (D.weakCtx Finset.subset_union_left)
   have : insert A Δ ⊆ insert A (Γ ∪ Δ) := by grind
-  exact implI (Γ ∪ Δ) <| E.weakCtx this
+  exact impI (Γ ∪ Δ) <| E.weakCtx this
 
 /-- Proof irrelevant cut rule. -/
 theorem DerivableIn.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom} :
@@ -249,22 +228,12 @@ def Theory.Derivation.subs {Γ Γ' Δ : Ctx Atom} {B : Proposition Atom}
       exact (Ds B h).weakCtx <| by grind
     case neg h =>
       exact ass <| by grind
-  | andI E E' => andI (E.subs Ds) (E'.subs Ds)
-  | andE₁ E => andE₁ <| E.subs Ds
-  | andE₂ E => andE₂ <| E.subs Ds
-  | orI₁ E => orI₁ <| E.subs Ds
-  | orI₂ E => orI₂ <| E.subs Ds
-  | @orE _ _ _ _ C C' _ E E' E'' .. => by
-    apply orE (E.subs Ds)
-    · rw [show insert C (Γ \ Γ' ∪ Δ) = (insert C Γ \ Γ') ∪ insert C Δ by grind]
-      exact E'.subs Ds |>.weakCtx (by grind)
-    · rw [show insert C' (Γ \ Γ' ∪ Δ) = (insert C' Γ \ Γ') ∪ insert C' Δ by grind]
-      exact E''.subs Ds |>.weakCtx (by grind)
-  | @implI _ _ _ A' _ _ E .. => by
-    apply implI
+  | @impI _ _ _ A' _ _ E .. => by
+    apply impI
     rw [show insert A' (Γ \ Γ' ∪ Δ) = (insert A' Γ \ Γ') ∪ insert A' Δ by grind]
     exact E.subs Ds |>.weakCtx (by grind)
-  | implE E E' => implE (E.subs Ds) (E'.subs Ds)
+  | impE E E' => impE (E.subs Ds) (E'.subs Ds)
+  | botE E => botE <| E.subs Ds
 
 /-- Transport a derivation along a substitution of atoms. -/
 def Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom']
@@ -272,16 +241,9 @@ def Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [Decida
     T.Derivation Γ B → (T.subst f).Derivation (Γ.subst f) (B >>= f)
   | ax h => ax <| Set.mem_image_of_mem (· >>= f) h
   | ass h => ass <| Finset.mem_image_of_mem (· >>= f) h
-  | andI D E => andI (D.substAtom f) (E.substAtom f)
-  | andE₁ D => andE₁ (D.substAtom f)
-  | andE₂ D => andE₂ (D.substAtom f)
-  | orI₁ D => orI₁ (D.substAtom f)
-  | orI₂ D => orI₂ (D.substAtom f)
-  | orE D E E' => orE (D.substAtom f)
-    ((Finset.image_insert (· >>= f) _ _) ▸ E.substAtom f)
-    ((Finset.image_insert (· >>= f) _ _) ▸ E'.substAtom f)
-  | implI _ D => implI _ <| (Finset.image_insert (· >>= f) _ _) ▸ (D.substAtom f)
-  | implE D E => implE (D.substAtom f) (E.substAtom f)
+  | impI _ D => impI _ <| (Finset.image_insert (· >>= f) _ _) ▸ (D.substAtom f)
+  | impE D E => impE (D.substAtom f) (E.substAtom f)
+  | botE D => botE (D.substAtom f)
 
 theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom']
     {T : Theory Atom}
@@ -292,12 +254,12 @@ theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [Decidabl
 /-! ### Properties of equivalence -/
 
 /-- A derivation of the canonical tautology. -/
-def Theory.derivationTop [Inhabited Atom] : T⇓(⊤ : Proposition Atom) :=
-  implI ∅ <| ass <| by grind
+def Theory.derivationTop : T⇓(⊤ : Proposition Atom) :=
+  impI ∅ <| ass <| by grind
 
-theorem derivableIn_top [Inhabited Atom] : DerivableIn T (⊤ : Proposition Atom) := ⟨derivationTop⟩
+theorem derivableIn_top : DerivableIn T (⊤ : Proposition Atom) := ⟨derivationTop⟩
 
-theorem derivable_iff_equiv_top [Inhabited Atom] (A : Proposition Atom) :
+theorem derivable_iff_equiv_top (A : Proposition Atom) :
     DerivableIn T A ↔ A ≡[T] ⊤ := by
   constructor <;> intro h
   · refine ⟨derivationTop.weakCtx <| by grind, ?_⟩
diff --git a/Cslib/Logics/Propositional/NaturalDeduction/FromHilbert.lean b/Cslib/Logics/Propositional/NaturalDeduction/FromHilbert.lean
new file mode 100644
index 000000000..b954334da
--- /dev/null
+++ b/Cslib/Logics/Propositional/NaturalDeduction/FromHilbert.lean
@@ -0,0 +1,219 @@
+/-
+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
+
+public import Cslib.Logics.Propositional.Metalogic.DeductionTheorem
+
+/-! # Natural Deduction Rules as Hilbert Wrappers
+
+This module provides ND-flavored lemma names as thin wrappers around the
+Hilbert `DerivationTree` infrastructure, giving the familiar `impI`/`impE`/`botE`
+interface. It also derives cut, weakening, and substitution within the
+Hilbert framework.
+
+## Main Definitions
+
+### Core ND Rules (Type-level)
+- `impI`: Implication introduction (deduction theorem wrapper)
+- `impE`: Implication elimination (modus ponens wrapper)
+- `botE`: Ex falso quodlibet (EFQ axiom + modus ponens)
+- `assume`: Assumption (context membership wrapper)
+- `axiomRule`: Theory axiom (axiom schema wrapper)
+
+### Derived Rules (Type-level)
+- `hilbertCut`: Cut rule within the Hilbert framework
+- `hilbertWeakening`: Explicit weakening
+
+### Prop-level Versions
+- `impIDeriv`, `impEDeriv`, `botEDeriv`, `hilbertCutDeriv`,
+  `hilbertWeakeningDeriv`: `Deriv`-level versions of the above
+
+## Design
+
+These wrappers provide the familiar natural deduction interface while
+being backed by the Hilbert derivation tree. This file coexists with
+the standalone `NaturalDeduction/Basic.lean`.
+
+## References
+
+* Cslib/Logics/Propositional/NaturalDeduction/Basic.lean -- standalone ND system
+* Cslib/Logics/Propositional/Metalogic/DeductionTheorem.lean -- deduction theorem
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL
+
+open Cslib.Logic
+
+variable {Atom : Type*}
+
+/-! ## Core ND Rules (Type-level) -/
+
+/-- **Implication Introduction** (→I): From `A :: Γ ⊢ B`, derive `Γ ⊢ A → B`.
+
+This is the deduction theorem, presented with the familiar ND name. -/
+noncomputable def impI {Γ : List (PL.Proposition Atom)}
+    {A B : PL.Proposition Atom}
+    (d : DerivationTree (A :: Γ) B) :
+    DerivationTree Γ (A.imp B) :=
+  deductionTheorem Γ A B d
+
+/-- **Implication Elimination** (→E / Modus Ponens):
+From `Γ ⊢ A → B` and `Γ ⊢ A`, derive `Γ ⊢ B`. -/
+def impE {Γ : List (PL.Proposition Atom)}
+    {A B : PL.Proposition Atom}
+    (d₁ : DerivationTree Γ (A.imp B))
+    (d₂ : DerivationTree Γ A) :
+    DerivationTree Γ B :=
+  DerivationTree.modus_ponens Γ A B d₁ d₂
+
+/-- **Ex Falso Quodlibet** (⊥E): From `Γ ⊢ ⊥`, derive `Γ ⊢ A`.
+
+Uses the EFQ axiom (`⊥ → A`) combined with modus ponens. -/
+def botE {Γ : List (PL.Proposition Atom)}
+    {A : PL.Proposition Atom}
+    (d : DerivationTree Γ Proposition.bot) :
+    DerivationTree Γ A :=
+  DerivationTree.modus_ponens Γ Proposition.bot A
+    (DerivationTree.weakening [] Γ _
+      (DerivationTree.ax [] _ (.efq A))
+      (fun _ h => nomatch h))
+    d
+
+/-- **Assumption**: If `φ ∈ Γ`, then `Γ ⊢ φ`. -/
+def assume {Γ : List (PL.Proposition Atom)}
+    {φ : PL.Proposition Atom}
+    (h : φ ∈ Γ) :
+    DerivationTree Γ φ :=
+  DerivationTree.assumption Γ φ h
+
+/-- **Axiom Rule**: If `φ` is an axiom schema, then `Γ ⊢ φ`. -/
+def axiomRule {Γ : List (PL.Proposition Atom)}
+    {φ : PL.Proposition Atom}
+    (h : PropositionalAxiom φ) :
+    DerivationTree Γ φ :=
+  DerivationTree.ax Γ φ h
+
+/-! ## Derived Rules (Type-level) -/
+
+/-- **Cut Rule**: From `Γ ⊢ A` and `A :: Δ ⊢ B`, derive `Γ ++ Δ ⊢ B`.
+
+Uses the deduction theorem to discharge `A` from the second derivation,
+then modus ponens with the first, combined via weakening. -/
+noncomputable def hilbertCut {Γ Δ : List (PL.Proposition Atom)}
+    {A B : PL.Proposition Atom}
+    (d₁ : DerivationTree Γ A)
+    (d₂ : DerivationTree (A :: Δ) B) :
+    DerivationTree (Γ ++ Δ) B := by
+  -- Deduction theorem: Δ ⊢ A → B
+  have h_dt := deductionTheorem Δ A B d₂
+  -- Weaken d₁ to Γ ++ Δ
+  have h_d₁ := DerivationTree.weakening Γ (Γ ++ Δ) A d₁
+    (fun x hx => List.mem_append.mpr (Or.inl hx))
+  -- Weaken h_dt to Γ ++ Δ
+  have h_dt' := DerivationTree.weakening Δ (Γ ++ Δ) (A.imp B) h_dt
+    (fun x hx => List.mem_append.mpr (Or.inr hx))
+  -- MP: (Γ ++ Δ) ⊢ B
+  exact DerivationTree.modus_ponens (Γ ++ Δ) A B h_dt' h_d₁
+
+/-- **Weakening**: From `Γ ⊢ φ` and `Γ ⊆ Δ`, derive `Δ ⊢ φ`.
+
+Direct wrapper around the `DerivationTree.weakening` constructor. -/
+def hilbertWeakening {Γ Δ : List (PL.Proposition Atom)}
+    {φ : PL.Proposition Atom}
+    (d : DerivationTree Γ φ)
+    (h : ∀ x ∈ Γ, x ∈ Δ) :
+    DerivationTree Δ φ :=
+  DerivationTree.weakening Γ Δ φ d h
+
+/-! ## Prop-level (`Deriv`) Versions -/
+
+/-- Implication introduction at the `Deriv` level. -/
+theorem impIDeriv {Γ : List (PL.Proposition Atom)}
+    {A B : PL.Proposition Atom}
+    (h : Deriv (A :: Γ) B) : Deriv Γ (A.imp B) := by
+  obtain ⟨d⟩ := h
+  exact ⟨impI d⟩
+
+/-- Implication elimination at the `Deriv` level. -/
+theorem impEDeriv {Γ : List (PL.Proposition Atom)}
+    {A B : PL.Proposition Atom}
+    (h₁ : Deriv Γ (A.imp B)) (h₂ : Deriv Γ A) :
+    Deriv Γ B := by
+  obtain ⟨d₁⟩ := h₁; obtain ⟨d₂⟩ := h₂
+  exact ⟨impE d₁ d₂⟩
+
+/-- Ex falso quodlibet at the `Deriv` level. -/
+theorem botEDeriv {Γ : List (PL.Proposition Atom)}
+    {A : PL.Proposition Atom}
+    (h : Deriv Γ Proposition.bot) : Deriv Γ A := by
+  obtain ⟨d⟩ := h
+  exact ⟨botE d⟩
+
+/-- Cut rule at the `Deriv` level. -/
+theorem hilbertCutDeriv
+    {Γ Δ : List (PL.Proposition Atom)}
+    {A B : PL.Proposition Atom}
+    (h₁ : Deriv Γ A) (h₂ : Deriv (A :: Δ) B) :
+    Deriv (Γ ++ Δ) B := by
+  obtain ⟨d₁⟩ := h₁; obtain ⟨d₂⟩ := h₂
+  exact ⟨hilbertCut d₁ d₂⟩
+
+/-- Weakening at the `Deriv` level. -/
+theorem hilbertWeakeningDeriv
+    {Γ Δ : List (PL.Proposition Atom)}
+    {φ : PL.Proposition Atom}
+    (h : Deriv Γ φ) (hsub : ∀ x ∈ Γ, x ∈ Δ) :
+    Deriv Δ φ := by
+  obtain ⟨d⟩ := h
+  exact ⟨hilbertWeakening d hsub⟩
+
+/-! ## Substitution -/
+
+/-- Helper: axiom schemata are preserved under substitution. -/
+theorem subst_preserves_axiom
+    {Atom : Type u} {Atom' : Type u}
+    {φ : PL.Proposition Atom}
+    (h : PropositionalAxiom φ) (f : Atom → PL.Proposition Atom') :
+    PropositionalAxiom (φ.subst f) := by
+  cases h with
+  | implyK a b => exact .implyK (a.subst f) (b.subst f)
+  | implyS a b c => exact .implyS (a.subst f) (b.subst f) (c.subst f)
+  | efq a => exact .efq (a.subst f)
+  | peirce a b => exact .peirce (a.subst f) (b.subst f)
+
+/-- Transport a derivation tree along an atom substitution.
+
+If `Γ ⊢ φ` then `Γ.map (·.subst f) ⊢ φ.subst f`. -/
+def hilbertSubstitution
+    {Atom : Type u} {Atom' : Type u} [DecidableEq Atom']
+    {Γ : List (PL.Proposition Atom)} {φ : PL.Proposition Atom}
+    (d : DerivationTree Γ φ) (f : Atom → PL.Proposition Atom') :
+    DerivationTree (Γ.map (·.subst f)) (φ.subst f) :=
+  match d with
+  | .ax Γ' _ h_ax =>
+    .ax (Γ'.map (·.subst f)) _ (subst_preserves_axiom h_ax f)
+  | .assumption _ ψ h_mem =>
+    .assumption _ _ (List.mem_map.mpr ⟨ψ, h_mem, rfl⟩)
+  | .modus_ponens _ _ _ d₁ d₂ =>
+    .modus_ponens _ _ _ (hilbertSubstitution d₁ f) (hilbertSubstitution d₂ f)
+  | .weakening _ _ _ d' h_sub =>
+    .weakening _ _ _ (hilbertSubstitution d' f) (fun _ hx =>
+      let ⟨y, hy_mem, hy_eq⟩ := List.mem_map.mp hx
+      List.mem_map.mpr ⟨y, h_sub y hy_mem, hy_eq⟩)
+
+/-- Substitution at the `Deriv` level. -/
+theorem hilbertSubstitutionDeriv
+    {Atom : Type u} {Atom' : Type u} [DecidableEq Atom']
+    {Γ : List (PL.Proposition Atom)} {φ : PL.Proposition Atom}
+    (h : Deriv Γ φ) (f : Atom → PL.Proposition Atom') :
+    Deriv (Γ.map (·.subst f)) (φ.subst f) := by
+  obtain ⟨d⟩ := h
+  exact ⟨hilbertSubstitution d f⟩
+
+end Cslib.Logic.PL
diff --git a/Cslib/Logics/Propositional/ProofSystem/Axioms.lean b/Cslib/Logics/Propositional/ProofSystem/Axioms.lean
new file mode 100644
index 000000000..e26bc6242
--- /dev/null
+++ b/Cslib/Logics/Propositional/ProofSystem/Axioms.lean
@@ -0,0 +1,55 @@
+/-
+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
+
+public import Cslib.Logics.Propositional.Defs
+
+/-! # Axiom Schemata for Propositional Logic
+
+This module defines the axiom schemata for the propositional Hilbert-style proof system.
+
+## Main Definition
+
+- `PropositionalAxiom`: An inductive type enumerating the 4 axiom schemata of classical
+  propositional logic: `implyK` (weakening), `implyS` (distribution), `efq` (ex falso),
+  and `peirce` (Peirce's law / classical reasoning).
+
+## References
+
+* Cslib/Logics/Modal/Metalogic/DerivationTree.lean -- modal axiom pattern (first 4 constructors)
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL
+
+variable {Atom : Type*}
+
+/-- Axiom schemata for classical propositional logic.
+
+The 4 axiom constructors are:
+- **implyK** (weakening): `φ → (ψ → φ)`
+- **implyS** (distribution): `(φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))`
+- **efq** (ex falso quodlibet): `⊥ → φ`
+- **peirce** (Peirce's law): `((φ → ψ) → φ) → φ`
+
+Together with modus ponens, these axioms characterize classical propositional logic. -/
+inductive PropositionalAxiom : PL.Proposition Atom → Prop where
+  /-- Weakening: `φ → (ψ → φ)` -/
+  | implyK (φ ψ : PL.Proposition Atom) :
+      PropositionalAxiom (φ.imp (ψ.imp φ))
+  /-- Distribution: `(φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))` -/
+  | implyS (φ ψ χ : PL.Proposition Atom) :
+      PropositionalAxiom ((φ.imp (ψ.imp χ)).imp ((φ.imp ψ).imp (φ.imp χ)))
+  /-- Ex falso quodlibet: `⊥ → φ` -/
+  | efq (φ : PL.Proposition Atom) :
+      PropositionalAxiom (Proposition.bot.imp φ)
+  /-- Peirce's law / DNE: `((φ → ψ) → φ) → φ` -/
+  | peirce (φ ψ : PL.Proposition Atom) :
+      PropositionalAxiom (((φ.imp ψ).imp φ).imp φ)
+
+end Cslib.Logic.PL
diff --git a/Cslib/Logics/Propositional/ProofSystem/Derivation.lean b/Cslib/Logics/Propositional/ProofSystem/Derivation.lean
new file mode 100644
index 000000000..8448065b0
--- /dev/null
+++ b/Cslib/Logics/Propositional/ProofSystem/Derivation.lean
@@ -0,0 +1,147 @@
+/-
+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
+
+public import Cslib.Logics.Propositional.ProofSystem.Axioms
+public import Cslib.Foundations.Logic.Metalogic.Consistency
+
+/-! # DerivationTree -- Syntactic Proof System for Propositional Logic
+
+This module defines a Hilbert-style syntactic proof system for classical propositional
+logic, parameterized over an atom type. The key components are:
+
+- `DerivationTree`: An inductive type with 4 constructors representing proof trees.
+- `Deriv`: A `Prop`-level wrapper (`Nonempty (DerivationTree Γ φ)`).
+- `Derivable`: Derivability from the empty context.
+- `propDerivationSystem`: A `DerivationSystem (PL.Proposition Atom)` instance connecting
+  to the generic MCS framework from `Consistency.lean`.
+
+## Design
+
+`DerivationTree` is a `Type` (not a `Prop`) to enable pattern matching and computable
+height functions. The `Deriv` wrapper provides the `Prop` version for the generic
+`DerivationSystem`.
+
+Unlike the modal `DerivationTree`, the propositional version has only 4 constructors
+(no necessitation rule), since propositional logic has no modal operators.
+
+## References
+
+* Cslib/Logics/Modal/Metalogic/DerivationTree.lean -- modal derivation tree pattern
+* Cslib/Foundations/Logic/Metalogic/Consistency.lean -- generic MCS API
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL
+
+open Cslib.Logic
+
+variable {Atom : Type*}
+
+/-! ## Derivation Trees -/
+
+/-- Derivation tree for classical propositional logic.
+
+`DerivationTree Γ φ` represents a proof tree showing that formula `φ` is derivable
+from context `Γ`. Since it is a `Type` (not `Prop`), we can pattern match on it
+for computable functions like `height`.
+
+The 4 constructors are:
+1. **ax**: Any axiom instance is derivable from any context.
+2. **assumption**: Any formula in the context is derivable.
+3. **modus_ponens**: From `Γ ⊢ φ → ψ` and `Γ ⊢ φ`, derive `Γ ⊢ ψ`.
+4. **weakening**: From `Γ ⊢ φ` and `Γ ⊆ Δ`, derive `Δ ⊢ φ`. -/
+inductive DerivationTree : List (PL.Proposition Atom) → PL.Proposition Atom → Type _ where
+  /-- Axiom rule: axiom schema instances are derivable from any context. -/
+  | ax (Γ : List (PL.Proposition Atom)) (φ : PL.Proposition Atom)
+      (h : PropositionalAxiom φ) : DerivationTree Γ φ
+  /-- Assumption rule: formulas in the context are derivable. -/
+  | assumption (Γ : List (PL.Proposition Atom)) (φ : PL.Proposition Atom)
+      (h : φ ∈ Γ) : DerivationTree Γ φ
+  /-- Modus ponens: from `Γ ⊢ φ → ψ` and `Γ ⊢ φ`, derive `Γ ⊢ ψ`. -/
+  | modus_ponens (Γ : List (PL.Proposition Atom)) (φ ψ : PL.Proposition Atom)
+      (d₁ : DerivationTree Γ (φ.imp ψ))
+      (d₂ : DerivationTree Γ φ) : DerivationTree Γ ψ
+  /-- Weakening: from `Γ ⊢ φ` and `Γ ⊆ Δ`, derive `Δ ⊢ φ`. -/
+  | weakening (Γ Δ : List (PL.Proposition Atom)) (φ : PL.Proposition Atom)
+      (d : DerivationTree Γ φ)
+      (h : ∀ x ∈ Γ, x ∈ Δ) : DerivationTree Δ φ
+
+namespace DerivationTree
+
+/-! ## Height Measure -/
+
+/-- Computable height function for derivation trees.
+
+Used for well-founded recursion in the deduction theorem proof. -/
+def height : DerivationTree Γ φ → Nat
+  | .ax _ _ _ => 0
+  | .assumption _ _ _ => 0
+  | .modus_ponens _ _ _ d₁ d₂ => 1 + max d₁.height d₂.height
+  | .weakening _ _ _ d _ => 1 + d.height
+
+/-! ## Height Properties -/
+
+theorem height_modus_ponens_left {Γ : List (PL.Proposition Atom)} {φ ψ : PL.Proposition Atom}
+    (d₁ : DerivationTree Γ (φ.imp ψ)) (d₂ : DerivationTree Γ φ) :
+    d₁.height < (modus_ponens Γ φ ψ d₁ d₂).height := by
+  simp [height]; omega
+
+theorem height_modus_ponens_right {Γ : List (PL.Proposition Atom)} {φ ψ : PL.Proposition Atom}
+    (d₁ : DerivationTree Γ (φ.imp ψ)) (d₂ : DerivationTree Γ φ) :
+    d₂.height < (modus_ponens Γ φ ψ d₁ d₂).height := by
+  simp [height]; omega
+
+theorem height_weakening {Γ Δ : List (PL.Proposition Atom)} {φ : PL.Proposition Atom}
+    (d : DerivationTree Γ φ) (h : ∀ x ∈ Γ, x ∈ Δ) :
+    d.height < (weakening Γ Δ φ d h).height := by
+  simp [height]
+
+end DerivationTree
+
+/-! ## Derivability (Prop wrapper) -/
+
+/-- `Deriv Γ φ` holds iff there exists a derivation tree deriving `φ` from `Γ`.
+This is the `Prop`-level wrapper used by the generic `DerivationSystem`. -/
+def Deriv (Γ : List (PL.Proposition Atom)) (φ : PL.Proposition Atom) : Prop :=
+  Nonempty (DerivationTree Γ φ)
+
+/-- `Derivable φ` means `φ` is derivable from the empty context. -/
+def Derivable (φ : PL.Proposition Atom) : Prop :=
+  Deriv [] φ
+
+/-! ## Basic Combinators -/
+
+theorem mp_deriv {Γ : List (PL.Proposition Atom)} {φ ψ : PL.Proposition Atom}
+    (h₁ : Deriv Γ (φ.imp ψ)) (h₂ : Deriv Γ φ) : Deriv Γ ψ := by
+  obtain ⟨d₁⟩ := h₁; obtain ⟨d₂⟩ := h₂
+  exact ⟨.modus_ponens Γ φ ψ d₁ d₂⟩
+
+theorem weakening_deriv {Γ Δ : List (PL.Proposition Atom)} {φ : PL.Proposition Atom}
+    (h : Deriv Γ φ) (hsub : ∀ x ∈ Γ, x ∈ Δ) : Deriv Δ φ := by
+  obtain ⟨d⟩ := h
+  exact ⟨.weakening Γ Δ φ d hsub⟩
+
+theorem assumption_deriv {Γ : List (PL.Proposition Atom)} {φ : PL.Proposition Atom}
+    (h : φ ∈ Γ) : Deriv Γ φ :=
+  ⟨.assumption Γ φ h⟩
+
+/-! ## DerivationSystem Instance -/
+
+/-- The propositional derivation system, connecting the propositional proof system to the
+generic MCS framework from `Consistency.lean`.
+
+This provides `Deriv`, `weakening`, `assumption`, and `mp` as required by
+`DerivationSystem (PL.Proposition Atom)`. -/
+def propDerivationSystem : Metalogic.DerivationSystem (PL.Proposition Atom) where
+  Deriv := Deriv
+  weakening := fun hd hsub => weakening_deriv hd hsub
+  assumption := fun hmem => assumption_deriv hmem
+  mp := fun h₁ h₂ => mp_deriv h₁ h₂
+
+end Cslib.Logic.PL
diff --git a/Cslib/Logics/Propositional/ProofSystem/Instances.lean b/Cslib/Logics/Propositional/ProofSystem/Instances.lean
new file mode 100644
index 000000000..3180b6068
--- /dev/null
+++ b/Cslib/Logics/Propositional/ProofSystem/Instances.lean
@@ -0,0 +1,90 @@
+/-
+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
+
+public import Cslib.Logics.Propositional.ProofSystem.Derivation
+public import Cslib.Foundations.Logic.ProofSystem
+
+/-! # Instance Registration for Propositional.HilbertCl
+
+This module registers `InferenceSystem`, `ModusPonens`, all `HasAxiom*`,
+and `PropositionalHilbert` instances for the `Propositional.HilbertCl` tag type,
+connecting the abstract typeclass hierarchy to the concrete derivation tree.
+
+## Architecture
+
+The `InferenceSystem` instance maps `HilbertCl⇓φ` to `DerivationTree [] φ`.
+This makes `InferenceSystem.DerivableIn HilbertCl φ = Nonempty (DerivationTree [] φ)`.
+
+Since `PropositionalConnectives (PL.Proposition Atom)` maps `bot := .bot` and
+`imp := .imp`, the generic axiom formulas (`Axioms.ImplyK`, etc.) are definitionally
+equal to the concrete formulas used in `PropositionalAxiom`.
+
+## References
+
+* Cslib/Logics/Bimodal/ProofSystem/Instances.lean -- bimodal instance pattern
+* Cslib/Foundations/Logic/ProofSystem.lean -- typeclass hierarchy
+-/
+
+@[expose] public section
+
+
+open Cslib.Logic
+
+variable {Atom : Type*} [DecidableEq Atom]
+
+namespace Cslib.Logic.PL
+
+section PropositionalInstances
+
+/-! ## InferenceSystem Instance -/
+
+instance : InferenceSystem Propositional.HilbertCl
+    (PL.Proposition Atom) where
+  derivation φ := PL.DerivationTree
+    ([] : List (PL.Proposition Atom)) φ
+
+/-! ## ModusPonens Instance -/
+
+instance :
+    ModusPonens Propositional.HilbertCl
+      (F := PL.Proposition Atom) where
+  mp := fun h1 h2 => by
+    obtain ⟨d1⟩ := h1; obtain ⟨d2⟩ := h2
+    exact ⟨PL.DerivationTree.modus_ponens [] _ _ d1 d2⟩
+
+/-! ## Propositional Axiom Instances -/
+
+instance :
+    HasAxiomImplyK Propositional.HilbertCl
+      (F := PL.Proposition Atom) where
+  implyK := ⟨PL.DerivationTree.ax [] _ (.implyK _ _)⟩
+
+instance :
+    HasAxiomImplyS Propositional.HilbertCl
+      (F := PL.Proposition Atom) where
+  implyS := ⟨PL.DerivationTree.ax [] _ (.implyS _ _ _)⟩
+
+instance :
+    HasAxiomEFQ Propositional.HilbertCl
+      (F := PL.Proposition Atom) where
+  efq := ⟨PL.DerivationTree.ax [] _ (.efq _)⟩
+
+instance :
+    HasAxiomPeirce Propositional.HilbertCl
+      (F := PL.Proposition Atom) where
+  peirce := ⟨PL.DerivationTree.ax [] _ (.peirce _ _)⟩
+
+/-! ## PropositionalHilbert Instance -/
+
+instance :
+    PropositionalHilbert Propositional.HilbertCl
+      (F := PL.Proposition Atom) where
+
+end PropositionalInstances
+
+end Cslib.Logic.PL