Definability of Functional Properties in the Basic Modal-Temporal Language over Ordered Frames

Technische Samenvatting: Definieerbaarheid van Functionele Eigenschappen in de Basale Modale-Temporele Taal over Geordende Frames

Probleemstelling
Dit artikel onderzoekt de expressieve kracht van de basale modale-temporele taal $LT \times W$, gevormd door het toevoegen van de temporele operatoren $G$ (altijd in de toekomst) en $H$ (altijd in het verleden) van Prior aan de basale modale taal met $\Box$ (in alle functionele afbeeldingen). De studie richt zich op de definieerbaarheid van negen specifieke functionele eigenschappen—totaliteit, niet-totaliteit, injectiviteit, surjectiviteit, monotoniciteit, strikte monotoniciteit, antitoniciteit, strikte antitoniciteit en constantie—over vijf verschillende ordentypen: preorders (PRE), strikte preorders (sPRE), partiële orden (PO), lineaire orden (LO) en strikte lineaire orden (sLO).

Een centrale uitdaging die wordt aangepakt is de "multiflow"-setting, waarbij meerdere toegankelijkheidsfuncties samenbestaan en modale operatoren ononderscheidenlijk kwantificeren over hun gecombineerde afbeeldingen. Vorig werk (bijv. [1, 3]) had de analyse beperkt tot strikte lineaire orden en globale restricties zoals de Uniform Domain (U-Dom) eigenschap. Dit artikel beoogt te bepalen of deze eigenschappen in isolatie definieerbaar zijn en hoe hun definieerbaarheid varieert over een breder spectrum van ordestructuren, waarbij specifiek de impact van twee semantische interpretaties wordt onderzocht: de standaardinterpretatie (inclusief het huidige moment) en de strikte interpretatie (exclusief het huidige moment).

Methodologie
De auteurs hanteren een tweestaps analytische benadering om de expressieve grenzen van $LT \times W$ in kaart te brengen:

1. Algemene Geordende Multiflow Setting: De studie stelt eerst de definieerbaarheidslimieten vast in de algemene setting waar frames bestaan uit willekeurige families van functies. Hierbij fungeren modale operatoren als tweede-orde kwantoren over de unie van alle functionele afbeeldingen. De auteurs maken gebruik van surjectieve p-morfismen (die functionele bisimulaties induceren) om ondefinieerbaarheid te bewijzen. Als een p-morfisme een frame dat een eigenschap bezit afbeeldt op een frame dat die eigenschap niet bezit, dan is de eigenschap ondefinieerbaar.
2. Structurele Verfijning (Minimale Frames): Om de bron van de expressieve beperkingen te isoleren, introduceren de auteurs "minimale functionele frames" (de $O_2$-familie), waarbij de frames worden beperkt tot maximaal twee flows en een enkele toegankelijkheidsfunctie. Deze reductie brengt de tweede-orde complexiteit van de multiflow-setting terug naar een eerste-orde relationele lezing.
3. Comparatieve Analyse: De studie vergelijkt de resultaten van minimale frames met twee andere kaders:
   • Geïndexeerde Talen: Waarbij operatoren expliciet gelabeld zijn om specifieke functies te onderscheiden.
   • Uniform Domain (U-Dom) Frames: Waarbij alle functies in een frame een gemeenschappelijk domein delen.
4. Semantische Variaties: De analyse wordt uitgevoerd onder zowel standaard ($G, H$) als strikte ($G^*, H^*$) interpretaties om te bepalen of het uitsluiten van het huidige moment het landschap van definieerbaarheid verandert.

Belangrijkste Bijdragen en Resultaten

• Expressieve Limieten in de Multiflow Setting:
  In de algemene multiflow-setting is de taal aanzienlijk zwak. De studie bewijst dat alleen totaliteit en surjectiviteit definieerbaar zijn, en alleen binnen lineaire orden (LO en sLO). Alle andere eigenschappen (injectiviteit, monotoniciteit, constantie, etc.) zijn ondefinieerbaar in elke ordentype, inclusief lineaire orden. Dit wordt toegeschreven aan de "ononderscheidelijke kwantificering" over meerdere functies, wat het gedrag van individuele functies vertroebelt.

