@[reducible, inline]

noncomputable abbrev LO.Modal.Standard.Kripke.GLCanonicalFrame {α : Type u} [Inhabited α] [DecidableEq α] : LO.Modal.Standard.Kripke.Frame

Equations

• LO.Modal.Standard.Kripke.GLCanonicalFrame = LO.Modal.Standard.Kripke.CanonicalFrame 𝐆𝐋

@[reducible, inline]

noncomputable abbrev LO.Modal.Standard.Kripke.GLCanonicalModel {α : Type u} [Inhabited α] [DecidableEq α] : LO.Modal.Standard.Kripke.Model α

Equations

• LO.Modal.Standard.Kripke.GLCanonicalModel = LO.Modal.Standard.Kripke.CanonicalModel 𝐆𝐋

theorem LO.Modal.Standard.Kripke.filter_truthlemma {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Inhabited (Λ)-MCT] [Λ.IsNormal] {T : LO.Modal.Standard.Theory α} [T.SubformulaClosed] {X : (LO.Modal.Standard.Kripke.CanonicalModel Λ).World} {Y : (LO.Modal.Standard.Kripke.CanonicalModel Λ).World} (hXY : autoParam (LO.Modal.Standard.Kripke.filterEquiv (LO.Modal.Standard.Kripke.CanonicalModel Λ) T X Y) _auto✝) {p : LO.Modal.Standard.Formula α} (hp : autoParam (p ∈ T) _auto✝) : p ∈ X.theory ↔ p ∈ Y.theory

@[reducible, inline]

noncomputable abbrev LO.Modal.Standard.Kripke.GLFilteredFrame {α : Type u} [Inhabited α] [DecidableEq α] (p : LO.Modal.Standard.Formula α) : LO.Modal.Standard.Kripke.FiniteFrame

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Modal.Standard.Kripke.GLFilteredFrame.def_rel {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Standard.Formula α} {X : LO.Modal.Standard.Kripke.GLCanonicalFrame.World} {Y : LO.Modal.Standard.Kripke.GLCanonicalFrame.World} : (LO.Modal.Standard.Kripke.GLFilteredFrame p).Rel ⟦X⟧ ⟦Y⟧ ↔ (∀ q ∈ □''⁻¹↑(𝒮 p), □q ∈ X.theory → q ⋏ □q ∈ Y.theory) ∧ ∃ r ∈ □''⁻¹↑(𝒮 p), □r ∉ X.theory ∧ □r ∈ Y.theory

@[reducible, inline]

noncomputable abbrev LO.Modal.Standard.Kripke.GLFilteredModel {α : Type u} [Inhabited α] [DecidableEq α] (p : LO.Modal.Standard.Formula α) : LO.Modal.Standard.Kripke.Model α

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Modal.Standard.Kripke.irreflexive_GLFilteredFrame {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Standard.Formula α} : Irreflexive (LO.Modal.Standard.Kripke.GLFilteredFrame p).Rel

theorem LO.Modal.Standard.Kripke.transitive_GLFilteredFrame {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Standard.Formula α} : Transitive (LO.Modal.Standard.Kripke.GLFilteredFrame p).Rel

theorem LO.Modal.Standard.Kripke.GL_truthlemma {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Standard.Formula α} {X : (LO.Modal.Standard.Kripke.CanonicalModel 𝐆𝐋).World} {q : LO.Modal.Standard.Formula α} (hq : q ∈ 𝒮 p) : LO.Modal.Standard.Formula.Kripke.Satisfies (LO.Modal.Standard.Kripke.GLFilteredModel p) ⟦X⟧ q ↔ q ∈ X.theory

theorem LO.Modal.Standard.Kripke.exists_finite_frame {α : Type u} {p : LO.Modal.Standard.Formula α} {𝔽 : LO.Modal.Standard.Kripke.FrameClass} : ¬𝔽ꟳ.alt ⊧ p ↔ ∃ F ∈ 𝔽.toFiniteFrameClass, ¬F.alt ⊧ p

instance LO.Modal.Standard.Kripke.GL_complete {α : Type u} [Inhabited α] [DecidableEq α] : LO.Complete 𝐆𝐋 LO.Modal.Standard.Kripke.TransitiveIrreflexiveFrameClassꟳ.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.instFiniteFramePropertyGLTransitiveIrreflexiveFrameClass {α : Type u} [Inhabited α] [DecidableEq α] : LO.Modal.Standard.Kripke.FiniteFrameProperty 𝐆𝐋 LO.Modal.Standard.Kripke.TransitiveIrreflexiveFrameClass

Equations

• LO.Modal.Standard.Kripke.instFiniteFramePropertyGLTransitiveIrreflexiveFrameClass = LO.Modal.Standard.Kripke.FiniteFrameProperty.mk