Tarski–Vaught witness test

Suppose $\mathcal{A}\prec \mathcal{M}$ and $\mathcal{M}\models \mathrm{\exists }x\psi [\bar{a}]$. By elementarity $\mathcal{A}\models \mathrm{\exists }x\psi [\bar{a}]$, so some $b\in A$ satisfies $\mathcal{A}\models \psi [\bar{a},x:=b]$. Applying elementarity to the matrix and this enlarged tuple gives $\mathcal{M}\models \psi [\bar{a},x:=b]$. This proves necessity, including existential sentences with no parameters.

Now assume the witness condition. For a term evaluated at a tuple from $A$, variable values and constant values coincide in the two structures. If its argument terms coincide, their values belong to $A$, and the restricted function gives the same output in both structures. Constructor induction therefore gives equality of all term values, with positive arity as required by the signature convention. Literal equality and relation restriction then give identical truth values for atomic formulas, with the positive arities in the signature.

Induct simultaneously over all parameter tuples for each formula. If $\theta$ has identical truth in both structures, $\mathrm{\neg }\theta$ does too, since its truth is the negation of that same value. If $\theta ,\eta$ each have identical truth, $\theta \wedge \eta$ does too, since it is true exactly when both are true. Restrict a given tuple to the required free variables when applying the induction hypothesis.

For $\mathrm{\exists }x\psi$, if it holds in $\mathcal{A}$, choose its witness $b\in A$. The induction hypothesis for $\psi$ transfers its truth to $\mathcal{M}$, where $b$ is also a witness. Conversely, if it holds in $\mathcal{M}$, the assumed condition supplies $b\in A$ for which the matrix is true in $\mathcal{M}$. The induction hypothesis transfers the matrix to $\mathcal{A}$, giving the existential statement there. Updates at $x$ overwrite any earlier value, so the argument also covers a vacuous quantifier.

Steps 1.2–1.4 cover the primitive constructors equality, relations, negation, conjunction and existential quantification. All other connectives are their abbreviations. Thus every formula agrees on every tuple from $A$, which is exactly $\mathcal{A}\prec \mathcal{M}$. Together with step 1.1 this proves the equivalence.