Juego de Ehrenfeucht-Fraïssé

En la disciplina matemática de la teoría de modelos , el juego de Ehrenfeucht-Fraïssé (también llamado juegos de ida y vuelta) es una técnica basada en la semántica de juegos para determinar si dos estructuras son elementalmente equivalentes . La principal aplicación de los juegos de Ehrenfeucht-Fraïssé es la de demostrar la inexpresabilidad de ciertas propiedades en la lógica de primer orden. De hecho, los juegos de Ehrenfeucht-Fraïssé proporcionan una metodología completa para demostrar resultados de inexpresabilidad para la lógica de primer orden . En este papel, estos juegos son de particular importancia en la teoría de modelos finitos y sus aplicaciones en la informática (específicamente la verificación asistida por computadora y la teoría de bases de datos ), ya que los juegos de Ehrenfeucht-Fraïssé son una de las pocas técnicas de la teoría de modelos que siguen siendo válidas en el contexto de los modelos finitos. Otras técnicas ampliamente utilizadas para demostrar resultados de inexpresabilidad, como el teorema de compacidad , no funcionan en modelos finitos.

También se pueden definir juegos de tipo Ehrenfeucht-Fraïssé para otras lógicas, como las lógicas de puntos fijos ^[1] y los juegos de guijarros para lógicas de variables finitas; las extensiones son lo suficientemente potentes como para caracterizar la definibilidad en la lógica existencial de segundo orden .

Idea principal

La idea principal del juego es que tenemos dos estructuras y dos jugadores: Spoiler y Duplicator . Duplicator quiere demostrar que las dos estructuras son elementalmente equivalentes (satisfacen las mismas oraciones de primer orden ), mientras que Spoiler quiere demostrar que son diferentes. El juego se juega en rondas. Una ronda se desarrolla de la siguiente manera: Spoiler elige cualquier elemento de una de las estructuras y Duplicator elige un elemento de la otra estructura. En términos simplificados, la tarea del Duplicator es elegir siempre un elemento "similar" al que ha elegido Spoiler, mientras que la tarea del Spoiler es elegir un elemento para el que no exista ningún elemento "similar" en la otra estructura. Duplicator gana si existe un isomorfismo entre las subestructuras eventuales elegidas de las dos estructuras diferentes; de lo contrario, gana Spoiler.

El juego dura un número fijo de pasos (que es un ordinal, normalmente un número finito o ). ${\displaystyle \gamma }$ ${\displaystyle \omega }$

Definición

Supongamos que se nos dan dos estructuras y , cada una sin símbolos de función y con el mismo conjunto de símbolos de relación , y un número natural fijo n . Podemos definir entonces el juego de Ehrenfeucht–Fraïssé como un juego entre dos jugadores, Spoiler y Duplicator, que se juega de la siguiente manera: ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle {\mathfrak {B}}}$ ${\displaystyle G_{n}({\mathfrak {A}},{\mathfrak {B}})}$

1. El primer jugador, Spoiler, elige un miembro de o un miembro de . ${\displaystyle a_{1}}$ ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle b_{1}}$ ${\displaystyle {\mathfrak {B}}}$
2. Si Spoiler eligió un miembro de , Duplicator eligió un miembro de ; de lo contrario, Duplicator eligió un miembro de . ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle b_{1}}$ ${\displaystyle {\mathfrak {B}}}$ ${\displaystyle a_{1}}$ ${\displaystyle {\mathfrak {A}}}$
3. Spoiler elige un miembro de o un miembro de . ${\displaystyle a_{2}}$ ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle b_{2}}$ ${\displaystyle {\mathfrak {B}}}$
4. Duplicator elige un elemento o en el modelo del cual Spoiler no eligió. ${\displaystyle a_{2}}$ ${\displaystyle b_{2}}$
5. Spoiler y Duplicator continúan eligiendo miembros de y para más pasos. ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle {\mathfrak {B}}}$ ${\displaystyle n-2}$
6. Al final del juego, hemos elegido elementos distintos de y de . Por lo tanto, tenemos dos estructuras en el conjunto , una inducida desde a través del mapa que envía a , y la otra inducida desde a través del mapa que envía a . Duplicator gana si estas estructuras son iguales; Spoiler gana si no lo son. ${\displaystyle a_{1},\dots ,a_{n}}$ ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle b_{1},\dots ,b_{n}}$ ${\displaystyle {\mathfrak {B}}}$ ${\displaystyle \{1,\dots ,n\}}$ ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle i}$ ${\displaystyle a_{i}}$ ${\displaystyle {\mathfrak {B}}}$ ${\displaystyle i}$ ${\displaystyle b_{i}}$

Para cada n definimos una relación si Duplicator gana el juego de n movimientos . Todas estas son relaciones de equivalencia en la clase de estructuras con los símbolos de relación dados. La intersección de todas estas relaciones es nuevamente una relación de equivalencia . ${\displaystyle {\mathfrak {A}}\ {\overset {n}{\sim }}\ {\mathfrak {B}}}$ ${\displaystyle G_{n}({\mathfrak {A}},{\mathfrak {B}})}$ ${\displaystyle {\mathfrak {A}}\sim {\mathfrak {B}}}$

