💻 computer science

Knowing-Value Logic with Successor Arithmetic

Diese Arbeit erweitert die bedingte Knowing-Value-Logik um Gleichheit und Nachfolgearithmetik, um das Schließen unter arithmetischen Operationen zu handhaben, wobei sie die endliche Modell-Eigenschaft sowie Vollständigkeitsresultate über nicht-standardmäßige und standardmäßige Modelle etabliert und gleichzeitig deren Anwendung bei der Lösung des „Consecutive Numbers“-Rätsels mittels Public-Announcement-Operatoren demonstriert.

Ursprüngliche Autoren: Hongyi Wang (Department of Philosophy, Peking University)

Veröffentlicht 2026-07-01

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Hongyi Wang (Department of Philosophy, Peking University)

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 Rätsel zu lösen, aber anstatt nur zu wissen, dass etwas wahr ist (wie „Der Butler war es“), müssen Sie wissen, welcher spezifische Wert es ist (wie „Der Name des Butlers ist John“). Dies ist der Kern der „Knowing-Value“-Logik (Wissen-eines-Wertes-Logik).

Lange Zeit verfügten Logiker über ein Werkzeugset, um „Wissen-dass“ zu handhaben, aber wenn es um „Wissen-was“ ging, insbesondere wenn Zahlen im Spiel waren, waren ihre Werkzeuge etwas stumpf. Sie konnten sagen: „S weiß, dass das Passwort eine 4-stellige Zahl ist“, aber sie konnten nicht einfach erklären, welche interne Mathematik dahintersteckt oder wie die Zahlen zueinander in Beziehung stehen (wie zum Beispiel, dass 5 die nächste Zahl nach 4 ist).

Dieses Paper von Hongyi Wang baut ein neues, schärferes Werkzeugset auf, das die epistemische Logik (die Logik des Wissens) mit der Arithmetik (speziell dem Zählen und der „Nächste-Zahl-Regel“) kombiniert.

Hier ist eine Aufschreibung dessen, was das Paper macht, unter Verwendung einfacher Analogien:

1. Das Problem: Das „stumpfe Messer“

Betrachten Sie die alten Logiksysteme als ein stumpfes Messer. Sie konnten einen Satz wie „Anne weiß, dass die Zahlen aufeinanderfolgend sind“ zwar zerlegen, aber sie mussten „aufeinanderfolgend“ als einen einzigen, unzerbrechlichen Block behandeln (wie eine ganze Kartoffel). Sie konnten die Scheiben darin nicht sehen.

Das Problem: Im echten Leben denken wir oft über Zahlen nach. Wenn Anne weiß, dass die Zahlen aufeinanderfolgend sind, und sie weiß, dass ihre Zahl die 5 ist, sollte sie sofort wissen, dass Bills Zahl entweder 4 oder 6 ist. Die alte Logik konnte diese interne mathematische Struktur nicht erfassen. Sie behandelte „5“ und „6“ lediglich als zufällige Etiketten und nicht als Zahlen, die eine spezifische Beziehung zueinander haben (nämlich, dass die eine der „Nachfolger“ der anderen ist).

2. Die Lösung: Ein „Lasercutter“

Wang führt eine neue Logik namens ELKvSAr ein. Betrachten Sie dies als einen Lasercutter, der direkt durch die Mathematik schneiden kann.

Das neue Werkzeug: Es fügt eine Nachfolgefunktion hinzu (nennen wir sie S). Wenn man die Zahl 0 hat, dann ist S(0) die 1, S(1) ist die 2, und so weiter.
Das Ergebnis: Nun kann die Logik sagen: „Anne weiß, dass Bills Zahl der S von Annes Zahl ist.“ Dies bewahrt die interne Struktur der Mathematik und ermöglicht ein wesentlich präziseres Schließen.

3. Der „Paralleluniversum“-Trick (Nicht-standardmäßige Modelle)

Hier wird es etwas knifflig, aber das Paper verwendet einen cleveren Umweg.

