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

Resumo Técnico: Lógica Modal de Primeira Ordem em HOL: Embeddings Profundos e Rasos com Fidelidade Automatizada

Enunciado do Problema
A lógica modal de primeira ordem (FML) combina o poder expressivo da quantificação com a modalidade, servindo como um arcabouço crítico para aplicações em inteligência artificial, ciência da computação e filosofia. Embora os embeddings da lógica modal proposicional (PML) em lógica de ordem superior clássica (HOL) tenham sido automatizados com sucesso, estender essas técnicas para FML introduz uma complexidade significativa. Especificamente, a FML requer o tratamento de ligação de variáveis, substituição e quantificação sobre domínios que podem ser incontáveis. Trabalhos anteriores [5] estabeleceram uma metodologia de embedding profundo e raso para PML, mas não abordaram a maquinaria de substituição ou as questões de surjetividade inerentes à quantificação de primeira ordem. O desafio reside em fornecer simultaneamente um embedding profundo (para raciocínio sintático) e embeddings rasos (para busca de provas automatizada), enquanto se prova sua fidelidade mútua, particularmente quando o domínio de indivíduos é incontável e a atribuição de variáveis no embedding raso é restrita a um conjunto enumerável (por exemplo, números naturais).

Metodologia
Os autores estendem o ambiente Isabelle/HOL para suportar FML sob semântica de Kripke de domínio constante. A metodologia emprega três embeddings paralelos:

1. Embedding Profundo (Deep Embedding): As fórmulas são representadas como um tipo de dado indutivo $\mathcal{F}$. A verdade é definida recursivamente sobre um modelo $\langle W, R, I, D \rangle$, uma atribuição $g$ e um mundo $w$. A validade ($ValD$) quantifica universalmente sobre todos os modelos, atribuições que respeitam o domínio $D$ e mundos.
2. Embedding Raso Maximal (Maximal Shallow Embedding): As fórmulas são elevadas a termos $\lambda$ abstraindo explicitamente sobre todos os parâmetros do modelo ($W, R, I, D, g, w$). Isso permite o uso direto da automação do Isabelle, mas resulta em tipos complexos.
3. Embedding Raso Mínimo (Minimal Shallow Embedding): Implementado como uma locale do Isabelle/HOL (MinS), esta abordagem promove parâmetros estáticos ($W, R, I, g$) a argumentos da locale, reduzindo o tipo da fórmula para $w \Rightarrow bool$. Crucialmente, o quantificador existencial é codificado usando o ligador de meta-nível nativo do Isabelle, enquanto o operador modal desloca o parâmetro do mundo.

Para preencher a lacuna entre o embedding profundo e o embedding raso mínimo, os autores desenvolvem uma maquinaria de substituição abrangente (predicados de variáveis livres/ligadas, substituição que evita captura, renomeação alfabética) necessária para lidar com quantificadores de primeira ordem, que estava ausente no trabalho proposicional anterior.

Uma inovação técnica central é a mecanização do teorema de Löwenheim–Skolem descendente enumerável para FML. Este teorema garante que, para qualquer modelo e qualquer subdomínio inicial enumerável $D_0$, existe um subdomínio elementar enumerável $\mathcal{N}$ que preserva a verdade. Isso é usado para resolver o problema da surjetividade: como a atribuição raso-mínima $g: V \to D$ (onde $V = \mathbb{N}$) não pode ser surjetiva sobre um domínio incontável $D$, a fidelidade direta falha. Ao construir um subdomínio elementar enumerável $\mathcal{N}$ sobre o qual $g$ pode ser surjetiva, e provar que a verdade em $D$ coincide com a verdade em $\mathcal{N}$, os autores recuperam a fidelidade sobre o domínio completo.

Principais Contribuições

1. Desenvolvimento de MinFMLinHOL: Uma teoria completa de Isabelle/HOL que cobre FML com átomos relacionais binários, conectivos proposicionais, quantificação existencial e o operador de caixa (box) sob semântica de domínio constante.
2. Três Embeddings: A provisão de um embedding profundo, um embedding raso maximal e um embedding raso mínimo leve (empacotado como uma locale).
3. Teorema de Fidelidade Global: A introdução da locale MinS permite um teorema global forte, FaithfulMS_all, afirmando que quantificar sobre todas as interpretações raso-mínimas recupera exatamente a validade profunda.
4. Maquinaria de Substituição: O desenvolvimento de ferramentas sintáticas necessárias (lemmas de substituição, renomeação, indução baseada em tamanho) para o embedding profundo de FML, estendendo o trabalho proposicional anterior.
5. Teorema de Löwenheim–Skolem Mecanizado: A formalização do teorema de Löwenheim–Skolem descendente para semântica de Kripke de domínio constante, que sustenta a automação da prova de fidelidade entre os embeddings profundo e raso-mínimo.
6. Resolução de Surjetividade: O design de uma locale refinada MinS_surj que assume que a atribuição é surjetiva sobre um subdomínio elementar, elevando a fidelidade do alcance da atribuição para o domínio total $D$.

Resultos
O desenvolvimento é validado através de vários experimentos:

• Verificação Axiomática: Confirmação do axioma-K, da regra de necessidade e da validade das fórmulas Barcan e da contraparte de Barcan (que são válidas sob semântica de domínio constante).
• Correspondências de Quadros (Frame Correspondences): Verificação automatizada de correspondências entre quadros reflexivos, transitivos e simétricos e os esquemas de axiomas T, 4 e B.
• Automação: O uso das ferramentas sledgehammer e nitpick é demonstrado. O embedding raso-mínimo permite que o sledgehammer trate objetivos modais de primeira ordem como objetivos ordinários de HOL, enquanto o nitpick pode encontrar contraexemplos ao reduzir o tipo do domínio, efetivamente contornando as salvaguardas explícitas do domínio.

Significância
O artigo afirma que este trabalho representa a extensão natural das metodologias de embedding proposicional anteriores para o caso de primeira ordem. Sua principal significância reside em demonstrar que embeddings profundos e rasos podem coexistir em uma única teoria HOL com provas de fidelidade automatizadas, mesmo na presença de quantificação de primeira ordem e domínios incontáveis. Ao alavancar o mecanismo de locale e o teorema de Löwenheim–Skolem, os autores superam a barreira técnica da surjetividade da atribuição de variáveis, permitindo o uso de poderosas ferramentas de automação de HOL para lógica modal de primeira ordem sem sacrificar o rigor da representação sintática profunda. O trabalho estabelece uma base para futuras extensões, como semântica de domínio variável ou a inclusão de igualdade, focando atualmente no fragmento minimal de domínio constante.