Equivalencia e inexpresabilidad

Es fácil demostrar que si Duplicator gana este juego para todos los n finitos , es decir, , entonces y son elementalmente equivalentes. Si el conjunto de símbolos de relación que se considera es finito, la recíproca también es cierta. ${\displaystyle {\mathfrak {A}}\sim {\mathfrak {B}}}$ ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle {\mathfrak {B}}}$

Si una propiedad es verdadera para pero no verdadera para , pero y se puede demostrar que son equivalentes proporcionando una estrategia ganadora para Duplicator, entonces esto demuestra que es inexpresable en la lógica capturada por este juego. ^{[ se necesita más explicación ]} ${\displaystyle Q}$ ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle {\mathfrak {B}}}$ ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle {\mathfrak {B}}}$ ${\displaystyle Q}$

Historia

El método de ida y vuelta utilizado en el juego de Ehrenfeucht–Fraïssé para verificar la equivalencia elemental fue dado por Roland Fraïssé en su tesis; ^{[2] [3]} fue formulado como un juego por Andrzej Ehrenfeucht . ^[4] Los nombres Spoiler y Duplicator se deben a Joel Spencer . ^[5] Otros nombres habituales son Eloise [sic] y Abelard (y a menudo denotados por y ) en honor a Heloise y Abelard , un esquema de nombres introducido por Wilfrid Hodges en su libro Model Theory , o alternativamente Eva y Adán. ${\displaystyle \exists }$ ${\displaystyle \forall }$

Lectura adicional

El capítulo 1 del texto de teoría de modelos de Poizat ^[6] contiene una introducción al juego de Ehrenfeucht–Fraïssé, al igual que los capítulos 6, 7 y 13 del libro de Rosenstein sobre órdenes lineales . ^[7] Un ejemplo simple del juego de Ehrenfeucht–Fraïssé se da en una de las columnas de MathTrek de Ivars Peterson. ^[8]

Las diapositivas de Phokion Kolaitis ^[9] y el capítulo del libro de Neil Immerman ^[10] sobre los juegos de Ehrenfeucht–Fraïssé analizan las aplicaciones en informática, la metodología para demostrar resultados de inexpresabilidad y varias pruebas de inexpresabilidad simples utilizando esta metodología.

Los juegos de Ehrenfeucht-Fraïssé son la base para la operación de la derivada sobre los modeloides. Los modeloides son ciertas relaciones de equivalencia y la derivada permite una generalización de la teoría del modelo estándar.

Referencias

1. Bosse, Uwe (1993). "Un juego de Ehrenfeucht–Fraïssé para lógica de punto fijo y lógica de punto fijo estratificada" (PDF) . En Börger, Egon (ed.). Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italia, 28 de septiembre - 2 de octubre de 1992. Artículos seleccionados . Lecture Notes in Computer Science. Vol. 702. Springer-Verlag . págs. 100–114. doi :10.1007/3-540-56992-8_8. ISBN . 3-540-56992-8.Zbl 0808.03024  .
2. Sur une nouvelle Classification des systèmes de Relations , Roland Fraïssé, Comptes Rendus 230 (1950), 1022-1024.
3. Sur quelques Classifications des systèmes de Relations , Roland Fraïssé, tesis, París, 1953; publicado en Publications Scientifiques de l'Université d'Alger , serie A 1 (1954), 35–182.
4. Una aplicación de juegos al problema de completitud para teorías formalizadas, A. Ehrenfeucht, Fundamenta Mathematicae 49 (1961), 129–141.
5. Enciclopedia de Filosofía de Stanford, entrada sobre lógica y juegos.
6. Un curso de teoría de modelos , Bruno Poizat, trad. Moses Klein, Nueva York: Springer-Verlag, 2000.
7. Ordenamientos lineales , Joseph G. Rosenstein, Nueva York: Academic Press, 1982.
8. Ejemplo del juego Ehrenfeucht-Fraïssé.
9. Curso sobre juegos combinatorios en teoría de modelos finitos por Phokion Kolaitis (archivo .ps)
10. Neil Immerman (1999). "Capítulo 6: Juegos Ehrenfeucht-Fraïssé". Complejidad Descriptiva . Saltador. págs. 91-112. ISBN 978-0-387-98600-5.

• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel ; Vardi, Moshe Y .; Venema, Yde; Weinstein, Scott (2007). Teoría de modelos finitos y sus aplicaciones . Textos en informática teórica. Una serie EATCS. ​​Berlín: Springer-Verlag . ISBN. 978-3-540-00428-8.Zbl 1133.03001  .

Enlaces externos

• Seis conferencias sobre juegos de Ehrenfeucht-Fraïssé en el CLUB DE EXPLORADORES DE MATEMÁTICAS, Departamento de Matemáticas de Cornell.
• Modeloides I, Miroslav Benda, Transactions of the American Mathematical Society, vol. 250 (junio de 1979), págs. 47-90 (44 páginas)