def LO.Modal.Kripke.complexityLimitedFrame (F : Frame) (r : F.World) (φ : Formula ℕ) : 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 : Model) (w : M.World) (φ : Formula ℕ) : Model

Equations

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

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

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

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

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