diff --git a/Cslib.lean b/Cslib.lean
index 6e70be7b9..e1389503e 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -69,6 +69,7 @@ public import Cslib.Foundations.Data.RelatesInSteps
 public import Cslib.Foundations.Data.Set.Saturation
 public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
+public import Cslib.Foundations.Logic.Connectives
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Cslib.Foundations.Logic.LogicalEquivalence
 public import Cslib.Foundations.Relation.Attr
diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean
new file mode 100644
index 000000000..18a847236
--- /dev/null
+++ b/Cslib/Foundations/Logic/Connectives.lean
@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Benjamin Brast-McKie
+-/
+
+module
+
+import Cslib.Init
+
+/-! # Connective Typeclasses for Propositional Logic
+
+This module defines a typeclass hierarchy for propositional logical connectives. Each formula
+type registers itself as an instance of the appropriate connective class, enabling polymorphic
+axiom definitions and notation that work uniformly across different formula types.
+
+## Design
+
+The hierarchy adopts five constructors `{atom, bot, imp, and, or}`,
+following the operator-typeclass direction of fmontesi's PR #607 (one class per operator):
+- **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr`
+- **Bundled class**: `PropositionalConnectives` (extends `HasBot` and `HasImp`)
+
+Conjunction (`HasAnd`) and disjunction (`HasOr`) are treated as independent primitives rather
+than Łukasiewicz-derived connectives. The classical encodings `φ ∧ ψ := ¬(φ → ¬ψ)` and
+`φ ∨ ψ := ¬φ → ψ` are only propositionally equivalent to `∧` and `∨` in classical logic
+([Avigad2022]); they fail in intuitionistic and minimal logic. Making `and`
+and `or` primitive via `HasAnd`/`HasOr` supports all three logic strengths with a single
+typeclass hierarchy.
+
+Negation and verum stay derived: each concrete formula type defines `neg φ := φ → ⊥` and
+`top := ⊥ → ⊥` as `abbrev`s, which are valid in minimal, intuitionistic, and classical logic
+alike, so no typeclass machinery is needed for them.
+
+## References
+
+* [J. Avigad, *Mathematical Logic and Computation*][Avigad2022]
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- A type has a falsum (bottom) connective. -/
+class HasBot (F : Type*) where
+  /-- The falsum/bottom connective. -/
+  bot : F
+
+/-- A type has an implication connective. -/
+class HasImp (F : Type*) where
+  /-- The implication connective. -/
+  imp : F → F → F
+
+/-- A type has a conjunction connective. -/
+class HasAnd (F : Type*) where
+  /-- The conjunction connective. -/
+  and : F → F → F
+
+/-- A type has a disjunction connective. -/
+class HasOr (F : Type*) where
+  /-- The disjunction connective. -/
+  or : F → F → F
+
+/-- Propositional connectives: falsum and implication.
+
+`HasAnd` and `HasOr` are defined as standalone atomic classes in this module.
+When all four connectives are needed, use
+`[PropositionalConnectives F] [HasAnd F] [HasOr F]`. -/
+class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F
+
+end Cslib.Logic
diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean
index e9c603d91..2242eaa90 100644
--- a/Cslib/Logics/Propositional/Defs.lean
+++ b/Cslib/Logics/Propositional/Defs.lean
@@ -1,37 +1,47 @@
 /-
-Copyright (c) 2025 Thomas Waring. All rights reserved.
+Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Thomas Waring
+Authors: Thomas Waring, Benjamin Brast-McKie
 -/
 
 module
 
+import Cslib.Init
+public import Cslib.Foundations.Logic.Connectives
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Mathlib.Data.FunLike.Basic
-public import Mathlib.Data.Set.Image
+public import Mathlib.Data.Set.Basic
 public import Mathlib.Order.TypeTags
 
 /-! # Propositions and theories
 
 ## Main definitions
 
-- `Proposition` : the type of propositions over a given type of atom. This type has a `Bot`
-instance whenever `Atom` does, and a `Top` whenever `Atom` is inhabited.
+- `Proposition` : the type of propositions over a given type of atom. Primitives are `atom`,
+  `bot` (falsum), `imp` (implication), `and` (conjunction), and `or` (disjunction). Negation
+  (`neg`), verum (`top`), and biconditional (`iff`) are derived connectives (`abbrev`s). This
+  follows the natural deduction tradition ([Avigad2022]) in which `neg A` abbreviates `A → ⊥`
+  rather than being taken as primitive.
 - `Theory` : set of `Proposition`.
-- `IsIntuitionistic` : a theory is intuitionistic if it contains the principle of explosion.
-- `IsClassical` : an intuitionistic theory is classical if it further contains double negation
-elimination.
+- `IsIntuitionistic` : an inference system is intuitionistic if it derives the principle of
+  explosion.
+- `IsClassical` : an inference system is classical if it further derives double negation
+  elimination.
 - `Proposition.subst` : replace `atom x` in a `A : Proposition Atom` with `f x`, for a function
   `f : Atom → Proposition Atom'`. This induces a monad structure on `Proposition`, with
   `pure := Proposition.atom`. `Theory` is a functor, by mapping each proposition `A ∈ T` to
   `f <$> A`.
 - `Theory.intuitionisticCompletion` : the freely generated intuitionistic theory extending a given
