From b0d085e1677ba2af96cf7fd67ff8621af56e5cc4 Mon Sep 17 00:00:00 2001 From: benbrastmckie Date: Thu, 2 Jul 2026 17:54:21 -0700 Subject: [PATCH] feat(Logics/Modal): refactor formula primitives to {atom, bot, imp, box} MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Modal formula type with primitives {atom, bot, imp, box}; diamond derived as ¬□¬. Adds self-owned Foundations/Logic/Connectives (HasBox/ModalConnectives), K/T/B/4/5/D validity + canonicity (Basic, Cube), model-class-parametric Proposition.Equiv S integrated with the shared LogicalEquivalence framework (LogicalEquivalence, Denotation). Adds Avigad2022 and ChagrovZakharyaschev1997 references for the cited sources. --- Cslib.lean | 1 + Cslib/Foundations/Logic/Connectives.lean | 91 +++++++ Cslib/Logics/Modal/Basic.lean | 275 ++++++++++++++------- Cslib/Logics/Modal/Cube.lean | 1 + Cslib/Logics/Modal/Denotation.lean | 25 +- Cslib/Logics/Modal/LogicalEquivalence.lean | 218 +++++++++------- CslibTests/GrindLint.lean | 4 + references.bib | 18 ++ 8 files changed, 444 insertions(+), 189 deletions(-) create mode 100644 Cslib/Foundations/Logic/Connectives.lean diff --git a/Cslib.lean b/Cslib.lean index eea1f4491..cb7464daa 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -73,6 +73,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..80164f52f --- /dev/null +++ b/Cslib/Foundations/Logic/Connectives.lean @@ -0,0 +1,91 @@ +/- +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 propositional +and modal logic levels. Each formula type registers itself as an instance of the appropriate +connective class, enabling polymorphic axiom definitions and notation. + +## Design + +The hierarchy adopts a hybrid design, +following the operator-typeclass direction of fmontesi's PR #607 (one class per operator): +- **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr`, `HasBox` +- **Bundled classes**: `PropositionalConnectives`, `ModalConnectives` + +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 +([Avigad2022]); 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. + +## References + +* [J. Avigad, *Mathematical Logic and Computation*][Avigad2022] +-/ + +@[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. + +Box represents universal quantification over accessible worlds (`∀ w', r w w' → φ`), +distributes over implication (axiom K), and is the subject of the necessitation rule. +In classical systems, +diamond (possibility) is derived as `¬□¬φ`. Non-classical modal logics (intuitionistic, +minimal) require a separate `HasDia` typeclass, since `□` and `◇` become independent +operators in those settings. -/ +class HasBox (F : Type*) where + /-- The necessity/box modality. -/ + box : 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 and implication. + +`HasAnd` and `HasOr` are defined as standalone atomic classes in this module. +When all four connectives are needed, use +`[PropositionalConnectives F] [HasAnd F] [HasOr F]`. -/ +class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F + +/-- Modal connectives: propositional connectives plus box (necessity). + +Diamond (possibility) is derivable from box and propositional connectives via +classical negation (`◇φ := ¬□¬φ`) and need not appear in the typeclass. Non-classical modal +logics (intuitionistic, minimal) require extending this class with a primitive `HasDia` once +those formula types are formalized. -/ +class ModalConnectives (F : Type*) extends PropositionalConnectives F, HasBox F + +end Cslib.Logic diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index fda217a1c..94e2402db 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -1,23 +1,48 @@ /- Copyright (c) 2026 Fabrizio Montesi. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Fabrizio Montesi, Marianna Girlando +Authors: Fabrizio Montesi, Marianna Girlando, Benjamin Brast-McKie -/ module public import Cslib.Init +public import Cslib.Foundations.Logic.Connectives public import Cslib.Foundations.Logic.InferenceSystem -public import Mathlib.Data.Set.Basic public import Mathlib.Order.Defs.Unbundled -public import Cslib.Foundations.Relation.Euclidean public import Mathlib.Logic.Nonempty +public import Cslib.Foundations.Relation.Defs /-! # Modal Logic Modal logic is a logic for reasoning about relational structures, studying statements about necessity (`□φ`) and possibility `◇φ`. +## Primitives + +The formula type uses `{atom, bot, imp, box}` as primitive constructors (no native `and`/`or`). +Negation, conjunction, disjunction, and diamond (possibility) are derived connectives via +the Lukasiewicz convention: `¬φ := φ → ⊥`, `φ ∧ ψ := ¬(φ → ¬ψ)`, `φ ∨ ψ := ¬φ → ψ`. + +**Why box, not diamond?** CSLib takes box as primitive because the necessitation rule +(`if ⊢ φ then ⊢ □φ`) and the K axiom (`□(φ → ψ) → (□φ → □ψ)`) are pure proof rules on a +single primitive; with diamond primitive, necessitation becomes the interaction law `¬◇¬` +([P. Blackburn, M. de Rijke, Y. Venema, *Modal Logic*][Blackburn2001] Chapter 1 takes the +diamond-first alternative). See [A. Chagrov, M. Zakharyaschev, +*Modal Logic*][ChagrovZakharyaschev1997] Section 3.1 for the box-first presentation. Box +corresponds to universal quantification over accessible worlds (`∀ w', r w w' → φ`), +preserves conjunction (`□(φ ∧ ψ) ↔ □φ ∧ □ψ`), and distributes over implication (axiom K). +Diamond is then derived classically as +`◇φ := ¬□¬φ`, which corresponds to `(□(φ → ⊥)) → ⊥`. This derivation relies on excluded middle +(`¬¬p ↔ p`) and fails in intuitionistic or minimal modal logic, where box and diamond are +independent operators. Once non-classical modal logics are formalized in CSLib, `HasDia` should +be added as a primitive typeclass alongside `HasBox`. + +Note: The propositional formula type `PL.Proposition` has `and`/`or` as native constructors +with `HasAnd`/`HasOr` instances. The Lukasiewicz convention here is specific to `Modal.Proposition` +because it lacks those constructors. The embedding `PL.Proposition.toModal` (in `FromPropositional`) +therefore encodes `and`/`or` using this convention when translating propositional formulas. + ## References * [P. Blackburn, M. de Rijke, Y. Venema, *Modal Logic*][Blackburn2001] @@ -36,49 +61,111 @@ structure Model (World : Type*) (Atom : Type*) where /-- Valuation of atoms at a world. -/ v : World → Atom → Prop -/-- Propositions. -/ +/-- Propositions. Primitives are atoms, falsum, implication, and necessity (box). -/ inductive Proposition (Atom : Type u) : Type u where /-- Atomic proposition. -/ | atom (p : Atom) - /-- Negation. -/ - | not (φ : Proposition Atom) - /-- Conjunction. -/ - | and (φ₁ φ₂ : Proposition Atom) - /-- Possibility. -/ - | diamond (φ : Proposition Atom) - -@[inherit_doc] scoped prefix:40 "¬" => Proposition.not -@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and -@[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond - -/-- Disjunction. -/ -def Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬(¬φ₁ ∧ ¬φ₂) - -@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or - -/-- Implication. -/ -def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂ - -@[inherit_doc] scoped infix:30 " → " => Proposition.impl + /-- Falsum / bottom. -/ + | bot + /-- Implication. -/ + | imp (φ₁ φ₂ : Proposition Atom) + /-- Necessity / box. -/ + | box (φ : Proposition Atom) + deriving DecidableEq, BEq + +/-- Negation as derived connective: ¬φ := φ → ⊥ -/ +abbrev Proposition.neg (φ : Proposition Atom) : Proposition Atom := .imp φ .bot + +/-- Verum / top: ⊤ := ⊥ → ⊥ -/ +abbrev Proposition.top : Proposition Atom := .imp .bot .bot + +/-- Disjunction: φ₁ ∨ φ₂ := ¬φ₁ → φ₂ -/ +abbrev Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := + .imp (.imp φ₁ .bot) φ₂ + +/-- Conjunction: φ₁ ∧ φ₂ := ¬(φ₁ → ¬φ₂) -/ +abbrev Proposition.and (φ₁ φ₂ : Proposition Atom) : Proposition Atom := + .imp (.imp φ₁ (.imp φ₂ .bot)) .bot + +/-- Possibility / diamond: `◇φ := ¬□¬φ = (□(φ → ⊥)) → ⊥`. + +Diamond is a derived connective in classical modal logic. It is defined via classical negation as +`◇φ := ¬□¬φ`, which expands to `(□(φ → ⊥)) → ⊥`. The forward direction (`◇φ → ¬□¬φ`) holds by +definition; the backward direction (`¬□¬φ → ◇φ`) uses excluded middle. This derivation fails in +minimal modal logic, where `□` and `◇` are independent operators. [Blackburn2001] Chapter 1 +takes diamond as primitive; [ChagrovZakharyaschev1997] Section 3.1 takes box as primitive +and derives diamond via classical negation. -/ +abbrev Proposition.diamond (φ : Proposition Atom) : Proposition Atom := + .neg (.box (.neg φ)) /-- Bi-implication. -/ -def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁) - -@[inherit_doc] scoped infix:30 " ↔ " => Proposition.iff +abbrev Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := + .and (.imp φ₁ φ₂) (.imp φ₂ φ₁) -/-- Necessity. -/ -def Proposition.box (φ : Proposition Atom) : Proposition Atom := ¬◇¬φ +/-- Bottom element of `Proposition Atom`, registered as the canonical `⊥`. -/ +instance : Bot (Proposition Atom) := ⟨.bot⟩ +@[inherit_doc] scoped prefix:40 "¬" => Proposition.neg +@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and +@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or +@[inherit_doc] scoped infix:30 " → " => Proposition.imp @[inherit_doc] scoped prefix:40 "□" => Proposition.box +@[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond +@[inherit_doc] scoped infix:20 " ↔ " => Proposition.iff + +/-- Register `Modal.Proposition` as an instance of `ModalConnectives`. -/ +instance : ModalConnectives (Proposition Atom) where + bot := .bot + imp := .imp + box := .box /-- Satisfaction relation. `Satisfies m w φ` means that, in the model `m`, the world `w` satisfies the proposition `φ`. -/ @[scoped grind] def Satisfies (m : Model World Atom) (w : World) : Proposition Atom → Prop | .atom p => m.v w p - | .not φ => ¬Satisfies m w φ - | .and φ₁ φ₂ => Satisfies m w φ₁ ∧ Satisfies m w φ₂ - | .diamond φ => ∃ w', m.r w w' ∧ Satisfies m w' φ + | .bot => False + | .imp φ₁ φ₂ => Satisfies m w φ₁ → Satisfies m w φ₂ + | .box φ => ∀ w', m.r w w' → Satisfies m w' φ + +/-- Satisfaction of negation. -/ +theorem Satisfies.neg_iff : Satisfies m w (¬φ) ↔ ¬Satisfies m w φ := + ⟨fun h hs => h hs, fun h hs => absurd hs h⟩ + +/-- Satisfaction of diamond. -/ +theorem Satisfies.diamond_iff : Satisfies m w (◇φ) ↔ ∃ w', m.r w w' ∧ Satisfies m w' φ := by + unfold Proposition.diamond Proposition.neg + simp only [Satisfies] + constructor + · intro h + by_contra hc + push Not at hc + exact h fun w' hr hs => absurd hs (hc w' hr) + · intro ⟨w', hr, hs⟩ hbox + exact hbox w' hr hs + +/-- Satisfaction of conjunction. -/ +theorem Satisfies.and_iff : Satisfies m w (φ₁ ∧ φ₂) ↔ Satisfies m w φ₁ ∧ Satisfies m w φ₂ := by + change ((Satisfies m w φ₁ → Satisfies m w φ₂ → False) → False) ↔ _ + constructor + · intro h + constructor + · by_contra h1; exact h (fun hs => absurd hs h1) + · by_contra h2; exact h (fun _ hs => absurd hs h2) + · intro ⟨h1, h2⟩ hf; exact hf h1 h2 + +/-- Satisfaction of disjunction. -/ +theorem Satisfies.or_iff : Satisfies m w (φ₁ ∨ φ₂) ↔ Satisfies m w φ₁ ∨ Satisfies m w φ₂ := by + change ((Satisfies m w φ₁ → False) → Satisfies m w φ₂) ↔ _ + constructor + · intro h + rcases Classical.em (Satisfies m w φ₁) with h1 | h1 + · exact Or.inl h1 + · exact Or.inr (h h1) + · intro h hn + cases h with + | inl h => exact absurd h hn + | inr h => exact h /-- Judgement, representing the conclusions one reaches in modal logic. -/ structure Judgement World Atom where @@ -97,55 +184,55 @@ structure Judgement World Atom where @[simp, scoped grind =] def Satisfies.Bundled (j : Judgement World Atom) : Prop := Satisfies j.m j.w j.φ +/-- Register `Judgement` as a `HasInferenceSystem`, using `Satisfies.Bundled` as the +satisfaction predicate. -/ instance : HasInferenceSystem (Judgement World Atom) := ⟨Satisfies.Bundled⟩ open scoped InferenceSystem Proposition -@[scoped grind =_] +/-- Unfolding lemma: the derivation notation `⇓Modal[m,w ⊨ φ]` equals `Satisfies m w φ`. -/ +@[scoped grind =] theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom} : - Satisfies m w φ = ⇓Modal[m,w ⊨ φ] := rfl + ⇓Modal[m,w ⊨ φ] = Satisfies m w φ := rfl /-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/ @[scoped grind =] -theorem not_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by - induction φ generalizing w <;> grind +theorem neg_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := Satisfies.neg_iff -/-- Characterisation of the `∨` connective. - -Disjunction is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. -/ +/-- Characterisation of the `∨` connective. -/ @[scoped grind =] theorem Satisfies.or_iff_or {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by grind [Proposition.or] - -/-- Characterisation of the `→` connective. + ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := Satisfies.or_iff -Implication is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. --/ +/-- Characterisation of the `→` connective. -/ @[scoped grind =] theorem Satisfies.impl_iff_impl {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by grind [Proposition.impl] + ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := + Iff.rfl -/-- Characterisation of the `↔` connective. +/-- Characterisation of the `□` modality. -/ +@[scoped grind =] +theorem Satisfies.box_iff_forall {m : Model World Atom} : + ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := + Iff.rfl -Bi-implication is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. -/ +/-- Characterisation of the `◇` modality. -/ @[scoped grind =] -theorem Satisfies.iff_iff_iff {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by - simp only [Proposition.iff] - grind [= derivation_def] +theorem Satisfies.diamond_iff_exists {m : Model World Atom} : + ⇓Modal[m,w ⊨ ◇φ] ↔ ∃ w', m.r w w' ∧ ⇓Modal[m,w' ⊨ φ] := Satisfies.diamond_iff -/-- Characterisation of the `□` modality. +/-- Characterisation of `∧` in terms of satisfaction. -/ +@[scoped grind =] +theorem Satisfies.and_iff_and {m : Model World Atom} : + ⇓Modal[m,w ⊨ φ₁ ∧ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∧ ⇓Modal[m,w ⊨ φ₂] := Satisfies.and_iff -Necessity is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. -/ +/-- Characterisation of the `↔` connective. -/ @[scoped grind =] -theorem Satisfies.box_iff_forall {m : Model World Atom} : - ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by grind [Proposition.box] +theorem Satisfies.iff_iff_iff {m : Model World Atom} : + ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by + grind -/-- The theory of a world in a model is the set of all propositions that it satifies. -/ +/-- The theory of a world in a model is the set of all propositions that it satisfies. -/ abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) := {φ | ⇓Modal[m,w ⊨ φ]} @@ -153,16 +240,23 @@ abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) := abbrev TheoryEq (m : Model World Atom) (w₁ w₂ : World) := theory m w₁ = theory m w₂ -theorem TheoryEq.ext_iff : TheoryEq m w₁ w₂ ↔ (∀ φ, φ ∈ theory m w₁ ↔ φ ∈ theory m w₂) := by - grind +/-- Two worlds are theory-equivalent iff they satisfy the same propositions. -/ +theorem TheoryEq.ext_iff : TheoryEq m w₁ w₂ ↔ (∀ φ, φ ∈ theory m w₁ ↔ φ ∈ theory m w₂) := + Set.ext_iff /-- Any proposition satisfied by a world is in the theory of that world. -/ @[scoped grind →] -theorem satisfies_theory (h : Satisfies m w φ) : φ ∈ theory m w := by grind +theorem satisfies_theory (h : Satisfies m w φ) : φ ∈ theory m w := h /-- If two worlds are not theory equivalent, there exists a distinguishing proposition. -/ lemma not_theoryEq_satisfies (h : ¬TheoryEq m w₁ w₂) : - ∃ φ, (⇓Modal[m,w₁ ⊨ φ] ∧ ¬⇓Modal[m,w₂ ⊨ φ]) := by grind [=_ not_satisfies] + ∃ φ, (⇓Modal[m,w₁ ⊨ φ] ∧ ¬⇓Modal[m,w₂ ⊨ φ]) := by + rw [TheoryEq.ext_iff] at h + push Not at h + obtain ⟨φ, h⟩ := h + rcases h with ⟨h1, h2⟩ | ⟨h1, h2⟩ + · exact ⟨φ, h1, h2⟩ + · exact ⟨¬φ, neg_satisfies.mpr h1, fun h3 => neg_satisfies.mp h3 h2⟩ /-- If two worlds are theory equivalent and the former satisfies a proposition, the latter does as well. -/ @@ -174,11 +268,8 @@ theorem theoryEq_satisfies {m : Model World Atom} (h : TheoryEq m w₁ w₂) /-- The K axiom, valid for all models. -/ theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)] := by grind -set_option linter.tacticAnalysis.verifyGrindOnly false in /-- The dual axiom, valid for all models. -/ -theorem Satisfies.dual : ⇓Modal[m,w ⊨ ◇φ ↔ ¬□¬φ] := by - grind only [Satisfies.iff_iff_iff.mpr, → satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl, - =_ derivation_def, = not_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true] +theorem Satisfies.dual : ⇓Modal[m,w ⊨ ◇φ ↔ ¬□¬φ] := iff_iff_iff.mpr Iff.rfl /-- The T axiom, valid for all reflexive models. -/ theorem Satisfies.t {m : Model World Atom} [instRefl : Std.Refl m.r] {w : World} @@ -189,53 +280,52 @@ theorem Satisfies.t_refl {r : World → World → Prop} [Nonempty Atom] (h : ∀ {v} {w} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ φ → ◇φ]) : Std.Refl r where refl w := by have a := Classical.arbitrary Atom - let v := fun (w' : World) (a : Atom) => w' = w - let h' := h (v := v) (w := w) (φ := .atom a) + let v : World → Atom → Prop := fun w' _ => w' = w + have h' := h (v := v) (w := w) (φ := .atom a) grind /-- In any reflexive model, `□φ → φ` is equivalent to `φ → ◇φ`. -/ -theorem Satisfies.t_box_diamond [Std.Refl m.r] : ⇓Modal[m,w ⊨ □φ → φ] ↔ ⇓Modal[m,w ⊨ φ → ◇φ] := by - have := Std.Refl.refl (r := m.r) w +theorem Satisfies.t_box_diamond [Std.Refl m.r] : + ⇓Modal[m,w ⊨ □φ → φ] ↔ ⇓Modal[m,w ⊨ φ → ◇φ] := by + have hrefl := Std.Refl.refl (r := m.r) w grind /-- The B axiom, valid for all symmetric models. -/ -theorem Satisfies.b {m : Model World Atom} [Std.Symm m.r] {w : World} (φ : Proposition Atom) : - ⇓Modal[m,w ⊨ φ → □◇φ] := by - have := Std.Symm.symm (r := m.r) w - grind +theorem Satisfies.b {m : Model World Atom} [instSymm : Std.Symm m.r] {w : World} + (φ : Proposition Atom) : + ⇓Modal[m,w ⊨ φ → □◇φ] := by grind [instSymm.symm] /-- Any model that admits the axiom B is symmetric. -/ theorem Satisfies.b_symm {World Atom} {r : World → World → Prop} [Nonempty Atom] (h : ∀ {v} {w} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ φ → □◇φ]) : Std.Symm r where - symm w₁ := by + symm {w₁ w₂} hr := by have a := Classical.arbitrary Atom - let v₁ := fun (w' : World) (a : Atom) => w' = w₁ - let h₁ := h (v := v₁) (w := w₁) (φ := .atom a) - simp [impl_iff_impl] at h₁ + let v₁ := fun (w' : World) (_ : Atom) => w' = w₁ + have h₁ := h (v := v₁) (w := w₁) (φ := .atom a) grind /-- The 4 axiom, valid for all transitive models. -/ theorem Satisfies.four {m : Model World Atom} [IsTrans World m.r] {w : World} (φ : Proposition Atom) : ⇓Modal[m,w ⊨ ◇◇φ → ◇φ] := by - simp only [impl_iff_impl] intro h - rcases h with ⟨w', h₁, w'', h₂, hs⟩ - exact ⟨w'', IsTrans.trans _ _ _ h₁ h₂, hs⟩ + obtain ⟨w', hr₁, h'⟩ := diamond_iff.mp h + obtain ⟨w'', hr₂, hs⟩ := diamond_iff.mp h' + exact diamond_iff.mpr ⟨w'', IsTrans.trans _ _ _ hr₁ hr₂, hs⟩ /-- Any model that admits 4 is transitive. -/ theorem Satisfies.four_trans {r : World → World → Prop} [Nonempty Atom] (h : ∀ {v} {w} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ ◇◇φ → ◇φ]) : IsTrans World r where trans w₁ w₂ w₃ h₁ h₂ := by have a := Classical.arbitrary Atom - let v := fun (w' : World) (a : Atom) => w' = w₃ - let h' := h (v := v) (w := w₁) (φ := .atom a) + let v := fun (w' : World) (_ : Atom) => w' = w₃ + have h' := h (v := v) (w := w₁) (φ := .atom a) grind /-- The 5 axiom, valid for all Euclidean models. -/ theorem Satisfies.five {m : Model World Atom} [Relation.RightEuclidean m.r] {w : World} (φ : Proposition Atom) : ⇓Modal[m,w ⊨ ◇φ → □◇φ] := by - have := @Relation.RightEuclidean.rightEuclidean (r := m.r) + have heuc := @Relation.RightEuclidean.rightEuclidean (r := m.r) grind /-- Any model that admits 5 is Euclidean. -/ @@ -244,14 +334,15 @@ theorem Satisfies.five_rightEuclidean {r : World → World → Prop} [Nonempty A Relation.RightEuclidean r where rightEuclidean {w₁ w₂ w₃} h₁ h₂ := by have a := Classical.arbitrary Atom - let v := fun (w' : World) (a : Atom) => w' = w₃ - let h' := h (v := v) (w := w₁) (φ := .atom a) + let v := fun (w' : World) (_ : Atom) => w' = w₃ + have h' := h (v := v) (w := w₁) (φ := .atom a) grind /-- The D axiom, valid for all serial models. -/ -theorem Satisfies.d {m : Model World Atom} [Relation.Serial m.r] {w} (φ : Proposition Atom) : +theorem Satisfies.d {m : Model World Atom} [hSer : Relation.Serial m.r] {w} + (φ : Proposition Atom) : ⇓Modal[m,w ⊨ □φ → ◇φ] := by - have : ∃ w', m.r w w' := Relation.Serial.serial w + have hex : ∃ w', m.r w w' := hSer.serial w grind /-- Any model that admits D is serial. -/ @@ -259,8 +350,8 @@ theorem Satisfies.d_serial {r : World → World → Prop} [Nonempty Atom] (h : ∀ {v} {w} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ □φ → ◇φ]) : Relation.Serial r where serial w₁ := by have a := Classical.arbitrary Atom - let v := fun (w' : World) (a : Atom) => w' = w₁ - let h' := h (v := v) (w := w₁) (φ := .atom a) + let v := fun (_ : World) (_ : Atom) => True + have h' := h (v := v) (w := w₁) (φ := .atom a) grind /-- A proposition is valid in a class of models `S` (modelled as a set) if it is satisfied under diff --git a/Cslib/Logics/Modal/Cube.lean b/Cslib/Logics/Modal/Cube.lean index 98e825014..91e411802 100644 --- a/Cslib/Logics/Modal/Cube.lean +++ b/Cslib/Logics/Modal/Cube.lean @@ -7,6 +7,7 @@ Authors: Fabrizio Montesi, Marianna Girlando module public import Cslib.Logics.Modal.Basic +public import Cslib.Foundations.Relation.Euclidean /-! # Modal Logic Cube diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean index b74e8f3f1..206ebaed4 100644 --- a/Cslib/Logics/Modal/Denotation.lean +++ b/Cslib/Logics/Modal/Denotation.lean @@ -1,12 +1,13 @@ /- Copyright (c) 2026 Fabrizio Montesi. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Fabrizio Montesi +Authors: Fabrizio Montesi, Benjamin Brast-McKie -/ module public import Cslib.Logics.Modal.Basic +public import Mathlib.Data.Set.Basic /-! # Denotational semantics for Modal Logic @@ -25,9 +26,9 @@ open scoped Proposition InferenceSystem def Proposition.denotation (m : Model World Atom) : Proposition Atom → Set World | .atom p => {w | m.v w p} - | .not φ => (φ.denotation m)ᶜ - | .and φ₁ φ₂ => φ₁.denotation m ∩ φ₂.denotation m - | .diamond φ => {w | ∃ w', m.r w w' ∧ w' ∈ φ.denotation m} + | .bot => ∅ + | .imp φ₁ φ₂ => (φ₁.denotation m)ᶜ ∪ φ₂.denotation m + | .box φ => {w | ∀ w', m.r w w' → w' ∈ φ.denotation m} /-- Characterisation theorem for the denotational semantics. -/ @[scoped grind =] @@ -38,14 +39,24 @@ theorem satisfies_mem_denotation {m : Model World Atom} {φ : Proposition Atom} /-- A world is in the denotation of a proposition iff it is not in the denotation of the negation of the proposition. -/ @[scoped grind =] -theorem not_denotation {m : Model World Atom} (φ : Proposition Atom) : +theorem neg_denotation {m : Model World Atom} (φ : Proposition Atom) : w ∉ (¬φ).denotation m ↔ w ∈ φ.denotation m := by - grind [_=_ satisfies_mem_denotation] + simp [Proposition.denotation] /-- Two worlds are theory-equivalent iff they are denotationally equivalent. -/ theorem theoryEq_denotation_eq {m : Model World Atom} {w₁ w₂ : World} : (TheoryEq m w₁ w₂) ↔ (∀ (φ : Proposition Atom), w₁ ∈ (φ.denotation m) ↔ w₂ ∈ (φ.denotation m)) := by - apply Iff.intro <;> grind [_=_ satisfies_mem_denotation] + constructor + · intro h φ + have hext := TheoryEq.ext_iff.mp h φ + exact ⟨fun h₁ => satisfies_mem_denotation.mpr (hext.mp (satisfies_mem_denotation.mp h₁)), + fun h₂ => satisfies_mem_denotation.mpr (hext.mpr (satisfies_mem_denotation.mp h₂))⟩ + · intro h + apply TheoryEq.ext_iff.mpr + intro φ + have hd := h φ + exact ⟨fun h₁ => satisfies_mem_denotation.mp (hd.mp (satisfies_mem_denotation.mpr h₁)), + fun h₂ => satisfies_mem_denotation.mp (hd.mpr (satisfies_mem_denotation.mpr h₂))⟩ end Cslib.Logic.Modal diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean index 0fc089e4e..53492ed70 100644 --- a/Cslib/Logics/Modal/LogicalEquivalence.lean +++ b/Cslib/Logics/Modal/LogicalEquivalence.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Copyright (c) 2026 Fabrizio Montesi, Benjamin Brast-McKie. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Fabrizio Montesi +Authors: Fabrizio Montesi, Benjamin Brast-McKie -/ module @@ -9,124 +9,162 @@ module public import Cslib.Logics.Modal.Basic public import Cslib.Foundations.Logic.LogicalEquivalence -/-! # Logical Equivalence in Modal Logic +/-! # Logical Equivalence for Modal Propositions -This module defines logical equivalence for modal propositions. -The definitions are parametric on the class of models under consideration. +This file defines a one-hole context for `Proposition`, a fill operation that substitutes a +proposition into the hole, and the model-class-parametric equivalence `Proposition.Equiv S`, +which is instantiated as an instance of the `LogicalEquivalence` framework +(`Cslib.Foundations.Logic.LogicalEquivalence`). -We also instantiate `LogicalEquivalence` for Modal Logic K, i.e., equivalence -for the class of all models. +## Main Definitions + +* `Proposition.Context` -- a one-hole context matching the fork's `Proposition` constructors +* `Proposition.Context.fill` -- substitute a proposition into the hole +* `Proposition.Equiv S` -- two propositions are equivalent in the class of models `S`: they agree + on satisfaction at every model in `S` and every world +* `≡[S]` / `≡` -- notation for `Proposition.Equiv S` / `Proposition.Equiv Set.univ` +* `Satisfies.Context` -- a judgemental context for `Judgement` +* The `LogicalEquivalence (Proposition Atom) (Judgement World Atom) Satisfies.Bundled` instance, + registering Modal logic K's equivalence with the shared Foundations framework + +## Design Notes + +The `Context` constructors mirror the recursive positions of `Proposition`: `imp` has two +sub-proposition positions (left and right), and `box` has one. The ground constructors `atom` and +`bot` have no sub-propositions, so they do not appear in `Context`. + +`Proposition.Equiv` is parametric in the model class `S`, mirroring the parametricity of +`Proposition.valid` (`Basic.lean`). This lets equivalence be stated relative to any frame class +(e.g. the T/B/4/5/S4/S5 classes from `Cube.lean`), not just the class of all models: `◇□φ ≡[S] □φ` +is an S5 fact that is inexpressible with an equivalence hardwired to all models. The unqualified +`≡` is `Equiv Set.univ`, matching the all-models equivalence used by `Cslib.Logic.HML`. -/ @[expose] public section namespace Cslib.Logic.Modal -open scoped InferenceSystem Proposition Satisfies +open scoped InferenceSystem Proposition -/-- The modal propositions `φ₁` and `φ₂` are equivalent in the class of models `S`. -/ -def Proposition.Equiv (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) - : Prop := +/-- A one-hole context for `Proposition`. Each constructor corresponds to a recursive position +in `Proposition`: `impL` is the left argument of `imp`, `impR` is the right argument, and `box` +is the argument of `box`. The `hole` constructor marks the position to be filled. -/ +inductive Proposition.Context (Atom : Type u) : Type u where + /-- The position to substitute. -/ + | hole + /-- Context in the left argument of `imp`. -/ + | impL (c : Context Atom) (φ : Proposition Atom) + /-- Context in the right argument of `imp`. -/ + | impR (φ : Proposition Atom) (c : Context Atom) + /-- Context under `box`. -/ + | box (c : Context Atom) + +/-- Fill the hole in a context with a proposition. -/ +def Proposition.Context.fill : Proposition.Context Atom → Proposition Atom → Proposition Atom + | .hole, φ => φ + | .impL c ψ, φ => c.fill φ → ψ + | .impR ψ c, φ => ψ → c.fill φ + | .box c, φ => □(c.fill φ) + +instance : HasContext (Proposition Atom) := ⟨Proposition.Context Atom, Proposition.Context.fill⟩ + +open scoped Proposition.Context + +/-- Two propositions `φ₁` and `φ₂` are logically equivalent in the class of models `S` when they +agree on satisfaction at every model in `S` and every world. -/ +def Proposition.Equiv (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) : Prop := ∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] @[inherit_doc] -scoped notation φ₁ " ≡[" S "] " φ₂ => Proposition.Equiv S φ₁ φ₂ +scoped notation:50 φ₁ " ≡[" S "] " φ₂ => Proposition.Equiv S φ₁ φ₂ @[inherit_doc] -scoped notation φ₁ " ≡ " φ₂ => Proposition.Equiv Set.univ φ₁ φ₂ +scoped notation:50 φ₁ " ≡ " φ₂ => Proposition.Equiv Set.univ φ₁ φ₂ +/-- Unfolding lemma for `Proposition.Equiv`. -/ @[scoped grind =] theorem Proposition.equiv_def (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) : - (φ₁ ≡[S] φ₂) ↔ - (∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) := by rfl + (φ₁ ≡[S] φ₂) ↔ (∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) := Iff.rfl +/-- `Proposition.Equiv` characterised as agreement of satisfaction, splitting the object-level +`↔` into the meta-level `Iff`. -/ @[scoped grind =] theorem Proposition.equiv_iff (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) : - (φ₁ ≡[S] φ₂) ↔ - (∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by - simp [Proposition.equiv_def, Satisfies.iff_iff_iff] - -theorem Proposition.equiv_valid (S : Set (Model World Atom)) - (φ₁ φ₂ : Proposition Atom) (h : φ₁ ≡[S] φ₂) : - (φ₁.valid S ↔ φ₂.valid S) := by - grind - -/-- Propositional contexts. -/ -inductive Proposition.Context (Atom : Type u) : Type u where - | hole - | not (c : Context Atom) - | andL (c : Context Atom) (φ : Proposition Atom) - | andR (φ : Proposition Atom) (c : Context Atom) - | diamond (c : Context Atom) - -/-- Replaces a hole in a propositional context with a proposition. -/ -@[scoped grind =] -def Proposition.Context.fill (c : Context Atom) (φ : Proposition Atom) := - match c with - | hole => φ - | not c => .not (c.fill φ) - | andL c φ' => (c.fill φ).and φ' - | andR φ' c => φ'.and (c.fill φ) - | diamond c => .diamond (c.fill φ) - -instance : HasContext (Proposition Atom) := ⟨Proposition.Context Atom, Proposition.Context.fill⟩ - -@[scoped grind =_] -lemma Proposition.Context.fill_def {Γ : HasContext.Context (Proposition Atom)} : - Γ.fill φ = Γ<[φ] := rfl - -open scoped Proposition Proposition.Context - -/-- Logical equivalence is an equivalence relation. -/ -instance {World Atom} (S : Set (Model World Atom)) : - IsEquiv (Proposition Atom) (Proposition.Equiv S) := by - rw [← equivalence_iff_isEquiv] - grind [Equivalence] - -/-- Logical equivalence is a congruence. -/ -instance {World Atom} (S : Set (Model World Atom)) : - Congruence (Proposition Atom) (Proposition.Equiv S) where - elim ctx φ₁ φ₂ heqv m hₘ w := by - induction ctx generalizing w - case hole => grind - case not c ih | andL c ih | andR c ih => - specialize ih w - grind - case diamond c ih => - rw [Satisfies.iff_iff_iff] - apply Iff.intro - all_goals - rintro ⟨w', h⟩ - specialize ih w' - grind - -/-- Judgemental contexts. -/ + (φ₁ ≡[S] φ₂) ↔ (∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by + simp only [Proposition.equiv_def] + constructor + · intro h m hm w + have hh := h m hm w + rw [Proposition.iff, Satisfies.and_iff_and, Satisfies.impl_iff_impl, + Satisfies.impl_iff_impl] at hh + rw [derivation_def, derivation_def] + exact ⟨hh.1, hh.2⟩ + · intro h m hm w + have hh := h m hm w + rw [Proposition.iff, Satisfies.and_iff_and, Satisfies.impl_iff_impl, Satisfies.impl_iff_impl] + rw [derivation_def, derivation_def] at hh + exact ⟨hh.1, hh.2⟩ + +/-- Logically equivalent propositions are valid in the same models: `Equiv` bridges to +`Proposition.valid`. -/ +theorem Proposition.equiv_valid (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) + (h : φ₁ ≡[S] φ₂) : φ₁.valid S ↔ φ₂.valid S := by + rw [Proposition.equiv_iff] at h + simp only [Proposition.valid] + exact ⟨fun hv m hm w => (h m hm w).mp (hv m hm w), fun hv m hm w => (h m hm w).mpr (hv m hm w)⟩ + +instance (S : Set (Model World Atom)) : IsEquiv (Proposition Atom) (Proposition.Equiv S) where + refl a := by rw [Proposition.equiv_iff]; grind + symm a b h := by rw [Proposition.equiv_iff] at h ⊢; grind + trans a b c h1 h2 := by rw [Proposition.equiv_iff] at h1 h2 ⊢; grind + +instance (S : Set (Model World Atom)) : Congruence (Proposition Atom) (Proposition.Equiv S) where + elim : + Covariant (Proposition.Context Atom) (Proposition Atom) (Proposition.Context.fill) + (Proposition.Equiv S) := by + intro ctx φ₁ φ₂ heqv + rw [Proposition.equiv_iff] at heqv ⊢ + intro m hm w + induction ctx generalizing w with + | hole => exact heqv m hm w + | impL c φ ih => + simp only [Proposition.Context.fill, derivation_def] + exact ⟨fun hf ha => hf ((ih w).mpr ha), fun hf ha => hf ((ih w).mp ha)⟩ + | impR φ c ih => + simp only [Proposition.Context.fill, derivation_def] + exact ⟨fun hf ha => (ih w).mp (hf ha), fun hf ha => (ih w).mpr (hf ha)⟩ + | box c ih => + simp only [Proposition.Context.fill, derivation_def] + exact ⟨fun hf w' hr => (ih w').mp (hf w' hr), fun hf w' hr => (ih w').mpr (hf w' hr)⟩ + +/-- Judgemental contexts for Modal logic: a model together with a world, into which a +proposition is placed to form a `Judgement`. -/ structure Satisfies.Context (World Atom : Type*) where /-- The model to consider. -/ m : Model World Atom - /-- The world to check propositions against. -/ + /-- The world to check the proposition against. -/ w : World /-- Fills a judgemental context with a proposition. -/ def Satisfies.Context.fill (c : Satisfies.Context World Atom) (φ : Proposition Atom) : - Judgement World Atom := Modal[c.m, c.w ⊨ φ] + Judgement World Atom := + Modal[c.m, c.w ⊨ φ] -instance judgementalContext : - HasHContext (Judgement World Atom) (Proposition Atom) := +instance judgementalContext : HasHContext (Judgement World Atom) (Proposition Atom) := ⟨Satisfies.Context World Atom, Satisfies.Context.fill⟩ -@[scoped grind =_] -lemma Satisfies.Context.fill_def {c : Satisfies.Context World Atom} : - Modal[c.m,c.w ⊨ φ] = c<[φ] := rfl - -open scoped Satisfies.Context - -/-- Logical equivalence for Modal Logic K. That is, no assumptions on models are made. -/ -instance : LogicalEquivalence - (Proposition Atom) (Judgement World Atom) Satisfies.Bundled where +/-- Modal logic K's equivalence, registered as an instance of the `LogicalEquivalence` +framework: equivalence relative to the class of all models (`Proposition.Equiv Set.univ`) +preserves validity of judgements under any judgemental context. -/ +instance : LogicalEquivalence (Proposition Atom) (Judgement World Atom) Satisfies.Bundled where eqv := Proposition.Equiv Set.univ - eqvFillValid heqv c h := by - specialize heqv c.m - grind + eqvFillValid {φ₁ φ₂ : Proposition Atom} (heqv : φ₁ ≡ φ₂) + (c : HasHContext.Context (Judgement World Atom) (Proposition Atom)) + (h : Satisfies.Bundled c<[φ₁]) : Satisfies.Bundled c<[φ₂] := by + rw [Proposition.equiv_iff] at heqv + have hw := heqv c.m (Set.mem_univ c.m) c.w + simp only [derivation_def] at hw + simp only [Satisfies.Bundled, HasHContext.fill, Satisfies.Context.fill] at h ⊢ + exact hw.mp h end Cslib.Logic.Modal diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean index deba30056..5ecaa2f0d 100644 --- a/CslibTests/GrindLint.lean +++ b/CslibTests/GrindLint.lean @@ -85,6 +85,10 @@ open_scoped_all Cslib #grind_lint skip Cslib.LTS.IsBisimulation.traceEq #grind_lint skip Cslib.LTS.IsBisimulationUpTo.isBisimulation #grind_lint skip Cslib.Logic.HML.theoryEq_isBisimulation +#grind_lint skip Cslib.Logic.Modal.neg_denotation +#grind_lint skip Cslib.Logic.Modal.Satisfies.and_iff_and +#grind_lint skip Cslib.Logic.Modal.Satisfies.iff_iff_iff +#grind_lint skip Cslib.Logic.Modal.Satisfies.or_iff_or #guard_msgs in #grind_lint check (min := 20) in Cslib diff --git a/references.bib b/references.bib index 984dc6e23..9ff5cd86b 100644 --- a/references.bib +++ b/references.bib @@ -30,6 +30,14 @@ @article{AngluinLaird1988 doi = {10.1007/BF00116829} } +@book{Avigad2022, + author = {Jeremy Avigad}, + title = {Mathematical Logic and Computation}, + publisher = {Cambridge University Press}, + year = {2022}, + isbn = {978-1-108-84072-1} +} + @book{Baader1998, author = {Baader, Franz and Nipkow, Tobias}, title = {Term rewriting and all that}, @@ -49,6 +57,16 @@ @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}, + 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},