Completeness

@[reducible, inline]

abbrev LO.Modal.Kripke.canonicalFrame {S : Type u_1} [Entailment (Formula ℕ) S] (𝓢 : S) [Entailment.Consistent 𝓢] [Entailment.K 𝓢] : Frame

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.canonicalFrame 𝓢 = { World := LO.Modal.MaximalConsistentSet 𝓢, Rel := fun (X Y : LO.Modal.MaximalConsistentSet 𝓢) => □''⁻¹↑X ⊆ ↑Y, world_nonempty := ⋯ }

@[simp]

theorem LO.Modal.Kripke.canonicalFrame.rel_def_box {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢] {Ω₁ Ω₂ : (canonicalFrame 𝓢).World} : Ω₁ ≺ Ω₂ ↔ ∀ {φ : Formula ℕ}, □φ ∈ Ω₁ → φ ∈ Ω₂

theorem LO.Modal.Kripke.canonicalFrame.multirel_def_multibox {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢] {Ω₁ Ω₂ : (canonicalFrame 𝓢).World} {n : ℕ} : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ : Formula ℕ}, □^[n]φ ∈ ↑Ω₁ → φ ∈ ↑Ω₂

theorem LO.Modal.Kripke.canonicalFrame.multirel_def_multibox' {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢] {Ω₁ Ω₂ : (canonicalFrame 𝓢).World} {n : ℕ} : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ : Formula ℕ}, φ ∈ □''⁻¹^[n]↑Ω₁ → φ ∈ ↑Ω₂

theorem LO.Modal.Kripke.canonicalFrame.multirel_def_multidia {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢] {Ω₁ Ω₂ : (canonicalFrame 𝓢).World} {n : ℕ} : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ : Formula ℕ}, φ ∈ ↑Ω₂ → ◇^[n]φ ∈ ↑Ω₁

theorem LO.Modal.Kripke.canonicalFrame.rel_def_dia {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢] {Ω₁ Ω₂ : (canonicalFrame 𝓢).World} : Ω₁ ≺ Ω₂ ↔ ∀ {φ : Formula ℕ}, φ ∈ ↑Ω₂ → ◇φ ∈ ↑Ω₁

@[reducible, inline]

abbrev LO.Modal.Kripke.canonicalModel {S : Type u_1} [Entailment (Formula ℕ) S] (𝓢 : S) [Entailment.Consistent 𝓢] [Entailment.K 𝓢] : Model

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.canonicalModel 𝓢 = { toFrame := LO.Modal.Kripke.canonicalFrame 𝓢, Val := fun (Ω : (LO.Modal.Kripke.canonicalFrame 𝓢).World) (a : ℕ) => LO.Modal.Formula.atom a ∈ ↑Ω }

@[reducible]

instance LO.Modal.Kripke.instSemanticsFormulaNatWorldCanonicalModel {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢] : Semantics (Formula ℕ) (canonicalModel 𝓢).World

Equations

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

theorem LO.Modal.Kripke.truthlemma {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢] {φ : Formula ℕ} {Ω : (canonicalModel 𝓢).World} : Ω ⊧ φ ↔ φ ∈ ↑Ω

theorem LO.Modal.Kripke.iff_valid_on_canonicalModel_deducible {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢] {φ : Formula ℕ} : canonicalModel 𝓢 ⊧ φ ↔ 𝓢 ⊢! φ

class LO.Modal.Kripke.Canonical {S : Type u_1} [Entailment (Formula ℕ) S] (𝓢 : S) [Entailment.Consistent 𝓢] [Entailment.K 𝓢] (C : FrameClass) : Prop

Imported declaration from the Incompleteness formalization.

• canonical : canonicalFrame 𝓢 ∈ C

instance LO.Modal.Kripke.instCompleteFormulaNatFrameClassOfCanonical {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢] {C : FrameClass} [Canonical 𝓢 C] : Complete 𝓢 C