Das Problem: Wenn man versucht zu beweisen, dass diese neue Logik perfekt für alle Standardzahlen (1, 2, 3...) funktioniert, stößt man auf eine mathematische Wand. Es ist, als versuche man, einen unendlichen Ozean in einen endlichen Eimer zu füllen; die Mathematik wird in der Standardweise „zu groß“, um handhabbar zu sein. Das Paper beweist, dass man kein perfektes, vollständiges Regelwerk für nur die Standardzahlen haben kann.
Der Umweg: Der Autor baut ein Paralleluniversum (genannt „nicht-standardmäßige Modelle“). Stellen Sie sich ein Universum vor, das exakt wie unsere Zahlenreihe aussieht, aber zusätzliche „Schleifen“ oder „Ketten“ von Zahlen angehängt hat.
Die Magie: In diesem Paralleluniversum funktioniert die Mathematik perfekt. Der Autor beweist, dass, wenn eine Aussage in diesem Paralleluniversum wahr ist, sie auch in unserer Standardwelt wahr ist. Es ist wie der Test eines Brückendesigns im Windkanal (das Paralleluniversum), um sicherzustellen, dass es in der echten Stadt (die Standardwelt) standhält.

4. Das „Aufeinanderfolgende Zahlen“-Rätsel

Um dieses neue Werkzeug zu demonstrieren, löst der Autor ein klassisches Rätsel:

Der Aufbau: Zwei Personen, Anne und Bill, werden gesagt, dass sie zwei aufeinanderfolgende natürliche Zahlen haben (wie 5 und 6). Anne flüstert ihre Zahl sich selbst zu, Bill flüstert seine. Sie können die Zahlen des jeweils anderen nicht sehen.
Das Gespräch:
1. Anne sagt: „Ich weiß deine Zahl nicht.“ (Dies verrät uns, dass ihre Zahl nicht 0 ist, denn wenn sie 0 hätte, wüsste sie, dass Bill die 1 haben muss).
2. Bill sagt: „Ich weiß deine Zahl nicht.“ (Dies verrät uns, dass seine Zahl nicht 0 oder 1 ist).
3. Anne sagt: „Jetzt weiß ich deine Zahl!“
4. Bill sagt: „Jetzt weiß ich deine!“
Die Logik: Mit der neuen „Lasercutter“-Logik formalisiert das Paper genau, wie jeder Satz die Schichten der Möglichkeiten abträgt, wobei die „Nachfolger“-Regel genutzt wird, um Zahlen Schritt für Schritt zu eliminieren, bis nur noch das korrekte Paar (1 und 2 oder 2 und 3) übrig bleibt. Es beweist, dass die Logik diese schrittweise Deduktion perfekt handhaben kann.

5. Das Fazit

Das Paper erreicht im Wesentlichen drei Dinge:

Es hat das Werkzeug gebaut: Es hat ein neues Logiksystem geschaffen, das versteht, wie man „einen Wert weiß“ mit „Zählen“ kombiniert.
Es hat bewiesen, dass das Werkzeug funktioniert: Es hat gezeigt, dass das System logisch fundiert und vollständig ist (das heißt, es kann alles beweisen, was wahr ist), indem es den „Paralleluniversum“-Trick verwendet hat.
Es hat bewiesen, dass das Werkzeug nutzbar ist: Es hat gezeigt, dass man diese Rätsel tatsächlich mit einem Computer lösen kann (das System ist „entscheidbar“), was bedeutet, dass man nicht in einer Endlosschleife stecken bleibt, während man versucht, sie zu lösen.

Kurz gesagt: Der Autor hat ein Logiksystem, das gut darin war, „Fakten zu wissen“, aufgerüstet, damit es gut darin ist, „Zahlen zu wissen“, hat einen cleveren mathematischen Trick verwendet, um sicherzustellen, dass das Upgrade solide ist, und es dann benutzt, um ein klassisches Knobelrätsel über aufeinanderfolgende Zahlen zu lösen.

