🔢 mathematics

Doctrinal Semantics of Directed First-Order Logic

Dieser Beitrag stellt eine gerichtete Prädikatenlogik erster Stufe mit asymmetrischer Gleichheit und einem auf Polarität basierenden syntaktischen System vor, das eine korrekte und vollständige kategorische Semantik mittels „gerichteter Doktrinen" bereitstellt, die gerichtete Gleichheit als relativen linken Adjungierten charakterisieren und Lawvers klassische Gleichheit verallgemeinern.

Ursprüngliche Autoren: Andrea Laretto, Fosco Loregian, Niccolò Veltri

Veröffentlicht 2026-05-12

📖 6 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Andrea Laretto, Fosco Loregian, Niccolò Veltri

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen, einen Satz von Regeln für ein Spiel zu schreiben, in dem sich Dinge ändern können, wobei die Regeln für „Änderung" sich von den Regeln für „Gleichheit" unterscheiden.

In der klassischen Logik (der in Mathematik und Informatik verwendeten) ist Gleichheit wie ein Spiegel. Wenn $A$ gleich $B$ ist, dann ist $B$ automatisch gleich $A$ . Es ist eine zweispurige Straße. In der realen Welt sind jedoch viele Dinge gerichtet. Wenn Sie ein Dokument umschreiben, gehen Sie von Version 1 zu Version 2. Sie können nicht einfach magisch ohne erneute Arbeit zu Version 1 zurückkehren. Wenn Sie einen Prozess haben, der ein rohes Ei in ein gekochtes Ei verwandelt, funktioniert dieser Prozess nicht rückwärts.

Dieser Artikel stellt eine neue Art von Logik vor, die gerichtete Prädikatenlogik erster Stufe genannt wird. Denken Sie daran als an ein Regelbuch für eine Welt, in der „Gleichheit" tatsächlich eine Einbahnstraße oder eine „Umschreibung" ist.

Hier ist die Aufschlüsselung ihrer Ideen mit einfachen Analogien:

1. Das Problem: Der „Spiegel" versus der „Pfeil"

In der traditionellen Logik sagen Sie mit „x gleich y", dass sie austauschbar sind.

Der Spiegel: Wenn ich einen Spiegel vor Sie halte, sieht Ihr Spiegelbild genau so aus wie Sie. Wenn ich Sie mit Ihrem Spiegelbild vertausche, ändert sich nichts.
Der Pfeil: In dieser neuen Logik ist die Beziehung ein Pfeil ( $x \le y$ ). Es bedeutet „x kann zu y werden" oder „x wird zu y umgeschrieben". Aber Sie können nicht notwendigerweise von $y$ zurück zu $x$ gehen.

Die Autoren wollten ein Logiksystem aufbauen, das diese Pfeile als fundamentale Bausteine behandelt, anstatt sie nur als nachträglichen Einfall hinzuzufügen.

2. Die Lösung: „Polarität" (Die Ampeln)

Die größte Kopfschmerzen bei der Erstellung dieser Logik ist die Verfolgung der Richtung.
Stellen Sie sich eine Kreuzung vor.

Positive Variablen sind Autos, die vorwärts fahren.
Negative Variablen sind Autos, die rückwärts fahren (oder die Straße aus der entgegengesetzten Richtung betrachten).
Dinaturale Variablen sind Autos, die in beide Richtungen fahren können, aber nur, wenn sie vorsichtig sind.

In der klassischen Logik müssen Sie sich keine Sorgen machen, in welche Richtung ein Auto zeigt; es ist einfach ein Auto. In dieser neuen Logik haben die Autoren ein System der Polaritäten erfunden. Sie teilen den „Kontext" (die Liste der verfügbaren Variablen) in drei separate Spuren auf:

Die negative Spur: Variablen hier können nur in „rückwärtigen" Positionen verwendet werden.
Die positive Spur: Variablen hier können nur in „vorwärtigen" Positionen verwendet werden.
Die dinaturale Spur: Variablen hier sind speziell; sie können in beiden Spuren erscheinen, müssen aber an beiden Stellen dieselbe Variable sein (wie ein Auto, das gleichzeitig vorwärts und rückwärts in einer Schleife fährt).

Dieses System wirkt wie ein strenger Verkehrspolizist. Es verhindert, dass Sie versehentlich eine Regel schreiben, die besagt: „Wenn A zu B wird, dann wird B zu A" (was die Einbahnstraßennatur der Logik brechen würde). Es zwingt die Logik, die Richtung des Pfeils zu respektieren.

3. Der „Magische Trick": Relative Adjunktionen

