Un jeu combinatoire à deux joueurs joué sur une paire de structures relationnelles où un joueur (Spoiler) cherche à mettre en évidence une différence et l'autre (Duplicateur) cherche à préserver une quasi-isomorphie partielle ; l'existence d'une stratégie gagnante pour le Duplicateur en k tours caractérise l'indiscernabilité par les formules du premier ordre de rang quantificateur ≤ k.

Principe

Transformer l'indiscernabilité syntaxique (formules de rang quantificateur borné) en un dispositif opérationnel : chaque quantificateur devient un choix d'élément dans l'une ou l'autre structure, et les réponses maintiennent une relation aller-retour qui réalise des quasi-isomorphismes partiels.

Démonstration

Comparer deux graphes finis G et H : pour montrer qu'ils satisfont les mêmes phrases du premier ordre de rang ≤ 2, exhiber une stratégie du Duplicateur en deux tours qui associe toujours au sommet choisi par le Spoiler un sommet ayant les mêmes relations d'adjacence vis-à-vis des sommets déjà choisis ; une telle stratégie implique l'absence de formule FO de rang ≤ 2 qui les sépare.

Mauvaise application

Conclure qu'une victoire du Duplicateur pour un k fixé implique que les structures sont élémentairement équivalentes (c.-à-d. satisfont exactement les mêmes formules du premier ordre) — cela exige une victoire pour tout k fini, pas uniquement pour un k donné.

Conséquence

Fournit une méthode concrète pour prouver des résultats d'indéfinissabilité ou d'indiscernabilité, pour borner la puissance expressive de fragments du premier ordre et pour établir des minorations en construisant des stratégies gagnantes du Spoiler.

Inversion

Vu à l'inverse comme une construction aller-retour : au lieu d'un jeu, interpréter l'existence de stratégies du Duplicateur pour tout k comme un critère coinductif d'équivalence élémentaire ; inverser les rôles met l'accent sur les propriétés séparatrices plutôt que sur l'indiscernabilité.

Limite

S'applique au calcul des prédicats du premier ordre relationnel et à ses fragments de rang quantificateur fini ; il ne capture pas directement des extensions comme les logiques à point fixe, les logiques du second ordre ou les quantificateurs de cardinalité sans adaptations.

Tension sémantique

En tension avec les méthodes de bisimulation : les deux capturent l'indiscernabilité mais pour des fragments syntaxiques différents (Ehrenfeucht–Fraïssé pour le rang quantificateur FO, bisimulation pour les logiques modales/gardées) ; la confusion apparaît lorsqu'on tente d'utiliser l'une pour des propriétés natives de l'autre.

Synthèse

Le jeu d'Ehrenfeucht–Fraïssé concrétise la comparaison de structures en transformant l'alternance des quantificateurs en une suite de choix : une stratégie gagnante du Duplicateur jusqu'à k tours est le témoin combinatoire qu'aucune phrase du premier ordre de rang ≤ k ne distingue les deux structures.