💻 computer science

Inference-Behaviour Semantics for All $^\ast$ Connectives in Two-Dimensional Sequent Calculi

Diese Arbeit validiert den neuen Ansatz der Inferenz-Verhaltens-Semantik (I-bS), indem sie systematisch über 10.000 Konnektorenregelpaare in zweidimensionalen Sequenzenkalkülen analysiert, um 21 bedeutsame Konnektoren zu identifizieren und deren semantische Interrelationen über verschiedene logische Systeme hinweg präzise abzubilden, wobei sich zeigt, dass intuitionistische Konnektoren exakt die Hälfte der Bedeutung ihrer klassischen Gegenstücke erfassen.

Ursprüngliche Autoren: Sophie Nagler

Veröffentlicht 2026-07-23

📖 6 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Sophie Nagler

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 zu verstehen, was ein Wort wirklich bedeutet. Sie denken vielleicht, es ginge um die Wörterbuchdefinition, aber eine Gruppe von Philosophen und Logikern argumentiert, dass Bedeutung eigentlich über den Gebrauch definiert wird. Es ist wie beim Erlernen des Fahrradfahrens: Man versteht „Fahrradfahren“ nicht, indem man ein Handbuch lift; man versteht es dadurch, wie man tritt, das Gleichgewicht hält und lenkt. In der Welt der formalen Logik sind diese „Wörter“ Symbole, die Junktoren genannt werden (wie „und“, „oder“, „nicht“ und „wenn“). Jahrzehntelang haben Logiker versucht herauszufinden, was die wahre Bedeutung dieser Symbole ist, indem sie die Regeln untersuchten, die ihre Verwendung in Beweisen bestimmen. Dieses Feld wird beweistheoretische Semantik genannt. Die große Frage lautet: Wenn wir die Regeln des Spiels ändern (die Logik), ändern sich dann die Bedeutungen der Wörter? Oder gibt es einen festen, unveränderlichen „Kern“ oder eine „Seele“ jeder Junktor, die unabhängig vom Kontext gleich bleibt?

Diese Arbeit taucht tief in diese Frage ein und nutzt eine neue Methode namens Inferenz-Verhaltens-Semantik (I-bS). Betrachten Sie I-bS als einen Hochtechnologie-Scanner, der nicht nur die Regeln auf dem Papier betrachtet, sondern beobachtet, wie sich ein Symbol verhält, wenn es gezwungen ist, seine eigene Existenz in einer am stärksten reduzierten, puristischen Umgebung zu beweisen. Die Autoren wollten wissen: Wenn wir jede mögliche Art und Weise nehmen würden, eine Regel für eine logische Junktor zu schreiben, und diese in dieser minimalen Umgebung testen würden – welche davon besitzen tatsächlich einen einzigartigen, bedeutungsvollen „Fingerabdruck“? Sie haben nicht nur geraten; sie bauten eine massive Testumgebung auf, um zu sehen, welche Regeln überleben und welche untergehen.

Die große Junktoren-Volkszählung

Die Autoren setzten sich zum Ziel, eine beeindruckende Anzahl von Möglichkeiten zu testen: 10.816 verschiedene Regelpaare. Stellen Sie sich ein riesiges Gitter vor, bei dem jedes Quadrat eine andere Art darstellt, ein logisches „Wort“ unter Verwendung von höchstens zwei Ausgangsschritten und zwei aktiven Bestandteilen zu definieren. Sie speisten all diese 10.816 Kandidaten in ihre „minimale Ableitungsrelation“ ein. Sie können sich diese Ableitungsrelation als ein winziges, leeres Zimmer vorstellen, das nur die absoluten Grundlagen des Denkens enthält: eine Regel, die besagt, dass „A gleich A ist“ (Identität), und eine Regel, die besagt, dass „wenn aus A folgt B und aus B folgt C, dann folgt aus A auch C“ (Cut). Es ist das logische Äquivalent eines Überlebenskits für Minimalisten – kein Schnickschnack, keine zusätzlichen Werkzeuge, nur das Wesentliche.

Das Ziel war zu sehen, welche dieser 10.816 Kandidaten beweisen konnten, in diesem Raum „definierbar“ zu sein. Um definierbar zu sein, musste eine Junktor zwei strengen Tests standhalten:

