Documentation

Mathlib.ModelTheory.Ultraproducts

Ultraproducts and Łoś's Theorem #

Main Definitions #

Main Results #

Tags #

ultraproduct, Los's theorem

theorem FirstOrder.Language.Ultraproduct.funMap_cast {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → FirstOrder.Language.Structure L (M a)] {n : } (f : FirstOrder.Language.Functions L n) (x : Fin n(a : α) → M a) :
theorem FirstOrder.Language.Ultraproduct.term_realize_cast {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → FirstOrder.Language.Structure L (M a)] {β : Type u_3} (x : β(a : α) → M a) (t : FirstOrder.Language.Term L β) :
theorem FirstOrder.Language.Ultraproduct.boundedFormula_realize_cast {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → FirstOrder.Language.Structure L (M a)] [∀ (a : α), Nonempty (M a)] {β : Type u_3} {n : } (φ : FirstOrder.Language.BoundedFormula L β n) (x : β(a : α) → M a) (v : Fin n(a : α) → M a) :
(FirstOrder.Language.BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ∀ᶠ (a : α) in u, FirstOrder.Language.BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
theorem FirstOrder.Language.Ultraproduct.realize_formula_cast {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → FirstOrder.Language.Structure L (M a)] [∀ (a : α), Nonempty (M a)] {β : Type u_3} (φ : FirstOrder.Language.Formula L β) (x : β(a : α) → M a) :
(FirstOrder.Language.Formula.Realize φ fun i => Quotient.mk' (x i)) ∀ᶠ (a : α) in u, FirstOrder.Language.Formula.Realize φ fun i => x i a
theorem FirstOrder.Language.Ultraproduct.sentence_realize {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → FirstOrder.Language.Structure L (M a)] [∀ (a : α), Nonempty (M a)] (φ : FirstOrder.Language.Sentence L) :
Filter.Product (u) 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.

instance FirstOrder.Language.Ultraproduct.Product.instNonempty {α : Type u_1} {M : αType u_2} {u : Ultrafilter α} [∀ (a : α), Nonempty (M a)] :