---
tag: 60SA99BER7
kind: statement
role: proposition
name: Tarski–Vaught test
msc: [03C07]
uses: [8WZF9SBP39, 676H7EGTKJ, 983GZBQYT4, HYJ10AF6RT]
about: [8WZF9SBP39]
sources:
  - url: https://en.wikipedia.org/wiki/Elementary_equivalence
---

## Statement

Let $L$ be a signature and let $\mathcal{M}$ be a [[substructure|676H7EGTKJ]] of an $L$-[[structure|983GZBQYT4]] $\mathcal{N}$, with domains $M \subseteq N$.
Then $\mathcal{M}$ is an [[elementary substructure|8WZF9SBP39]] of $\mathcal{N}$ if and only if the following holds.
For every $L$-[[formula|HYJ10AF6RT]] $\varphi(x_1, \dots, x_n, y)$ and all $a_1, \dots, a_n \in M$, if $\mathcal{N} \models \exists y \, \varphi(a_1, \dots, a_n, y)$, then there is $b \in M$ with $\mathcal{N} \models \varphi(a_1, \dots, a_n, b)$.

## Remarks

The condition mentions truth only in $\mathcal{N}$, which makes it easier to check than the definition.
The forward direction is direct: if $\mathcal{N} \models \exists y \, \varphi(\bar a, y)$, then $\mathcal{M} \models \exists y \, \varphi(\bar a, y)$, so some $b \in M$ has $\mathcal{M} \models \varphi(\bar a, b)$, hence $\mathcal{N} \models \varphi(\bar a, b)$.
For the converse, one proves by induction on $\varphi$ that $\mathcal{M} \models \varphi(\bar a)$ if and only if $\mathcal{N} \models \varphi(\bar a)$.
Atomic formulas agree because $\mathcal{M}$ is a substructure, the connectives are immediate, and the condition handles the existential quantifier.

Example of use: in the proof of the downward [[Löwenheim–Skolem theorem|484M0TZ1S7]], one closes a subset of $N$ under witnesses for all existential formulas.
The test then shows that the result is an elementary substructure.

## Explanations

### L1 human

The test says: a substructure is elementary when every object that the big structure can describe with parameters from the small one has a witness already in the small one.
The positive integers inside $(\N, <)$ fail the test: the formula $y < 1$ has the witness $0$ in $\N$ but none among the positive integers.

### L2 human

The Tarski–Vaught test is the standard tool to build elementary substructures.
It underlies the downward Löwenheim–Skolem theorem and the construction of Skolem hulls.
Combined with automorphisms of $\mathcal{N}$ that fix finitely many elements of $M$, it also proves results such as $(\Q, <) \preceq (\R, <)$: if $\mathcal{N} \models \exists y \, \varphi(\bar a, y)$, an automorphism fixing $\bar a$ moves a witness into $\Q$.