Completeness

@[reducible, inline]

noncomputable abbrev LO.Modal.Formula.subformulasGrz {α : Type u} [DecidableEq α] (φ : Formula α) : FormulaFinset α

Imported declaration from the Incompleteness formalization.

Equations

• φ.subformulasGrz = φ.subformulas ∪ Finset.image (fun (ψ : LO.Modal.Formula α) => □(ψ ==> □ψ)) (Finset.prebox φ.subformulas)

@[simp]

theorem LO.Modal.Formula.subformulasGrz.mem_self {φ : Formula ℕ} : φ ∈ φ.subformulasGrz

theorem LO.Modal.Formula.subformulasGrz.mem_boximpbox {φ ψ : Formula ℕ} (h : ψ ∈ Finset.prebox φ.subformulas) : □(ψ ==> □ψ) ∈ φ.subformulasGrz

theorem LO.Modal.Formula.subformulasGrz.mem_origin {φ ψ : Formula ℕ} (h : ψ ∈ φ.subformulas) : ψ ∈ φ.subformulasGrz

theorem LO.Modal.Formula.subformulasGrz.mem_imp {φ ψ χ : Formula ℕ} (h : ψ ==> χ ∈ φ.subformulasGrz) : ψ ∈ φ.subformulasGrz ∧ χ ∈ φ.subformulasGrz

theorem LO.Modal.Formula.subformulasGrz.mem_imp₁ {φ ψ χ : Formula ℕ} (h : ψ ==> χ ∈ φ.subformulasGrz) : ψ ∈ φ.subformulasGrz

theorem LO.Modal.Formula.subformulasGrz.mem_imp₂ {φ ψ χ : Formula ℕ} (h : ψ ==> χ ∈ φ.subformulasGrz) : χ ∈ φ.subformulasGrz

theorem LO.Modal.Formula.subformulasGrz.mem_left {φ ψ : Formula ℕ} (h : ψ ∈ φ.subformulas) : ψ ∈ φ.subformulasGrz

@[reducible, inline]

abbrev LO.Modal.Hilbert.Grz.Kripke.miniCanonicalFrame (φ : Formula ℕ) : Kripke.FiniteFrame

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Modal.Hilbert.Grz.Kripke.miniCanonicalFrame.reflexive {φ : Formula ℕ} : Std.Refl (miniCanonicalFrame φ).Rel

theorem LO.Modal.Hilbert.Grz.Kripke.miniCanonicalFrame.transitive {φ : Formula ℕ} : IsTrans (miniCanonicalFrame φ).World (miniCanonicalFrame φ).Rel

theorem LO.Modal.Hilbert.Grz.Kripke.miniCanonicalFrame.antisymm {φ : Formula ℕ} : Std.Antisymm (miniCanonicalFrame φ).Rel

@[reducible, inline]

abbrev LO.Modal.Hilbert.Grz.Kripke.miniCanonicalModel (φ : Formula ℕ) : Kripke.Model

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Modal.Hilbert.Grz.Kripke.truthlemma_lemma1 {φ ψ : Formula ℕ} {X : ComplementClosedConsistentFinset Hilbert.Grz φ.subformulasGrz} (hq : □ψ ∈ φ.subformulas) : (Finset.prebox ↑X).modalBox ∪ {□(ψ ==> □ψ), -ψ} ⊆ φ.subformulasGrz⁻

theorem LO.Modal.Hilbert.Grz.Kripke.truthlemma_lemma2 {φ ψ : Formula ℕ} {X : ComplementClosedConsistentFinset Hilbert.Grz φ.subformulasGrz} (hq₁ : □ψ ∈ φ.subformulas) (hq₂ : □ψ ∉ X) : FormulaFinset.Consistent Hilbert.Grz ((Finset.prebox ↑X).modalBox ∪ {□(ψ ==> □ψ), -ψ})

theorem LO.Modal.Hilbert.Grz.Kripke.truthlemma_lemma3 {φ : Formula ℕ} : Hilbert.Grz ⊢! φ ⋏ □(φ ==> □φ) ==> □φ

theorem LO.Modal.Hilbert.Grz.Kripke.truthlemma {φ ψ : Formula ℕ} {X : (miniCanonicalModel φ).World} (q_sub : ψ ∈ φ.subformulas) : Formula.Kripke.Satisfies (miniCanonicalModel φ) X ψ ↔ ψ ∈ X

instance LO.Modal.Hilbert.Grz.Kripke.complete : Complete Hilbert.Grz Kripke.ReflexiveTransitiveAntiSymmetricFiniteFrameClass