@[reducible, inline]

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

Equations

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

@[simp]

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

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

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

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

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

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

@[reducible, inline]

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

Equations

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

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

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

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

@[reducible, inline]

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

Equations

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

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

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

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

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

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

instance LO.Modal.Hilbert.Grz.Kripke.instFiniteFramePropertyNatReflexiveTransitiveAntiSymmetricFiniteFrameClass : Kripke.FiniteFrameProperty (Hilbert.Grz ℕ) Kripke.ReflexiveTransitiveAntiSymmetricFiniteFrameClass