Technische Zusammenfassung: Knowing-Value-Logik mit Nachfolger-Arithmetik

Problemstellung
Diese Arbeit setzt sich mit den Einschränkungen bestehender „Knowing-Value“-Logiken auseinander, insbesondere der konditionalen Knowing-Value-Logik ($ELKvr$) und ihrer Erweiterung durch öffentliche Bekanntgaben ($PALKvr$), die von Wang und Fan vorgeschlagen wurden. Während diese Systeme Aussagen wie „Agent $i$ kennt den Wert von $c$ unter der Bedingung $\phi$ “ formalisieren, fehlt ihnen die syntaktische Mechanik, um arithmetische Operationen und Gleichheit direkt zu handhaben. Folglich können sie die interne Struktur von Propositionen, die Zahlen involvieren, nicht erfassen, wie etwa die Beziehung zwischen aufeinanderfolgenden ganzen Zahlen. In natürlichen Sprachszenarien und Logikrätseln (z. B. dem „Consecutive Numbers“-Rätsel) basiert das Schließen oft auf der Interaktion zwischen epistemischen Operatoren, Gleichheit und arithmetischen Funktionen (speziell der Nachfolgerfunktion). Die bestehenden Frameworks behandeln numerische Bedingungen als opake Propositionalsymbole, wodurch sie nicht in der Lage sind, Implikationen abzuleiten, die in der natürlichen Sprache offensichtlich sind (z. B. dass das Wissen, eine Zahl sei vierstellig, und das Wissen der Implikation „wenn vierstellig, dann 1111“, das Wissen über den Wert 1111 implizieren sollte). Darüber hinaus sind die Standardsemantiken dieser Logiken, die auf unstrukturierten Mengen von Objekten basieren, unzureichend, um spezifische mathematische Strukturen wie die natürlichen Zahlen mit einer Nachfolgerfunktion abzubilden.

Methodik
Der Autor führt eine neue Logik ein, $ELKvSAr$ (das ankündigungsfreie Fragment von $PALKvSAr$), welche die konditionale Knowing-Value-Logik erweitert um:

Terme: Einschließlich einer rigiden Konstante $0$, nicht-rigider Konstanten $C$ und der Nachfolgerfunktion $S$ .
Atomare Formeln: Gleichheit zwischen Termen ( $t_1 \approx t_2$ ).
Semantik: Die Arbeit definiert zwei unterschiedliche Klassen von Modellen:
- Standardmodelle: Basierend auf den Standard-Natürlichen Zahlen $(\mathbb{N}, S)$ .
- Nicht-Standardmodelle: Basierend auf einem spezifischen nicht-standardmäßigen Modell der Nachfolger-Arithmetik $(\mathbb{N}^\star, S^\star)$ , wobei $\mathbb{N}^\star$ die Standard-Natürlichen Zahlen plus unendlich viele „Z-Ketten“ (Kopien der ganzen Zahlen) umfasst. Diese Erweiterung ist notwendig, da die Logik über die Klasse der Standardmodelle nicht kompakt ist.

Der technische Ansatz umfasst:

