def LO.Modal.Kripke.complexityLimitedFrame (F : LO.Modal.Kripke.Frame) (r : F.World) (φ : LO.Modal.Formula ℕ) : LO.Modal.Kripke.Frame

Equations

• LO.Modal.Kripke.complexityLimitedFrame F r φ = LO.Modal.Kripke.Frame.mk ↑{x : F.World | ∃ n ≤ φ.complexity, r ≺^[n] x} fun (x y : ↑{x : F.World | ∃ n ≤ φ.complexity, r ≺^[n] x}) => ↑x ≺ ↑y

def LO.Modal.Kripke.complexityLimitedModel (M : LO.Modal.Kripke.Model) (w : M.World) (φ : LO.Modal.Formula ℕ) : LO.Modal.Kripke.Model

Equations

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

theorem LO.Modal.Kripke.iff_satisfy_complexityLimitedModel_aux {M : LO.Modal.Kripke.Model} {r x : M.World} {φ ψ : LO.Modal.Formula ℕ} (hq : ψ ∈ φ.subformulae) (hx : ∃ n ≤ φ.complexity - ψ.complexity, r ≺^[n] x) : x ⊧ ψ ↔ LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.complexityLimitedModel M r φ) ⟨x, ⋯⟩ ψ

theorem LO.Modal.Kripke.iff_satisfy_complexityLimitedModel {M : LO.Modal.Kripke.Model} {r : M.World} {φ : LO.Modal.Formula ℕ} : r ⊧ φ ↔ LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.complexityLimitedModel M r φ) ⟨r, ⋯⟩ φ

theorem LO.Modal.Kripke.complexityLimitedModel_subformula_closedAux {M : LO.Modal.Kripke.Model} {r : M.World} {φ ψ₁ ψ₂ : LO.Modal.Formula ℕ} (hq₁ : φ ∈ ψ₁.subformulae) (hq₂ : φ ∈ ψ₂.subformulae) : LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.complexityLimitedModel M r ψ₁) ⟨r, ⋯⟩ φ → LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.complexityLimitedModel M r ψ₂) ⟨r, ⋯⟩ φ

theorem LO.Modal.Kripke.complexityLimitedModel_subformula_closed {M : LO.Modal.Kripke.Model} {r : M.World} {φ ψ : LO.Modal.Formula ℕ} (hq : φ ∈ ψ.subformulae) : LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.complexityLimitedModel M r φ) ⟨r, ⋯⟩ φ ↔ LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.complexityLimitedModel M r ψ) ⟨r, ⋯⟩ φ