-theory.
+  theory.
 
 ## Notation
 
 We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum,
 conjunction, disjunction, implication and negation.
+
+## References
+
+* [J. Avigad, *Mathematical Logic and Computation*][Avigad2022]
 -/
 
 @[expose] public section
@@ -42,44 +52,61 @@ variable {Atom : Type u} [DecidableEq Atom]
 
 namespace Cslib.Logic.PL
 
-/-- Propositions. -/
+/-- Propositions. Primitives are atoms, falsum, implication, conjunction, and disjunction. -/
 inductive Proposition (Atom : Type u) : Type u where
   /-- Propositional atoms -/
   | atom (x : Atom)
+  /-- Falsum / bottom -/
+  | bot
+  /-- Implication -/
+  | imp (a b : Proposition Atom)
   /-- Conjunction -/
   | and (a b : Proposition Atom)
   /-- Disjunction -/
   | or (a b : Proposition Atom)
-  /-- Implication -/
-  | impl (a b : Proposition Atom)
 deriving DecidableEq, BEq
 
-instance instBotProposition [Bot Atom] : Bot (Proposition Atom) := ⟨.atom ⊥⟩
-instance instInhabitedOfBot [Bot Atom] : Inhabited Atom := ⟨⊥⟩
+/-- Negation as a derived connective: ¬A := A → ⊥ -/
+abbrev Proposition.neg : Proposition Atom → Proposition Atom := (Proposition.imp · .bot)
 
-/-- We view negation as a defined connective ~A := A → ⊥ -/
-abbrev Proposition.neg [Bot Atom] : Proposition Atom → Proposition Atom := (Proposition.impl · ⊥)
+/-- Verum / top as a derived connective: ⊤ := ⊥ → ⊥ -/
+abbrev Proposition.top : Proposition Atom := .imp .bot .bot
 
-/-- A fixed choice of a derivable proposition (of course any two are equivalent). -/
-abbrev Proposition.top [Inhabited Atom] : Proposition Atom := impl (.atom default) (.atom default)
+/-- Biconditional as a derived connective: A ↔ B := (A → B) ∧ (B → A) -/
+abbrev Proposition.iff (A B : Proposition Atom) : Proposition Atom :=
+  (A.imp B).and (B.imp A)
 
-instance instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top⟩
-
-example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl
+instance : Bot (Proposition Atom) := ⟨.bot⟩
+instance : Top (Proposition Atom) := ⟨.top⟩
 
 @[inherit_doc] scoped infix:36 " ∧ " => Proposition.and
 @[inherit_doc] scoped infix:35 " ∨ " => Proposition.or