Konservativität: Sie durfte nicht magisch neue Dinge beweisen, die ohne sie nicht möglich gewesen wären. Sie musste fair spielen.
Einzigartigkeit: Sie musste das Einzige sein, das das tut, was sie tut. Wenn ein anderes Symbol exakt dieselbe Aufgabe erfüllen konnte, war sie nicht einzigartig genug, um eine eigene spezielle Bedeutung zu haben.

Der Filter: Von 10.816 auf 21

Als sich der Staub gelegt hatte, waren die Ergebnisse überraschend spezifisch. Von den 10.816 Kandidaten bestanden nur 376 den ersten Test (Konservativität). Doch als der zweite Test (Einzigartigkeit) angewendet wurde, schrumpfte die Liste noch weiter zusammen. Am Ende fanden die Autoren genau 21 Junktoren, die „minimal bedeutungsvoll“ waren.

Diese 21 Überlebenden sind die „reinen“ Versionen logischer Wörter. Dazu gehören:

Bottom und Top: Die logischen Äquivalente von „Falsch“ und „Wahr“.
Zwei Arten der Negation: Eine, die wie das „nicht“ in der intuitionistischen Logik wirkt (eine vorsichtige Art der Verneinung), und eine andere, die wie das „nicht“ in der dual-intuitionistischen Logik wirkt (eine aggressivere Art). Das Paper zeigt, dass die „klassische“ Negation, die wir in der alltäglichen Mathematik verwenden, tatsächlich ein Mix aus diesen zwei unterschiedlichen Bedeutungen ist.
Konjunktionen (Und): Es gibt eine „additive“ Version (wie ein Standard-„und“) und eine „multiplikative“ Version (ein strengeres „und“, das Ressourcen verbraucht).
Disjunktionen (Oder): Ähnlich gibt es ein Standard-„oder“ und eine strengere „Fission“-Version.
Implikationen (Wenn... dann): Es gibt Rechts-Implikationen und Links-Implikationen, jeweils mit additiven und multiplikativen Nuancen.
Konverse und Inverse: Das Paper fand auch bedeutungsvolle Versionen dieser Junktoren, die umgedreht oder auf den Kopf gestellt wurden.

Die anderen 10.795 Kandidaten? Sie wurden abgelehnt. Einige waren „Bloatnectives“ (Aufbläh-Junktoren) – Regeln, die auf dem Papier anders aussah, aber exakt dasselbe wie die 21 Gewinner agierten, nur mit angehängten, nutzlosen Schritten. Andere waren nicht konservativ (sie brachen die Regeln des Zimmers) oder nicht einzigartig (sie waren zu ähnlich zu anderen Symbolen, um eine distinkte Identität zu besitzen).

Die Entdeckung der „Halben Bedeutung“

Einer der spielerischsten und zugleich tiefgründigsten Befunde betrifft die Frage, wie sich diese Bedeutungen ändern, wenn wir von einer Art der Logik zur anderen wechseln. Das Paper demonstriert, dass die klassische Logik (die Standardlogik, die in der meisten Mathematik verwendet wird) wie ein Mixer ist, der verschiedene Zutaten vermengt.

Zum Beispiel gehen wir in der klassischen Logik meist davon aus, dass „und“ einfach nur eine Sache ist. Aber dieses Paper zeigt, dass das klassische „und“ tatsächlich eine Mischung aus zwei unterschiedlichen Bedeutungen ist: dem additiven „und“ und dem multiplikativen „und“. Wenn man zur intuitionistischen Logik wechselt (eine Logik, die in der Informatik und konstruktiven Mathematik verwendet wird), verliert man die multiplikative Version. Man bleibt nur mit der additiven Version zurück.

Die Autoren kommen zu dem Schluss, dass die intuitionistische Negation, Disjunktion und Implikation jeweils nur die Hälfte der Bedeutung ihrer klassischen Gegenstücke erfassen. Es ist, als ob die klassische Logik sagt: „Ich bin ein fertiges Sandwich“, während die intuitionistische Logik sagt: „Ich bin nur das Brot“ und die dual-intuitionistische Logik sagt: „Ich bin nur die Füllung“. Keines von beiden ist „falsch“, aber sie verwenden jeweils nur die halben Zutaten.

Warum das wichtig ist

