Lindström Maximality for Fitting's Finite Heyting-Valued Modal Logic with Exact Truth Tests

Resumo Técnico: Maximalidade de Lindström para a Lógica Modal de Valores de Heyting de Fitting com Testes de Verdade Exata

Enunciado do Problema
O artigo aborda a caracterização do poder expressivo de lógicas modais multivaloradas, especificamente a lógica de Fitting sobre uma álgebra de Heyting finita fixa ($L$). Embora existam teoremas de maximalidade no estilo de Lindström para a lógica modal clássica e para lógicas multivaloradas sobre cadeias MTL-finitas (álgebras linearmente ordenadas), um resultado correspondente estava ausente para o caso não linear. Trabalhos anteriores de Badia e Olkhovikov estabeleceram a maximalidade sobre cadeias MTL-finitas utilizando o predecessor imediato único do elemento topo (1) para separar valores designados de não-designados. Essa abordagem falha para álgebras de Heyting finitas arbitrárias, que podem carecer de linearidade e de um único átomo coberto abaixo de 1. O problema central é determinar se a apresentação de Maruyama da lógica de Fitting — que utiliza testes de verdade unários ($T_\ell$) em vez de constantes de verdade primitivas para todos os valores — retém a maximalidade entre suas extensões abstratas sem assumir que a álgebra seja uma cadeia.

Metodologia
O autor emprega uma abordagem de modelo-teórica adaptada de teoremas de Lindström clássicos e multivalorados. A metodologia envolve:

1. Definição da Lógica Base: Utilizando a versão de Maruyama da lógica de Fitting ($FML_L$) sobre quadros de Kripke nítidos (crisp), onde as fórmulas assumem valores em uma álgebra de Heyting finita $L$. A linguagem inclui testes de verdade exata $T_\ell$ tal que $T_\ell \phi$ avalia como 1 se, e somente se, $\phi$ avalia como $\ell$.
2. Introdução de Operadores Booleanos Derivados: Para substituir o mecanismo de separação dependente da cadeia, o autor define testes de valor Booleano:
   • $D\phi := T_1\phi$ (Verdadeiro se $\phi$ é designado/igual a 1).
   • $N\phi := T_0(T_1\phi)$ (Verdadeiro se $\phi$ é não-designado/não igual a 1).
   • Um modal existencial derivado $\Diamond_1 \phi := T_0(\Box N\phi)$, que expressa a existência de um estado acessível onde $\phi$ possui o valor 1.
3. Extensões Abstratas: O artigo considera extensões abstratas $\mathcal{L}$ de $FML_L$ que satisfazem três propriedades de modelo-teórica: Compacidade, a Propriedade da União de Tarski e invariância forte sob bisimulação.
4. Saturação e Desenrolamento (Unravelling): A prova constrói extensões elementares saturadas usando técnicas de desenrolamento. Ela utiliza o modal derivado $\Diamond_1$ para definir "tipos sucessores" e utiliza a Compacidade e a Propriedade da União de Tarski para construir modelos onde esses tipos são realizados.
5. O Lema de Decisão: Um passo crítico envolve um "Lema de Decisão" que utiliza o par $(D\psi, N\psi)$ para separar qualquer nova fórmula hipotética da lógica base. Isso substitui o argumento do "predecessor imediato de 1" usado em provas baseadas em cadeias.

Contribuições Principais e Resultados

• Teorema de Maximalidade de Lindström: O resultado principal (Teorema 1) afirma que, para qualquer álgebra de Heyting finita fixa $L$, a versão de Maruyama da lógica de Fitting é maximal com relação ao poder de expressão de 1 entre todas as suas extensões abstratas que são compactas, possuem a Propriedade da União de Tarski e são fortemente invariantes sob bisimulação.
• Remoção da Suposição de Linearidade: O artigo generaliza com sucesso o teorema de maximalidade de cadeias MTL para o caso de álgebras de Heyting finitas arbitrárias. A prova demonstra que os testes de verdade exata fornecem poder de separação suficiente sem exigir uma ordem linear ou um átomo coberto distinguido.
• Definibilidade de Valor Exato: Como consequência do teorema de maximalidade (Corolário 1), o artigo prova que para qualquer fórmula $\phi$ em uma extensão $\mathcal{L}$ e para qualquer valor $\ell \in L$, o conjunto de modelos pontuados onde $\phi$ assume o valor exato $\ell$ é definível por uma fórmula na lógica base $FML_L$. Especificamente, a "fibra de valor exato" é definível, embora o artigo note que isso não implica necessariamente a existência de uma única fórmula em $FML_L$ que reproduza a semântica total de $\ell$.
• Propriedade de Hennessy-Milner para Modelos Saturados: O artigo estabelece que, para modelos saturados de $FML_L$, a equivalência modal implica bisimulação, estendendo os fenômenos padrão de Hennessy-Milner para este cenário multivalorado.

Significância e Alegações
O artigo alega resolver uma lacuna na literatura referente aos limites expressivos de lógicas modais multivaloradas sobre álgebras não lineares. Ao demonstrar que os testes de verdade exata ($T_\ell$) geram pares de decisão booleanos ($D\phi, N\phi$) capazes de separar valores designados de não-designados, o autor mostra que as restrições estruturais da álgebra subjacente (especificamente a linearidade) não são necessárias para a maximalidade de Lindström.

A significância reside em:

1. Generalização: Estender o escopo dos teoremas de Lindström além do cenário restritivo de cadeias finitas para a classe mais ampla de álgebras de Heyting finitas.
2. Identificação de Mecanismo: Identificar os testes de valor Booleano derivados dos testes de verdade exata como o mecanismo crucial para a separação de valores e argumentos de saturação em cenários não lineares.
3. Definibilidade: Estabelecer que a lógica base é suficientemente expressiva para definir as fibras de valor exato de qualquer fórmula em uma extensão "razoável", reforçando a robustez da apresentação de Maruyama.

O autor mantém-se modesto quanto a direções futuras, observando questões em aberto, tais como se a Propriedade da União de Tarski pode ser enfraquecida, como lidar com relações de acessibilidade $L$-valoradas (fuzzy) e se as definições separadas de valor exato podem ser unificadas em uma única fórmula que reproduza a semântica total.