Axiomatisierung: Vorschlag des Systems $ELKVSAr$, welches Axiome für Gleichheit, Nachfolger-Arithmetik (z. B. $\neg Sx \approx 0$ , Injektivität von $S$ ) sowie spezifische Axiome/Regeln zur Verknüpfung von Knowing-Value und Arithmetik (z. B. $KvrS$, $KVE1$, $KVE2$) enthält. Ein wesentliches Merkmal ist die $Kvr$-Elim-Regel, die analog zur Existenzquantorelimination in der Prädikatenlogik erster Stufe funktioniert und es ermöglicht, relativierte Knowing-Value-Operatoren während der Ableitung zu entfernen.
Vollständigkeitsbeweis: Beweis der starken Vollständigkeit bezüglich nicht-standardmäßiger Modelle. Der Beweis nutzt eine neuartige Konstruktion eines baumartigen kanonischen Frames anstelle eines Standard-kanonischen Modells. Dies beinhaltet die Konstruktion von Historien maximal konsistenter Mengen und die Definition einer Bewertungsfunktion, die Konstanten auf Elemente in $\mathbb{N}^\star$ abbildet und dabei die durch den Knowing-Value-Operator induzierten Äquivalenzrelationen sowie die arithmetische Struktur respektiert.
Endliche Modell-Eigenschaft und Entscheidbarkeit: Nachweis, dass jede erfüllbare Formel ein endliches nicht-standardmäßiges Modell besitzt, welches dann über eine injektive Abbildung, die arithmetische Distanzen bewahrt und Komponenten trennt, auf ein endliches Standardmodell abgebildet werden kann. Dies etabliert die endliche Modell-Eigenschaft und die Entscheidbarkeit.
Anwendung: Formalisierung des „Consecutive Numbers“-Rätsels unter Verwendung von öffentlichen Bekanntnisoperatoren ($PALKvSAr$), um zu zeigen, wie sich das Wissen von Agenten durch arithmetische Deduktionen entwickelt.

Wesentliche Beiträge und Ergebnisse

Logik-Erweiterung: Die Einführung von $ELKvSAr$ und $PALKvSAr$, welche Gleichheit und die Nachfolgerfunktion in die konditionale Knowing-Value-Logik integrieren.
Axiomatisches System: Die Definition von $ELKVSAr$, das als stark vollständig bezüglich der Klasse der nicht-standardmäßigen Modelle und als schwach vollständig bezüglich der Klasse der Standardmodelle bewiesen wird.
Metalogische Eigenschaften:
- Endliche Modell-Eigenschaft (FMP): Die Logik besitzt die FMP sowohl bezüglich Standard- als auch Nicht-Standardmodellen.
- Entscheidbarkeit: Das Erfüllbarkeitsproblem für $ELKvSAr$ ist entscheidbar.
Nicht-Kompaktheit: Die Arbeit beweist, dass $ELKvSAr$ bezüglich der Standardmodelle nicht kompakt ist, was die Einführung nicht-standardmäßiger Modelle für den Vollständigkeitsbeweis motiviert.
Rätsellösung: Das „Consecutive Numbers“-Rätsel wird erfolgreich innerhalb des Systems formalisiert und gelöst, was zeigt, dass die Logik die schrittweise Eliminierung von Möglichkeiten basierend auf arithmetischen Beschränkungen und epistemischen Updates erfassen kann.

Bedeutung
Die Arbeit beansprucht, einen neuartigen Rahmen für die Integration von epistemischer Logik mit Arithmetik bereitzustellen. Durch die Anreicherung der Knowing-Value-Logik mit der Nachfolgerfunktion überwindet das System die grobkörnige Natur früherer Ansätze und ermöglicht die Formalisierung von Schlussfolgerungen, die von der internen Struktur numerischer Propositionen abhängen. Die Arbeit stellt ein Gleichgewicht zwischen Ausdrucksstärke (Handhabung von Arithmetik und epistemischer Interaktion) und computationaler Komplexität (Aufrechterhaltung der Entscheidbarkeit) her. Die Autoren merken an, dass dieses Framework die Grundlage für zukünftige Erweiterungen bildet, die komplexere arithmetische Strukturen (Addition und Multiplikation) beinhalten, welche für die Lösung von Rätseln wie „Sum and Product“ notwendig wären, wobei solche Erweiterungen erhebliche Herausforderungen hinsichtlich der Vollständigkeit und Entscheidbarkeit mit sich bringen.

1. Das Problem: Das „stumpfe Messer“

2. Die Lösung: Ein „Lasercutter“

3. Der „Paralleluniversum“-Trick (Nicht-standardmäßige Modelle)

4. Das „Aufeinanderfolgende Zahlen“-Rätsel

5. Das Fazit

Mehr davon