Un juego combinatorio de dos jugadores sobre un par de estructuras relacionales en el que un jugador (Spoiler) intenta mostrar una diferencia y el otro (Duplicator) intenta preservar una casi-isomorfía parcial; la existencia de una estrategia ganadora para Duplicator en k rondas caracteriza la indistinguibilidad por fórmulas de primer orden de rango de cuantificadores ≤ k.

Principio

Traducir la indistinguibilidad sintáctica (fórmulas con rango de cuantificador acotado) a un dispositivo operativo: cada cuantificador corresponde a elegir un elemento en una de las estructuras y las jugadas de respuesta mantienen una relación de ida y vuelta que realiza quasi-isomorfías parciales.

Demostración

Comparar dos grafos finitos G y H: para mostrar que concuerdan en todas las oraciones de primer orden de rango ≤ 2, exhibir una estrategia de Duplicator para dos rondas que siempre asigne al vértice elegido por Spoiler un vértice con las mismas relaciones de adyacencia respecto a los vértices ya elegidos; tal estrategia implica que no existe una fórmula FO de rango ≤ 2 que los separe.

Aplicación incorrecta

Concluir que una victoria de Duplicator para un k fijo implica que las estructuras son elementarmente equivalentes — eso requiere una victoria para cada k finito, no solo para uno.

Consecuencia

Proporciona un método concreto para probar resultados de indefinibilidad o indistinguibilidad, para acotar la expresividad de fragmentos de FO y para derivar cotas inferiores mediante la construcción de estrategias ganadoras de Spoiler.

Inversión

Visto al revés como una construcción de ida y vuelta: en lugar de un juego, interpretar la existencia de estrategias de Duplicator para todo k como un criterio coinductivo de equivalencia elemental; invertir roles pone el foco en propiedades distinguidoras en vez de indistinguibilidad.

Límite

Se aplica a la lógica de primer orden relacional y a sus fragmentos de rango de cuantificador finito; no captura directamente extensiones como lógicas de punto fijo, lógicas de orden superior o cuantificadores de cardinalidad sin adaptaciones.

Tensión semántica

En tensión con métodos de bisimulación: ambos capturan indistinguibilidad pero para fragmentos sintácticos distintos (Ehrenfeucht–Fraïssé para el rango de cuantificadores de FO, bisimulación para fragmentos modales/guardados); confundirlos conduce a errores de aplicación.

Síntesis

El juego de Ehrenfeucht–Fraïssé convierte la alternancia de cuantificadores en una sucesión de elecciones concretas: una estrategia ganadora de Duplicator hasta k rondas es el testimonio combinatorio de que ninguna fórmula FO de rango ≤ k distingue las dos estructuras.