Élimination des quantificateurs

En logique mathématique, ou plus précisément en théorie des modèles, l'élimination des quantificateurs est l'action consistant à trouver une formule sans quantificateur équivalente à une formule donnée contenant éventuellement des quantificateurs dans la théorie considérée d'un certain langage.

Ainsi, si l'on considère la théorie des corps réels clos, le langage de cette théorie est L={+,•,<,0,1} où +,• sont deux symboles de fonction d'arité 2, < est un symbole de relation binaire, et 0,1 sont deux symboles de constante, la L-formule ∃x (ax² + bx + c = 0) est équivalente à la L-formule  dans la théorie, car dans cette théorie ax² + bx + c = 0 admet une racine si et seulement si a, b et c sont tous nuls, ou a est nul mais b est non nul, ou a non nul et  est positif.

Définitions 
Soient L un langage et T une L-théorie, on dit que T admet l'élimination des quantificateurs si pour toute L-formule F, il existe une L-formule G sans quantificateur telle que . Autrement dit, une théorie T du langage L admet l'élimination des quantificateurs si toute formule du langage L est équivalente à une formule sans quantificateur dans cette théorie.

Intérêt d'élimination des quantificateurs 
Les formules sans variables sont souvent plus facile à décider ; l'algorithme d'élimination des quantificateurs peut donc servir de procédure de décision pour cette théorie. Dans une théorie décidable admettant l'élimination des quantificateurs, il existe un algorithme qui en acceptant une formule donne toujours une formule sans quantificateur. Le seul problème est l'efficacité de l'algorithme. 

Elle nous permet aussi de mieux comprendre les ensembles définissables dans une théorie.

Quelques critères d'élimination des quantificateurs

Critère 1 
Soit  une L-theorie. 

Supposons que pour toute L-formule  sans quantificateur il existe une L-formule sans quantificateur  telle que . 

Alors, T admet l'élimination des quantificateurs.

Preuve 
Soit  une L-formule. On montre par l'induction sur la complexité de  qu'il existe une L-formule  sans quantificateur telle que .

Si  alors posons . Supposons que la propriété est vraie pour toutes les formules de complexité strictement plus petite que . Si , il y a trois cas : soit , alors par hypothèse d'induction il existe  sans quantificateur telle que  est équivalente à , il suffit de poser ; soit , alors par hypothèse d'induction il existe  et  sans quantificateur telles que  et , et on pose ; soit , par hypothèse de l'induction il existe  sans quantificateur telle que , et par hypothèse, il existe  sans quantificateur telle que , on pose .

Exemple: DLO 
On montre que  (Dense Linear Ordering) admet l’élimination des quantificateurs en vérifiant la condition du critère 1. Autrement dit, soit  une formule sans quantificateur, cherchons une formule  sans quantificateur telle que . 

 est sans quantificateur, donc  est équivalente à une formule sous forme disjonctive  où les  sont des formules atomiques (ou leur négation) du langage de . Comme  si et seulement si  pour un certain ,   est équivalente à une formule de la forme   où les  sont des formules atomiques (ou leur négation) du langage de .

Comme , , ,  et , on peut supposer que les  sont de la forme : , ou 

S'il existe  tel que  alors , donc  convient. Supposons que  pour tout . 

S'il existe  tel que  alors  convient. Donc on peut supposer que  n'est pas de la forme  pour tout . 

Donc les  sont de la forme : , ou .

Ainsi  où les  sont de la forme  ou , et les  sont de la forme  ou . 

On a que . Donc on a deux cas :

 Si , alors  convient. 

 Sinon si  ou , alors  convient car l'ordre est sans extrémités.

 Sinon  car l'ordre est dense, donc  convient.

Critère 2 
Soit  une L−théorie. 

Supposons que pour toute L-formule sans quantificateur , si  et  sont deux modèles de ,  est une sous-structure commune de  et ,  des éléments de l’ensemble de base de , et il existe  tel que , alors il existe  dans le domaine de  tel que . 

Alors,  admet l’élimination des quantificateurs.