• De Impact van Minimale Frames:
  Door de semantiek te beperken tot minimale frames (enkele functie), breidt het landschap van definieerbaarheid zich dramatisch uit:

  • Monotoniciteit en Antitoniciteit: Deze worden definieerbaar in alle ordentypen (PRE, sPRE, PO, LO, sLO).
  • Injectiviteit: Wordt definieerbaar in strikte lineaire orden (sLO) onder de standaardinterpretatie.
  • Strikte Monotoniciteit/Antitoniciteit: Worden definieerbaar in strikte preorders en strikte lineaire orden.
  • Constantie: Blijft ondefinieerbaar in niet-lineaire orden (PRE, sPRE, PO), zelfs in minimale frames, wat een afwijkend argument voor semantische equivalentie vereist (aangezien het behouden blijft onder p-morfismen).

• De Rol van de Strikte Interpretatie:
  In de algemene multiflow-setting levert de keuze tussen standaard en strikte interpretaties identieke resultaten op. Echter, in minimale frames biedt de strikte interpretatie ($G^*, H^*$) cruciale winst:

  • Het maakt de definitie van injectiviteit mogelijk in lineaire orden (LO) waar de standaardinterpretatie faalt.
  • Het staat de definitie van strikte monotoniciteit en strikte antitoniciteit toe in alle ordentypen, inclusief niet-strikte (PRE, PO), door ze effectief te behandelen als hun strikte tegenhangers.

• Equivalentie van Kaders:
  Het artikel toont aan dat de definieerbaarheidspatronen verkregen in minimale frames identiek zijn aan die in geïndexeerde talen (waar functies syntactisch onderscheiden worden) en Uniform Domain (U-Dom) frames. Dit geeft aan dat de expressieve beperkingen van het oorspronkelijke kader niet voortkomen uit de zwakte van de operatoren zelf, maar uit de ongecontroleerde veelheid van functies met uiteenlopende domeinen. Zodra de functionele veelheid wordt gecontroleerd (via structurele vereenvoudiging, domeinuniformiteit of syntactische indexering), herstellen de basale operatoren hun volledige capaciteit.

• Fundamentele Obstakels:
  Zelfs na het controleren van de functionele veelheid, blijft een "harde kern" van eigenschappen—totaliteit, niet-totaliteit, injectiviteit, surjectiviteit en constantie—ondefinieerbaar in alle niet-lineaire orden (PRE, sPRE, PO). De auteurs concluderen dat het gebrek aan connectiviteit (onvergelijkbaarheid van punten) een fundamenteel obstakel is dat temporele modaliteiten niet kunnen overwinnen, ongeacht de interpretatie of structurele verfijning.

Significantie
Het artikel biedt een systematische classificatie van de expressieve limieten van de basale modale-temporele taal over geordende frames. De primaire significantie ligt in het identificeren dat het onvermogen om fundamentele functionele eigenschappen te definiëren in de oorspronkelijke multiflow-setting een structureel artefact is van ongecontroleerde functionele veelheid, en niet een inherente tekortkoming van de temporele operatoren.

Door aan te tonen dat minimale frames, geïndexeerde talen en U-Dom-frames identieke definieerbaarheidspatronen opleveren, verheldert het werk de precieze condities waaronder functionele eigenschappen definieerbaar worden. Het stelt vast dat hoewel structurele vereenvoudiging de definieerbaarheid van monotoniciteit en antitoniciteit over alle orden kan herstellen, het gebrek aan lineaire connectiviteit een hardnekkige barrière blijft voor eigenschappen die globale domeinvergelijkingen vereisen (zoals totaliteit en injectiviteit) in niet-lineaire structuren. De studie benadrukt ook de bijzondere status van constantie, die standhoudt tegen standaard ondefinieerbaarheidsbewijzen via p-morfismen in minimale frames, wat een uniek argument voor semantische equivalentie vereist.