Jogo de Ehrenfeucht–Fraïssé: diferenças entre revisões

Na disciplina matemática da teoria dos modelos, o jogo de Ehrenfeucht–Fraïssé (também chamado de jogo de vai-e-voltavem) é uma técnica prapara 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 provideprovê 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 finitofinitos. Outra técnica para provar a inexpressibilidade de resultados é o [[teorema da compacidade]], que não funciona em modelos finitos.

A idéia 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 turnosjogadas 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.

e <math>\mathfrak{B}</math>, 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''. Nós podemosPodemos definir o jogo de Ehrenfeucht–Fraïssé <math>G_n(\mathfrak{A},\mathfrak{B})</math> para ser um jogo de dois participantes, Spoiler e Duplicador, jogado da seguinte maneira:

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é nãona sua tese;<ref>''Sur une nouvelle classification des systèmes de relations'', Roland Fraïssé, ''Comptes Rendus'' '''230''' (1950), 1022&ndash;1024.</ref><ref>''Sur quelques classifications des systèmes de relations'', Roland Fraïssé, thesis, Paris, 1953;

Capítulo 1 da teoria modalde moddelos de Poizat<ref>''A Course in Model Theory'', Bruno Poizat, tr. Moses Klein, New York: