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

Technische Samenvatting: Eerstelijns Modale Logica in HOL: Diepe en Ondiepe Embeddings met Geautomatiseerde Getrouwheid

Probleemstelling
Eerstelijns modale logica (FML) combineert de expressieve kracht van kwantificatie met modaliteit, en dient als een cruciaal kader voor toepassingen in kunstmatige intelligentie, informatica en filosofie. Hoewel de embeddings van propositionele modale logica (PML) naar klassieke hogere-orde logica (HOL) succesvol geautomatiseerd zijn, introduceert het uitbreiden van deze technieken naar FML aanzienlijke complexiteit. Specifiek vereist FML het afhandelen van variabele binding, substitutie en kwantificatie over domeinen die onaftelbaar kunnen zijn. Voorgaand werk [5] vestigde een diepe-en-ondiepe embedding-methodologie voor PML, maar sprak de substitutie-machinerie of de surjectiviteitsproblemen die inherent zijn aan eerstelijns kwantificatie niet aan. De uitdaging ligt in het gelijktijdig bieden van een diepe embedding (voor syntactische redenering) en ondiepe embeddings (voor geautomatiseerde bewijsoptimalisatie), terwijl men hun wederzijdse getrouwheid bewijst, met name wanneer het domein van individuen onaftelbaar is en de variabele toewijzing in de ondiepe embedding beperkt is tot een aftelbare verzameling (bijv. natuurlijke getallen).

Methodologie
De auteurs breiden de Isabelle/HOL-omgeving uit om FML te ondersteunen onder constant-domein Kripke-semantiek. De methodologie maakt gebruik van drie parallelle embeddings:

1. Diepe Embedding: Formulae worden gerepresenteerd als een inductief datatype $\mathcal{F}$. Waarheid wordt recursief gedefinieerd over een model $\langle W, R, I, D \rangle$, een toewijzing $g$, en een wereld $w$. Geldigheid ($ValD$) kwantificeert universeel over alle modellen, toewijzingen die het domein $D$ respecteren, en werelden.
2. Maximale Ondiepe Embedding: Formulae worden opgehoogd naar $\lambda$-termen die expliciet abstraheren over alle modelparameters ($W, R, I, D, g, w$). Dit maakt direct gebruik van Isabelle's automatisering mogelijk, maar resulteert in complexe typen.
3. Minimale Ondiepe Embedding: Geïmplementeerd als een Isabelle/HOL locale (MinS), promoot deze benadering statische parameters ($W, R, I, g$) naar locale-argumenten, waardoor het formule-type wordt gereduceerd tot $w \Rightarrow bool$. Cruciaal is dat de existentiële kwantificator wordt gecodeerd met behulp van Isabelle's natuurlijke meta-niveau binder, terwijl de modale operator de wereldparameter verschuift.

Om de kloof tussen de diepe en de minimale ondiepe embedding te overbruggen, ontwikkelen de auteurs een uitgebreide substitutie-machinerie (predicaten voor vrije/gebonden variabelen, foutloze substitutie, alfabetische hernoeming) die noodzakelijk is voor het afhandelen van eerstelijns kwantificatoren, wat ontbrak in het eerdere propositionele werk.

Een centrale technische innovatie is de mechanisering van de aftelbare neerwaartse Löwenheim–Skolem-stelling voor FML. Deze stelling garandeert dat er voor elk model en elke aftelbare initiële sub-domein $D_0$, een aftelbare elementaire sub-domein $\mathcal{N}$ bestaat die de waarheid behoudt. Dit wordt gebruikt om het surjectiviteitsprobleem op te lossen: aangezien de minimale ondiepe toewijzing $g: V \to D$ (waarbij $V = \mathbb{N}$) niet surjectief kan zijn op een onaftelbaar domein $D$, faalt directe getrouwheid. Door een aftelbare elementaire sub-domein $\mathcal{N}$ te construeren waarop $g$ wel surjectief kan zijn, en te bewijzen dat waarheid in $D$ samenvalt met waarheid in $\mathcal{N}$, herstellen de auteurs de getrouwheid over het volledige domein.

Belangrijkste Bijdragen

1. MinFMLinHOL Ontwikkeling: Een volledige Isabelle/HOL-theorie die FML dekt met binaire relationele atomen, propositionele connectieven, existentiële kwantificatie en de box-modaliteit onder constant-domein semantiek.
   2.Drie Embeddings: De voorziening van een diepe embedding, een maximale ondiepe embedding, en een lichte minimale ondiepe embedding (verpakt als een locale).
2. Globale Getrouwheidstheorema: De introductie van de MinS locale maakt een sterke globale stelling mogelijk, FaithfulMS_all, die stelt dat kwantificeren over alle minimale ondiepe interpretaties exact de diepe geldigheid herstelt.
3. Substitutie-machinerie: De ontwikkeling van noodzakelijke syntactische instrumenten (substitutie-lemma's, hernoeming, grootte-gebaseerde inductie) voor de diepe embedding van FML, ter uitbreiding van het eerdere propositionele werk.
4. Mechaniseerde Löwenheim–Skolem-stelling: De formalisering van de neerwaartse Löwenheim–Skolem-stelling voor constant-domein Kripke-semantiek, die de automatisering van het getrouwheidsbewijs tussen diepe en minimale ondiepe embeddings onderbouwt.
5. Surjectiviteit-oplossing: Het ontwerp van een verfijnde locale MinS_surj die aanneemt dat de toewijzing surjectief is op een elementaire sub-domein, waardoor getrouwheid wordt opgetild van het bereik van de toewijzing naar het volledige domein $D$.

Resultaten
De ontwikkeling wordt gevalideerd door verschillende experimenten:

• Axiomatische Verificatie: Bevestiging van het K-axioma, de necessitatie-regel, en de geldigheid van zowel de Barcan als de converse Barcan formules (die gelden onder constant-domein semantiek).
• Frame Correspondenties: Geautomatiseerde verificatie van correspondenties tussen reflexieve, transitieve en symmetrische frames en de T, 4, en B axioma-schema's.
• Automatisering: Het gebruik van de sledgehammer en nitpick tools wordt gedemonstreerd. De minimale ondiepe embedding stelt sledgehammer in staat om eerstelijns modale doelen als gewone HOL-doelen te behandelen, terwijl nitpick tegenvoorbeelden kan vinden door het domein-type te verkleinen, waardoor de expliciete domein-guards effectief worden omzeild.

Betekenis
Het artikel beweert dat dit werk de natuurlijke uitbreiding is van eerdere propositionele embedding-methodologieën naar het eerstelijns geval. De primaire betekenis ligt in het aantonen dat diepe en ondiepe embeddings kunnen samenbestaan in één enkele HOL-theorie met geautomatiseerde getrouwheidsbewijzen, zelfs in aanwezigheid van eerstelijns kwantificatie en onaftelbare domeinen. Door gebruik te maken van de locale-mechanisme en de Löwenheim–Skolem-stelling, overwinnen de auteurs de technische barrière van variabele toewijzing-surjectiviteit, wat het gebruik van krachtige HOL-automatiseringstools voor eerstelijns modale logica mogelijk maakt zonder de strengheid van de diepe syntactische representatie op te offeren. Het werk legt een fundament voor toekomstige uitbreidingen, zoals variërende-domein semantiek of de inclusie van gelijkheid, terwijl het momenteel focust op het minimale constant-domein fragment.