Provabilitätslogik

2023 Autor: Noah Black | [email protected]. Zuletzt bearbeitet: 2023-05-24 11:17

Eintragsnavigation

• Eintragsinhalt
• Literaturverzeichnis
• Akademische Werkzeuge
• Freunde PDF Vorschau
• Autor und Zitierinfo
• Zurück nach oben

Provabilitätslogik

Erstveröffentlichung Mi 2. April 2003; inhaltliche Überarbeitung Mi 5. April 2017

Die Provabilitätslogik ist eine modale Logik, mit der untersucht wird, was arithmetische Theorien in einer eingeschränkten Sprache über ihre Provabilitätsprädikate ausdrücken können. Die Logik wurde von Entwicklungen in der Metamathematik wie Gödels Unvollständigkeitssätzen von 1931 und Löbs Satz von 1953 inspiriert. Als modale Logik wurde die Beweisbarkeitslogik seit Anfang der siebziger Jahre untersucht und hatte wichtige Anwendungen in den Grundlagen der Mathematik.

Aus philosophischer Sicht ist die Beweisbarkeitslogik interessant, weil das Konzept der Beweisbarkeit in einer festen Theorie der Arithmetik eine einzigartige und unproblematische Bedeutung hat, abgesehen von Konzepten wie Notwendigkeit und Wissen, die in der modalen und epistemischen Logik untersucht wurden. Darüber hinaus bietet die Beweisbarkeitslogik Werkzeuge, um den Begriff der Selbstreferenz zu untersuchen.

• 1. Die Geschichte der Beweisbarkeitslogik

• 2. Das Axiomensystem der Aussagenprüfbarkeitslogik

  • 2.1 Axiome und Regeln
  • 2.2 Der Fixpunktsatz

• 3. Mögliche Weltsemantik und topologische Semantik

  • 3.1 Charakterisierung und modale Solidität
  • 3.2 Modale Vollständigkeit
  • 3.3 Mangel an vollständiger Vollständigkeit
  • 3.4 Topologische Semantik für die Beweisbarkeitslogik

• 4. Provabilitätslogik und Peano-Arithmetik

  • 4.1 Arithmetische Solidität
  • 4.2 Arithmetische Vollständigkeit

• 5. Der Umfang der Beweisbarkeitslogik

  • 5.1 Grenzen
  • 5.2 Interpretierbarkeitslogik
  • 5.3 Aussagenquantifizierer
  • 5.4 Japaridzes bimodale und polymodale Beweisbarkeitslogik
  • 5.5 Prädikatenprüfbarkeitslogik
  • 5.6 Andere Verallgemeinerungen
• 6. Philosophische Bedeutung
• Literaturverzeichnis
• Akademische Werkzeuge

• Andere Internetquellen

  • Beiträge und Präsentationen
  • Andere Seiten
• Verwandte Einträge

1. Die Geschichte der Beweisbarkeitslogik

Zwei Forschungsstränge haben zur Geburt der Beweisbarkeitslogik geführt. Der erste stammt aus einer Arbeit von K. Gödel (1933), in der er Übersetzungen von der intuitionistischen Aussagenlogik in die Modallogik (genauer gesagt in das heutzutage als S4 bezeichnete System) einführt und kurz erwähnt, dass die Beweisbarkeit als Modaloperator angesehen werden kann. Noch früher begann CI Lewis mit dem modernen Studium der Modallogik, indem er eine strikte Implikation als eine Art Deduzierbarkeit einführte, wobei er in einem formalen System wie Principia Mathematica Deduzierbarkeit gemeint haben könnte, was jedoch aus seinen Schriften nicht klar hervorgeht.

Der andere Strang beginnt mit der Erforschung der Metamathematik: Was können mathematische Theorien über sich selbst sagen, indem sie interessante Eigenschaften codieren? 1952 stellte L. Henkin eine täuschend einfache Frage, die von Gödels Unvollständigkeitssätzen inspiriert war. Um Henkins Frage zu formulieren, sind weitere Hintergrundinformationen erforderlich. Zur Erinnerung: Gödels erster Unvollständigkeitssatz besagt, dass für eine ausreichend starke formale Theorie wie Peano Arithmetic jeder Satz, der seine eigene Unbeweisbarkeit behauptet, tatsächlich unbeweisbar ist. Andererseits kann man von „außerhalb“der formalen Theorie sehen, dass ein solcher Satz im Standardmodell wahr ist, was auf eine wichtige Unterscheidung zwischen Wahrheit und Beweisbarkeit hinweist.

Formaler sei (ulcorner A \ urcorner) die Gödel-Zahl der arithmetischen Formel (A), die das Ergebnis der Zuweisung eines numerischen Codes zu (A) ist. Sei (Prov) das formalisierte Beweisbarkeitsprädikat für Peano Arithmetic, das die Form (existiert p \, \ Proof (p, x)) hat. Hier ist (Proof) das formalisierte Beweisprädikat der Peano-Arithmetik, und (Proof (p, x)) steht für „Gödel-Zahl (p) codiert einen korrekten Beweis aus den Axiomen der Peano-Arithmetik von die Formel mit der Gödel-Zahl (x)”. (Für eine genauere Formulierung siehe Smoryński (1985), Davis (1958).) Nehmen wir nun an, dass Peano Arithmetic beweist, dass (A \ leftrightarrow \ neg) (Prov (ulcorner A \ urcorner)) Nach Gödels Ergebnis ist (A) in der Peano-Arithmetik nicht beweisbar, und daher ist es wahr, denn tatsächlich besagt der selbstreferenzielle Satz (A) "Ich bin nicht beweisbar".

Henkin hingegen wollte wissen, ob etwas über Sätze gesagt werden kann, die ihre eigene Beweisbarkeit behaupten: Angenommen, Peano Arithmetic beweist (B \ leftrightarrow \ Prov (ulcorner B \ urcorner)), was bedeutet dies für (B.)? Drei Jahre später nahm M. Löb die Herausforderung an und beantwortete Henkins Frage auf überraschende Weise. Obwohl alle in Peano Arithmetic nachweisbaren Sätze tatsächlich für die natürlichen Zahlen zutreffen, hat Löb gezeigt, dass die formalisierte Version dieser Tatsache, (Prov (ulcorner B \ urcorner) rightarrow B), nur in Peano Arithmetic bewiesen werden kann in dem trivialen Fall, dass Peano Arithmetic bereits (B) selbst beweist. Dieses Ergebnis, das jetzt als Satz von Löb bezeichnet wird, beantwortet sofort Henkins Frage. (Einen Beweis für Löbs Theorem finden Sie in Abschnitt 4.) Löb zeigte auch eine formalisierte Version seines Theorems.nämlich, dass Peano Arithmetic beweist

) Prov (ulcorner \ Prov (ulcorner B \ urcorner) rightarrow B \ urcorner) rightarrow \ Prov (ulcorner B \ urcorner).)

In derselben Arbeit formulierte Löb drei Bedingungen für das Beweisprädikat der Peano-Arithmetik, die eine nützliche Modifikation der komplizierten Bedingungen darstellen, die Hilbert und Bernays 1939 eingeführt haben, um Gödels zweiten Unvollständigkeitssatz zu beweisen. Im Folgenden wird die Ableitbarkeit von (A) aus der Peano-Arithmetik mit (PA \ vdash A) bezeichnet:

1. Wenn (PA \ vdash A), dann (PA \ vdash \ Prov (ulcorner A \ urcorner));
2. (PA \ vdash \ Prov (ulcorner A \ rightarrow B \ urcorner) rightarrow (Prov (ulcorner A \ urcorner) rightarrow \ Prov (ulcorner B \ urcorner));)
3. (PA \ vdash \ Prov (ulcorner A \ urcorner) rightarrow \ Prov (ulcorner \ Prov (ulcorner A \ urcorner) urcorner).)

Diese Löb-Bedingungen, wie sie heutzutage genannt werden, scheinen nach einer modalen logischen Untersuchung zu verlangen, bei der die Modalität (Box) für Beweisbarkeit in PA steht. Ironischerweise wurde das erste Mal, dass die formalisierte Version von Löbs Theorem als Modalprinzip angegeben wurde

) Box (Box A \ rechter Pfeil A) rechter Pfeil \ Box A)

war in einem Artikel von Smiley im Jahr 1963 über die logische Grundlage der Ethik, die überhaupt nicht arithmetisch berücksichtigte. Relevantere Untersuchungen begannen jedoch erst fast zwanzig Jahre nach Veröffentlichung von Löbs Artikel ernsthaft. In den frühen 1970er Jahren entwickelte sich rasch die Logik der Aussagenprüfbarkeit, bei der mehrere Forscher in verschiedenen Ländern unabhängig voneinander die wichtigsten Ergebnisse nachweisen konnten, die in den Abschnitten 2, 3 und 4 erörtert wurden. Es stellte sich heraus, dass die Logik der Aussagenprüfbarkeit genau das erfasst, was viele formale Theorien der Arithmetik können sagen Sie mit Aussagen über ihr eigenes Beweisbarkeitsprädikat. In jüngerer Zeit haben Forscher die Grenzen dieses Ansatzes untersucht und mehrere interessante, aussagekräftigere Erweiterungen der Beweisbarkeitslogik vorgeschlagen (siehe Abschnitt 5).

2. Das Axiomensystem der Aussagenprüfbarkeitslogik

Die logische Sprache der Aussagenprüfbarkeitslogik enthält neben Satzatomen und den üblichen wahrheitsfunktionalen Operatoren sowie dem Widerspruchsymbol (bot) einen Modaloperator (Box) mit der beabsichtigten Bedeutung „nachweisbar in (T)”, wobei (T) eine ausreichend starke formale Theorie ist, sagen wir Peano Arithmetic (siehe Abschnitt 4). (Diamond A) ist eine Abkürzung für (neg \, \ Box \ neg \, A). Somit ist die Sprache dieselbe wie die von Modalsystemen wie K und S4, die in der Eingangsmodallogik dargestellt sind.

2.1 Axiome und Regeln

Die Aussagenprüfbarkeitslogik wird nach Gödel und Löb oft als GL bezeichnet. (Alternative Namen, die in der Literatur für äquivalente Systeme gefunden werden, sind L, G, KW, K4W und PrL). Der logische GL ergibt sich aus dem Hinzufügen des folgenden Axioms zur grundlegenden modalen Logik K:

) tag {GL} Box (Box A \ rightarrow A) rightarrow \ Box A.)

Zur Erinnerung: Da GL K erweitert, enthält es alle Formeln, die die Form einer Satztautologie haben. Aus dem gleichen Grund enthält der GL die

) tag {Verteilungsaxiom} Box (A \ rightarrow B) rightarrow (Box A \ rightarrow \ Box B).)

Darüber hinaus wird es gemäß der Modus Ponens-Regel geschlossen, die es ermöglicht, (B) von (A \ rightarrow B) und (A) abzuleiten, und der Generalisierungsregel, die besagt, dass if (A) ist ein Satz von GL, dann ist es auch (Box A).

