@[reducible, inline]

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

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_of_mem_subformula {φ ψ : Formula ℕ} (h : ψ ∈ φ.subformulas) : ψ ∈ φ.subformulasGrz

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

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.Grz.Kripke.miniCanonicalFrame {S : Type u_1} [Entailment (Formula ℕ) S] (𝓢 : S) [Entailment.Grz 𝓢] [Entailment.Consistent 𝓢] (φ : Formula ℕ) : Kripke.Frame

Equations

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

instance LO.Modal.Hilbert.Grz.Kripke.instIsReflexiveMiniCanonicalFrame {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Grz 𝓢] {φ : Formula ℕ} : (miniCanonicalFrame 𝓢 φ).IsReflexive

instance LO.Modal.Hilbert.Grz.Kripke.instIsAntisymmetricMiniCanonicalFrame {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Grz 𝓢] {φ : Formula ℕ} : (miniCanonicalFrame 𝓢 φ).IsAntisymmetric

instance LO.Modal.Hilbert.Grz.Kripke.instIsTransitiveMiniCanonicalFrame {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Grz 𝓢] {φ : Formula ℕ} : (miniCanonicalFrame 𝓢 φ).IsTransitive

instance LO.Modal.Hilbert.Grz.Kripke.instIsFiniteGrzMiniCanonicalFrame {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Grz 𝓢] {φ : Formula ℕ} : (miniCanonicalFrame 𝓢 φ).IsFiniteGrz

@[reducible, inline]

abbrev LO.Modal.Hilbert.Grz.Kripke.miniCanonicalModel {S : Type u_1} [Entailment (Formula ℕ) S] (𝓢 : S) [Entailment.Grz 𝓢] [Entailment.Consistent 𝓢] (φ : Formula ℕ) : Kripke.Model

Equations

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

theorem LO.Modal.Hilbert.Grz.Kripke.truthlemma_lemma1 {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} {φ ψ : Formula ℕ} {X : ComplementClosedConsistentFinset 𝓢 φ.subformulasGrz} (hq : □ψ ∈ φ.subformulas) : (Finset.prebox ↑X).box ∪ {□(ψ ➝ □ψ), -ψ} ⊆ φ.subformulasGrz⁻

theorem LO.Modal.Hilbert.Grz.Kripke.truthlemma_lemma2 {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Grz 𝓢] {φ ψ : Formula ℕ} {X : ComplementClosedConsistentFinset 𝓢 φ.subformulasGrz} (hψ₁ : □ψ ∈ φ.subformulas) (hψ₂ : □ψ ∉ X) : FormulaFinset.Consistent 𝓢 ((Finset.prebox ↑X).box ∪ {□(ψ ➝ □ψ), -ψ})

theorem LO.Modal.Hilbert.Grz.Kripke.truthlemma_lemma3 {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Grz 𝓢] {φ : Formula ℕ} : 𝓢 ⊢! φ ⋏ □(φ ➝ □φ) ➝ □φ

theorem LO.Modal.Hilbert.Grz.Kripke.truthlemma {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Grz 𝓢] {φ ψ : Formula ℕ} {X : (miniCanonicalModel 𝓢 φ).World} (q_sub : ψ ∈ φ.subformulas) : Formula.Kripke.Satisfies (miniCanonicalModel 𝓢 φ) X ψ ↔ ψ ∈ X

theorem LO.Modal.Hilbert.Grz.Kripke.complete_of_mem_miniCanonicalFrame {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Grz 𝓢] (C : Kripke.FrameClass) (hC : ∀ {φ : Formula ℕ}, miniCanonicalFrame 𝓢 φ ∈ C) : Complete 𝓢 C

instance LO.Modal.Hilbert.Grz.Kripke.instCompleteNormalNatFormulaFrameClassFinite_Grz : Complete Hilbert.Grz Kripke.FrameClass.finite_Grz

instance LO.Modal.Hilbert.Grz.Kripke.instStrictlyWeakerThanFormulaNatNormalS4McK : Hilbert.S4McK ⪱ Hilbert.Grz

instance LO.Modal.Hilbert.Grz.Kripke.instStrictlyWeakerThanFormulaNatNormalS4 : Hilbert.S4 ⪱ Hilbert.Grz

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicS4McKGrz : Modal.S4McK ⪱ Modal.Grz