💻 computer science

Labelled Sequent Calculi for Propositional Team Logics

Diese Arbeit präsentiert sounde und vollständige beschriftete Sequenzenkalküle mit admissiblen Strukturregeln und terminierenden Beweissuchverfahren für vier propositionale Team-Logiken, einschließlich der basischen inquisitiven Logik und der propositionalen intuitionistischen Abhängigkeitslogik, zusammen mit deren Tensor-Disjunktionserweiterungen.

Ursprüngliche Autoren: Fausto Barbero, Marianna Girlando, Valentin Müller, Fan Yang

Veröffentlicht 2026-07-01

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Fausto Barbero, Marianna Girlando, Valentin Müller, Fan Yang

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, ein Logikrätsel zu lösen. Auf die traditionelle Art (die als „Tarskische Semantik“ bezeichnet wird) betrachten Sie das Rätsel aus nur einem spezifischen Blickwinkel. Sie fragen: „Ist diese Aussage genau hier, an diesem einen Ort, wahr?“

Die Autoren dieser Arbeit arbeiten jedoch mit einer anderen Art von Logik, der sogenannten Team-Semantik. Anstatt nur auf einen einzelnen Ort zu schauen, stellen Sie sich vor, Sie betrachten ein ganzes Team von Menschen, die zusammenstehen. Sie fragen nicht, ob eine Aussage für eine einzelne Person wahr ist; Sie fragen, ob sie für das gesamte Team beim gemeinsamen Handeln wahr ist.

Dieser „Team“-Ansatz wird in realen Szenarien verwendet, wie zum Beispiel bei der Ermittlung, wie Variablen voneinander abhängen (z. B. „Hängt der Preis von der Farbe ab?“) oder beim Verständnis der Bedeutung von Fragen in der Sprache (z. B. „Ist es wahr, dass es regnet ODER ist es wahr, dass es schneit?“).

Das Problem: Wie man Dinge über Teams beweist

Die Autoren wollten eine Reihe von Regeln (einen „Taschenrechner“) erstellen, um zu beweisen, ob Aussagen über diese Teams wahr oder falsch sind. Sie nennen diese Labelled Sequent Calculi (beschriftte Sequenzenkalküle).

Stellen Sie sich einen „Sequenten“ wie eine Waage vor. Auf der einen Seite haben Sie eine Liste von Fakten, die Sie kennen (den aktuellen Zustand des Teams). Auf der anderen Seite steht eine Schlussfolgerung, die Sie beweisen wollen. Das Ziel ist zu zeigen, dass, wenn die Fakten auf der linken Seite wahr sind, die Schlussfolgerung auf der rechten Seite ebenfalls wahr sein muss.

Das Papier stellt vier spezifische „Taschenrechner“ (Beweissysteme) für vier verschiedene Arten von Team-Logiken vor:

Basale inquisitive Logik: Die Standard-Team-Logik für Fragen.
Propositionale intuitionistische Abhängigkeitslogik: Team-Logik, die „Abhängigkeiten“ handhabt (wie „A hängt von B ab“).
Zwei erweiterte Versionen: Diese fügen eine spezielle „Tensor-Disjunktion“ hinzu (eine ausgeklügelte Art zu sagen: „das Team in zwei separate Gruppen aufzuteilen, um verschiedene Dinge zu prüfen“).

Die Werkzeuge: Labels als Teammitglieder

Um diese Kalküle funktionsfähig zu machen, verwenden die Autoren Labels (Beschriftungen).

Stellen Sie sich vor, jedes Mitglied Ihres Teams hat ein Namensschild.
Einige Namensschilder sind für Individuen (einzelne Personen).
Einige Namensschilder sind für Gruppen (das gesamte Team).
Die Regeln erlauben es, Dinge zu sagen wie „Die Gruppe x ist dieselbe wie die Gruppe y“ oder „Gruppe x ist eine Teilmenge von Gruppe y“.

Das Papier präsentiert zwei Haupttypen dieser Kalküle:

1. Der „detaillierte“ Taschenrechner (G(L))