Preuve 

Montrons la réciproque (la preuve directe est plus délicate). Soit  une L-formule sans quantificateur. Soient , deux modèles de ,  une sous-structure commune de  et , et  des éléments de . Supposons que . Alors par élimination des quantificateurs, il existe une L-formule sans quantificateur  telle que , et . Or, comme  est une sous-structure de  et  est sans quantificateur,  équivaut à , équivalant, de même, à , d'où enfin .

Exemple: DAG 
On montre que la théorie de groupe abélien divisible sans torsion () admet l’élimination des quantificateurs en montrant qu'elle vérifie la condition du critère 2. 

Soit  une formule sans quantificateur. Soient , deux groupes abélians divisibles sans torsion,  un sous-groupe commun de  et ,  tels que . On montre d'abord qu'il existe un sous-groupe commun  de  et  tel que  est un sous-groupe de , et puis on montre que  avant de conclure.

Montrons qu'il existe un sous-groupe commun  de  et  tel que  est une sous-groupe de :
Posons . On définit une relation d'équivalence  sur  par  si et seulement si . Posons . Notons  la -classe de . On définit  en posant .

 est bien définie: Soient On a que  Comme 

 est un groupe: Soient  On a ;

;

 est sans torsion: Soit  On a donc  Donc  Ainsi  car  est sans torsion.

 est divisible: Soit 

 est abélian: Soient 

Monstrons que  définie par  est une homomorphisme injectif: ;

 soient  alors ;

 soient  si et seulement si 

Montrons que  définie par  bien défini et est un homomorphisme injectif:

 est bien défini: Soient  alors . Donc 

 est un homomorphisme injectif: ;

 soient , 

 soient , si , alors , donc , donc ; si, alors 

De même, il existe aussi un homomorphisme injective de  dans . Ainsi on peut identifier  avec un sous-groupe commun conenant  de  et .

Montrons que :

 est une formule sans quantificateur, donc elle est équivalente à une formule sous forme disjonctive:  où les  sont des formules atomiques ou des négations de formules atomique du langage.
Quand  est satisfait, il existe  tel que  est satisfait.

Comme dans le langage, le seul symbole de prédicat est le symbole  et le seul symbole de fonction est ,  une formule atomique dans ce langage est de la forme  où les . Ainsi 

S'il existe  tel que , alors comme , car G est un groupe disivisble. Donc .

Sinon,  Comme H est sans torsion, donc  est infini, car sinon pour tout . Comme pour tout  est fini, il existe un élément dans  qui satisfait 

Comment  est une sous groupe de , il existe un élément de  satisfait , par conséquent,

Critère 3 
Soit  une L−théorie telle que

1. Pour toute , il existe une  et un monomorphisme tels que pour tout  et monomorphisme , il existe  tel que .

2. Si  sont deux modèles de  et  est sous-structure de  alors pour toute L-formule  et tout  dans la domaine de , s'il existe  dans la domaine de  tel que  est satisfaite dans , alors elle l'est aussi dans .

Alors,  admet l'élimination des quantificateurs.

Preuve 
Soit  une L-formule sans quantificateur. Supposons que  soient deux modèles de ,  une sous-structure commune de  et  ,  des éléments dans  et  un élément de  tels que . Montrons qu'il existe  dans  tel que  et puis conclure par le critère 1:

Comme  et que  est une sous-structure de , on a que . Par hypothèse 1) il existe  telle que pour toute  qui est extension de ,  est une sous-structure de . Par conséquent,  est sous-structure de  et de .

Comme  est une formule sans quantificateur,  est une sous-structure de  et que les formules sans quantificateurs sont préservées par la sous-structure, on a que . De même .

Ainsi on conclut par le critère 2 que  admet l'élimination des quantificateurs.

Exemple: Corps algébriquement clos 
On note  pour la théorie des corps algébriquement clos. Pour démontrer que  admet l'élimination des quantificateurs, on montre d'abord l'ensemble  des conséquences universelles de la théorie des corps algébriquement clos est la théorie des anneaux intègres. Et puis, on montre que  vérifie les conditions du critère 3 pour conclure.