Dies ist nicht nur ein Spiel des Sortierens von Symbolen. Das Paper validiert eine neue Art, Bedeutung zu verstehen, nämlich die Inferenz-Verhaltens-Semantik. Indem die Autoren beweisen, dass diese Methode natürlich das Rauschen herausfiltert und exakt die 21 Junktoren hinterlässt, über die Logiker seit Jahrzehnten debattieren, zeigen sie, dass ihre Methode funktioniert. Es legt nahe, dass die „Bedeutung“ eines logischen Wortes nichts ist, was wir willkürlich erfinden; es ist etwas, das wir entdecken, indem wir beobachten, wie es sich verhält, wenn es auf seine absolut wesentlichen Bestandteile reduziert wird.

Das Paper behauptet nicht, alle Rätsel der Logik gelöst zu haben. Es lässt offene Fragen darüber, wie dies mit komplexeren Regeln oder anderen Arten von Logik funktioniert. Aber für die 21 Junktoren, die den Test bestanden haben, verfügen wir nun über eine präzise, regelunabhängige Landkarte ihrer Bedeutungen. Wir wissen, dass „und“ nicht einfach nur „und“ ist, und „nicht“ nicht einfach nur „nicht“. Es sind komplexe, vielschichtige Werkzeuge, und dieses Paper hat uns endlich den Bauplan geliefert, um sie voneinander zu unterscheiden.

Technisches Resümee: Inferenz-Verhaltens-Semantik für alle∗-Konnektive in zweidimensionalen Sequenzenkalkülen

1. Problemstellung

Das Paper adressiert eine zentrale Herausforderung der beweistheoretischen Semantik (P-tS): wie man bedeutungsinvariante semantische Erklärungen für logische Konnektive über verschiedene logische Systeme hinweg (z. B. klassische, intuitionistische, lineare und dual-intuitionistische Logiken) bereitstellen kann. Traditionelle Ansätze, wie die modelltheoretische Semantik (M-tS) und die Basis-Erweiterungs-Semantik (B-eS), leiden oft unter einem „Globalismus“, bei dem die Änderung der Logik eine Änderung der Bedeutung der Konnektive erfordert (z. B. das klassische „und“ gegenüber dem intuitionistischen „und“). Dies führt zu einer Situation, in der logische Unstimmigkeiten auf bloße Kommunikationsprobleme aufgrund unterschiedlicher Definitionen reduziert werden, anstatt auf substantielle Meinungsverschiedenheiten über geteilte Konzepte.

Das spezifische Problem, das dieses Paper behandelt, ist das Fehlen einer systematischen, formalen Implementierung der Inferenz-Verhaltens-Semantik (I-bS), eines kürzlich von Nagler [Nag26] vorgeschlagenen Ansatzes. Während I-bS einen vielversprechenden Rahmen bietet, um das „minimale Inferenzverhalten“ eines Konnektivs zu isolieren, um dessen Bedeutung zu definieren, fehlte ihm bisher eine umfassende technische Bewertung über den Raum möglicher Konnektivitätsregeln hinweg. Das Ziel des Papers ist es, I-bS zu validieren, indem es I-bS auf eine große, unstrukturierte Menge von Kandidaten-Konnektiven anwendet, um zu bestimmen, welche, falls überhaupt, über distinkte, minimale Bedeutungen verfügen, die unabhängig von spezifischen Strukturregeln (wie Schwächung oder Kontraktion) sind.

2. Methodik

Die Studie verwendet einen rigorosen, datengesteuerten Ansatz, um die „Bedeutung“ von Konnektiven basierend auf ihrem inferentiellen Gebrauch in einem minimalen Setting zu messen.

2.1 Untersuchungsgegenstand: Alle∗-Konnektive

Die Autoren definieren den Untersuchungsbereich als alle∗-Konnektive: operationale Regelpaare, die in zweidimensionalen Sequenzenkalkülen unter den folgenden Bedingungen formulierbar sind:

Operationale Regeln: Müssen separat, explizit und symmetrisch sein (Definition 3).
Beschränkungen: Höchstens zwei Prämissen-Sequenzen und höchstens zwei aktive Formeln pro Regel.
Gesamtraum: Dies ergibt genau 10.816 syntaktisch einzigartige Regelpaare (Kombinationen von Prämissenformen und Positionen aktiver Formeln).

2.2 Testumgebung: Minimale Ableitbarkeit