Der Begriff (GL \ vdash A) bezeichnet die Beweisbarkeit einer Modalformel (A) in der Aussagenprüfbarkeitslogik. Es ist nicht schwer zu erkennen, dass das Modalaxiom (Box A \ rightarrow \ Box \ Box A) (bekannt als Axiom 4 der Modallogik) im GL tatsächlich beweisbar ist. Um dies zu beweisen, verwendet man die Substitution (A \ Wedge \ Box A) für (A) im Axiom (GL). Wenn man dann sieht, dass der Vorgänger der resultierenden Implikation aus (Box A) folgt, wendet man das Verteilungsaxiom und die Generalisierungsregel sowie eine Aussagenlogik an. Sofern nicht ausdrücklich anders angegeben, steht in der Folge „Beweisbarkeitslogik“für das System GL der Aussagenprüfbarkeitslogik.

In Bezug auf die Beweistheorie der Beweisbarkeitslogik hat Valentini (1983) bewiesen, dass eine Standardformulierung für sequentielle Berechnungen von GL der Eliminierung von Schnitten gehorcht, was grob formuliert bedeutet, dass jede Formel, die aus GL in der sequentiellen Berechnung nachweisbar ist, auch einen sequentiellen GL-Beweis „ohne Umwege “(siehe den Eintrag zur Entwicklung der Beweistheorie für eine genaue Erklärung der Schnitteliminierung). In den letzten Jahren hat das Interesse an der Beweistheorie des GL erneut zugenommen, siehe zum Beispiel Goré und Ramanayake (2008). Die Schnitteliminierung führt zu der gewünschten Subformeleigenschaft für GL, da alle Formeln, die in einem schnittfreien Beweis erscheinen, Unterformeln der nachfolgenden Formeln sind.

Für neuere beweistheoretische Untersuchungen der Beweisbarkeitslogik basierend auf verschiedenen schnittfreien Sequenzkalkülen siehe (Negri 2005, 2014; Poggiolesi 2009). Negri präsentiert zwei äquivalente markierte Sequenzkalküle für GL und einen syntaktischen Beweis für die Eliminierung von Schnitten. Auch wenn für diese Kalküle aufgrund der Kennzeichnung keine vollständige Subformeleigenschaft gilt, können die üblichen Konsequenzen der Subformeleigenschaft festgestellt werden: Der markierte Formalismus ermöglicht einen direkten Vollständigkeitsnachweis, mit dem sowohl die Entscheidbarkeit als auch das endliche Modell festgestellt werden können Eigenschaft, was bedeutet, dass jede Formel, die nicht beweisbar ist, ein endliches Gegenmodell hat.

Eine faszinierende neue beweistheoretische Entwicklung ist Shamkanovs Erweiterung sequentieller Beweissysteme durch zirkuläre Beweise (Shamkanov 2014). Betrachten Sie ein sequentielles System für K4, das aus GL resultierende modale System, indem Sie das Axiom GL durch das schwächere Axiom (Box A \ rightarrow \ Box \ Box A) ersetzen (Axiom 4). Nehmen wir jedoch an, dass offene Hypothesen zulässig sind, vorausgesetzt, dass dieselbe Sequenz genau unterhalb dieser Hypothese im Beweisbaum auftritt. Technischer formuliert kann man eine kreisförmige Ableitung von einem gewöhnlichen Ableitungsbaum finden, indem man jedes seiner nicht axiomatischen Blätter mit einem identischen inneren Knoten verbindet. Shamkanov (2014) hat bewiesen, dass das resultierende System konsistent ist und dass darüber hinaus im Allgemeinen jede Sequenz genau dann eine GL-Ableitung aufweist, wenn sie eine zirkuläre K4-Ableitung aufweist. Zirkuläre Beweise bieten auch eine Methode, um theoretisch zu beweisen, dass Lyndons Interpolationssatz für GL gilt. Die Standardinterpolation für GL wurde bereits zuvor mit verschiedenen Methoden nachgewiesen (Boolos 1979; Smoryński 1978; Rautenberg 1983). (Weitere Informationen zu Lyndons Interpolationssatz für die Logik erster Ordnung finden Sie auch im Eintrag Modelltheorie erster Ordnung.)

2.2 Der Fixpunktsatz

Das wichtigste „modale“Ergebnis der Beweisbarkeitslogik ist der Fixpunktsatz, den D. de Jongh und G. Sambin 1975 unabhängig voneinander bewiesen haben (Sambin 1976). Obwohl es durch streng modale Methoden formuliert und bewiesen wird, hat der Fixpunktsatz immer noch eine große arithmetische Bedeutung. Es heißt im Wesentlichen, dass Selbstreferenz im folgenden Sinne nicht wirklich notwendig ist. Angenommen, alle Vorkommen der Satzvariablen (p) in einer gegebenen Formel (A (p)) fallen in den Geltungsbereich des Beweisbarkeitsoperators, zum Beispiel (A (p) = \ neg \ Box p) oder (A (p) = \ Box (p \ rightarrow q)). Dann gibt es eine Formel (B), in der (p) nicht erscheint, so dass alle in (B) vorkommenden Satzvariablen bereits in (A (p)) erscheinen, und zwar so

) GL \ vdash B \ leftrightarrow A (B).)

Diese Formel (B) wird als Fixpunkt von (A (p)) bezeichnet. Darüber hinaus ist der Fixpunkt eindeutig oder genauer, wenn es eine andere Formel (C) gibt, so dass (GL \ vdash C \ leftrightarrow A (C)), dann müssen wir (GL \ vdash haben B \ leftrightarrow C). Die meisten Beweise in der Literatur geben einen Algorithmus an, mit dem man den Fixpunkt berechnen kann (siehe Smoryński 1985, Boolos 1993, Sambin und Valentini 1982, Lindström 2006). Ein besonders kurzer und klarer Beweis sowie ein sehr effizienter Algorithmus zur Berechnung von Fixpunkten findet sich in Reidhaar-Olson (1990).

Angenommen, (A (p) = \ neg \, \ Box p). Dann ist der durch einen solchen Algorithmus erzeugte Fixpunkt (neg \, \ Box \ bot), und tatsächlich kann man das beweisen

) GL \ vdash \ neg \, \ Box \ bot \ leftrightarrow \ neg \, \ Box (neg \, \ Box \ bot).)

Wenn dies arithmetisch gelesen wird, ist die Richtung von links nach rechts nur die formalisierte Version von Gödels zweitem Unvollständigkeitssatz: Wenn eine ausreichend starke formale Theorie (T) wie Peano Arithmetic keinen Widerspruch beweist, dann ist sie in \ nicht beweisbar (T) dass (T) keinen Widerspruch beweist. Ausreichend starke konsistente arithmetische Theorien können daher ihre eigene Konsistenz nicht beweisen. Wir werden uns in Abschnitt 4 genauer mit der Beziehung zwischen Beweisbarkeitslogik und Arithmetik befassen. Zu diesem Zweck muss jedoch zunächst ein weiterer „modaler“Aspekt des GL bereitgestellt werden: die Semantik.

3. Mögliche Weltsemantik und topologische Semantik

Die Provabilitätslogik hat wie viele andere modale Logiken eine geeignete mögliche Weltsemantik. Zur Erinnerung, ein mögliches Weltenmodell (oder Kripke-Modell) ist ein Dreifach (M = \ langle W, R, V \ rangle), wobei (W) eine nicht leere Menge möglicher Welten ist (R) ist eine binäre Zugänglichkeitsrelation für (W), und (V) ist eine Bewertung, die jeder Satzvariablen für jede Welt in (W) einen Wahrheitswert zuweist. Das Paar (F = \ langle W, R \ rangle) wird als Rahmen dieses Modells bezeichnet. Der Wahrheitsbegriff einer Formel (A) in einem Modell (M) in einer Welt (W), Notation (M, w \ Modelle A), wird induktiv definiert. Wiederholen wir nur die interessanteste Klausel, die für den Beweisbarkeitsoperator (Box):

[M, w \ Modelle \ Box A \ Text {iff für jedes} w ', \ Text {wenn} wRw', \ Text {dann} M, w '\ Modelle A.)

Weitere Informationen zur Semantik möglicher Welten im Allgemeinen finden Sie in der Modallogik des Eintrags.

3.1 Charakterisierung und modale Solidität

Die Modallogik K gilt für alle Kripke-Modelle. Die Erweiterung GL lautet jedoch nicht: Wir müssen die Klasse der möglichen Weltenmodelle auf eine geeignetere beschränken. Nehmen wir an, dass eine Formel (A) in Frame (F), Notation (F \ Modelle A) gültig ist, wenn (A) in allen Welten in Kripke-Modellen (M) wahr ist. basierend auf (F). Es stellt sich heraus, dass das neue Axiom (GL) der Beweisbarkeitslogik einer Bedingung für Frames wie folgt entspricht:

Für alle Frames (F = \ langle W, R \ rangle, F \ models \ Box (Box p \ rightarrow p) rightarrow \ Box p) ist iff (R) transitiv und umgekehrt begründet.

Hier ist Transitivität die bekannte Eigenschaft, dass für alle Welten (w_1), (w_2), (w_3) in (W), wenn (w_1 Rw_2) und (w_2 Rw_3)), dann (w_1 Rw_3). Eine Beziehung ist umgekehrt begründet, wenn es keine unendlichen aufsteigenden Sequenzen gibt, dh Sequenzen der Form (w_1 Rw_2 Rw_3 R \ ldots). Beachten Sie, dass umgekehrt fundierte Frames auch irreflexiv sind, denn wenn (wRw), führt dies zu einer unendlichen aufsteigenden Sequenz (wRwRwR \ ldots).

Das obige Korrespondenzergebnis zeigt sofort, dass GL in Bezug auf die Klasse möglicher Weltenmodelle auf transitiven, umgekehrt fundierten Frames modal einwandfrei ist, da alle Axiome und Regeln von GL für solche Modelle gültig sind. Die Frage ist, ob die Vollständigkeit auch gilt: Zum Beispiel ist die Formel (Box A \ rightarrow \ Box \ Box A), die für alle transitiven Frames gültig ist, tatsächlich im GL nachweisbar, wie in Abschnitt 1 erwähnt Ist jede Formel, die für alle transitiven, umgekehrt fundierten Frames gültig ist, auch im GL nachweisbar?

3.2 Modale Vollständigkeit

K. Segerberg war sich der arithmetischen Bedeutung des GL nicht bewusst und bewies 1971, dass der GL in Bezug auf transitive, umgekehrt fundierte Frames tatsächlich vollständig ist. Auch D. de Jongh und S. Kripke haben dieses Ergebnis unabhängig voneinander bewiesen. Segerberg zeigte, dass der GL auch in Bezug auf die eingeschränktere Klasse endlicher transitiver irreflexiver Bäume vollständig ist, was sich später als sehr nützlich für Solovays Beweis des arithmetischen Vollständigkeitssatzes herausstellte (siehe Abschnitt 4).

Die Theoreme der modalen Solidität und Vollständigkeit führen sofort zu einem Entscheidungsverfahren, um zu prüfen, ob eine Modalformel (A) vorliegt, ob (A) aus dem GL folgt oder nicht, indem in der Tiefe zuerst durch irreflexive transitive Bäume begrenzter Tiefe gesucht wird. Wenn man das Verfahren etwas genauer betrachtet, kann gezeigt werden, dass GL in der rechnerischen Komplexitätsklasse PSPACE wie die bekannten Modallogiken K, T und S4 entscheidbar ist. Dies bedeutet, dass es eine Turing-Maschine gibt, die mit einer Formel (A) als Eingabe antwortet, ob (A) aus dem GL folgt oder nicht; Die Größe des Speichers, den die Turing-Maschine für ihre Berechnung benötigt, ist nur ein Polynom in der Länge von (A). Man kann zeigen, dass das Entscheidungsproblem für GL (wie auch die Entscheidungsprobleme für K, T und S4) PSPACE-vollständig ist,in dem Sinne, dass alle anderen Probleme in PSPACE nicht schwieriger sind als zu entscheiden, ob eine gegebene Formel ein Satz von GL ist. (Siehe Goré und Kelly (2007) für die Beschreibung eines automatisierten Theorembeweisers für GL.)

