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 φ₂

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} : w ∈ Proposition.denotation m φ ↔ ⇓{ m := m, w := w, φ := φ }

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) : w ∉ Proposition.denotation m (HasNot.not φ) ↔ w ∈ Proposition.denotation m φ

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✝} : Congruence.r (Equiv m) φ₁ φ₂ ↔ denotation m φ₁ = denotation m φ₂

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) φ₁ φ₂) : denotation m φ₁ = denotation m φ₂

grind-friendly first part of Proposition.equiv_iff_denotation_eq.