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-vientModèle:Référence nécessaire) 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

Deux structures. La première est un graphe à 4 éléments (un carré). La seconde, à 6 éléments, est deux carrés adjacents.

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₁, le duplicateur est tenté de répondre par y₁, y₂, y₆ ou y₅, 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₁, le duplicateur répond par y₁, le spoiler choisit y₄, le duplicateur répond par x₄. Les éléments choisis dans la première structure sont déconnectés (il n'y a pas d'arête entre x₁ et x₄), de même pour ceux de la seconde structure. Le duplicateur gagne.
• le spoiler choisit x₁, le duplicateur répond par y₁, le spoiler choisit x₂, le duplicateur répond par y₃. Les éléments choisis dans la première structure sont connectés (il y a une arête entre x₁ et x₂), de même pour ceux de la seconde structure. Le duplicateur gagne.
• le spoiler choisit x₁, le duplicateur répond par y₁, le spoiler choisit x₂, le duplicateur répond par y₄. Les éléments choisis dans la première structure sont connectés (il y a une arête entre x₁ et x₂), 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 :

1. Le spoiler joue en premier et choisit un élément $a_1$ de $A$ ou un élément $b_1$ de $B$.
2. 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$.
3. Le spoiler choisit un élément $a_2$ de $A$ ou un élément $b_2$ de $B$.
4. Le duplicateur choisit un élément $a_2$ ou $b_2$ dans la structure que le spoiler n'a pas choisie.
5. Le spoiler et le duplicateur continuent de choisir des éléments dans $A$ et $B$ jusqu'à obtenir $n$ éléments chacun.
6. À 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 Modèle:Citation étrangère et Modèle:Citation étrangère 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

Modèle:Section vide ou incomplète 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	Modèle:Lien
logique existentielle du second ordre monadique	Jeu d'Ajtai-FaginModèle:Référence nécessaire
logique modale	Jeu de bissimilation

Bibliographie

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

• Modèle:Ouvrage.

• Modèle:Ouvrage.
• Modèle:Ouvrage — Chapitre 6
• Modèle:Ouvrage
• Modèle:Ouvrage
• Modèle:Lien web

• Un exemple consultable en ligne : Modèle:Lien web
• Six Lectures Ehrenfeucht-Fraïssé games at MATH EXPLORERS' CLUB, Cornell Department of Mathematics.

Articles connexes

• Complexité descriptive
• Théorie des bases de données
• Théorie des jeux
• Langage formel
• Calcul des prédicats