Dynamic Hypersequents for Public Announcement Logic

Resumo Técnico: Hipersequentes Dinâmicos para Lógica de Anúncio Público

Enunciação do Problema
A Lógica Epistêmica Dinâmica (DEL), e especificamente a Lógica de Anúncio Público (PAL), modela a evolução do conhecimento através de atualizações de informação. Embora a semântica da PAL seja bem compreendida como transformações de modelos de Kripke (onde um anúncio restringe o conjunto de mundos possíveis), os quadros existentes de teoria da prova lutam para capturar essa dinâmica ao nível sintático. Tentativas anteriores, incluindo métodos de tabela e vários cálculos de sequentes (rotulados e não rotulados), frequentemente falham em alcançar simultaneamente uma genuína propriedade de subfórmula, a admissibilidade de todas as regras estruturais (incluindo contração) e a eliminação sintática de corte. Muitos sistemas existentes dependem de axiomas de redução que traduzem fórmulas dinâmicas em estáticas, obscurecendo assim a natureza dinâmica da lógica dentro do próprio sistema de prova.

Metodologia
Os autores propõem um novo quadro de teoria da prova baseado em hipersequentes dinâmicos. Esta abordagem estende o cálculo de hipersequentes para S5 (introduzido em [15, 16]) incorporando um mecanismo para modelar transições entre modelos epistêmicos induzidas por anúncios públicos.

1. Sequentes Dinâmicos: Um sequente dinâmico é definido como uma sequência de sequentes padrão rotulados por sequências finitas distintas de anúncios (por exemplo, $\alpha_1 \Gamma_1 | \dots | \alpha_n \Gamma_n$). Intuitivamente, um sequente dinâmico representa um mundo específico $w$ em um modelo inicial $M$ e suas "cópias" em modelos sucessivamente atualizados $M_{\alpha}$.
2. Hipersequentes Dinâmicos (DHS): Um hipersequente dinâmico é uma coleção de sequentes dinâmicos. Esta estrutura representa sintaticamente um modelo epistêmico inteiro e suas atualizações sucessivas simultaneamente. Os autores interpretam um DHS como uma disjunção de fórmulas boxeadas, onde cada componente corresponde a um mundo no modelo ou em suas atualizações.
3. O Cálculo ($DHSPAL$): Os autores definem um cálculo $DHSPAL$ compreendendo:
   • Regras Proposicionais e Modais: Adaptadas de cálculos de hipersequentes padrão para S5.
   • Regras de Anúncio: Regras $(L[\cdot])$ e $(R[\cdot])$ que decompõem fórmulas de anúncio público $[A]B$. Estas regras gerenciam explicitamente a transição de um estado atual para um estado atualizado, introduzindo novos sequentes dinâmicos rotulados com a sequência de anúncio estendida $\alpha \cdot A$.
   • Regras Estruturais Dinâmicas: Regras específicas como $(Lat)$e$(Rat)$ (Permanência Atômica), $(New)$ (garantindo que mundos em modelos atualizados existam nos anteriores) e $(Recall)$ (garantindo que a fórmula anunciada valha no modelo anterior).
   • Regra Modal Dinâmica: Uma regra especializada $(L\Box_3)$ que lida com a interação entre conhecimento ($\Box$) e sequências de anúncios, distinguindo entre mundos que sobrevivem a uma atualização e aqueles que não sobrevivem.

Principais Contribuições e Resultados
O artigo estabelece que $DHSPAL$ é um sistema de prova robusto para PAL, alcançando várias propriedades que sistemas anteriores não possuíam simultaneamente:

• Admissibilidade de Regras Estruturais: Os autores provam a hp-admissibilidade (admissibilidade que preserva a altura) de enfraquecimento, contração e uma regra de mesclagem. Crucialmente, isso inclui contração, que é frequentemente difícil de alcançar em lógicas dinâmicas sem perder analiticidade.
• Invertibilidade de Regras Lógicas: Todas as regras lógicas no cálculo são mostradas como hp-invertíveis. Esta propriedade é essencial para a busca de prova e para estabelecer a eliminação de corte.
• Eliminação Sintática de Corte: O artigo fornece uma prova da admissibilidade da Regra de Corte. A prova baseia-se em uma dupla indução: uma na complexidade DHS da fórmula de corte (uma medida de complexidade relativa à sequência de anúncios) e outra na soma das alturas das derivações das premissas.
• Correção e Completude: O cálculo é provado correto e completo em relação à semântica padrão de Kripke da PAL. A prova de completude envolve derivar todos os axiomas no estilo de Hilbert da PAL, incluindo os axiomas de redução, dentro do quadro de hipersequentes dinâmicos.
• Propriedade de Subfórmula: Como consequência da eliminação de corte, o cálculo goza da propriedade de subfórmula, garantindo que qualquer fórmula em uma derivação seja uma subfórmula do sequente final ou de um anúncio ocorrendo dentro dele.

Significado e Alegações
Os autores afirmam que este trabalho representa um passo significativo para abordar a lacuna entre a dinâmica semântica da PAL e sua teoria da prova sintática. Ao usar hipersequentes dinâmicos, o sistema captura o caráter dinâmico da lógica através de meios puramente estruturais, evitando a necessidade de elementos semânticos explícitos (como rótulos para mundos) ou redução à lógica estática.

O artigo afirma que, segundo o conhecimento dos autores, $DHSPAL$ é o primeiro cálculo para PAL que satisfaz simultaneamente:

1. Admissibilidade de todas as regras estruturais (incluindo contração).
2. Invertibilidade de todas as regras lógicas.
3. Eliminação sintática de corte.
4. Uma genuína propriedade de subfórmula.

Os autores concluem que o quadro de hipersequentes dinâmicos é suficientemente expressivo e robusto para servir como fundamento para o desenvolvimento de cálculos de sequentes para classes mais amplas de lógicas epistêmicas dinâmicas envolvendo diferentes tipos de atualizações de informação. Eles sugerem que trabalhos futuros poderiam explorar decidibilidade, interpolação e análise de complexidade dentro deste quadro.