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} (r : α → α → Prop) : Model α (α → Prop)

Given a relation r 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 r = { r := r, v := fun (w : α) (P : α → Prop) => P w }

@[reducible, inline]

abbrev Cslib.Logic.Modal.Model.ofContainers {α : Type u_1} {β : Type u_2} [Membership α β] (r : α → α → Prop) : Model α β

Given a relation r 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 r = { r := r, v := fun (w : α) (p : β) => w ∈ p }

@[reducible, inline]

abbrev Cslib.Logic.Modal.Model.ofSets {α : Type u_1} (r : α → α → Prop) : Model α (Set α)

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

Equations

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

theorem Cslib.Logic.Modal.Model.ofSets_eq_ofPredicates {α : Type u_1} (r : α → α → Prop) : ofSets r = ofPredicates r

The set model and predicate model of a relation are definitionally equal.

Models of Lean predicates

theorem Cslib.Logic.Modal.Satisfies.ofPredicates_atom_iff {α : Type u_1} {a : α} {P : α → Prop} (r : α → α → Prop) : ⇓{ m := Model.ofPredicates r, 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_preserves_iff {α : Type u_1} {P : α → Prop} (r : α → α → Prop) : (∀ (a : α), ⇓{ m := Model.ofPredicates r, w := a, φ := HasImp.imp (Proposition.atom P) (HasBox.box (Proposition.atom P)) }) ↔ Relation.Preserves r P

Under Model.ofPredicates r, P → □P is an axiom iff r preserves P.

@[reducible, inline]

abbrev Cslib.Logic.Modal.Proposition.Equiv.OfPredicates {α : Type u_1} (r : α → α → Prop) (φ₁ φ₂ : Proposition (α → Prop)) : Prop

Logical equivalence under Model.ofPredicates r.

Equations

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

@[reducible, inline]

abbrev Cslib.Logic.Modal.Proposition.Equiv.OfContainers {α : Type u_1} {β : Type u_2} [Membership α β] (r : α → α → Prop) (φ₁ φ₂ : Proposition β) : Prop

Logical equivalence under Model.ofContainers r.

Equations

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

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

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

theorem Cslib.Logic.Modal.Proposition.equivOfContainers_denotation_eq {β : Type u_1} {α : Type u_2} [Membership α β] {r : α → α → Prop} {φ₁ φ₂ : Proposition β} : Congruence.r (Equiv.OfContainers r) φ₁ φ₂ ↔ denotation (Model.ofContainers r) φ₁ = denotation (Model.ofContainers r) φ₂

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

theorem Cslib.Logic.Modal.Proposition.equivOfPredicates_and {α : Type u_1} {r : α → α → Prop} {P Q : α → Prop} : Congruence.r (Equiv.OfPredicates r) (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 Lean modal model induced by r.

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

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

theorem Cslib.Logic.Modal.Satisfies.ofPredicates_preserves_reflTransGen {α : Type u_1} {r : α → α → Prop} {P : α → Prop} (h : ∀ (a : α), ⇓{ m := Model.ofPredicates r, w := a, φ := HasImp.imp (Proposition.atom P) (HasBox.box (Proposition.atom P)) }) (a : α) : ⇓{ m := Model.ofPredicates (Relation.ReflTransGen r), w := a, φ := HasImp.imp (Proposition.atom P) (HasBox.box (Proposition.atom P)) }

Invariants are preserved by the reflexive and transitive closure of the accessibility relation.