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

Sintesi Tecnica: Logica Modale del Primo Ordine in HOL: Embedding Profondi e Superficiali con Fedeltà Automatizzata

Problematica
La logica modale del primo ordine (FML) combina il potere espressivo della quantificazione con la modalità, fungendo da quadro critico per applicazioni nell'intelligenza artificiale, l'informatica e la filosofia. Sebbene gli embedding della logica modale proposizionale (PML) in la logica dell'ordine superiore classica (HOL) siano stati automatizzati con successo, l'estensione di tali tecniche alla FML introduce una complessità significativa. Nello specifico, la FML richiede la gestione del legame delle variabili, della sostituzione e della quantificazione su domini che possono essere incontabili. Lavori precedenti [5] hanno stabilito una metodologia di embedding profondo e superficiale per la PML, ma non hanno affrontato la meccanica della sostituzione o i problemi di suriettività inerenti alla quantificazione del primo ordine. La sfida consiste nel fornire simultaneamente un embedding profondo (per il ragionamento sintattico) e degli embedding superficiali (per la ricerca automatica delle prove), provando al contempo la loro mutua fedeltà, in particolare quando il dominio degli individui è incontabile e l'assegnazione delle variabili nell'embedding superficiale è limitata a un insieme numerabile (ad esempio, i numeri naturali).

Metodologia
Gli autori estendono l'ambiente Isabelle/HOL per supportare la FML sotto la semantica di Kripke a dominio costante. La metodologia impiega tre embedding paralleli:

1. Embedding Profondo (Deep Embedding): Le formule sono rappresentate come un tipo di dato induttivo $\mathcal{F}$. La verità è definita ricorsivamente su un modello $\langle W, R, I, D \rangle$, un'assegnazione $g$, e un mondo $w$. La validità ($ValD$) quantifica universalmente su tutti i modelli, le assegnazioni che rispettano il dominio $D$, e i mondi.
2. Embedding Superficiale Massimale (Maximal Shallow Embedding): Le formule sono sollevate a termini $\lambda$ che astraggono esplicitamente su tutti i parametri del modello ($W, R, I, D, g, w$). Ciò consente l'uso diretto dell'automazione di Isabelle, ma risulta in tipi complessi.
3. Embedding Superficiale Minimo (Minimal Shallow Embedding): Implementato come una locale di Isabelle/HOL (MinS), questo approccio promuove i parametri statici ($W, R, I, g$) ad argomenti della locale, riducendo il tipo della formula a $w \Rightarrow bool$. Crucialmente, il quantificatore esistenziale è codificato utilizzando il binder meta-livello nativo di Isabelle, mentre l'operatore modale sposta il parametro del mondo.

Per colmare il divario tra l'embedding profondo e quello superficiale minimo, gli autori sviluppano una completa meccanica di sostituzione (predicati di variabili libere/legate, sostituzione che evita la cattura, rinomina alfabetica) necessaria per gestire i quantificatori del primo ordine, che era assente nel precedente lavoro proposizionale.

Un'innovazione tecnica centrale è la meccanizzazione del teorema di Löwenheim–Skolem discendente numerabile per la FML. Questo teorema garantisce che per ogni modello e per ogni sottodominio iniziale numerabile $D_0$, esiste un sottodominio elementare numerabile $\mathcal{N}$ che preserva la verità. Ciò viene utilizzato per risolvere il problema della suriettività: poiché l'assegnazione superficiale minima $g: V \to D$ (dove $V = \mathbb{N}$) non può essere suriettiva su un dominio incontabile $D$, la fedeltà diretta fallisce. Costruendo un sottodominio elementare numerabile $\mathcal{N}$ sul quale $g$ può essere suriettiva, e provando che la verità in $D$ coincide con la verità in $\mathcal{N}$, gli autori recuperano la fedeltà sull'intero dominio.

Contributi Chiave

1. Sviluppo di MinFMLinHOL: Una teoria completa di Isabelle/HOL che copre la FML con atomi relazionali binari, connettivi proposizionali, quantificazione esistenziale e l'operatore box sotto la semantica a dominio costante.
2. Tre Embedding: La fornitura di un embedding profondo, di un embedding superficiale massimale e di un embedding superficiale minimo leggero (impacchettato come una locale).
3. Teorema di Fedeltà Globale: L'introduzione della locale MinS consente un teorema globale forte, FaithfulMS_all, che afferma che quantificare su tutte le interpretazioni superficiali minime recupera esattamente la validità profonda.
4. Meccanica di Sostituzione: Lo sviluppo degli strumenti sintetici necessari (lemmi di sostituzione, rinomina, induzione basata sulla dimensione) per l'embedding profondo della FML, estendendo il precedente lavoro proposizionale.
5. Teorema di Löwenheim–Skolem Meccanizzato: La formalizzazione del teorema discendente di Löwenheim–Skolem per la semantica di Kripke a dominio costante, che sostiene l'automazione della prova di fedeltà tra l'embedding profondo e quello superficiale minimo.
6. Risoluzione della Suriettività: Il design di una locale raffinata MinS_surj che assume che l'assegnazione sia suriettiva su un sottodominio elementare, elevando la fedeltà dall'intervallo dell'assegnazione all'intero dominio $D$.

Risultati
Lo sviluppo è validato attraverso diversi esperimenti:

• Verifica Assiomatica: Conferma dell'assioma K, della regola di necessità, e della validità sia dei formulati Barcan che di quelli di conversa Barcan (che valgono sotto la semantica a dominio costante).
• Corrispondenze di Frame: Verifica automatizzata delle corrispondenze tra frame riflessivi, transitivi e simmetrici e gli schemi assiematici T, 4 e B.
• Automazione: L'uso degli strumenti sledgehammer e nitpick è dimostrato. L'embedding superficiale minimo consente a sledgehammer di trattare gli obiettivi modali del primo ordine come ordinari obiettivi HOL, mentre nitpick può trovare controesempi restringendo il tipo di dominio, bypassando efficacemente le esplicite guardie del dominio.

Significatività
Il documento sostiene che questo lavoro rappresenti l'estensione naturale delle metodologie di embedding proposizionale pregresse al caso del primo ordine. La sua significatività primaria risiede nel dimostrare che gli embedding profondi e superficiali possono coesistere in una singola teoria HOL con prove di fedeltà automatizzate, anche in presenza di quantificazione del primo ordine e domini incontabili. Sfruttando il meccanismo della locale e il teorema di Löwenheim–Skolem, gli autori superano l'ostacolo tecnico della suriettività dell'assegnazione delle variabili, abilitando l'uso di potenti strumenti di automazione HOL per la logica modale del primo ordine senza sacrificare il rigore della rappresentazione sintattica profonda. Il lavoro stabilisce una base per estensioni future, come la semantica a dominio variabile o l'inclusione dell'uguaglianza, concentrandosi attualmente sul frammento minimo a dominio costante.