diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index e9c603d91..203105559 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/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,34 +47,37 @@ 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 @@ -77,9 +85,10 @@ 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) diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean index 560ecb69e..8cdc085b0 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. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Thomas Waring +Authors: Thomas Waring, Benjamin Brast-McKie -/ module @@ -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 @@ -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 @@ -42,21 +43,27 @@ 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, +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: +- `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 -- 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] +* [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,7 +90,8 @@ 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, 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 @@ -92,23 +100,31 @@ inductive Theory.Derivation {T : Theory Atom} : Ctx Atom → Proposition Atom /-- Conjunction introduction -/ | 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 - /-- 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 -/ + | andE₁ {Γ : Ctx Atom} {A B : Proposition Atom} : + Derivation Γ (A ∧ B) → Derivation Γ A + /-- Right conjunction elimination -/ + | andE₂ {Γ : Ctx Atom} {A B : Proposition Atom} : + Derivation Γ (A ∧ B) → Derivation Γ B + /-- Left disjunction introduction -/ + | orI₁ {Γ : Ctx Atom} {A B : Proposition Atom} : + Derivation Γ A → Derivation Γ (A ∨ B) + /-- Right disjunction introduction -/ + | orI₂ {Γ : 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 + | 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 {Γ : Ctx Atom} {A B : Proposition 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 + /-- 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 @@ -155,8 +171,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 Atom).Equiv +/-- Equivalent propositions (over the base theory IPL). -/ +abbrev Equiv : Proposition Atom → Proposition Atom → Prop := IPL.Equiv @[inherit_doc] scoped infix:29 " ≡ " => Equiv @@ -170,17 +186,18 @@ 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'' => + | 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) - (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) + (DA.weak hTheory (Finset.insert_subset_insert _ hCtx)) + (DB.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) /-- Weakening the theory only. -/ def Theory.Derivation.weakTheory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom} @@ -213,9 +230,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 +266,23 @@ 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 + | @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 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 + · 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) + | 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'] @@ -272,16 +290,18 @@ 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) + | 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 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) + | 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) + | efq D => efq (D.substAtom f) theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom'] {T : Theory Atom} @@ -292,12 +312,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, ?_⟩ @@ -307,6 +327,20 @@ theorem derivable_iff_equiv_top [Inhabited Atom] (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 8cdaa806d..7187ad054 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. 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,11 @@ 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 -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`. -/ @[expose] public section @@ -20,57 +22,40 @@ 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] [Bot Atom] {T : Theory Atom} +variable {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} namespace Theory -instance instIsIntuitionisticIPL : IsIntuitionistic Atom (IPL Atom) where - efq A := ax (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) := - implE (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Γ) - +/-- `CPL` is classical: it contains `¬¬A → A` for all `A`. -/ instance instIsClassicalCPL : IsClassical Atom (CPL Atom) where dne A := ax (dne_mem_cpl A) /-- 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 - -instance instIsIntuitionisticOfIsClassical [IsClassical Atom T] : IsIntuitionistic Atom T where - efq A := implI _ <| byContra <| ass (by grind) + impE (A := ¬¬A) ((dne A : T⇓(¬¬A → A)) |>.weakCtx <| Finset.empty_subset ..) D.impI /-- 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 orI₂ + apply impI + apply impE (A := A ∨ ¬ A) (ass <| by grind) + apply orI₁ + 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 (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 := ⟨A, rfl⟩ @@ -79,23 +64,29 @@ lemma lem_mem_lem (A : Proposition Atom) : (A ∨ ¬ A) ∈ LEM Atom := ⟨A, rf def Pierce (Atom : Type u) : 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 := ⟨A, B, rfl⟩ -instance instIsClassicalLEM : IsClassical Atom (LEM Atom ∪ IPL Atom : Theory Atom) where +instance instIsClassicalLEM : IsClassical Atom (LEM Atom) where dne A := by - apply implI - apply orE (ax <| Set.mem_union_left _ <| lem_mem_lem A) + apply impI + apply orE + · exact ax (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 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 Atom ∪ IPL Atom : Theory Atom) where +instance instIsClassicalPierce : IsClassical Atom (Pierce 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 <| pierce_mem_pierce A ⊥) + apply impI + apply efq + 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..18ff882d3 100644 --- a/references.bib +++ b/references.bib @@ -476,3 +476,45 @@ @mastersthesis{Calisto2022 school = {Universidade do Minho}, year = {2022} } + +@incollection{Gentzen1935, + author = {Gentzen, Gerhard}, + 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, + 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} +}