Basic Modal Logic for Lean

@[reducible, inline]

abbrev Cslib.Logic.Modal.Model.unimodalOfPredicates {τ : PFunctor.{u_1, u_2}} [τ.Unary] {α : Type u_3} (r : α → α → Prop) : Model α τ (α → Prop)

Builds a unimodal predicate model from a binary relation.

Equations

• Cslib.Logic.Modal.Model.unimodalOfPredicates r = Cslib.Logic.Modal.Model.ofPredicates (Cslib.Frame.ofRelation r)

@[reducible, inline]

abbrev Cslib.Logic.Modal.Model.unimodalOfContainers {τ : PFunctor.{u_1, u_2}} [τ.Unary] {α : Type u_3} {β : Type u_4} [Membership α β] (r : α → α → Prop) : Model α τ β

Builds a unimodal container model from a binary relation.

Equations

• Cslib.Logic.Modal.Model.unimodalOfContainers r = Cslib.Logic.Modal.Model.ofContainers (Cslib.Frame.ofRelation r)

theorem Cslib.Logic.Modal.Satisfies.unimodalOfPredicates_preserves_iff {τ : PFunctor.{u_3, u_2}} [τ.Unary] [Unique τ.A] {α : Type u_1} {P : α → Prop} (r : α → α → Prop) : (∀ (a : α), ⇓{ m := Model.unimodalOfPredicates r, w := a, φ := HasImp.imp (Proposition.atom P) (HasBox.box (Proposition.atom P)) }) ↔ Relation.Preserves r P

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

theorem Cslib.Logic.Modal.Satisfies.unimodalOfPredicates_preserves_reflTransGen {τ : PFunctor.{u_3, u_2}} [τ.Unary] [Unique τ.A] {α : Type u_1} {r : α → α → Prop} {P : α → Prop} (h : ∀ (a : α), ⇓{ m := Model.unimodalOfPredicates r, w := a, φ := HasImp.imp (Proposition.atom P) (HasBox.box (Proposition.atom P)) }) (a : α) : ⇓{ m := Model.unimodalOfPredicates (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.