Une procédure ou une propriété d'une théorie du premier ordre ou d'un langage formel qui transforme toute formule contenant des quantificateurs existentiels ou universels en une formule équivalente ne contenant aucun quantificateur, au sens sémantique de la théorie.

Principe

Si une théorie admet l'élimination des quantificateurs alors pour toute formule φ(x) il existe une formule sans quantificateurs ψ(x) telle que φ et ψ définissent le même ensemble dans chaque modèle de la théorie ; la procédure réécrit systématiquement les expressions quantifiées en utilisant les primitives du langage et les axiomes de la théorie.

Démonstration

Dans la théorie des corps réels clos, la procédure de Tarski (mise en œuvre par la décomposition cylindrique) transforme une formule avec inégalités polynomiales et quantificateurs en une combinaison booléenne équivalente de conditions de signes polynomiaux, permettant de décider la vérité des phrases sur les nombres réels.

Mauvaise application

Supposer que l'élimination des quantificateurs est disponible pour des théories quelconques (par exemple l'arithmétique de Peano) ou utiliser une transformation dite 'd'élimination' qui ne préserve que la satisfaisabilité et non l'équivalence ; appliquer la procédure sans vérifier si le langage cible peut exprimer la formule éliminée conduit à des réécritures invalides.

Conséquence

Lorsqu'elle est appliquée avec succès, l'élimination des quantificateurs fournit une procédure de décision effective pour les phrases, des caractérisations des ensembles définissables et des formules simplifiées pour la construction de modèles et les requêtes ; elle peut toutefois entraîner une explosion de taille des formules ou une complexité de calcul élevée.

Inversion

Réintroduire des quantificateurs (ou les ajouter) augmente la puissance expressive et permet de décrire de manière compacte des familles de structures ou des comportements infinis qu'une formule sans quantificateurs ne peut pas; l'inversion met en évidence une perte de brièveté ou de commodité définitionnelle.

Limite

S'applique aux cadres du premier ordre et dépend de la théorie et du langage ; certaines théories admettent une élimination complète, d'autres une élimination partielle ou relative, et les logiques d'ordre supérieur ou les théories avec constructions non interprétées peuvent ne pas admettre d'élimination. Les coûts computationnels et la représentabilité dans le langage quantificateur‑libre cible sont des limites pratiques.

Tension sémantique

Une tension apparaît entre l'élimination des quantificateurs et la skolemisation : la skolemisation supprime les existenciels en ajoutant des symboles de fonctions mais ne préserve que la satisfaisabilité, pas l'équivalence ; l'élimination préserve l'équivalence mais peut nécessiter des constructions booléennes ou algébriques plus riches.

Synthèse

L'élimination des quantificateurs est à la fois une propriété sémantique d'une théorie et une famille de procédures syntaxiques qui remplacent des descriptions quantifiées par des formules équivalentes sans quantificateurs ; sa présence implique décidabilité et descriptions concrètes des ensembles définissables, son absence signale des barrières expressives ou computationnelles.