Jogo de Ehrenfeucht–Fraïssé

Na disciplina matemática da teoria dos modelos, o jogo de Ehrenfeucht–Fraïssé (também chamado de jogo de vai-e-vem) é uma técnica para determinar se duas estruturas são elementarmente equivalentes. A principal aplicação dos jogos de Ehrenfeucht–Fraïssé são provar a inexpressibilidade de certas propriedades da lógica de primeira ordem. De fato, essa técnica provê uma completa metodologia para provar resultados inexpressíveis para lógica de primeira ordem. Nesse papel, estes jogos são de importância particular para a teoria dos modelos finitos e aplicações na ciência da computação (especialmente bancos de dados), desde que os jogos de Ehrenfeucht–Fraïssé são umas das poucas técnicas da teoria dos modelos que permanecem válidas para um contexto de modelos finitos. Outra técnica para provar a inexpressibilidade de resultados é o teorema da compacidade, que não funciona em modelos finitos.

Ideia principal

A ideia principal por trás do jogo é que temos duas estruturas e dois jogadores (descritos abaixo). Um dos jogadores quer mostrar que as duas estruturas são diferentes, enquanto o outro jogador quer mostrar que elas são similares (de acordo com a lógica de primeira ordem). O jogo é jogado em jogadas e rodadas, uma rodada procede da seguinte forma: o primeiro jogador (Spoiler) escolhe um elemento de uma das estruturas, e o outro jogador (Duplicador) escolhe um elemento da outra estrutura. O objetivo do Duplicador é sempre pegar um elemento que é similar ao que ele já pegou. O segundo jogador ganha se houve isomorfismo entre os elementos escolhidos de duas estruturas.

O jogo dura por um número fixo de passos ($\gamma$) (ordinal, mas geralmente finito ou $\omega$).

Definição

Suponha que são dadas duas estruturas ${\mathfrak {A}}$ e ${\mathfrak {B}}$, cada uma sem nenhum símbolo de função e o mesmo número de símbolos de relação e um número fixo n. Podemos definir o jogo de Ehrenfeucht–Fraïssé $G_{n}({\mathfrak {A}},{\mathfrak {B}})$ para ser um jogo de dois participantes, Spoiler e Duplicador, jogado da seguinte maneira:

1. O primeiro jogador, Spoiler, pega tanto um membro $a_{1}$ de ${\mathfrak {A}}$ ou um membro $b_{1}$ de ${\mathfrak {B}}$.
2. Se Spoiler pegou um membro de ${\mathfrak {A}}$, Duplicador pega um membro $b_{1}$ de ${\mathfrak {B}}$; senão, Duplicador pega um membro $a_{1}$ de ${\mathfrak {A}}$.
3. Spoiler pega tanto um membro $a_{2}$ de ${\mathfrak {A}}$ ou um membro $b_{2}$ de ${\mathfrak {B}}$.
4. Duplicador pega um elemento $a_{2}$ ou $b_{2}$ do modelo do qual Spoiler não pegou.
5. Spoiler e Duplicador continuam a pegar membros ${\mathfrak {A}}$ e ${\mathfrak {B}}$ por $n-2$ mais passos.
6. Na conclusão do jogo, nós temos pego elementos distindos $a_{1},\dots ,a_{n}$ de ${\mathfrak {A}}$ e $b_{1},\dots ,b_{n}$ de ${\mathfrak {B}}$. Nós então temos duas estruturas na forma $\{1,\dots ,n\}$, uma induzida de ${\mathfrak {A}}$ via o mapa enviado $i$ para $a_{i}$, e outro induzido de ${\mathfrak {B}}$ via o enviado $i$ para $b_{i}$. Duplicador ganha se as estruturas são as mesmas; Spoiler ganha se não forem.

É fácil prover que se Duplicador ganha todos os jogos para todos n, então ${\mathfrak {A}}$ e ${\mathfrak {B}}$ são elementarmente equivalentes. Se um conjunto de símbolos de relações começa a ser considerado finito, o oposto também é verdade.

História

O método de ida e volta usado nos jogos de Ehrenfeucht–Fraïssé verificam a elementaridade da equivalência dada por Roland Fraïssé na sua tese; que foi formulada por um jogo por Andrzej Ehrenfeucht Os nomes Spoiler e Duplicador são devido a Joel Spencer..

Mais leitura

Capítulo 1 da teoria de moddelos de Poizat contém os jogos de Ehrenfeucht–Fraïssé , assim como o capítulo 6,7, 13 do livro de Rosenstein's em relação de ordem.

Ligações externas

• Six Lectures Ehrenfeucht-Fraïssé gamesat MATH EXPLORERS' CLUB, Cornell Department of Mathematics.