-@[inherit_doc] scoped infix:30 " → " => Proposition.impl
+@[inherit_doc] scoped infix:30 " → " => Proposition.imp
+@[inherit_doc] scoped infix:20 " ↔ " => Proposition.iff
 @[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg
 
+/-- Register `Proposition` as an instance of `PropositionalConnectives`. -/
+instance : PropositionalConnectives (Proposition Atom) where
+  bot := .bot
+  imp := .imp
+
+/-- Register `HasAnd` instance for `Proposition`. -/
+instance : HasAnd (Proposition Atom) where
+  and := .and
+
+/-- Register `HasOr` instance for `Proposition`. -/
+instance : HasOr (Proposition Atom) where
+  or := .or
+
 /-- Substitute each atom in a proposition for a proposition, possibly changing the atomic
 language. -/
 def Proposition.subst {Atom Atom' : Type u} (f : Atom → Proposition Atom') :
     Proposition Atom → Proposition Atom'
   | atom x => f x
-  | and A B => (A.subst f) ∧ (B.subst f)
-  | or A B => (A.subst f) ∨ (B.subst f)
-  | impl A B => (A.subst f) → (B.subst f)
+  | bot => .bot
+  | imp A B => .imp (A.subst f) (B.subst f)
+  | and A B => .and (A.subst f) (B.subst f)
+  | or A B => .or (A.subst f) (B.subst f)
 
 -- This is probably a lawful monad, but that doesn't seem to be important.
 instance : Monad Proposition where
@@ -99,24 +126,28 @@ instance : Functor Theory where
   map f := Set.image (f <$> ·)
 
 /-- The empty theory corresponds to minimal propositional logic. -/
-abbrev MPL (Atom : Type u) : Theory (Atom) := ∅
+abbrev MPL : Theory (Atom) := ∅
 
 /-- Intuitionistic propositional logic adds the principle of explosion (ex falso quodlibet). -/
-abbrev IPL (Atom : Type u) [Bot Atom] : Theory Atom := {⊥ → A | A : Proposition Atom}
+abbrev IPL : Theory Atom :=
+  Set.range (Proposition.imp ⊥ ·)
 
 omit [DecidableEq Atom] in
-lemma efq_mem_ipl [Bot Atom] (A : Proposition Atom) : (⊥ → A) ∈ IPL Atom := ⟨A, rfl⟩
-
-/-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/
-@[reducible]
-def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) :=
-  (WithBot.some <$> T) ∪ IPL (WithBot Atom)
+lemma efq_mem_ipl (A : Proposition Atom) : (⊥ → A) ∈ IPL (Atom := Atom) := ⟨A, rfl⟩
 
 /-- Classical logic further adds double negation elimination. -/
-abbrev CPL (Atom : Type u) [Bot Atom] : Theory Atom := {¬¬A → A | A : Proposition Atom}
+abbrev CPL : Theory Atom :=
+  Set.range (fun (A : Proposition Atom) ↦ ¬¬A → A)
 
 omit [DecidableEq Atom] in
-lemma dne_mem_cpl [Bot Atom] (A : Proposition Atom) : (¬¬A → A) ∈ CPL Atom := ⟨A, rfl⟩
+lemma dne_mem_cpl (A : Proposition Atom) : (¬¬A → A) ∈ CPL (Atom := Atom) := ⟨A, rfl⟩
+
+/-- Extend a theory `T` to an intuitionistic theory over a larger atom type by adding the principle
+of explosion. The atom type is extended with `WithBot` to ensure the result is over a strictly
+larger language. -/
+@[reducible]
+def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) :=
+  (WithBot.some <$> T) ∪ IPL
 
 open InferenceSystem
 
@@ -124,16 +155,16 @@ open InferenceSystem
 generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an
 implication connective. -/
 @[scoped grind]
-class IsIntuitionistic (Atom : Type u) [Bot Atom] (S : Type*)
+class IsIntuitionistic (Atom : Type u) (S : Type*)
     [InferenceSystem S (Proposition Atom)] where
-  /-- The principle of explosion (ex falso quolibet). -/
+  /-- The principle of explosion (ex falso quodlibet). -/
   efq (A : Proposition Atom) : S⇓(⊥ → A)
 
 /-- An inference system is classical if it validates double-negation elimination. TODO: this should
 be generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an
 implication connective. -/
 @[scoped grind]
