Intuitionistic Monotone Modal Logic: Proof Theory and Semantics

Resumo Técnico: Lógica Modal Monótona Intuicionista: Teoria da Prova e Semântica

Problema
O artigo aborda uma lacuna no estudo da lógica modal monotônica intuicionista, especificamente a lógica IM introduzida recentemente em [27]. Enquanto a lógica monotônica clássica ($M$) é bem estudada e fundamenta sistemas como a lógica de jogos e a lógica de coalizão, seus contrapartes intuicionistas permanecem subdesenvolvidos em comparação com os análogos intuicionistas de lógicas modais normais (como $K$ e $S4$). O trabalho existente sobre lógicas monotônicas intuicionistas inclui CM (modalidades completamente independentes), WM (estilo Wijesekera, permitindo zero ou um conclusão) e IM (derivada via tradução para a lógica de primeira ordem intuicionista). No entanto, a IM carecia de um tratamento de teoria da prova dedicado, de um estudo sistemático de suas extensões e de resultados básicos de decidibilidade. Além disso, a relação entre variantes construtivas (como WM) e variantes intuicionistas (como IM) da lógica monotônica exigia esclarecimento.

Metodologia
Os autores empregam uma abordagem dual combinando caracterização semântica e análise de teoria da prova:

1. Caracterização Semântica: Os autores definem quadros de vizinhança construtivos (derivados de [11]) para fornecer uma semântica para IM e suas extensões. Diferente dos modelos de vizinhança intuicionistas em [27], esses quadros utilizam uma pré-ordenação e uma função de vizinhança que mapeia mundos para conjuntos de conjuntos de mundos. Eles introduzem o conceito de quadros contínuos para capturar as propriedades específicas de IM. Uma construção de modelo canônico usando segmentos (pares de teorias primas e coleções de conjuntos de teorias) é utilizada para provar a completude.

2. Análise de Teoria da Prova: Os autores desenvolvem um cálculo de sequente livre de corte, $C_{IM}$, para IM. Este cálculo é adaptado do cálculo estruturado $HM$ para a lógica monotônica clássica [14]. Características estruturais principais incluem:

   • Fórmulas Marcadas: As fórmulas são marcadas com polaridade de entrada ($\bullet$) ou saída ($\circ$).
   • Blocos: Conectivos estruturais $\{ \Delta \}$ representando conjuntos de vizinhança.
   • Poda de Saída ($\downarrow$): Uma operação distintiva na regra de implicação ($\to^\bullet$) que remove fórmulas de saída (e esvazia blocos de saída) ao mover-se das premissas para as conclusões. Esta operação é crucial para capturar o axioma $I3$ ($(2\top \to 3\phi) \to 3\phi$).
   • Extensões: O cálculo é estendido modularmente para lidar com os axiomas $N, P, T, D,$ e $K$ através da adição de regras estruturais específicas (ex: $n, p, d, t, k$), mantendo as regras lógicas inalteradas, aderindo ao princípio de Dösen.

Principais Contribuições

1. Completude Semântica: O artigo fornece uma semântica completa e sonora para IM e suas extensões em relação a classes de quadros de vizinhança construtivos contínuos. Isso difere da abordagem de tradução para primeira ordem de [27] ao oferecer uma semântica modal direta que auxilia na compreensão do cálculo de sequente.
2. Cálculo Livre de Corte ($C_{IM}$): Os autores apresentam um cálculo de sequente terminante e livre de corte para IM. O cálculo simula com sucesso os axiomas de IM, particularmente a interação entre as modalidades via o axioma $I3$, através do mecanismo de poda de saída.
3. Decidibilidade: Ao estabelecer a propriedade de subfórmula e uma condição de verificação de loop para a busca de prova reversa em $C_{IM}$, os autores provam que IM é decidível.
4. Relação com $WM$: O artigo demonstra uma relação próxima entre IM e WM. Ao modificar a operação de poda de saída em $C_{IM}$ para afunilamento de saída (que remove blocos inteiros de saída em vez de apenas esvaziá-los), os autores derivam um cálculo $C_{WM}$ para WM. Isso permite uma re-prova de que IM e WM possuem diferentes fragmentos 2-livres, enquanto compartilham o mesmo fragmento 3-livre.
5. Extensões: O arcabouço é estendido para cobrir extensões axiomáticas de IM (incluindo $N, P, T, D, K$). Para o axioma $K$, o cálculo é generalizado para permitir blocos contendo multiconjuntos de fórmulas, introduzindo uma nova regra $k$ para dividir blocos.

Resultos

• Completude: O Teorema 2.14 estabelece que $\vdash_{IM \oplus Ax} \phi$ se, e somente se, $\Vdash_{IM \oplus Ax} \phi$ para qualquer subconjunto de axiomas $Ax \subseteq \{N, P, T, D, K\}$.
• Eliminação de Corte: O Teorema 3.12 prova a admissibilidade do corte (e regras de substituição) em $C_{IM}$, garantando que o cálculo é analítico.
• Decidibilidade: O Teorema 3.14 confirma que o problema de derivabilidade de IM é decidível.
• Distinção de Fragmentos: O artigo re-confirma que IM e WM diferem em seus fragmentos 2-livres (especificamente em relação à derivabilidade de $((3\bot \to \bot) \to \bot) \to 3\bot$), enquanto compartilham o mesmo fragmento 3-livre.
• Correção e Completude para Extensões: Os Teoremas 4.4 e 4.14 estendem os resultados de correção e completude para todas as extensões axiomáticas consideradas, incluindo aquelas com o axioma $K$.

Significância
O artigo afirma preencher a lacuna no estudo de teoria da prova e semântica da IM. Ao fornecer um cálculo livre de corte, estabelece a IM como uma lógica bem comportada com um problema de derivabilidade decidível. Uma descoberta central é a revelação de uma analogia entre as variantes construtivas/intuicionistas da lógica monotônica ($M$) e da lógica normal ($K$):

• Variantes construtivas (como WM) correspondem a restrições de sucedente único de cálculos de Gentzen padrão.
• Variantes intuicionistas (como IM) correspondem a restrições de sucedente único de cálculos de sequente estruturados (envolvendo blocos e operações de poda específicas).

Esta percepção estrutural justifica a IM como uma variante intuicionista fiel da lógica monotônica clássica. Os autores observam que seu trabalho abre questões relativas à generalização deste padrão para outras lógicas modais e ao potencial de extração de contramodelos a partir de derivações falhas, o que identificam como direções para pesquisas futuras.