Japaridzes polymodale Logik

Japaridzes polymodale Logik ( GLP ) ist ein System der Beweisbarkeitslogik mit unendlich vielen Beweisbarkeitsmodalitäten . Dieses System spielte eine wichtige Rolle in einigen Anwendungen von Beweisbarkeitsalgebren in der Beweistheorie und wird seit den späten 1980er Jahren intensiv erforscht. Es ist nach Giorgi Japaridze benannt .

Sprache und Axiomatisierung

Die Sprache der GLP erweitert die Sprache der klassischen Aussagenlogik um die unendliche Reihe $[0],[1],[2],...$ von Notwendigkeitsoperatoren. Ihre dualen Möglichkeitsoperatoren $<0>,<1>,<2>,...$ sind definiert durch $< n > p = \neg[n]\neg p$ .

Die Axiome der GLP sind allesamt klassische Tautologien und alle Formeln einer der folgenden Formen:

$[n](p \to q) \to ([n] p \to [n] q)$
$[n]([n] p \to p) \to [n] p$
$[n] p \to [n +1] p$
$< n > p \to [n +1]< n > p$

Und die Schlussregeln lauten:

Aus $p$ und $p \to q$ folgt $q.$
Aus $p$ schließen wir $[0] p$

Beweisbarkeitssemantik

Betrachten wir eine hinreichend starke Theorie erster Stufe $T,$ $wie$ etwa die Peano-Arithmetik $PA . Definieren$ $wir$ die Reihe $T₀, T₁, T₂, ...$ von Theorien wie folgt:

$T 0$ ist $T$
$T n +1$ ist die Erweiterung von $T$ $$ $n$ durch die zusätzlichen Axiome $\forallxF (x)$ für jede Formel $F (x)$ , sodass $T n$ alle Formeln $F (0), F (1), F (2),... beweist.$

Für jedes $n$ sei $Pr n (x)$ eine natürliche Arithmetisierung des Prädikats $" x$ ist die Gödelzahl eines in $T n beweisbaren Satzes "$ .

Eine Realisierung ist eine Funktion $*$ , die jedes nichtlogische Atom $a$ der Sprache von GLP auf einen Satz $a *$ der Sprache von $T$ abbildet . Sie lässt sich auf alle Formeln der Sprache von GLP erweitern, indem sie festlegt, dass $*$ mit den Booleschen Konnektiven kommutiert und dass $([n] F)*$ $Pr n (' F *')$ ist , wobei $' F *'$ für die Gödelzahl von $F *$ steht .

Ein Satz über die arithmetische Vollständigkeit ^{[ 1 ]} für GLP besagt, dass eine Formel $F$ genau dann in GLP beweisbar ist , wenn für jede Interpretation $*$ der Satz $F * in$ $T$ beweisbar ist .

Das oben beschriebene Verständnis der Reihe $T₀, T₁, T₂, ... von Theorien ist nicht das einzige natürliche Verständnis, das$ die Korrektheit und Vollständigkeit des GLP gewährleistet. Beispielsweise kann jede Theorie $Tₙ$ als um alle wahren $Πₙ$ $- Sätze als zusätzliche Axiome erweiterte Theorie$ $T$ verstanden werden . George Boolos zeigte ^[²^{] , dass das GLP} $auch$ dann korrekt und vollständig bleibt, wenn die Analysis ( Arithmetik zweiter Stufe ) die Rolle der Basistheorie $T$ übernimmt .

Andere Semantik

Es wurde gezeigt ^{[ 1 ]} , dass GLP bezüglich jeder Klasse von Kripke-Rahmen unvollständig ist .

Eine natürliche topologische Semantik der GLP interpretiert Modalitäten als Ableitungsoperatoren eines polytopologischen Raums . Solche Räume werden GLP-Räume genannt, wenn sie alle Axiome der GLP erfüllen. Die GLP ist vollständig bezüglich der Klasse aller GLP-Räume. ^{[ 3 ]}

Rechenkomplexität

Das Problem, ein Theorem der GLP zu sein, ist PSPACE-vollständig . Dasselbe gilt für dasselbe Problem, beschränkt auf variablenfreie Formeln der GLP. ^{[ 4 ]}

Geschichte

