Documentation

Foundation.Modal.Kripke.GL.Completeness

source
@[reducible, inline]
abbrev LO.Modal.Kripke.GLCompleteFrame {α : Type u} [Inhabited α] [DecidableEq α] (p : LO.Modal.Formula α) :
LO.Kripke.FiniteFrame
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem LO.Modal.Kripke.GLCompleteFrame.irreflexive {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} :
    Irreflexive (LO.Modal.Kripke.GLCompleteFrame p).Rel
    source
    theorem LO.Modal.Kripke.GLCompleteFrame.transitive {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} :
    Transitive (LO.Modal.Kripke.GLCompleteFrame p).Rel
    source
    @[reducible, inline]
    abbrev LO.Modal.Kripke.GLCompleteModel {α : Type u} [Inhabited α] [DecidableEq α] (p : LO.Modal.Formula α) :
    LO.Kripke.Model α
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LO.Modal.Kripke.GL_truthlemma {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {X : (LO.Modal.Kripke.GLCompleteModel p).World} (q_sub : q ∈ 𝒮 p) :
      LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.GLCompleteModel p) X q ↔ q ∈ X.formulae
      source
      instance LO.Modal.Kripke.GL_complete {α : Type u} [Inhabited α] [DecidableEq α] :
      LO.Complete 𝐆𝐋 LO.Kripke.TransitiveIrreflexiveFrameClassꟳ#α
      Equations
      • ⋯ = ⋯
      source
      instance LO.Modal.Kripke.instFiniteFramePropertyGLTransitiveIrreflexiveFrameClass {α : Type u} [Inhabited α] [DecidableEq α] :
      LO.Modal.Kripke.FiniteFrameProperty 𝐆𝐋 LO.Kripke.TransitiveIrreflexiveFrameClass
      Equations
      • LO.Modal.Kripke.instFiniteFramePropertyGLTransitiveIrreflexiveFrameClass = LO.Modal.Kripke.FiniteFrameProperty.mk