Tarski-Vaught test

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

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

References

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