GLP, unter dem Namen GP, wurde von Giorgi Japaridze in seiner Dissertation „Modal Logical Means of Investigating Provability“ ( Moskauer Staatliche Universität , 1986) eingeführt und zwei Jahre später veröffentlicht ^{[ 1 ]} . Die Veröffentlichung umfasste (a) den Vollständigkeitssatz für GLP bezüglich seiner Beweisbarkeitsinterpretation (Beklemishev entwickelte später einen einfacheren Beweis desselben Satzes ^{[ 5 ]} ) und (b) einen Beweis, dass keine Kripke-Rahmen für GLP existieren. Beklemishev führte außerdem eine umfassendere Studie zu Kripke-Modellen für GLP durch ^{[ 6 ]} . Topologische Modelle für GLP wurden von Beklemishev, Bezhanishvili, Icard und Gabelaia untersucht ^{[ 3 ,}^{7 ]} . Die Entscheidbarkeit von GLP im Polynomraum wurde von I. Shapirovsky bewiesen ^{[ 8 ]}^, und die PSPACE-Schwere seines variablenfreien Fragments wurde von F. Pakhomov bewiesen. ^{[ 4 ]} Zu den bemerkenswertesten Anwendungen von GLP gehörte seine Verwendung bei der beweistheoretischen Analyse der Peano-Arithmetik , der Ausarbeitung einer kanonischen Methode zur Wiederherstellung der Ordinalnotation bis $ɛ 0$ aus der entsprechenden Algebra und der Konstruktion einfacher kombinatorischer unabhängiger Aussagen (Beklemishev ^{[ 9 ]} ).

Eine umfassende Übersicht über GLP im Kontext von Beweisbarkeitslogiken im Allgemeinen gab George Boolos in seinem Buch „The Logic of Provability“ . ^{[ 10 ]}

Literatur

L. Beklemishev, „Beweisbarkeitsalgebren und beweistheoretische Ordinalzahlen, I“ . Annals of Pure and Applied Logic 128 (2004), S. 103–123.
L. Beklemishev, J. Joosten und M. Vervoort, „Eine finitäre Behandlung des geschlossenen Fragments der Beweisbarkeitslogik von Japaridze“ . Journal of Logic and Computation 15 (2005), Nr. 4, S. 447–463.
L. Beklemishev, „Kripke-Semantik für Beweisbarkeitslogik GLP“ . Annals of Pure and Applied Logic 161, 756–774 (2010).
L. Beklemishev, G. Bezhanishvili und T. Icar, „Über topologische Modelle der GLP“. Beweistheorien, Ontos Mathematische Logik , 2, Hrsg. R. Schindler, Ontos Verlag, Frankfurt, 2010, S. 133–153.
L. Beklemishev, „Über die Craig-Interpolation und die Fixpunkteigenschaften von GLP“. Beweise, Kategorien und Berechnungen . S. Feferman et al. (Hrsg.), College Publications 2010, S. 49–60.
L. Beklemishev, „Ordinale Vollständigkeit der bimodalen Beweisbarkeitslogik GLB“ . Lecture Notes in Computer Science 6618 (2011), S. 1–15.
L. Beklemishev, „Ein vereinfachter Beweis des Satzes über die arithmetische Vollständigkeit für die Beweisbarkeitslogik GLP“ . Proceedings of the Steklov Institute of Mathematics 274 (2011), S. 25–33.
L. Beklemishev und D. Gabelaia, „Topologische Vollständigkeit der Beweisbarkeitslogik GLP“ . Annals of Pure and Applied Logic 164 (2013), S. 1201–1223.
G. Boolos, „Die analytische Vollständigkeit der polymodalen Logiken von Japaridze“ . Annals of Pure and Applied Logic 61 (1993), S. 95–111.
G. Boolos, Die Logik der Beweisbarkeit Cambridge University Press, 1993.
EV Dashkov, „Über das positive Fragment der polymodalen Beweisbarkeitslogik GLP“. Mathematical Notes 2012; 91:318–333.
D. Fernandez-Duque und J. Joosten, „ Wohlordnungen in der transfiniten Japaridze-Algebra “. Logic Journal of the IGPL 22 (2014), S. 933–963. doi : 10.1093/jigpal/jzu018 . arXiv : 1212.3468 .
G. Japaridze, „Die polymodale Logik der Beweisbarkeit“ . Intensionale Logiken und logische Struktur von Theorien . Metsniereba, Tiflis, 1988, S. 16–48 (Russisch).
F. Pakhomov, „Zur Komplexität des geschlossenen Fragments der Beweisbarkeitslogik von Japaridze“ . Archive for Mathematical Logic 53 (2014), S. 949–967.
DS Shamkanov, „Interpolationseigenschaften für Beweisbarkeitslogiken GL und GLP“ . Proceedings of the Steklov Institute of Mathematics 274 (2011), S. 303–316.
I. Shapirovsky, „PSPACE-Entscheidbarkeit der polymodalen Logik von Japaridze“ . Advances in Modal Logic 7 (2008), S. 289–304.

