# Jeu d'Ehrenfeucht-Fraïssé

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, c'est-à-dire savoir si elles satisfont les mêmes énoncés de logique du premier ordre. Son nom provient des mathématiciens Andrzej Ehrenfeucht et Roland Fraïssé. 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.

## Principe

Le jeu d'Ehrenfeucht-Fraïssé se joue sur deux structures et entre deux joueurs appelés spoiler et duplicateur. La figure ci-contre montre deux structures. Le spoiler veut montrer que les deux structures sont différentes, alors que le duplicateur veut montrer qu'elles sont isomorphes. 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. Par exemple, si le spoiler choisit x$_1$, le duplicateur est tenté de répondre par y$_1$, y$_2$, y$_6$ ou y$_5$, mais a priori pas y3 (et y4) car y3 ne ressemble pas à un coin de carré.
Lorsque tous les tours sont joués, le duplicateur gagne si les éléments choisis dans la première structure forment une structure isomorphe à la restriction aux éléments choisis dans la seconde. Par exemple, si on joue deux tours, voici deux exemples de parties du jeu :
* le spoiler choisit x$_1$, le duplicateur répond par y$_1$, le spoiler choisit y$_4$, le duplicateur répond par x$_4$. Les éléments choisis dans la première structure sont déconnectés (il n'y a pas d'arête entre x$_1$ et x$_4$), de même pour ceux de la seconde structure. Le duplicateur gagne.
* le spoiler choisit x$_1$, le duplicateur répond par y$_1$, le spoiler choisit x$_2$, le duplicateur répond par y$_3$. Les éléments choisis dans la première structure sont connectés (il y a une arête entre x$_1$ et x$_2$), de même pour ceux de la seconde structure. Le duplicateur gagne.
* le spoiler choisit x$_1$, le duplicateur répond par y$_1$, le spoiler choisit x$_2$, le duplicateur répond par y$_4$. Les éléments choisis dans la première structure sont connectés (il y a une arête entre x$_1$ et x$_2$), mais pas dans la seconde structure. Le duplicateur a mal joué et perd.

## Description formelle

On suppose données deux structures $A$ et $B$, 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é $G_{n}(A,B)$ entre deux joueurs, le spoiler et le duplicateur, se joue comme suit :
* Le spoiler joue en premier et choisit un élément $a_{1}$ de $A$ ou un élément $b_{1}$ de $B$.
* Si le spoiler a pris un élément de $A$, le duplicateur choisit un élément $b_{1}$ de $B$; sinon, le duplicateur choisit un élément $a_{1}$ de $A$.
* Le spoiler choisit un élément $a_{2}$ de $A$ ou un élément $b_{2}$ de $B$.
* Le duplicateur choisit un élément $a_{2}$ ou $b_{2}$ dans la structure que le spoiler n'a pas choisie.
* Le spoiler et le duplicateur continuent de choisir des éléments dans $A$ et $B$ jusqu'à obtenir $n$ éléments chacun.
* À la fin du jeu, des éléments $a_{1},\dots ,a_{n}$ de $A$ et $b_{1},\dots ,b_{n}$ de $B$ ont été choisis. Le duplicateur gagne le jeu si l'application $a_{i}\to b_{i}$ est un isomorphisme partiel, et sinon c'est le spoiler qui gagne.
Pour chaque entier n, on définit la relation $A\sim _{n}B$ par la propriété que le duplicateur gagne le jeu $G_{n}(A,B)$ à n tours. Il est facile de prouver que si le duplicateur gagne pour tout n, alors $A$ et $B$ 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 $A\sim _{n}B$ si et seulement si $A$ et $B$ satisfont les mêmes formules du premier ordre de rang de quantificateurs au plus $n$. Ceci fournit un outil efficace pour prouver qu'une propriété $P$ n'est pas définissable en logique du premier ordre. Pour cela, on cherche deux familles $A_{n}$ et $B_{n}$ de structures telles que toutes les $A_{n}$ vérifient $P$ et aucune des $B_{n}$ ne la vérifie, et que $A_{n}\sim _{n}B_{n}$. Si on suppose que $P$ est exprimable par une formule de rang de quantificateurs au plus $n$ et que $A_{n}$ la vérifie, la structure $B_{n}$ ne la vérifie pas, en contradiction avec les faits que $A_{n}\sim _{n}B_{n}$.

## Historique

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 et dans sa thèse. Elle a été exprimée comme un jeu par Andrzej Ehrenfeucht. Les noms de « spoiler » et « duplicateur » sont dus à Joel Spencer. 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. Le problème de décider si le duplicateur gagne à un jeu de Ehrenfeucht-Fraïssé est PSPACE-complet.

## Extensions

On peut définir des variantes aux jeux d'Ehrenfeucht-Fraïssé pour caractériser la définissabilité dans d'autres logiques.
| Logique | Jeu associé |
| Logique du premier ordre | Jeu d'Ehrenfeucht-Fraïssé |
| Logiques de point fixe | |
| logiques à un nombre fini de variables | jeux à jetons (en) |
| logique existentielle du second ordre monadique | Jeu d'Ajtai-Fagin |
| logique modale | Jeu de bissimilation |