Test de Tarski‑Vaught

Un critère syntaxique permettant de décider quand un sous‑structure A d'une structure M (dans un langage du premier ordre donné) est un sous‑modèle élémentaire : A est élémentaire dans M si et seulement si pour toute formule φ(x,y) et tout tuple a de A, si M satisfait ∃x φ(x,a) alors il existe b dans A tel que M satisfasse φ(b,a).