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

← Ver a alteração anterior Ver a alteração posterior →

Conteúdo apagado Conteúdo adicionado

Em linha

Revisão das 22h51min de 14 de março de 2014

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.

Idéia principal

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 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:

O primeiro jogador, Spoiler, pega tanto um membro $a_{1}$ de ${\mathfrak {A}}$ ou um membro $b_{1}$ de ${\mathfrak {B}}$ .
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}}$ .
Spoiler pega tanto um membro $a_{2}$ de ${\mathfrak {A}}$ ou um membro $b_{2}$ de ${\mathfrak {B}}$ .
Duplicador pega um elemento $a_{2}$ ou $b_{2}$ do modelo do qual Spoiler não pegou.
Spoiler e Duplicador continuam a pegar membros ${\mathfrak {A}}$ e ${\mathfrak {B}}$ por $n-2$ mais passos.
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;^[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

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]

References

↑ 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. Moses Klein, New York: Springer-Verlag, 2000.
↑ Linear Orderings, Joseph G. Rosenstein, New York: Academic Press, 1982.

External links

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

[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.

[1]

[2]

[3]

[4]

[5]

[6]

@@ Linha 1: / Linha 1: @@
-Na disciplina matemática da teoria dos modelos, o jogo de Ehrenfeucht–Fraïssé(também chamado de jogo de vai-e-volta) é uma técnica pra 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 provide 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 finito. Outra técnica para provar a inexpressibilidade de resultados é o [[teorema da compacidade]], que não funciona em modelos finitos.
+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.
 == Idéia principal ==
-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 turnos 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.
+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 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 (<math>\gamma</math>) (ordinal, mas geralmente finito ou <math>\omega</math>).
@@ Linha 8: / Linha 8: @@
 == Definição==
 Suponha que são dadas duas estruturas <math>\mathfrak{A}</math>
-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 podemos 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:
+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''. Podemos 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 primeiro jogador, Spoiler, pega tanto um membro <math>a_1</math> de <math>\mathfrak{A}</math> ou um membro <math>b_1</math> de <math>\mathfrak{B}</math>.
 # Se Spoiler pegou um membro de <math>\mathfrak{A}</math>, Duplicador pega um membro <math>b_1</math> de <math>\mathfrak{B}</math>; senão, Duplicador pega um membro <math>a_1</math> de <math>\mathfrak{A}</math>.
@@ Linha 19: / Linha 19: @@
 == 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é não 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;
+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;<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;
 published in ''Publications Scientifiques de l'Université d'Alger'', series A '''1''' (1954), 35&ndash;182.</ref>
 que foi formulada por um jogo por Andrzej Ehrenfeucht <ref>An application of games to the completeness problem for formalized theories, A. Ehrenfeucht, ''Fundamenta Mathematicae'' '''49''' (1961), 129&ndash;141.</ref> Os nomes Spoiler e Duplicador são devido a Joel Spencer.<ref>[http://plato.stanford.edu/entries/logic-games/ Stanford Encyclopedia of Philosophy, entry on Logic and Games.]</ref>.
@@ Linha 25: / Linha 25: @@
 == Mais leitura ==
-Capítulo 1 da teoria modal de Poizat<ref>''A Course in Model Theory'', Bruno Poizat, tr. Moses Klein, New York:
+Capítulo 1 da teoria de moddelos de Poizat<ref>''A Course in Model Theory'', Bruno Poizat, tr. Moses Klein, New York:
 Springer-Verlag, 2000.</ref> 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]].<ref>''Linear Orderings'', Joseph G. Rosenstein, New York: Academic Press, 1982.</ref>