Beweisbarkeitsmodelle

Grundinformationen

• Papier-ID: 2510.06696
• Titel: Provability Models
• Autoren: Mojtaba Mojtahedi (Universität Gent), Borja Sierra Miranda (Universität Bern)
• Klassifizierung: math.LO (Mathematische Logik)
• Veröffentlichungsdatum: 15. Oktober 2025
• Papierlink: https://arxiv.org/abs/2510.06696

Zusammenfassung

Dieses Papier untersucht eine neue Kripke-ähnliche Semantik – Beweisbarkeitsmodelle (provability models) – für klassische Modallogiken. Die Forschung umfasst Beweisbarkeitsmodelle für die propositionalen Modallogiken K, K4, S4, GL, GLP sowie die Interpretierbarkeitslogik ILM. Beweisbarkeitsmodelle kombinieren Merkmale von Kripke-Modellen mit dem Ansatz, einzelnen Welten Logiken zuzuordnen. Das Modell wurde ursprünglich von Mojtahedi 2022 eingeführt, um arithmetische Vollständigkeit für intuitionistische Beweisbarkeitslogik zu etablieren. Bemerkenswert ist, dass dieses Papier zeigt, dass ILM für dieselben Beweisbarkeitsmodelle wie GL vollständig ist. Im Fall von GL und ILM werden Beweisbarkeitsmodelle zu vorhersagbaren und entscheidbaren Beweisbarkeitsmodellen verfeinert, und es wird die Solidität und Vollständigkeit von GLP für Beweisbarkeitsmodelle nachgewiesen.

Forschungshintergrund und Motivation

Kernproblem

In der traditionellen Beweisbarkeitslogikforschung werden Modaloperatoren typischerweise als Beweisbarkeitsprädikate in einem bestimmten System der Arithmetik erster Ordnung oder der Mengenlehre interpretiert. Alternativ kann □A als L ⊢ A interpretiert werden (für eine gegebene propositionale Theorie L). Obwohl für jede Logik L, die GL enthält, gezeigt werden kann, dass GL für L-Interpretationen solid ist, kann keine solche L-Interpretation Vollständigkeit für GL liefern.

Bedeutung des Problems

Dieses Scheitern steht im Gegensatz zu PA-Interpretationen und entsteht hauptsächlich, weil die Logik L keine Kripke-Modelle simulieren kann, während die Peano-Arithmetik ihre Fähigkeit nutzen kann, Kripke-Modelle zu simulieren (wie von Solovay gezeigt). Daher kann nicht erwartet werden, dass GL die Beweisbarkeitslogik einer einzelnen propositionalen Logik ist.

Einschränkungen bestehender Ansätze

1. Beschränkungen standardmäßiger Kripke-Modelle: Können arithmetische Interpretationen der Beweisbarkeitslogik nicht direkt behandeln
2. Unvollständigkeit propositionaler Beweisbarkeitsinterpretationen: Eine einzelne propositionale Logik kann keine Vollständigkeit für GL liefern
3. Komplexe Rahmeneigenschaften: Wie in Iemhoffs Semantik erschweren komplexe Rahmeneigenschaften die Etablierung arithmetischer Vollständigkeitssätze

Forschungsmotivation

Dieses Papier überbrückt diese Einschränkung, indem es Kripke-Rahmen explizit in propositionale Logiken integriert, standardmäßige Kripke-Modelle betrachtet, bei denen jede Welt w mit einer Logik Lw ausgestattet ist, und Erreichbarkeitsverhältnisse zwischen diesen Theorien basierend auf der zugrunde liegenden Erreichbarkeitsrelation auferlegt.

Kernbeiträge

