Cet article est une ébauche concernant les mathématiques.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
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 faciles à 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 (théorème de Tarski-Seidenberg (en), algorithme de décomposition algébrique cylindrique (en)) ;
Toutes ces théories sont donc modèle-complètes (en).
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
↑(en) Philipp Rothmaler, Introduction to Model Theory, CRC Press, (lire en ligne), p. 141.
↑(en) Jeanne Ferrante et Charles Rackoff, « A decision procedure for the first order theory of real addition with order », SIAM J. on Computing, vol. 4, no 1, , p. 69-76 (DOI 10.1137/0204006).
↑(en) Aaron R. Bradley et Zohar Manna, The Calculus of Computation : Decision Procedures with Applications to Verification, Berlin, Springer, , 366 p. (ISBN978-3-540-74112-1).
↑(en) Rüdiger Loos et Volker Weispfenning, « Applying linear quantifier elimination », The Computer Journal, vol. 36, no 5, , p. 450-462 (DOI 10.1093/comjnl/36.5.450, lire en ligne [PDF]).