Juego 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 demostrar la inexpresabilidad de ciertas propiedades en lógica de primer orden. De hecho, los juegos de Ehrenfeucht-Fraïssé proporcionan una metodología completa para demostrar resultados de inexpresibilidad 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 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 modelos finitos. Otras técnicas ampliamente utilizadas para demostrar resultados de inexpresibilidad, como el teorema de compacidad , no funcionan en modelos finitos.

Los juegos tipo Ehrenfeucht-Fraïssé también se pueden definir para otras lógicas, como la lógica de punto fijo ^[1] y los juegos de guijarros para lógicas de variables finitas; Las extensiones son lo suficientemente poderosas como para caracterizar la definibilidad en la lógica existencial de segundo orden .

Idea principal

La idea principal detrás del juego es que tenemos dos estructuras y dos jugadores: Spoiler y Duplicator . Duplicator quiere mostrar que las dos estructuras son elementalmente equivalentes (satisfacen las mismas oraciones de primer orden ), mientras que Spoiler quiere mostrar que son diferentes. El juego se juega por 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 Duplicador es elegir siempre un elemento "similar" al que ha elegido el Spoiler, mientras que la tarea del Spoiler es elegir un elemento para el cual no existe ningún elemento "similar" en la otra estructura. El duplicador gana si existe un isomorfismo entre las subestructuras eventuales elegidas entre 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 tenemos dos estructuras y , cada una sin símbolos de función y el mismo conjunto de símbolos de relación , y un número natural fijo n . Entonces podemos definir el juego 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 elige un miembro de ; de lo contrario, Duplicator elige 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 finalizar el juego, hemos elegido distintos elementos de y de . Por lo tanto, tenemos dos estructuras en el conjunto , una inducida a través del envío del mapa a y la otra inducida a través del envío del mapa a . El duplicador gana si estas estructuras son iguales; El 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 el Duplicador 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 consideran es finito, lo contrario también es cierto. ${\displaystyle {\mathfrak {A}}\sim {\mathfrak {B}}}$ ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle {\mathfrak {B}}}$

Si una propiedad es cierta pero no cierta , pero se puede demostrar que y es equivalente 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

Roland Fraïssé presentó en su tesis el método de ida y vuelta utilizado en el juego Ehrenfeucht-Fraïssé para verificar la equivalencia elemental; ^{[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 ) después de Heloise y Abelard , un esquema de nomenclatura introducido por Wilfrid Hodges en su libro Model Theory , o alternativamente Eva y Adán. ${\displaystyle \exists }$ ${\displaystyle \forall }$

Otras lecturas

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

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

Los juegos de Ehrenfeucht-Fraïssé son la base para el funcionamiento de derivadas en modeloides. Los modeloides son ciertas relaciones de equivalencia y la derivada proporciona una generalización de la teoría de modelos estándar.

Referencias

1. Bosse, Uwe (1993). "Un juego de Ehrenfeucht-Fraïssé para lógica de puntos fijos y lógica de puntos fijos estratificada" (PDF) . En Börger, Egon (ed.). Lógica informática: sexto taller, CSL'92, San Miniato, Italia, 28 de septiembre - 2 de octubre de 1992. Artículos seleccionados . Apuntes de conferencias sobre informática. 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 de 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, tr. 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; Kolaítis, Phokion G.; Libkin, Leonid; Martín, Marx; Spencer, Joel ; Vardi, Moshe Y .; Venema, Ydé; Weinstein, Scott (2007). Teoría de modelos finitos y sus aplicaciones . Textos de 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 MATH EXPLORERS' CLUB, Departamento de Matemáticas de Cornell.
• Modeloides I, Miroslav Benda, Transacciones de la Sociedad Matemática Estadounidense, vol. 250 (junio de 1979), págs. 47 - 90 (44 páginas)