1. Einführung des Beweisbarkeitsmodell-Rahmens: Neue Kripke-ähnliche Semantik für klassische Modallogiken
2. Etablierung von Vollständigkeit für mehrere Modallogiken: Nachweis von Solidität und Vollständigkeit für K, K4, S4, GL für Beweisbarkeitsmodelle
3. Konstruktion unabhängiger Beweisbarkeitsmodelle: Besonders für GL und ILM, Demonstration von Beweisbarkeitsmodellen unabhängig von standardmäßigen Kripke-Modellen
4. Realisierung von Entscheidbarkeit: Im Fall von GL und ILM Konstruktion entscheidbarer Beweisbarkeitsmodelle
5. Erweiterung auf multimodale Logik: Nachweis von Solidität und Vollständigkeit von GLP (multimodale Beweisbarkeitslogik) für Beweisbarkeitsmodelle
6. Etablierung der ILM-Vollständigkeit: Nachweis, dass die Interpretierbarkeitslogik ILM für dieselben Beweisbarkeitsmodelle wie GL vollständig ist

Methodische Details

Aufgabendefinition

Untersuchung von Beweisbarkeitsmodellen als Semantik für Modallogiken, wobei:

• Eingabe: Modallogische Formeln und Beweisbarkeitsmodelle
• Ausgabe: Beurteilung der Gültigkeit von Formeln im Modell
• Einschränkungen: Modelle müssen spezifische logische Eigenschaften und Rahmenbedingungen erfüllen

Modellarchitektur

Definition von Beweisbarkeits-Vormodellen

Ein Beweisbarkeits-Vormodell P = (W, <, {Lw}w∈W, V) enthält:

• W: nicht-leere Menge von Welten
• <: binäre Relation auf W
• Lw: Logik für jede <-erreichbare Welt w
• V: Bewertungsrelation für Atomformeln

Gültigkeitsdefinition

Für eine Formel A wird P, w |= A induktiv definiert durch:

• Kompatibilität mit booleschen Konnektiven
• P, w |= □A genau dann, wenn ∀u ⪯ w (⊢u A)

Beweisbarkeitsmodell-Bedingungen

Ein Beweisbarkeits-Vormodell wird zu einem Beweisbarkeitsmodell, wenn es erfüllt:

• Modale Vollständigkeit: Für jede reine Modalformel A, wenn P, w |=+ A dann ⊢w A

Technische Innovationen

1. Logisierung von Rahmenbedingungen

Beweisbarkeitsmodelle können Rahmenbedingungen als Inferenzregeln der einzelnen Welten zugeordneten Logiken absorbieren:

• Transitivität kann durch Notwendigkeitsregel ersetzt werden
• Inverse Wohlgegründetheit kann durch Löb-Regel ersetzt werden

2. Konstruktive Methoden

Für GL und ILM werden konstruktive Methoden zur Konstruktion von Beweisbarkeitsmodellen bereitgestellt:

Satz 4.4: Für jeden invers wohlgegründeten Baum-Beweisbarkeits-Vormodell P existiert ein Beweisbarkeitsmodell P̄ mit Notwendigkeitsregel, so dass:

• P̄ hat Notwendigkeitsregel
• P ⊆ P̄
• P̄ ist das kleinste Beweisbarkeitsmodell, das P enthält

3. Entscheidbarkeitssicherung

Wenn P bifinit ist, dann ist P̄ entscheidbar, wobei bifinit bedeutet, dass W und Axiom(Lw) für jedes w∈W endlich sind.

Experimentelle Einrichtung

Theoretischer Verifikationsrahmen

Das Papier führt hauptsächlich theoretische Beweise durch; der Verifikationsrahmen umfasst:

1. Soliditätsbeweise

Für verschiedene Modallogiken wird nachgewiesen, dass wenn die Logik ⊢ A, dann P |= A für alle entsprechenden Beweisbarkeitsmodelle P gilt.

2. Vollständigkeitsbeweise

Nachweis, dass wenn P |= A für alle entsprechenden Beweisbarkeitsmodelle P, dann die Logik ⊢ A.

3. Starke Vollständigkeit

Besonders für GL wird starke Vollständigkeit nachgewiesen: Γ |=P A impliziert Γ ⊢GL A.

Verifikation von Konstruktionsmethoden

Durch konkrete Konstruktionen wird verifiziert:

