Juego de Ehrenfeucht–Fraïssé

En la teoría de modelos, los juegos de Ehrenfeucht–Fraïssé (también llamados juegos back-and-forth) es una técnica para determinar si dos estructuras son elementalmente equivalentes. La aplicación principal de esta técnica es para probar la inexpresibilidad de ciertas propiedades en lógica de primer orden. De hecho, los juegos de Ehrenfeucht–Fraïssé proporcionan una metodología completa para probar resultados de inexpresibilidad en la lógica de primer orden. Con ese rol, estos juegos son de especial importancia en la teoría de modelos finitos y sus aplicaciones en informática (específicamente Ordenador Aided Verificación y bases de datos), ya que los juegos de Ehrenfeucht–Fraïssé son uno de las pocas técnicas de teoría de modelos que mantiene su validez en el contexto de modelos finitos. Otras técnicas ampliamente utilizadas para probar resultados de inexpresiblidad, como el teorema de compacidad, no es válida en modelos finitos.

Los juegos de Ehrenfeucht–Fraïssé también pueden ser definidos para otras lógicas, como lógicas de punto fijo^[1] y juegos pebble para lógicas de variables finitas. Las extensiones son bastante potentes para caracterizar la definibilidad en lógica de segundo orden existencial.

Idea principal[editar]

Para el juego se fijan dos estructuras, y dos jugadores. Uno de los jugadores quiere mostrar que las dos estructuras son diferentes (llamado Spoiler), mientras que el otro jugador quiere mostrar que son similares según lógica de primer orden (llamado Duplicator). El juego se juega en turnos y rondas. Una ronda procede como sigue: Primero el primer jugador (Spoiler) escoge cualquier elemento de una de las estructuras, y el otro jugador (Duplicator) escoge un elemento de la otra estructura. La tarea de Duplicator es siempre elegir un elemento que es «similar» al que Spoiler escogió. Duplicator gana si existe un isomorfismo entre los elementos escogidos en las dos estructuras diferentes.

El juego dura una cantidad fija de rondas $\gamma$ (un ordinal, pero normalmente un número finito o $\omega$ ).

Definición[editar]

Supongamos que tenemos dos estructuras ${\mathfrak {A}}$ y ${\mathfrak {B}}$ , 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. Entonces podemos definir el juego de Ehrenfeucht–Fraïssé $\displaystyle G_{n}({\mathfrak {A}},{\mathfrak {B}})$ como un juego entre dos jugadores, Spoiler y Duplicator, jugado como sigue:

El primer jugador, Spoiler, elige o un elemento $a_{1}$ de ${\mathfrak {A}}$ o un elemento $b_{1}$ de $\displaystyle {\mathfrak {B}}$ .
Si Spoiler eligió un elemento de ${\mathfrak {A}}$ , Duplicator elige un miembro $b_{1}$ de ${\mathfrak {B}}$ ; de otra forma, Duplicator elige un elemento $a_{1}$ de ${\mathfrak {A}}$ .
Spoiler elige un elemento $a_{2}$ de ${\mathfrak {A}}$ o un elemento $b_{2}$ de ${\mathfrak {B}}$ .
Duplicator elige un elemento $a_{2}$ o $b_{2}$ en la estructura sobre la que Spoiler no eligió.
Spoiler y Duplicator cotinúan eligiendo elementos de ${\mathfrak {A}}$ y ${\mathfrak {B}}$ para $n-2$ pasos más.
Al final del juego, hemos escogido elementos distintos $a_{1},\dots ,a_{n}$ de ${\mathfrak {A}}$ y $b_{1},\dots ,b_{n}$ de ${\mathfrak {B}}$ . Por lo tanto tenemos dos estructuras en el conjunto $\{1,\dots ,n\}$ , una inducida de ${\mathfrak {A}}$ vía el mapeo de $\displaystyle i$ en $a_{i}$ , y la otra inducida de ${\mathfrak {B}}$ vía el mapeo de $i$ en $b_{i}$ .

Duplicator gana si estas estructuras son isomorfas; Spoiler gana si no son.

Para cada $n$ definimos una relación ${\mathfrak {A}}{\stackrel {n}{\sim }}{\mathfrak {B}}$ si Duplicator gana el juego a n rondas $\displaystyle G_{n}({\mathfrak {A}},{\mathfrak {B}})$ . Estas son todas las 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 la relación de equivalencia ${\mathfrak {A}}\sim {\mathfrak {B}}$ .

