diff --git a/Cslib.lean b/Cslib.lean index 3ec5b03f6..ed2f5d02e 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -69,6 +69,7 @@ public import Cslib.Foundations.Data.Relation 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.Semantics.FLTS.Basic diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean new file mode 100644 index 000000000..2df2b283a --- /dev/null +++ b/Cslib/Foundations/Logic/Connectives.lean @@ -0,0 +1,114 @@ +/- +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 Composable Logics + +This module defines a typeclass hierarchy for logical connectives, shared across the four +logic levels (Propositional, Modal, Temporal, Bimodal). Each formula type registers itself +as an instance of the appropriate connective class, enabling polymorphic axiom definitions +and notation. + +## Design + +The hierarchy follows the Foundation pattern (FormalizedFormalLogic/Foundation): +- **Atomic classes**: `HasBot`, `HasImp`, `HasBox`, `HasUntil`, `HasSince` +- **Bundled classes**: `PropositionalConnectives`, `ModalConnectives`, + `TemporalConnectives`, `BimodalConnectives` +- **Derived connectives**: `ImpBotDerived` for `neg`, `top`, `or`, `and` from `bot`/`imp` + +Each concrete formula type duplicates its constructors (Lean 4 cannot extend inductives) +and registers as an instance of the appropriate bundled class. + +Falsum and implication are taken as the only propositional primitives because `{imp, bot}` +is functionally complete for classical logic: every other connective is definable, so it can +be a derived `abbrev` rather than a constructor. This keeps the inductive formula types as +small as possible -- minimising the case count in every recursion and induction over formulas +-- and lets the derived connectives unfold to `imp`/`bot` definitionally, so reasoning about +`¬`, `∧`, `∨`, and `↔` needs no separate axioms or bridging lemmas. + +## References + +* [A. Church, *Introduction to Mathematical Logic*][Church1956] +* [A. Heyting, *Die formalen Regeln der intuitionistischen Logik*][Heyting1930] +* [G. Gentzen, *Untersuchungen über das logische Schließen*][Gentzen1935] +* [A. Chagrov, M. Zakharyaschev, *Modal Logic*][ChagrovZakharyaschev1997], Chapter 1 +-/ + +@[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 necessity (box) modality. -/ +class HasBox (F : Type*) where + /-- The necessity/box modality. -/ + box : F → F + +/-- A type has an until temporal operator. -/ +class HasUntil (F : Type*) where + /-- The until temporal operator. -/ + untl : F → F → F + +/-- A type has a since temporal operator. -/ +class HasSince (F : Type*) where + /-- The since temporal operator. -/ + snce : F → F → F + +/-- Propositional connectives: falsum and implication. -/ +class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F + +/-- Modal connectives: propositional connectives plus necessity. -/ +class ModalConnectives (F : Type*) extends PropositionalConnectives F, HasBox F + +/-- Temporal connectives: propositional connectives plus until and since. -/ +class TemporalConnectives (F : Type*) extends PropositionalConnectives F, HasUntil F, HasSince F + +/-- Bimodal connectives: modal connectives plus until and since. + Note: we extend `ModalConnectives` and add `HasUntil`/`HasSince` directly + rather than extending `TemporalConnectives`, to avoid a typeclass diamond. -/ +class BimodalConnectives (F : Type*) extends ModalConnectives F, HasUntil F, HasSince F + +/-- Derived connectives definable from `bot` and `imp` alone. + +Provides `neg`, `top`, `or`, `and` as abbreviations: negation is implication to falsum +(`neg φ := imp φ bot`), verum is `imp bot bot`, disjunction is `imp (neg φ) ψ`, and conjunction +is `neg (imp φ (neg ψ))`. These are forced once `{imp, bot}` is fixed as the primitive basis -- +each is the truth-functional definition of the connective in terms of implication and falsum -- +so the choice carries no information beyond the basis itself. + +**Status**: This class is intentionally uninstantiated. Each concrete formula type +(PL.Proposition, Modal.Proposition, Temporal.Formula, Bimodal.Formula) defines its +own `abbrev` connectives directly on the inductive constructors, which are +definitionally equal to these defaults. Registering typeclass instances would add +resolution overhead at every use site with no benefit, since the `abbrev` definitions +already compute. The class is retained as a specification artifact and for potential +future use in polymorphic proof-system abstractions that need to quantify over derived +connectives generically. -/ +class ImpBotDerived (F : Type*) [HasBot F] [HasImp F] where + /-- Negation: `neg φ := imp φ bot` -/ + neg : F → F := fun φ => HasImp.imp φ HasBot.bot + /-- Top/verum: `top := imp bot bot` -/ + top : F := HasImp.imp HasBot.bot HasBot.bot + /-- Disjunction: `or φ ψ := imp (neg φ) ψ` where `neg φ := imp φ bot` -/ + or : F → F → F := fun φ ψ => HasImp.imp (HasImp.imp φ HasBot.bot) ψ + /-- Conjunction: `and φ ψ := neg (imp φ (neg ψ))` -/ + and : F → F → F := fun φ ψ => + HasImp.imp (HasImp.imp φ (HasImp.imp ψ HasBot.bot)) HasBot.bot + +end Cslib.Logic diff --git a/Cslib/Foundations/Logic/InferenceSystem.lean b/Cslib/Foundations/Logic/InferenceSystem.lean index 854b8deb1..3a111589f 100644 --- a/Cslib/Foundations/Logic/InferenceSystem.lean +++ b/Cslib/Foundations/Logic/InferenceSystem.lean @@ -6,9 +6,9 @@ Authors: Fabrizio Montesi module -public import Cslib.Init +import Cslib.Init -/-! -/ +/-! # Inference System Typeclass -/ @[expose] public section diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index fa3caf53e..98118f9a6 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -1,22 +1,25 @@ /- -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.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), and `imp` (implication); since `{imp, bot}` is functionally complete for + classical logic, conjunction, disjunction, negation, and verum are derived connectives + (`abbrev`s) rather than constructors, keeping the inductive minimal. - `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 @@ -32,6 +35,11 @@ theory. We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum, conjunction, disjunction, implication and negation. + +## References + +* [A. Church, *Introduction to Mathematical Logic*][Church1956] +* [A. Chagrov, M. Zakharyaschev, *Modal Logic*][ChagrovZakharyaschev1997], Chapter 1 -/ @[expose] public section @@ -42,44 +50,54 @@ variable {Atom : Type u} [DecidableEq Atom] namespace Cslib.Logic.PL -/-- Propositions. -/ +/-- Propositions. Primitives are atoms, falsum, and implication. -/ inductive Proposition (Atom : Type u) : Type u where /-- Propositional atoms -/ | atom (x : Atom) - /-- Conjunction -/ - | and (a b : Proposition Atom) - /-- Disjunction -/ - | or (a b : Proposition Atom) + /-- Falsum / bottom -/ + | bot /-- Implication -/ - | impl (a b : Proposition Atom) + | imp (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) +/-- Disjunction as a derived connective: A ∨ B := ¬A → B -/ +abbrev Proposition.or (A B : Proposition Atom) : Proposition Atom := + .imp (.imp A .bot) B -instance instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top⟩ +/-- Conjunction as a derived connective: A ∧ B := ¬(A → ¬B) -/ +abbrev Proposition.and (A B : Proposition Atom) : Proposition Atom := + .imp (.imp A (.imp B .bot)) .bot -example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl +/-- 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 : 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 prefix:40 " ¬ " => Proposition.neg +/-- Register `Proposition` as an instance of `PropositionalConnectives`. -/ +instance : PropositionalConnectives (Proposition Atom) where + bot := .bot + imp := .imp + /-- 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) -- This is probably a lawful monad, but that doesn't seem to be important. instance : Monad Proposition where @@ -102,45 +120,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..eeb2a9c7c 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,18 @@ 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), +implication introduction and elimination, and ex falso quodlibet (bottom elimination). +Conjunction and disjunction rules are derivable from these primitives together with +the definitions of `∧` and `∨` in terms of `→` and `⊥`, so they need not be postulated. ## 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!) +* [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,32 +80,22 @@ 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, implication intro/elim, +and ex falso quodlibet (bottom 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 /-- Assumption -/ | ass {Γ : Ctx Atom} {A : Proposition Atom} (_ : A ∈ Γ) : Derivation Γ A - /-- 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) - /-- 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 + /-- Ex falso quodlibet (bottom elimination) -/ + | botE {Γ : 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 @@ -170,17 +157,9 @@ 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'' => - 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) + | botE D => botE <| D.weak hTheory hCtx /-- Weakening the theory only. -/ def Theory.Derivation.weakTheory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom} @@ -213,9 +192,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 +228,12 @@ 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 - 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) + | botE E => botE <| 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 +241,9 @@ 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) - | 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) + | impI _ D => impI _ <| (Finset.image_insert (· >>= f) _ _) ▸ (D.substAtom f) + | impE D E => impE (D.substAtom f) (E.substAtom f) + | botE D => botE (D.substAtom f) theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom'] {T : Theory Atom} @@ -292,12 +254,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, ?_⟩ diff --git a/references.bib b/references.bib index 973371b65..2a4946b09 100644 --- a/references.bib +++ b/references.bib @@ -49,6 +49,17 @@ @book{Blackburn2001 collection={Cambridge Tracts in Theoretical Computer Science} } +@book{ChagrovZakharyaschev1997, + author = {Chagrov, Alexander and Zakharyaschev, Michael}, + title = {Modal Logic}, + series = {Oxford Logic Guides}, + volume = {35}, + publisher = {Oxford University Press}, + address = {Oxford}, + year = {1997}, + isbn = {978-0-19-853779-3} +} + @misc{Burghardt2018, title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}}, url = {https://arxiv.org/abs/1806.05036v2}, @@ -112,6 +123,16 @@ @misc{ WikipediaMyhillNerode2026 note = {[Online; accessed 9-April-2026]} } +@book{Church1956, + author = {Church, Alonzo}, + title = {Introduction to Mathematical Logic}, + volume = {1}, + publisher = {Princeton University Press}, + address = {Princeton}, + year = {1956}, + isbn = {978-0-691-02906-1} +} + @article{ Chargueraud2012, title = {The {Locally} {Nameless} {Representation}}, volume = {49}, @@ -149,6 +170,17 @@ @article{ FLP1985 numpages = {9} } +@article{Gentzen1935, + author = {Gentzen, Gerhard}, + title = {Untersuchungen {\"u}ber das logische Schlie{\ss}en. {I}}, + journal = {Mathematische Zeitschrift}, + volume = {39}, + number = {1}, + pages = {176--210}, + year = {1935}, + doi = {10.1007/BF01201353} +} + @article{ Girard1987, title={Linear logic}, author={Girard, Jean-Yves}, @@ -204,6 +236,15 @@ @article{ Hennessy1985 bibsource = {dblp computer science bibliography, https://dblp.org} } +@article{Heyting1930, + author = {Heyting, Arend}, + title = {Die formalen Regeln der intuitionistischen Logik}, + journal = {Sitzungsberichte der Preu{\ss}ischen Akademie der + Wissenschaften, physikalisch-mathematische Klasse}, + year = {1930}, + pages = {42--56} +} + @book{ KatzLindell2020, author = {Jonathan Katz and Yehuda Lindell}, @@ -296,6 +337,15 @@ @Book{ Montesi2023 keywords = {choreographic-programming,choreographic-language,choreography,concurrency-theory} } +@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} +} + @article{ Nipkow2001, title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})}, author = {Nipkow, Tobias}, @@ -337,6 +387,18 @@ @Book{ Sangiorgi2011 doi = {10.1017/CBO9780511777110} } +@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} +} + @incollection{ Thomas1990, author = {Wolfgang Thomas}, editor = {Jan van Leeuwen},