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

Resumen Técnico: Maximalidad de Lindström para la Lógica Modal de Valores de Heyting de Fitting con Pruebas de Verdad Exactas

Planteamiento del Problema
El artículo aborda la caracterización del poder expresivo de las lógicas modales polivalentes, específicamente la lógica modal de Fitting sobre un álgebra de Heyting finita fija ($L$). Si bien existen teoremas de maximalidad de estilo Lindström para la lógica modal clásica y para las lógicas de muchos valores sobre cadenas MTL finitas (álgebras linealmente ordenadas), faltaba un resultado correspondiente para el caso no lineal. Trabajos previos de Badia y Olkhovikov establecieron la maximalidad sobre cadenas MTL finitas utilizando el predecesor inmediato único del elemento superior (1) para separar los valores designados de los no designados. Este enfoque falla para las álgebras de Heyting arbitrarias, que pueden carecer de linealidad y de un único átomo coadyacente por debajo de 1. El problema central es determinar si la presentación de la lógica de Fitting de Maruyama —que utiliza pruebas de verdad unarias exactas ($T_\ell$) en lugar de constantes de verdad primitivas para todos los valores— conserva la maximalidad entre sus extensiones abstractas sin asumir que el álgebra es una cadena.

Metodología
El autor emplea un enfoque de modelos adaptado de los teoremas de Lindström clásicos y de muchos valores. La metodología consiste en:

1. Definición de la Lógica Base: Utilizando la versión de Maruyama de la lógica de Fitting ($FML_L$) sobre marcos de Kripke nítidos (crisp), donde las fórmulas toman valores en un álgebra de Heyting finita $L$. El lenguaje incluye pruebas de verdad exactas $T_\ell$ tales que $T_\ell \phi$ evalúa a 1 si y solo si $\phi$ evalúa a $\ell$.
2. Introducción de Operadores Booleanos Derivados: Para reemplazar el mecanismo de separación dependiente de la cadena, el autor define pruebas de valor booleano:
   • $D\phi := T_1\phi$ (Verdadero si y solo si $\phi$ es designado/igual a 1).
   • $N\phi := T_0(T_1\phi)$ (Verdadero si y solo si $\phi$ es no designado/no igual a 1).
   • Una modalidad existencial derivada $\Diamond_1 \phi := T_0(\Box N\phi)$, que expresa la existencia de un estado accesible donde $\phi$ tiene el valor 1.
3. Extensiones Abstractas: El artículo considera extensiones abstractas $\mathcal{L}$ de $FML_L$ que satisfacen tres propiedades de modelos: Compacidad, la Propiedad de Unión de Tarski e invariancia fuerte bajo bisimulación.
4. Saturación y Desenrollado (Unravelling): La demostración construye extensiones elementales saturadas utilizando técnicas de desenrollado. Aprovecha la modalidad derivada $\Diamond_1$ para definir "tipos sucesores" y utiliza la Compacidad y las propiedades de Unión de Tarski para construir modelos donde estos tipos se realizan.
5. El Lema de Decisión: Un paso crítico involucra un "Lema de Decisión" que utiliza el par $(D\psi, N\psi)$ para separar cualquier nueva fórmula hipotética de la lógica base. Esto reemplaza el argumento del "predecesor inmediato de 1" utilizado en las demostraciones basadas en cadenas.

Contribuciones Clave y Resultados

• Teorema de Maximalidad de Lindström: El resultado principal (Teorema 1) establece que, para cualquier álgebra de Heyting finita $L$ fija, la versión de Maruyama de la lógica de Fitting es maximal con respecto al poder de expresión de 1 entre todas sus extensiones abstractas que son compactas, poseen la Propiedad de Unión de Tarski y son fuertemente invariantes bajo bisimulación.
• Eliminación del Supuesto de Linealidad: El artículo generaliza con éxito el resultado de maximalidad desde los álgebras linealmente ordenadas (cadenas MTL) hacia las álgebras de Heyting finitas arbitrarias. La demostración demuestra que las pruebas de verdad exactas proporcionan un poder de separación suficiente sin requerir un orden lineal o un átomo coadyacente distinguido.
• Definibilidad de Valor Exacto: Como consecuencia del teorema de maximalidad (Corolario 1), el artículo demuestra que para cualquier fórmula $\phi$ en una extensión $\mathcal{L}$ y cualquier valor $\ell \in L$, el conjunto de modelos apuntados donde $\phi$ toma el valor exacto $\ell$ es definible mediante una fórmula en la lógica base $FML_L$. Específicamente, la "fibra de valor exacto" es definible, aunque el artículo señala que esto no implica necesariamente la existencia de una única fórmula en $FML_L$ que reproduzca la semántica completa de $\phi$.
• Propiedad de Hennessy-Milner para Modelos Saturados: El artículo establece que, para modelos saturados de $FML_L$, la equivalencia modal implica bisimulación, extendiendo los fenómenos estándar de Hennessy-Milner a este entorno de muchos valores.

Significancia y Reivindicaciones
El artículo afirma resolver un vacío en la literatura respecto a los límites de expresividad de las lógicas modales de muchos valores sobre álgebras no lineales. Al demostrar que las pruebas de verdad exactas ($T_\ell$) generan pares de decisión booleanos ($D\phi, N\phi$) capaces de separar los valores designados de los no designados, el autor muestra que las restricciones estructurales del álgebra subyacente (específicamente la linealidad) no son necesarias para la maximalidad de Lindström.

La significancia radica en:

1. Generalización: Extender el alcance de los teoremas de Lindström más allá del entorno restrictivo de las cadenas finitas hacia la clase más amplia de las álgebras de Heyting finitas.
2. Identificación del Mecanismo: Identificar las pruebas de valor booleano derivadas de las pruebas de verdad exactas como el mecanismo crucial para la separación de valores y los argumentos de saturación en entornos no lineales.
3. Definibilidad: Establecer que la lógica base es suficientemente expresiva para definir las fibras de valor exacto de cualquier fórmula en una extensión "razonable", reforzando la robustez de la presentación de Maruyama.

El autor mantiene la modestia respecto a direcciones futuras, señalando cuestiones abiertas tales como si la Propiedad de Unión de Tarski puede debilitarse, cómo manejar relaciones de accesibilidad con valores de $L$ (difusas/fuzzy) y si las definiciones separadas de valor exacto pueden unificarse en una sola fórmula que reproduzca la semántica completa.