KHIncompleteness

theorem LO.Modal.Kripke.valid_atomic_H_of_valid_atomic_L {F : Frame} {a : ℕ} : F ⊧ Axioms.L (Formula.atom a) → F ⊧ Axioms.H (Formula.atom a)

theorem LO.Modal.Kripke.valid_atomic_L_of_valid_atomic_H {F : Frame} {a : ℕ} : F ⊧ Axioms.H (Formula.atom a) → F ⊧ Axioms.L (Formula.atom a)

theorem LO.Modal.Kripke.valid_atomic_L_iff_valid_atomic_H {F : Frame} : F ⊧ Axioms.L (Formula.atom 0) ↔ F ⊧ Axioms.H (Formula.atom 0)

theorem LO.Modal.Kripke.valid_atomic_4_of_valid_atomic_L {F : Frame} : F ⊧ Axioms.L (Formula.atom 0) → F ⊧ Axioms.Four (Formula.atom 0)

theorem LO.Modal.Kripke.valid_atomic_Four_of_valid_atomic_H {F : Frame} : F ⊧ Axioms.H (Formula.atom 0) → F ⊧ Axioms.Four (Formula.atom 0)

@[reducible, inline]

abbrev LO.Modal.Kripke.cresswellFrame : Frame

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, match_pattern, inline]

abbrev LO.Modal.Kripke.cresswellFrame.sharp (n : ℕ) : cresswellFrame.World

Imported declaration from the Incompleteness formalization.

Equations

• n♯ = (n, 0)

def LO.Modal.Kripke.cresswellFrame.«term_♯» : Lean.TrailingParserDescr

Imported notation from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.cresswellFrame.«term_♯» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.cresswellFrame.«term_♯» 1024 1024 (Lean.ParserDescr.symbol "♯")

@[reducible, match_pattern, inline]

abbrev LO.Modal.Kripke.cresswellFrame.flat (n : ℕ) : cresswellFrame.World

Imported declaration from the Incompleteness formalization.

Equations

• n♭ = (n, 1)

def LO.Modal.Kripke.cresswellFrame.«term_♭» : Lean.TrailingParserDescr

Imported notation from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.cresswellFrame.«term_♭» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.cresswellFrame.«term_♭» 1024 1024 (Lean.ParserDescr.symbol "♭")

theorem LO.Modal.Kripke.cresswellFrame.trichonomy {x y : cresswellFrame.World} : x ≺ y ∨ x = y ∨ y ≺ x

Imported declaration from the Incompleteness formalization.

theorem LO.Modal.Kripke.cresswellFrame.sharp_to_flat {n m : ℕ} : n♯ ≺ m♭

@[simp]

theorem LO.Modal.Kripke.cresswellFrame.not_flat_to_sharp {n m : ℕ} : ¬n♭ ≺ m♯

theorem LO.Modal.Kripke.cresswellFrame.sharp_to_sharp {n m : ℕ} : n♯ ≺ m♯ ↔ n ≤ m + 1

theorem LO.Modal.Kripke.cresswellFrame.flat_to_flat {n m : ℕ} : n♭ ≺ m♭ ↔ n > m

theorem LO.Modal.Kripke.cresswellFrame.exists_flat_of_from_flat {n : ℕ} {x : cresswellFrame.World} (h : n♭ ≺ x) : ∃ (m : ℕ), x = (m, 1) ∧ n > m

@[reducible, inline]

abbrev LO.Modal.Kripke.cresswellModel : Model

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.cresswellModel = { toFrame := LO.Modal.Kripke.cresswellFrame, Val := fun (w : LO.Modal.Kripke.cresswellFrame.World) (x : ℕ) => w ≠ 0♯ }

theorem LO.Modal.Kripke.not_valid_axiomFour_in_cresswellModel : ¬Formula.Kripke.Satisfies cresswellModel 2♯ (Axioms.Four (Formula.atom 0))

@[reducible, inline]

abbrev LO.Modal.Kripke.cresswellModel.truthset (φ : Formula ℕ) : Set cresswellModel.World

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.cresswellModel.truthset φ = {x : LO.Modal.Kripke.cresswellModel.World | LO.Modal.Formula.Kripke.Satisfies LO.Modal.Kripke.cresswellModel x φ}

theorem LO.Modal.Kripke.cresswellModel.truthset.infinite_of_all_flat {φ : Formula ℕ} (h : ∀ (n : ℕ), n♭ ∈ truthset φ) : (truthset φ).Infinite

theorem LO.Modal.Kripke.cresswellModel.truthset.exists_max_sharp {φ : Formula ℕ} (h₁ : ∀ (n : ℕ), n♭ ∈ truthset φ) (h₂ : (truthset φ)ᶜ.Finite) (h₃ : (truthset φ)ᶜ.Nonempty) : ∃ (n : ℕ), n♯ ∉ truthset φ ∧ ∀ m > n, m♯ ∈ truthset φ

theorem LO.Modal.Kripke.cresswellModel.truthset.exists_min_flat {φ : Formula ℕ} (h₁ : ∃ (n : ℕ), n♭ ∉ truthset φ) : ∃ (n : ℕ), n♭ ∉ truthset φ ∧ ∀ m < n, m♭ ∈ truthset φ

theorem LO.Modal.Kripke.cresswellModel.truthset.either_finite_cofinite {φ : Formula ℕ} : (truthset φ).Finite ∨ (truthset φ)ᶜ.Finite

theorem LO.Modal.Kripke.valid_axiomH_in_cresswellModel {φ : Formula ℕ} : cresswellModel ⊧ □(□φ <=> φ) ==> □φ

theorem LO.Modal.Kripke.provable_KH_of_valid_cresswellModel {φ : Formula ℕ} : Hilbert.KH ⊢! φ → cresswellModel ⊧ φ

theorem LO.Modal.Kripke.KH_unprov_axiomFour : Hilbert.KH ⊬ Axioms.Four (Formula.atom 0)

theorem LO.Modal.Kripke.KH_KripkeIncomplete : ¬∃ (C : FrameClass), ∀ (φ : Formula ℕ), Hilbert.KH ⊢! φ ↔ C ⊧ φ