Élimination des Quantificateurs

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.

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.

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.