A Gödel Modal Logic Over Witnessed Models

Resumen Técnico: Una Lógica Modal de Gödel sobre Modelos con Testigo

Planteamiento del Problema
Las lógicas modales de Gödel (GKs) proporcionan un marco para razonar sobre nociones graduadas de incompletitud y vaguedad utilizando los operadores de necesidad ($\Box$) y posibilidad ($\Diamond$) evaluados sobre el intervalo unitario real $[0,1]$. La semántica estándar para estas lógicas se basa en modelos de Kripke de Gödel (modelos G), donde el valor de verdad de una fórmula modal se define mediante el ínfimo o el supremo de los valores de verdad sobre los mundos accesibles. Una limitación crítica de esta semántica estándar es que estos límites no necesariamente deben ser alcanzados por ningún mundo accesible específico (un "testigo"). Este fenómeno basado en límites genera patologías lógicas significativas: la lógica carece de la Propiedad del Modelo Finito (FMP, por sus siglas en inglés) y ciertas validezades en modelos finitos (por ejemplo, $\Box\neg\neg\phi \to \neg\Box\phi$) fallan en modelos infinitos. En consecuencia, los argumentos semánticos suelen requerir un comportamiento genuinamente infinitario, lo que complica el razonamiento automatizado y el análisis de la teoría de la prueba.

Metodología
Los autores introducen GW, una lógica modal de Gödel basada en modelos con testigo (witnessed models). En un modelo GW, la semántica de los operadores modales está constreñida de tal manera que el ínfimo y el supremo que definen los valores de verdad de $\Box\phi$ y $\Diamond\phi$ deben ser alcanzados por al menos un mundo accesible (un "testigo"). Esto asegura que el valor de verdad de una fórmula modal esté determinado por mundos concretos en lugar de aproximaciones asintóticas.

Para analizar GW, los autores desarrollan un cálculo de refutación basado en restricciones llamado CGW. La metodología implica:

1. Lenguaje de Restricciones: Las fórmulas se traducen en restricciones sobre un conjunto contable de etiquetas que representan mundos. Estas restricciones involucran términos atómicos (mundos, relaciones de accesibilidad $R$ y evaluaciones proposicionales) y relaciones ($<, \le, >, \ge$) sobre números racionales en $[0,1]$.
2. Cálculo de Refutación: CGW está diseñado para certificar que una fórmula no es válida en ningún modelo GW. Emplea reglas proposicionales, reglas modales (que introducen nuevas etiquetas para testigos) y reglas para la relación de accesibilidad (reglas $R$).
3. Búsqueda de Pruebas y Generación de Contramodelos: Los autores diseñan un procedimiento de búsqueda de pruebas hacia atrás que termina. Si la búsqueda no logra derivar una contradicción, el procedimiento rastrea la computación para construir un contramodelo finito (específicamente, un modelo GW discreto) para la fórmula de entrada.
4. Análisis de Complejidad: Se esboza un procedimiento de decisión PSPACE, utilizando una búsqueda recursiva que gestiona las asignaciones de valores de verdad a las subfórmulas sin construir explícitamente todo el modelo en memoria.

Contribuciones Clave

• Definición de GW: La formalización de la lógica modal de Gödel sobre modelos de Kripke con testigo, distinguiéndola de la GK estándar y de la variante nítida (crisp) $GW^c$.
• Cálculo CGW: La presentación de un cálculo de refutación sólido y completo para GW. El cálculo maneja las restricciones específicas de la semántica con testigo, particularmente el requisito de que los límites sean alcanzados.
• Propiedad del Modelo Finito (FMP): Los autores demuestran que GW posee la FMP como una consecuencia directa del procedimiento de búsqueda de pruebas que termina. Si una fórmula no es válida, existe un contramodelo finito. Esto contrasta con la GK estándar, que carece de la FMP.
• Incrustación y No Interdefinibilidad:
  • El artículo demuestra que la lógica modal clásica K puede incrustarse en GW (y lógicas relacionadas) mediante una traducción que involucra la doble negación.
  • Demuestra que $\Box$ y $\Diamond$ no son interdefinibles en ninguna lógica modal contenida dentro de $GW^c$, extendiendo resultados previos conocidos para modelos nítidos.
• Resultados de Complejidad: El problema de validez para GW se establece como PSPACE-completo. El límite inferior proviene de la incrustación de K, y el límite superior se deriva del procedimiento PSPACE para la existencia de contramodelos.
• Implementación: Se implementa un prototipo de probador llamado gwref, que utiliza el motor JTabWb y el solver Choco para las comprobaciones de consistencia de restricciones.

Resultados

• Solidez y Completitud: Se demuestra que CGW es sólido y completo con respecto a los modelos GW. Una fórmula $\phi$ es válida en GW si y solo si el conjunto de restricciones $\{w : \phi < 1\}$ no es demostrable en CGW.
• Terminación: El cálculo es fuertemente terminante. Una relación bien fundada sobre multiconjuntos de restricciones asegura que cualquier búsqueda de prueba hacia atrás finalice.
• Extracción de Contramodelos: Cuando la búsqueda de la prueba falla, el procedimiento construye un contramodelo discreto con un tamaño acotado por $O(|\phi|^{| \phi |})$.
• Jerarquía Lógica: El artículo clarifica las relaciones entre varias lógicas: $GK \subset G^c \subset GW^c$ y $GK \subset GW \subset GW^c$. Muestra que el axioma "Nítido" (válido en $G^c$) no es válido en $GW$, y que el axioma "Con Testigo" ($\Box\neg\neg\alpha \to \neg\neg\Box\alpha$) es válido en $GW$ pero no en $G^c$.

Significancia
El artículo argumenta que la semántica con testigo proporciona una forma fundamentada de superar las dificultades asociadas con los fenómenos basados en límites en las lógicas modales difusas. Al asegurar que los comportamientos existenciales y universales estén respaldados por testigos explícitos, la semántica de GW se asemeja más a la cuantificación guardada en la lógica de primer orden y restaura una lectura constructiva.

La significancia de este trabajo radica en:

1. Restauración de Propiedades Constructivas: La FMP y los resultados de decidibilidad hacen que GW sea adecuado para el razonamiento automatizado, permitiendo que los argumentos semánticos infinitarios sean reemplazados por argumentos combinatorios finitos.
2. Alineación Teórica de la Prueba: La semántica con testigo se alinea más estrechamente con los cálculos sintácticos, facilitando las construcciones de modelos canónicos y las demostraciones de completitud estándar.
3. Conexiones con Lógicas Intermedias: Los resultados se posicionan como relevantes para el estudio de las lógicas de predicados intermedias, sugiriendo conexiones profundas con propiedades como el Teorema de Herbrand y la interpolación en fragmentos de un solo argumento de las lógicas de predicados intuicionistas.
4. Aplicabilidad Práctica: El desarrollo de un procedimiento de búsqueda de pruebas que termina con generación de contramodelos ofrece una herramienta práctica para verificar propiedades en sistemas que involucran incertidumbre graduada, representación del conocimiento y sistemas multiagente.

Los autores señalan que, si bien el enfoque funciona bien para modelos con testigo, tratar las lógicas modales de Gödel con modelos sin testigo sigue siendo un problema abierto significativamente más difícil. El trabajo futuro incluye la extensión del procedimiento a otras lógicas con testigo con restricciones de marco adicionales (reflexividad, transitividad) y el desarrollo de una semántica de K de birelación para GW.