Um die Komplexität genauer zu betrachten, ist die Klasse P von Funktionen, die in einem Zeitpolynom in der Länge der Eingabe berechenbar ist, in PSPACE enthalten, das wiederum in der Klasse EXPTIME von Funktionen enthalten ist, die in exponentieller Zeit berechenbar sind (siehe die Berechenbarkeit und Komplexität des Eintrags). Es bleibt ein berühmtes offenes Problem, ob diese beiden Einschlüsse streng sind, obwohl viele Komplexitätstheoretiker glauben, dass sie es sind. Einige andere bekannte modale Logiken, wie die epistemische Logik mit allgemeinem Wissen, sind in EXPTIME entscheidbar, daher können sie abhängig von den offenen Problemen komplexer sein als GL.

3.3 Mangel an vollständiger Vollständigkeit

Viele bekannte Modallogiken (S) sind nicht nur in Bezug auf eine geeignete Klasse von Frames vollständig, sondern sogar stark vollständig. Um die starke Vollständigkeit zu erklären, benötigen wir den Begriff der Ableitbarkeit aus einer Reihe von Annahmen. Eine Formel (A) kann aus dem Satz von Annahmen (Gamma) in einer Modallogik (S) abgeleitet werden, die als (Gamma \ vdash A) geschrieben ist, wenn (A) in ist (Gamma) oder (A) folgt aus Formeln in (Gamma) und Axiomen von (S) durch Anwendung von Modus Ponens und der Generalisierungsregel. Hier kann die Generalisierungsregel nur auf Ableitungen ohne Annahmen angewendet werden (siehe Hakli und Negri 2010).

Nun ist eine modale Logik (S) stark vollständig, wenn für alle (endlichen oder unendlichen) Mengen (Gamma) und alle Formeln (A) gilt:

Wenn in geeigneten (S) - Frames (A) in allen Welten wahr ist, in denen alle Formeln von (Gamma) wahr sind, dann (Gamma \ vdash A) in der Logik (S).

Diese Bedingung gilt für Systeme wie K, M, K4, S4 und S5. Wenn auf endliche Mengen (Gamma) beschränkt, entspricht die obige Bedingung der Vollständigkeit.

Eine starke Vollständigkeit gilt jedoch nicht für die Beweisbarkeitslogik, da die semantische Kompaktheit versagt. Semantische Kompaktheit ist die Eigenschaft, dass für jede unendliche Menge (Gamma) von Formeln, Wenn jede endliche Teilmenge (Delta) von (Gamma) ein Modell in einem geeigneten (S) - Frame hat, dann hat (Gamma) auch ein Modell in einem geeigneten (S) -Rahmen.

Nehmen Sie als Gegenbeispiel den unendlichen Satz von Formeln

) Gamma = { Diamond p_0, \ Box (p_0 \ rightarrow \ Diamond p_1), \ Box (p_1 \ rightarrow \ Diamond p_2), \ Box (p_2 \ rightarrow \ Diamond p_3), \ ldots, \ Box (p_n \ rightarrow \ Diamond p_ {n + 1}), \ ldots })

Dann kann man für jede endliche Teilmenge (Delta) von (Gamma) ein Modell auf einem transitiven, umgekehrt fundierten Rahmen und einer Welt im Modell konstruieren, in der alle Formeln von (Delta) sind wahr. Durch die modale Solidität beweist GL also nicht (bot) von (Delta) für ein endliches (Delta \ subseteq \ Gamma), und ein fortiori GL beweist nicht (bot) von (Gamma), da jeder GL-Beweis endlich ist. Andererseits ist leicht zu erkennen, dass es kein Modell auf einem transitiven, umgekehrt fundierten Rahmen gibt, in dem in jeder Welt alle Formeln von (Gamma) gelten. Somit folgt (bot) semantisch aus (Gamma), ist jedoch im GL nicht nachweisbar, was der Bedingung einer starken Vollständigkeit widerspricht.

3.4 Topologische Semantik für die Beweisbarkeitslogik

Als Alternative zur Semantik möglicher Welten kann vielen modalen Logiken eine topologische Semantik gegeben werden. Sätze können eindeutig als Teilmengen eines topologischen Raums interpretiert werden. Es ist auch leicht zu erkennen, dass der Satzkonnektiv (wedge) der satztheoretischen Operation (cap) entspricht, während (vee) (cup), (neg) entspricht dem satztheoretischen Komplement und (rightarrow) entspricht (subseteq). Modallogiken, die das Reflexionsaxiom (Box A \ rightarrow A) enthalten, werden auch von den Modaloperatoren besonders natürlich interpretiert. Für diese Logik entspricht (Diamond) dem Verschlussoperator in einem topologischen Raum, während (Box) dem Innenraum entspricht. Um zu sehen, warum diese Interpretationen angemessen sind,Beachten Sie, dass das Reflexionsaxiom der Tatsache entspricht, dass jeder Satz in seinem Verschluss enthalten ist und jeder Satz sein Inneres enthält.

Die Beweisbarkeitslogik beweist jedoch keine Reflexion, da die Instanziierung (Box \ bot \ rightarrow \ bot) der Reflexion zu einem Widerspruch zum Axiom (GL) führen würde.

Die Bereitstellungslogik erfordert daher einen anderen Ansatz. Basierend auf einem Vorschlag von J. McKinsey und A. Tarski (1944) untersuchte L. Esakia (1981, 2003) die Interpretation von (Diamond) als abgeleitetem Mengenoperator (d), der eine Menge abbildet (B) auf die Menge seiner Grenzpunkte (d (B)). Um die Konsequenzen dieser Interpretation von (Diamond) zu erklären, benötigen wir zwei weitere Definitionen, nämlich der Konzepte, die an sich dicht und verstreut sind. Eine Teilmenge (B) eines topologischen Raums wird als an sich dicht bezeichnet, wenn (B \ subseteq d (B)). Ein topologischer Raum wird als gestreut bezeichnet, wenn er keine nicht leere Teilmenge enthält, die an sich dicht ist. Die Ordnungszahlen in ihrer Intervalltopologie bilden Beispiele für verstreute Räume. Esakia (1981) erwies sich als wichtige Entsprechung: Er zeigte, dass ein topologischer Raum das Axiom GL genau dann erfüllt, wenn der Raum verstreut ist. Diese Entsprechung führte bald zu dem von Abashidze (1985) und Blass (1990) unabhängig gefundenen Ergebnis, dass die Beweisbarkeitslogik in Bezug auf jede Ordnungszahl (ge \ omega ^ \ omega) vollständig ist.

In den letzten Jahren hat die topologische Semantik für die Beweisbarkeitslogik eine echte Wiederbelebung erfahren, insbesondere in der Untersuchung der bimodalen Beweisbarkeitslogik GLB von Japaridze, einer Erweiterung von GL (Japaridze 1986). Die Logik GLB erweist sich hinsichtlich ihrer möglichen Weltsemantik als modal unvollständig, in dem Sinne, dass sie keiner Klasse von Rahmen entspricht. Dieses Merkmal stellt den bimodalen GLB in einen scharfen Kontrast zum unimodalen GL, der der Klasse der endlichen transitiven irreflexiven Bäume entspricht, wie oben erwähnt. Beklemishev et al. (2009) haben gezeigt, dass GLB jedoch hinsichtlich seiner topologischen Semantik vollständig ist (siehe auch Beklemishev 2009, Icard 2011). Ein faszinierender Nachhall von Esakias Korrespondenz zwischen GL und verstreuten topologischen Räumen findet sich sogar in neueren topologischen Studien zur räumlichen und epistemischen Logik (siehe Aiello et al.2007). (Weitere Informationen zu GLB finden Sie in Abschnitt 5.4.)

4. Provabilitätslogik und Peano-Arithmetik

Von der Formulierung des GL an fragten sich die Forscher, ob es für formale Theorien wie Peano Arithmetic (PA) angemessen ist: Beweist der GL alles über den Begriff der Beweisbarkeit, der in einer aussagekräftigen Modalsprache ausgedrückt und in Peano Arithmetic bewiesen werden kann, oder Sollten dem GL weitere Grundsätze hinzugefügt werden? Um diesen Begriff der Angemessenheit genauer zu machen, definieren wir eine Realisierung (manchmal als Übersetzung oder Interpretation bezeichnet) als eine Funktion f, die jedem Satzatom der Modallogik einen Satz der Arithmetik zuweist, wobei

• (f (bot) = \ bot;)
• (f) respektiert die logischen Verknüpfungen, zum Beispiel (f (B \ rechter Pfeil C) = (f (B) rechter Pfeil f (C));) und
• (Box) wird als Beweisprädikat (Prov) übersetzt, also (f (Box B) = \ Prov (ulcorner f (B) urcorner).)

4.1 Arithmetische Solidität

Es war bereits in den frühen 1970er Jahren klar, dass der GL in Bezug auf PA formal arithmetisch einwandfrei ist:

) text {If} GL \ vdash A, \ text {dann für alle Realisierungen} f, \ PA \ vdash f (A).)

Um einen Eindruck von der Metamathematik zu bekommen, skizzieren wir den Schallschutz.

Beweisskizze der arithmetischen Solidität. PA beweist in der Tat die Verwirklichung von Aussagen-Tautologien, und die Beweisbarkeit des Verteilungsaxioms von GL übersetzt sich in

) PA \ vdash \ Prov (ulcorner A \ rightarrow B \ urcorner) rightarrow (Prov (ulcorner A \ urcorner) rightarrow \ Prov (ulcorner B \ urcorner)))

für alle Formeln A und B, die nur Löbs zweite Ableitbarkeitsbedingung sind (siehe Abschnitt 1). Darüber hinaus befolgt PA den Modus Ponens sowie die Übersetzung der Generalisierungsregel:

) text {If} PA \ vdash A, \ text {then} PA \ vdash \ Prov (ulcorner A \ urcorner),)

Dies ist nur Löbs erste Ableitbarkeitsbedingung. Schließlich ist die Übersetzung des Hauptaxioms (GL) in PA tatsächlich nachweisbar:

) PA \ vdash \ Prov (ulcorner \ Prov (ulcorner A \ urcorner) rightarrow A \ urcorner) rightarrow \ Prov (ulcorner A \ urcorner).)

Dies ist genau die formalisierte Version des in Abschnitt 1 erwähnten Satzes von Löb.

Lassen Sie uns eine Skizze des Beweises von Löbs Theorem selbst aus seinen Ableitbarkeitsbedingungen geben (der Beweis der formalisierten Version ist ähnlich). Der Beweis basiert auf Gödels Diagonalisierungs-Lemma, das besagt, dass es für jede arithmetische Formel (C (x)) eine arithmetische Formel (B) gibt, so dass

) PA \ vdash B \ leftrightarrow C (ulcorner B \ urcorner).)

In Worten, die Formel (B) sagt "Ich habe Eigenschaft (C)."

