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 : α) → L.Structure (M a)] : L.Prestructure ((↑u).productSetoid 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 : α) → L.Structure (M a)] : L.Structure ((↑u).Product 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 : α) → L.Structure (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 : α) → L.Structure (M a)] {β : Type u_3} (x : β → (a : α) → M a) (t : L.Term β) : 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 : α) → L.Structure (M a)] [∀ (a : α), Nonempty (M a)] {β : Type u_3} {n : ℕ} (φ : L.BoundedFormula β n) (x : β → (a : α) → M a) (v : Fin n → (a : α) → M a) : (φ.Realize (fun (i : β) => Quotient.mk' (x i)) fun (i : Fin n) => Quotient.mk' (v i)) ↔ ∀ᶠ (a : α) in ↑u, φ.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 : α) → L.Structure (M a)] [∀ (a : α), Nonempty (M a)] {β : Type u_3} (φ : L.Formula β) (x : β → (a : α) → M a) : (φ.Realize fun (i : β) => Quotient.mk' (x i)) ↔ ∀ᶠ (a : α) in ↑u, φ.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 : α) → 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.

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