From ac9ee64e70b640e13853e5b78ba502edb042d210 Mon Sep 17 00:00:00 2001
From: benbrastmckie <benbrastmckie@gmail.com>
Date: Tue, 16 Jun 2026 12:53:54 -0700
Subject: [PATCH 1/5] feat(Logics/Propositional): five-primitive formula type
 with primitive bot

Add `bot` as a primitive constructor of `Proposition Atom`, eliminating all
`[Bot Atom]` constraints from propositional logic signatures.

- New `Connectives.lean`: typeclass hierarchy (HasBot, HasImp, HasAnd, HasOr)
- `Defs.lean`: five-primitive Proposition type with derived neg, top, iff
- `Basic.lean`: natural deduction with impI/impE, andI/andE1/andE2, orI1/orI2
- `Theory.lean`: remove [Bot Atom], add instIsIntuitionisticIntuitionisticCompletion
- Replace German-language references with Avigad 2022, Prawitz 1965
- Semantics files deferred to follow-up PR per reviewer request

Reconciles with merged PR #536 (InferenceSystem-parameterized typeclasses).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 Cslib.lean                                    |   1 +
 Cslib/Foundations/Logic/Connectives.lean      |  71 +++++++++
 Cslib/Logics/Propositional/Defs.lean          | 105 +++++++-----
 .../Propositional/NaturalDeduction/Basic.lean | 149 +++++++++---------
 .../NaturalDeduction/Theory.lean              |  91 ++++++-----
 references.bib                                |   8 +
 6 files changed, 280 insertions(+), 145 deletions(-)
 create mode 100644 Cslib/Foundations/Logic/Connectives.lean

diff --git a/Cslib.lean b/Cslib.lean
index eea1f4491..cb7464daa 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -73,6 +73,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..16d13e043
--- /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 a hybrid five-primitive propositional signature `{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..edf49f384 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,26 @@ 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⟩
+
+/-- 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
 
 open InferenceSystem
 
@@ -124,16 +153,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 984dc6e23..8fac9b0e6 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},

From 23f345d8e27f1f2f6b5dfa8d696b96dc1dd4dfd5 Mon Sep 17 00:00:00 2001
From: benbrastmckie <benbrastmckie@gmail.com>
Date: Wed, 17 Jun 2026 10:25:41 -0700
Subject: [PATCH 2/5] doc: fix docstrings for primitive bot perspective
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Update intuitionisticCompletion docstring — the old wording "Attach a
bottom element" was misleading since bot is already a constructor.
Change "five-primitive propositional signature" to "five constructors"
in Connectives.lean to avoid conflating generators with operations.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 Cslib/Foundations/Logic/Connectives.lean | 2 +-
 Cslib/Logics/Propositional/Defs.lean     | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean
index 16d13e043..18a847236 100644
--- a/Cslib/Foundations/Logic/Connectives.lean
+++ b/Cslib/Foundations/Logic/Connectives.lean
@@ -16,7 +16,7 @@ axiom definitions and notation that work uniformly across different formula type
 
 ## Design
 
-The hierarchy adopts a hybrid five-primitive propositional signature `{atom, bot, imp, and, or}`,
+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`)
diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean
index edf49f384..2242eaa90 100644
--- a/Cslib/Logics/Propositional/Defs.lean
+++ b/Cslib/Logics/Propositional/Defs.lean
@@ -142,7 +142,9 @@ abbrev CPL : Theory Atom :=
 omit [DecidableEq Atom] in
 lemma dne_mem_cpl (A : Proposition Atom) : (¬¬A → A) ∈ CPL (Atom := Atom) := ⟨A, rfl⟩
 
-/-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/
+/-- 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

From b0600aad7925e569fc370e6c67c88b5f46a6ec16 Mon Sep 17 00:00:00 2001
From: benbrastmckie <benbrastmckie@gmail.com>
Date: Mon, 29 Jun 2026 08:48:16 -0700
Subject: [PATCH 3/5] feat(Logics/Propositional): make IPL the base logic with
 primitive ex falso

