@[reducible, inline]

abbrev LO.Modal.Kripke.CanonicalFrame {α : Type u} (Λ : LO.Modal.Hilbert α) [Nonempty (LO.Modal.MCT Λ)] : LO.Kripke.Frame

Equations

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

@[simp]

theorem LO.Modal.Kripke.CanonicalFrame.rel_def_box {α : Type u} {Λ : LO.Modal.Hilbert α} [Nonempty (LO.Modal.MCT Λ)] {Ω₁ : (LO.Modal.Kripke.CanonicalFrame Λ).World} {Ω₂ : (LO.Modal.Kripke.CanonicalFrame Λ).World} : Ω₁ ≺ Ω₂ ↔ ∀ {p : LO.Modal.Formula α}, □p ∈ Ω₁.theory → p ∈ Ω₂.theory

theorem LO.Modal.Kripke.CanonicalFrame.multirel_def_multibox {α : Type u} [DecidableEq α] {Λ : LO.Modal.Hilbert α} [Λ.IsNormal] [Nonempty (LO.Modal.MCT Λ)] {Ω₁ : (LO.Modal.Kripke.CanonicalFrame Λ).World} {Ω₂ : (LO.Modal.Kripke.CanonicalFrame Λ).World} {n : ℕ} : Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : LO.Modal.Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory

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

theorem LO.Modal.Kripke.CanonicalFrame.multirel_def_multidia {α : Type u} [DecidableEq α] {Λ : LO.Modal.Hilbert α} [Λ.IsNormal] [Nonempty (LO.Modal.MCT Λ)] {Ω₁ : (LO.Modal.Kripke.CanonicalFrame Λ).World} {Ω₂ : (LO.Modal.Kripke.CanonicalFrame Λ).World} {n : ℕ} : Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : LO.Modal.Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory

theorem LO.Modal.Kripke.CanonicalFrame.rel_def_dia {α : Type u} [DecidableEq α] {Λ : LO.Modal.Hilbert α} [Λ.IsNormal] [Nonempty (LO.Modal.MCT Λ)] {Ω₁ : (LO.Modal.Kripke.CanonicalFrame Λ).World} {Ω₂ : (LO.Modal.Kripke.CanonicalFrame Λ).World} : Ω₁ ≺ Ω₂ ↔ ∀ {p : LO.Modal.Formula α}, p ∈ Ω₂.theory → ◇p ∈ Ω₁.theory

@[reducible, inline]

abbrev LO.Modal.Kripke.CanonicalModel {α : Type u} (Λ : LO.Modal.Hilbert α) [Nonempty (LO.Modal.MCT Λ)] : LO.Kripke.Model α

Equations

• LO.Modal.Kripke.CanonicalModel Λ = { Frame := LO.Modal.Kripke.CanonicalFrame Λ, Valuation := fun (Ω : (LO.Modal.Kripke.CanonicalFrame Λ).World) (a : α) => LO.Modal.Formula.atom a ∈ Ω.theory }

@[reducible]

instance LO.Modal.Kripke.CanonicalModel.instSemanticsFormulaWorld {α : Type u} {Λ : LO.Modal.Hilbert α} [Nonempty (LO.Modal.MCT Λ)] : LO.Semantics (LO.Modal.Formula α) (LO.Modal.Kripke.CanonicalModel Λ).World

Equations

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

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

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

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

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

theorem LO.Modal.Kripke.complete_of_mem_canonicalFrame {α : Type u} [DecidableEq α] {Λ : LO.Modal.Hilbert α} [Λ.IsNormal] {p : LO.Modal.Formula α} [Nonempty (LO.Modal.MCT Λ)] {𝔽 : LO.Kripke.FrameClass} (hFC : LO.Modal.Kripke.CanonicalFrame Λ ∈ 𝔽) : 𝔽#α ⊧ p → Λ ⊢! p

instance LO.Modal.Kripke.instComplete_of_mem_canonicalFrame {α : Type u} [DecidableEq α] {Λ : LO.Modal.Hilbert α} [Λ.IsNormal] [Nonempty (LO.Modal.MCT Λ)] (𝔽 : LO.Kripke.FrameClass) (hFC : LO.Modal.Kripke.CanonicalFrame Λ ∈ 𝔽) : LO.Complete Λ 𝔽#α

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