-class IsClassical (Atom : Type u) [Bot Atom] (S : Type*)
+class IsClassical (Atom : Type u) (S : Type*)
     [InferenceSystem S (Proposition Atom)] where
   /-- Double-negation elimination. -/
   dne (A : Proposition Atom) : S⇓(¬¬A → A)
diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
index 560ecb69e..51ac2669a 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,21 +42,20 @@ 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),
+conjunction introduction and elimination (×2), disjunction introduction (×2) and elimination,
+and implication introduction and elimination — 10 constructors in total. Ex falso quodlibet
+(bottom elimination) is a derived rule requiring `[IsIntuitionistic T]`.
+
+Logic strength is controlled by the theory parameter:
+- `MPL` (minimal propositional logic, see [Avigad2022] §3): no axioms beyond the
+  10 primitive rules; bottom has no special status.
+- `IPL` (intuitionistic propositional logic): adds the principle of explosion `⊥ → A`.
+- `CPL` (classical propositional logic): adds double negation elimination `¬¬A → A`.
 
 ## References
 
-- Dag Prawitz, *Natural Deduction: a proof-theoretical study*.
-- The sequent-style natural deduction I present here doesn't seem to be common, but it is tersely
-presented in §10.4 of Troelstra & van Dalen's *Constructivism in Mathematics: an introduction*, and
-in §2.2 of Sorensen & Urzyczyn's *Lectures on the Curry-Howard Isomorphism*. (Suggestions of better
-references welcome!)
+* [J. Avigad, *Mathematical Logic and Computation*][Avigad2022]
 -/
 
 @[expose] public section
@@ -83,31 +82,38 @@ 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, conjunction intro/elim,
+disjunction intro/elim, and implication intro/elim.
+Ex falso quodlibet (bottom elimination) is a derived rule requiring `[IsIntuitionistic T]`. -/
 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} :
+  | andI {A B : Proposition Atom} (Γ : Ctx 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)
+  /-- Left conjunction elimination -/
+  | andE1 {A B : Proposition Atom} (Γ : Ctx Atom) :
+      Derivation Γ (A ∧ B) → Derivation Γ A
+  /-- Right conjunction elimination -/
+  | andE2 {A B : Proposition Atom} (Γ : Ctx Atom) :
+      Derivation Γ (A ∧ B) → Derivation Γ B
+  /-- Left disjunction introduction -/
+  | orI1 {A B : Proposition Atom} (Γ : Ctx Atom) :
+      Derivation Γ A → Derivation Γ (A ∨ B)
+  /-- Right disjunction introduction -/
+  | orI2 {A B : Proposition Atom} (Γ : Ctx 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
+  | orE {A B C : Proposition Atom} (Γ : Ctx 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
 
 /-- Inference system for derivations under the theory `T`. -/
@@ -156,7 +162,7 @@ theorem Theory.equiv_iff {A B : Proposition Atom} :
     exact ⟨D, E⟩
 
 /-- Minimally equivalent propositions. -/
-abbrev Equiv : Proposition Atom → Proposition Atom → Prop := (MPL Atom).Equiv
+abbrev Equiv : Proposition Atom → Proposition Atom → Prop := MPL.Equiv
 
 @[inherit_doc]
 scoped infix:29 " ≡ " => Equiv
@@ -170,17 +176,17 @@ 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)
+  | @andI _ _ _ A B Γ D₁ D₂ => andI Δ (D₁.weak hTheory hCtx) (D₂.weak hTheory hCtx)
+  | @andE1 _ _ _ A B Γ D => andE1 Δ (D.weak hTheory hCtx)
+  | @andE2 _ _ _ A B Γ D => andE2 Δ (D.weak hTheory hCtx)
+  | @orI1 _ _ _ A B Γ D => orI1 Δ (D.weak hTheory hCtx)
+  | @orI2 _ _ _ A B Γ D => orI2 Δ (D.weak hTheory hCtx)
+  | @orE _ _ _ _ _ _ _ D DA DB =>
+    orE Δ (D.weak hTheory hCtx)
+      (DA.weak hTheory (Finset.insert_subset_insert _ hCtx))
+      (DB.weak hTheory (Finset.insert_subset_insert _ 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)
 
 /-- Weakening the theory only. -/
 def Theory.Derivation.weakTheory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom}
@@ -213,9 +219,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 +255,22 @@ 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
+  | @andI _ _ _ A' B' Γ E₁ E₂ => andI _ (E₁.subs Ds) (E₂.subs Ds)
+  | @andE1 _ _ _ A' B' Γ E => andE1 _ (E.subs Ds)
+  | @andE2 _ _ _ A' B' Γ E => andE2 _ (E.subs Ds)
+  | @orI1 _ _ _ A' B' Γ E => orI1 _ (E.subs Ds)
+  | @orI2 _ _ _ A' B' Γ E => orI2 _ (E.subs Ds)
+  | @orE _ _ _ A' B' C' Γ E EA EB => by
+    apply orE _ (E.subs Ds)
+    · rw [show insert A' (Γ \ Γ' ∪ Δ) = (insert A' Γ \ Γ') ∪ insert A' Δ by grind]
+      exact EA.subs Ds |>.weakCtx (by grind)
+    · rw [show insert B' (Γ \ Γ' ∪ Δ) = (insert B' Γ \ Γ') ∪ insert B' Δ by grind]
+      exact EB.subs Ds |>.weakCtx (by grind)
+  | @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)
 
 /-- Transport a derivation along a substitution of atoms. -/
 def Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom']
