@[reducible, inline]

abbrev LO.Modal.Hilbert.Kripke.canonicalFrame (H : Hilbert ℕ) [H.IsNormal] [H.Consistent] : 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 : Hilbert ℕ} [H.IsNormal] [H.Consistent] {Ω₁ Ω₂ : (canonicalFrame H).World} : Ω₁ ≺ Ω₂ ↔ ∀ {φ : Formula ℕ}, □φ ∈ Ω₁.theory → φ ∈ Ω₂.theory

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

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

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

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

@[reducible, inline]

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

Equations

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

@[reducible]

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

Equations

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

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

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

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

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

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

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

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