Es fácil probar que si Duplicator gana este juego para todo n, o sea ${\mathfrak {A}}\sim {\mathfrak {B}}$ , entonces ${\mathfrak {A}}$ y ${\mathfrak {B}}$ son elementalmente equivalentes. Si el conjunto de símbolos de relación considerado es finito, la vuelta también es cierta.

Historia[editar]

El método back-and-forth utilizado en los juegos de Ehrenfeucht–Fraïssé para verificar la equivalencia elemental fue dado por Roland Fraïssé en su tesis. Fue formulado como un juego por Andrzej Ehrenfeucht.^[2]^[3]^[4] Los nombres Spoiler y Duplicator se deben a Joel Spencer.^[5] Otros nombres habituales son Eloísa y Abelardo (a menudo denotados por $\exists$ y $\forall$ ) basados en Eloísa y Abelardo, un esquema de nombres introducido por Wilfrid Hodges en su libro Model Theory.

Otras lecturas[editar]

El capítulo 1 del libro de teoría de modelos de Poizat contiene una introducción a los juegos de Ehrenfeucht–Fraïssé, como así también los capítulos 6, 7, y 13 de libro de Rosenstein sobre órdenes lineales.^[6]^[7] Un ejemplo sencillo de los juegos de Ehrenfeucht–Fraïssé está dado en uno de las columnas de Ivars Peterson para MathTrek.^[8]

En las filminas de Phokion Kolaitis y en el capítulo del libro sobre juegos de Ehrenfeucht–Fraïssé de Neil Immerman se habla sobre las aplicaciones en informática, la metodología para probar resultados de inexpresibilidad y se dan ejemplos sencillos de pruebas de inexpresiblidad que utilizan esta metodología.^[9]^[10]

Referencias[editar]

↑ Bosse, Uwe (1993). «An Ehrenfeucht–Fraïssé game for fixpoint logic and stratified fixpoint logic». En Börger, Egon, ed. Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers. Lecture Notes in Computer Science 702. Springer-Verlag. pp. 100-114. ISBN 3-540-56992-8. Zbl 0808.03024.
↑ Sur une nouvelle classification des systèmes de relations, Roland Fraïssé, Comptes Rendus 230 (1950), 1022–1024.
↑ Sur quelques classifications des systèmes de relations, Roland Fraïssé, thesis, Paris, 1953; published in Publications Scientifiques de l'Université d'Alger, series A 1 (1954), 35–182.
↑ An application of games to the completeness problem for formalized theories, A. Ehrenfeucht, Fundamenta Mathematicae 49 (1961), 129–141.
↑ Stanford Encyclopedia of Philosophy, entry on Logic and Games.
↑ A Course in Model Theory, Bruno Poizat, tr.
↑ Linear Orderings, Joseph G. Rosenstein, New York: Academic Press, 1982.
↑ Example of the Ehrenfeucht-Fraïssé game.
↑ Course on combinatorial games in finite model theory by Phokion Kolaitis (.ps file).
↑ Neil Immerman (1999). Descriptive complexity. Springer. ISBN 978-0-387-98600-5.

Enlaces externos[editar]

Seis Conferencias Ehrenfeucht-Fraïssé juegos en Club de exploradores de matemáticas, Departamento de Matemáticas de Cornell.

Datos: Q1300013

[1] Bosse, Uwe (1993). «An Ehrenfeucht–Fraïssé game for fixpoint logic and stratified fixpoint logic». En Börger, Egon, ed. Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers. Lecture Notes in Computer Science 702. Springer-Verlag. pp. 100-114. 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é, thesis, Paris, 1953; published in Publications Scientifiques de l'Université d'Alger, series A 1 (1954), 35–182.

[4] An application of games to the completeness problem for formalized theories, A. Ehrenfeucht, Fundamenta Mathematicae 49 (1961), 129–141.

[5] Stanford Encyclopedia of Philosophy, entry on Logic and Games.

[6] A Course in Model Theory, Bruno Poizat, tr.

[7] Linear Orderings, Joseph G. Rosenstein, New York: Academic Press, 1982.

[8] Example of the Ehrenfeucht-Fraïssé game.

[9] Course on combinatorial games in finite model theory by Phokion Kolaitis (.ps file).

[Immerman1999-10] Neil Immerman (1999). Descriptive complexity. Springer. ISBN 978-0-387-98600-5.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]