@@ -272,16 +278,17 @@ 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)
+  | andI _ D₁ D₂ => andI _ (D₁.substAtom f) (D₂.substAtom f)
+  | andE1 _ D => andE1 _ (D.substAtom f)
+  | andE2 _ D => andE2 _ (D.substAtom f)
+  | orI1 _ D => orI1 _ (D.substAtom f)
+  | orI2 _ D => orI2 _ (D.substAtom f)
+  | orE _ D DA DB =>
+    orE _ (D.substAtom f)
+      ((Finset.image_insert (· >>= f) _ _) ▸ (DA.substAtom f))
+      ((Finset.image_insert (· >>= f) _ _) ▸ (DB.substAtom f))
+  | impI _ D => impI _ <| (Finset.image_insert (· >>= f) _ _) ▸ (D.substAtom f)
+  | impE D E => impE (D.substAtom f) (E.substAtom f)
 
 theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom']
     {T : Theory Atom}
@@ -292,12 +299,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/Theory.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
index 8cdaa806d..cb75cc979 100644
--- a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
+++ b/Cslib/Logics/Propositional/NaturalDeduction/Theory.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
 
@@ -9,9 +9,12 @@ public import Cslib.Logics.Propositional.NaturalDeduction.Basic
 
 /-! # Results on propositional theories
 
-In this file we prove the expected results that `IPL Atom` is an intuitionistic theory, and
-`CPL Atom` is a classical theory. We provide derived rules for common intuitionistic and classical
+In this file we prove the expected results that `IPL` is an intuitionistic theory, and
+`CPL` is a classical theory. We provide derived rules for common intuitionistic and classical
 proof patterns.
+
+Since `Proposition` has `bot` as a primitive constructor, no `[Bot Atom]` constraint is needed:
+`⊥ : Proposition Atom` is always available as `.bot`.
 -/
 
 @[expose] public section
@@ -22,13 +25,24 @@ namespace Cslib.Logic.PL
 
 open Proposition Theory InferenceSystem DerivableIn Derivation IsIntuitionistic IsClassical
 
-variable {Atom : Type u} [DecidableEq Atom] [Bot Atom] {T : Theory Atom}
+variable {Atom : Type u} [DecidableEq Atom] {T : Theory Atom}
 
 namespace Theory
 
