Intuitionistic Common Knowledge

1. Formulação do Problema

O artigo aborda a lacuna na teoria da prova e na complexidade computacional da Lógica de Conhecimento Comum Intuicionista (ICK). Enquanto a lógica de Conhecimento Comum (CK) clássica é bem compreendida, sua contraparte intuicionista — introduzida por Jäger e Marti — carece de sistemas de prova totalmente analíticos e de métodos diretos para raciocínio automatizado.

• Contexto: A ICK estende a Lógica Proposicional Intuicionista (IPL) com modalidades de conhecimento ($K_a$) para múltiplos agentes e um operador de conhecimento comum ($C$) definido como um ponto fixo máximo.
• Limitações do Trabalho Existente: Sistemas anteriores baseavam-se em cálculos de sequentes não analíticos com regras de indução explícitas ou corte ilimitado, tornando a busca por provas automatizada difícil. Além disso, extensões para condições padrão de frames epistêmicos (S4 e S5) não haviam sido desenvolvidas sistematicamente, e a complexidade da verificação de validade permanecia em grande parte inexplorada (exceto para o caso geral, recentemente mostrado como completo em ExpTime).
• Objetivo: Fornecer axiomatizações sólidas e completas, cálculos de sequentes cíclicos analíticos e análise de complexidade para a ICK sobre classes de frames que satisfazem as condições de reflexividade, S4 e S5.

2. Metodologia

O autor emprega uma abordagem multifacetada combinando teoria da prova, teoria dos modelos e teoria dos jogos:

• Semântica: A lógica é interpretada sobre modelos de Kripke birelacionais consistindo em uma ordem parcial intuicionista ($\leq$) representando o crescimento da informação e relações de acessibilidade modal ($R_a$) para agentes. Uma restrição chave é a confluência triangular ($w \leq v \land v R_a u \implies w R_a u$), garantindo a persistência da verdade (monotonicidade) sob o crescimento da informação.
• Axiomatização: O artigo constrói sistemas estilo Hilbert para ICK, ICKT (reflexivo), ICKS4 e ICKS5. Esses sistemas são modulares, estendendo um sistema base com axiomas para reflexividade ($T_a$), introspecção positiva ($S4_a$) e introspecção negativa/classicidade ($S5_a$, $K^c_a$).
• Sistemas de Prova Cíclica: Para alcançar a analiticidade (onde todas as fórmulas em uma prova são subfórmulas da raiz), o autor introduz cálculos de sequentes cíclicos.
  • Esses cálculos permitem provas não bem-fundadas (árvores infinitas) que são então podadas em provas cíclicas finitas contendo arestas de retorno.
  • A correção é garantida por um critério global de correção (para provas não bem-fundadas) ou um critério local de correção (para provas cíclicas), exigindo que ramos infinitos passem pela expansão do conhecimento comum ($C$) infinitas vezes.
  • Para o caso S5, que se comporta classicamente em relação ao conhecimento, o sistema requer cortes analíticos (cortes restritos ao fechamento por negação da fórmula raiz) para manter a completude.
• Raciocínio Automatizado via Jogos de Paridade: O problema de busca por prova é reduzido à resolução de jogos de paridade.
  • Um jogo de dois jogadores é definido entre um Proponente (buscando uma prova) e um Refutador (buscando um contra-modelo).
  • Estratégias vencedoras para o Proponente correspondem a provas cíclicas.
  • O jogo é determinado sem memória, permitindo o uso de algoritmos eficientes para jogos de paridade para decidir a validade.
• Tradução: Uma variante modal da tradução de Kuroda é desenvolvida para incorporar a lógica clássica de Conhecimento Comum sobre S5 ($CKS5$) na $ICKS5$, estabelecendo uma redução em tempo polinomial.

3. Principais Contribuições

