feat(Logics/Propositional): five-primitive formula type with primitive bot

Cslib/Logics/Propositional/Defs.lean

@@ -1,37 +1,42 @@
 /-
 Copyright (c) 2025 Thomas Waring. 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.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.
+- `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
 
 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 +47,48 @@ 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
 
 /-- 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
@@ -98,42 +107,23 @@ 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 (Atom : Type u) : 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}
-
-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)
+/-- 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 (Atom : Type u) [Bot Atom] : Theory Atom := {¬¬A → A | A : Proposition Atom}
+abbrev CPL (Atom : Type u) : Theory Atom := {¬¬A → A | A : Proposition Atom}
 
 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 := ⟨A, rfl⟩
 
 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) [Bot Atom] (S : Type*)
-    [InferenceSystem S (Proposition Atom)] where
-  /-- The principle of explosion (ex falso quolibet). -/
-  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)