Promote ex falso quodlibet (bottom-elimination) to an ungated primitive
constructor of the natural-deduction Derivation, so IPL is the base
propositional logic and the primitive bot constructor has an inference
rule. IPL becomes the empty base theory; CPL still adds double negation
elimination.

The minimal-logic (MPL) layer is deferred to a separate PR: this removes
MPL, the IsIntuitionistic typeclass, intuitionisticCompletion, and the
derived efq rules, keeping the classical layer (byContra/lem/pierce and
the IsClassical instances for CPL/LEM/Pierce) intact, re-proved via the
efq constructor.

Per reviewer feedback (Waring, CSLib Zulip 'Propositional Logic'):
- Drop the connective typeclasses (Foundations/Logic/Connectives.lean and
  its registration instances) -- a separate development handled via PR #607.
- Restore references (Gentzen 1935, Prawitz 1965, Troelstra-van Dalen 1988)
  and add the CSLib Zulip thread link.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019sHZHp7U5qSiEzioK1nGEH
---
 Cslib.lean                                    |  1 -
 Cslib/Foundations/Logic/Connectives.lean      | 71 -------------------
 Cslib/Logics/Propositional/Defs.lean          | 46 +-----------
 .../Propositional/NaturalDeduction/Basic.lean | 32 ++++++---
 .../NaturalDeduction/Theory.lean              | 49 +++----------
 references.bib                                | 48 ++++++++++---
 6 files changed, 76 insertions(+), 171 deletions(-)
 delete mode 100644 Cslib/Foundations/Logic/Connectives.lean

diff --git a/Cslib.lean b/Cslib.lean
index cb7464daa..eea1f4491 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -73,7 +73,6 @@ 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
deleted file mode 100644
index 18a847236..000000000
--- a/Cslib/Foundations/Logic/Connectives.lean
+++ /dev/null
@@ -1,71 +0,0 @@
-/-
-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 2242eaa90..60ca8f674 100644
--- a/Cslib/Logics/Propositional/Defs.lean
+++ b/Cslib/Logics/Propositional/Defs.lean
@@ -7,7 +7,6 @@ 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.Basic
@@ -23,16 +22,12 @@ public import Mathlib.Order.TypeTags
   follows the natural deduction tradition ([Avigad2022]) in which `neg A` abbreviates `A → ⊥`
   rather than being taken as primitive.
 - `Theory` : set of `Proposition`.
-- `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.
 
 ## Notation
 
@@ -85,19 +80,6 @@ instance : Top (Proposition Atom) := ⟨.top⟩
 @[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') :
@@ -125,15 +107,9 @@ protected def subst {Atom Atom' : Type u} (T : Theory Atom) (f : Atom → Propos
 instance : Functor Theory where
   map f := Set.image (f <$> ·)
 
-/-- The empty theory corresponds to minimal propositional logic. -/
-abbrev MPL : Theory (Atom) := ∅
-
-/-- Intuitionistic propositional logic adds the principle of explosion (ex falso quodlibet). -/
-abbrev IPL : Theory Atom :=
-  Set.range (Proposition.imp ⊥ ·)
-
-omit [DecidableEq Atom] in
-lemma efq_mem_ipl (A : Proposition Atom) : (⊥ → A) ∈ IPL (Atom := Atom) := ⟨A, rfl⟩
+/-- Intuitionistic propositional logic: the base theory. Ex falso quodlibet is a primitive
+inference rule (see `Derivation.efq`), so no explosion axioms are needed. -/
+abbrev IPL : Theory Atom := ∅
 
 /-- Classical logic further adds double negation elimination. -/
 abbrev CPL : Theory Atom :=
@@ -142,24 +118,8 @@ abbrev CPL : Theory Atom :=
 omit [DecidableEq Atom] in
 lemma dne_mem_cpl (A : Proposition Atom) : (¬¬A → A) ∈ CPL (Atom := Atom) := ⟨A, rfl⟩
 
-/-- Extend a theory `T` to an intuitionistic theory over a larger atom type by adding the principle
-of explosion. The atom type is extended with `WithBot` to ensure the result is over a strictly
-larger language. -/
-@[reducible]
-def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) :=
-  (WithBot.some <$> T) ∪ IPL
-
 open InferenceSystem
 
-/-- An inference system is intuitionistic if it derives ex falso quodlibet. TODO: this should be
-generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an
-implication connective. -/
-@[scoped grind]
-class IsIntuitionistic (Atom : Type u) (S : Type*)
-    [InferenceSystem S (Proposition Atom)] where
-  /-- 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. -/
diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
index 51ac2669a..7aa2996ab 100644
--- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
+++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
@@ -13,7 +13,7 @@ public import Mathlib.Data.Finset.Image
 
 /-! # Natural deduction for propositional logic
 
-We define, for minimal logic, deduction trees (a `Type`) and derivability (a `Prop`) relative to a
+We define deduction trees (a `Type`) and derivability (a `Prop`) relative to a
 `Theory` (set of propositions).
 
 ## Main definitions
@@ -44,18 +44,25 @@ abbreviates a derivation of `A` in the empty context: `T⇓(∅ ⊢ A)`.
 
 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]`.