Der Artikel verwendet ein ausgefeiltes mathematisches Konzept namens „Adjunktion", um zu erklären, wie Gleichheit funktioniert.

Alte Logik: Gleichheit ist wie eine Maschine, die zwei Variablen nimmt und sie zu einer zusammendrückt.
Neue Logik: Da die Pfeile einseitig sind, können Sie sie nicht einfach zusammendrücken. Sie benötigen eine Maschine, die zwei Variablen nimmt (eine mit Blick nach vorne, eine mit Blick nach hinten) und sie zu einer einzigen „Schleifen"-Variable zusammendrückt.

Die Autoren beweisen, dass diese „gerichtete Gleichheit" angesichts der Verkehrsregeln (der Polaritäten) der bestmögliche Weg ist, dieses Zusammendrücken durchzuführen. Sie nennen dies einen „Relativen Linken Adjunkten". In einfacher Sprache: Es ist der effizienteste Weg, ein vorwärtsbewegtes Ding und ein rückwärtsbewegtes Ding in eine einzige Einheit zu kombinieren, ohne die Regeln des Systems zu brechen.

4. Die „Doktrinen" (Das Regelbuch)

Um sicherzustellen, dass ihre Logik tatsächlich funktioniert, haben sie eine „Doktrinale Semantik" aufgebaut.
Stellen Sie sich eine Doktrin als ein Wörterbuch vor, das die abstrakten Regeln der Logik in eine konkrete Welt übersetzt.

In ihrer Welt sind Typen Vorordnungen.
- Was ist eine Vorordnung? Stellen Sie sich eine Liste von Elementen vor, bei denen einige „kleiner oder gleich" anderen sind, aber nicht alles vergleichbar ist. Zum Beispiel ist in einem Videospiel „Level 1" kleiner als „Level 2", aber „Level 1" ist nicht unbedingt direkt kleiner als „Level 3" (Sie könnten es überspringen).
Sie bewiesen, dass ihre Logik korrekt und vollständig ist.
- Korrekt: Wenn Sie etwas in ihrem Regelbuch beweisen können, ist es in der realen Welt (der Vorordnungs-Welt) wahr.
- Vollständig: Wenn etwas in der realen Welt wahr ist, können Sie es mit ihrem Regelbuch beweisen.

5. Warum dies wichtig ist (laut dem Artikel)

Die Autoren zeigen, dass diese Logik perfekt geeignet ist, um Dinge zu beschreiben, die in Schritten oder Prozessen geschehen, wie zum Beispiel:

Umschreibung: Einen Satz in einem Dokument ändern.
Graph-Umschreibung: Die Verbindungen in einem Netzwerk ändern (wie ein soziales Netzwerk oder eine Schaltung).
Petri-Netze: Eine Möglichkeit zu modellieren, wie Ressourcen durch ein System fließen (wie Kunden in einer Bank oder Token in einem Spiel).

Sie erwähnen speziell, dass diese Logik beweisunabhängig ist. Das bedeutet, ihnen ist nicht wichtig, wie Sie von A nach B gelangt sind (der spezifische Pfad oder Beweis), sondern nur, dass Sie von A nach B gelangen können. Dies unterscheidet sich von einigen fortgeschrittenen Theorien der Informatik, die jeden einzelnen Schritt der Reise beachten.

Zusammenfassung

Die Autoren haben eine neue Sprache für die Logik entwickelt, die „Änderung" als Einbahnstraße behandelt. Um den Verkehr korrekt fließen zu lassen, haben sie ein System von „Spuren" (Polaritäten) erfunden, um sicherzustellen, dass Variablen nicht verwirrt werden, in welche Richtung sie zeigen. Sie bewiesen, dass dieses System mathematisch solide ist und perfekt zu einer Welt passt, in der Dinge geordnet, aber nicht notwendigerweise symmetrisch sind (wie eine To-do-Liste oder ein Spielverlauf).

Sie haben dies nicht erfunden, um Krankheiten zu heilen oder direkt neue Apps zu bauen; sie taten es, um eine fundamentale Lücke in der Art und Weise zu schließen, wie Mathematiker und Informatiker die Logik der „gerichteten" Änderung verstehen.

Technische Zusammenfassung: Doktrinale Semantik der gerichteten Prädikatenlogik erster Stufe

1. Problemstellung

Der Beitrag adressiert die Herausforderung, gerichtete Gleichheit innerhalb eines logischen Rahmens zu formalisieren. Während Lawvers kategorialer Blickwinkel die klassische Gleichheit erfolgreich als linker Adjunkt zur Kontraktion charakterisierte, stützt sich dieser Ansatz auf Symmetrie. In der gerichteten Typtheorie, wo Typen als Kategorien (oder Preordnungen) und nicht als Gruppoiden (oder Mengen) interpretiert werden, wird Gleichheit zu einer asymmetrischen Relation (z. B. eine Umformung $a \to b$ oder eine Ordnung $a \le b$ ).

