Joc de Ehrenfeucht–Fraïssé

En la teoria de models, els jocs de Ehrenfeucht–Fraïssé (també cridats jocs back-and-forth) és una tècnica per a determinar si dos estructures són elementalmente equivalents. L'aplicació principal d'esta tècnica és per a provar la inexpresibilidad de certes propietats en llògica de primer orde. De fet, els jocs de Ehrenfeucht–Fraïssé proporcionen una metodologia completa per a provar resultats de inexpresibilidad en la llògica de primer orde. En eixe rol, estos jocs són d'especial importància en la teoria de models finitos i les seues aplicacions en informàtica (específicament Ordenador Aided Verificació i bases de senyes), ya que els jocs de Ehrenfeucht–Fraïssé són una de les poques tècniques de teoria de models que manté la seua validea en el context de models finitos. Atres tècniques àmpliament utilisades per a provar resultats de inexpresiblidad, com el teorema de compacidad, no és vàlida en models finitos.

Els jocs de Ehrenfeucht–Fraïssé també poden ser definits per a atres llògiques, com llògiques de punt fix i jocs pebble per a llògiques de variables finitas. Les extensions són prou potents per a caracterisar la definibilidad en llògica de segon orde existencial.

Idea principal

Per al joc es fixen dos estructures, i dos jugadors. Un dels jugadors vol mostrar que les dos estructures són diferents (cridat Spoiler), mentres que l'atre jugador vol mostrar que són similars segons llògica de primer orde (cridat Duplicator). El joc es juga en tandes i rondes. Una ronda procedix com seguix: Primer el primer jugador (Spoiler) tria qualsevol element d'una de les estructures, i l'atre jugador (Duplicator) tria un element de l'atra estructura. La tasca de Duplicator és sempre elegir un element que és «similar» al que Spoiler va triar. Duplicator gana si existix un isomorfisme entre els elements triats en les dos estructures diferents.

El joc dura una cantitat fixa de rondes $\gamma$ (un ordinal, pero normalment un número finito o $\omega$).

Definició

Supongam que tenim dos estructures $𝔄$ i $𝔅$, cada una sense símbols de funció i en el mateix conjunt de símbols de relació, i un número natural fixe n. Llavors podem definir el joc de Ehrenfeucht–Fraïssé $G_n(𝔄,𝔅)$ com un joc entre dos jugadors, Spoiler i Duplicator, jugat com seguix:

1. El primer jugador, Spoiler, elegix o un element $a_1$ de $𝔄$ o un element $b_1$ de $𝔅$.
2. Si Spoiler va elegir un element de $𝔄$, Duplicator elegix un membre $b_1$ de $𝔅$; d'una atra forma, Duplicator elegix un element $a_1$ de $𝔄$.
3. Spoiler elegix un element $a_2$ de $𝔄$ o un element $b_2$ de $𝔅$.
4. Duplicator elegix un element $a_2$ o $b_2$ en l'estructura sobre la que Spoiler no va elegir.
5. Spoiler i Duplicator cotinúan elegint elements de $𝔄$ i $𝔅$ per a $n-2$ passos més.${\displaystyle }$
6. Al final del joc, hem triat elements distints $a_1,\dots ,a_n$ de $𝔄$ i $b_1,\dots ,b_n$ de $𝔅$. Per lo tant tenim dos estructures en el conjunt $\{1,\dots ,n\}$, una induïda de $𝔄$ via el mapage de $i$ en $a_i$, i l'atra induïda de $𝔅$ via el mapage de $i$ en $b_i$.

Duplicator gana si estes estructures són isomorfas; Spoiler gana si no són.

Per a cada $n$ definim una relació $𝔄\stackrel{n}{\sim }𝔅$ si Duplicator guanya el joc a n rondes $G_n(𝔄,𝔅)$. Estes són totes les relacions d'equivalència en la classe d'estructures en els símbols de relació donats. L'intersecció de totes estes relacions és novament la relació d'equivalència $𝔄\sim 𝔅$.

És fàcil provar que si Duplicator guanya este joc per a tot n, o siga $𝔄\sim 𝔅$, llavors $𝔄$ i $𝔅$ són elementalmente equivalents. Si el conjunt de símbols de relació considerat és finito, el regrés també és certa.