Propriété d'une théorie selon laquelle toute formule est équivalente dans la théorie à une formule sans quantificateurs ; autrement dit, les ensembles définissables se décrivent dans la langue donnée sans recours aux quantificateurs existentiels ou universels.

Principe

Réduire la définissabilité à des atomes et combinaisons booléennes : lorsqu'on peut éliminer les quantificateurs, les questions sur les ensembles et relations définissables se ramènent à des vérifications sans quantificateurs, permettant souvent des descriptions explicites et des procédures de décision.

Démonstration

Exemple : la théorie des corps réels clos admet l'élimination des quantificateurs dans la langue des corps ordonnés, ce qui fournit une description explicite des ensembles définissables comme combinaisons booléennes finies d'inégalités polynomiales ; les corps algébriquement clos admettent l'élimination des quantificateurs dans la langue des anneaux, ce qui simplifie la classification des ensembles définissables.

Mauvaise application

Supposer que l'élimination des quantificateurs dans une langue étendue se répercute sur la langue originale, ou croire que l'EDQ garantit automatiquement des procédures de décision efficaces : l'EDQ fournit une réduction logique mais pas nécessairement un algorithme efficace en termes de complexité.

Conséquence

L'élimination des quantificateurs donne des caractérisations concrètes des ensembles définissables, induit souvent la complétude modélique et entraîne fréquemment la décidabilité lorsque la théorie sans quantificateurs est traitable algorithmique.

Inversion

L'absence d'élimination des quantificateurs signifie qu'il existe des propriétés exprimables uniquement avec des quantificateurs ; de telles théories conservent des phénomènes définissables d'ordre supérieur qui ne se réduisent pas à des formules sans quantificateurs.

Limite

L'élimination des quantificateurs dépend de la langue : ajouter ou retirer des symboles (fonctions, relations, sortes) peut créer ou faire disparaître l'EDQ ; c'est aussi une équivalence syntaxique relative à la théorie, non une propriété absolue des structures sans référence à la langue choisie.

Tension sémantique

Tension entre EDQ et complétude modélique : l'EDQ implique la complétude modélique, mais la réciproque est généralement fausse ; autre tension : EDQ vs élimination des imaginaires — l'EDQ porte sur les formules, l'EI sur les paramètres canoniques des ensembles définissables.

Synthèse

L'élimination des quantificateurs signifie que la puissance expressive d'une théorie se capture sans quantificateurs dans sa langue, transformant des problèmes abstraits de définissabilité en descriptions explicites sans quantificateurs et rendant souvent concrètes les tâches de décision et de classification.