@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.CanonicalFrame {α : Type u} (Λ : LO.Modal.Standard.DeductionParameter α) [Inhabited (Λ)-MCT] : LO.Modal.Standard.Kripke.Frame

Equations

• LO.Modal.Standard.Kripke.CanonicalFrame Λ = LO.Modal.Standard.Kripke.Frame.mk (Λ)-MCT fun (Ω₁ Ω₂ : (Λ)-MCT) => □''⁻¹Ω₁.theory ⊆ Ω₂.theory

@[simp]

theorem LO.Modal.Standard.Kripke.CanonicalFrame.rel_def_box {α : Type u} {Λ : LO.Modal.Standard.DeductionParameter α} [Inhabited (Λ)-MCT] {Ω₁ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World} {Ω₂ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World} : LO.Modal.Standard.Kripke.Frame.Rel' Ω₁ Ω₂ ↔ ∀ {p : LO.Modal.Standard.Formula α}, □p ∈ Ω₁.theory → p ∈ Ω₂.theory

theorem LO.Modal.Standard.Kripke.CanonicalFrame.multirel_def_multibox {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Λ.IsNormal] [Inhabited (Λ)-MCT] {Ω₁ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World} {Ω₂ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World} {n : ℕ} : LO.Modal.Standard.Kripke.Frame.RelItr' n Ω₁ Ω₂ ↔ ∀ {p : LO.Modal.Standard.Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory

theorem LO.Modal.Standard.Kripke.CanonicalFrame.multirel_def_multibox' {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Λ.IsNormal] [Inhabited (Λ)-MCT] {Ω₁ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World} {Ω₂ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World} {n : ℕ} : LO.Modal.Standard.Kripke.Frame.RelItr' n Ω₁ Ω₂ ↔ ∀ {p : LO.Modal.Standard.Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory

theorem LO.Modal.Standard.Kripke.CanonicalFrame.multirel_def_multidia {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Λ.IsNormal] [Inhabited (Λ)-MCT] {Ω₁ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World} {Ω₂ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World} {n : ℕ} : LO.Modal.Standard.Kripke.Frame.RelItr' n Ω₁ Ω₂ ↔ ∀ {p : LO.Modal.Standard.Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory

theorem LO.Modal.Standard.Kripke.CanonicalFrame.rel_def_dia {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Λ.IsNormal] [Inhabited (Λ)-MCT] {Ω₁ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World} {Ω₂ : (LO.Modal.Standard.Kripke.CanonicalFrame Λ).World} : LO.Modal.Standard.Kripke.Frame.Rel' Ω₁ Ω₂ ↔ ∀ {p : LO.Modal.Standard.Formula α}, p ∈ Ω₂.theory → ◇p ∈ Ω₁.theory

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.CanonicalModel {α : Type u} (Λ : LO.Modal.Standard.DeductionParameter α) [Inhabited (Λ)-MCT] : LO.Modal.Standard.Kripke.Model α

Equations

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

@[reducible]

instance LO.Modal.Standard.Kripke.CanonicalModel.instSemanticsFormulaWorld {α : Type u} {Λ : LO.Modal.Standard.DeductionParameter α} [Inhabited (Λ)-MCT] : LO.Semantics (LO.Modal.Standard.Formula α) (LO.Modal.Standard.Kripke.CanonicalModel Λ).World

Equations

• LO.Modal.Standard.Kripke.CanonicalModel.instSemanticsFormulaWorld = LO.Modal.Standard.Formula.Kripke.Satisfies.semantics

theorem LO.Modal.Standard.Kripke.truthlemma {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Λ.IsNormal] [Inhabited (Λ)-MCT] {p : LO.Modal.Standard.Formula α} {Ω : (LO.Modal.Standard.Kripke.CanonicalModel Λ).World} : Ω ⊧ p ↔ p ∈ Ω.theory

theorem LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Λ.IsNormal] [Inhabited (Λ)-MCT] {p : LO.Modal.Standard.Formula α} : LO.Modal.Standard.Kripke.CanonicalModel Λ ⊧ p ↔ Λ ⊢! p

theorem LO.Modal.Standard.Kripke.realize_axiomset_of_self_canonicalModel {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Λ.IsNormal] [Inhabited (Λ)-MCT] : LO.Modal.Standard.Kripke.CanonicalModel Λ ⊧* Ax(Λ)

theorem LO.Modal.Standard.Kripke.realize_theory_of_self_canonicalModel {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Λ.IsNormal] [Inhabited (Λ)-MCT] : LO.Modal.Standard.Kripke.CanonicalModel Λ ⊧* LO.System.theory Λ

theorem LO.Modal.Standard.Kripke.complete_of_mem_canonicalFrame {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Λ.IsNormal] {p : LO.Modal.Standard.Formula α} [Inhabited (Λ)-MCT] {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} (hFC : LO.Modal.Standard.Kripke.CanonicalFrame Λ ∈ 𝔽) : 𝔽 ⊧ p → Λ ⊢! p

theorem LO.Modal.Standard.Kripke.instComplete_of_mem_canonicalFrame {α : Type u} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Λ.IsNormal] [Inhabited (Λ)-MCT] {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} (hFC : LO.Modal.Standard.Kripke.CanonicalFrame Λ ∈ 𝔽) : LO.Complete Λ 𝔽

instance LO.Modal.Standard.Kripke.K_complete {α : Type u} [DecidableEq α] : LO.Complete 𝐊 LO.Modal.Standard.Kripke.AllFrameClass.alt

Equations

• ⋯ = ⋯