Beweis des Satzes von Löb:. Angenommen, (PA \ vdash \ Prov (ulcorner A \ urcorner) rightarrow A); wir müssen zeigen, dass (PA \ vdash A). Durch das Diagonalisierungs-Lemma gibt es eine Formel (B), so dass

) PA \ vdash B \ leftrightarrow (Prov (ulcorner B \ urcorner) rightarrow A).)

Daraus folgt aus Löbs ersten und zweiten Ableitbarkeitsbedingungen sowie einigen Aussagen, dass

) PA \ vdash \ Prov (ulcorner B \ urcorner) leftrightarrow \ Prov (ulcorner \ Prov (ulcorner B \ urcorner) rightarrow A \ urcorner).)

Also wieder durch Löbs zweite Bedingung,) PA \ vdash \ Prov (ulcorner B \ urcorner) rightarrow (Prov (ulcorner \ Prov (ulcorner B \ urcorner) urcorner) rightarrow \ Prov (ulcorner A \ urcorner)).)

Auf der anderen Seite gibt Löbs dritte Bedingung

) PA \ vdash \ Prov (ulcorner B \ urcorner) rightarrow \ Prov (ulcorner \ Prov (ulcorner B \ urcorner) urcorner),)

so

) PA \ vdash \ Prov (ulcorner B \ urcorner) rightarrow \ Prov (ulcorner A \ urcorner).)

Zusammen mit der Annahme, dass (PA \ vdash \ Prov (ulcorner A \ urcorner) rightarrow A) dies ergibt

) PA \ vdash \ Prov (ulcorner B \ urcorner) rightarrow A.)

Schließlich impliziert die durch das Diagonalisierungs-Lemma erzeugte Gleichung, dass (PA \ vdash B), also (PA \ vdash \ Prov (ulcorner B \ urcorner)), also

) PA \ vdash A,)

wie gewünscht.

Beachten Sie, dass das Ersetzen von (bot) durch (A) in Löbs Theorem ergibt, dass (PA \ vdash \ neg \, \ Prov (ulcorner \ bot \ urcorner)) (PA \ impliziert) vdash \ bot), was nur das Gegenteil von Gödels zweitem Unvollständigkeitssatz ist.

4.2 Arithmetische Vollständigkeit

Das wegweisende Ergebnis der Beweisbarkeitslogik ist der arithmetische Vollständigkeitssatz von R. Solovay von 1976, der zeigt, dass der GL tatsächlich für die Peano-Arithmetik angemessen ist:

) GL \ vdash A \ text {genau dann, wenn für alle Realisierungen} f, \ PA \ vdash f (A).)

Dieser Satz besagt im Wesentlichen, dass die modale Logik GL alles erfasst, was Peano Arithmetic in modalen Begriffen wahrheitsgemäß über sein eigenes Beweisbarkeitsprädikat sagen kann. Die Richtung von links nach rechts, die arithmetische Festigkeit von GL, wurde oben diskutiert. Solovay machte sich daran, die andere, viel schwierigere Richtung durch Kontraposition zu beweisen. Sein Beweis basiert auf komplizierten selbstreferenziellen Techniken, und hier kann nur ein kleiner Einblick gegeben werden.

Der modale Vollständigkeitssatz von Segerberg war ein wichtiger erster Schritt in Solovays Beweis der arithmetischen Vollständigkeit von GL in Bezug auf Peano-Arithmetik. Angenommen, GL beweist nicht die Modalformel (A). Dann gibt es der Modalität halber einen endlichen transitiven irreflexiven Baum, so dass (A) an der Wurzel dieses Baumes falsch ist. Jetzt entwickelte Solovay einen genialen Weg, um einen solchen endlichen Baum in der Sprache der Peano-Arithmetik zu simulieren. So fand er eine Erkenntnis (f) von Modalformeln zu arithmetischen Sätzen, so dass die Peano-Arithmetik (f (A)) nicht beweist.

Solovays Vollständigkeitssatz bietet eine alternative Möglichkeit, viele arithmetische Sätze zu konstruieren, die in der Peano-Arithmetik nicht beweisbar sind. Zum Beispiel ist es einfach, ein mögliches Weltenmodell zu erstellen, um zu zeigen, dass GL nicht (Box p \ vee \ Box \ neg \, p) beweist, so dass nach Solovays Theorem ein arithmetischer Satz (f (p)) so, dass Peano Arithmetic nicht beweist (Prov (ulcorner f (p) urcorner) vee \ Prov (ulcorner \ neg \, f (p) urcorner)). Dies impliziert insbesondere, dass in der Peano-Arithmetik weder (f (p)) noch (neg \, f (p)) nachweisbar ist; Nehmen wir im Gegenteil an, dass (PA \ vdash f (p)) dann nach Löbs erster Bedingung und Satzlogik (PA \ vdash \ Prov (ulcorner f (p) urcorner) vee \ Prov (ulcorner \ neg \, f (p) urcorner)), was zu einem Widerspruch führt, und ähnlich, wenn man annimmt, dass (PA \ vdash \ neg \, f (p)).

Solovays Theorem ist so bedeutsam, weil es zeigt, dass ein interessantes Fragment einer unentscheidbaren formalen Theorie wie der Peano-Arithmetik - nämlich das, was die Arithmetik aussagekräftig über ihr eigenes Beweisbarkeitsprädikat ausdrücken kann - mit Hilfe einer entscheidbaren Modallogik, GL, untersucht werden kann eine übersichtliche mögliche Weltsemantik.

5. Der Umfang der Beweisbarkeitslogik

In diesem Abschnitt werden einige aktuelle Trends in der Forschung zur Beweisbarkeitslogik erörtert. Ein wichtiger Aspekt betrifft die Grenzen des Geltungsbereichs des GL, wobei die Hauptfrage lautet, für welche formalen Theorien außer der Peano-Arithmetik der GL die geeignete Aussagenprüfbarkeitslogik ist. Als nächstes diskutieren wir einige Verallgemeinerungen der Aussagenprüfbarkeitslogik in ausdrucksstärkeren Modalsprachen.

5.1 Grenzen

In den letzten Jahren haben Logiker viele andere Arithmetiksysteme untersucht, die schwächer sind als die Peano-Arithmetik. Oft ließen sich diese Logiker von Berechenbarkeitsproblemen inspirieren, beispielsweise von der Untersuchung von Funktionen, die in Polynomzeit berechenbar sind. Sie haben die Frage teilweise beantwortet: "Für welche arithmetischen Theorien gilt Solovays arithmetischer Vollständigkeitssatz (in Bezug auf das entsprechende Beweisbarkeitsprädikat) noch?" Um diese Frage zu diskutieren, sind zwei Konzepte erforderlich. (Delta_0) - Formeln sind arithmetische Formeln, bei denen beispielsweise alle Quantifizierer durch einen Term begrenzt sind

) für alle y \ le \ bs \ bs 0 \: \ für alle z \ le y \: \ für alle x \ le y + z \: (x + y \ le (y + (y + z))),)

Dabei ist (bs) der Nachfolgeoperator ("(+ 1)"). Die arithmetische Theorie (I \ Delta_0) (wobei I für "Induktion" steht) ähnelt der Peano-Arithmetik, außer dass sie weniger Induktion zulässt: das Induktionsschema

[A (0) Keil \ für alle x \, (A (x) rechter Pfeil A (bs x)) rechter Pfeil \ für alle x \, A (x))

ist auf (Delta_0) - Formeln (A) beschränkt.

Wie De Jongh und andere (1991) betonten, gilt die arithmetische Vollständigkeit sicherlich für Theorien (T), die die folgenden zwei Bedingungen erfüllen:

1. (T) beweist die Induktion für (Delta_0) - Formeln, und (T) beweist EXP, die Formel, die ausdrückt, dass für alle (x) seine Potenz (2 ^ x) existiert. In mehr Standardnotation: (T) erweitert (I \ Delta_0) + EXP;
2. (T) beweist keine falschen Sätze der Form (existiert x \, A (x)) mit (A (x)) einer (Delta_0) - Formel.

Für solche Theorien gilt die arithmetische Solidität und Vollständigkeit des GL, vorausgesetzt, (Box) bedeutet (Prov_T), ein natürliches Beweisbarkeitsprädikat in Bezug auf eine ausreichend einfache Axiomatisierung von (T). Also für Modalsätze (A):

) GL \ vdash A \ text {genau dann, wenn für alle Realisierungen} f, T \ vdash f (A).)

Es ist noch nicht klar, ob Bedingung 1 eine Untergrenze für den Umfang der Beweisbarkeitslogik vorsieht. Zum Beispiel ist es immer noch eine offene Frage, ob GL die Beweisbarkeitslogik von (I \ Delta_0 + \ Omega_1) ist, eine Theorie, die etwas schwächer ist als (I \ Delta_0) + EXP in diesem (Omega_1) ist das Axiom, das behauptet, dass für alle (x) seine Kraft (x ^ { log (x)}) existiert. Die Provabilitätslogik GL ist in Bezug auf (I \ Delta_0 + \ Omega_1) arithmetisch korrekt, jedoch mit Ausnahme einiger Teilergebnisse von Berarducci und Verbrugge (1993), die arithmetische Realisierungen bereitstellen, die mit (I \ Delta_0 + \ Omega_1) für eine Einschränkung übereinstimmen Klasse von Sätzen im Einklang mit GL, bleibt die Frage offen. Ihre Antwort kann von offenen Problemen in der rechnerischen Komplexitätstheorie abhängen.

Das obige Ergebnis von De Jongh et al. zeigt ein starkes Merkmal der Beweisbarkeitslogik: Für viele verschiedene arithmetische Theorien erfasst der GL genau das, was diese Theorien über ihre eigenen Beweisbarkeitsprädikate sagen. Gleichzeitig ist dies eine Schwäche. Zum Beispiel weist die Logik der Aussagenprüfbarkeit nicht auf Unterschiede zwischen jenen Theorien hin, die endlich axiomatisierbar sind, und solchen, die es nicht sind.

5.2 Interpretierbarkeitslogik

Um in einer modalen Sprache über wichtige Unterscheidungen zwischen Theorien sprechen zu können, haben Forscher die Beweisbarkeitslogik auf viele verschiedene Arten erweitert. Lassen Sie uns einige erwähnen. Eine Erweiterung besteht darin, eine binäre Modalität (interpretiert) hinzuzufügen, wobei für eine gegebene arithmetische Theorie (T) der Modalsatz (A \ interpretiert B) für "(T + B " stehen soll) ist interpretierbar in (T + A)”(Švejdar, 1983). De Jongh und Veltman (1990) untersuchten die modale Semantik für verschiedene Interpretierbarkeitslogiken, während De Jongh und Visser (1991) die explizite Fixpunkteigenschaft für die wichtigsten bewiesen. Visser charakterisierte die Interpretierbarkeitslogik der gängigsten endlich axiomatisierten Theorien, und Berarducci und Shavrukov charakterisierten unabhängig voneinander die für PA, die nicht endlich axiomatisierbar ist. Es scheint, dass in der Tat,Die Interpretierbarkeitslogik endlich axiomatisierbarer Theorien unterscheidet sich von der Interpretierbarkeitslogik der Peano-Arithmetik (siehe Montagna 1987; Visser 1990, 1998; Berarducci 1990, Shavrukov 1988; Joosten und Visser 2000).

5.3 Aussagenquantifizierer

