Denotational semantics for Modal Logic #
A denotational semantics for modal logic, inspired by the one for Hennessy-Milner Logic
(Cslib.Logic.HML).
def
Cslib.Logic.Modal.Proposition.denotation
{World : Type u_1}
{Atom : Type u_2}
(m : Model World Atom)
:
Proposition Atom → Set World
Denotation of a proposition.
Equations
- Cslib.Logic.Modal.Proposition.denotation m (Cslib.Logic.Modal.Proposition.atom p) = {w : World | m.v w p}
- Cslib.Logic.Modal.Proposition.denotation m φ.not = (Cslib.Logic.Modal.Proposition.denotation m φ)ᶜ
- Cslib.Logic.Modal.Proposition.denotation m (φ₁.and φ₂) = Cslib.Logic.Modal.Proposition.denotation m φ₁ ∩ Cslib.Logic.Modal.Proposition.denotation m φ₂
- Cslib.Logic.Modal.Proposition.denotation m φ.diamond = {w : World | ∃ (w' : World), m.r w w' ∧ w' ∈ Cslib.Logic.Modal.Proposition.denotation m φ}
Instances For
theorem
Cslib.Logic.Modal.satisfies_mem_denotation
{World : Type u_1}
{Atom : Type u_2}
{w : World}
{m : Model World Atom}
{φ : Proposition Atom}
:
Characterisation theorem for the denotational semantics.
theorem
Cslib.Logic.Modal.not_denotation
{World : Type u_1}
{Atom : Type u_2}
{w : World}
{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.
theorem
Cslib.Logic.Modal.theoryEq_denotation_eq
{World : Type u_1}
{Atom : Type u_2}
{m : Model World Atom}
{w₁ w₂ : World}
:
TheoryEq m w₁ w₂ ↔ ∀ (φ : Proposition Atom), w₁ ∈ Proposition.denotation m φ ↔ w₂ ∈ Proposition.denotation m φ
Two worlds are theory-equivalent iff they are denotationally equivalent.
theorem
Cslib.Logic.Modal.Proposition.equiv_iff_denotation_eq
{World✝ : Type u_1}
{Atom✝ : Type u_2}
{m : Model World✝ Atom✝}
{φ₁ φ₂ : Proposition Atom✝}
:
Logically equivalent propositions under a model have the same denotation.
theorem
Cslib.Logic.Modal.Proposition.denotation_eq_of_equiv
{World✝ : Type u_1}
{Atom✝ : Type u_2}
{m : Model World✝ Atom✝}
{φ₁ φ₂ : Proposition Atom✝}
(h : Congruence.r (Equiv m) φ₁ φ₂)
:
grind-friendly first part of Proposition.equiv_iff_denotation_eq.