diff --git a/Cslib.lean b/Cslib.lean index 37a038ee4..d525304b6 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -131,3 +131,4 @@ public import Cslib.Logics.LinearLogic.CLL.MLL public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic public import Cslib.Logics.Propositional.Defs public import Cslib.Logics.Propositional.NaturalDeduction.Basic +public import Cslib.Logics.Propositional.NaturalDeduction.Theory diff --git a/Cslib/Computability/Automata/NA/Concat.lean b/Cslib/Computability/Automata/NA/Concat.lean index 0b2c10d3e..7cc7c1c18 100644 --- a/Cslib/Computability/Automata/NA/Concat.lean +++ b/Cslib/Computability/Automata/NA/Concat.lean @@ -177,7 +177,7 @@ theorem finConcat_language_eq [Inhabited Symbol] : obtain ⟨ss, ⟨_, h_ωtr⟩, _⟩ := concat_run_exists h_xl1 h_run2 #adaptation_note /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ - have h_mtr := LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (xl1.length + xl2.length)) + have h_mtr := LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (a := xl1.length + xl2.length)) simp [← append_append_ωSequence, extract_eq_drop_take, take_append_of_le_length, ← List.length_append] at h_mtr have : ss (xl1.length + xl2.length) = (ss.drop xl1.length) xl2.length := by grind diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index fa3caf53e..a3999a983 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -6,7 +6,7 @@ Authors: Thomas Waring module -public import Cslib.Init +public import Cslib.Foundations.Logic.InferenceSystem public import Mathlib.Data.FunLike.Basic public import Mathlib.Data.Set.Image public import Mathlib.Order.TypeTags @@ -99,56 +99,61 @@ instance : Functor Theory where map f := Set.image (f <$> ·) /-- The empty theory corresponds to minimal propositional logic. -/ -abbrev MPL : Theory (Atom) := ∅ +abbrev MPL (Atom : Type u) : Theory (Atom) := ∅ /-- Intuitionistic propositional logic adds the principle of explosion (ex falso quodlibet). -/ -abbrev IPL [Bot Atom] : Theory Atom := - Set.range (⊥ → ·) - -/-- Classical logic further adds double negation elimination. -/ -abbrev CPL [Bot Atom] : 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 - 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 - -/-- A theory is classical if it validates double-negation elimination. -/ -@[scoped grind] -class IsClassical [Bot Atom] (T : Theory Atom) where - dne (A : Proposition Atom) : (¬¬A → A) ∈ T +abbrev IPL (Atom : Type u) [Bot Atom] : Theory Atom := {⊥ → A | A : Proposition Atom} omit [DecidableEq Atom] in -@[scoped grind =] -theorem isClassicalIff [Bot Atom] (T : Theory Atom) : IsClassical T ↔ CPL ⊆ T := by grind +lemma efq_mem_ipl [Bot Atom] (A : Proposition Atom) : (⊥ → A) ∈ IPL Atom := ⟨A, rfl⟩ -instance instIsIntuitionisticIPL [Bot Atom] : IsIntuitionistic (Atom := Atom) IPL where - efq A := Set.mem_range.mpr ⟨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) -instance instIsClassicalCPL [Bot Atom] : IsClassical (Atom := Atom) CPL where - dne A := Set.mem_range.mpr ⟨A, rfl⟩ +/-- Classical logic further adds double negation elimination. -/ +abbrev CPL (Atom : Type u) [Bot Atom] : Theory Atom := {¬¬A → A | A : Proposition Atom} omit [DecidableEq Atom] in -@[scoped grind →] -theorem instIsIntuitionisticExtention [Bot Atom] {T T' : Theory Atom} [IsIntuitionistic T] - (h : T ⊆ T') : IsIntuitionistic T' := by grind +lemma dne_mem_cpl [Bot Atom] (A : Proposition Atom) : (¬¬A → A) ∈ CPL Atom := ⟨A, rfl⟩ -omit [DecidableEq Atom] in -@[scoped grind →] -theorem instIsClassicalExtention [Bot Atom] {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') : - IsClassical T' := by grind +open InferenceSystem -/-- 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 +/-- 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*) + [InferenceSystem S (Proposition Atom)] where + /-- Double-negation elimination. -/ + dne (A : Proposition Atom) : S⇓(¬¬A → A) + +-- should this be proof-relevant? +/-- A theory is inconsistent if it derives every proposition. -/ +@[mk_iff] +class IsInconsistent (Atom : Type u) (S : Type*) [InferenceSystem S (Proposition Atom)] where + /-- Every proposition is derivable. -/ + forall_derivableIn (A : Proposition Atom) : DerivableIn S A + +/-- A theory is consistent is there is a non-derivable proposition. -/ +@[mk_iff] +class IsConsistent (Atom : Type u) (S : Type*) [InferenceSystem S (Proposition Atom)] where + /-- Some proposition is not derivable. -/ + exists_not_derivableIn : ∃ A : Proposition Atom, ¬ DerivableIn S A -instance instIsIntuitionisticIntuitionisticCompletion (T : Theory Atom) : - IsIntuitionistic T.intuitionisticCompletion := by grind +omit [DecidableEq Atom] in +lemma isInconsistent_iff_not_isConsistent {S : Type*} [InferenceSystem S (Proposition Atom)] : + IsInconsistent Atom S ↔ ¬ IsConsistent Atom S := by + simp [isInconsistent_iff, isConsistent_iff] end Cslib.Logic.PL.Theory diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean index ba3f5bbac..8bf3b1273 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean @@ -11,8 +11,6 @@ public import Mathlib.Data.Finset.Insert public import Mathlib.Data.Finset.SDiff public import Mathlib.Data.Finset.Image -@[expose] public section - /-! # Natural deduction for propositional logic We define, for minimal logic, deduction trees (a `Type`) and derivability (a `Prop`) relative to a @@ -61,6 +59,8 @@ in §2.2 of Sorensen & Urzyczyn's *Lectures on the Curry-Howard Isomorphism*. (S references welcome!) -/ +@[expose] public section + universe u namespace Cslib.Logic.PL @@ -156,7 +156,7 @@ theorem Theory.equiv_iff {A B : Proposition Atom} : exact ⟨D, E⟩ /-- Minimally equivalent propositions. -/ -abbrev Equiv : Proposition Atom → Proposition Atom → Prop := MPL.Equiv +abbrev Equiv : Proposition Atom → Proposition Atom → Prop := (MPL Atom).Equiv @[inherit_doc] scoped infix:29 " ≡ " => Equiv diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean new file mode 100644 index 000000000..13b7d9b1f --- /dev/null +++ b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean @@ -0,0 +1,347 @@ +/- +Copyright (c) 2025 Thomas Waring. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas Waring +-/ +module + +public import Cslib.Logics.Propositional.NaturalDeduction.Basic +public import Mathlib.Order.Antisymmetrization +public import Mathlib.Tactic.TFAE + +/-! # Results and constructions for propositional theories + +This file provides results and constructions for manipulating proposition theories. + +## Main definitions + +- `Theory.Embedding`, `Theory.WeakerThan` : proof-relevant and -irrelevant ordering between + theories. Any `T` derivations maps along `emb : T.Embedding T'` into a `T'` derivation. +- `Theory.Saturated` : a theory which contains all of its theorems. Every theory `T` can be + completed to a saturated theory `T.saturation`. +- `LEM` and `Pierce` are theories consisting of, respectively, instances of the law of excluded + middle and Pierce's law. These are used for alternative axiomatisations of classical logic. + +## Main results + +- `Theory.WeakerThan` is a preorder, and equality in its poset reflection (expressed as `T ≈ T'`) + is characterised by `T.saturation = T'.saturation`. +- We show that `IPL` is an intuitionistic theory, and that the theories `CPL`, `LEM ∪ IPL` and + `Pierce ∪ IPL` are equivalent and classical. +-/ + +@[expose] public section + +universe u + +namespace Cslib.Logic.PL + +open Proposition Theory InferenceSystem DerivableIn Derivation IsIntuitionistic IsClassical + +variable {Atom : Type u} [DecidableEq Atom] + +namespace Theory + +/-! ### Ordering between theories -/ + +/-- `T.Embedding T'` packages the information required to lift `T`-derivations into + `T'`-derivations. See `Derivation.mapEmbedding`. -/ +protected structure Embedding (T T' : Theory Atom) where + /-- A `T` derivation of every `T`-axiom. -/ + derOfMem {A : Proposition Atom} (hA : A ∈ T) : T'⇓A + +open Embedding + +variable {T T' T'' : Theory Atom} + +/-- Map a derivation along an embedding. -/ +def Derivation.mapEmbedding (emb : T.Embedding T') {Γ : Ctx Atom} {A : Proposition Atom} : + T.Derivation Γ A → T'.Derivation Γ A + | ax hA => (emb.derOfMem hA).weak_ctx (Finset.empty_subset Γ) + | ass hA => ass hA + | andI D E => andI (D.mapEmbedding emb) (E.mapEmbedding emb) + | andE₁ D => andE₁ (D.mapEmbedding emb) + | andE₂ D => andE₂ (D.mapEmbedding emb) + | orI₁ D => orI₁ (D.mapEmbedding emb) + | orI₂ D => orI₂ (D.mapEmbedding emb) + | orE D DA DB => orE (D.mapEmbedding emb) (DA.mapEmbedding emb) (DB.mapEmbedding emb) + | implI _ D => implI _ (D.mapEmbedding emb) + | implE D E => implE (D.mapEmbedding emb) (E.mapEmbedding emb) + +namespace Embedding + +/-- If `T` is a subset of `T'`, `T` embeds into `T'`. -/ +def ofSubset (h : T ⊆ T') : T.Embedding T' := ⟨fun hA => ax (h hA)⟩ + +/-- A theory embeds into itself. -/ +protected def refl : T.Embedding T := ⟨(ax ·)⟩ + +/-- Composition of two embeddings. -/ +protected def comp (emb : T.Embedding T') (emb' : T'.Embedding T'') : T.Embedding T'' := + ⟨fun hA => (emb.derOfMem hA).mapEmbedding emb'⟩ + +end Embedding + +/-- `T` is weaker than `T'` if it embeds into `T'`. This is equivalent to every proposition +derivable in `T` being derivable in `T'`. -/ +def WeakerThan (T T' : Theory Atom) : Prop := Nonempty (T.Embedding T') + +instance : LE (Theory Atom) where + le := Theory.WeakerThan + +lemma WeakerThan.mk' (h : ∀ {A}, A ∈ T → DerivableIn T' A) : T ≤ T' := ⟨⟨fun hA => h hA⟩⟩ + +/-- Noncomputably obtain an embedding from `T ≤ T'`. -/ +noncomputable def WeakerThan.embedding (h : T ≤ T') : T.Embedding T' := h.some + +lemma WeakerThan.of_subset (h : T ⊆ T') : T ≤ T' := ⟨Embedding.ofSubset h⟩ + +/-- Noncomputably turn a `T` derivation into a `T'` derivation, for `T ≤ T'`. -/ +noncomputable def Derivation.mapLE (h : T ≤ T') {Γ : Ctx Atom} {A : Proposition Atom} + (D : T⇓(Γ ⊢ A)) : T'⇓(Γ ⊢ A) := D.mapEmbedding h.embedding + +namespace WeakerThan + +instance instIsPreorderWeakerThan : IsPreorder (Theory Atom) Theory.WeakerThan where + refl _ := ⟨Embedding.refl⟩ + trans _ _ _ h h' := ⟨h.embedding.comp h'.embedding⟩ + +instance instPreorderTheory : Preorder (Theory Atom) where + lt T T' := T ≤ T' ∧ ¬(T' ≤ T) + le_refl T := ⟨Embedding.refl⟩ + le_trans _ _ _ h h' := ⟨h.embedding.comp h'.embedding⟩ + +lemma iff_forall_mem_derivableIn : + T ≤ T' ↔ ∀ {A : Proposition Atom}, A ∈ T → DerivableIn T' A := + ⟨fun h _ hA => ⟨h.embedding.derOfMem hA⟩, .mk'⟩ + +lemma iff_forall_derivableIn_of_derivableIn : + T ≤ T' ↔ ∀ A : Proposition Atom, DerivableIn T A → DerivableIn T' A := by + constructor + · intro h A hA + exact ⟨hA.toDerivation.mapLE h⟩ + · intro h + refine ⟨⟨?_⟩⟩ + intro A hA + exact (h A ⟨ax hA⟩).toDerivation + +instance : Bot (Theory Atom) := ⟨MPL Atom⟩ + +instance : OrderBot (Theory Atom) where + bot_le _ := WeakerThan.of_subset <| Set.empty_subset .. + +instance : Top (Theory Atom) := ⟨Set.univ⟩ + +instance : OrderTop (Theory Atom) where + le_top _ := WeakerThan.of_subset <| Set.subset_univ .. + +end WeakerThan + +open WeakerThan + +/-- Equivalence `T ≈ T'` holds if `T` is weaker than `T'` and vice-versa. -/ +instance theorySetoid : Setoid (Theory Atom) := AntisymmRel.setoid (Theory Atom) WeakerThan + +lemma setoid_def : T ≈ T' ↔ T ≤ T' ∧ T' ≤ T := Iff.rfl + +lemma equiv_iff_forall_mem_derivableIn : + T ≈ T' ↔ (∀ A ∈ T, DerivableIn T' A) ∧ (∀ A ∈ T', DerivableIn T A) := by + simp_rw [setoid_def, iff_forall_mem_derivableIn] + +lemma equiv_iff_forall_derivableIn_derivableIn : + T ≈ T' ↔ ∀ A : Proposition Atom, DerivableIn T A ↔ DerivableIn T' A := by + constructor + · intro ⟨h, h'⟩ A + exact ⟨iff_forall_derivableIn_of_derivableIn.mp h A, + iff_forall_derivableIn_of_derivableIn.mp h' A⟩ + · intro h + refine ⟨iff_forall_derivableIn_of_derivableIn.mpr fun A => (h A).mp, + iff_forall_derivableIn_of_derivableIn.mpr fun A => (h A).mpr⟩ + + +/-! ### Saturated theories -/ + +/-- A theory is saturated if it contains every proposition which it derives. -/ +def Saturated (T : Theory Atom) : Prop := ∀ A : Proposition Atom, DerivableIn T A → A ∈ T + +/-- The saturation of a theory is the collection of all propositions it derives. -/ +def saturation (T : Theory Atom) : Theory Atom := {A : Proposition Atom | DerivableIn T A } + +lemma subset_saturation_self : T ⊆ T.saturation := fun _ hA => ⟨ax hA⟩ + +@[simp] +lemma saturation_le_iff : T.saturation ≤ T' ↔ T ≤ T' := by + rw [iff_forall_mem_derivableIn, iff_forall_derivableIn_of_derivableIn] + simp [saturation] + +lemma saturation_le_self : T.saturation ≤ T := saturation_le_iff.mpr le_rfl + +lemma Saturated.iff_saturation_subset : T.saturation ⊆ T ↔ T.Saturated := Set.setOf_subset + +lemma le_iff_saturation_subset_saturation : T ≤ T' ↔ T.saturation ⊆ T'.saturation := by + rw [iff_forall_derivableIn_of_derivableIn] + rfl + +lemma equiv_iff_saturation_eq : T ≈ T' ↔ T.saturation = T'.saturation := by + simp_rw [setoid_def, le_iff_saturation_subset_saturation, Set.Subset.antisymm_iff] + +lemma saturation_saturated : T.saturation.Saturated := by + rw [←Saturated.iff_saturation_subset, ←le_iff_saturation_subset_saturation] + exact saturation_le_self + +lemma Saturated.TFAE : [T.Saturated, T.saturation ⊆ T, T.saturation = T].TFAE := by + tfae_have 2 ↔ 1 := Saturated.iff_saturation_subset + tfae_have 2 ↔ 3 := by simp [Set.Subset.antisymm_iff, T.subset_saturation_self] + tfae_finish + +@[simp] +lemma saturation_idem : T.saturation.saturation = T.saturation := + Saturated.TFAE.out 0 2 |>.mp saturation_saturated + +lemma isInconsistent_iff_saturation_eq_top : IsInconsistent Atom T ↔ T.saturation = ⊤ := by + simp [isInconsistent_iff, saturation, Top.top, Set.eq_univ_iff_forall] + +/-! ### Intuitionistic and classical theories -/ + +variable [Bot Atom] {T T' T'' : Theory Atom} + +/-- `IPL` is indeed intuitionistic. -/ +instance instIsIntuitionisticIPL : IsIntuitionistic Atom (IPL Atom) where + efq A := ax (efq_mem_ipl A) + +/-- `IPL` embeds into every intuitionisitc theory carries an embedding. -/ +noncomputable def IsIntuitionistic.embeddingIPL [IsIntuitionistic Atom T] : + (IPL Atom).Embedding T where + derOfMem hA := by rw [←Classical.choose_spec hA]; exact efq _ + +/-- If an intuitionistic theory embeds into `T`, it itself is intuitionistic. -/ +@[implicit_reducible] def instIsIntuitionisticOfEmbedding [IsIntuitionistic Atom T] + (emb : T.Embedding T') : IsIntuitionistic Atom T' where + efq A := (efq A : T⇓(⊥ → A)).mapEmbedding emb + +lemma IsIntuitionistic.nonempty_iff_ipl_le : Nonempty (IsIntuitionistic Atom T) ↔ IPL Atom ≤ T := by + constructor + · exact fun ⟨_⟩ => ⟨embeddingIPL⟩ + · exact fun hle => ⟨instIsIntuitionisticOfEmbedding hle.embedding⟩ + +/-- Derivation of efq in an arbitrary context. -/ +def IsIntuitionistic.efqCtx [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Proposition Atom) + : T⇓(Γ ⊢ ⊥ → A) := (efq A : T⇓(⊥ → A)).weak_ctx (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Γ) + +lemma IsIntuitionistic.isInconsistent_iff_derivableIn_bot [IsIntuitionistic Atom T] : + IsInconsistent Atom T ↔ DerivableIn T (⊥ : Proposition Atom) := by + refine ⟨fun h => h.forall_derivableIn ⊥, ?_⟩ + intro ⟨D⟩ + constructor + intro A + exact ⟨efqRule ∅ A D⟩ + +/-- `CPL` is indeed classical. -/ +instance instIsClassicalCPL : IsClassical Atom (CPL Atom) where + dne A := ax (dne_mem_cpl A) + +/-- `CPL` embeds into any classical theory. -/ +noncomputable def IsClassical.embeddingCPL [IsClassical Atom T] : (CPL Atom).Embedding T where + derOfMem hA := by rw [←Classical.choose_spec hA]; exact dne _ + +/-- Obtain `IsClassical Atom T'` from an embedding into `T'` of a classical theory `T`. -/ +@[implicit_reducible] +def instIsClassicalOfEmbedding [IsClassical Atom T] (emb : T.Embedding T') : + IsClassical Atom T' where + dne A := (dne A : T⇓(¬¬A → A)).mapEmbedding emb + +lemma IsClassical.nonempty_iff_cpl_le : Nonempty (IsClassical Atom T) ↔ CPL Atom ≤ T := by + constructor + · exact fun ⟨_⟩ => ⟨embeddingCPL⟩ + · exact fun hle => ⟨instIsClassicalOfEmbedding hle.embedding⟩ + +/-- 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)) |>.weak_ctx <| Finset.empty_subset ..) D.implI + +instance instIsIntuitionisticOfIsClassical [IsClassical Atom T] : IsIntuitionistic Atom T where + efq A := implI _ <| 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 .. + +/-- Proof by cases for a classical theory. -/ +def IsClassical.byCases [IsClassical Atom T] {Γ : Ctx Atom} {A B : Proposition Atom} + (D : T⇓(insert A Γ ⊢ B)) (D' : T⇓(insert (¬ A) Γ ⊢ B)) : T⇓(Γ ⊢ B) := + (lem A |>.weak_ctx <| Finset.empty_subset Γ).orE D D' + +/-- 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 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} + +omit [DecidableEq Atom] in +lemma lem_mem_lem (A : Proposition Atom) : (A ∨ ¬ A) ∈ LEM Atom := ⟨A, rfl⟩ + +/-- `LEM` extends `IPL` to a classical theory. -/ +instance instIsClassicalLEM : IsClassical Atom (LEM Atom ∪ IPL Atom : Theory Atom) where + dne A := by + have : IsIntuitionistic Atom (LEM Atom ∪ IPL Atom : Theory Atom) := + instIsIntuitionisticOfEmbedding (.ofSubset Set.subset_union_right) + apply implI + apply orE (ax <| Set.mem_union_left _ <| lem_mem_lem A) + · exact ass (Finset.mem_insert_self A _) + · apply contra (¬A) A <;> grind + +theorem CPL_equiv_LEM_union_IPL : CPL Atom ≈ (LEM Atom ∪ IPL Atom : Theory Atom) := by + rw [equiv_iff_forall_mem_derivableIn] + constructor + · intro _ hA + exact ⟨(ax hA).mapEmbedding embeddingCPL⟩ + · rintro _ (⟨A, rfl⟩ | ⟨A, rfl⟩) + · exact ⟨lem A⟩ + · exact ⟨efq A⟩ + +/-- The axiom system consisting of instances of Pierce's law. -/ +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⟩ + +/-- Pierce's law extends `IPL` to a classical theory. -/ +instance instIsClassicalPierce : IsClassical Atom (Pierce Atom ∪ IPL Atom : Theory Atom) where + dne A := by + have : IsIntuitionistic Atom (Pierce Atom ∪ IPL Atom : Theory Atom) := + instIsIntuitionisticOfEmbedding (.ofSubset Set.subset_union_right) + apply implI + apply implE (A := (A → ⊥) → A) (ax <| Set.mem_union_left _ <| pierce_mem_pierce A ⊥) + apply implI + apply contra (¬ A) A <;> grind + +theorem CPL_equiv_pierce_union_IPL : CPL Atom ≈ (Pierce Atom ∪ IPL Atom : Theory Atom) := by + rw [equiv_iff_forall_mem_derivableIn] + constructor + · intro _ hA + exact ⟨(ax hA).mapEmbedding embeddingCPL⟩ + · rintro _ (⟨A, B, rfl⟩ | ⟨A, rfl⟩) + · exact ⟨pierce A B⟩ + · exact ⟨efq A⟩ + +end Cslib.Logic.PL.Theory diff --git a/lake-manifest.json b/lake-manifest.json index 3dcdfeb38..b16de692d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2d59066e04cb90e9fa4d1393a8cd1ee8ace8daa7", + "rev": "672768680fb7e4eff7dac7ceca12bc3889fd60fd", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "672768680fb7e4eff7dac7ceca12bc3889fd60fd", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", diff --git a/lakefile.toml b/lakefile.toml index 390db150b..6f836bf81 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -18,6 +18,7 @@ weak.linter.unicodeLinter = false [[require]] name = "mathlib" scope = "leanprover-community" +rev = "672768680fb7e4eff7dac7ceca12bc3889fd60fd" [[lean_lib]] name = "Cslib" @@ -26,6 +27,7 @@ globs = ["Cslib.*"] [[lean_lib]] name = "CslibTests" globs = ["CslibTests.+"] +moreLeanArgs = ["-Dweak.linter.style.header=false"] [[lean_exe]] name = "checkInitImports"