Eine andere Möglichkeit, den Rahmen der Aussagenprüfbarkeitslogik zu erweitern, besteht darin, Satzquantifizierer hinzuzufügen, damit man Prinzipien wie die von Goldfarb ausdrücken kann:

) forall p \, \ forall q \, \ existiert r \: \ Box ((Box p \ vee \ Box q) leftrightarrow \ Box r),)

zu sagen, dass es für zwei beliebige Sätze einen dritten Satz gibt, der genau dann beweisbar ist, wenn einer der ersten beiden Sätze beweisbar ist. Dieses Prinzip ist in der Peano-Arithmetik nachweisbar (siehe z. B. Artemov und Beklemishev 1993). Die Menge der Sätze von GL mit Aussagenquantifizierern, die arithmetisch gültig ist, erweist sich als unentscheidbar (Shavrukov 1997).

5.4 Japaridzes bimodale und polymodale Beweisbarkeitslogik

Japaridzes (1988) bimodale Logik GLB hat zwei (Box) -ähnliche Beweisbarkeitsoperatoren, die mit ([0]) und ([1]) bezeichnet werden, mit ihren dualen (Diamond) -ähnlichen Operatoren (langle 0 \ rangle) bzw. (langle 1 \ rangle). In Japaridzes Interpretation kann man sich ([0]) als das Standard-Beweisbarkeitsprädikat in der Peano-Arithmetik vorstellen. Andererseits entspricht ([1]) einem stärkeren Beweisbarkeitsprädikat, nämlich (omega) - Beweisbarkeit.

Definieren wir die Konzepte, die erforderlich sind, um diese beabsichtigte Interpretation von GLB zu verstehen. Eine arithmetische Theorie (T) ist definiert als (omega) - genau dann konsistent, wenn für alle Formeln A mit der freien Variablen (x), (T \ vdash \ neg \, A (I_n)) für alle (n) impliziert, dass (T \ not \ vdash \ existiert x \, A (x)); hier ist (I_n) die Ziffer von (n), dh der Ausdruck (bs \ bs \ ldots \ bs 0) mit (n) Vorkommen des Nachfolgeoperators (bs). Peano Arithmetic (PA) ist das bekannteste Beispiel für eine (omega) - konsistente Theorie (siehe auch Gödels Unvollständigkeitssätze). Nun sei PA (^ +) die arithmetische Theorie, deren Axiome die von PA zusammen mit allen Sätzen (forall x \, \ neg \, A (x)) sind, so dass für jedes (n), PA (vdash \ neg \, A (I_n)). Jetzt (omega) - Beweisbarkeit ist einfach Beweisbarkeit in PA (^ +),es ist also das Dual von (omega) - Konsistenz.

Japaridzes bimodale Beweisbarkeitslogik GLB kann durch die Axiome und Regeln des GL (siehe Abschnitt 2) axiomatisiert werden, die separat für [0] und [1] formuliert sind. Darüber hinaus hat GLB zwei gemischte Axiome:) tag {Monotonie} [0] A \ rightarrow [1] A)) tag {(Pi ^ 0_1) - Vollständigkeit} langle 0 \ rangle A \ rightarrow [1] langle 0 \ rangle A) Japaridzes Logik ist entscheidbar und hat eine vernünftige Kripke-Semantik. Sie ist arithmetisch fundiert und vollständig in Bezug auf Peano Arithmetic (Japaridze 1988, Boolos 1993).

Ein polymodales Analogon von Japaridzes GLB namens GLP hat in den letzten Jahren viel Aufmerksamkeit erhalten. GLP hat unendlich viele (Box) - ähnliche Beweisbarkeitsoperatoren, die durch Boxen ([n]) für jede natürliche Zahl (n) bezeichnet werden, mit ihren doppelten (Diamond) - ähnlichen Operatoren (langle n \ rangle). Wieder kann man sich vorstellen, dass ([0]) für das Standard-Beweisbarkeitsprädikat in Peano Arithmetic steht, (langle 1 \ rangle) für (omega) - Beweisbarkeit usw. GLP wurde ausgehend von den Axiomen und Regeln des GL (siehe Abschnitt 2) axiomatisiert, die für jedes ([n]) separat formuliert wurden. Darüber hinaus hat GLP drei gemischte Axiomschemata, nämlich wie von Beklemishev (2010) formuliert: [m] A \ rightarrow [n] A, \ mbox {für} m \ leq n)) langle k \ rangle A \ rightarrow [n] langle k \ rangle A, \ mbox {für} k \ lt n) [m] A \ rightarrow [n] [m] A, \ mbox {für} m \ leq n)

GLP wurde kürzlich mit einer Kripke-Semantik ausgestattet, in Bezug auf die es vollständig ist, und es wurde auch gezeigt, dass es in Bezug auf Peano-Arithmetik arithmetisch vollständig ist (siehe Beklemishev 2010a, 2011a). Genau wie bei GL ist das Entscheidungsproblem für GLP PSPACE-vollständig (Shapirovsky 2008), während sein geschlossenes Fragment polynomial zeitlich entscheidbar ist (Pakhomov 2014).

In den letzten Jahren wurde eine Reihe von Ergebnissen über die polymodale Logik GLP starker Prädizierbarkeitsprädikate nachgewiesen. Hier folgen einige besonders fruchtbare Themen:

• das geschlossene Fragment von GLP (siehe Ignatiev 1993; Beklemishev, Joosten und Vervoort 2005);
• GLP und beweistheoretische Ordnungszahlen (Beklemishev 2004);
• Interpolationssätze für GLP (siehe Beklemishev 2010b, Shamkanov 2011);
• Die Beziehung zwischen topologischer Semantik und Mengenlehre, unter anderem insbesondere große Kardinalaxiome und stationäre Reflexion (siehe Beklemishev 2011b; Beklemishev und Gabelaia 2013, 2014; Fernández-Duque 2014).

5.5 Prädikatenprüfbarkeitslogik

Schließlich kann man natürlich die Prädikaten-Beweisbarkeitslogik studieren. Die Sprache ist die der Prädikatenlogik ohne Funktionssymbole zusammen mit dem Operator (Box). Hier wird die Situation viel komplexer als im Fall der Aussagenprüfbarkeitslogik. Zunächst hat die einfach quantifizierte Version von GL nicht die Festkomma-Eigenschaft, ist in Bezug auf keine Klasse von Kripke-Frames vollständig und in Bezug auf Peano Arithmetic (Montagna, 1984) nicht arithmetisch vollständig. Dann stellt sich die Frage: Gibt es eine gut axiomatisierte Prädikaten-Beweisbarkeitslogik, die angemessen ist und genau die gültigen Prinzipien der Beweisbarkeit beweist? Die Antwort ist leider ein klares Nein:Vardanyan (1986) hat auf der Grundlage von Ideen von Artemov (1985a) bewiesen, dass die Menge der Sätze der Prädikatenprüfbarkeitslogik, deren Realisierungen in PA nachweisbar sind, nicht einmal rekursiv aufzählbar ist, sondern (Pi ^ 0_2) - vollständig, es hat also keine vernünftige Axiomatisierung. Visser und De Jonge (2006) zeigten, dass es kein Entkommen aus dem Satz von Vardanyan gibt, indem sie eine Verallgemeinerung beweisen: Für eine breite Palette von arithmetischen Theorien (T) ist die Menge der Sätze der Prädikatenprüfbarkeitslogik, deren Realisierungen alle in \ beweisbar sind (T) stellt sich als (Pi ^ 0_2) heraus - ebenfalls vollständig. Für eine breite Palette von arithmetischen Theorien (T) erweist sich die Menge der Sätze der Prädikatenprüfbarkeitslogik, deren Realisierungen alle in (T) beweisbar sind, ebenfalls als (Pi ^ 0_2) - vollständig. Für eine breite Palette von arithmetischen Theorien (T) erweist sich die Menge der Sätze der Prädikatenprüfbarkeitslogik, deren Realisierungen alle in (T) beweisbar sind, ebenfalls als (Pi ^ 0_2) - vollständig.

5.6 Andere Verallgemeinerungen

In der obigen Diskussion wurden viele andere wichtige Forschungsbereiche zur Beweisbarkeitslogik und ihren Erweiterungen ausgelassen. Der interessierte Leser wird auf folgende Bereiche hingewiesen:

• die Beweisbarkeitslogik der intuitionistischen Arithmetik (siehe Troelstra 1973; Visser 1982, 1999; Iemhoff 2000, 2001, 2003; Visser 2002, 2008);
• Klassifikation der Beweisbarkeitslogik (siehe Visser 1980, Artemov 1985b, Beklemishev 1989, Beklemishev et al. 1999);
• Rosser-Bestellungen und Proof-Beschleunigung (siehe Guaspari und Solovay 1979, Švejdar 1983, Montagna 1992);
• verschiedene Arten von bimodaler Beweisbarkeitslogik mit Beweisbarkeitsoperatoren für verschiedene Theorien (siehe Carlson 1986; Smoryński 1985; Beklemishev 1994, 1996);
• Beweisbarkeitslogiken für Standardprüfbarkeit kombiniert mit ungewöhnlichen Beweisbarkeitsprädikaten, die PA extern aufzählen, wie Fefermans und Parikhs Beweisbarkeitsprädikate und langsame Beweisbarkeitsprädikate (siehe Montagna 1978; Visser 1989; Shavrukov 1994; Lindström 1994, 2006; Henk und Pakhomov 2016 (Andere Internetressourcen));
• die Logik expliziter Beweise (siehe Artemov 1994, 2001; Artemov und Montagna 1994; Artemov und Iemhoff 2007);
• Anwendungen der Beweisbarkeitslogik in der Beweistheorie (siehe Beklemishev 1999, 2004, 2005, 2006);
• positive Beweisbarkeitslogik und Reflexionsrechnung (siehe Beklemishev 2012, 2014; Dashkov 2012);
• Verallgemeinerungen der polymodalen Beweisbarkeitslogik GLP, nämlich Beweisbarkeitslogiken mit unendlich vielen Modalitäten (siehe Beklemishev et al. 2014; Fernández-Duque und Joosten 2013a, 2013b, 2013 (Other Internet Resources), 2014);
• Beziehungen zwischen Beweisbarkeitslogik und (mu) - Kalkül (siehe van Benthem 2006, Visser 2005, Alberucci und Facchini 2009); und
• Beweisbarkeitsalgebren, auch diagonalisierbare Algebren oder Magari-Algebren genannt (siehe Magari 1975a, 1975b; Montagna 1979, 1980a, 1980b; Shavrukov 1993a, 1993b, 1997; Zambella 1994; aktuelle Ergebnisse zu ihren Elementartheorien siehe Pakhomov 2012, 2014 (Other Internet) Ressourcen), 2015 (Andere Internetressourcen)).

Für den Leser, der einen Beitrag zum Bereich der Beweisbarkeitslogik und ihren Verallgemeinerungen leisten möchte, haben Beklemishev und Visser (2006) eine kommentierte Liste faszinierender offener Probleme vorgeschlagen.

6. Philosophische Bedeutung