Diese Version ist sehr präzise. Sie verwendet komplexe Labels, die Teams, deren Vereinigungen (das Zusammenführen zweier Teams) und deren Durchschnitte (das Finden der Überschneidung zwischen zwei Teams) darstellen können.

Analogie: Dies ist wie ein High-End-GPS, das jedes einzelne Auto in einem Stau verfolgt, deren exakte Positionen und wie sie Spuren zusammenführen oder trennen. Es ist mathematisch rigoros und spiegelt exakt wider, wie Teams in der realen Welt agieren.
Der Haken: Da es so viele Details verfolgt, ist es schwer zu sagen, ob das GPS jemals mit dem Rechnen aufhören wird (es könnte ewig laufen).

2. Der „terminierende“ Taschenrechner (G*(L))

Um das Problem des „ewigen Laufens“ zu lösen, haben die Autoren eine vereinfachte Version erstellt.

Analogie: Anstatt jedes Auto exakt zu verfolgen, sagt dieses GPS einfach: „Wir haben eine Liste von 5 Autos. Lassen Sie uns jede mögliche Kombination dieser 5 Autos prüfen.“
Der Trick: Sie nehmen an, dass es eine endliche Anzahl von möglichen „Zuständen“ gibt (wie eine begrenzte Anzahl möglicher Wetterbedingungen). Da die Anzahl der Möglichkeiten begrenzt ist, ist der Taschenrechner garantiert nach einer Weile fertig. Er wird entweder einen Beweis finden (Erfolg!) oder auf eine Wand stoßen, an der keine Regeln mehr anwendbar sind (Fehlgeschlagen/Gegenbeispiel).
Warum das wichtig ist: Dies garantiert, dass Sie immer ein Computerprogramm schreiben können, um zu entscheiden, ob eine Aussage in diesen Logiken wahr oder falsch ist.

Die wichtigsten Regeln des Spiels

Das Papier beweist, dass ihre Kalküle korrekt (sound) und vollständig (complete) sind:

Korrektheit (Sound): Wenn der Taschenrechner „Wahr“ sagt, ist es tatsächlich wahr. (Der Taschenrechner lügt nicht).
Vollständigkeit (Complete): Wenn etwas tatsächlich wahr ist, kann der Taschenrerechner schließlich einen Beweis dafür finden. (Der Taschenrechner übersieht nichts).

Sie haben auch bewiesen, dass die Kalküle über admissibile Regeln verfügen.

Schwächung (Weakening): Sie können zusätzliche, nutzlose Fakten zu Ihrer Liste hinzufügen, ohne die Logik zu brechen.
Kontraktion (Contraction): Wenn Sie dieselbe Tatsache zweimal auflisten, können Sie sie so behandeln, als wäre sie nur einmal aufgelistet.
Cut: Wenn Sie beweisen, dass A zu B führt und B zu C führt, können Sie direkt von „A führt zu C“ ausgehen, ohne den Zwischenschritt zu zeigen.

Die „Tensor“-Heraherforderung

Einer der schwierigsten Teile dieses Papers war der Umgang mit der Tensor-Disjunktion (der „Splitting“-Regel).

Die Analogie: Stellen Sie sich ein Team von Detektiven vor.
- Die Standard-Logik sagt: „Das gesamte Team löst den Fall, wenn sie sich alle auf die Antwort einigen.“
- Die Tensor-Logik sagt: „Das Team löst den Fall, wenn wir sie in zwei Gruppen aufteilen können, wobei Gruppe A einen Teil des Falls löst und Gruppe B den Rest.“
Die Autoren mussten eine spezielle Regel (die fin-Regel genannt wird) erfinden, um dies zu handhaben. Da sie annahmen, dass die Anzahl der möglichen „Welten“ (Bewertungen) endlich ist, konnten sie sagen: „Jedes Team ist einfach eine Kombination dieser spezifischen, begrenzten Welten.“ Dies ermöglichte es ihnen, das Splitting-Verhalten mathematisch zu simulieren.

Zusammenfassung

Kurz gesagt haben die Autoren zwei Regelwerke gebaut, um Logikrätsel zu lösen, die Gruppen von Menschen (Teams) betreffen:

