# mathlib3documentation

model_theory.ultraproducts

# Ultraproducts and Łoś's Theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main Definitions #

• first_order.language.ultraproduct.Structure is the ultraproduct structure on filter.product.

## Main Results #

• Łoś's Theorem: first_order.language.ultraproduct.sentence_realize. An ultraproduct models a sentence φ if and only if the set of structures in the product that model φ is in the ultrafilter.

## Tags #

ultraproduct, Los's theorem

@[protected, instance]
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) :
(λ (i : fin n), (x i)) = (λ (a : α), (λ (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 : } (φ : 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)] :