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 φ.neg = (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}
:
w ∈ Proposition.denotation m φ ↔ InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ }
Characterisation theorem for the denotational semantics.
theorem
Cslib.Logic.Modal.neg_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.