Hyperformalism for Relevant Modal Logics

Resumo Técnico: Hiperformalismo para Lógicas Modais Relevantes

Problema e Contexto
O artigo aborda a análise de lógicas relevantes através da lente do hiperformalismo, uma propriedade na qual uma lógica permanece fechada sob substituições não uniformes. Nas lógicas formais padrão, os átomos são tratados como independentes via substituição uniforme. O hiperformalismo estende essa independência, permitindo que ocorrências distintas do mesmo átomo sejam tratadas como independentes se aparecerem em contextos sintáticos suficientemente diferentes (por exemplo, em diferentes "profundidades" ou sob diferentes operadores modais). Embora o hiperformalismo tenha sido aplicado com sucesso a lógicas relevantes não modais (como $B$ e $DR$), revelando fortes propriedades de compartilhamento de variáveis e identificando novas lógicas relevantes, sua aplicação a lógicas modais relevantes permanece pouco explorada. Os autores buscam estender essas técnicas para configurações modais, investigando especificamente como a presença do operador modal $\square$ interage com substituições não uniformes e o compartilhamento de variáveis.

Metodologia
Os autores empregam uma combinação de técnicas proof-teóricas e semânticas para analisar lógicas modais relevantes:

1. Estrutura Sintática (MPos): Os autores definem um conjunto de posições, $MPos = \{l, r, n, b\}^*c$, onde $l$ e $r$ denotam ramos esquerddo e direito de condicionais, $n$ denota negação, e $b$ denota o escopo do operador modal $\square$.
2. Substituições: Eles definem substituições MPos como funções $\sigma: MPos \times At \to L$ que respeitam a estrutura das fórmulas. Crucialmente, essas substituições tratam átomos em diferentes posições como independentes, sujeitos a restrições específicas de "fidelidade" (por exemplo, $\sigma_{xnn}(p) = \sigma_x(p)$ para preservar as propriedades de dupla negação).
3. Análise Proof-Teórica: O artigo analisa a lógica modal relevante base $B^\square$ (formada pela adição dos axiomas $C$ e da regra $RM$ à lógica relevante $B$). Eles provam o fechamento sob substituições MPos via indução em derivações.
4. Extensões: Os autores definem relações de equivalência em $MPos$ correspondentes aos axiomas modais $T, 4, K,$ e $RN$. Eles investigam as lógicas resultantes $B^\square_S$ e seu fechamento sob as correspondentes $MPos_S$-substituições.
5. Caracterização Semântica: Para caracterizar a maior sublógica hiperformal de lógica modal clássica $K$ (denotada como $KMPos$), os autores introduzem:
   • Atribuições MPosK: Funções $\alpha: MPos \times W \times At \to \{0, 1\}$ sobre quadros de Kripke, onde os valores de verdade variam com base no índice de posição.
   • Tableaux Analíticos: Um sistema de tableau com nós $\langle x, \omega, A, i \rangle$ rastreando posições ($x$), mundos ($\omega$), fórmulas ($A$) e valores de verdade ($i$).
6. Modelos Canônicos: A completude é estabelecida via construção de conjuntos de ramos maximais, testemunhados e consistentes com o tableau e seus respectivos modelos canônicos.

Principais Contribuições e Resultados

1. Hiperformalismo MPos de $B^\square$:

   • Teorema 2.1: A lógica base $B^\square$ é provada como sendo MPos-hiperformal. A prova demonstra que os axiomas ($C$) e regras ($RM$) do sistema preservam a teorematicidade sob substituições MPos.
   • Compartilhamento de Variáveis: Como consequência, $B^\square$ satisfaz a propriedade de compartilhamento de variáveis MPos. Se $A \to B$ é um teorema, existe uma variável compartilhada $p$ tal que a posição de $p$ em $A$ e $B$ são equivalentes sob a relação $\sim_{nn}$ (diferindo apenas por pares de negações).
   • Corolário 2.6: Uma consequência específica é que qualquer teorema $A \to B$ em $B^\square$ compartilha uma variável aninhada dentro do mesmo número de operadores $\square$ tanto no antecedente quanto no consequente.

2. Extensões de $B^\square$:

   • Teorema 2.7: Para qualquer subconjunto $S \subseteq \{T, 4, K, RN\}$, a lógica $B^\square_S$ é $MPos_S$-hiperformal, onde $MPos_S$ incorpora relações de equivalência que refletem os axiomas modais específicos (por exemplo, $xby \sim_4 xbby$ para o axioma 4).
   • Compartilhamento de Variáveis Refinado: Essas extensões produzem propriedades de compartilhamento de variáveis refinadas. Por exemplo, em $B^\square_{\{4\}}$, variáveis compartilhadas devem ter o mesmo "modo" (extensional vs. intensional), efetivamente eliminando a contagem de operadores $\square da condição de compartilhamento.

3. Caracterização de $KMPos$:

   • Os autores definem $KMPos$ como a maior sublógica hiperformal de MPos da lógica modal clássica $K$.
   • Caracterização Semântica: $KMPos$ é caracterizada pela validade em quadros de Kripke equipados com atribuições MPosK.
   • Caracterização por Tableau: Um sistema de tableau sônico e completo é fornecido para $KMPos$.
   • Teorema 3.6: $KMPos$ é equivalente ao conjunto de fórmulas $A$ tais que, para alguma substituição atômica $\iota$ injetiva-até-a-fidelidade, $\iota(A)$ é um teorema de $K$. Isso confirma que $KMPos$ é o subconjunto maximal de $K$ fechado sob substituições MPos.
   • Compartilhamento de Variáveis: O Teorema 3.9 estabelece que $KMPos$ possui a propriedade de compartilhamento de variáveis.

4. Transitividade e Natureza de $KMPos$:

   • Teorema 4.1: $KMPos$ é transitiva. Os autores argumentam que, ao contrário das abordagens de "peneira sintática" para a relevância (que frequentemente falham na transitividade), $KMPos$ evita tais patologias porque é definida por uma propriedade de fechamento (hiperformalismo) em vez de um filtro estático sobre teoremas clássicos.

Significância e Alegações
O artigo afirma que o hiperformalismo é uma ferramenta poderosa para analisar lógicas modais relevantes, capaz de revelar fortes propriedades de compartilhamento de variáveis mesmo em sistemas fracos como $B^\square$. No entanto, os autores argumentam que $B^\square$ não é a lógica mais forte com essas características.

A principal significância reside na introdução e caracterização de $KMPos$. Os autores postulam que $KMPos$ representa a "maior" lógica modal relevante no sentido de ser a sublógica maximal de $K$ que é fechada sob substituições MPos. Eles afirmam que $KMPos$ oferece vantagens semânticas e proof-teóricas sobre $B^\square$ e outras lógicas modais relevantes tradicionais. Especificamente, eles argumentam que $KMPos$ não é meramente uma "peneira sintática" (um termo pejorativo para lógicas definidas simplesmente filtrando teoremas clássicos) porque é transitiva e definida por uma propriedade de fechamento robusta.

O artigo conclui desafiando a preferência por lógicas modais relevantes "tradicionais" (como $B^\square$) sobre $KMPos$. Os autores sugerem que, a menos que existam razões específicas para preferir as primeiras, pesquisadores devem considerar $KMPos$, pois ela retém as características desejáveis de compartilhamento de variáveis enquanto é uma sublógica maximal da lógica modal clássica. O artigo reconhece que uma caracterização axiomática de $KMPos$ permanece um problema em aberto, observando que tais lógicas historicamente resistiram à axiomatização recursiva.