Obwohl die Aussagenprüfbarkeitslogik eine Modallogik mit einer Art "Notwendigkeits" -Operator ist, widersteht sie Quines (1976) kontroverser Kritik an Modalbegriffen als unverständlich, bereits aufgrund ihrer klaren und eindeutigen arithmetischen Interpretation. Beispielsweise sind im Gegensatz zu vielen anderen Modallogiken Formeln mit verschachtelten Modalitäten wie (Box \ Diamond p \ rightarrow \ Box \ bot) weder problematisch noch gibt es Streitigkeiten darüber, welche Tautologien sein sollten. Tatsächlich verkörpert die Beweisbarkeitslogik alle Desiderata, die Quine (1953) für syntaktische Behandlungen der Modalität darlegte.

Die Hauptpfeile von Quine waren auf die Logik modaler Prädikate gerichtet, insbesondere auf die Konstruktion von Sätzen, die Modaloperatoren im Rahmen von Quantifizierern enthalten („Quantifizieren in“). In der Prädikatenprüfbarkeitslogik, in der sich Quantifizierer über natürliche Zahlen erstrecken, sind sowohl die De-dicto- als auch die de-re-Modalitäten im Gegensatz zu anderen modalen Logiken einfach zu interpretieren (siehe den Hinweis zur De-dicto / de-re-Unterscheidung). Zum Beispiel Formeln wie

) forall x \, \ Box \, \ existiert y \, (y = x))

sind überhaupt nicht problematisch. Wenn die Nummer (n) (x) zugewiesen ist, dann ist (Box \, \ existiert y \, (y = x)) in Bezug auf diese Zuordnung wahr, wenn der Satz (existiert y \, (y = I_n)) ist in der Peano-Arithmetik beweisbar; hier ist (I_n) die Ziffer von (n), dh der Ausdruck (bs \ bs \ ldots \ bs 0) mit (n) Vorkommen des Nachfolgeoperators (bs). Dieser Satz gilt für alle (n) im Standardmodell der natürlichen Zahlen, und (für alle x \, \ Box \, \ existiert y \, (y = x)) ist sogar in der Peano-Arithmetik beweisbar.

Übrigens die Barcan-Formel

) forall x \, \ Box \, A (x) rightarrow \ Box \, \ forall x \, A (x))

gilt nicht für die ganzen Zahlen, geschweige denn beweisbar (nehmen Sie zum Beispiel für (A (x)) die Formel "(x) codiert keinen Beweis von (bot)"). Sein Gegenteil

) Box \, \ forall x \, A (x) rightarrow \ forall x \, \ Box \, A (x))

Andererseits ist in Peano Arithmetic für jede Formel (A) nachweisbar.

Die Provabilitätslogik unterscheidet sich stark von anderen Modallogiken, auch von solchen mit einem scheinbar ähnlichen Zweck. Während zum Beispiel die Beweisbarkeitslogik die Beweisbarkeit in formalen Theorien der Arithmetik erfasst, versucht die epistemische Logik, Wissen zu beschreiben, das als eine Art informelle Beweisbarkeit angesehen werden könnte. In vielen Versionen der epistemischen Logik ist eines der wichtigsten Prinzipien das Wahrheitsaxiom (5):

) mbox {S5} vdash \ Box A \ rightarrow A, (text {wenn man} A kennt, \ text {dann} A \ text {ist wahr}).)

Das analoge Prinzip gilt eindeutig nicht für den GL: Immerhin

) text {if} GL \ vdash \ Box A \ rightarrow A, \ text {then} GL \ vdash A.)

Es erscheint daher falsch, die Stärke beider Begriffe zu vergleichen oder sie in einem modalen System zu kombinieren. Vielleicht ist formale Beweisbarkeit in gewissem Sinne ein stärkerer Begriff als informelle Beweisbarkeit, aber definitiv ist dies weder eine arithmetische Wahrheit oder Gültigkeit, noch ist die andere Richtung. Diskussionen über die Konsequenzen von Gödels Unvollständigkeitssätzen beinhalten manchmal Verwirrung um den Begriff der Beweisbarkeit, was zu Behauptungen führt, dass Menschen formale Systeme schlagen könnten, wenn sie Theoreme „kennen“(siehe Davis (1990, 1993) für eine gute Diskussion solcher Behauptungen).

Alles in allem ist formale Beweisbarkeit ein genau definiertes Konzept, viel mehr als Wahrheit und Wissen. Selbstreferenz im Rahmen der Beweisbarkeit führt also nicht zu semantischen Paradoxien wie dem Lügner. Stattdessen hat es zu einigen der wichtigsten Ergebnisse der Mathematik geführt, wie zum Beispiel zu Gödels Unvollständigkeitssätzen.

Literaturverzeichnis

Allgemeine Hinweise zur Beweisbarkeitslogik

• Artemov, SN, 2006, "Modal Logic in Mathematics", in P. Blackburn et al. (Hrsg.), Handbook of Modal Logic, Amsterdam: Elsevier, S. 927–970.
• Artemov, SN und LD Beklemishev, 2004, „Provability Logic“, in Handbook of Philosophical Logic, 2. Auflage, D. Gabbay und F. Guenthner, Hrsg., Band 13, Dordrecht: Kluwer, S. 229–403.
• Boolos, G., 1979, Die Unbeweisbarkeit der Konsistenz: Ein Essay in Modal Logic, Cambridge: Cambridge University Press.
• –––, 1993, The Logic of Provability, New York und Cambridge: Cambridge University Press.
• de Jongh, DHJ und G. Japaridze, 1998, "The Logic of Provability", im Handbuch der Beweistheorie, Buss, SR (Hrsg.), Amsterdam: Nordholland, S. 475-546.
• Lindström, P., 1996, „Provability Logic-A Short Introduction“, Theoria, 52 (1–2): 19–61.
• Segerberg, K., 1971, Ein Essay in klassischer Modallogik, Uppsala: Filosofiska Föreningen och Filosofiska Institutionen vid Uppsala Universitet.
• Švejdar, V., 2000, „On Provability Logic“, Nordic Journal of Philosophy, 4: 95–116.
• Smoryński, C., 1985, Selbstreferenz und Modallogik, New York: Springer-Verlag.
• Verbrugge, R. 1996, „Provability“in der Encyclopedia of Philosophy (Beilage), DM Borchert (Hrsg.), New York: Simon und Schuster MacMillan, S. 476–478.
• Visser, A., 1998, "Provability Logic", in Routledge Encyclopedia of Philosophy, W. Craig (Hrsg.), London: Routledge, S. 793–797.

Geschichte

• van Benthem, JFAK, 1978, "Four Paradoxes", Journal of Philosophical Logic, 7 (1): 49–72.
• Boolos, G. und G. Sambin, 1991, „Provability: Die Entstehung einer mathematischen Modalität“, Studia Logica, 50 (1): 1–23.
• Gödel, K., 1933, „Eine Interpretation des intuitionistischen Interessenkalküls“, Ergebnisse eines Mathematischen Kolloquiums, 4: 39–40; Übersetzung "Eine Interpretation des intuitionistischen Satzkalküls" in K. Gödel, Gesammelte Werke, S. Feferman et al. (Hrsg.), Oxford und New York: Oxford University Press, Band 1, 1986, S. 300–302.
• –––, 1931, „Über formale unentscheidbare Sätze der Principia Mathematica und Verwandter Systeme I“, Monatshefte für Mathematik und Physik, 38: 173–198.
• Halbach, V. und A. Visser, 2014, „Der Henkin-Satz“, in M. Mazano, I. Sain und E. Alonso (Hrsg.), Das Leben und Werk von Leon Henkin: Essays on His Contributions, Dordrecht: Springer International Publishing, S. 249–263.
• Henkin, L., 1952, "Ein Problem bezüglich der Provabilität", Journal of Symbolic Logic, 17: 160.
• –––., 1954, „Rezension von G. Kreisel: Über ein Problem von Leon Henkin“, Journal of Symbolic Logic, 19 (3): 219–220.
• Hilbert, D. und P. Bernays, 1939, Grundlagen der Mathematik, Band 2, Berlin / Heidelberg / New York: Springer-Verlag.
• Kreisel, G., 1953, „Über ein Problem von Leon Henkin“, Indagationes Mathematicae, 15: 405–406.
• Lewis, CI, 1912, „Implikation und die Algebra der Logik“, Mind, 21: 522–531.
• Löb, MH, 1955, „Lösung eines Problems von Leon Henkin“, Journal of Symbolic Logic, 20: 115–118.
• Macintyre, AJ und H. Simmons, 1973, „Gödels Diagonalisierungstechnik und verwandte Eigenschaften von Theorien“, Colloquium Mathematicum, 28: 165–180.
• Magari, R., 1975a, „Die diagonalisierbaren Algebren“, Bollettino della Unione Mathematica Italiana, 12: 117–125.
• –––, 1975b, „Repräsentations- und Dualitätstheorie für diagonalisierbare Algebren“, Studia Logica, 34 (4): 305–313.
• Smiley, TJ, 1963, „Die logische Grundlage der Ethik“, Acta Philosophica Fennica, 16: 237–246.
• Smoryński, C., 1991, „Die Entwicklung der Selbstreferenz: Löbs Theorem“, in T. Drucker (Hrsg.), Perspektiven zur Geschichte der mathematischen Logik, Basel: Birkhäuser, S. 110–133.

Cut-Elimination für Beweisbarkeitslogik

• Goré, R. und R. Ramanayake, 2008, "Valentinis Cut-Elimination for Provability Logic Resolved", in Advances in Modal Logic, Band 7, C. Areces und R. Goldblatt (Hrsg.), London: College Publications, S. 67 -86.
• Negri, S., 2005, „Proof Analysis in Modal Logic“, Journal of Philosophical Logic, 50: 507–544.
• Negri, S., 2014, „Beweise und Gegenmodelle in der nichtklassischen Logik“, Logica Universalis, 8 (1): 25–60.
• Poggiolesi, F., 2009, „Eine rein syntaktische und schnittfreie sequentielle Berechnung für die modale Logik der Provabilität“, The Review of Symbolic Logic, 2 (4): 593–611.
• Rautenberg, W., 1983, "Modal Tableau Calculi and Interpolation", Journal of Philosophical Logic, 12 (4): 403–423.
• Sambin, G. und S. Valentini, 1982, „The Modal Logic of Provability. The Sequential Approach “, Journal of Philosophical Logic, 11 (3): 311–342.
• Shamkanov, DS, 2011, „Interpolationseigenschaften für Provability Logics GL und GLP“, Proceedings of the Steklov Institute of Mathematics, 274 (1): 303–316.
• –––, 2014, „Circular Proofs for the Gödel-Löb Provability Logic“, Mathematical Notes, 96 (4): 575–585.
• Smoryński, C., 1978, „Beths Theorem und selbstreferenzielle Sätze“, Studies in Logic and the Foundations of Mathematics, 96: 253–261.
• Valentini, S., 1983, „The Modal Logic of Provability: Cut-Elimination“, Journal of Philosophical Logic, 12: 471–476.

Der Fixpunktsatz

• de Jongh, DHJ, und F. Montagna, 1988, „Provable Fixed Points“, Mathematical Logic Quarterly, 34 (3): 229–250.
• Lindström, P., 2006, „Anmerkung zu einigen Fixpunktkonstruktionen in der Provabilitätslogik“, Journal of Philosophical Logic, 35 (3): 225–230.
• Reidhaar-Olson, L., 1990, „Ein neuer Beweis des Fixpunktsatzes der Provabilitätslogik“, Notre Dame Journal of Formal Logic, 31 (1): 37–43.
• Sambin, G., 1976, „Ein effektiver Fixpunktsatz in intuitionistisch diagonalisierbaren Algebren (Die Algebraisierung der Theorien, die Theor ausdrücken, IX)“, Studia Logica 35: 345–361.
• Sambin, G. und S. Valentini, 1982, „The Modal Logic of Provability. The Sequential Approach “, Journal of Philosophical Logic, 11 (3): 311–342.