+implication introduction and elimination, and ex falso quodlibet (⊥-elimination) — 11 constructors
+in total. IPL is the base logic; ex falso is primitive so no extra axioms are needed for explosion.
+Taking ex falso quodlibet as a primitive rule gives `⊥` an elimination rule rather than leaving it
+a constructor with no inference behaviour, following the natural-deduction tradition
+[Avigad2022], [TroelstraVanDalen1988], [Prawitz1965], [Gentzen1935].
 
 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`.
+- `IPL` (intuitionistic propositional logic): the base theory (empty); ex falso is a primitive rule.
 - `CPL` (classical propositional logic): adds double negation elimination `¬¬A → A`.
 
+The design of this module was discussed on the
+[CSLib Zulip thread on Propositional Logic](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Propositional.20Logic).
+
 ## References
 
 * [J. Avigad, *Mathematical Logic and Computation*][Avigad2022]
+* [A. S. Troelstra, D. van Dalen, *Constructivism in Mathematics*][TroelstraVanDalen1988]
+* [D. Prawitz, *Natural Deduction: A Proof-Theoretical Study*][Prawitz1965]
+* [G. Gentzen, *Investigations into Logical Deduction*][Gentzen1935]
 -/
 
 @[expose] public section
@@ -83,8 +90,7 @@ 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`. 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]`. -/
+disjunction intro/elim, implication intro/elim, and ex falso quodlibet (⊥-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
@@ -115,6 +121,9 @@ inductive Theory.Derivation {T : Theory Atom} : Ctx Atom → Proposition Atom 
   /-- Implication elimination (modus ponens) -/
   | impE {Γ : Ctx Atom} {A B : Proposition Atom} :
       Derivation Γ (A → B) → Derivation Γ A → Derivation Γ B
+  /-- Ex falso quodlibet (⊥-elimination). Makes IPL the base logic: from a derivation of
+  `⊥`, derive any proposition. -/
+  | efq {Γ : 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
@@ -161,8 +170,8 @@ theorem Theory.equiv_iff {A B : Proposition Atom} :
   · intro ⟨⟨D⟩, ⟨E⟩⟩
     exact ⟨D, E⟩
 
-/-- Minimally equivalent propositions. -/
-abbrev Equiv : Proposition Atom → Proposition Atom → Prop := MPL.Equiv
+/-- Equivalent propositions (over the base theory IPL). -/
+abbrev Equiv : Proposition Atom → Proposition Atom → Prop := IPL.Equiv
 
 @[inherit_doc]
 scoped infix:29 " ≡ " => Equiv
@@ -187,6 +196,7 @@ def Theory.Derivation.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposit
       (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)
+  | efq D => efq (D.weak hTheory hCtx)
 
 /-- Weakening the theory only. -/
 def Theory.Derivation.weakTheory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom}
@@ -271,6 +281,7 @@ def Theory.Derivation.subs {Γ Γ' Δ : Ctx Atom} {B : Proposition Atom}
     rw [show insert A' (Γ \ Γ' ∪ Δ) = (insert A' Γ \ Γ') ∪ insert A' Δ by grind]
     exact E.subs Ds |>.weakCtx (by grind)
   | impE E E' => impE (E.subs Ds) (E'.subs Ds)
+  | efq E => efq (E.subs Ds)
 
 /-- Transport a derivation along a substitution of atoms. -/
 def Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom']
@@ -289,6 +300,7 @@ def Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [Decida
       ((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)
+  | efq D => efq (D.substAtom f)
 
 theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom']
     {T : Theory Atom}
diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
index cb75cc979..68c061c94 100644
--- a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
+++ b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
@@ -9,9 +9,8 @@ public import Cslib.Logics.Propositional.NaturalDeduction.Basic
 
 /-! # Results on propositional theories
 
-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.
+In this file we prove that `CPL` is a classical theory. We provide derived rules for common
+classical proof patterns.
 
 Since `Proposition` has `bot` as a primitive constructor, no `[Bot Atom]` constraint is needed:
 `⊥ : Proposition Atom` is always available as `.bot`.
@@ -23,48 +22,21 @@ universe u
 
 namespace Cslib.Logic.PL
 
-open Proposition Theory InferenceSystem DerivableIn Derivation IsIntuitionistic IsClassical
+open Proposition Theory InferenceSystem DerivableIn Derivation IsClassical
 
 variable {Atom : Type u} [DecidableEq Atom] {T : Theory Atom}
 
 namespace Theory
 
-/-- `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 Γ)
-
-/-- Efq as a derived rule. -/
-def IsIntuitionistic.efqRule [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Proposition Atom)
-    (D : T⇓(Γ ⊢ ⊥)) : T⇓(Γ ⊢ A) :=
-  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 <| 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) :=
   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 := 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
