The Tarski-Vaught test (sometimes called Tarski's criterion) is a result in model theory which characterizes the elementary substructures of a given structure using definable sets. It is often used to determine whether a substructure of a structure is elementary, and is particularly useful in the construction of elementary substructures. Formally,

For a given first-order language $mathcal\{L\}$, let $mathcal\{N\}$ be a structure with domain $N$, and $mathcal\{M\}$ be a substructure of $mathcal\{N\}$ with domain $M$ (written $mathcal\{M\}subseteqmathcal\{N\}$). Then $mathcal\{M\}$ is an elementary substructure of $mathcal\{N\}$ (written

More generally, the Tarski-Vaught test can be applied to any set of formulas Φ closed under taking subformulas. In this case it says that all formulas in the set are absolute for $mathcal\{M\}subseteqmathcal\{N\}$ if and only if whenever φ in the set Φ is of the form $exists\; xpsi(x,y\_1,...,y\_n)$ and y_i are in M then

$mathcal\{N\}vDash(exists\; xin\; N\; psi(x,y\_1,...,y\_n))$

implies

$mathcal\{N\}vDash(exists\; xin\; Mpsi(x,y\_1,...,y\_n)).$

Roughly speaking, this means that whenever N contains an element with some property definable by formulas from Φ then M contains an element with this property. The Tarski-Vaught theorem for elementary embeddings is the special case of this when Φ consists of all formulas; for technical reasons it is sometimes useful to allow Φ to consist of just a finite number of formulas (often all subformulas of a given formula).

Proof

First suppose

$mathcal\{N\}modelsexists\; xvarphi[b\_1,ldots,b\_n]$

(Note that the bracket notation here is used to indicate the semantic evaluation of the free variables of the formula.) But then, by definition of an elementary substructure,

$mathcal\{M\}modelsexists\; xvarphi[b\_1,ldots,b\_n]$

Thus there exists an $ain\; M$ such that $mathcal\{M\}modelsvarphi[a,b\_1,ldots,b\_n]$. Again by definition of elementary substructure, $mathcal\{N\}modelsvarphi[a,b\_1,ldots,b\_n]$, so $ain\; A$. Thus $Acap\; Mneemptyset$ as desired.

Conversely, suppose every nonempty subset of $N$ definable in $mathcal\{N\}$ with parameters from $M$ contains an element of $M$. We prove

$mathcal\{M\}notmodelspsi[a,a\_1,ldots,a\_n]$

so by the induction hypothesis, for all $ain\; M$,

(*) $mathcal\{N\}notmodelspsi[a,a\_1,ldots,a\_n]$

Now consider the set $Asubseteq\; N$ defined in $mathcal\{N\}$ by $psi(x,x\_1,ldots,x\_n)$ using parameters $a\_1,ldots,a\_n$. If there exists $bin\; N$ such that $mathcal\{N\}modelspsi[b,a\_1,ldots,a\_n]$, then $Aneemptyset$. By our hypothesis then, there exists an $ain\; Acap\; M$. But this contradicts (*). Thus $mathcal\{N\}notmodelsexists\; xpsi[a\_1,ldots,a\_n]$. It follows that

References

• Slaman, Theodore A. and W. Hugh Woodin. Mathematical Logic: The Berkeley Undergraduate Course. Spring 2006.