É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éfinitionsModifier

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 quantificateursModifier

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 quantificateursModifier

Critère 1Modifier

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.

PreuveModifier

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: DLOModifier

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 2Modifier

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.

PreuveModifier

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: DAGModifier

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 3Modifier

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.

PreuveModifier

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 closModifier

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  . 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 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  .

ExemplesModifier

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

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

ConséquenceModifier

Modèle-complétudeModifier

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érencesModifier

  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, Berlin, Springer, , 366 p. (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 aussiModifier

Articles connexesModifier

BibliographieModifier

  • 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