A New Ehrenfeucht-Fraïssé Game for Dependence Logic

Resumo Técnico: Um Novo Jogo de Ehrenfeucht–Fraïssé para a Lógica de Dependência

Problema
A lógica de dependência ($D$) estende a lógica de primeira ordem ao adicionar átomos de dependência $=(\vec{x}, y)$, que afirmam que o valor de $y$ é funcionalmente determinado pelos valores de $\vec{x}$. A semântica de $D$ é tipicamente definida via semântica de equipes (teams), onde fórmulas são avaliadas sobre conjuntos de atribuições (equipes) em vez de uma única atribuição. Consequentemente, tentativas anteriores de definir um jogo de Ehrenfeucht–Fraïssé (EF) para a lógica de dependência, como a apresentada em [15], basearam-se em jogadas de "segunda ordem" onde os jogadores selecionam equipes inteiras ou conjuntos de atribuições. Os autores argumentam que, como as equipes podem ser massivas, essas jogadas são computacionalmente e conceitualmente complicadas. O artigo busca definir um jogo EF de "primeira ordem" para a lógica de dependência, onde as jogadas consistem em elementos únicos, de forma análoga ao jogo EF clássico para a lógica de primeira ordem, enquanto ainda captura o poder expressivo da lógica de dependência.

Metodologia
Os autores introduzem um novo jogo, denotado por $EF^{dep}_n(A, B)$, jogado entre duas estruturas $A$ e $B$. A metodologia envolve três componentes primários:

1. A Mecânica do Jogo:
   O jogo prossegue por $n$ rodadas. Em cada rodada $k$, o Jogador I (o sabotador/spoiler) seleciona um elemento $x_k$ de $A$ ou de $B$. Crucialmente, o Jogador I também deve declarar um conjunto de "compromissos de dependência" $W_k \subseteq \mathcal{P}(n)$ e conjuntos de fórmulas atômicas $U^+_k, U^-_k$.

   • Se um conjunto de índices $\{i_0, \dots, i_{k-1}\} \in W_k$, o Jogador I declara que a jogada atual $x_k$ é determinada unicamente pelas jogadas anteriores feitas no mesmo modelo (isto é, $x_k$ depende apenas de $\{x_{i_0}, \dots, x_{i_{k-1}}\}$ se $x_k \in A$, ou dos elementos correspondentes em $B$).
   • O Jogador II (o duplicador/duplicator) responde com um elemento $y_k$ da estrutura oposta.
   • A condição de vitória para o Jogador II em uma única partida não é baseada nos compromissos; em vez disso, os compromissos são apenas avaliados ao considerar múltiplas partidas simultaneamente.

2. Estratégias de Vitória Uniforme:
   A inovação central é a definição de uma estratégia de vitória uniforme para o Jogador II. Uma estratégia é uniformemente vencedora se, sempre que o Jogador I jogar de forma consistente (isto é, fizer os mesmos compromissos e satisfizer as mesmas fórmulas atômicas através de múltiplas partidas), as respostas do Jogador II respeitarem as dependências declaradas. Especificamente, se as jogadas do Jogador I em duas partidas diferentes forem idênticas nos índices declarados em $W_k$, as respostas do Jogador II também devem ser idênticas. Este mecanismo permite que o jogo capture a natureza funcional dos átomos de dependência sem exigir que os jogadores selecionem equipes inteiras.

3. Jogo Auxiliar e Equivalência:
   Para provar o resultado de caracterização, os autores introduzem um jogo auxiliar, $EFD_n((A, X), (B, Y))$, baseado em equipes indexadas. Este jogo é uma modificação do jogo em [15], mas utiliza funções suplementares (que definem como as equipes são expandidas) como jogadas, em vez de equipes propriamente ditas. Os autores estabelecem uma ponte entre os dois jogos:

   • Eles mostram que, se o Jogador II possui uma estratégia vencedora no jogo auxiliar $EFD_n$, ela possui uma estratégia de vitória uniforme no novo jogo $EF^{dep}_n$.
   • Eles provam que a existência de uma estratégia de vitória uniforme em $EF^{dep}_n(A, B)$ é equivalente à preservação da verdade de $A$ para $B$ para todas as sentenças de lógica de dependência de rank de quantificadores $\le n$.

Principais Contribuições e Resultados

• Definição de $EF^{dep}_n(A, B)$: O artigo define um novo jogo EF onde as jogadas são elementos únicos, não equipes. Isso resolve a complexidade das jogadas de "segunda ordem" encontradas em formulações anteriores.
• Condição de Uniformidade: O papel introduz o conceito de uma "estratégia de vitória uniforme", que impõe que as respostas do Jogador II devem respeitar as dependências funcionais declaradas pelo Jogador I através de múltiplas partidas.
• Teorema de Caracterização: O principal resultado (Teorema 6.1) estabelece que, para quaisquer duas estruturas $A$ e $B$, o Jogador II possui uma estratégia de vitória uniforme em $EF^{dep}_n(A, B)$ para todo $n$ se, e somente se, $A$ e $B$ são elementarmente equivalentes na lógica de dependência ($A \equiv_D B$).
• Redução para Jogadas de Primeira Ordem: Os autores demonstram que, apesar da natureza de "segunda ordem" da semântica da lógica de dependência, o jogo pode ser jogado com jogadas de primeira ordem, desde que a estratégia satisfaça a condição de uniformidade.

Significância e Alegações
O artigo afirma fornecer uma caracterização de "primeira ordem" da equivalência elementar na lógica de dependência, espelhando o resultado clássico para a lógica de primeira ordem. A significância reside na simplificação da análise via jogo da lógica de dependência, evitando a manipulação de grandes equipes durante o jogo.

Os autores são modestos quanto ao escopo de seus resultados. Eles observam que:

• A prova do resultado principal depende de uma forma normal específica para sentenças de lógica de dependência (Teorema 2.5), a qual reconhecem ser um tanto insatisfatória, pois desconecta o comprimento do jogo diretamente do rank de quantificadores de fórmulas arbitrárias.
• Os resultados dependem fortemente da fechamento descendente (downward closedness) da lógica de dependência (Fato 2.3). Consequentemente, os autores afirmam que estes resultados não podem ser imediatamente transferidos para outras lógicas de equipe que carecem dessa propriedade, como a lógica de inclusão ou a lógica de independência.
• Sugere-se que trabalhos futuros explorem se jogos semelhantes podem ser construídos para a lógica de inclusão e para a lógica de independência, e investiguem se o comprimento do jogo pode ser conectado de forma mais estreita ao rank de quantificadores sem depender de formas normais.

O artigo não propõe novas aplicações ou propostas experimentais, mas foca estritamente na caracterização teórica da lógica de dependência via semântica de jogo.