Mögliche Weltsemantik und topologische Semantik

• Abashidze, M., 1985, „Ordinale Vollständigkeit des Gödel-Löb-Modalsystems“(auf Russisch) in Intensional Logics and the Logical Structure of Theories, Tiflis: Metsniereba, S. 49–73.
• Aiello, M., I. Pratt-Hartmann und J. van Benthem (Hrsg.), 2007, Handbuch der Raumlogik, Berlin: Springer-Verlag.
• Beklemishev, LD 2009, „Ordinale Vollständigkeit der bimodalen Provabilitätslogik GLB“, im Internationalen Tiflis-Symposium für Logik, Sprache und Berechnung, Berlin: Springer-Verlag, S. 1–15.
• Beklemishev, LD, G. Bezhanishvili und T. Icard, 2009, „Über topologische Modelle von GLP“, in R. Schindler (Hrsg.), Wege der Beweistheorie (Ontos Mathematical Logic: Band 2), Frankfurt: Ontos Verlag, S. 133–153.
• Blass, A., 1990, "Infinitary Combinatorics and Modal Logic", Journal of Symbolic Logic, 55 (2): 761–778.
• Esakia, L., 1981, „Diagonale Konstruktionen, Löbs Formel und Cantors verstreute Räume“(in russischer Sprache), in Studies in Logic and Semantics, Z. Mikeladze (Hrsg.), Tiflis: Metsniereba, S. 128–143.
• –––, 2003, „Intuitionistische Logik und Modalität über Topologie“, Annals of Pure and Applied Logic, 127: 155–170.
• Goré, R., 2009, „Machine Checking Proof Theory: Eine Anwendung von Logik auf Logik“, In ICLA '09: Proceedings der 3. indischen Konferenz über Logik und ihre Anwendungen, Berlin: Springer-Verlag, S. 23–35.
• Goré, R. und J. Kelly, 2007, "Automated Proof Search in Gödel-Löb Provability Logic", British Logic Colloquium 2007, verfügbar unter https://www.dcs.bbk.ac.uk/~roman/blc/.
• Hakli, R. und S. Negri, 2012, „Schlägt der Abzugssatz für die Modallogik fehl?“, Synthese 187 (3): 849–867.
• Icard, TF III, 2011, „Eine topologische Untersuchung des geschlossenen Fragments von GLP“, Journal of Logic and Computation, 21 (4): 683–696; Erstveröffentlichung 2009 2009, doi: 10.1093 / logcom / exp043
• Japaridze, GK, 1986, The Modal Logical Means of Investigation of Provability, These in Philosophy (in russischer Sprache), Moskau.
• McKinsey, JCC und A. Tarski, 1944, „Die Algebra der Topologie“, Annals of Mathematics, 45: 141–191.

Provabilität und Peano-Arithmetik

• Davis, M., 1958, Computability and Unsolvability, New York, McGraw-Hill; Nachdruck mit zusätzlichem Anhang, New York, Dover Publications 1983.
• Feferman, S., 1960, „Arithmetisierung der Metamathematik in einem allgemeinen Umfeld“, Fundamenta Mathematicae, 49 (1): 35–92.
• Hájek, P. und P. Pudlák, 1993, Metamathematik der Arithmetik erster Ordnung, Berlin: Springer-Verlag.
• Solovay, RM, 1976, „Provability Interpretations of Modal Logic“, Israel Journal of Mathematics, 25: 287–304.

Der Umfang der Beweisbarkeitslogik: Grenzen

• Berarducci, A. und R. Verbrugge, 1993, „Über die Provabilitätslogik der begrenzten Arithmetik“, Annals of Pure and Applied Logic, 61: 75–93.
• Buss, SR, 1986, Bounded Arithmetic, Neapel: Bibliopolis.
• de Jongh, DHJ, M. Jumelet und F. Montagna, 1991, „Über den Beweis des Satzes von Solovay“, Studia Logica, 50 (1): 51–70.

Interpretierbarkeitslogik

• Berarducci, A., 1990, „Die Interpretierbarkeitslogik der Peano-Arithmetik“, Journal of Symbolic Logic, 55: 1059–1089.
• de Jongh, DHJ, und F. Veltman, 1990, "Provability Logics for Relative Interpretability", in PP Petkov (Hrsg.), Mathematical Logic: Proceedings der Heyting 1988 Summer School in Varna, Bulgarien, Boston: Plenum Press, pp. 31–42.
• de Jongh, DHJ und A. Visser, 1991, „Explizite Fixpunkte in der Interpretierbarkeitslogik“, Studia Logica, 50 (1): 39–49.
• Joosten, JJ, und Visser, A., 2000, „Die Interpretierbarkeitslogik aller vernünftigen arithmetischen Theorien“, Erkenntnis, 53 (1-2): 3–26.
• Montagna, F., 1987, „Provability in Finite Subtheories of PA“, Journal of Symbolic Logic, 52 (2): 494–511.
• Shavrukov, V. Yu., 1988, "Die Logik der relativen Interpretierbarkeit über Peano-Arithmetik", Technischer Bericht Nr. 5, Moskau: Steklov Mathematical Institute (in russischer Sprache).
• Švejdar, V., 1983, „Modal Analysis of Generalized Rosser Sentences“, Journal of Symbolic Logic, 48: 986–999.
• Visser, A., 1990, „Interpretability Logic“, in PP Petkov (Hrsg.), Mathematical Logic: Proceedings der Heyting 1988 Summer School in Varna, Bulgarien, Boston: Plenum Press, S. 175–209.
• –––, 1998, „Ein Überblick über die Interpretierbarkeitslogik“, in M. Kracht et al. (Hrsg.), Advances in Modal Logic (Band 1), Stanford: CSLI Publications, S. 307–359.

Aussagenquantifizierer

• Artemov, SN und LD Beklemishev, 1993, „Über Aussagenquantifizierer in der Provabilitätslogik“, Notre Dame Journal of Formal Logic, 34: 401–419.
• Shavrukov, V. Yu., 1997, „Unentscheidbarkeit in diagonalisierbaren Algebren“, Journal of Symbolic Logic, 62: 79–116.

Japaridzes bimodale und polymodale Beweisbarkeitslogik

• Beklemishev, LD, 2004, „Provabilitätsalgebren und beweistheoretische Ordnungszahlen, I“, Annals of Pure and Applied Logic, 128: 103–123.
• –––, 2010a, „Kripke Semantics for Provability Logic GLP“, Annals of Pure and Applied Logic, 161 (6): 756–774.
• –––, 2010b, „Über die Craig-Interpolation und die Fixpunkteigenschaften von GLP“, in S. Feferman et al. (Hrsg.), Proofs, Categories and Computations (Tributes, 13), London: College Publications, S. 49–60.
• –––, 2011a, „Ein vereinfachter Beweis des arithmetischen Vollständigkeitssatzes für die Provabilitätslogik GLP“, Proceedings Steklov Institute of Mathematics, 274 (1): 25–33.
• –––, 2011b, „Ordinale Vollständigkeit der bimodalen Provabilitätslogik GLB“, in N. Bezhanishvili et al. (Hrsg.), Logik, Sprache und Berechnung, 8. Internationales Tiflis-Symposium TbiLLC 2009 (Lecture Notes in Computer Science: Band 6618), Heidelberg: Springer, S. 1–15.
• Beklemishev, LD und D. Gabelaia, 2013, „Topologische Vollständigkeit der Provability Logic GLP“, Annals of Pure and Applied Logic, 164 (12): 1201–1223.
• –––, 2014, „Topologische Interpretationen der Provabilitätslogik“, in G. Bezhanishvili (Hrsg.), Leo Esakia über Dualität in modaler und intuitionistischer Logik (Herausragende Beiträge zur Logik: Band 4), Heidelberg: Springer, S. 257– 290.
• Beklemishev, LD, J. Joosten und M. Vervoort, 2005, „Eine endgültige Behandlung des geschlossenen Fragments von Japaridzes Provabilitätslogik“, Journal of Logic and Computation, 15 (4): 447–463.
• Fernández-Duque, D. und JJ Joosten, 2014, „Gutordnungen zur transfiniten Japaridze-Algebra“, Logic Journal der IGPL, 22 (6): 933–963.
• Ignatiev, KN, 1993, „Über starke Provizierbarkeitsprädikate und die damit verbundene modale Logik“, Journal of Symbolic Logic, 58: 249–290.
• Japaridze, G., 1988, „The Polymodal Provability Logic“, In Intensional Logics und der logischen Struktur von Theorien: Material aus dem vierten sowjetisch-finnischen Symposium über Logik, Telavi, S. 16–48.
• Pakhomov, FN, 2014, „Über die Komplexität des geschlossenen Fragments von Japaridzes Provabilitätslogik“, Archive for Mathematical Logic, 53 (7-8): 949–967.

Prädikatenprüfbarkeitslogik

• Artemov, SN, 1985a, „Nichtarithmetik der Wahrheit Prädikatlogik der Provabilität“, Doklady Akademii Nauk SSSR, 284: 270–271 (in russischer Sprache); Englische Übersetzung in Sowjetische Mathematik Doklady, 32: 403–405.
• McGee, V. und G. Boolos, 1987, „Der Grad der Sätze von Prädikaten-Provabilitätslogiken, die unter jeder Interpretation wahr sind“, Journal of Symbolic Logic, 52: 165–171.
• Vardanyan, VA, 1986, „Arithmetische Komplexität der Prädikatenlogik der Provabilität und ihrer Fragmente“, Doklady Akademii Nauk SSSR, 288: 11–14 (in russischer Sprache); Englische Übersetzung in Sowjetische Mathematik Doklady, 33: 569–572.
• Visser, A. und M. de Jonge, 2006, „No Escape from Vardanyans Theorem“, Archive of Mathematical Logic, 45 (5): 539–554.

Andere Verallgemeinerungen

