Élimination des quantificateurs

Un article de Wikipédia, l'encyclopédie libre.
Sauter à la navigation Sauter à la recherche

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 (x² + bx + c = 0) est équivalente à la L-formule  dans la théorie, car dans cette théorie x² + 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[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

Critère 1[modifier | modifier le code]

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[modifier | modifier le code]

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 H2 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[modifier | modifier le code]

On montre que admet l’élimination des quantificateur 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 les formules atomiques du langage de ou les négations de formules du langage de . Comme si et seulement si pour un certain , est équivalente à une formule de la forme où les sont les formules atomiques du langage de ou les négations de formules du langage de .

Comme , , , et , on peut supposer que les Ai sont des formes:

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 des formes:.

Ainsi où les Ai sont de la forme xi=xj ou de la forme xi<xj, et les Aj sont de la forme x<xi ou de la forme xi<x.

On a que . Donc on a deux cas:

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

Sinon car l'ordre est dense, donc convient.

Critère 2[modifier | modifier le code]

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 la domaine de tel que .

Alors, admet l’élimination des quantificateurs.

Preuve[modifier | modifier le code]

Soit une L-formule sans quantificateur. Soient , deux modèles de , une sous-structure commune de et , et des éléments de . Par hypothèse, on a que si et seulement si . Ainsi il existe une L-formule sans quantificateur telle que . Et on conclut par le critère 1.

Exemple: DAG[modifier | modifier le code]

On montre que la théorie de groupe abélian 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 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: ;

;

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

est bien défini: Soient . 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[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

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'annaux 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 quantificqteur, éléments de la domaine de . Supposont qu'il existe élément de la domaine de tel que . Monstrons 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 i. 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 polynome de . est un polynome de . Donc il existe dans tels que . On a deux cas:

S'il existe un polynome non nul, alors comme on a pour tout i, 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[modifier | modifier le code]

Exemples de théories admettant l'élimination des quantificateurs :

Toutes ces théories sont donc modèle-complètes (en).

Conséquence[modifier | modifier le code]

Modèle-complèt[modifier | modifier le code]

Soit T une L-théorie admettant l'élimination des quantificateurs. Soient M,N deux modèles de T tels que M est une sous-structure de M. Soit F une L-formule et s une assignation des variables dans M. Par l'élimination des quantificateurs, il existe une L-formule sans quantificateur G qui est équivalente à F dans T. On a que M|=F[s] si et seulement si M|=G[s] et que N|=F[s] si et seulement si N|=G[s]. Comme l'injection canonique de M dans N est un homomorphisme injective et que G est une formule sans quantificateur, on a que M|=G[s] si et seulement si N|= G[s]. On conclut que M|=F[s] si et seulement si N|= F[s]. Donc M et N sont élémentairement équivalent. Ainsi T est modèle-complète.

Notes et références[modifier | modifier le code]

  1. (en) Philipp Rothmaler, Introduction to Model Theory, CRC Press, (lire en ligne), p. 141.
  2. (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).
  3. (en) Aaron R. Bradley et Zohar Manna, The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, (ISBN 978-3-540-74112-1).
  4. (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]).

Voir aussi[modifier | modifier le code]

Articles connexes[modifier | modifier le code]

Bibliographie[modifier | modifier le code]

  • 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 (ISBN 2-7056 5830-0)
  • 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