@@ -80,7 +52,8 @@ def IsClassical.pierce [IsClassical Atom T] (A B : Proposition Atom) : T⇓(((A
   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
+  exact efq (impE (ass <| Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self _ _)))
+                  (ass <| Finset.mem_insert_self _ _))
 
 /-- The axiom system consisting of instances of LEM. -/
 def LEM : Theory Atom := {A ∨ ¬ A | A : Proposition Atom}
@@ -96,23 +69,23 @@ 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 ∪ IPL : Theory Atom) where
+instance instIsClassicalLEM : IsClassical Atom (LEM : Theory Atom) where
   dne A := by
     apply impI
     apply orE
-    · exact ax <| Set.mem_union_left _ <| lem_mem_lem A
+    · exact ax (lem_mem_lem A)
     · exact ass (Finset.mem_insert_self A _)
-    · apply impE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A))
+    · apply efq
       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 ∪ IPL : Theory Atom) where
+instance instIsClassicalPierce : IsClassical Atom (Pierce : Theory Atom) where
   dne A := by
     apply impI
-    apply impE (A := (A → ⊥) → A) (ax <| Set.mem_union_left _ <| pierce_mem_pierce A ⊥)
+    apply impE (A := (A → ⊥) → A) (ax <| pierce_mem_pierce A ⊥)
     apply impI
-    apply impE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A))
+    apply efq
     apply impE (A := ¬ A)
     · exact ass (Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self _ _)))
     · exact ass (Finset.mem_insert_self _ _)
diff --git a/references.bib b/references.bib
index 8fac9b0e6..d241a6c86 100644
--- a/references.bib
+++ b/references.bib
@@ -1,11 +1,3 @@
-@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},
@@ -484,3 +476,43 @@ @mastersthesis{Calisto2022
   school       = {Universidade do Minho},
   year         = {2022}
 }