Um die Bedeutung eines Konnektivs vom strukturellen Merkmal spezifischer Logiken zu isolieren, verwenden die Autoren einen minimalen Hintergrundkalkül, der besteht aus:

Identität ( $Id_{pr}$ ): Beschränkt auf primitive Formeln.
Schnitt ( $Cut_{cd}$ ): Ein kontextdifferenzierender Schnitt-Regel.
Strukturelle Annahmen: Der Kalkül setzt Austausch (Multimengen) voraus, schließt aber Schwächung und Kontraktion aus. Dies repräsentiert den „substrukturellen Kern“, der vielen Logiken gemeinsam ist.

2.3 Messinstrument: Inferenzverhalten

Die Kernmetrik ist das Inferenzverhalten, definiert als das syntaktische Muster, das ein Konnektiv zeigt, wenn seine Definierbarkeit innerhalb des minimalen Kalküls bewiesen wird.

Definierbarkeitskriterien: Folgend nach Belnap [Bel62], ist ein Konnektiv definierbar, wenn seine Hinzufügung zum Kalkül zu einer konservativen Erweiterung führt (keine neuen Theoreme ohne den Konnektiv) und Eindeutigkeit besitzt (der Konnektiv ist bis auf Isomorphie eindeutig bestimmt).
Semantische Klausel: Die „Bedeutung“ eines Konnektivs wird als sein minimales operationales Regelpaar identifiziert, das das minimale Inferenzverhaltensprofil liefert (die kürzeste Liste der Komponentenpositionen, die der Konnektiv und seine aktiven Formeln während eines Definierbarkeitsbeweises besetzen).

2.4 Datengenerierung und Analyse

Die Autoren filtern die 10.816 Kandidaten systematisch:

Filter 1 (Formulierbarkeit): Alle 10.816 Regelpaare.
Filter 2 (Konservativität): Beweis der Schnitt-Elimination für die positiven Fälle und Konstruktion von Gegenbeispielen für die nicht-konservativen Fälle. Dies reduziert die Menge auf 376 konservative Konnektive.
Filter 3 (Eindeutigkeit): Etablierung horizontaler und vertikaler Interderivierbarkeit. Dies reduziert die Menge weiter auf 150 eindeutig definierbare Konnektive.
Minimalitätsanalyse: Unter den 150 definierbaren Konnektiven unterscheiden die Autoren zwischen „minimalen“ Konnektiven und „Bloatnectives“ (äquivalente Konnektive mit syntaktischen Redundanzen). Durch Anwendung von Kriterien für die Prämissentyp-Minimalität (niedrigste Kardinalität der Prämissen-Sequenzen) isolieren sie die wahrhaft minimalen semantischen Klauseln.

3. Zentrale Beiträge und Ergebnisse

3.1 Identifizierung von 21 minimal bedeutungsvollen Konnektiven

Das Hauptergebnis ist die Identifizierung von genau 21 minimal bedeutungsvollen Konnektiven. Diese entsprechen vertrauten logischen Konstanten und deren Kehrwerten/Inversen, jedoch mit präzisen Unterscheidungen zwischen additiven (Gitter) und multiplikativen (Gruppe) Versionen:

Nullär: Unten ( $\bot$ ) und Oben ( $\top$ ).
Unär: Zwei Formen der Negation (Intuitionistische $\neg$ und Dual-Intuitionistische $\sim$ ), sowie eine „triviale“ Kehrwert-Negation.
Binär:
- Konjunktion: Additiv ( $\sqcap$ ) und Multiplikativ ( $\otimes$ ).
- Disjunktion: Additiv ( $\sqcup$ ) und Multiplikativ ( $\oplus$ ).
- Implikation: Additiv Rechts ( $\rightsquigarrow$ ), Multiplikativ Rechts ( $\to$ ), Additiv Links und Multiplikativ Links.
- Kehrwerte und Inverse: Jede der obigen hat distinkte semantische Klauseln für ihre Kehrwerte (Komponenten vertauschen) und Inverse.

3.2 Semantische Klauseln und Frameworks

