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}
{τ : PFunctor.{u_2, u_3}}
{Atom : Type u_4}
(m : Model World τ Atom)
:
Proposition τ Atom → Set World
Denotation of a proposition.
Equations
- One or more equations did not get rendered due to their size.
- Cslib.Logic.Modal.Proposition.denotation m (Cslib.Logic.Modal.Proposition.atom p) = {w : World | m.v w p}
- Cslib.Logic.Modal.Proposition.denotation m Cslib.Logic.Modal.Proposition.false = ∅
- Cslib.Logic.Modal.Proposition.denotation m φ.not = (Cslib.Logic.Modal.Proposition.denotation m φ)ᶜ
- Cslib.Logic.Modal.Proposition.denotation m (φ₁.or φ₂) = Cslib.Logic.Modal.Proposition.denotation m φ₁ ∪ Cslib.Logic.Modal.Proposition.denotation m φ₂
Instances For
theorem
Cslib.Logic.Modal.satisfies_mem_denotation
{World : Type u_1}
{τ : PFunctor.{u_2, u_3}}
{Atom : Type u_4}
{w : World}
{m : Model World τ Atom}
{φ : Proposition τ Atom}
:
Characterisation theorem for the denotational semantics.
theorem
Cslib.Logic.Modal.not_denotation
{World : Type u_1}
{τ : PFunctor.{u_2, u_3}}
{Atom : Type u_4}
{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}
{τ : PFunctor.{u_2, u_3}}
{Atom : Type u_4}
{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}
{τ✝ : PFunctor.{u_2, u_3}}
{Atom✝ : Type u_4}
{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}
{τ✝ : PFunctor.{u_2, u_3}}
{Atom✝ : Type u_4}
{m : Model World✝ τ✝ Atom✝}
{φ₁ φ₂ : Proposition τ✝ Atom✝}
(h : Congruence.r (Equiv m) φ₁ φ₂)
:
grind-friendly first part of Proposition.equiv_iff_denotation_eq.