English
For a bounded formula φ with n free variables, its realization in the ultraproduct with a family x_i and v is equivalent to the almost-everywhere realization in the coordinate models; i.e., Realize in the ultraproduct holds iff almost all components realize the corresponding coordinatewise instances.
Русский
Для ограниченной формулы φ с n свободными переменными реализация φ в ультропроизведении с семействами x_i и v эквивалентна почти везде реализации на координатах; т.е. Realize в ультропроизведении эквиваленты реализуется почти во всех компонентных моделях.
LaTeX
$$$\phi.Realize\bigl( (x_i) \bigr) \text{ in ultraproduct } \iff \forall^u a, \phi.Realize\bigl( (x_i(a))\bigr)$$$
Lean4
theorem boundedFormula_realize_cast {β : Type*} {n : ℕ} (φ : L.BoundedFormula β n) (x : β → ∀ a, M a)
(v : Fin n → ∀ a, M a) :
(φ.Realize (fun i : β => (x i : (u : Filter α).Product M)) (fun i => (v i : (u : Filter α).Product M))) ↔
∀ᶠ a : α in u, φ.Realize (fun i : β => x i a) fun i => v i a :=
by
letI := (u : Filter α).productSetoid M
induction φ with
| falsum => simp only [BoundedFormula.Realize, eventually_const]
|
equal =>
have h2 : ∀ a : α, (Sum.elim (fun i : β => x i a) fun i => v i a) = fun i => Sum.elim x v i a := fun a =>
funext fun i => Sum.casesOn i (fun i => rfl) fun i => rfl
simp only [BoundedFormula.Realize, h2]
erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm, term_realize_cast, term_realize_cast]
exact Quotient.eq''
|
rel =>
have h2 : ∀ a : α, (Sum.elim (fun i : β => x i a) fun i => v i a) = fun i => Sum.elim x v i a := fun a =>
funext fun i => Sum.casesOn i (fun i => rfl) fun i => rfl
simp only [BoundedFormula.Realize, h2]
erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm]
conv_lhs => enter [2, i]; erw [term_realize_cast]
apply relMap_quotient_mk'
| imp _ _ ih ih' =>
simp only [BoundedFormula.Realize, ih v, ih' v]
rw [Ultrafilter.eventually_imp]
| @all k φ ih =>
simp only [BoundedFormula.Realize]
apply
Iff.trans (b :=
∀ m : ∀ a : α, M a,
φ.Realize (fun i : β => (x i : (u : Filter α).Product M))
(Fin.snoc (((↑) : (∀ a, M a) → (u : Filter α).Product M) ∘ v) (m : (u : Filter α).Product M)))
· exact Quotient.forall
have h' :
∀ (m : ∀ a, M a) (a : α),
(fun i : Fin (k + 1) => (Fin.snoc v m : _ → ∀ a, M a) i a) = Fin.snoc (fun i : Fin k => v i a) (m a) :=
by
refine fun m a => funext (Fin.reverseInduction ?_ fun i _ => ?_)
· simp only [Fin.snoc_last]
· simp only [Fin.snoc_castSucc]
simp only [← Fin.comp_snoc]
simp only [Function.comp_def, ih, h']
refine ⟨fun h => ?_, fun h m => ?_⟩
· contrapose! h
simp_rw [← Ultrafilter.eventually_not, not_forall] at h
refine
⟨fun a : α => Classical.epsilon fun m : M a => ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m), ?_⟩
rw [← Ultrafilter.eventually_not]
exact Filter.mem_of_superset h fun a ha => Classical.epsilon_spec ha
· rw [Filter.eventually_iff] at *
exact Filter.mem_of_superset h fun a ha => ha (m a)
