@[reducible, inline]

abbrev LO.Modal.Hilbert.Kripke.canonicalFrame (H : LO.Modal.Hilbert ℕ) [H.IsNormal] [H.Consistent] : LO.Modal.Kripke.Frame

Equations

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

@[simp]

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.rel_def_box {H : LO.Modal.Hilbert ℕ} [H.IsNormal] [H.Consistent] {Ω₁ Ω₂ : (LO.Modal.Hilbert.Kripke.canonicalFrame H).World} : Ω₁ ≺ Ω₂ ↔ ∀ {φ : LO.Modal.Formula ℕ}, □φ ∈ Ω₁.theory → φ ∈ Ω₂.theory

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.multirel_def_multibox {H : LO.Modal.Hilbert ℕ} [H.IsNormal] [H.Consistent] {Ω₁ Ω₂ : (LO.Modal.Hilbert.Kripke.canonicalFrame H).World} {n : ℕ} : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ : LO.Modal.Formula ℕ}, □^[n]φ ∈ Ω₁.theory → φ ∈ Ω₂.theory

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.multirel_def_multibox' {H : LO.Modal.Hilbert ℕ} [H.IsNormal] [H.Consistent] {Ω₁ Ω₂ : (LO.Modal.Hilbert.Kripke.canonicalFrame H).World} {n : ℕ} : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ : LO.Modal.Formula ℕ}, φ ∈ □''⁻¹^[n]Ω₁.theory → φ ∈ Ω₂.theory

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.multirel_def_multidia {H : LO.Modal.Hilbert ℕ} [H.IsNormal] [H.Consistent] {Ω₁ Ω₂ : (LO.Modal.Hilbert.Kripke.canonicalFrame H).World} {n : ℕ} : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ : LO.Modal.Formula ℕ}, φ ∈ Ω₂.theory → ◇^[n]φ ∈ Ω₁.theory

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.rel_def_dia {H : LO.Modal.Hilbert ℕ} [H.IsNormal] [H.Consistent] {Ω₁ Ω₂ : (LO.Modal.Hilbert.Kripke.canonicalFrame H).World} : Ω₁ ≺ Ω₂ ↔ ∀ {φ : LO.Modal.Formula ℕ}, φ ∈ Ω₂.theory → ◇φ ∈ Ω₁.theory

@[reducible, inline]

abbrev LO.Modal.Hilbert.Kripke.canonicalModel (H : LO.Modal.Hilbert ℕ) [H.IsNormal] [H.Consistent] : LO.Modal.Kripke.Model

Equations

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

@[reducible]

instance LO.Modal.Hilbert.Kripke.instSemanticsFormulaNatWorldCanonicalModel {H : LO.Modal.Hilbert ℕ} [H.IsNormal] [H.Consistent] : LO.Semantics (LO.Modal.Formula ℕ) (LO.Modal.Hilbert.Kripke.canonicalModel H).World

Equations

• LO.Modal.Hilbert.Kripke.instSemanticsFormulaNatWorldCanonicalModel = LO.Modal.Formula.Kripke.Satisfies.semantics

theorem LO.Modal.Hilbert.Kripke.truthlemma {H : LO.Modal.Hilbert ℕ} [H.IsNormal] [H.Consistent] {φ : LO.Modal.Formula ℕ} {Ω : (LO.Modal.Hilbert.Kripke.canonicalModel H).World} : Ω ⊧ φ ↔ φ ∈ Ω.theory

theorem LO.Modal.Hilbert.Kripke.iff_valid_on_canonicalModel_deducible {H : LO.Modal.Hilbert ℕ} [H.IsNormal] [H.Consistent] {φ : LO.Modal.Formula ℕ} : LO.Modal.Hilbert.Kripke.canonicalModel H ⊧ φ ↔ H ⊢! φ

theorem LO.Modal.Hilbert.Kripke.realize_axiomset_of_self_canonicalModel {H : LO.Modal.Hilbert ℕ} [H.IsNormal] [H.Consistent] : LO.Modal.Hilbert.Kripke.canonicalModel H ⊧* H.axioms

theorem LO.Modal.Hilbert.Kripke.realize_theory_of_self_canonicalModel {H : LO.Modal.Hilbert ℕ} [H.IsNormal] [H.Consistent] : LO.Modal.Hilbert.Kripke.canonicalModel H ⊧* LO.System.theory H

theorem LO.Modal.Hilbert.Kripke.complete_of_canonical {H : LO.Modal.Hilbert ℕ} [H.IsNormal] [H.Consistent] {φ : LO.Modal.Formula ℕ} {C : LO.Modal.Kripke.FrameClass} (hFC : LO.Modal.Hilbert.Kripke.canonicalFrame H ∈ C) : C ⊧ φ → H ⊢! φ

theorem LO.Modal.Hilbert.Kripke.instCompleteOfCanonical {H : LO.Modal.Hilbert ℕ} [H.IsNormal] [H.Consistent] {C : LO.Modal.Kripke.FrameClass} (hC : LO.Modal.Hilbert.Kripke.canonicalFrame H ∈ C) : LO.Complete H C

instance LO.Modal.Hilbert.K.Kripke.complete : LO.Complete (LO.Modal.Hilbert.K ℕ) LO.Modal.Kripke.AllFrameClass

Equations

• LO.Modal.Hilbert.K.Kripke.complete = ⋯