Filteration

def LO.Modal.Kripke.filterEquiv (M : Model) (T : FormulaSet ℕ) (x y : M.World) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.filterEquiv M T x y = ∀ (φ : LO.Modal.Formula ℕ), autoParam (φ ∈ T) LO.Modal.Kripke.filterEquiv._auto_1 → (x ⊧ φ ↔ y ⊧ φ)

theorem LO.Modal.Kripke.filterEquiv.equivalence (M : Model) (T : FormulaSet ℕ) : Equivalence (filterEquiv M T)

def LO.Modal.Kripke.FilterEqvSetoid (M : Model) (T : FormulaSet ℕ) : Setoid M.World

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.FilterEqvSetoid M T = { r := LO.Modal.Kripke.filterEquiv M T, iseqv := ⋯ }

@[reducible, inline]

abbrev LO.Modal.Kripke.FilterEqvQuotient (M : Model) (T : FormulaSet ℕ) : Type

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.FilterEqvQuotient M T = Quotient (LO.Modal.Kripke.FilterEqvSetoid M T)

theorem LO.Modal.Kripke.FilterEqvQuotient.finite (M : Model) (T : FormulaSet ℕ) (T_finite : Set.Finite T) : Finite (FilterEqvQuotient M T)

instance LO.Modal.Kripke.instNonemptyFilterEqvQuotient (M : Model) (T : FormulaSet ℕ) : Nonempty (FilterEqvQuotient M T)

class LO.Modal.Kripke.FilterOf (FM M : Model) (T : FormulaSet ℕ) [T.SubformulaClosed] : Prop

Imported declaration from the Incompleteness formalization.

• def_world : FM.World = FilterEqvQuotient M T
• def_rel₁ {x y : M.World} : x ≺ y → cast ⋯ ⟦x⟧ ≺ cast ⋯ ⟦y⟧
• def_box {Qx Qy : FM.World} : Qx ≺ Qy → Quotient.lift₂ (fun (x y : M.World) => ∀ (φ : Formula ℕ), □φ ∈ T → x ⊧ □φ → y ⊧ φ) ⋯ (cast ⋯ Qx) (cast ⋯ Qy)
• def_valuation (Qx : FM.World) (a : ℕ) (ha : Formula.atom a ∈ T := by trivial) : FM.Val Qx a ↔ Quotient.lift (fun (x : M.World) => M.Val x a) ⋯ (cast ⋯ Qx)

theorem LO.Modal.Kripke.reflexive_filterOf_of_reflexive {M : Model} {T : FormulaSet ℕ} [T.SubformulaClosed] {FM : Model} (h_filter : FilterOf FM M T) (hRefl : Std.Refl M.Rel) : Std.Refl FM.Rel

theorem LO.Modal.Kripke.serial_filterOf_of_serial {M : Model} {T : FormulaSet ℕ} [T.SubformulaClosed] {FM : Model} (h_filter : FilterOf FM M T) (hSerial : Serial M.Rel) : Serial FM.Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.standardFilterationValuation (M : Model) (T : FormulaSet ℕ) (Qx : FilterEqvQuotient M T) (a : ℕ) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.standardFilterationValuation M T Qx a = ∀ (ha : LO.Modal.Formula.atom a ∈ T), Quotient.lift (fun (x : M.World) => M.Val x a) ⋯ Qx

@[reducible, inline]

abbrev LO.Modal.Kripke.coarsestFilterationFrame (M : Model) (T : FormulaSet ℕ) [T.SubformulaClosed] : Frame

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.coarsestFilterationModel (M : Model) (T : FormulaSet ℕ) [T.SubformulaClosed] : Model

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.coarsestFilterationModel M T = { toFrame := LO.Modal.Kripke.coarsestFilterationFrame M T, Val := LO.Modal.Kripke.standardFilterationValuation M T }

instance LO.Modal.Kripke.coarsestFilterationModel.filterOf {M : Model} {T : FormulaSet ℕ} [T.SubformulaClosed] : FilterOf (coarsestFilterationModel M T) M T

@[reducible, inline]

abbrev LO.Modal.Kripke.finestFilterationFrame (M : Model) (T : FormulaSet ℕ) : Frame

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.finestFilterationModel (M : Model) (T : FormulaSet ℕ) : Model

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.finestFilterationModel M T = { toFrame := LO.Modal.Kripke.finestFilterationFrame M T, Val := LO.Modal.Kripke.standardFilterationValuation M T }

instance LO.Modal.Kripke.finestFilterationModel.filterOf {M : Model} {T : FormulaSet ℕ} [T.SubformulaClosed] : FilterOf (finestFilterationModel M T) M T

theorem LO.Modal.Kripke.finestFilterationModel.symmetric_of_symmetric {M : Model} {T : FormulaSet ℕ} (hSymm : IsSymmetric M.Rel) : IsSymmetric (finestFilterationModel M T).Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.finestFilterationTransitiveClosureModel (M : Model) (T : FormulaSet ℕ) : Model

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.finestFilterationTransitiveClosureModel M T = { toFrame := LO.Modal.Kripke.finestFilterationFrame M T^+, Val := LO.Modal.Kripke.standardFilterationValuation M T }

theorem LO.Modal.Kripke.finestFilterationTransitiveClosureModel.filterOf {M : Model} {T : FormulaSet ℕ} [T.SubformulaClosed] (M_trans : IsTrans M.World M.Rel) : FilterOf (finestFilterationTransitiveClosureModel M T) M T

Imported declaration from the Incompleteness formalization.

theorem LO.Modal.Kripke.finestFilterationTransitiveClosureModel.transitive {M : Model} {T : FormulaSet ℕ} : IsTrans (finestFilterationTransitiveClosureModel M T).World (finestFilterationTransitiveClosureModel M T).Rel

theorem LO.Modal.Kripke.finestFilterationTransitiveClosureModel.symmetric_of_symmetric {M : Model} {T : FormulaSet ℕ} (M_symm : IsSymmetric M.Rel) : IsSymmetric (finestFilterationTransitiveClosureModel M T).Rel

theorem LO.Modal.Kripke.finestFilterationTransitiveClosureModel.reflexive_of_transitive_reflexive {M : Model} {T : FormulaSet ℕ} [T.SubformulaClosed] (M_trans : IsTrans M.World M.Rel) (M_refl : Std.Refl M.Rel) : Std.Refl (finestFilterationTransitiveClosureModel M T).Rel

theorem LO.Modal.Kripke.filteration {M : Model} {T : FormulaSet ℕ} [T.SubformulaClosed] (FM : Model) (filterOf : FilterOf FM M T) {x : M.World} {φ : Formula ℕ} (hs : φ ∈ T) : x ⊧ φ ↔ cast ⋯ ⟦x⟧ ⊧ φ