• Existenz endlicher Beweisbarkeitsmodelle
• Realisierung von Entscheidbarkeit
• Unabhängigkeit (nicht abhängig von standardmäßigen Kripke-Modellen)

Experimentelle Ergebnisse

Hauptergebnisse

1. Vollständigkeit grundlegender Modallogiken

• K: Solid und vollständig für Beweisbarkeitsmodelle (Sätze 3.6, 3.7)
• K4: Solid und vollständig für Beweisbarkeitsmodelle mit Notwendigkeitsregel oder Transitivität (Sätze 3.8, 3.9)
• S4: Solid und vollständig für reflexive, transitive Beweisbarkeitsmodelle mit Notwendigkeitsregel und lokaler Vollständigkeit (Sätze 3.11, 3.12)

2. Ergebnisse für Beweisbarkeitslogik GL

• Solidität: GL ist solid für invers wohlgegründete Beweisbarkeitsmodelle mit Notwendigkeitsregel und Löb-Regel (Satz 3.14)
• Vollständigkeit: GL ist vollständig für endliche transitive nicht-reflexive Beweisbarkeitsmodelle (Satz 3.17)
• Starke Vollständigkeit: GL ist stark vollständig für Beweisbarkeitsmodelle mit Notwendigkeitsregel und Löb-Regel (Satz 3.18)
• Endlichkeitsvollständigkeit: GL ist vollständig für Endlichkeits-Beweisbarkeitsmodelle (Satz 4.6)

3. Ergebnisse für Interpretierbarkeitslogik ILM

• Solidität: ILM ist solid für invers wohlgegründete Beweisbarkeitsmodelle mit Notwendigkeitsregel (Satz 5.6)
• Vollständigkeit: ILM ist vollständig für endliche Baum-invers wohlgegründete Beweisbarkeitsmodelle mit Notwendigkeitsregel (Satz 5.10)
• Endlichkeitsvollständigkeit: ILM ist vollständig für Endlichkeits-Beweisbarkeitsmodelle (Satz 5.13)

4. Ergebnisse für multimodale Beweisbarkeitslogik GLP

• Solidität und Vollständigkeit: GLP ist solid und stark vollständig für Multi-Beweisbarkeits-GLP-Modelle (Sätze 6.2, 6.3)

Konstruktive Ergebnisse

Erfolgreiche Konstruktion von Beweisbarkeitsmodellen unabhängig von standardmäßigen Kripke-Modellen, besonders:

• Für jeden invers wohlgegründeten Baum-Rahmen und jede Zuweisung von Formelmengen zu Knoten kann das minimale Beweisbarkeitsmodell konstruiert werden
• Im bifiniten Fall ist das konstruierte Modell entscheidbar

Verwandte Arbeiten

Traditionelle Beweisbarkeitslogikforschung

• Solovay (1976): Etablierung der Beweisbarkeitslogik von PA
• Boolos (1995), Smoryński (1985): Klassische Lehrbücher der Beweisbarkeitslogik
• Artemov und Beklemishev (2004): Umfassende Übersicht

Semantische Ansätze

• Standardmäßige Kripke-Semantik: Für verschiedene Modallogiken
• Veltman-Modelle: Für Interpretierbarkeitslogik ILM
• Topologische Semantik: Für GLP-Vollständigkeit

Intuitionistische Beweisbarkeitslogik

• Iemhoff (2001-2003): Einführung von Iemhoffs Semantik
• Mojtahedi (2022): Erste Verwendung von Beweisbarkeitsmodellen zur Etablierung arithmetischer Vollständigkeit für intuitionistische Beweisbarkeitslogik

Schlussfolgerungen und Diskussion

Hauptschlussfolgerungen

1. Einheitlicher Rahmen: Beweisbarkeitsmodelle bieten einen einheitlichen semantischen Rahmen für mehrere Modallogiken
2. Konstruktivität: Besonders für GL und ILM können unabhängige Beweisbarkeitsmodelle konstruktiv etabliert werden
3. Entscheidbarkeit: Unter angemessenen Bedingungen sind Beweisbarkeitsmodelle entscheidbar
4. Flexibilität: Rahmenbedingungen können durch logische Eigenschaften ersetzt werden, was größere Flexibilität bietet