+
+@article{Gentzen1935,
+  author       = {Gentzen, Gerhard},
+  title        = {Untersuchungen {\"u}ber das logische Schlie{\ss}en. {I}},
+  journal      = {Mathematische Zeitschrift},
+  volume       = {39},
+  number       = {1},
+  pages        = {176--210},
+  year         = {1935},
+  doi          = {10.1007/BF01201353}
+}
+
+@book{Prawitz1965,
+  author       = {Prawitz, Dag},
+  title        = {Natural Deduction: A Proof-Theoretical Study},
+  publisher    = {Almqvist \& Wiksell},
+  address      = {Stockholm},
+  year         = {1965},
+  note         = {Reprinted by Dover Publications, 2006}
+}
+
+@book{TroelstraVanDalen1988,
+  author       = {Troelstra, A. S. and van Dalen, D.},
+  title        = {Constructivism in Mathematics: An Introduction},
+  volume       = {1},
+  series       = {Studies in Logic and the Foundations of Mathematics},
+  number       = {121},
+  publisher    = {North-Holland},
+  address      = {Amsterdam},
+  year         = {1988},
+  isbn         = {978-0-444-70506-8}
+}
+
+@book{Avigad2022,
+  author       = {Jeremy Avigad},
+  title        = {Mathematical Logic and Computation},
+  publisher    = {Cambridge University Press},
+  year         = {2022},
+  isbn         = {978-1-108-84072-1}
+}

From e6d92df6ab7680514d1cd12e86ff23519862cd9d Mon Sep 17 00:00:00 2001
From: benbrastmckie <benbrastmckie@gmail.com>
Date: Thu, 2 Jul 2026 09:42:51 -0700
Subject: [PATCH 4/5] fix(Logics/Propositional): revert binder and naming
 churn, restore derived rules
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

PR review polish for #648. Reverts unrequested churn on Thomas Waring's
original design: makes Γ implicit again on the Derivation constructors
(andI/andE/orI/orE), restores the andE₁/andE₂/orI₁/orI₂ subscript names,
and cleans up the resulting explicit-Γ/`_` noise at all call sites in
weak/subs/substAtom. Keeps the intentional impI/impE rename.

Restores contra/efqRule as plain derived rules over the now-primitive
efq constructor (no longer needs an IsIntuitionistic typeclass), and uses
contra to simplify IsClassical.pierce back to a readable tactic proof.

Makes Atom explicit again on CPL/LEM/Pierce (Mathlib-typical for
type-family constants), removing the `(Atom := Atom)` noise at their use
sites, and unifies CPL's definition with the set-builder idiom already
used for LEM/Pierce. Normalizes copyright headers to the standard
single-copyright-line, dual-author-line format.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Cslib/Logics/Propositional/Defs.lean          |  7 +-
 .../Propositional/NaturalDeduction/Basic.lean | 83 +++++++++++--------
 .../NaturalDeduction/Theory.lean              | 23 +++--
 3 files changed, 63 insertions(+), 50 deletions(-)

diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean
index 60ca8f674..203105559 100644
--- a/Cslib/Logics/Propositional/Defs.lean
+++ b/Cslib/Logics/Propositional/Defs.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved.
+Copyright (c) 2025 Thomas Waring. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Waring, Benjamin Brast-McKie
 -/
@@ -112,11 +112,10 @@ inference rule (see `Derivation.efq`), so no explosion axioms are needed. -/
 abbrev IPL : Theory Atom := ∅
 
 /-- Classical logic further adds double negation elimination. -/
-abbrev CPL : Theory Atom :=
-  Set.range (fun (A : Proposition Atom) ↦ ¬¬A → A)
+abbrev CPL (Atom : Type u) : Theory Atom := {¬¬A → A | A : Proposition Atom}
 
 omit [DecidableEq Atom] in
-lemma dne_mem_cpl (A : Proposition Atom) : (¬¬A → A) ∈ CPL (Atom := Atom) := ⟨A, rfl⟩
+lemma dne_mem_cpl (A : Proposition Atom) : (¬¬A → A) ∈ CPL Atom := ⟨A, rfl⟩
 
 open InferenceSystem
 
diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
index 7aa2996ab..8cdc085b0 100644
--- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
+++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved.
+Copyright (c) 2025 Thomas Waring. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Waring, Benjamin Brast-McKie
 -/
@@ -32,6 +32,7 @@ defines an instance of `InferenceSystem T Sequent`.
 - `Derivation.weak` : weakening as a derived rule.
 - `Derivation.cut`, `Derivation.subs` : replace a hypothesis in a derivation — the two versions
 differ in the construction of the relevant derivation.
+- `Derivation.contra` : deriving anything from contradictory hypotheses.
 - `Theory.equiv_equivalence` : equivalence of propositions is an equivalence relation.
 
 ## Notation
@@ -97,26 +98,26 @@ inductive Theory.Derivation {T : Theory Atom} : Ctx Atom → Proposition Atom 
   /-- Assumption -/
   | ass {Γ : Ctx Atom} {A : Proposition Atom} (_ : A ∈ Γ) : Derivation Γ A
   /-- Conjunction introduction -/
-  | andI {A B : Proposition Atom} (Γ : Ctx Atom) :
+  | andI {Γ : Ctx Atom} {A B : Proposition Atom} :
       Derivation Γ A → Derivation Γ B → Derivation Γ (A ∧ B)
   /-- Left conjunction elimination -/
-  | andE1 {A B : Proposition Atom} (Γ : Ctx Atom) :
+  | andE₁ {Γ : Ctx Atom} {A B : Proposition Atom} :
       Derivation Γ (A ∧ B) → Derivation Γ A
   /-- Right conjunction elimination -/
-  | andE2 {A B : Proposition Atom} (Γ : Ctx Atom) :
+  | andE₂ {Γ : Ctx Atom} {A B : Proposition Atom} :
       Derivation Γ (A ∧ B) → Derivation Γ B
   /-- Left disjunction introduction -/
-  | orI1 {A B : Proposition Atom} (Γ : Ctx Atom) :
+  | orI₁ {Γ : Ctx Atom} {A B : Proposition Atom} :
       Derivation Γ A → Derivation Γ (A ∨ B)
   /-- Right disjunction introduction -/
-  | orI2 {A B : Proposition Atom} (Γ : Ctx Atom) :
+  | orI₂ {Γ : Ctx Atom} {A B : Proposition Atom} :
       Derivation Γ B → Derivation Γ (A ∨ B)
   /-- Disjunction elimination -/
-  | orE {A B C : Proposition Atom} (Γ : Ctx Atom) :
+  | orE {Γ : Ctx Atom} {A B C : Proposition Atom} :
       Derivation Γ (A ∨ B) → Derivation (insert A Γ) C → Derivation (insert B Γ) C →
       Derivation Γ C
   /-- Implication introduction -/
-  | impI {A B : Proposition Atom} (Γ : Ctx Atom) :
+  | impI {Γ : Ctx Atom} {A B : Proposition Atom} :
       Derivation (insert A Γ) B → Derivation Γ (A → B)
   /-- Implication elimination (modus ponens) -/
   | impE {Γ : Ctx Atom} {A B : Proposition Atom} :
@@ -185,16 +186,16 @@ 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 _ _ _ 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)
+  | 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 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
+  | impI D => impI <| D.weak hTheory <| Finset.insert_subset_insert _ hCtx
   | impE D D' => impE (D.weak hTheory hCtx) (D'.weak hTheory hCtx)
   | efq D => efq (D.weak hTheory hCtx)
 