Ein detailliertes, mathematisch perfektes Regelwerk, das komplexe Gruppeninteraktionen handhabt, aber schwer zu automatisieren ist.
Ein vereinfachtes, garantiert endendes Regelwerk, das eine begrenzte Anzahl von Möglichkeiten annimmt, was es Computern ermöglicht, automatisch zu prüfen, ob eine Aussage wahr oder falsch ist.

Sie haben bewiesen, dass beide Regelwerke für die von ihnen untersuchten spezifischen Logiken zuverlässig (korrekt) und umfassend (vollständig) sind.

Technische Zusammenfassung: Labelled-Sequent-Kalküle für propositionale Team-Logiken

Problemstellung
Die Arbeit befasst sich mit den beweistheoretischen Herausforderungen der propositionalen Logiken, die auf Team-Semantik basieren. Während die semantischen Eigenschaften von nach unten abgeschlossenen (downward-closed) Team-Logiken – insbesondere die basale inquisitive Logik (InqB), die propositionale intuitionistische Abhängigkeitslogik (PID) und deren Erweiterungen um die Tensor-Disjunktion (InqqB $\lor$ und PID $\lor$ ) – gut verstanden sind, bleibt deren Beweistheorie unterentwickelt. Bestehende analytische Beweissysteme für diese Logiken, wie etwa Multi-Typ-Display-Kalküle oder Deep-Inference-Sequent-Kalküle, erfordern oft komplexe strukturelle Anreicherungen von Gentzen-artigen Sequenten. Die Autoren identifizieren die Notwendigkeit modularer, gelabelter Sequent-Kalküle, die die spezifischen Erfüllungsbedingungen der Team-Semantik handhaben können, insbesondere das Verhalten der Tensor-Disjunktion ( $\lor$ ) und der Abhängigkeits-Atome, während gleichzeitig Eigenschaften wie Schnitt-Admissibilität (cut-admissibility) und terminierender Beweissuche gewährleistet werden.

Methodik
Die Autoren entwickeln zwei Familien von gelabelten Sequent-Kalkülen für die vier Ziel-Logiken:

Allgemeine gelabelte Kalküle ( $G(L)$ ): Diese Systeme verwenden Labels, die aus unendlichen Mengen von Team-Variablen ( $S$ für Singleton-Teams, $A$ für beliebige Teams) kombiniert mit mengentheoretischen Operationen (Vereinigung $\cup$ und Schnittmenge $\cap$ ) konstruiert sind. Die Labels repräsentieren beliebige Teams, Singleton-Teams und deren Kombinationen. Die Kalküle umfassen:
- Anfangssequenten und logische Regeln: Diese spiegeln die Erfüllungsbedingungen wider, die in der Team-Semantik definiert sind (z. B. Regeln für $\land$ , $\lor$ , $\to$ und die Tensor-Disjunktion $\lor$ ).
- Ordnungsregeln: Eine Reihe von Regeln, welche die mengentheoretischen Eigenschaften von Teams formalisieren (z. B. Transitivität, Vereinigung, Schnittmenge und die Eigenschaft des leeren Teams).
- Spezielle Regeln: Eine Regel namens fin wird eingeführt, um die Annahme zu behanden, dass die Menge der propositionalen Variablen $P$ endlich ist. Diese Regel ermöglicht es dem System, jedes Team als Vereinigung von $2^{|P|}$ Valuations zu beschreiben, was entscheidend für die Simulation der Tensor-Disjunktion über klassische Formeln ist.
- Modularität: Die Systeme sind so konzipiert, dass die Kalküle für PID und PID $\lor$ durch Hinzufügen spezifischer Regeln für Abhängigkeits-Atome zu den Kalkülen für InqB und InqB $\lor$ erhalten werden.
Terminierende Kalküle ( $G^\star(L)$ ): Um die automatisierte Beweissuche zu erleichtern, führen die Autoren eine vereinfachte Variante ein, bei der die Labels als endliche Mengen von Variablen statt als komplexe Terme unter Verwendung von Vereinigungen und Schnittmengen definiert sind. Dieser Ansatz eliminiert die Notwendigkeit von relationalen Atomen und Ordnungsregeln und ersetzt sie durch Regeln, die direkt auf der Menge der Variablen in einem Label operieren.

