Jogo de Ehrenfeucht–Fraïssé

Origem: Wikipédia, a enciclopédia livre.
Saltar para a navegação Saltar para a pesquisa

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[editar | editar código-fonte]

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 () (ordinal, mas geralmente finito ou ).

Definição[editar | editar código-fonte]

Suponha que são dadas duas estruturas e , 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é para ser um jogo de dois participantes, Spoiler e Duplicador, jogado da seguinte maneira:

  1. O primeiro jogador, Spoiler, pega tanto um membro de ou um membro de .
  2. Se Spoiler pegou um membro de , Duplicador pega um membro de ; senão, Duplicador pega um membro de .
  3. Spoiler pega tanto um membro de ou um membro de .
  4. Duplicador pega um elemento ou do modelo do qual Spoiler não pegou.
  5. Spoiler e Duplicador continuam a pegar membros e por mais passos.
  6. Na conclusão do jogo, nós temos pego elementos distindos de e de . Nós então temos duas estruturas na forma , uma induzida de via o mapa enviado para , e outro induzido de via o enviado para . 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 e 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[editar | editar código-fonte]

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;[1][2] que foi formulada por um jogo por Andrzej Ehrenfeucht [3] Os nomes Spoiler e Duplicador são devido a Joel Spencer.[4].

Mais leitura[editar | editar código-fonte]

Capítulo 1 da teoria de moddelos de Poizat[5] 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.[6]

Referências

  1. Sur une nouvelle classification des systèmes de relations, Roland Fraïssé, Comptes Rendus 230 (1950), 1022–1024.
  2. 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.
  3. An application of games to the completeness problem for formalized theories, A. Ehrenfeucht, Fundamenta Mathematicae 49 (1961), 129–141.
  4. Stanford Encyclopedia of Philosophy, entry on Logic and Games.
  5. A Course in Model Theory, Bruno Poizat, tr. Moses Klein, New York: Springer-Verlag, 2000.
  6. Linear Orderings, Joseph G. Rosenstein, New York: Academic Press, 1982.

Ligações externas[editar | editar código-fonte]