@@ -231,7 +232,7 @@ def Theory.Derivation.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom}
     (D : T⇓(Γ ⊢ A)) (E : T⇓(insert A Δ ⊢ B)) : T⇓((Γ ∪ Δ) ⊢ B) := by
   refine impE (A := A) ?_ (D.weakCtx Finset.subset_union_left)
   have : insert A Δ ⊆ insert A (Γ ∪ Δ) := by grind
-  exact impI (Γ ∪ Δ) <| E.weakCtx this
+  exact impI <| E.weakCtx this
 
 /-- Proof irrelevant cut rule. -/
 theorem DerivableIn.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom} :
@@ -265,18 +266,18 @@ def Theory.Derivation.subs {Γ Γ' Δ : Ctx Atom} {B : Proposition Atom}
       exact (Ds B h).weakCtx <| by grind
     case neg h =>
       exact ass <| by grind
-  | @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)
+  | @andI _ _ _ Γ A' B' E₁ E₂ => andI (E₁.subs Ds) (E₂.subs Ds)
+  | @andE₁ _ _ _ Γ A' B' E => andE₁ (E.subs Ds)
+  | @andE₂ _ _ _ Γ A' B' E => andE₂ (E.subs Ds)
+  | @orI₁ _ _ _ Γ A' B' E => orI₁ (E.subs Ds)
+  | @orI₂ _ _ _ Γ A' B' E => orI₂ (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
+  | @impI _ _ _ Γ A' _ E => by
     apply impI
     rw [show insert A' (Γ \ Γ' ∪ Δ) = (insert A' Γ \ Γ') ∪ insert A' Δ by grind]
     exact E.subs Ds |>.weakCtx (by grind)
@@ -289,16 +290,16 @@ 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₁ 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)
+  | andI D₁ D₂ => andI (D₁.substAtom f) (D₂.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 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)
+  | impI D => impI <| (Finset.image_insert (· >>= f) _ _) ▸ (D.substAtom f)
   | impE D E => impE (D.substAtom f) (E.substAtom f)
   | efq D => efq (D.substAtom f)
 
