Two Remarks about Game Semantics of Classical Logic

Resumo Técnico: Duas Observações sobre Semântica de Jogos da Lógica Clássica

Autor: Thierry Coquand
Contexto: Artigo dedicado a Stefano Berardi, explorando observações não publicadas deste último sobre semântica de jogos para a lógica clássica.

1. Problema e Contexto

O artigo aborda a semântica de jogos para a lógica clássica, especificamente no contexto do cálculo proposicional infinitário e da aritmética de Heyting (HAω) estendida. O problema central reside em entender como a validade clássica pode ser caracterizada através de estratégias de jogo que permitem o "backtracking" (retrocesso), e quais são as limitações dessa abordagem.

O autor revisita duas observações de Stefano Berardi que desafiam ou refinam a compreensão atual sobre:

1. A extensão natural das noções de "visões" (views) e debates para sequências de interação transfinitas.
2. A validade da motivação da semântica de realização (realizability) baseada em jogos, que, segundo Berardi, pode validar fórmulas falsas sob certas condições de continuidade.

2. Metodologia

O autor utiliza a semântica de jogos de informação perfeita entre dois jogadores:

• $\exists$loise (Existencial): Joga por fórmulas existenciais ($\bigvee$).
• $\forall$belard (Universal): Joga por fórmulas universais ($\bigwedge$).

A inovação chave em relação à lógica intuicionista é que $\exists$loise pode fazer "backtracking" (mudar de ideia e retroceder em suas escolhas anteriores). Isso modela o processo de eliminação de cortes (cut-elimination) na prova clássica.

A metodologia envolve:

• Definição de Sequências de Interação: Representação das jogadas como pares $(V, \phi)$, onde $V(n)$ é o conjunto de jogadas anteriores visíveis (a "visão") e $\phi(n)$ indica a qual jogada anterior a jogada atual responde.
• Análise de Estratégias: Construção de estratégias vencedoras para $\exists$loise em fórmulas clássicas, incluindo casos com funções e escolha enumerável.
• Contra-exemplos: Construção de cenários onde estratégias vencedoras existem para fórmulas logicamente falsas, testando os limites da semântica baseada em continuidade.

3. Contribuições e Resultados Chave

Primeira Observação: Extensão Transfinita de Debates

• Contexto: Em trabalhos anteriores [4, 5], provou-se que uma sequência infinita de interação implica a existência de uma subsequência infinita específica.
• Refinamento de Berardi: Berardi observou que é possível refinar esse resultado para garantir a unicidade de uma sequência infinita $n_k$ tal que $n_k + 1 = \phi(n_{k+1})$ e que essas segmentos formam uma partição de $[0, \omega[$.
• Significado Técnico:
  • A unicidade dessa sequência é crucial porque identifica exatamente qual dos dois jogadores é responsável por um debate infinito.
  • Isso permite definir uma "visão" no estágio $\omega$ ($V(\omega)$), permitindo estender a sequência de interação para ordinais transfinitos.
  • Se o debate é infinito, a paridade das jogadas indica quem "perdeu" (quem não pode mais avançar), formalizando a ideia de que um debate infinito é atribuído a um único jogador.

Segunda Observação: Falha da Continuidade na Realização

• Contexto: Em [2], foi proposta uma interpretação de realização modificada para HAω com escolha enumerável, baseada na ideia de que se $\forall$belard joga de forma "contínua" (usando apenas informação finita sobre a função atual), $\exists$loise eventualmente vence.
• O Contra-Exemplo (Fórmula Falsa): Berardi apresentou uma fórmula falsa em HAω:
  $$\bigvee_f \bigwedge_x \bigvee_y (f(x) = 0 \land f(y) \neq 0)$$
  Esta fórmula afirma que existe uma função $f$ que tem um zero e um não-zero. Embora falsa (pois nem toda função tem essa propriedade, ou mais precisamente, a interpretação lógica da fórmula é problemática no contexto clássico sem restrições adequadas), $\exists$loise possui uma estratégia vencedora contra qualquer oponente contínuo.
  • Estratégia de $\exists$loise: Ela começa com uma função constante $f_0 = 1$. Se $\forall$belard responder com $x_0$, ela atualiza a função para $f_1$ onde $f_1(0)=0$. Se $\forall$belard responder com $x_1 < 1$, ela vence. Caso contrário, ela atualiza novamente para $f_2$ onde $f_2(1)=0$, e assim sucessivamente.
  • O Paradoxo: Como $\forall$belard joga de forma contínua, ele eventualmente deve fornecer um $x_n < n$, permitindo que $\exists$loise vença. No entanto, a fórmula é falsa.
• Interação Infinita: Quando a estratégia vencedora de $\exists$loise para a fórmula falsa é confrontada com a estratégia vencedora para a negação da fórmula, gera-se um debate infinito. Isso demonstra que a eliminação de cortes não termina neste cenário.
• Conclusão da Observação: Argumentos baseados puramente em continuidade são insuficientes para caracterizar a semântica de realização. O fato de $\exists$loise vencer contra oponentes contínuos não garante que a fórmula seja verdadeira ou realizável no sentido construtivo clássico.

4. Significado e Implicações

• Limites da Semântica de Jogos: O trabalho mostra que a capacidade de um jogador vencer contra oponentes com recursos limitados (como continuidade ou recursão primitiva) não é suficiente para validar a verdade lógica de uma fórmula.
• Assimetria de Recursos: O artigo destaca que, se houver uma assimetria nos recursos computacionais entre os jogadores (ex: um jogador tem poder computacional superior), o jogador mais forte pode levar o outro a "acreditar" em uma afirmação falsa através de um jogo infinito. Isso é ilustrado pela comparação com o trabalho de Soloviev sobre a função de Ackermann.
• Refinamento da Teoria: A observação sobre a extensão transfinita oferece uma ferramenta mais precisa para analisar a estrutura de debates infinitos e a responsabilidade pela não-terminação, refinando a análise geométrica das sequências de interação.
• Homenagem: O trabalho serve como um tributo à intuição de Stefano Berardi, conectando suas observações não publicadas a desenvolvimentos recentes na teoria de tipos e semântica de jogos.

Em suma, Coquand utiliza as observações de Berardi para demonstrar que a semântica de jogos clássica, embora poderosa para modelar a eliminação de cortes, requer cuidados adicionais ao lidar com infinitos e continuidade, pois a vitória estratégica em jogos com restrições de informação não equivale necessariamente à validade lógica ou realizabilidade.