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

Technisches Resümee: Definierbarkeit funktionaler Eigenschaften in der basalen modal-temporalen Sprache über geordneten Frames

Problemstellung
Diese Arbeit untersucht die Ausdrucksstärke der basalen modal-temporalen Sprache $LT \times W$, die durch das Hinzufügen von Priors temporalen Operatoren $G$ (immer in der Zukunft) und $H$ (immer in der Vergangenheit) zur basalen modalen Sprache mit $\Box$ (in allen funktionalen Bildern) gebildet wird. Die Studie konzentriert sich auf die Definierbarkeit von neun spezifischen funktionalen Eigenschaften – Totalität, Nicht-Totalität, Injektivität, Surjektivität, Monotonie, strikte Monotonie, Antitonie, strikte Antitonie und Konstanz – über fünf verschiedene Ordnungstypen: Präordnungen (PRE), strikte Präordnungen (sPRE), partielle Ordnungen (PO), lineare Ordnungen (LO) und strikte lineare Ordnungen (sLO).

Eine zentrale Herausforderung ist das „Multiflow“-Setting, in dem mehrere Zugänglichkeitsfunktionen koexistieren und modale Operatoren wahllos über deren kombinierte Bilder quantifizieren. Vorherige Arbeiten (z. B. [1, 3]) hatten die Analyse auf strikte lineare Ordnungen und globale Einschränkungen wie die Eigenschaft des einheitlichen Definitionsbereichs (Uniform Domain, U-Dom) beschränkt. Diese Arbeit zielt darauf ab, zu bestimmen, ob diese Eigenschaften isoliert definierbar sind und wie sich ihre Definierbarkeit über ein breiteres Spektrum von Ordnungsstrukturen hinweg verändert, wobei insbesondere der Einfluss zweier semantischer Lesarten untersucht wird: der Standardinterpretation (einschließlich des aktuellen Augenblicks) und der strikten Interpretation (unter Ausschluss des aktuellen Augenblicks).

Methodik
Die Autoren wenden einen zweistufigen analytischen Ansatz an, um die Ausdrucksgrenzen von $LT \times W$ abzubilden:

1. Beliebiges geordnetes Multiflow-Setting: Die Studie etabliert zunächst die Grenzen der Definierbarkeit im allgemeinen Setting, in dem Frames aus beliebigen Familien von Funktionen bestehen. Hier agieren modale Operatoren als zweite Ordnung über die Vereinigung aller Funktionsbilder. Die Autoren nutzen surjektive p-Morphismen (die funktionale Bisimulationen induzieren), um die Undefinierbarkeit zu beweisen. Wenn ein p-Morphismus einen Frame, der eine Eigenschaft erfüllt, auf einen abbildet, der diese nicht erfüllt, ist die Eigenschaft undefinierbar.
2. Strukturelle Verfeinerung (Minimale Frames): Um die Quelle der Ausdrucksbeschränkungen zu isolieren, führen die Autoren „minimale funktionale Frames“ (die $O_2$-Familie) ein, welche die Frames auf höchstens zwei Flows und eine einzige Zugänglichkeitsfunktion beschränken. Diese Reduktion kollabiert die Komplexität zweiter Ordnung des Multiflow-Settings in eine relationale Lesart erster Ordnung.
3. Vergleichende Analyse: Die Studie vergleft die Ergebnisse minimaler Frames mit zwei anderen Frameworks:
   • Indizierte Sprachen: Wo Operatoren explizit gelabelt sind, um spezifische Funktionen zu unterscheiden.
   • Uniform Domain (U-Dom) Frames: Wo alle Funktionen in einem Frame einen gemeinsamen Definitionsbereich teilen.
4. Semantische Variationen: Die Analyse wird sowohl unter standardmäßigen ($G, H$) als auch unter strikten ($G^*, H^*$) Interpretationen durchgeführt, um zu bestimmen, ob der Ausschluss des aktuellen Augenblicks die Landschaft der Definierbarkeit verändert.

Zentrale Beiträge und Ergebnisse

• Ausdrucksgrenzen im Multiflow-Setting:
  In dem allgemeinen Multiflow-Setting ist die Sprache signifikant schwach. Die Studie beweist, dass nur Totalität und Surjektivität definierbar sind, und dies nur innerhalb linearer Ordnungen (LO und sLO). Alle anderen Eigenschaften (Injektivität, Monotonie, Konstanz usw.) sind in jedem Ordnungstyp, einschließlich linearer, undefinierbar. Dies wird der „wahllosen Quantifizierung“ über mehrere Funktionen zugeschrieben, welche die individuellen Verhaltensweisen der Funktionen verschleiert.