-instance instIsIntuitionisticIPL : IsIntuitionistic Atom (IPL Atom) where
+/-- `IPL` is intuitionistic: it contains `⊥ → A` for all `A`. -/
+instance instIsIntuitionisticIPL : IsIntuitionistic Atom (IPL (Atom := Atom)) where
   efq A := ax (efq_mem_ipl A)
 
+/-- `CPL` is classical: it contains `¬¬A → A` for all `A`. -/
+instance instIsClassicalCPL : IsClassical Atom (CPL (Atom := Atom)) where
+  dne A := ax (dne_mem_cpl A)
+
+/-- The intuitionistic completion of any theory is intuitionistic. -/
+instance instIsIntuitionisticIntuitionisticCompletion [DecidableEq (WithBot Atom)]
+    (T : Theory Atom) :
+    IsIntuitionistic (WithBot Atom) T.intuitionisticCompletion where
+  efq A := ax (Set.mem_union_right _ (efq_mem_ipl A))
+
 /-- Derivation of efq in an arbitrary context. -/
 def IsIntuitionistic.efqCtx [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Proposition Atom)
     : T⇓(Γ ⊢ ⊥ → A) := (efq A : T⇓(⊥ → A)).weakCtx (Finset.empty_subset Γ)
@@ -36,66 +50,71 @@ def IsIntuitionistic.efqCtx [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Propo
 /-- Efq as a derived rule. -/
 def IsIntuitionistic.efqRule [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Proposition Atom)
     (D : T⇓(Γ ⊢ ⊥)) : T⇓(Γ ⊢ A) :=
-  implE (A := ⊥) (efqCtx Γ A) D
+  impE (A := ⊥) (efqCtx Γ A) D
 
 /-- Prove any proposition from contradictory hypotheses. -/
 def IsIntuitionistic.contra [IsIntuitionistic Atom T] {Γ : Ctx Atom} (A B : Proposition Atom)
     (hΓ : A ∈ Γ) (hΓ' : (¬A) ∈ Γ) : T⇓(Γ ⊢ B) :=
-  efqRule Γ B <| implE (ass hΓ') (ass hΓ)
-
-instance instIsClassicalCPL : IsClassical Atom (CPL Atom) where
-  dne A := ax (dne_mem_cpl A)
+  efqRule Γ B <| impE (ass hΓ') (ass hΓ)
 
 /-- Proof by contradiction as a derived rule. -/
 def IsClassical.byContra [IsClassical Atom T] {Γ : Ctx Atom} {A : Proposition Atom}
     (D : T⇓(insert (¬ A) Γ ⊢ ⊥)) : T⇓(Γ ⊢ A) :=
-  implE (A := ¬¬A) ((dne A : T⇓(¬¬A → A)) |>.weakCtx <| Finset.empty_subset ..) D.implI
+  impE (A := ¬¬A) ((dne A : T⇓(¬¬A → A)) |>.weakCtx <| Finset.empty_subset ..) D.impI
 
 instance instIsIntuitionisticOfIsClassical [IsClassical Atom T] : IsIntuitionistic Atom T where
-  efq A := implI _ <| byContra <| ass (by grind)
+  efq A := impI _ <| byContra <| ass (by grind)
 
 /-- Law of excluded middle in a classical theory. -/
 def IsClassical.lem [IsClassical Atom T] (A : Proposition Atom) : T⇓(A ∨ ¬ A) := by
   apply byContra
-  apply implE (ass <| Finset.mem_insert_self ..)
-  apply orI₂; apply implI
-  apply implE (A := A ∨ ¬ A) (ass <| by grind)
-  exact orI₁ <| ass <| Finset.mem_insert_self ..
+  apply impE (ass <| Finset.mem_insert_self ..)
+  apply orI2
+  apply impI
+  apply impE (A := A ∨ ¬ A) (ass <| by grind)
+  apply orI1
+  exact ass <| Finset.mem_insert_self ..
 
 /-- Pierce's law in a classical theory. -/
 def IsClassical.pierce [IsClassical Atom T] (A B : Proposition Atom) : T⇓(((A → B) → A) → A) := by
-  apply implI; apply byContra
-  apply implE (ass <| Finset.mem_insert_self ..)
-  apply implE (A := A → B) (ass <| by grind); apply implI
+  apply impI; apply byContra
+  apply impE (ass <| Finset.mem_insert_self ..)
+  apply impE (A := A → B) (ass <| by grind); apply impI
   apply contra A B <;> grind
 
 /-- The axiom system consisting of instances of LEM. -/
-def LEM (Atom : Type u) [Bot Atom] : Theory Atom := {A ∨ ¬ A | A : Proposition Atom}
+def LEM : Theory Atom := {A ∨ ¬ A | A : Proposition Atom}
 
 omit [DecidableEq Atom] in
-lemma lem_mem_lem (A : Proposition Atom) : (A ∨ ¬ A) ∈ LEM Atom := ⟨A, rfl⟩
+lemma lem_mem_lem (A : Proposition Atom) : (A ∨ ¬ A) ∈ LEM (Atom := Atom) := ⟨A, rfl⟩
 
 /-- The axiom system consisting of instances of Pierce's law. -/
-def Pierce (Atom : Type u) : Theory Atom :=
+def Pierce : Theory Atom :=
   {((A → B) → A) → A | (A : Proposition Atom) (B : Proposition Atom)}
 
-omit [DecidableEq Atom] [Bot Atom] in
-lemma pierce_mem_pierce (A B : Proposition Atom) : (((A → B) → A) → A) ∈ Pierce Atom := ⟨A, B, rfl⟩
+omit [DecidableEq Atom] in
+lemma pierce_mem_pierce (A B : Proposition Atom) :
+    (((A → B) → A) → A) ∈ Pierce (Atom := Atom) := ⟨A, B, rfl⟩
 
-instance instIsClassicalLEM : IsClassical Atom (LEM Atom ∪ IPL Atom : Theory Atom) where
+instance instIsClassicalLEM : IsClassical Atom (LEM ∪ IPL : Theory Atom) where
   dne A := by
-    apply implI
-    apply orE (ax <| Set.mem_union_left _ <| lem_mem_lem A)
+    apply impI
+    apply orE
+    · exact ax <| Set.mem_union_left _ <| lem_mem_lem A
     · exact ass (Finset.mem_insert_self A _)
-    · apply implE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A))
-      apply implE (A := ¬ A) <;> exact ass (by grind)
+    · apply impE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A))
+      apply impE (A := ¬ A)
+      · exact ass (Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self _ _)))
+      · exact ass (Finset.mem_insert_self _ _)
 