Zentrale Beiträge und Ergebnisse

Korrektheit und Vollständigkeit: Die Autoren beweisen, dass die allgemeinen Kalküle $G(L)$ korrekt und vollständig in Bezug auf die entsprechenden Team-Semantiken und Hilbert-artigen Axiomatisierungen sind. Dies wird durch den Nachweis der Admissibilität struktureller Regeln (Schwächung, Kontraktion, Schnitt) sowie durch die Feststellung der Admissibilität abgeleiteter Regeln (wie mp für Modus Ponens und flat für die Flachheit klassischer Formeln) erreicht.
Schnitt-Admissibilität: Ein zentrales technisches Ergebnis ist der Beweis der Schnitt-Admissibilität für alle vier Kalküle. Der Beweis erfolgt durch Induktion über den Rang der Schnittformel und die Höhe der Ableitung unter Verwendung einer lexikographischen Ordnung, die sowohl die Komplexität der Formel als auch das Label berücksichtigt.
Terminierende Beweissuche: Die Arbeit präsentiert explizite, terminierende Beweissuche-Algorithmen für die vereinfachten Kalküle $G^\star(L)$ . Der Algorithmus konstruiert einen Beweissuche-Baum von der Wurzel aus (root-first). Es wird bewiesen, dass er terminiert, da die Anzahl der möglichen gelabelten Formeln endlich ist (gegeben eine endliche Menge propositionaler Variablen und eine endliche Menge von Subformeln).
Entscheidungsverfahren: Die terminierende Natur der $G^\star(L)$ -Kalküle impliziert, dass die Erfüllbarkeits- und Gültigkeits-Probleme für InqB, PID, InqB $\lor$ und PID $\lor$ entscheidbar sind. Die Autoren liefern eine Gegenmodell-Konstruktion aus jedem gesättigten (offenen) Zweig des Beweissuche-Baums, was die Vollständigkeit des Suchverfahrens sicherstellt.

Bedeutung und Behauptungen
Die Arbeit behauptet, dass ihr primärer Beitrag in der Bereitstellung der ersten korrekten und vollständigen gelabelten Sequent-Kalküle für das volle Spektrum der propositionalen Team-Logiken einschließlich Tensor-Disjunktion und Abhängigkeits-Atomen liegt. Die Autoren heben zwei distinkte Vorteile ihres Ansatzes hervor:

Modularität: Die Beweissysteme können durch einfaches Hinzufügen oder Entfernen von Regeln an unterschiedliche Mengen von Junktoren oder Atomen angepasst werden, eine Eigenschaft, die in den starreren strukturierten Kalkülen der bisherigen Literatur nicht vorhanden ist.
Terminierung und Entscheidbarkeit: Durch die Vereinfachung der Label-Struktur in $G^\star(L)$ bieten die Autoren ein konkretes Entscheidungsverfahren für diese Logiken, was einen bedeutenden Schritt für das automatisierte Schließen in der Team-Semantik darstellt.

Die Autoren merken an, dass die allgemeinen Kalküle $G(L)$ aufgrund von Fixed-Premise-Regeln und der Fähigkeit, über beliebige Teilmengen mittels Variablen zu argumentieren, kürzere Beweise liefern können, die vereinfachten Kalküle $G^\star(L)$ jedoch essenziell für die Etablierung der Terminierung sind. Die Arbeit ist auf Sprachen mit endlich vielen propositionalen Atomen beschränkt, eine notwendige Bedingung für die fin-Regel und die Terminierung der Beweissuche in Gegenwart der Tensor-Disjunktion. Die Arbeit schließt mit der Identifizierung zukünftiger Arbeiten ab, einschließlich der Erweiterung dieser Systeme auf Sprachen mit unendlich vielen Atomen und der Entwicklung von Beweissystemen für andere Klassen von Team-Logiken, wie etwa solche ohne intuitionistische Implikation oder solche, die die Vereinigungs-Abschluss-Eigenschaft (union closure property) besitzen.