Die Kernschwierigkeit liegt im Umgang mit Varianz (Polarität). In einer gerichteten Umgebung kann eine Variable in einer „negativen" Position (kontravariant, z. B. die Quelle eines Morphismus) oder in einer „positiven" Position (kovariant, z. B. das Ziel) auftreten. Standardlogische Regeln für Gleichheit (Reflexivität und die J-Regel/Elimination) versagen in diesem Kontext, da sie implizit Symmetrie voraussetzen oder zulassen, dass Variablen gleichzeitig in beiden Polaritäten auftreten, was zur Herleitung von Symmetrie führen würde ( $a \le b \vdash b \le a$ ), was in der gerichteten Logik ungültig ist. Frühere Versuche einer gerichteten Typtheorie kämpfen oft mit diesen Polaritätsbeschränkungen, insbesondere im Kontext beweisirrelevanter Logik (wo Gleichheit eine Proposition und nicht ein Typ mit mehreren Inhabern ist).

2. Methodik

Die Autoren entwickeln eine gerichtete Prädikatenlogik erster Stufe (dFOL) und ihre doktrinale Semantik durch eine Verallgemeinerung von Lawvers Rahmenwerk der Hyperdoktrinen.

Syntax: Polarisierter Kontext

Die Syntax führt einen polarisierten Kontext $[\Theta \mid \Delta \mid \Gamma]$ ein, der Variablen basierend auf ihrer Varianz in drei Mengen partitioniert:

$\Theta$ (Negativ): Variablen, die ausschließlich in kontravarianten Positionen auftreten.
$\Gamma$ (Positiv): Variablen, die ausschließlich in kovarianten Positionen auftreten.
$\Delta$ (Dinatural): Variablen, die in beiden Positionen auftreten (oder als solche behandelt werden dürfen).

Wesentliche syntaktische Merkmale umfassen:

Gerichtete Gleichheit ( $\le_A$ ): Eine primitive Relation $s \le_A t$ , wobei $s$ im negativen Kontext und $t$ im positiven Kontext typisiert ist.
Polarisierte Implikation: Die Implikation $\psi \Rightarrow \phi$ tauscht die Polarität des Kontexts für $\psi$ aus (verschiebt sie von der linken auf die rechte Seite des Turnstils), was die Kontravarianz des ersten Arguments widerspiegelt.
Polarisierte Quantoren: Quantoren ( $\forall^p, \exists^p$ ) sind durch die Polarität $p \in \{-, \Delta, +\}$ indiziert, um die Varianz der gebundenen Variable zu verfolgen.
Substitutionsregeln: Ein spezialisierter Substitutionsmechanismus (Definition 2.7) behandelt die Neuindizierung von Termen über polarisierte Kontexte hinweg und stellt sicher, dass dinaturale Variablen konsistent substituiert werden.

Semantik: Gerichtete Doktrinen

Die Semantik wird über gerichtete Doktrinen erfasst, eine Verallgemeinerung von Lawvers Doktrinen.

Basis-Kategorie: Anstelle einer Standardkategorie von Typen ist die Basis eine Polarisationskategorie $ndp(\mathcal{C})$ , deren Objekte Tripel $(\Theta, \Delta, \Gamma)$ sind und deren Morphismen die Varianzstruktur respektieren.
Faserstruktur: Ein Funktor $P: ndp(\mathcal{C})^{op} \to \mathbf{Pos}$ bildet polarisierte Kontexte auf Posets von Formeln ab.
Wesentliche Bedingungen:
- Keine-dinaturale-Varianz (ndv): Eine Bedingung, die sicherstellt, dass dinaturale Variablen in Prädikaten nur durch das Zusammenführen positiver und negativer Variablen entstehen und keine „dritte" Art von Varianz zulassen.
- Relative Adjunktionen: Gerichtete Gleichheit wird nicht als Standard-linker Adjunkt charakterisiert, sondern als linker relativer Adjunkt zu einer kontraktionsähnlichen Operation, die zwei Variablen entgegengesetzter Polarität zu einer einzigen dinaturalen Variable zusammenführt. Dies erfasst die syntaktische Beschränkung, die die Herleitung von Symmetrie verhindert.
- Polarisierte Implikation: Charakterisiert als relativer Koadjunkt.

3. Wesentliche Beiträge

