Jeu d'Ehrenfeucht-Fraïssé

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

En logique mathématique, et notamment en théorie des modèles finis, le jeu d'Ehrenfeucht-Fraïssé  (aussi appelé jeu du va-et-vient) est une technique pour déterminer si deux structures sont élémentairement équivalentes. La principale application du jeu d'Ehrenfeucht-Fraïssé est de prouver que certaines propriétés ne sont pas exprimables en logique du premier ordre. Cet usage est d'une importance particulière en théorie des modèles finis et dans ses applications informatiques, comme en vérification de modèles et en théorie des bases de données, puisque les jeux d'Ehrenfeucht-Fraïssé sont l'une des rares techniques de la théorie des modèles qui restent valables dans le contexte de modèles finis. Les autres techniques de preuve pour prouver que des énoncés sont inexprimables, tels que le théorème de compacité, ne s'appliquent pas dans les modèles finis.

Des jeux d'Ehrenfeucht-Fraïssé peuvent également être définis pour d'autres logiques, comme des logiques de point fixe[1] et des jeux à jetons (en) pour des logiques à un nombre fini de variables ; ces extensions sont assez puissantes pour caractériser la définissabilité dans la logique existentielle du second ordre.

Principe[modifier | modifier le code]

Le jeu se joue sur deux structures et entre deux joueurs appelés spoiler et duplicateur. Le spoiler veut montrer que les deux structures sont différentes, alors que le duplicateur veut montrer qu'elles sont isomorphes (au sens de la logique du premier ordre). Le jeu est joué en un nombre fini de tours. Un tour se déroule comme suit : d'abord, le spoiler choisit un élément arbitraire de l'une des deux structures, et ensuite le duplicateur choisit un élément de l'autre structure. La tâche du duplicateur est de toujours choisir un élément qui est « similaire » à celui choisi par le spoiler. Le jeu comporte un nombre fini de tours. Le duplicateur gagne si les éléments choisis dans la premier structure forment une structure isomorphe à la restriction aux éléments choisis dans la seconde.

Description[modifier | modifier le code]

On suppose données deux structures et , sans symboles de fonction et avec le même ensemble de symboles de relation. On fixe un entier naturel n. Le jeu d'Ehrenfeucht-Fraïssé entre deux joueurs, le spoiler et le duplicateur, se joue comme suit :

  1. Le spoiler joue en premier et choisit un élément de ou un élément de .
  2. Si le spoiler a pris un élément de , le duplicateur choisit un élément de ; sinon, le duplicateur choisit un élément de .
  3. Le spoiler choisit un élément de ou un élément de .
  4. Le duplicateur choisit un élément ou dans la structure que le spoiler n'a pas choisie.
  5. Le spoiler et le duplicateur continuent de choisir des éléments dans et jusqu'à obtenir éléments chacun.
  6. À la fin du jeu, des éléments de et de ont été choisis. Le duplicateur gagne le jeu si l'application est un isomorphisme partiel, et sinon c'est le spoiler qui gagne.

Pour chaque entier n, on définit la relation par la propriété que le duplicateur gagne le jeu à n tours. Il est facile de prouver que si le duplicateur gagne pour tout n, alors et sont élémentairement équivalent. Si l'ensemble des symboles de relations est fini, la réciproque est également vraie.

L'importance du jeu réside dans le fait que si et seulement si et satisfont les mêmes formules du premier ordre de rang de quantificateurs au plus . Ceci fournit un outil efficace[2] pour prouver qu'une propriété n'est pas définissable en logique du premier ordre. Pour cela, on cherche deux familles et de structures telles que toutes les vérifient et aucune des ne la vérifie, et que . Si on suppose que est exprimable par une formule de rang de quantificateurs au plus et que la vérifie, la structure ne la vérifie pas, en contradiction avec les faits que .

Historique[modifier | modifier le code]

La méthode du va-et-vient utilisée dans le jeu d'Ehrenfeucht-Fraïssé pour vérifier l'équivalence élémentaire a été formulée par Roland Fraïssé dans une note aux Comptes rendus de l'Académie des sciences[3] et dans sa thèse[4]. Elle a été exprimée comme un jeu par Andrzej Ehrenfeucht[5]. Les noms de « spoiler » et « duplicateur » sont dus à Joel Spencer[6]. D'autres noms employés sont Éloise et Abélard (et souvent notés ∃ et ∀) d'après Héloïse et Abélard, une dénomination introduite par Wilfrid Hodges dans son livre Model Theory. Neil Immerman suggère « Samson » et « Delilah », avec les mêmes initiales.

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

  1. Uwe Bosse, « An Ehrenfeucht–Fraïssé game for fixpoint logic and stratified fixpoint logic », dans Egon Börger (éditeur), Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers, Springer-Verlag, coll. « Lecture Notes in Computer Science » (no 702), (ISBN 3-540-56992-8, zbMATH 0808.03024), p. 100-114.
  2. Libkin.
  3. « Sur une nouvelle classification des systèmes de relations », CRAS, vol. 230,‎ , p. 1022-1024 (lire en ligne).
  4. « Sur quelques classifications des systèmes de relations », Publications Scientifiques de l'Université d'Alger série A1,‎ , p. 35-182 — Thèse de doctorat, Université de Paris, 1953
  5. Andrzej Ehrenfeucht, « An application of games to the completeness problem for formalized theories », Fundamenta Mathematicae, vol. 49,‎ 1960/1961, p. 129-141.
  6. Stanford Encyclopedia of Philosophy, « Logic and Games ».
(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Ehrenfeucht–Fraïssé game » (voir la liste des auteurs).

Bibliographie[modifier | modifier le code]

Le jeu d'Ehrenfeucht-Fraïssé est exposé dans de nombreux manuels de référence, parmi lesquels il y a les suivants :

  • Joseph G. Rosenstein, Linear Orderings, Academic Press, , 487 p. (ISBN 9780125976800).

Articles connexes[modifier | modifier le code]