Einschränkungen

1. GLP-Einschränkungen: Für GLP wurde noch keine entscheidbare Beweisbarkeitsmodell-Klasse gefunden
2. Konstruktionskomplexität: Einige Konstruktionen (wie kanonische Modelle für GLP) sind möglicherweise nicht konstruktiv
3. Anwendungsbereich: Hauptsächlich anwendbar auf Logiken mit Beweisbarkeitseigenschaften

Zukünftige Richtungen

Das Papier stellt explizit mehrere offene Fragen:

1. Erweiterung auf Beweislogiken: Definition von Beweisbarkeits-Stil-Modellen für Beweislogik LP und JGL
2. Intuitionistische Modallogik: Definition von Beweisbarkeitsmodellen für intuitionistische Modallogiken mit zwei Modaloperatoren □ und ◇
3. Entscheidbare Modelle für GLP: Suche nach entscheidbaren Beweisbarkeitsmodell-Klassen für GLP
4. Vereinfachung arithmetischer Vollständigkeit: Erforschung, ob arithmetische Vollständigkeit für ILM durch Beweisbarkeitsmodelle vereinfacht werden kann

Tiefgreifende Bewertung

Stärken

1. Theoretische Innovation: Einführung eines völlig neuen semantischen Rahmens, der mehrere Modallogiken einheitlich behandelt
2. Technische Tiefe: Bereitstellung detaillierter mathematischer Beweise und Konstruktionsmethoden
3. Praktischer Wert: Besonders Verbesserungen in der Entscheidbarkeit sind von großer Bedeutung
4. Systematik: Systematische Behandlung von grundlegenden Modallogiken bis zu komplexen Beweisbarkeitslogiken

Schwächen

1. Komplexität: Die Komplexität einiger Konstruktionen (besonders GLP) kann ihre praktische Anwendung einschränken
2. Offene Probleme: Wichtige offene Probleme bleiben ungelöst, wie entscheidbare Modelle für GLP
3. Anwendungsbereich: Hauptsächlich auf theoretische Forschung beschränkt; praktischer Anwendungswert bleibt zu erforschen

Einflussfähigkeit

1. Theoretischer Beitrag: Bietet neue Forschungsrichtungen für Modallogik-Semantik
2. Methodologischer Wert: Die Logisierungsmethode von Rahmenbedingungen hat universelle Bedeutung
3. Nachfolgeforschung: Bietet neue Werkzeuge für Forschung in intuitionistischer Logik, Beweislogik und anderen Bereichen

Anwendungsszenarien

1. Beweisbarkeitslogikforschung: Besonders geeignet für Forschung, die arithmetische Vollständigkeit erfordert
2. Modallogik-Semantik: Bietet neue semantische Methoden für komplexe Modallogiken
3. Rechnerische Logik: Potenzieller Wert in Anwendungen, die Entscheidbarkeit erfordern

Literaturverzeichnis

Das Papier zitiert umfangreiche relevante Literatur, einschließlich:

• Klassische Literatur der Beweisbarkeitslogik (Boolos, Smoryński, Solovay etc.)
• Wichtige Arbeiten zur Modallogik-Semantik (Blackburn etc.)
• Schlüsselforschung zur Interpretierbarkeitslogik (Berarducci, Shavrukov etc.)
• Verwandte Arbeiten zur intuitionistischen Beweisbarkeitslogik (Iemhoff etc.)

Dieses Papier leistet wichtige theoretische Beiträge im Bereich der Modallogik-Semantik und bietet einen neuen einheitlichen Rahmen zur Behandlung verschiedener Beweisbarkeitslogiken, während es gleichzeitig bedeutende Fortschritte in Konstruktivität und Entscheidbarkeit erzielt. Obwohl noch einige offene Fragen bestehen, legt diese Arbeit eine solide Grundlage für nachfolgende Forschungen.