1. Extensão para Frames S4 e S5: O artigo estende sistematicamente a ICK para classes de frames reflexivos, S4 e S5, fornecendo axiomatizações estilo Hilbert sólidas e completas para cada uma.
2. Cálculos Cíclicos Analíticos: Introduz os primeiros cálculos de sequentes cíclicos analíticos para conhecimento comum intuicionista. Diferentemente de sistemas anteriores, estes eliminam a necessidade de regras de indução explícitas e corte ilimitado, garantindo que as provas sejam analíticas.
3. Automação da Busca por Prova: O artigo demonstra que a busca por prova nesses cálculos pode ser automatizada reduzindo o problema à resolução de jogos de paridade. Isso fornece um método algorítmico direto para construir provas ou encontrar contra-modelos.
4. Limites de Complexidade:
   • Estabelece que o problema de validade para todas as lógicas consideradas (ICK, ICKT, ICKS4, ICKS5) é solucionável em Tempo Exponencial (ExpTime).
   • Prova que o problema de validade para ICKS5 é completo em ExpTime fornecendo uma redução em tempo polinomial a partir da $CKS5$ clássica.
5. Propriedade do Modelo Finito: Através da construção de modelos canônicos finitos (usando teorias primas e fechamentos por negação), o artigo prova que todas as lógicas consideradas possuem a propriedade do modelo finito, implicando decidibilidade.

4. Principais Resultados

• Solidez e Completude: O artigo prova que as axiomatizações e os cálculos cíclicos são sólidos e completos em relação às suas respectivas classes de frames.
  • A completude para cálculos não bem-fundados é mostrada via um argumento de jogo de busca por prova (determinação de jogos de Gale-Stewart).
  • A completude para cálculos cíclicos é derivada traduzindo provas não bem-fundadas em provas cíclicas.
  • Para S5, a completude é estabelecida diretamente via construção de um modelo canônico com cortes analíticos.
• Propriedade da Disjunção: A Propriedade Semântica da Disjunção vale para ICK, ICKT e ICKS4 (se $\phi \lor \psi$ é válido, então $\phi$ ou $\psi$ é válido). No entanto, essa propriedade falha para ICKS5, pois o conhecimento em modelos S5 se comporta classicamente (ex: $K_a \phi \lor \neg K_a \phi$ é válido).
• Interpretação: O autor oferece uma interpretação da ICK como uma lógica para raciocinar sobre conhecimento sobre estados de informação em evolução.
  • Mundos representam estágios de crescimento da informação.
  • A reflexividade corresponde a agentes infalíveis (apenas provas corretas).
  • O S5 corresponde a agentes "hiper-céticos" que apenas confiam nas verdades mais básicas (tautologias lógicas) e desconfiam de qualquer nova informação que possa contradizer seu estado atual, levando a um comportamento clássico.
• Tradução: A tradução $tr(\phi)$ (prefixando fórmulas com $\neg\neg$ e após cada modalidade) incorpora com sucesso a $CKS5$ clássica na $ICKS5$, esclarecendo a relação entre as abordagens clássica e intuicionista.

5. Significado

• Avanço Teórico: Este trabalho preenche uma lacuna crítica na literatura ao fornecer os primeiros sistemas de prova totalmente analíticos para conhecimento comum intuicionista, permitindo uma compreensão mais profunda da estrutura da teoria da prova da lógica.
• Viabilidade Computacional: Ao reduzir a busca por prova a jogos de paridade, o artigo fornece um caminho concreto para a implementação de ferramentas de raciocínio automatizado para lógica epistêmica intuicionista, um campo anteriormente prejudicado por sistemas não analíticos.
• Classificação de Complexidade: Estabelecer a completude em ExpTime para ICKS5 coloca a lógica na mesma classe de complexidade que sua contraparte clássica, sugerindo que a natureza construtiva da lógica não aumenta inerentemente a dificuldade computacional para o caso S5.
• Direções Futuras: O framework abre caminhos para o estudo de extensões com co-implicação (lógica bi-intuicionista) para modelar perda de informação, e para a extração de interpolantes, que são cruciais para aplicações de representação e raciocínio de conhecimento (KRR).

Em resumo, o artigo de Zenger fornece uma fundação abrangente para o Conhecimento Comum Intuicionista, preenchendo a lacuna entre semântica construtiva e raciocínio automatizado através do uso inovador de provas cíclicas e jogos de paridade.