mathlib documentation

model_theory.ultraproducts

Ultraproducts and Łoś's Theorem #

Main Definitions #

Main Results #

Tags #

ultraproduct, Los's theorem

@[protected, instance]
def first_order.language.ultraproduct.setoid_prestructure {α : Type u_1} (M : α → Type u_2) (u : ultrafilter α) {L : first_order.language} [Π (a : α), L.Structure (M a)] :
Equations
@[protected, instance]
def first_order.language.ultraproduct.Structure {α : Type u_1} {M : α → Type u_2} {u : ultrafilter α} {L : first_order.language} [Π (a : α), L.Structure (M a)] :
Equations
theorem first_order.language.ultraproduct.fun_map_cast {α : Type u_1} {M : α → Type u_2} {u : ultrafilter α} {L : first_order.language} [Π (a : α), L.Structure (M a)] {n : } (f : L.functions n) (x : fin nΠ (a : α), M a) :
first_order.language.Structure.fun_map f (λ (i : fin n), (x i)) = (λ (a : α), first_order.language.Structure.fun_map f (λ (i : fin n), x i a))
theorem first_order.language.ultraproduct.term_realize_cast {α : Type u_1} {M : α → Type u_2} {u : ultrafilter α} {L : first_order.language} [Π (a : α), L.Structure (M a)] {β : Type u_3} (x : β → Π (a : α), M a) (t : L.term β) :
first_order.language.term.realize (λ (i : β), (x i)) t = (λ (a : α), first_order.language.term.realize (λ (i : β), x i a) t)
theorem first_order.language.ultraproduct.bounded_formula_realize_cast {α : Type u_1} {M : α → Type u_2} {u : ultrafilter α} {L : first_order.language} [Π (a : α), L.Structure (M a)] [∀ (a : α), nonempty (M a)] {β : Type u_3} {n : } (φ : L.bounded_formula β n) (x : β → Π (a : α), M a) (v : fin nΠ (a : α), M a) :
φ.realize (λ (i : β), (x i)) (λ (i : fin n), (v i)) ∀ᶠ (a : α) in u, φ.realize (λ (i : β), x i a) (λ (i : fin n), v i a)
theorem first_order.language.ultraproduct.realize_formula_cast {α : Type u_1} {M : α → Type u_2} {u : ultrafilter α} {L : first_order.language} [Π (a : α), L.Structure (M a)] [∀ (a : α), nonempty (M a)] {β : Type u_3} (φ : L.formula β) (x : β → Π (a : α), M a) :
φ.realize (λ (i : β), (x i)) ∀ᶠ (a : α) in u, φ.realize (λ (i : β), x i a)
theorem first_order.language.ultraproduct.sentence_realize {α : Type u_1} {M : α → Type u_2} {u : ultrafilter α} {L : first_order.language} [Π (a : α), L.Structure (M a)] [∀ (a : α), nonempty (M a)] (φ : L.sentence) :
u.product M φ ∀ᶠ (a : α) in u, M a φ

Łoś's Theorem : A sentence is true in an ultraproduct if and only if the set of structures it is true in is in the ultrafilter.

@[protected, instance]
def first_order.language.ultraproduct.product.nonempty {α : Type u_1} {M : α → Type u_2} {u : ultrafilter α} [∀ (a : α), nonempty (M a)] :