• Der Einfluss minimaler Frames:
  Durch die Beschränkung der Semantik auf minimale Frames (einzelne Funktion) erweitert sich die Landschaft der Definierbarkeit dramatisch:

  • Monotonie und Antitonie: Diese werden in allen Ordnungstypen definierbar (PRE, sPRE, PO, LO, sLO).
  • Injektivität: Wird in strikten linearen Ordnungen (sLO) unter der Standardinterpretation definierbar.
  • Strikte Monotonie/Antitonie: Werden in strikten Präordnungen und strikten linearen Ordnungen definierbar.
  • Konstanz: Bleibt selbst in minimalen Frames in nicht-linearen Ordnungen (PRE, sPRE, PO) undefinierbar, was ein Argument der distinkten semantischen Äquivalenz erfordert.

• Die Rolle der strikten Interpretation:
  Im allgemeinen Multiflow-Setting liefert die Wahl zwischen standardmäßiger und strikter Interpretation identische Ergebnisse. In minimalen Frames jedoch bietet die strikte Interpretation ($G^*, H^*$) entscheidende Gewinne:

  • Sie ermöglicht die Definition von Injektivität in linearen Ordnungen (LO), wo die Standardinterpretation scheitert.
  • Sie erlaubt die Definition von strikter Monotonie und strikter Antitonie in allen Ordnungstypen, einschließlich nicht-strikter (PRE, PO), indem sie diese effektiv als deren strikte Gegenstücke behandelt.

• Äquivalenz der Frameworks:
  Das Paper zeigt, dass die in minimalen Frames gewonnenen Definierbarkeitsmuster identisch mit denen der indizierten Sprachen (wo Funktionen syntaktisch unterschieden werden) und der Uniform Domain (U-Dom) Frames sind. Dies deutet darauf hin, dass die Ausdrucksbeschränkungen des ursprünglichen Frameworks nicht aus der Schwäche der Operatoren selbst resultieren, sondern aus der unkontrollierten Multiplizität von Funktionen mit divergierenden Definitionsbereichen. Sobald die funktionale Multiplizität kontrolliert wird (durch strukturelle Vereinfachung, einheitliche Definitionsbereiche oder syntaktische Indizierung), gewinnen die basalen Operatoren ihre volle Kapazität zurück.

• Fundamentale Hindernisse:
  Selbst nach der Kontrolle der funktionalen Multiplizität bleibt ein „harter Kern“ von Eigenschaften – Totalität, Nicht-Totalität, Injektivität, Surjektivität und Konstanz – in allen nicht-linearen Ordnungen (PRE, sPRE, PO) undefinierbar. Die Autoren kommen zu dem Schluss, dass der Mangel an Konnektivität (Inkomparabilität von Punkten) ein fundamentales Hindernis darstellt, das temporale Modalitäten nicht überwinden können, unabhängig von der Interpretation oder strukturellen Verfeinerung.

Bedeutung
Das Paper liefert eine systematische Klassifizierung der Ausdrucksgrenzen der basalen modal-temporalen Sprache über geordneten Frames. Seine primäre Bedeutung liegt in der Identifizierung der Tatsache, dass die Unfähigkeit, fundamentale funktionale Eigenschaften im ursprünglichen Multiflow-Setting zu definieren, ein strukturelles Artefakt unkontrollierter funktionaler Multiplizität ist und kein inhärenter Fehler der temporalen Operatoren.

Indem gezeigt wird, dass minimale Frames, indizierte Sprachen und U-Dom-Frames identische Definierbarkeitsmuster liefern, klärt die Arbeit die präzisen Bedingungen, unter denen funktionale Eigenschaften definierbar werden. Sie stellt fest, dass während strukturelle Vereinfachung die Definierbarkeit von Monotonie und Antitonie über alle Ordnungen hinweg wiederherstellen kann, der Mangel an linearer Konnektivität eine beständige Barriere für Eigenschaften bleibt, die globale Definitionsvergleiche (wie Totalität und Injektivität) erfordern, in nicht-linearen Strukturen. Die Studie hebt zudem den besonderen Status der Konstanz hervor, die der Standard-Undefinierbarkeit mittels p-Morphismen in minimalen Frames widersteht und ein einzigartiges Argument der semantischen Äquivalenz erfordert.