@[reducible, inline]

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

Equations

• φ.subformulaeGrz = φ.subformulae ∪ Finset.image (fun (ψ : LO.Modal.Formula α) => □(ψ ➝ □ψ)) (Finset.prebox φ.subformulae)

@[simp]

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

theorem LO.Modal.Formula.subformulaeGrz.mem_boximpbox {φ ψ : LO.Modal.Formula ℕ} (h : ψ ∈ Finset.prebox φ.subformulae) : □(ψ ➝ □ψ) ∈ φ.subformulaeGrz

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

theorem LO.Modal.Formula.subformulaeGrz.mem_imp {φ ψ χ : LO.Modal.Formula ℕ} (h : ψ ➝ χ ∈ φ.subformulaeGrz) : ψ ∈ φ.subformulaeGrz ∧ χ ∈ φ.subformulaeGrz

theorem LO.Modal.Formula.subformulaeGrz.mem_imp₁ {φ ψ χ : LO.Modal.Formula ℕ} (h : ψ ➝ χ ∈ φ.subformulaeGrz) : ψ ∈ φ.subformulaeGrz

theorem LO.Modal.Formula.subformulaeGrz.mem_imp₂ {φ ψ χ : LO.Modal.Formula ℕ} (h : ψ ➝ χ ∈ φ.subformulaeGrz) : χ ∈ φ.subformulaeGrz

@[reducible, inline]

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

Equations

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

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

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

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

@[reducible, inline]

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

Equations

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

theorem LO.Modal.Hilbert.Grz.Kripke.truthlemma.lemma1 {φ ψ : LO.Modal.Formula ℕ} {X : LO.Modal.CCF (LO.Modal.Hilbert.Grz ℕ) φ.subformulaeGrz} (hq : □ψ ∈ φ.subformulae) : (Finset.prebox X.formulae).box ∪ {□(ψ ➝ □ψ), -ψ} ⊆ φ.subformulaeGrz⁻

theorem LO.Modal.Hilbert.Grz.Kripke.truthlemma.lemma2 {φ ψ : LO.Modal.Formula ℕ} {X : LO.Modal.CCF (LO.Modal.Hilbert.Grz ℕ) φ.subformulaeGrz} (hq₁ : □ψ ∈ φ.subformulae) (hq₂ : □ψ ∉ X.formulae) : LO.Modal.Formulae.Consistent (LO.Modal.Hilbert.Grz ℕ) ((Finset.prebox X.formulae).box ∪ {□(ψ ➝ □ψ), -ψ})

theorem LO.Modal.Hilbert.Grz.Kripke.truthlemma.lemma3 {φ : LO.Modal.Formula ℕ} : LO.Modal.Hilbert.KT ℕ ⊢! φ ⋏ □(φ ➝ □φ) ➝ □φ

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

instance LO.Modal.Hilbert.Grz.Kripke.complete : LO.Complete (LO.Modal.Hilbert.Grz ℕ) LO.Modal.Kripke.ReflexiveTransitiveAntisymmetricFiniteFrameClass

Equations

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

instance LO.Modal.Hilbert.Grz.Kripke.instFiniteFramePropertyNatReflexiveTransitiveAntisymmetricFiniteFrameClass : LO.Modal.Hilbert.Kripke.FiniteFrameProperty (LO.Modal.Hilbert.Grz ℕ) LO.Modal.Kripke.ReflexiveTransitiveAntisymmetricFiniteFrameClass

Equations

• LO.Modal.Hilbert.Grz.Kripke.instFiniteFramePropertyNatReflexiveTransitiveAntisymmetricFiniteFrameClass = ⋯