Possibly Relevant Translations

Resumo Técnico: Possíveis Traduções Relevantes

Problema e Motivação
O artigo aborda a relação estrutural entre as lógicas relevantes (especificamente a linhagem Anderson–Belnap) e as lógicas modais normais. Embora a tradução da lógica intuicionista para a lógica modal clássica (via tradução de Gödel–McKinsey–Tarski) tenha historicamente fomentado um intercâmbio significativo entre tradições, uma tradução sistemática comparável entre lógicas relevantes e modais permanece subdesenvolvida. O autor visa estabelecer traduções completas e fiéis de lógicas relevantes para lógicas modais normais para esclarecer conexões estruturais, derivar resultados corolários e identificar limitações nas abordagens translacionais atuais. O trabalho foca inicialmente no fragmento positivo $\{\land, \lor, \to\}$ e estende-se gradualmente para incluir a constante de verdade $t$, a fusão $\circ$ e a negação $\neg$.

Metodologia
O artigo emprega uma abordagem semântica, utilizando transformações de modelos entre dois frameworks distintos:

1. Frames de Routley–Meyer: A semântica padrão para lógicas relevantes, definida como triplas $(K, R, N)$ onde $R$ é uma relação ternária e $N$ é um conjunto de pontos normais, sujeitos a restrições de ordem e relacionais específicas (por exemplo, a condição "down-down-up").
2. Frames de Kripke: A semântica padrão para lógicas modais normais, definida como pares $(W, R)$ (ou tuplas com relações adicionais para linguagens estendidas).

A metodologia central envolve a definição de uma função de tradução (denotada por $\star$, $\ast$, ou $\circ$) de fórmulas relevantes para fórmulas modais. Para provar que essas traduções são completas (se uma implicação relevante é válida, a tradução modal é válida) e fiéis (se a tradução modal é válida, a implicação relevante é válida), o autor constrói duas transformações de modelos:

• $F$: Mapeia modelos de Kripke pontuados para modelos de Routley–Meyer pontuados.
• $G$: Mapeia modelos de Routley–Meyer pontuados para modelos de Kripke pontuados.

Essas transformações são projetadas para satisfazer padrões de adjunção onde a satisfação em um modelo corresponde à satisfação da fórmula traduzida no outro. O artigo também utiliza a teoria da correspondência (especificamente a correspondência de Sahlqvist) para identificar as condições de frame na semântica de Kripke que correspondem a axiomas relevantes específicos.

Principais Contribuições e Resultados

1. Tradução Positiva Básica ($\star$):

   • O autor define uma tradução $\star$ para o fragmento $\{\land, \lor, \to\}$ onde $\to$ é mapeado para um operador modal definido $\neg \Diamond(\cdot, \neg \cdot)$.
   • Teorema 1.4: Estabelece que para a lógica relevante básica $B^+$ e a lógica modal binária $K_2$, $\vdash_{B^+} \phi \to \psi$ se e somente se $\vdash_{K_2} \phi^\star \supset \psi^\star$.
   • Extensão para Lógicas Mais Fortes: A tradução estende-se para lógicas axiomatizadas por subconjuntos de axiomas 7–10 (ex: $TW^+$, $TWJ^+$, $C^+$). No entanto, o artigo demonstra que esta tradução falha para lógicas que requerem contração (axioma 11) ou asserção (axioma 12), como $R^+$. A falha decorre do fato de que a semântica de Kripke mais simples carece das condições de ordem específicas (como a propriedade "down-down-up") inerentes aos frames de Routley–Meyer que são necessárias para validar esses axiomas.

2. Tradução de Implicação Aninhada ($\ast$):

   • Para abordar fórmulas onde o conectivo principal não é $\to$, uma segunda tradução $\ast$ é introduzida, mapeando $\phi \to \psi$ para $\Box_\to(\phi^\star \supset \psi^\star)$.
   • Teorema 1.7: Mostra que $\ast$ fornece um encaixe (embedding) completo e fiel de $B^+$ em $K_2$ para todas as fórmulas positivas, realizando $B^+$ como um fragmento sintático de $K_2$.
   • Assim como a tradução $\star$, esta abordagem também encontra limitações ao ser estendida para lógicas que envolvem contração e asserção.

3. Indecidibilidade e Interpolação:

   • O artigo transfere resultados de indecidibilidade de lógicas relevantes para lógicas modais. Especificamente, prova que as lógicas modais correspondentes às condições de frame de $TWJ^+$ e $C^+$ são indecidíveis (Teorema 1.9), suplementando resultados existentes de Urquhart e outros.
   • O autor levanta questões abertas sobre a Propriedade de Interpolação de Craig (CIP). Embora $K_2$ possua CIP, não se sabe se $B^+$ possui. A tradução sugere que, se $B^+$ carece de CIP, isso pode ser devido ao comportamento específico da tradução ou à falta de determinado vocabulário.

4. Traduções Estendidas ($\circ$):

   • Para superar as limitações das traduções anteriores em relação à contração e asserção, o artigo introduz uma tradução para uma linguagem modal mais rica contendo uma modalidade nulária $t$ e uma modalidade binária $\circ$.
   • Definição 2.2: Define Modal $B^+$ ($Mod.B^+$) como a menor lógica modal normal contendo axiomas de residuação e axiomas correspondentes às condições de frame de Routley–Meyer (reflexividade, transitividade, aumentos, etc.).
   • Teorema 2.5: Demonstra que, para a linguagem estendida com $t$ e $\circ$, a tradução $\circ$ é completa e fiel: $\vdash_B \phi$ se e somente se $\vdash_{Mod.B^+} t \supset \phi^\circ$. Esta tradução captura com sucesso as restrições estruturais dos frames de Routley–Meyer (incluindo a relação de ordem $\leq$) dentro da semântica de Kripke.
   • Teorema 2.8: Estende este resultado para a linguagem completa incluindo a negação $\neg$ ao introduzir uma modalidade unária $\Box_\neg$ e condições de frame correspondentes (involução e reversão de ordem).

Significância e Alegações
O artigo alega modestamente esclarecer as conexões estruturais entre lógicas relevantes e modais através de uma série de traduções. Sua principal significância reside em:

• Prover uma tradução completa e fiel da lógica relevante básica $B$ (e suas extensões com $t, \circ, \neg$) para uma lógica modal normal específica ($Mod.B$), realizando a lógica relevante como um fragmento sintático da lógica modal.
• Destacar as limitações de traduções mais simples (como $\star$) quando aplicadas a lógicas relevantes mais fortes (como $R^+$), notando especificamente que os frames de Kripke padrão não podem capturar as propriedades de ordem necessárias dos frames de Routley–Meyer sem axiomas ou modalidades adicionais.
• Facilitar a transferência de propriedades metalógicas, como decidibilidade e indecidibilidade, entre as duas tradições.
• Identificar questões abertas para trabalhos futuros, particularmente em relação à propriedade de interpolação em $B^+$ e o potencial para aprofundar a conexão estrutural para incluir lógicas incompletas de frame.

O autor afirma explicitamente que o artigo é "exploratório e amplo, em vez de profundo", deixando uma análise mais completa das motivações filosóficas e das relações estruturais mais profundas para trabalhos futuros.