Ultraproducts and Łoś's Theorem

Main Definitions

• FirstOrder.Language.Ultraproduct.Structure is the ultraproduct structure on Filter.Product.

Main Results

• Łoś's Theorem: FirstOrder.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

instance FirstOrder.Language.Ultraproduct.setoidPrestructure {α : Type u_1} (M : α → Type u_2) (u : Ultrafilter α) {L : FirstOrder.Language} [(a : α) → FirstOrder.Language.Structure L (M a)] : FirstOrder.Language.Prestructure L (Filter.productSetoid (↑u) M)

Equations

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

instance FirstOrder.Language.Ultraproduct.structure {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → FirstOrder.Language.Structure L (M a)] : FirstOrder.Language.Structure L (Filter.Product (↑u) M)

Equations

• FirstOrder.Language.Ultraproduct.structure = FirstOrder.Language.quotientStructure

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 : L.Functions n) (x : Fin n → (a : α) → M a) : (FirstOrder.Language.Structure.funMap f fun (i : Fin n) => Quotient.mk' (x i)) = Quotient.mk' fun (a : α) => FirstOrder.Language.Structure.funMap f fun (i : Fin n) => x i 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 β) : FirstOrder.Language.Term.realize (fun (i : β) => Quotient.mk' (x i)) t = Quotient.mk' fun (a : α) => FirstOrder.Language.Term.realize (fun (i : β) => x i a) t

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 : Fin n) => Quotient.mk' (v i)) ↔ ∀ᶠ (a : α) in ↑u, FirstOrder.Language.BoundedFormula.Realize φ (fun (i : β) => x i a) fun (i : Fin n) => 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)] : Nonempty (Filter.Product (↑u) M)

Equations

• (_ : Nonempty (Filter.Product (↑u) M)) = (_ : Nonempty (Filter.Product (↑u) M))