-instance instIsClassicalPierce : IsClassical Atom (Pierce Atom ∪ IPL Atom : Theory Atom) where
+instance instIsClassicalPierce : IsClassical Atom (Pierce ∪ IPL : Theory Atom) where
   dne A := by
-    apply implI
-    apply implE (A := (A → ⊥) → A) (ax <| Set.mem_union_left _ <| pierce_mem_pierce A ⊥)
-    apply implI
-    apply implE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A))
-    apply implE (A := ¬ A) <;> exact ass (by grind)
+    apply impI
+    apply impE (A := (A → ⊥) → A) (ax <| Set.mem_union_left _ <| pierce_mem_pierce A ⊥)
+    apply impI
+    apply impE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A))
+    apply impE (A := ¬ A)
+    · exact ass (Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self _ _)))
+    · exact ass (Finset.mem_insert_self _ _)
 
 end Cslib.Logic.PL.Theory
diff --git a/references.bib b/references.bib
index 973371b65..8b4450757 100644
--- a/references.bib
+++ b/references.bib
@@ -1,3 +1,11 @@
+@book{Avigad2022,
+  author       = {Jeremy Avigad},
+  title        = {Mathematical Logic and Computation},
+  publisher    = {Cambridge University Press},
+  year         = {2022},
+  isbn         = {978-1-108-84072-1}
+}
+
 @inproceedings{Aceto1999,
   author       = {Luca Aceto and
                   Anna Ing{\'{o}}lfsd{\'{o}}ttir},