• Alberucci, L. und A. Facchini, 2009, „On Modal μ-Calculus and Gödel-Löb Logic“, Studia Logica, 91: 145–169.
• Artemov, SN, 1985b, „On Modal Logics Axiomatizing Provability“, Izvestiya Akadademii Nauk SSSR, Seriya Matematicheskaya, 49 (6): 1123–1154 (in russischer Sprache); Englische Übersetzung in Mathematik der UdSSR - Izvestiya, 27 (3): 402–429.
• –––, 1994, „Logik der Beweise“, Annals of Pure and Applied Logic, 67 (2): 29–59.
• –––, 2001, „Explizite Provabilität und konstruktive Semantik“, Bulletin of Symbolic Logic, 7: 1–36.
• Artemov, SN und R. Iemhoff, 2007, „The Basic Intuitionistic Logic of Proofs“, Journal of Symbolic Logic, 72 (2): 439–451.
• Artemov, SN und F. Montagna, 1994, „Über Theorien erster Ordnung mit dem Operabilitätsoperator“, Journal of Symbolic Logic, 59 (4): 1139–1153.
• Beklemishev, LD, 1989, "Über die Klassifikation der Aussagen-Provabilitätslogik", Izvestiya Akademii Nauk SSSR, Seriya Matematicheskaya. 53 (5): 915–943 (in russischer Sprache); Englische Übersetzung in Mathematik der UdSSR - Izvestiya, 35 (1990) 247–275.
• –––, 1994, „On Bimodal Logics of Provability“, Annals of Pure and Applied Logic, 68: 115–160.
• –––, 1996, „Bimodale Logik zur Erweiterung arithmetischer Theorien“, Journal of Symbolic Logic, 61: 91–124.
• –––, 1999, „Parameterfreie Induktion und nachweislich insgesamt berechenbare Funktionen“, Theoretical Computer Science, 224: 13–33.
• –––, 2005, „Reflexionsprinzipien und Provabilitätsalgebren in der formalen Arithmetik“, Uspekhi Matematicheskikh Nauk, 60 (2): 3–78. (auf Russisch); Englische Übersetzung in: Russian Mathematical Surveys, 60 (2) (2005): 197–268.
• –––, 2006, „The Worm Principle“, in Lecture Notes in Logic 27. Logic Colloquium '02, Z. Chatzidakis, P. Koepke und W. Pohlers (Hrsg.), Natick (MA): AK Peters, pp 75–95.
• –––, 2012, „Kalibrieren der Provabilitätslogik: Von der Modallogik zur Reflexionsrechnung“, in T. Bolander, T. Braüner, S. Ghilardi und L. Moss (Hrsg.), Fortschritte in der Modallogik (Band 9), London: College Publications, S. 89–94.
• –––, 2014, „Positive Provabilitätslogik für einheitliche Reflexionsprinzipien“, Annals of Pure and Applied Logic, 165 (1): 82–105.
• Beklemishev, LD, D. Fernández-Duque und JJ Joosten, 2014, „Zur Bereitstellungslogik mit linear geordneten Modalitäten“, Studia Logica, 102 (3): 541–566.
• Beklemishev, LD, M. Pentus und N. Vereshchagin, 1999, Provability, Complexity, Grammatik, American Mathematical Society Translations (Reihe 2, Band 192).
• Beklemishev, LD und A. Visser, 2006, „Probleme in der Logik der Provabilität“, in DM Gabbay, SS Goncharov und M. Zakharyashev (Hrsg.), Mathematische Probleme aus der angewandten Logik I: Logik für das 21. Jahrhundert (International Mathematical Series), Band 4), New York: Springer, S. 77–136.
• van Benthem, J., 2006, „Modal Frame Correspondences and Fixed-Points“, Studia Logica, 83 (1-3): 133–155.
• Carlson, T., 1986, „Modale Logik mit mehreren Operatoren und Interpretierbarkeitsinterpretationen“, Israel Journal of Mathematics, 54 (1): 14–24.
• Dashkov, EV, 2012, „Über das positive Fragment der polymodalen Provabilitätslogik GLP“, Mathematical Notes, 91 (3): 318–333.
• Fernández-Duque, D., 2014, „The Polytopologies of Transfinite Provability Logic“, Archiv für mathematische Logik, 53 (3-4): 385–431.
• Fernández-Duque, D. und JJ Joosten, 2013a, „Hyperationen, Veblen-Progressionen und transfinite Iteration von Ordnungsfunktionen“, Annals of Pure and Applied Logic 164 (7-8): 785–801, [online verfügbar].
• Fernández-Duque, D. und JJ Joosten, 2013b, „Models of Transfinite Provability Logic“, Journal of Symbolic Logic, 78 (2): 543–561, [online verfügbar].
• Guaspari, D. und RM Solovay, 1979, „Rosser Sentences“, Annals of Mathematical Logic, 16: 81–99.
• Iemhoff, R., 2000, "Eine Modalanalyse einiger Prinzipien der Provabilitätslogik der Heyting-Arithmetik", in Advances in Modal Logic (Band 2), M. Zakharyashev et al. (Hrsg.), Stanford: CSLI Publications, S. 319–354.
• –––, 2001, „Über die zulässigen Regeln der intuitionistischen Aussagenlogik“, Journal of Symbolic Logic, 66: 281–294.
• –––, 2003, „Preservativity Logic: Ein Analogon der Interpretierbarkeitslogik für konstruktive Theorien“, Mathematical Logic Quarterly, 49 (3): 1–21.
• Lindström, P., 1994, "Die modale Logik der Parikh-Provabilität", Filosofiska Meddelanden, Gröna Serien, Göteborg: Göteborgs Universitetet.
• Lindström, P., 2006, „Über Parikh-Provabilität: Eine Übung in modaler Logik“, in H. Lagerlund, S. Lindström und R. Sliwinski (Hrsg.), Modality Matters: 25 Essays zu Ehren von Krister Segerberg, Uppsala: Uppsala Philosophical Studies (Band 53), S. 53–287.
• Montagna, F., 1978, „Zur Algebraisierung eines Feferman-Prädikats“, Studia Logica, 37 (3): 221–236.
• –––, 1979, „Über die diagonalisierbare Algebra der Peano-Arithmetik“, Bollettino della Unione Matematica Italiana, B (5), 16: 795–812.
• –––, 1980a, „Interpretationen der Theorie erster Ordnung diagonalisierbarer Algebren in der Peano-Arithmetik“, Studia Logica, 39: 347–354.
• –––, 1980b, „Unentscheidbarkeit der Theorie diagonalisierbarer Algebren erster Ordnung“, Studia Logica, 39: 355–359.
• –––, 1984, „The Predicate Modal Logic of Provability“, Notre Dame Journal of Formal Logic, 25 (2): 179–189.
• –––, 1992, „Polynomiell und superexponentiell kürzere Beweise in Fragmenten der Arithmetik“, Journal of Symbolic Logic, 57: 844–863.
• Pakhomov, FN, 2012, „Unentscheidbarkeit der Elementartheorie des Halbgitters von GLP-Wörtern“, Sbornik: Mathematics, 203 (8): 1211.
• Shapirovsky, I., 2008, „PSPACE-Entscheidbarkeit von Japaridzes polymodaler Logik“, Advances in Modal Logic, 7: 289–304.
• Shavrukov, V. Yu., 1993a, „Eine Anmerkung zu den diagonalisierbaren Algebren von PA und ZF“, Annals of Pure and Applied Logic, 61: 161–173.
• –––, 1993b, „Subalgebren diagonalisierbarer Algebren arithmetischer Theorien“, Dissertationes Mathematicae, 323.
• –––, 1994, „Ein kluges Kind von Peano“, Notre Dame Journal of Formal Logic, 35 (2): 161–185.
• Troelstra, AS, 1973, Metamathematische Untersuchung intuitionistischer Arithmetik und Analyse, Berlin: Springer-Verlag.
• Visser, A., 1980, Aspekte der Diagonalisierung und Provabilität, Ph. D. Diplomarbeit, Utrecht: Universität Utrecht.
• –––, 1982, „Über das Vollständigkeitsprinzip: Eine Studie zur Beweisbarkeit in Heytings Arithmetik und Erweiterungen“, Annals of Mathematical Logic, 22 (3): 263–295.
• –––, 1989, „Peanos intelligente Kinder: Eine logische Studie zur Provabilitätslogik von Systemen mit integrierter Konsistenz“, Notre Dame Journal of Formal Logic, 30 (2): 161–196.
• –––, 1999, „Rules and Arithmetics“, Notre Dame Journal of Formal Logic, 40 (1): 116–140.
• –––, 2002, „Substitutionen von (Sigma_1) Sätzen: Erkundungen zwischen intuitionistischer Aussagenlogik und intuitionistischer Arithmetik“, Annals of Pure and Applied Logic, 114: 227–271.
• –––, 2005, „Löbs Logik trifft den μ-Kalkül“, in A. Middeldorp, V. van Oostrom, F. van Raamsdonk und R. de Vrijer (Hrsg.), Prozesse, Begriffe und Zyklen: Schritte auf der Straße to Infinity, Berlin: Springer, S. 14–25.
• –––, 2008, „Geschlossene Fragmente der Provabilitätslogik konstruktiver Theorien“, Journal of Symbolic Logic, 73: 1081–1096.
• Zambella, D., 1994, „Shavrukovs Theorem über die Subalgebren diagonalisierbarer Algebren für Theorien, die (I \ Delta_0 + \ exp) enthalten“, Notre Dame Journal of Formal Logic, 35: 147–157.

Philosophische Bedeutung

• Davis, M., 1990, "Is Mathematical Insight Algorithmic?", Kommentar zu Roger Penrose, The Emperors New Mind, Behavioral and Brain Sciences, 13: 659–660.
• –––, 1993, „Wie subtil ist Gödels Theorem?“(Kommentar zu Roger Penrose, Der neue Geist des Kaisers), Behavioral and Brain Sciences, 16: 611–612.
• Egré, P., 2005, „Das Wissensparadoxon im Lichte der Interpretierbarkeit der Modalität der Modallogik“, Journal of Logic, Language and Information, 14 (1): 13–48.
• Kaplan, D. und R. Montague, 1960, „Ein wiedergewonnenes Paradoxon“, Notre Dame Journal of Formal Logic, 1 (3): 79–90.
• Montague, R., 1963, „Syntaktische Behandlungen der Modalität mit Folgerungen aus Reflexionsprinzipien und endlicher Axiomatisierbarkeit“, Acta Philosophica Fennica, 16: 153–67.
• Quine, WV, 1966, „Necessary Truth“, in Quine, WV, Die Wege des Paradoxons und andere Essays, New York: Random House, S. 48–56.
• –––, 1953, „Three Grades of Modal Involvement“, in Proceedings des 11. Internationalen Kongresses für Philosophie, Amsterdam: Nordholland, S. 65-81; Nachdruck in WV Quine, The Ways of Paradox und anderen Essays, New York: Random House, 1966, S. 156–174.

Akademische Werkzeuge

	Wie man diesen Eintrag zitiert.
	Vorschau der PDF-Version dieses Eintrags bei den Freunden der SEP-Gesellschaft.
	Schlagen Sie dieses Eintragsthema im Internet Philosophy Ontology Project (InPhO) nach.
	Erweiterte Bibliographie für diesen Eintrag bei PhilPapers mit Links zu seiner Datenbank.

Andere Internetquellen

Beiträge und Präsentationen

• Fernández-Duque, D. und JJ Joosten, 2013, „Die Omega-Regel-Interpretation der Transfinite Provability Logic“, Online-Manuskript auf arxiv.org.
• Henk, P. und Pakhomov, F., 2016, Manuskript „Langsame und gewöhnliche Bereitstellbarkeit für Peano-Arithmetik“auf arxiv.org.
• Pakhomov, F., 2014, „Über Elementartheorien von GLP-Algebren“, Manuskript auf arxiv.org.
• Pakhomov, F., 2015, „Über Elementartheorien von Ordnungsnotationssystemen basierend auf Reflexionsprinzipien“, Manuskript auf arxiv.org.
• Visser, Albert, Über formale Beweisbarkeit versus menschliche Beweisbarkeit (auf Niederländisch), Online-Manuskript, Universität Utrecht.
• Verbrugge, Rineke, Präsentationsfolien zur Beweisbarkeitslogik, Folien, Universität Groningen

Andere Seiten

• Offene Probleme in der von Lev Beklemishev gepflegten Provability Logic
• Mailingliste Grundlagen der Mathematik, New York University