🔢 mathematics

Towards an Inferentialist Account of Information Through Proof-theoretic Semantics

Dieser Beitrag schlägt eine inferentialistische Konzeption von Information vor, die auf der beweistheoretischen Semantik basiert, die traditionelle Wahrheit durch Inferierbarkeit ersetzt und einen mathematisch-logischen Rahmen für den „Inferon" entwickelt, der eine rigorose Analyse des Informationsflusses in verteilten Systemen ermöglicht.

Ursprüngliche Autoren: Matthew Collins, Timo Eckhardt, David Pym

Veröffentlicht 2026-05-08

📖 6 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Matthew Collins, Timo Eckhardt, David Pym

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

Das große Ganze: Was ist Information eigentlich?

Stellen Sie sich vor, Sie versuchen, ein Haus zu bauen. Sie haben Ziegelsteine, Holz und Nägel, aber keinen Bauplan. Sie wissen, wie man Ziegelsteine stapelt, aber Sie wissen nicht, warum sie standhalten oder wie sie zusammenpassen, um einen Raum zu bilden.

Die Autoren dieses Papiers argumentieren, dass wir in unserer modernen Welt ständig über „Information" sprechen (in Computern, Nachrichten, Wissenschaft und im täglichen Leben), aber wir haben kein solides, mathematisches Fundament dafür, was Information ist. Ohne diesen Bauplan ist es schwierig zu verstehen, wie komplexe Systeme (wie das Internet oder globale Lieferketten) tatsächlich funktionieren.

Ihr Ziel ist es, eine neue Art von Bauplan zu erstellen. Anstatt Information dadurch zu definieren, ob sie in einem statischen Sinne „wahr" ist (wie eine Tatsache, die in einem Buch steht), wollen sie sie dadurch definieren, wie sie verwendet wird, um eine Schlussfolgerung zu ziehen. Sie nennen dies einen „inferentialistischen" Ansatz.

Der alte Weg vs. der neue Weg

