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

Author: benbrastmckie

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

Cslib/Foundations/Logic/Connectives.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. -/

Cslib/Logics/Propositional/Defs.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,24 @@ 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
+[Gentzen1935], [Prawitz1965], [TroelstraVanDalen1988].
 
 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]
+* [G. Gentzen, *Untersuchungen über das logische Schließen. I*][Gentzen1935]
+* [D. Prawitz, *Natural Deduction: A Proof-Theoretical Study*][Prawitz1965]
+* [A. S. Troelstra, D. van Dalen, *Constructivism in Mathematics*][TroelstraVanDalen1988]
 -/
 
 @[expose] public section
@@ -83,8 +89,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 +120,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 +169,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 +195,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 +280,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 +299,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}

Cslib/Logics/Propositional/NaturalDeduction/Basic.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 _ _)