Syntax von dFOL: Ein präzises natürlicher Deduktionssystem für Prädikatenlogik erster Stufe mit gerichteter Gleichheit, das ein rigoroses System von Polaritäten bietet, inspiriert durch Dinaturalität. Dieses System verbietet explizit die Herleitung von Symmetrie für gerichtete Gleichheit, während es Standardlogische Konnektive beibehält.
Charakterisierung gerichteter Gleichheit: Der Beitrag verallgemeinert Lawvers „Gleichheit als linker Adjunkt" zu gerichteter Gleichheit als linker relativer Adjunkt. Dies liefert eine präzise kategoriale universelle Eigenschaft für gerichtete Gleichheit, die die Asymmetrie der Relation berücksichtigt.
Gerichtete Doktrinen: Die Einführung gerichteter Doktrinen als semantischer Rahmen. Die Autoren beweisen, dass die Syntax von dFOL bezüglich dieser Semantik korrekt und vollständig ist.
Preordnungs-Vollständigkeit: Ein spezifisches Vollständigkeitsresultat wird für den klassischen Fragment von dFOL bezüglich des Standardmodells der Preordnungen ( $\mathbf{Preord}$ ) bewiesen. Dies etabliert, dass jede Folgerung, die in allen Preordnungsmodellen gültig ist, in der Syntax herleitbar ist.
Umgang mit Polarität: Der Beitrag zeigt, wie Varianz in einem beweisirrelevanten Setting gehandhabt werden kann, und unterscheidet dies von beweisrelevanten gerichteten Typtheorien (wie denen in $\mathbf{Cat}$ ) durch die Verwendung von poset-faserten Fibrationen und fasern mit Poset-Werten.

4. Ergebnisse

Korrektheit und Vollständigkeit: Die Autoren etablieren eine Bi-Adjunktion zwischen der Kategorie der Theorien ( $\mathbf{Theory}$ ) und der 2-Kategorie der gerichteten Doktrinen ( $\mathbf{DDoctrine}$ ). Dies impliziert, dass dFOL die interne Sprache gerichteter Doktrinen ist.
Vollständigkeit für Preordnungen: Unter Verwendung einer für polarisierte Kontexte angepassten Henkin-artigen Konstruktion beweist der Beitrag, dass der klassische Fragment von dFOL bezüglich des Modells der Preordnungen vollständig ist. Die Konstruktion definiert den Bereich des Modells als die Menge der geschlossenen Terme, geordnet durch die Herleitbarkeit gerichteter Gleichheit ( $\le_A$ ).
Abgeleitete Regeln: Das System unterstützt abgeleitete Regeln für Transitivität, Reflexivität und Kongruenz gerichteter Gleichheit sowie Interaktionsregeln zwischen polarisierten Quantoren und Implikation.
Gegenbeispiele: Der Beitrag illustriert, dass Symmetrie ( $a \le b \vdash b \le a$ ) nicht herleitbar ist, und das Preordnungsmodell dient als Gegenmodell für solche Herleitungen.

5. Bedeutung und Behauptungen

Der Beitrag beansprucht, die Arbeit Lawvers über die Rolle von Varianz und Hom-Funktoren in der Logik voranzutreiben. Spezifisch:

Er bietet eine präzise syntaktische und semantische Charakterisierung gerichteter Gleichheit in einem beweisirrelevanten Setting und schließt eine Lücke zwischen klassischer Logik und gerichteter Typtheorie.
Er verallgemeinert das Konzept der Gleichheit als Adjunkt auf den gerichteten Fall durch relative Adjunktionen und bietet ein neues kategoriales Werkzeug zum Verständnis gerichteter Strukturen.
Er zeigt, dass gerichtete Logik mit Standardlogischen Techniken (wie Henkin-Vollständigkeit) behandelt werden kann, indem Polaritäten sorgfältig durch polarisierte Kontexte verwaltet werden, anstatt komplexe geometrische oder höher-kategoriale Maschinen zu erfordern.
Die Arbeit wird als grundlegender Schritt für das Schließen über Umformungssysteme und gerichtete Phänomene (Prozesse, Übergänge) innerhalb eines logischen Rahmens positioniert, getrennt von den beweisrelevanten Ansätzen der Homotopie-Typtheorie.

Die Autoren stellen explizit fest, dass ihr Fokus auf dem beweisirrelevanten Fall liegt, gerechtfertigt durch die Natur der Umformungslogik (wo eine Umformung entweder stattfindet oder nicht) und die Verwendung von poset-faserten Fibrationen in der kategorialen Logik. Sie beanspruchen nicht, die volle Komplexität der abhängigen gerichteten Typtheorie zu lösen, sondern bieten ein robustes Fundament für den Fall der Prädikatenlogik erster Stufe auf Preordnungs-Basis.