@@ -312,7 +313,7 @@ theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [Decidabl
 
 /-- A derivation of the canonical tautology. -/
 def Theory.derivationTop : T⇓(⊤ : Proposition Atom) :=
-  impI ∅ <| ass <| by grind
+  impI <| ass <| by grind
 
 theorem derivableIn_top : DerivableIn T (⊤ : Proposition Atom) := ⟨derivationTop⟩
 
@@ -326,6 +327,20 @@ theorem derivable_iff_equiv_top (A : Proposition Atom) :
     rw [←show (∅ : Ctx Atom) = ∅ ∪ ∅ by rfl] at this
     exact this h.mpr
 
+/-! ### Ex falso and contradiction -/
+
+/-- Ex falso quodlibet as a derived rule. This coincides with the primitive `efq` constructor;
+the wrapper is kept, with an explicit conclusion argument, for readability at call sites and for
+parity with the pre-primitive-`efq` design where `efqRule` had to thread through an intuitionistic
+typeclass. -/
+def Theory.Derivation.efqRule {Γ : Ctx Atom} (A : Proposition Atom) (D : T⇓(Γ ⊢ ⊥)) :
+    T⇓(Γ ⊢ A) := efq D
+
+/-- Prove any proposition from contradictory hypotheses. -/
+def Theory.Derivation.contra {Γ : Ctx Atom} (A B : Proposition Atom) (hΓ : A ∈ Γ)
+    (hΓ' : (¬A) ∈ Γ) : T⇓(Γ ⊢ B) :=
+  efqRule B <| impE (ass hΓ') (ass hΓ)
+
 namespace Theory
 
 /-- Change the conclusion along an equivalence. -/
diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
index 68c061c94..7187ad054 100644
--- a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
+++ b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved.
+Copyright (c) 2025 Thomas Waring. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Waring, Benjamin Brast-McKie
 -/
@@ -29,7 +29,7 @@ variable {Atom : Type u} [DecidableEq Atom] {T : Theory Atom}
 namespace Theory
 
 /-- `CPL` is classical: it contains `¬¬A → A` for all `A`. -/
-instance instIsClassicalCPL : IsClassical Atom (CPL (Atom := Atom)) where
+instance instIsClassicalCPL : IsClassical Atom (CPL Atom) where
   dne A := ax (dne_mem_cpl A)
 
 /-- Proof by contradiction as a derived rule. -/
@@ -41,10 +41,10 @@ def IsClassical.byContra [IsClassical Atom T] {Γ : Ctx Atom} {A : Proposition A
 def IsClassical.lem [IsClassical Atom T] (A : Proposition Atom) : T⇓(A ∨ ¬ A) := by
   apply byContra
   apply impE (ass <| Finset.mem_insert_self ..)
-  apply orI2
+  apply orI₂
   apply impI
   apply impE (A := A ∨ ¬ A) (ass <| by grind)
-  apply orI1
+  apply orI₁
   exact ass <| Finset.mem_insert_self ..
 
 /-- Pierce's law in a classical theory. -/
@@ -52,24 +52,23 @@ def IsClassical.pierce [IsClassical Atom T] (A B : Proposition Atom) : T⇓(((A
   apply impI; apply byContra
   apply impE (ass <| Finset.mem_insert_self ..)
   apply impE (A := A → B) (ass <| by grind); apply impI
-  exact efq (impE (ass <| Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self _ _)))
-                  (ass <| Finset.mem_insert_self _ _))
+  apply contra A B <;> grind
 
 /-- The axiom system consisting of instances of LEM. -/
-def LEM : Theory Atom := {A ∨ ¬ A | A : Proposition Atom}
+def LEM (Atom : Type u) : Theory Atom := {A ∨ ¬ A | A : Proposition Atom}
 
 omit [DecidableEq Atom] in
-lemma lem_mem_lem (A : Proposition Atom) : (A ∨ ¬ A) ∈ LEM (Atom := Atom) := ⟨A, rfl⟩
+lemma lem_mem_lem (A : Proposition Atom) : (A ∨ ¬ A) ∈ LEM Atom := ⟨A, rfl⟩
 
 /-- The axiom system consisting of instances of Pierce's law. -/
-def Pierce : Theory Atom :=
+def Pierce (Atom : Type u) : Theory Atom :=
   {((A → B) → A) → A | (A : Proposition Atom) (B : Proposition Atom)}
 
 omit [DecidableEq Atom] in
 lemma pierce_mem_pierce (A B : Proposition Atom) :
-    (((A → B) → A) → A) ∈ Pierce (Atom := Atom) := ⟨A, B, rfl⟩
+    (((A → B) → A) → A) ∈ Pierce Atom := ⟨A, B, rfl⟩
 
-instance instIsClassicalLEM : IsClassical Atom (LEM : Theory Atom) where
+instance instIsClassicalLEM : IsClassical Atom (LEM Atom) where
   dne A := by
     apply impI
     apply orE
@@ -80,7 +79,7 @@ instance instIsClassicalLEM : IsClassical Atom (LEM : Theory Atom) where
       · exact ass (Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self _ _)))
       · exact ass (Finset.mem_insert_self _ _)
 
-instance instIsClassicalPierce : IsClassical Atom (Pierce : Theory Atom) where
+instance instIsClassicalPierce : IsClassical Atom (Pierce Atom) where
   dne A := by
     apply impI
     apply impE (A := (A → ⊥) → A) (ax <| pierce_mem_pierce A ⊥)

From 9376b737a8a4ddadb04a1608a229524d71a2b4b4 Mon Sep 17 00:00:00 2001
From: benbrastmckie <benbrastmckie@gmail.com>
Date: Thu, 2 Jul 2026 09:42:55 -0700
Subject: [PATCH 5/5] chore(references): English citation for Gentzen 1935

Reviewer ctchou asked for English-language references. Replaces the
German-title journal entry with the standard English-translation
citation (Szabo (ed.), The Collected Papers of Gerhard Gentzen,
North-Holland, 1969, pp. 68-131), keeping a note pointing to the
original 1935 Mathematische Zeitschrift publication. The doc-comment
citation text in the .lean files already used the English title, so no
further changes were needed there.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 references.bib | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/references.bib b/references.bib
index d241a6c86..18ff882d3 100644
--- a/references.bib
+++ b/references.bib
@@ -477,15 +477,17 @@ @mastersthesis{Calisto2022
   year         = {2022}
 }
 
-@article{Gentzen1935,
+@incollection{Gentzen1935,
   author       = {Gentzen, Gerhard},
-  title        = {Untersuchungen {\"u}ber das logische Schlie{\ss}en. {I}},
-  journal      = {Mathematische Zeitschrift},
-  volume       = {39},
-  number       = {1},
-  pages        = {176--210},
-  year         = {1935},
-  doi          = {10.1007/BF01201353}
+  editor       = {Szabo, M. E.},
+  title        = {Investigations into Logical Deduction},
+  booktitle    = {The Collected Papers of Gerhard Gentzen},
+  publisher    = {North-Holland},
+  address      = {Amsterdam},
+  pages        = {68--131},
+  year         = {1969},
+  note         = {English translation of the 1935 German original, Mathematische Zeitschrift 39,
+                  176--210, doi:10.1007/BF01201353}
 }
 
 @book{Prawitz1965,