En la disciplina matemática de la teoría de modelos , el juego Ehrenfeucht-Fraïssé (también llamado juegos de ida y vuelta) es una técnica para determinar si dos estructuras son elementalmente equivalentes . La principal aplicación de los juegos de Ehrenfeucht-Fraïssé es probar 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 inexpresables para la lógica de primer orden . En este rol, 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 yteorí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 la compacidad , no funcionan en modelos finitos.
Los juegos similares a Ehrenfeucht – Fraïssé también se pueden definir para otras lógicas, como las lógicas de punto fijo [1] y los juegos de guijarros para lógicas de variables finitas; Las extensiones son lo suficientemente poderosas 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 diferentes, mientras que Spoiler quiere mostrar que son elementalmente equivalentes (satisfacen las mismas oraciones de primer orden ). El juego se juega rondas. Una ronda procede 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 que sea "similar" al que eligió 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 eventuales subestructuras elegidas entre las dos estructuras diferentes; de lo contrario, Spoiler gana.
El juego tiene una duración fija de pasos. (que es un ordinal, generalmente un número finito o ).
Definición
Supongamos que se nos dan dos estructuras y , cada uno 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é para ser un juego entre dos jugadores, Spoiler y Duplicator, jugado de la siguiente manera:
- El primer jugador, Spoiler, elige un miembro de o un miembro de .
- Si Spoiler eligió a un miembro de , Duplicator elige un miembro de ; de lo contrario, Duplicator elige un miembro de .
- Spoiler elige a un miembro de o un miembro de .
- El duplicador elige un elemento o en el modelo del que Spoiler no eligió.
- Spoiler y Duplicator continúan eligiendo miembros de y por más pasos.
- Al final del juego, hemos elegido elementos distintos de y de . Por lo tanto, tenemos dos estructuras en el set., uno inducido de a través del envío de mapas a , y el otro inducido de a través del envío de mapas a . El duplicador gana si estas estructuras son iguales; Spoiler gana si no es así.
Para cada n definimos una relaciónsi Duplicator gana el juego n -move. 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..
Equivalencia e inexpresable
Es fácil demostrar que si Duplicator gana este juego para todos los n finitos , es decir,, luego y son elementalmente equivalentes. Si el conjunto de símbolos de relación que se están considerando es finito, lo contrario también es cierto.
Si una propiedad es cierto de pero no es cierto de , pero y puede mostrarse equivalente proporcionando una estrategia ganadora para Duplicator, entonces esto muestra que es inexpresable en la lógica capturada por este juego. [ se necesita más explicación ]
Historia
El método de ida y vuelta utilizado en el juego 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 ) después de Heloise y Abelard , un esquema de nomenclatura introducido por Wilfrid Hodges en su libro Model Theory , o alternativamente Eva y Adam.
Otras lecturas
El capítulo 1 del texto de la 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] Un ejemplo sencillo del juego Ehrenfeucht – Fraïssé se da en una de las columnas MathTrek de Ivars Peterson. [8]
Las diapositivas de Phokion Kolaitis [9] y el capítulo del libro de Neil Immerman [10] sobre los juegos Ehrenfeucht – Fraïssé discuten aplicaciones en informática, la metodología para probar resultados de inexpresibilidad y varias pruebas simples de inexpresibilidad usando esta metodología.
Los juegos Ehrenfeucht – Fraïssé son la base para la operación 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
- ^ Bosse, Uwe (1993). "Un juego de Ehrenfeucht-Fraïssé para la lógica del punto fijo y la lógica del punto fijo estratificado" (PDF) . En Börger, Egon (ed.). Lógica de la informática: 6º Taller, CSL'92, San Miniato, Italia, 28 de septiembre - 2 de octubre de 1992. Artículos seleccionados . Apuntes de conferencias en informática. 702 . Springer-Verlag . págs. 100-114. doi : 10.1007 / 3-540-56992-8_8 . ISBN 3-540-56992-8. Zbl 0808.03024 .
- ^ Sur une nueva clasificación de sistemas de relaciones , Roland Fraïssé, Comptes Rendus 230 (1950), 1022-1024.
- ^ Sur quelques clasifications 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.
- ↑ Una aplicación de juegos al problema de completitud para teorías formalizadas , A. Ehrenfeucht, Fundamenta Mathematicae 49 (1961), 129-141.
- ^ Enciclopedia de filosofía de Stanford, entrada sobre lógica y juegos.
- ^ Un curso de teoría de modelos , Bruno Poizat, tr. Moses Klein, Nueva York: Springer-Verlag, 2000.
- ^ Ordenaciones lineales , Joseph G. Rosenstein, Nueva York: Academic Press, 1982.
- ^ Ejemplo del juego Ehrenfeucht-Fraïssé.
- ^ Curso sobre juegos combinatorios en teoría de modelos finitos por Phokion Kolaitis (archivo .ps)
- ^ 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 MATH EXPLORERS 'CLUB, Departamento de Matemáticas de Cornell.
- Modeloids I, Miroslav Benda, Transactions of the American Mathematical Society, vol. 250 (junio de 1979), págs.47 - 90 (44 páginas)