Knowing-Value Logic with Successor Arithmetic

Resumo Técnico: Lógica de Valor-Conhecimento com Aritmética de Sucessor

Problema
Este artigo aborda as limitações das existentes lógicas de "valor-conhecimento", especificamente a lógica de valor-conhecimento condicional ($ELKvr$) e sua extensão de anúncio público ($PALKvr$) propostas por Wang e Fan. Embora esses sistemas formalizem afirmações como "O agente $i$ conhece o valor de $c$ dado $\phi$", eles carecem da maquinaria sintática para lidar diretamente com operações aritméticas e igualdade. Consequentemente, não conseguem capturar a estrutura interna de proposições que envolvem números, como a relação entre inteiros consecutivos. Em cenários de linguagem natural e enigmas de lógica (ex: o enigma "Números Consecutivos"), o raciocínio frequentemente depende da interação entre operadores epistêmicos, igualdade e funções aritméticas (especificamente a função sucessor). Os frameworks existentes tratam condições numéricas como letras proposicionais opacas, falhando em derivar implicações que são óbvias na linguagem natural (ex: que saber que um número tem 4 dígitos e saber a implicação "se é de 4 dígitos, então é 1111" deve acarretar saber que o valor é 1111). Além disso, a semântica padrão para essas lógicas, baseada em conjuntos não estruturados de objetos, é insuficiente para modelar estruturas matemáticas específicas como os números naturais com uma função sucessor.

Metodologia
O autor introduz uma nova lógica, $ELKvSAr$ (o fragmento sem anúncios de $PALKvSAr$), que estende a lógica de valor-conhecimento condicional com:

1. Termos: Incluindo uma constante rígida $0$, constantes não-rígidas $C$, e a função sucessor $S$.
2. Fórmulas Atômicas: Igualdade entre termos ($t_1 \approx t_2$).
3. Semântica: O artigo define duas classes distintas de modelos:
   • Modelos Padrão: Baseados nos números naturais padrão $(\mathbb{N}, S)$.
   • Modelos Não-Padrão: Baseados em um modelo não-padrão específico de aritmética de sucessor $(\mathbb{N}^\star, S^\star)$, onde $\mathbb{N}^\star$ inclui os números naturais padrão mais infinitas "cadeias-Z" (cópias dos inteiros). Esta extensão é necessária porque a lógica não é compacta sobre a classe de modelos padrão.

A abordagem técnica envolve:

• Axiomatização: Propor o sistema $ELKVSAr$, que inclui axiomas para igualdade, aritmética de sucessor (ex: $\neg Sx \approx 0$, injetividade de $S$), e axiomas/regras específicos que fazem a ponte entre valor-conhecimento e aritmética (ex: $KvrS$, $KVE1$, $KVE2$). Uma característica fundamental é a regra $Kvr$-Elim, que funciona analogamente à eliminação do existencial na lógica de primeira ordem, permitindo a remoção de operadores de valor-conhecimento relativizados durante a derivação.
• Prova de Completude: Provar a completude forte em relação a modelos não-padrão. A prova utiliza uma construção inovadora de um quadro do tipo árvore (tree-like canonical frame) em vez de um modelo canônico padrão. Isso envolve a construção de histórias de conjuntos consistentes máximos e a definição de uma função de valoração que mapeia constantes para elementos em $\mathbb{N}^\star$ enquanto respeita as relações de equivalência induzidas pelo operador de valor-conhecimento e pela estrutura aritmética.
• Propriedade do Modelo Finito e Decidibilidade: Demonstrar que qualquer fórmula satisfatível possui um modelo não-padrão finito, que pode então ser mapeado para um modelo padrão finito via uma aplicação injetiva que preserva distâncias aritméticas e separa componentes. Isso estabelece a propriedade do modelo finito e a decidibilidade.
• Aplicação: Formalizar o enigma "Números Consecutivos" usando operadores de anúncio público ($PALKvSAr$) para mostrar como o conhecimento dos agentes evolui através de deduções aritméticas.

Principais Contribuições e Resultados

1. Extensão da Lógica: A introdução de $ELKvSAr$e$PALKvSAr$, integrando igualdade e a função sucessor à lógica de valor-conhecimento condicional.
2. Sistema Axiomático: A definição de $ELKVSAr$, que é provado ser:
   • Fortemente completo em relação à classe de modelos não-padrão.
   • Fracamente completo em relação à classe de modelos padrão.
3. Propriedades Meta-lógicas:
   • Propriedade do Modelo Finito (PMF): A lógica possui a PMF em relação a modelos tanto padrão quanto não-padrão.
   • Decidibilidade: O problema de satisfatibilidade para $ELKvSAr$ é decidível.
4. Não-Compactação: O artigo prova que $ELKvSAr$ não é compacta em relação a modelos padrão, motivando a introdução de modelos não-padrão para a prova de completude.
5. Solução do Enigma: O enigma "Números Consecutivos" é formalizado e resolvido com sucesso dentro do sistema, demonstrando que a lógica pode capturar a eliminação passo a passo de possibilidades baseadas em restrições aritméticas e atualizações epistêmicas.

Significância
O artigo afirma fornecer um novo framework para integrar a lógica epistêmica com a aritmética. Ao enriquecer a lógica de valor-conhecimento com a função sucessor, o sistema supera a natureza de grão grosso das abordagens anteriores, permitindo a formalização de um raciocínio que depende da estrutura interna de proposições numéricas. O trabalho estabelece um equilíbrio entre expressividade (lidar com aritmética e interação epistêmica) e complexidade computacional (mantendo a decidibilidade). Os autores observam que este framework lança as bases para extensões futuras envolvendo estruturas aritméticas mais complexas (adição e multiplicação), que seriam necessárias para resolver enigmas como "Soma e Produto", embora tais extensões apresentem desafios significativos em relação à completude e decidibilidade.