Modal Logic for Lean

This module develops the interplay between modal logic and Lean's propositional language, in order to enable the use of modal logic to reason about standard Lean relations using Prop.

@[reducible, inline]

abbrev Cslib.Logic.Modal.Model.ofPredicates {α : Type u_1} {τ : PFunctor.{u_2, u_3}} (f : Frame α τ) : Model α τ (α → Prop)

Given a frame f on α, constructs the modal model whose worlds are elements of α and whose atoms are Lean predicates on α (α → Prop).

Valuation checks that a world satisfies a predicate. For example, under Model.ofPredicates r, □P at a : α means that P a' holds at every a' such that r a a'.

Equations

• Cslib.Logic.Modal.Model.ofPredicates f = { toFrame := f, v := fun (w : α) (P : α → Prop) => P w }

@[reducible, inline]

abbrev Cslib.Logic.Modal.Model.ofContainers {α : Type u_1} {β : Type u_2} {τ : PFunctor.{u_3, u_4}} [Membership α β] (f : Frame α τ) : Model α τ β

Given a frame f on α and a container type β for α (Membership α β), constructs the modal model whose worlds are elements of α and whose atoms are of type β.

Valuation is membership. For example, under Model.ofContainers r, □b at a : α means that a' ∈ b holds for every a' such that r a a'.

Equations

• Cslib.Logic.Modal.Model.ofContainers f = { toFrame := f, v := fun (w : α) (p : β) => w ∈ p }

@[reducible, inline]

abbrev Cslib.Logic.Modal.Model.ofSets {α : Type u_1} {τ : PFunctor.{u_2, u_3}} (f : Frame α τ) : Model α τ (Set α)

Abbreviation for Model.ofContainers where the container type is a Set.

Equations

• Cslib.Logic.Modal.Model.ofSets f = Cslib.Logic.Modal.Model.ofContainers f

theorem Cslib.Logic.Modal.Model.ofSets_v_eq_ofPredicates_v {α : Type u_1} {τ : PFunctor.{u_2, u_3}} (f : Frame α τ) (w : α) (P : α → Prop) : (ofSets f).v w (Set.ofPred P) = (ofPredicates f).v w P

The valuations of the set model and the predicate model of a frame agree under Set.ofPred.

theorem Cslib.Logic.Modal.Satisfies.ofPredicates_atom_iff {α : Type u_1} {τ : PFunctor.{u_2, u_3}} {a : α} {P : α → Prop} (f : Frame α τ) : ⇓{ m := Model.ofPredicates f, w := a, φ := Proposition.atom P } ↔ P a

Under Model.ofPredicates r, an atomic proposition P holds at a iff P a.

theorem Cslib.Logic.Modal.Satisfies.ofPredicates_preservesMap_iff {α : Type u_1} {τ : PFunctor.{u_2, u_3}} {op : τ.A} {P : α → Prop} {Ps : τ.B op → α → Prop} (f : Frame α τ) : (∀ (w : α), ⇓{ m := Model.ofPredicates f, w := w, φ := HasImp.imp (Proposition.atom P) (HasNabla.nabla op fun (i : τ.B op) => Proposition.atom (Ps i)) }) ↔ f.PreservesMap op P Ps

In the predicate model generated by f, P → ∇[op]Ps holds everywhere iff op preserves the predicate map Ps from P.

theorem Cslib.Logic.Modal.Satisfies.ofContainers_atom_iff {α : Type u_1} {β : Type u_2} {τ : PFunctor.{u_3, u_4}} {w : α} [Membership α β] {f : Frame α τ} {b : β} : ⇓{ m := Model.ofContainers f, w := w, φ := Proposition.atom b } ↔ w ∈ b

@[reducible, inline]

abbrev Cslib.Logic.Modal.Proposition.Equiv.OfPredicates {α : Type u_1} {τ : PFunctor.{u_2, u_3}} (f : Frame α τ) (φ₁ φ₂ : Proposition τ (α → Prop)) : Prop

Logical equivalence under Model.ofPredicates.

Equations

• Cslib.Logic.Modal.Proposition.Equiv.OfPredicates f = Cslib.Logic.Modal.Proposition.Equiv (Cslib.Logic.Modal.Model.ofPredicates f)

@[reducible, inline]

abbrev Cslib.Logic.Modal.Proposition.Equiv.OfContainers {α : Type u_1} {β : Type u_2} {τ : PFunctor.{u_3, u_4}} [Membership α β] (f : Frame α τ) (φ₁ φ₂ : Proposition τ β) : Prop

Logical equivalence under Model.ofContainers.

Equations

• Cslib.Logic.Modal.Proposition.Equiv.OfContainers f = Cslib.Logic.Modal.Proposition.Equiv (Cslib.Logic.Modal.Model.ofContainers f)

theorem Cslib.Logic.Modal.Proposition.equivOfPredicates_denotation_eq {α : Type u_1} {τ : PFunctor.{u_2, u_3}} {f : Frame α τ} {φ₁ φ₂ : Proposition τ (α → Prop)} : Congruence.r (Equiv.OfPredicates f) φ₁ φ₂ ↔ denotation (Model.ofPredicates f) φ₁ = denotation (Model.ofPredicates f) φ₂

Logically equivalent propositions under Equiv.OfPredicates f have the same denotation in the Lean modal model induced by ofPredicates f.

theorem Cslib.Logic.Modal.Proposition.equivOfContainers_denotation_eq {α : Type u_1} {β : Type u_2} {τ : PFunctor.{u_3, u_4}} [Membership α β] {f : Frame α τ} {φ₁ φ₂ : Proposition τ β} : Congruence.r (Equiv.OfContainers f) φ₁ φ₂ ↔ denotation (Model.ofContainers f) φ₁ = denotation (Model.ofContainers f) φ₂

Logically equivalent propositions under Equiv.OfContainers f have the same denotation in the modal model induced by Model.ofContainers f.

theorem Cslib.Logic.Modal.Proposition.equivOfPredicates_and {α : Type u_1} {τ : PFunctor.{u_2, u_3}} {f : Frame α τ} {P Q : α → Prop} : Congruence.r (Equiv.OfPredicates f) (atom fun (a : α) => P a ∧ Q a) (HasAnd.and (atom P) (atom Q))

Pointwise conjunction of Lean predicates is logically equivalent to their modal conjunction in the predicate model induced by f.

theorem Cslib.Logic.Modal.Proposition.ofContainers_inf_equiv {α : Type u_1} {β : Type u_2} {τ : PFunctor.{u_3, u_4}} [Membership α β] [Min β] (f : Frame α τ) (p q : β) (h : ∀ (x : α), x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q) : Congruence.r (Equiv.OfContainers f) (atom (p ⊓ q)) (HasAnd.and (atom p) (atom q))

Under Equiv.OfContainers f, if membership in the infimum of two containers is equivalent to membership in both containers, then atomic infimum is logically equivalent to modal conjunction.