Montrons que  est la théorie des anneaux intègres:
Soit  un anneau intègre. Soit  corps-extension algébrique du corps de fraction de . On a que  est un modèle de . Comme il existe un homomorphisme injectif de  dans le corps de fraction de , et qu'il existe un homomorphisme injective du corps de fraction de  dans , on déduit que   est un sous-anneau de . Donc .  Soit . En particulier, . Comme de plus tous les axiomes de la théorie d'anneaux sont dans ,  est un anneau intègre. 

Montrons que  vérifie la première condition du critère 3:
Soit  un modèle de .  est un anneau intègre. Soit  le corps-extension algébrique du corps de fraction de . Soit  un modèle de  tel que  est un sous-anneau de . Comme  est un corps contenant , donc  contenant le corps de fraction de . Et comme  est algébriquement clos,  contient, par définition,  le corps-extension algébrique de . 

Montrons que  vérifie la deuxième condition du critère 3:
Soient  tels que  est une sous-structure de ,  une L-formule sans quantificateur,  éléments de la domaine de . Supposons qu'il existe  élément de la domaine de  tel que . Montrons qu'il existe  élément de la domaine de  tel que .  est une formule sans quantificateur donc elle est équivalente à une formule sous forme disjonctive  où les  sont des formules atomiques ou des négations de formules atomiques.  si et seulement si  pour un certain . On peut donc supposer, sans perte de généralité, que F est une formule de la forme  où les  sont des formules atomiques ou des négations de formules atomiques. Et le langage de ACF est le langage d'anneau, une formule atomique  est de la forme  où P est une polynôme de .  est un polynôme de . Donc il existe  dans  tels que . On a deux cas:

S'il existe un polynôme  non nul, alors comme on a  pour tout , on a en particulier . Comme M est un sous-corps algébriquement clos de N et b est un élément de la domaine de N, on a que b est un élément de la domaine de M.

Sinon, alors . Soient  l'ensemble de racines  de  pour tout . On sait que  est fini pour tout  et que  est infini donc il existe  dans  tel que . Donc il existe  dans la domaine de M tel que .

Exemples 
Exemples de théories admettant l'élimination des quantificateurs :
 corps réels clos (, algorithme de ) ;
 corps algébriquement clos de caractéristique quelconque ou fixée (par exemple via les bases de Gröbner et le théorème d'extension) ;
 théorie linéaire des rationnels ou des réels (algorithmes de Ferrante et Rackoff, de Loos et ) ;
 théorie linéaire des entiers, dite aussi arithmétique de Presburger.
Toutes ces théories sont donc .

Conséquence

Modèle-complétude 
Soit  une -théorie admettant l'élimination des quantificateurs. Soient  deux modèles de  tels que  est une sous-structure de . Soit  une -formule et  une assignation des variables dans . Par l'élimination des quantificateurs, il existe une -formule sans quantificateur  qui est équivalente à  dans . On a que  si et seulement si  et que  si et seulement si . Comme l'injection canonique de  dans  est un homomorphisme injectif et que  est une formule sans quantificateur, on a que  si et seulement si . On conclut que  si et seulement si . Donc  est une sous-structure élémentaire de . Ainsi  est modèle-complète (par définition).

Notes et références

Voir aussi

Articles connexes 
 Skolémisation
 Théorème de Herbrand

Bibliographie 
 Jean-Louis Krivine et Georg Kreisel, Éléments de logique mathématique (théorie des modèles), Paris, Dunod, 1966, chap. 4, pdf
 Jean-François Pabion, Logique mathématique, chapitre VI « Élimination des quantificateurs » pp. 191-210, Hermann, Paris 1976 
 René David, Karim Nour, Christophe Raffalli, Introduction à la logique-theorie de la démonstration, 2e édition, Dunod
David Marker, Model Theory: An introduction, Springer
René Cori, Daniel Lascar, Logique mathématique 2, Dunod

Algorithmique
Logique mathématique