Documentation

Logic.Modal.Kripke.Grz.Completeness

source
@[reducible, inline]
noncomputable abbrev LO.Modal.Formula.GrzSubformulas {α : Type u} [DecidableEq α] (p : LO.Modal.Formula α) :
LO.Modal.Formulae α
Equations
Instances For
    source
    def LO.Modal.Formula.«term𝒮ᴳ_» :
    Lean.ParserDescr
    Equations
    Instances For
      source
      @[simp]
      theorem LO.Modal.Formula.GrzSubformulas.mem_self {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} :
      p ∈ 𝒮ᴳ p
      source
      theorem LO.Modal.Formula.GrzSubformulas.mem_boximpbox {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (h : q ∈ Finset.prebox (𝒮 p)) :
      □(q ➝ □q) ∈ 𝒮ᴳ p
      source
      theorem LO.Modal.Formula.GrzSubformulas.mem_origin {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (h : q ∈ 𝒮 p) :
      q ∈ 𝒮ᴳ p
      source
      theorem LO.Modal.Formula.GrzSubformulas.mem_imp {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} (h : q ➝ r ∈ 𝒮ᴳ p) :
      q ∈ 𝒮ᴳ p ∧ r ∈ 𝒮ᴳ p
      source
      theorem LO.Modal.Formula.GrzSubformulas.mem_imp₁ {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} (h : q ➝ r ∈ 𝒮ᴳ p) :
      q ∈ 𝒮ᴳ p
      source
      theorem LO.Modal.Formula.GrzSubformulas.mem_imp₂ {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} (h : q ➝ r ∈ 𝒮ᴳ p) :
      r ∈ 𝒮ᴳ p
      source
      @[reducible, inline]
      abbrev LO.Modal.Kripke.GrzCompleteFrame {α : 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.GrzCompleteFrame.reflexive {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} :
        Reflexive (LO.Modal.Kripke.GrzCompleteFrame p).Rel
        source
        theorem LO.Modal.Kripke.GrzCompleteFrame.transitive {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} :
        Transitive (LO.Modal.Kripke.GrzCompleteFrame p).Rel
        source
        theorem LO.Modal.Kripke.GrzCompleteFrame.antisymm {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} :
        Antisymmetric (LO.Modal.Kripke.GrzCompleteFrame p).Rel
        source
        @[reducible, inline]
        abbrev LO.Modal.Kripke.GrzCompleteModel {α : 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.Grz_truthlemma {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {X : (LO.Modal.Kripke.GrzCompleteModel p).World} (q_sub : q ∈ 𝒮 p) :
          LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.GrzCompleteModel p) X q ↔ q ∈ X.formulae
          source
          instance LO.Modal.Kripke.Grz_complete {α : Type u} [Inhabited α] [DecidableEq α] :
          LO.Complete 𝐆𝐫𝐳 LO.Kripke.ReflexiveTransitiveAntisymmetricFrameClassꟳ#α
          Equations
          • ⋯ = ⋯
          source
          instance LO.Modal.Kripke.instFiniteFramePropertyGrzReflexiveTransitiveAntisymmetricFrameClass {α : Type u} [Inhabited α] [DecidableEq α] :
          LO.Modal.Kripke.FiniteFrameProperty 𝐆𝐫𝐳 LO.Kripke.ReflexiveTransitiveAntisymmetricFrameClass
          Equations
          • LO.Modal.Kripke.instFiniteFramePropertyGrzReflexiveTransitiveAntisymmetricFrameClass = LO.Modal.Kripke.FiniteFrameProperty.mk