Das Paper liefert explizite semantische Klauseln (minimale Regelpaare) für jeden der 21 Konnektive. Entscheidend ist, dass es zeigt, dass diese Bedeutungen logikunabhängig sind. Beispielsweise ist die semantische Klausel für die multiplikative Konjunktion ( $\otimes$ ) dieselbe, ob sie in der linearen Logik, der klassischen Logik oder der intuitionistischen Logik erscheint. Die Unterschiede darin, wie sich diese Konnektive in Voll-Logiken verhalten (z. B. die Äquivalenz von $\otimes$ und $\sqcap$ in der klassischen Logik), werden den Strukturressourcen (wie Kontraktion und Schwächung) zugeschrieben und nicht einer Änderung der Kernbedeutung des Konnektivs.

3.3 Semantische Wechselbeziehungen zwischen Logiken

Die Studie bildet die semantische Kompatibilität dieser 21 Konnektive über verschiedene Logiken hinweg ab:

Klassische Logik (LK): Verknüpft additive und multiplikative Versionen von Konjunktion, Disjunktion und Implikation. Sie verknüpft auch die beiden Formen der Negation.
Intuitionistische Logik (LJ): Ist kompatibel mit den additiven Versionen von Konjunktion und Disjunktion sowie der „rechten“ Implikation, erfasst aber nur die Hälfte der Bedeutung der klassischen Negation (speziell $\neg_{min}$ , unter Ausschluss von $\sim_{min}$ ).
Dual-Intuitionistische Logik (LDJ): Erfasst die andere Hälfte der klassischen Negation ( $\sim_{min}$ ) und die Duale der anderen Konnektive.
Lineare Logik (LL): Unterscheidet alle 21 Konnektive und behandelt sie als semantisch distinkt.

3.4 Validierung von I-bS

Das Paper behauptet, I-bS zu validieren, indem es zeigt, dass die Theorie bei einer blinden, erschöpfenden Suche nach möglichen Regeln ohne Bias gegenüber einer spezifischen Logik natürlich zu genau den Standard-Konnektiven konvergiert, die in etablierten logischen Systemen zu finden sind. Die Tatsache, dass der „Lärm“ (die anderen 10.795 Regelpaare) als nicht-definierbar oder nicht-minimal herausgefiltert wird, dient als „Sanity Check“ für die Theorie.

4. Bedeutung und Behauptungen

Das Paper positioniert seine Ergebnisse als eine Verifizierung des Frameworks der Inferenz-Verhaltens-Semantik. Seine Bedeutung liegt in:

Logikunabhängigkeit: Es bietet eine Methode, die Bedeutung von Konnektiven so zu definieren, dass sie über verschiedene Logiken hinweg invariant bleibt. Das Ändern der Logik (z. B. Hinzufügen von Schwächung) ändert nicht die Bedeutung des Konnektivs; es ändert lediglich den strukturellen Kontext, in dem der Konnektiv operiert.
Auflösung der Bedeutungsänderung: Es bietet eine semantische Erklärung dafür, warum klassische und intuitionistische Logiken scheinbar uneinig sind. Sie sind nicht notwendigerweise uneinig über die Bedeutung von „und“ oder „oder“; vielmehr unterscheiden sie sich darin, welche minimalen Konnektive sie zulassen und welche Strukturregeln sie erlauben. Beispielsweise ist das klassische „und“ eine Verschmelzung zweier distinkter minimaler Bedeutungen ( $\otimes$ und $\sqcap$ ), während das intuitionistische „und“ strikt $\sqcap$ ist.
Ontologische Sparsamkeit: Der Ansatz benötigt keine externen Modelle oder Basen und stützt sich ausschließlich auf den substrukturellen Kern des Beweissystems.
Vollständigkeit: Durch die Abdeckung des gesamten Raums formulierbarer Regeln unter den gegebenen Beschränkungen behauptet das Paper, eine vollständige Taxonomie minimaler Konnektiv-Bedeutungen in zweidimensionalen Sequenzenkalkülen erstellt zu haben.

Die Autoren bleiben hinsichtlich des Umfangs bescheiden und merken an, dass die Ergebnisse relativ zu den spezifischen Beschränkungen (zwei Prämissen, zwei aktive Formeln, spezifischer minimaler Kalkül) sind und zukünftige Arbeiten mehrdimensionale Kalküle, Quantifizierung oder alternative minimale Ableitbarkeitsrelationen untersuchen könnten. Innerhalb des definierten Rahmens behauptet das Paper jedoch, dass I-bS erfolgreich die primitiven Bedeutungen logischer Konnektive isoliert.