Die Beweisbarkeitslogik ist eine Modallogik, die den Modaloperator von K als Beweisbarkeit und ein zusätzliches Axiom interpretiert, das aus dem Satz von Löb abgeleitet ist .
Nun zeigt das SEP , dass es möglich ist, den 2. Unvollständigkeitssatz von Gödel aus diesem Aufbau abzuleiten . Aber was hat es mit dem 1. Unvollständigkeitssatz von Gödel zu tun ? Es scheint unwahrscheinlich, dass dies in Löbs Satz enthalten ist, da dieser eine Frage von Henkin zu Sätzen beantwortete, die ihre eigene Beweisbarkeit behaupten, während Gödel Sätze untersuchte, die ihre Nicht-Beweisbarkeit behaupteten.
(2 Jahre später) Ich bin über eine sehr schöne und saubere Antwort gestolpert, hier geht es weiter:
Nehmen wir zunächst an, dass die Arithmetik konsistent ist. Ist dies nicht der Fall, ist Gödel/Rosser trivial gültig, da ihr Ergebnis von der Form "wenn PA konsistent ist, dann ..." ist.
Nehmen Sie an, dass Sie F oder ¬F für jede Formel F beweisen können (im Gegensatz zum Satz von Gödel/Rosser).
Wenn Sie eine bestimmte willkürliche, aber feste Formel F beweisen können, dann können Sie auch Bew([F]) beweisen, wobei Bew das Standard-Beweisprädikat und der [] codierende (Meta-)Operator ist. Wenn Sie ¬F beweisen können, können Sie auch Bew([¬F]) beweisen. Unabhängig davon, ob F beweisbar oder ¬F beweisbar ist, können Sie also (Bew([¬F]) oder Bew([F])) für jede Formel F beweisen.
Aber nach Solovays Vollständigkeitssatz für die Beweisbarkeitslogik (System GL) sollte die Formel ([]F oder []¬F) dann ein Satz der GL sein. Es ist jedoch nicht. Gegenbeispiel Kripke-Modell: l[p] <- w -> r[¬p], Modell ist transitiv und konvers begründet, aber w |=/= ([]p oder []¬p).
Bearbeiten: Siehe meine andere Antwort (unter oder über dieser) .
Der zweite Satz wäre eigentlich (ASCII-Art, da uns hier LaTeX fehlt):
GL |- ~[]_|_ => GL |- _|_,
und nicht das, wofür SEP einen Beweis liefert, nämlich:
GL |- []~[]_|_ -> []_|_
das ist eigentlich eine "formalisierte" Version des zweiten Unvollständigkeitssatzes (PA spricht wieder über sich selbst). Ich glaube nicht, dass die oben angegebene erste Version Sinn macht (die "eigentliche" 2. IT), da wir wissen GL |-/- _|_(das heißt, dass GL konsistent ist)
Ich vermute also, dass das Beste, wonach Sie in GL suchen könnten, eine formalisierte Version des ersten Unvollständigkeitssatzes ist.
Vielleicht ist dies ein guter Ausgangspunkt (die folgende Formel ist in der Tat ein Theorem, Sie können dies anhand von Bäumen oder einem direkten Beweis in Boolos 'The Logic of Provability überprüfen):
GL |- [](p <-> ~[]p) -> [](p <-> ~[]_|_)
Was (grob) übersetzt werden kann als "Wenn (es ist beweisbar, dass) P sagt, dass P nicht beweisbar ist, dann ist P beweisbar, wenn und nur wenn Sie Konsistenz beweisen können".
If you assume:
[](p <-> ~[]p)
then
[](p <-> ~[]_|_),
and if []p, then:
[]~[]_|_, then
[]_|_, while if []~p, then
[]~~[]_|_, that is: [][]_|_
So:
GL |- ([](p <-> ~[]p) && ([]p or []~p)) -> ([]_|_ or [][]_|_)
Vielleicht gibt es sogar einen direkteren Weg, den ersten Satz darzustellen, ich bin mir nicht sicher. (Das wäre ein Kommentar gewesen, wenn ich einen posten dürfte. :) ).
Laut dieser Antwort von Peter Smith:
Wie Sie sagen, können Sie den zweiten Unvollständigkeitssatz aus den Hilbert-Bernays-Löb-Ableitbarkeitsbedingungen für das Beweisbarkeitsprädikat (die sich in der modalen "Beweisbarkeitslogik" widerspiegeln) zusammen mit dem Diagonalisierungslemma erhalten, das uns sagt, dass es a gibt Fixpunkt für 'nicht beweisbar'. Aber für den Standardbeweis des zweiten Theorems mit den Ableitbarkeitsbedingungen (nein?) braucht man das Diagonalisierungslemma.
Und dieses Diagonalisierungslemma liefert Ihnen natürlich fast sofort den ersten Satz.
Also, die Antwort ist ja.
Hunan Rostomyan