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). Autrement dit, A est fermée sous la fourniture de témoins existentiels dans M pour les formules à paramètres dans A.

Principe

L'élémentarité se vérifie par l'existence de témoins : pour être un sous‑modèle élémentaire, une sous‑structure doit contenir en elle-même des témoins pour chaque assertion existentielle vraie dans la structure plus grande avec paramètres tirés de la sous‑structure.

Démonstration

Dans la construction par le lemme de Löwenheim‑Skolem descendant, on vérifie souvent l'élémentarité du sous‑modèle construit en appliquant le critère de Tarski‑Vaught : en ajoutant dénombrablement de témoins pour les formules existentielles au fur et à mesure qu'on agrandit un ensemble, l'ensemble limite satisfait le critère et est donc un sous‑modèle élémentaire de la structure originale.

Mauvaise application

N'utiliser que des formules universelles ou oublier d'autoriser des paramètres provenant de la sous‑structure lors de l'application du test ; une autre erreur est de croire que le critère s'applique sans changement dans des logiques au‑delà du premier ordre sans traiter des propriétés sémantiques supplémentaires de ces logiques.

Conséquence

Le critère est un outil pratique pour construire et reconnaître des sous‑modèles élémentaires, permettant la construction de chaînes de sous‑structures élémentaires, d'enveloppes de Skolem et des applications dans des arguments de compacité et des réductions modèle‑théoriques.

Inversion

L'échec du critère atteste la non‑élémentarité : il existe une formule existentielle à paramètres dans A qui est satisfaite dans M mais sans témoin dans A, donc A omet une propriété existentielle de M et ne peut être élémentaire.

Limite

S'applique en logique du premier ordre aux sous‑structures d'un modèle donné dans un langage fixé ; il présuppose la sémantique usuelle où la quantification existentielle est réalisée par des éléments et ne se généralise pas automatiquement aux logiques d'ordre supérieur ou infinitaires sans modifications.

Tension sémantique

Le test de Tarski‑Vaught est une condition sur témoins existentiels qui complète des caractérisations plus sémantiques ou par va‑et‑vient de l'élémentarité (comme la satisfaction de toutes les formules ou des arguments par quasi‑isomorphismes) ; une tension apparaît dans le choix d'une méthode pratique pour vérifier l'élémentarité dans des constructions concrètes.

Synthèse

Le critère de Tarski‑Vaught réduit la tâche universelle de vérifier la vérité de toutes les formules à la vérification de l'existence de témoins pour les formules existentielles à paramètres : une sous‑structure est élémentaire exactement lorsqu'elle est fermée sous témoins existentiels, ce qui en fait un critère central et vérifiable en construction de modèles.