First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)

Resumen Técnico: Lógica Modal de Primer Orden en HOL: Embebidos Profundos y Superficiales con Fidelidad Automatizada

Planteamiento del Problema
La lógica modal de primer orden (FML) combina el poder expresivo de la cuantificación con la modalidad, sirviendo como un marco crítico para aplicaciones en inteligencia artificial, ciencias de la computación y filosofía. Si bien se ha automatizado con éxito la inserción (embedding) de la lógica modal proposicional (PML) en la lógica de orden superior clásica (HOL), la extensión de estas técnicas a la FML introduce una complejidad significativa. Específicamente, la FML requiere el manejo de la vinculación de variables, la sustitución y la cuantificación sobre dominios que pueden ser no contables. El trabajo previo [5] estableció una metodología de embebido profundo y superficial para la PML, pero no abordó la maquinaria de sustitución ni los problemas de suryectividad inherentes a la cuantificación de primer orden. El desafío radica en proporcionar simultáneamente un embebido profundo (para el razonamiento sintáctico) y embebidos superficiales (para la búsqueda de pruebas automatizada), probando su mutua fidelidad, particularmente cuando el dominio de los individuos es no contable y la asignación de variables en el embebido superficial está restringida a un conjunto contable (por ejemplo, los números naturales).

Metodología
Los autores extienden el entorno Isabelle/HOL para soportar FML bajo semántica de Kripke de dominio constante. La metodología emplea tres embebidos paralelos:

1. Embebido Profundo (Deep Embedding): Las fórmulas se representan como un tipo de dato inductivo $\mathcal{F}$. La verdad se define recursivamente sobre un modelo $\langle W, R, I, D \rangle$, una asignación $g$, y un mundo $w$. La validez ($ValD$) cuantifica universalmente sobre todos los modelos, asignaciones que respetan el dominio $D$, y mundos.
2. Embebido Superficial Máximo (Maximal Shallow Embedding): Las fórmulas se elevan a términos $\lambda$ abstrayendo explícitamente sobre todos los parámetros del modelo ($W, R, I, D, g, w$). Esto permite el uso directo de la automatización de Isabelle, pero resulta en tipos complejos.
3. Embebido Superficial Mínimo (Minimal Shallow Embedding): Implementado como un locale de Isabelle/HOL (MinS), este enfoque promueve los parámetros estáticos ($W, R, I, g$) a argumentos del locale, reduciendo el tipo de la fórmula a $w \Rightarrow bool$. Crucialmente, el cuantificador existencial se codifica utilizando el ligador de meta-nivel nativo de Isabelle, mientras que el operador modal desplaza el parámetro del mundo.

Para cerrar la brecha entre el embebido profundo y el superficial mínimo, los autores desarrollan una maquinaria de sustitución integral (predicados de variables libres/ligadas, sustitución que evita la captura, renombramiento alfabético) necesaria para manejar los cuantificadores de primer orden, la cual estaba ausente en el trabajo proposicional previo.

Una innovación técnica central es la mecanización del teorema de Löwenheim–Skolem descendente contable para FML. Este teorema garantiza que para cualquier modelo y cualquier subdominio inicial contable $D_0$, existe un subdominio elemental contable $\mathcal{N}$ que preserva la verdad. Esto se utiliza para resolver el problema de la suryectividad: dado que la asignación superficial mínima $g: V \to D$ (donde $V = \mathbb{N}$) no puede ser suryectiva sobre un dominio no contable $D$, la fidelidad directa falla. Al construir un subdominio elemental contable $\mathcal{N}$ sobre el cual $g$ puede ser suryectiva, y probar que la verdad en $D$ coincide con la verdad en $\mathcal{N}$, los autores recuperan la fidelidad sobre el dominio completo.

Contribuciones Clave

1. Desarrollo de MinFMLinHOL: Una teoría completa de Isabelle/HOL que cubre FML con átomos relacionales binarios, conectivas proposicionales, cuantificación existencial y el operador de caja bajo semántica de dominio constante.
2. Tres Embebidos: La provisión de un embebido profundo, un embebido superficial máximo y un embebido superficial mínimo ligero (empaquetado como un locale).
3. Teorema de Fidelidad Global: La introducción del locale MinS permite un teorema de fidelidad global fuerte, FaithfulMS_all, que establece que cuantificar sobre todas las interpretaciones superficiales mínimas recupera exactamente la validez profunda.
4. Maquinaria de Sustitución: El desarrollo de herramientas sintácticas necesarias (lemas de sustitución, renombramiento, inducción basada en tamaño) para el embebido profundo de FML, extendiendo el trabajo proposicional previo.
5. Teorema de Löwenheim–Skolem Mecanizado: La formalización del teorema de Löwenheim–Skolem descendente para la semántica de Kripke de dominio constante, que sustenta la automatización de la prueba de fidelidad entre los embebidos profundo y superficial mínimo.
6. Resolución de la Suryectividad: El diseño de un locale refinado MinS_surj que asume que la asignación es suryectiva sobre un subdominio elemental, elevando la fidelidad desde el rango de la asignación hacia el dominio completo $D$.

Resultados
El desarrollo se valida a través de varios experimentos:

• Verificación Axiomática: Confirmación del axioma-K, la regla de necesidad y la validez de las fórmulas Barcan y la fórmula de la Barcan inversa (que se cumplen bajo semántica de dominio constante).
• Correspondencias de Marcos (Frames): Verificación automatizada de las correspondencias entre marcos reflexivos, transitivos y simétricos y los esquemas de axiomas T, 4 y B.
• Automatización: Se demuestra el uso de las herramientas sledgehammer y nitpick. El embebido superficial mínimo permite que sledgehammer trate los objetivos modales de primer orden como objetivos ordinarios de HOL, mientras que nitpick puede encontrar contraejemplos reduciendo el tipo del dominio, evitando efectivamente las salvaguardas explícitas del dominio.

Significancia
El artículo afirma que este trabajo representa la extensión natural de las metodologías de embebido proposicional previas al caso de primer orden. Su principal significancia radica en demostrar que los embebidos profundos y superficiales pueden coexistir en una única teoría HOL con pruebas de fidelidad automatizadas, incluso en presencia de cuantificación de primer orden y dominios no contables. Al aprovechar el mecanismo de locale y el teorema de Löwenheim–Skolem, los autores superan la barrera técnica de la suryectividad de la asignación de variables, permitiendo el uso de potentes herramientas de automatización de HOL para la lógica modal de primer orden sin sacrificar el rigor de la representación sintáctica profunda. El trabajo establece una base para futuras extensiones, como la semántica de dominio variable o la inclusión de la igualdad, centrándose actualmente en el fragmento mínimo de dominio constante.