@[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_boximpbox {φ ψ : Formula ℕ} (h : ψ ∈ Finset.prebox φ.subformulas) : □(ψ ➝ □ψ) ∈ φ.subformulasGrz

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

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Modal.Kripke.Grz.miniCanonicalFrame.instIsFinite

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

instance LO.Modal.Kripke.Grz.miniCanonicalFrame.instIsReflWorldRel {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Grz 𝓢] {φ : Formula ℕ} : IsRefl (miniCanonicalFrame 𝓢 φ).World (miniCanonicalFrame 𝓢 φ).Rel

instance LO.Modal.Kripke.Grz.miniCanonicalFrame.instIsTransWorldRel {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Grz 𝓢] {φ : Formula ℕ} : IsTrans (miniCanonicalFrame 𝓢 φ).World (miniCanonicalFrame 𝓢 φ).Rel

instance LO.Modal.Kripke.Grz.miniCanonicalFrame.instIsAntisymmWorldRel {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Grz 𝓢] {φ : Formula ℕ} : IsAntisymm (miniCanonicalFrame 𝓢 φ).World (miniCanonicalFrame 𝓢 φ).Rel

instance LO.Modal.Kripke.Grz.miniCanonicalFrame.instIsPartialOrderWorldRel {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Grz 𝓢] {φ : Formula ℕ} : IsPartialOrder (miniCanonicalFrame 𝓢 φ).World (miniCanonicalFrame 𝓢 φ).Rel

@[reducible, inline]

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

Equations

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

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

theorem LO.Modal.Kripke.Grz.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.Kripke.Grz.truthlemma_lemma3 {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Grz 𝓢] {φ : Formula ℕ} : 𝓢 ⊢! φ ⋏ □(φ ➝ □φ) ➝ □φ

theorem LO.Modal.Kripke.Grz.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.Kripke.Grz.complete_of_mem_miniCanonicalFrame {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Grz 𝓢] (C : FrameClass) (hC : ∀ {φ : Formula ℕ}, miniCanonicalFrame 𝓢 φ ∈ C) : Complete 𝓢 C

instance LO.Modal.Hilbert.Grz.Kripke.complete : Complete Hilbert.Grz Kripke.FrameClass.finite_partial_order

theorem LO.Modal.Logic.Grz.Kripke.finite_partial_order : Logic.Grz = Kripke.FrameClass.finite_partial_order.logic

theorem LO.Modal.Logic.Grz.proper_extension_of_S4 : Logic.S4 ⊂ Logic.Grz

theorem LO.Modal.Logic.Grz.proper_extension_of_S4M : Logic.S4M ⊂ Logic.Grz