Tarski-Vaught test (source code)

= Tarski-Vaught test
{c}
{wiki=Tarski–Vaught_test}

A substructure $M\subseteq N$ is elementary if and only if, whenever $N\models\exists x\,\varphi(x,\bar a)$ with parameters $\bar a$ from $M$, some witness $b\in M$ satisfies $N\models\varphi(b,\bar a)$.