Der alte Weg (Das „Wahrheits"-Modell):
Stellen Sie sich einen Bibliothekar vor, der nur Bücher akzeptiert, die faktisch korrekt sind. Wenn ein Buch sagt „Der Himmel ist blau", überprüft der Bibliothekar eine riesige, perfekte Karte des Universums, um zu sehen, ob der Himmel tatsächlich blau ist. Wenn ja, ist das Buch „Information". Wenn das Buch sagt „Der Himmel ist grün", wird es als falsch abgelehnt.

Das Problem: Dies erfordert eine perfekte, externe Karte des Universums (ein „Modell"), auf die sich alle einigen. Es ist schwierig, diese Karte für komplexe, sich verändernde Systeme zu erstellen.

Der neue Weg (Das „Schlussfolgerungs"-Modell):
Die Autoren schlagen einen anderen Bibliothekar vor. Dieser Bibliothekar interessiert sich nicht für eine riesige Karte des Universums. Stattdessen kümmert er sich um Regeln.

Stellen Sie sich vor, Sie haben eine Reihe von Regeln: „Wenn es regnet, dann ist der Boden nass."
Wenn Sie dem Bibliothekar sagen: „Es regnet", kann er sofort schließen: „Daher ist der Boden nass."
In dieser Sichtweise geht es bei Information nicht darum, eine Tatsache mit der Realität abzugleichen; es geht darum, was Sie logisch ableiten können, basierend auf den Regeln, die Sie haben.

Die Autoren nennen diese neue Einheit der Information einen „Inferon" (kurz für „inferentielle Einheit"). Denken Sie an ein Inferon nicht als an eine Tatsache, sondern als an einen Zug in einem Logikspiel. Es ist ein Stück Information, das sagt: „Angesichts dieser Regeln kann ich diesen nächsten Schritt ableiten."

Die drei Säulen des Papiers

Das Papier baut diese neue Theorie auf drei Hauptbeinen auf:

1. Die Philosophie (Das „Warum")

Die Autoren betrachten einen berühmten Philosophen namens Dretske, der sagte, Information müsse etwas betreffen, wahr sein und übertragbar sein.

Die Wendung: Die Autoren behalten „etwas betreffen" und „übertragbar" bei, tauschen aber „Wahrheit" gegen „Ableitbarkeit" aus.
Analogie: Anstatt zu fragen: „Ist diese Aussage in der realen Welt wahr?", fragen sie: „Kann ich diese Aussage mit den Regeln, die ich gerade habe, beweisen?" Wenn Sie es beweisen können, zählt es als Information. Dies macht Information abhängig von der Person (oder dem Computer), die denkt, und von den Regeln, die sie verwendet.

2. Die Logik (Das „Wie")

Um dies mathematisch umzusetzen, verwenden sie ein Werkzeug namens Beweistheoretische Semantik.

Die Analogie: Stellen Sie sich ein riesiges, unendliches Notizbuch mit Regeln vor, das „Basis" genannt wird.
- Einige Regeln sind einfach: „Wenn Sie einen Schlüssel haben, können Sie die Tür öffnen."
- Einige Regeln sind komplex: „Wenn Sie einen Schlüssel HABEN UND die Tür nicht abgeschlossen ist, können Sie eintreten."
In ihrem System ist ein „Inferon" ein Stück Information, das durch einen bestimmten Satz von Regeln in diesem Notizbuch gestützt wird. Wenn Sie die richtigen Regeln haben (die Basis), „hält" die Information. Wenn Sie die Regeln ändern, kann sich die Information ändern.
Dies unterscheidet sich von der alten Methode (Situations-Theorie), die Information wie einen Schnappschuss einer Szene in einem Film behandelt. Die neue Methode behandelt Information wie einen Schritt in einem Rezept.

3. Die Systeme (Das „Wo")

Schließlich zeigen sie, wie dies in realen Systemen funktioniert, wie etwa in einem Computernetzwerk oder an einem Sicherheitskontrollpunkt.

Die Analogie: Denken Sie an eine Taschenlampe. Eine Taschenlampe hat einen Schalter und eine Glühbirne.
- In der alten Sichtweise könnte man sagen: „Der Schalter ist EIN, also ist die Glühbirne EIN."
- In ihrer neuen Sichtweise definieren sie einen „Kanal" (eine Verbindung) zwischen dem Schalter und der Glühbirne. Sie verwenden Regeln, um zu sagen: „Wenn der Schalter EIN ist (in diesem spezifischen Kontext), dann muss die Glühbirne leuchten."
Sie wenden dies auf ein komplexes Beispiel an: Flughafensicherheit.
- Ein Passagier durchläuft Check-in, Gepäckkontrolle und Passkontrolle.
- In jedem Schritt werden verschiedene „Basen" (Regelsätze) verwendet. Der Check-in-Mitarbeiter hat Regeln für Pässe; der Gepäckmitarbeiter hat Regeln für Gepäck.
- Das Papier zeigt, wie Information von einer Station zur nächsten fließt, nicht nur als Daten, sondern als logische Schlussfolgerungen. Zum Beispiel: „Weil der Pass im Schritt 1 überprüft wurde und die Regeln besagen, dass ein geprüfter Pass das Boarding erlaubt, kann der Passagier im Schritt 5 an Bord gehen."

Wichtige Erkenntnisse

Information ist ein Prozess: Es ist kein statisches Objekt, das in einer Datenbank sitzt; es ist ein aktiver Prozess des Denkens.
Kontext ist wichtig: Was als Information zählt, hängt von den „Regeln" (der Basis) ab, die Sie gerade verwenden. Eine Tatsache, die für einen Arzt Information ist, ist möglicherweise keine Information für einen Laien, weil sie unterschiedliche Regelbücher haben.
Akteure sind wichtig: Das Papier betont, dass „Akteure" (Menschen oder Computer) ihre eigenen spezifischen Fähigkeiten zum Schließen haben. Ein System funktioniert, wenn diese Akteure Informationen untereinander unter Verwendung gemeinsamer Regeln weitergeben können.

Zusammenfassung in einem Satz

Das Papier schlägt vor, dass wir aufhören, Information als „Fakten über die Welt" zu betrachten, und anfangen, sie als „Schritte in einem logischen Argument" zu betrachten, wobei der Wert der Information davon abhängt, was Sie daraus mit einem bestimmten Satz von Regeln ableiten können.

Technische Zusammenfassung: Hin zu einer inferentialistischen Begründung von Information durch proof-theoretische Semantik

1. Problemstellung

Der Beitrag adressiert das Fehlen vollständig überzeugender logischer oder mathematischer Fundamente für den Begriff der „Information", trotz dessen Zentrallität für die moderne Gesellschaft und die Informatik. Aktuelle Ansätze, insbesondere jene, die in der modelltheoretischen Semantik (wie der Situations-Theorie) verwurzelt sind, stützen sich auf Wahrheitsbedingungen, die aus externen Modellen abgeleitet werden. Die Autoren argumentieren, dass diese Abhängigkeit von Wahrheit (insbesondere der „Veridizitäts-These") und externen Modellen die Fähigkeit einschränkt, über komplexe, verteilte Informationsökosysteme zu reasoning. Sie postulieren die Notwendigkeit eines Rahmens, in dem die Bedeutung von Information durch ihre Verwendung im Inferenzprozess bestimmt wird, nicht durch ihre Korrespondenz zu einem Modell.

2. Methodik

Die Autoren schlagen eine inferentialistische semantische Theorie der Information vor, die in der Proof-Theoretischen Semantik (P-tS) verankert ist und speziell die Base-Extension-Semantik (B-eS) nutzt. Die Methodik umfasst drei interagierende Komponenten:

Konzeptuelle Analyse (Metaphysik): Die Autoren reinterpretieren Fred Dretskes Metaphysik der Information (Intentionalität, Wahrheit, Übertragbarkeit). Sie ersetzen die Anforderung der Wahrheit durch Inferierbarkeit. Information wird nicht als ein Fakt definiert, das in einem Modell wahr ist, sondern als eine Einheit, die aus einer Menge atomarer Regeln (einer „Basis") ableitbar ist.
Logik (Formalisierung): Der Beitrag nutzt P-tS, um eine mathematisch-logische Theorie einer primitiven Informationseinheit namens Inferon zu konstruieren. Dieser Ansatz kontrastiert mit dem modelltheoretischen Infon der Situations-Theorie (Barwise, Seligman u. a.).
- Inferone: Definiert als Tripel $\langle\langle P, \mathcal{P}, b \rangle\rangle$ , wobei $P$ eine atomare Proposition oder Prädikat ist, $\mathcal{P}$ eine lokale inferonische Basis (eine Menge atomarer Regeln) und $b$ eine Polarität (Behauptung oder Verneinung) darstellt.
- Bedeutung: Die Bedeutung eines Inferons leitet sich aus einer globalen Basis atomarer Regeln und der lokalen Basis des Inferons ab, nicht aus einem Modell erster Stufe.
- Logik: Die Autoren entwickeln eine Logik der Inferone auf Basis der intuitionistischen Logik und erweitern Sandqvists B-eS für die intuitionistische Aussagenlogik (IPL) sowie Gheorghius Erweiterung auf die Prädikatenlogik erster Stufe.
Systeme (Anwendung): Die entwickelten P-tS-Werkzeuge werden angewendet, um verteilte Systeme zu modellieren. Die Autoren passen das Framework der „Logik verteilter Systeme" (LDS) (Barwise & Seligman) an, indem sie Klassifikationen und Infomorphismen durch inferonische Basen und Inferomorphismen ersetzen.

3. Hauptbeiträge

A. Das Inferon und die inferentialistische Semantik

Der Kernbeitrag ist die Definition des Inferons als inferentialistisches Gegenstück zum Situations-Theorie-Infon.

Struktur: Ein Inferon $\iota = \langle\langle P, \mathcal{P}, b \rangle\rangle$ besteht aus einer Proposition $P$ , einer lokalen Basis $\mathcal{P}$ und einer Polarität $b$ .
Support-Relation: Gültigkeit wird über eine Support-Relation $\Vdash_B$ relativ zu einer Basis $B$ definiert. Ein atomares Inferon wird unterstützt, wenn es in der Vereinigung der globalen Basis und der lokalen Basis ableitbar ist: $\Vdash_B \langle\langle P, \mathcal{P}, b \rangle\rangle$ genau dann, wenn $\vdash_{B \cup \mathcal{P}} \langle\langle P, b \rangle\rangle$ .
Agentur: Das Framework führt agentenbezogene Modalitäten ( $[a]$ und $\langle a \rangle$ ) ein, um inferenzielle Fähigkeiten darzustellen. Die Fähigkeit eines Agenten, ein Inferon zu unterstützen, hängt von der Vereinigung der umgebenden Basis und der spezifischen Menge von Basen des Agenten ab.

B. Logische Ergebnisse

Der Beitrag etabliert die formalen Eigenschaften der Logik der Inferone:

Korrektheit und Vollständigkeit: Die Autoren beweisen Satz 11 (Korrektheit) und Satz 12 (Vollständigkeit) für die Aussagenlogik der Inferone und passen Sandqvists Beweise an. Diese Ergebnisse werden auf den Fall der Prädikatenlogik erster Stufe erweitert (Satz 11 und 12 erweitert).
Das (Inferon)-Axiom: Ein spezifisches Axiom wird eingeführt, um die Interaktion zwischen lokalen Basen und der globalen Support-Relation zu handhaben und so die Kohärenz zwischen dem Kalkül der natürlichen Deduktion und der Base-Extension-Semantik sicherzustellen.
Komplexe Inferone: Das Framework erlaubt logische Konnektive innerhalb von Inferonen, wobei Support-Relationen rekursiv definiert sind (Abbildung 9).

C. Informationsfluss und Inferomorphismen

Der Beitrag entwickelt eine inferentialistische Begründung des Informationsflusses in verteilten Systemen:

Inferomorphismen: Analog zu Infomorphismen in LDS ist ein Inferomorphismus ein Paar von Funktionen ( $f^\vee$ auf Terme, $f^\wedge$ auf Prädikate), das die Ableitbarkeitsrelation über verschiedene Basen hinweg erhält.
Kanäle: Ein Kanal wird als eine Familie von Inferomorphismen definiert, die einen gemeinsamen Kern (eine zentrale Basis) teilen.
Informationsfluss: Informationsfluss wird durch Constraints zwischen Inferonen über Kanäle hinweg charakterisiert. Wenn ein Constraint im Kern gilt, wird Information von einer Komponente auf eine andere übertragen.
Standorte und Kontexte: Die Autoren führen Standorte (endliche Mengen inferonischer Atome) und eine kontextuelle Support-Relation $\Vdash^P_B$ ein. Dies ermöglicht die Modellierung von Informationsfluss, bei dem Constraints durch Implikation und die Regel „Inf" internalisiert werden, anstatt externe semantische Bedingungen zu sein.

4. Ergebnisse und Beispiele

Der Beitrag demonstriert die Nützlichkeit des Frameworks durch mehrere Beispiele:

Kein Rauch ohne Feuer: Formalisiert die „Abstimmung" auf Constraints als Inferenzregeln, die inferonische Basen verknüpfen. Es zeigt, wie ein Agent Informationen über eine ferne Situation (Feuer) basierend auf lokaler Wahrnehmung (Rauch) und einem geteilten Constraint ableiten kann, ohne direkten Zugriff auf die fernen Fakten zu haben.
Das Rätsel der weisen Männer: Modelliert das epistemische Rätsel unter Verwendung fester inferenzieller Fähigkeiten. Agenten reasoning über die Unfähigkeit anderer Agenten zu inferieren, was demonstriert, wie das Framework das Reasoning über Inferenz selbst handhabt, ohne die Exploration eines unbeschränkten Zustandsraums zu erfordern.
Zugriffskontrolle: Modelliert ein System, bei dem ein Passwort und ein Token zu Zugriff führen, und veranschaulicht, wie Constraints durch Implikation in der Logik internalisiert werden können.
Flughafensicherheit: Eine detaillierte Fallstudie (Abbildung 11), die den Informationsfluss (Pässe, Tickets, Gepäck) durch ein verteiltes System modelliert. Sie demonstriert, wie Standorte (verfügbare Information an einem Ort) und Basen (Reasoning-Fähigkeiten) sich entwickeln und über Kanäle interagieren, um die Systemintegrität sicherzustellen (z. B. Passagiere mit Gepäck abzugleichen).

5. Bedeutung und Behauptungen

Der Beitrag beansprucht, eine konzeptionell rigorose mathematisch-logische Begründung von Information zu liefern, die auf Inferenz und Reasoning fundiert ist. Seine Bedeutung liegt in:

Verschiebung der Fundamente: Der Wechsel von einer modelltheoretischen Sicht (Wahrheit in einem Modell) zu einer proof-theoretischen Sicht (Ableitbarkeit in einer Basis). Dies stimmt mit der inferentialistischen Philosophie überein, dass Bedeutung durch Verwendung bestimmt wird.
Adressierung der Kategorien von Van Benthem: Die Autoren argumentieren, dass ihr Ansatz primär Information als Korrelation (via Inferone und Situationen) adressiert, aber auch Wege bietet, Information als Bereich (via Bereiche von Basen) und Information als Code (via inferentialen Inhalt von Nachrichten) zu behandeln.
Modellierung verteilter Systeme: Es bietet eine auf Reasoning basierende Theorie des Informationsflusses, die auf die Organisation von Informationsverarbeitungssystemen anwendbar ist und ein Werkzeug zum Verständnis komplexer Ökosysteme bietet, ohne sich auf potenziell unhandhabbare globale Modelle zu verlassen.
Bescheidenheit: Die Autoren charakterisieren diese Arbeit als einen „ersten Schritt" hin zu einer vollständigen inferentialistischen Begründung. Sie räumen ein, dass tiefgehende Diskussionen über Veridizität, Agentur und die Integration mit anderen logischen Dynamiken (z. B. Van Benthems Arbeit) zukünftigen Arbeiten vorbehalten bleiben. Sie beanspruchen nicht, alle grundlegenden Probleme gelöst zu haben, sondern haben ein viable logisches Framework für weitere Entwicklungen etabliert.