English
If an L-embedding f: M ⟶ N satisfies the Tarski–Vaught test, then f is L-elementary; i.e., for every finite n, every formula φ and x, φ is realized in N via f∘x iff it is realized in M via x.
Русский
Если вложение f: M → N удовлетворяет тесту Тарски–Ваутта, то оно элементарно; то есть для любой конечной длины n, любой формулы φ и любых x, φ существует в N через f∘x тогда и только тогда, когда φ существует в M через x.
LaTeX
$$$htv \Rightarrow \forall n\, (\varphi : L.Formula(Fin\,n))\, (x : Fin\,n \to M),\ \varphi.Realize (f \circ x) \leftrightarrow \varphi.Realize x$$$
Lean4
/-- The **Tarski-Vaught test** for elementarity of an embedding. -/
theorem isElementary_of_exists (f : M ↪[L] N)
(htv :
∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
φ.Realize default (Fin.snoc (f ∘ x) a : _ → N) → ∃ b : M, φ.Realize default (Fin.snoc (f ∘ x) (f b) : _ → N)) :
∀ {n} (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (f ∘ x) ↔ φ.Realize x :=
by
suffices h :
∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M), φ.Realize (f ∘ default) (f ∘ xs) ↔ φ.Realize default xs
by
intro n φ x
exact φ.realize_relabel_sumInr.symm.trans (_root_.trans (h n _ _) φ.realize_relabel_sumInr)
refine fun n φ => φ.recOn ?_ ?_ ?_ ?_ ?_
· exact fun {_} _ => Iff.rfl
· intros
simp [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]
· intros
simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]
erw [map_rel f]
· intro _ _ _ ih1 ih2 _
simp [ih1, ih2]
· intro n φ ih xs
simp only [BoundedFormula.realize_all]
refine ⟨fun h a => ?_, ?_⟩
· rw [← ih, Fin.comp_snoc]
exact h (f a)
· contrapose!
rintro ⟨a, ha⟩
obtain ⟨b, hb⟩ :=
htv n φ.not xs a
(by
rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)]
exact ha)
refine ⟨b, fun h => hb (Eq.mp ?_ ((ih _).2 h))⟩
rw [Unique.eq_default (f ∘ default), Fin.comp_snoc]
