Solution (source code)

= Solution

The <Tarski-Vaught test> states that a substructure $M\subseteq N$ is an <elementary substructure> if and only if every formula $\varphi(x,\bar y)$ and tuple $\bar a\in M$ satisfy
$$
N\models\exists x\,\varphi(x,\bar a)
\quad\Longrightarrow\quad
N\models\varphi(b,\bar a)\text{ for some }b\in M.
$$
Necessity follows immediately from elementarity. Conversely, assume the witness condition. Induct on formulas to prove that $M\models\psi(\bar a)$ exactly when $N\models\psi(\bar a)$ for every $\bar a\in M$. Atomic formulas agree because $M$ is a substructure, and Boolean connectives follow by induction. A witness in $M$ is also one in $N$; a witness in $N$ can be replaced by one in $M$ by hypothesis, after which induction applies to the matrix. Universal formulas follow by negation. Thus \b[the witness condition is equivalent to $M\preccurlyeq N$].