From c8df55537209f1555d2ada7f0760e6863d5896a7 Mon Sep 17 00:00:00 2001 From: benbrastmckie Date: Sun, 14 Jun 2026 05:53:05 -0700 Subject: [PATCH] task 188: implement five-primitive propositional logic PR MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Add Cslib/Foundations/Logic/Connectives.lean: HasBot, HasImp, HasAnd, HasOr, PropositionalConnectives typeclass hierarchy - Refactor Cslib/Logics/Propositional/Defs.lean: five-primitive Proposition {atom, bot, imp, and, or}, remove [Bot Atom] constraints, add PropositionalConnectives/HasAnd/HasOr instances, add biconditional iff abbrev - Update Cslib/Logics/Propositional/NaturalDeduction/Basic.lean: rename implI/implE to impI/impE, rename andE₁/₂/orI₁/₂ to ASCII-safe andE1/2/orI1/2, remove [Inhabited Atom] constraints Session: sess_1781439290_50c37f Co-Authored-By: Claude Sonnet 4.6 --- Cslib.lean | 1 + Cslib/Foundations/Logic/Connectives.lean | 96 ++++++++++++ Cslib/Logics/Propositional/Defs.lean | 143 +++++++++++++----- .../Propositional/NaturalDeduction/Basic.lean | 103 +++++++------ 4 files changed, 259 insertions(+), 84 deletions(-) create mode 100644 Cslib/Foundations/Logic/Connectives.lean diff --git a/Cslib.lean b/Cslib.lean index 5932e9207..1450ced83 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -69,6 +69,7 @@ public import Cslib.Foundations.Data.RelatesInSteps public import Cslib.Foundations.Data.Set.Saturation public import Cslib.Foundations.Data.StackTape public import Cslib.Foundations.Lint.Basic +public import Cslib.Foundations.Logic.Connectives public import Cslib.Foundations.Logic.InferenceSystem public import Cslib.Foundations.Logic.LogicalEquivalence public import Cslib.Foundations.Relation.Attr diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean new file mode 100644 index 000000000..93aedef5d --- /dev/null +++ b/Cslib/Foundations/Logic/Connectives.lean @@ -0,0 +1,96 @@ +/- +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 +([Wajsberg1938], [McKinsey1939]); 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. + +## Why Not Mathlib's `Bot` / `HImp`? + +Mathlib's `Bot` class is for algebraic bottom elements (lattice theory), and `HImp` is for +Heyting implication in a lattice. Neither is appropriate here: +- Formula types are not lattices; they are freely generated algebras. +- We need `imp` to be a binary constructor (taking two formula arguments), not a binary + operation on a lattice. +- The typeclass hierarchy here enables polymorphic axiom definitions that quantify over any + formula type satisfying the appropriate connective class, independently of any algebraic + structure. + +## References + +* [I. Johansson, *Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus*][Johansson1937] +* [M. Wajsberg, *Untersuchungen über den Aussagenkalkül von A. Heyting*][Wajsberg1938] +* [J. C. C. McKinsey, + *Proof of the Independence of the Primitive Symbols of Heyting's Calculus*][McKinsey1939] +* [D. Prawitz, *Natural Deduction: A Proof-Theoretical Study*][Prawitz1965] +* [A. S. Troelstra, D. van Dalen, + *Constructivism in Mathematics: An Introduction*][TroelstraVanDalen1988] +* [A. Church, *Introduction to Mathematical Logic*][Church1956] +* [G. Gentzen, *Untersuchungen über das logische Schließen*][Gentzen1935] +-/ + +@[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, implication, conjunction, and disjunction. + +`HasAnd` and `HasOr` are included because all four connectives are needed for a +five-primitive propositional signature `{atom, bot, imp, and, or}`. This bundled class +allows axiom schemas to be stated polymorphically over any formula type providing +all four connectives. + +Note: this does not extend `HasAnd` and `HasOr` directly to avoid forcing all +formula types to bundle conjunction and disjunction together with the minimal +`HasBot`/`HasImp` interface. When all four 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 fa3caf53e..48b51bacb 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -1,13 +1,14 @@ /- -Copyright (c) 2025 Thomas Waring. All rights reserved. +Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Thomas Waring +Authors: Thomas Waring, Benjamin Brast-McKie -/ module -public import Cslib.Init +public import Cslib.Foundations.Logic.Connectives public import Mathlib.Data.FunLike.Basic +public import Mathlib.Data.Set.Basic public import Mathlib.Data.Set.Image public import Mathlib.Order.TypeTags @@ -15,23 +16,73 @@ public import Mathlib.Order.TypeTags ## 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), following + the standard five-primitive signature of Gentzen/Prawitz/Troelstra-van Dalen. Negation (`neg`), + verum (`top`), and biconditional (`iff`) are derived connectives (`abbrev`s) rather than + constructors. - `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. + 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. + +## Design: Five Primitives + +Upstream used four constructors `{atom, and, or, impl}` with a `Bot` typeclass constraint +to simulate falsum. This PR changes to five primitives `{atom, bot, imp, and, or}` with derived +negation and verum, for the following reasons: + +1. **Minimal logic requires primitive `bot`**: Johansson's minimal logic (1937, [Johansson1937]) + is the standard basis for proof-relevant propositional logic. Minimal logic requires a + distinguishable bottom formula; without it, one obtains only the *positive fragment* (no + negation at all). The `[Bot Atom]` constraint approach simulates bottom via an atomic formula, + which conflates the logical bottom with atomic data. + +2. **Uniform negation**: With primitive `bot`, negation `¬A := A → ⊥` is uniformly available + without typeclass constraints. The old `[Bot Atom]` approach required `Inhabited Atom` for + `top` and `Bot Atom` for `neg`, producing a constraint proliferation. + +3. **Standard notation**: The constructor name `impl` is non-standard; Gentzen (1935, + [Gentzen1935]) and Prawitz (1965, [Prawitz1965]) both write the connective as `⊃` or `→`. + We rename to `imp` for clarity and alignment with the broader logic literature. + +4. **Functional completeness**: Adding `bot` as a primitive makes `{bot, imp, and, or}` the + standard five-primitive basis studied in [TroelstraVanDalen1988] Chapter 2 and + [Church1956] §24. This resolves the objection (CSLib PR #635) that the four-primitive + `{and, or, impl}` set is not functionally complete for classical logic (it lacks the + ability to express unsatisfiable formulas). ## Notation -We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum, -conjunction, disjunction, implication and negation. +We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ↔ ¬` for, respectively, falsum, +verum, conjunction, disjunction, implication, biconditional, and negation. + +## Architecture + +Two proof systems are defined for this propositional language: + +- **Layer 1 — Natural Deduction** (`NaturalDeduction/Basic.lean`): a `Theory.Derivation` inductive + with 10 primitive constructors. Logic strength is controlled by the theory parameter: `MPL` + (Johansson's minimal logic, [Johansson1937]), `IPL` (intuitionistic), and `CPL` (classical). + +- **Layer 2 — Hilbert System** (`ProofSystem/`): an axiom predicate hierarchy with sequent + derivability and a Hilbert-style proof-theoretic treatment (future PR). + +## References + +* [I. Johansson, *Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus*][Johansson1937] +* [G. Gentzen, *Untersuchungen über das logische Schließen*][Gentzen1935] +* [D. Prawitz, *Natural Deduction: A Proof-Theoretical Study*][Prawitz1965] +* [A. S. Troelstra, D. van Dalen, + *Constructivism in Mathematics: An Introduction*][TroelstraVanDalen1988] +* [A. Church, *Introduction to Mathematical Logic*][Church1956] +* [A. Chagrov, M. Zakharyaschev, *Modal Logic*][ChagrovZakharyaschev1997], Chapter 1 -/ @[expose] public section @@ -42,44 +93,64 @@ 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 — a primitive, not an atomic formula encoding of bottom. Making `bot` + primitive is required by Johansson's minimal logic ([Johansson1937]); without it, the + type only captures the positive fragment. -/ + | 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 → ⊥`. Valid in minimal, intuitionistic, and +classical logic alike. -/ +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 as a derived connective: `⊤ := ⊥ → ⊥`. Derivable in minimal logic. -/ +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 @@ -102,45 +173,45 @@ instance : Functor Theory where abbrev MPL : Theory (Atom) := ∅ /-- Intuitionistic propositional logic adds the principle of explosion (ex falso quodlibet). -/ -abbrev IPL [Bot Atom] : Theory Atom := - Set.range (⊥ → ·) +abbrev IPL : Theory Atom := + Set.range (Proposition.imp ⊥ ·) /-- Classical logic further adds double negation elimination. -/ -abbrev CPL [Bot Atom] : Theory Atom := +abbrev CPL : Theory Atom := Set.range (fun (A : Proposition Atom) ↦ ¬¬A → A) /-- A theory is intuitionistic if it validates ex falso quodlibet. -/ @[scoped grind] -class IsIntuitionistic [Bot Atom] (T : Theory Atom) where +class IsIntuitionistic (T : Theory Atom) where efq (A : Proposition Atom) : (⊥ → A) ∈ T omit [DecidableEq Atom] in @[scoped grind =] -theorem isIntuitionisticIff [Bot Atom] (T : Theory Atom) : IsIntuitionistic T ↔ IPL ⊆ T := by grind +theorem isIntuitionisticIff (T : Theory Atom) : IsIntuitionistic T ↔ IPL ⊆ T := by grind /-- A theory is classical if it validates double-negation elimination. -/ @[scoped grind] -class IsClassical [Bot Atom] (T : Theory Atom) where +class IsClassical (T : Theory Atom) where dne (A : Proposition Atom) : (¬¬A → A) ∈ T omit [DecidableEq Atom] in @[scoped grind =] -theorem isClassicalIff [Bot Atom] (T : Theory Atom) : IsClassical T ↔ CPL ⊆ T := by grind +theorem isClassicalIff (T : Theory Atom) : IsClassical T ↔ CPL ⊆ T := by grind -instance instIsIntuitionisticIPL [Bot Atom] : IsIntuitionistic (Atom := Atom) IPL where +instance instIsIntuitionisticIPL : IsIntuitionistic (Atom := Atom) IPL where efq A := Set.mem_range.mpr ⟨A, rfl⟩ -instance instIsClassicalCPL [Bot Atom] : IsClassical (Atom := Atom) CPL where +instance instIsClassicalCPL : IsClassical (Atom := Atom) CPL where dne A := Set.mem_range.mpr ⟨A, rfl⟩ omit [DecidableEq Atom] in @[scoped grind →] -theorem instIsIntuitionisticExtention [Bot Atom] {T T' : Theory Atom} [IsIntuitionistic T] +theorem instIsIntuitionisticExtention {T T' : Theory Atom} [IsIntuitionistic T] (h : T ⊆ T') : IsIntuitionistic T' := by grind omit [DecidableEq Atom] in @[scoped grind →] -theorem instIsClassicalExtention [Bot Atom] {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') : +theorem instIsClassicalExtention {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') : IsClassical T' := by grind /-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/ diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean index b1a8947e2..3d329180e 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,25 @@ 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, Johansson 1937 [Johansson1937]): 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!) +* [I. Johansson, *Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus*][Johansson1937] +* [D. Prawitz, *Natural Deduction: A Proof-Theoretical Study*][Prawitz1965] +* [A. S. Troelstra, D. van Dalen, + *Constructivism in Mathematics: An Introduction*][TroelstraVanDalen1988], Section 10.4 +* [G. Gentzen, + *Untersuchungen über das logische Schließen*][Gentzen1935] -/ @[expose] public section @@ -83,7 +87,9 @@ 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 @@ -93,21 +99,21 @@ inductive Theory.Derivation {T : Theory Atom} : Ctx Atom → Proposition Atom | andI {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ A → Derivation Γ B → Derivation Γ (A ∧ B) /-- Conjunction elimination left -/ - | andE₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A ∧ B) → Derivation Γ A + | andE1 {Γ : 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 + | andE2 {Γ : 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) + | orI1 {Γ : 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) + | orI2 {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ B → Derivation Γ (A ∨ B) /-- Disjunction elimination -/ | orE {Γ : Ctx Atom} {A B C : Proposition Atom} : Derivation Γ (A ∨ B) → Derivation (insert A Γ) C → Derivation (insert B Γ) C → Derivation Γ C /-- Implication introduction -/ - | implI {A B : Proposition Atom} (Γ : Ctx Atom) : + | impI {A B : Proposition Atom} (Γ : Ctx Atom) : Derivation (insert A Γ) B → Derivation Γ (A → B) - /-- Implication elimination -/ - | implE {Γ : Ctx Atom} {A B : Proposition Atom} : + /-- Implication elimination (modus ponens) -/ + | impE {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A → B) → Derivation Γ A → Derivation Γ B /-- Inference system for derivations under the theory `T`. -/ @@ -171,16 +177,16 @@ def Theory.Derivation.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposit | 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 + | andE1 D => andE1 <| D.weak hTheory hCtx + | andE2 D => andE2 <| D.weak hTheory hCtx + | orI1 D => orI1 <| D.weak hTheory hCtx + | orI2 D => orI2 <| D.weak hTheory hCtx | orE D D' D'' => orE (D.weak hTheory hCtx) (D'.weak hTheory <| Finset.insert_subset_insert _ hCtx) (D''.weak hTheory <| Finset.insert_subset_insert _ hCtx) - | @implI _ _ _ A B Γ D => implI (Δ) <| D.weak hTheory <| Finset.insert_subset_insert _ hCtx - | implE D D' => implE (D.weak hTheory hCtx) (D'.weak hTheory hCtx) + | @impI _ _ _ A B Γ D => impI (Δ) <| D.weak hTheory <| Finset.insert_subset_insert _ hCtx + | impE D D' => impE (D.weak hTheory hCtx) (D'.weak hTheory hCtx) /-- 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} : @@ -250,21 +256,21 @@ def Theory.Derivation.subs {Γ Γ' Δ : Ctx Atom} {B : Proposition Atom} 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 + | andE1 E => andE1 <| E.subs Ds + | andE2 E => andE2 <| E.subs Ds + | orI1 E => orI1 <| E.subs Ds + | orI2 E => orI2 <| E.subs Ds | @orE _ _ _ _ C C' _ E E' E'' .. => by apply orE (E.subs Ds) · rw [show insert C (Γ \ Γ' ∪ Δ) = (insert C Γ \ Γ') ∪ insert C Δ by grind] exact E'.subs Ds |>.weakCtx (by grind) · rw [show insert C' (Γ \ Γ' ∪ Δ) = (insert C' Γ \ Γ') ∪ insert C' Δ by grind] exact E''.subs Ds |>.weakCtx (by grind) - | @implI _ _ _ A' _ _ E .. => by - apply implI + | @impI _ _ _ A' _ _ E .. => by + apply impI rw [show insert A' (Γ \ Γ' ∪ Δ) = (insert A' Γ \ Γ') ∪ insert A' Δ by grind] exact E.subs Ds |>.weakCtx (by grind) - | implE E E' => implE (E.subs Ds) (E'.subs Ds) + | impE E E' => impE (E.subs Ds) (E'.subs Ds) /-- Transport a derivation along a substitution of atoms. -/ def Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom'] @@ -273,15 +279,15 @@ def Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [Decida | 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) + | 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 E E' => orE (D.substAtom f) ((Finset.image_insert (· >>= f) _ _) ▸ E.substAtom f) ((Finset.image_insert (· >>= f) _ _) ▸ E'.substAtom f) - | implI _ D => implI _ <| (Finset.image_insert (· >>= f) _ _) ▸ (D.substAtom f) - | implE D E => implE (D.substAtom f) (E.substAtom f) + | impI _ D => impI _ <| (Finset.image_insert (· >>= f) _ _) ▸ (D.substAtom f) + | impE D E => impE (D.substAtom f) (E.substAtom f) theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom'] {T : Theory Atom} @@ -291,13 +297,14 @@ 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 +/-- A derivation of the canonical tautology. With primitive `bot`, `⊤ := ⊥ → ⊥` is derivable +in minimal logic without any typeclass constraint on the atom type. -/ +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, ?_⟩