Referenzen

^ ^a ^b ^c G. Japaridze, „Die polymodale Logik der Beweisbarkeit“ . Intensionale Logiken und logische Struktur von Theorien . Metsniereba, Tiflis, 1988, S. 16–48 (Russisch).
^ G. Boolos, „Die analytische Vollständigkeit der polymodalen Logiken von Japaridze“ . Annals of Pure and Applied Logic 61 (1993), S. 95–111.
^ ^a ^b L. Beklemishev und D. Gabelaia, „Topologische Vollständigkeit der Beweisbarkeitslogik GLP“ . Annals of Pure and Applied Logic 164 (2013), S. 1201–1223.
^ ^a ^b F. Pakhomov, „Zur Komplexität des geschlossenen Fragments der Beweisbarkeitslogik von Japaridze“ . Archive for Mathematical Logic 53 (2014), S. 949–967.
^ L. Beklemishev, „Ein vereinfachter Beweis des Satzes von der arithmetischen Vollständigkeit für die Beweisbarkeitslogik GLP“ . Proceedings of the Steklov Institute of Mathematics 274 (2011), S. 25–33.
^ L. Beklemishev, „Kripke-Semantik für Beweisbarkeitslogik GLP“ . Annals of Pure and Applied Logic 161, 756–774 (2010).
^ L. Beklemishev, G. Bezhanishvili und T. Icard, „Über topologische Modelle der GLP“. Wege der Beweistheorie, Ontos Mathematische Logik , 2, Hrsg. R. Schindler, Ontos Verlag, Frankfurt, 2010, S. 133–153.
^ I. Shapirovsky, „PSPACE-Entscheidbarkeit der polymodalen Logik von Japaridze“ . Advances in Modal Logic 7 (2008), S. 289–304.
^ L. Beklemishev, „Beweisbarkeitsalgebren und beweistheoretische Ordinalzahlen, I“ . Annals of Pure and Applied Logic 128 (2004), S. 103–123.
^ G. Boolos, Die Logik der Beweisbarkeit . Cambridge University Press, 1993.

[japaridze1988-1] G. Japaridze, „Die polymodale Logik der Beweisbarkeit“ . Intensionale Logiken und logische Struktur von Theorien . Metsniereba, Tiflis, 1988, S. 16–48 (Russisch).

[2] G. Boolos, „Die analytische Vollständigkeit der polymodalen Logiken von Japaridze“ . Annals of Pure and Applied Logic 61 (1993), S. 95–111.

[beklemishev2013-3] L. Beklemishev und D. Gabelaia, „Topologische Vollständigkeit der Beweisbarkeitslogik GLP“ . Annals of Pure and Applied Logic 164 (2013), S. 1201–1223.

[pakhomov2014-4] F. Pakhomov, „Zur Komplexität des geschlossenen Fragments der Beweisbarkeitslogik von Japaridze“ . Archive for Mathematical Logic 53 (2014), S. 949–967.

[5] L. Beklemishev, „Ein vereinfachter Beweis des Satzes von der arithmetischen Vollständigkeit für die Beweisbarkeitslogik GLP“ . Proceedings of the Steklov Institute of Mathematics 274 (2011), S. 25–33.

[6] L. Beklemishev, „Kripke-Semantik für Beweisbarkeitslogik GLP“ . Annals of Pure and Applied Logic 161, 756–774 (2010).

[7] L. Beklemishev, G. Bezhanishvili und T. Icard, „Über topologische Modelle der GLP“. Wege der Beweistheorie, Ontos Mathematische Logik , 2, Hrsg. R. Schindler, Ontos Verlag, Frankfurt, 2010, S. 133–153.

[8] I. Shapirovsky, „PSPACE-Entscheidbarkeit der polymodalen Logik von Japaridze“ . Advances in Modal Logic 7 (2008), S. 289–304.

[9] L. Beklemishev, „Beweisbarkeitsalgebren und beweistheoretische Ordinalzahlen, I“ . Annals of Pure and Applied Logic 128 (2004), S. 103–123.

[10] G. Boolos, Die Logik der Beweisbarkeit . Cambridge University Press, 1993.

[ 1 ]

[

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

7 ]

[ 8 ]

[ 9 ]

[ 10 ]