Une théorie T (ou une structure) possède l'élimination des quantificateurs si toute formule du premier ordre est équivalente modulo T à une formule sans quantificateurs ; de manière équivalente, la vérité de toute formule est déterminée par des informations sans quantificateurs dans les modèles de T.

Principe

L'idée organisatrice est la réduction de la complexité logique : supprimer les quantificateurs existentiels et universels afin que les ensembles et relations définissables se décrivent par des conditions sans quantificateurs (souvent algébriques ou atomiques) dans le langage choisi.

Démonstration

Exemple : la théorie des corps réels clos admet l'élimination des quantificateurs dans le langage des anneaux ordonnés : toute formule est équivalente à une combinaison booléenne sans quantificateurs d'inégalités polynomiales, ce qui sous-tend la décidabilité et la description géométrique des ensembles définissables.

Mauvaise application

Supposer que l'élimination des quantificateurs est indépendante du langage ou de la théorie ; ignorer qu'elle peut échouer dans un langage donné mais se rétablir en ajoutant des symboles définitionnels ou des paramètres, ou confondre QE avec une simple décidabilité sans fournir de réduction effective.

Conséquence

Quand T a l'élimination des quantificateurs, les ensembles définissables sont contrôlés par formules sans quantificateurs, de nombreuses analyses modelthéoriques se simplifient (par ex. élimination des imaginaires, décomposition cellulaire dans des cas spécifiques) et apparaissent souvent des résultats sur la décidabilité et la classification.

Inversion

L'absence d'élimination des quantificateurs signifie que certaines propriétés nécessitent véritablement des quantificateurs pour être exprimées : les ensembles définissables ont alors une description et une classification plus complexes.

Limite

L'élimination des quantificateurs est relative à un langage et à une théorie ; changer le langage (ajouter des symboles de fonction ou de relation) peut faire apparaître ou disparaître QE. QE concerne les quantificateurs du premier ordre et ne restreint pas la définissabilité d'ordre supérieur ou infinitaire.

Tension sémantique

Une tension existe entre l'élimination des quantificateurs et la complétude modèle‑théorique : QE implique la complétude modèle, mais toute théorie modèle‑complète n'élimine pas forcément les quantificateurs dans le langage donné ; il y a aussi tension avec la décidabilité effective et les descriptions géométriques.

Synthèse

L'élimination des quantificateurs signifie que, modulo la théorie, toute relation définissable se décrit déjà sans quantificateurs : elle compresse la complexité du premier ordre en termes sans quantificateurs, ce qui permet des descriptions concrètes des ensembles définissables et souvent de simplifier les problèmes de décision.