Beweisbarkeitslogik für Rosser-Sätze

Abstract

Kurt Gödel zeigte 1931 in seiner klassischen Arbeit 'Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I', dass die wahren Sätze der Mathematik nicht als die Theoreme irgendeines formalen Systems erhalten werden können. Zum Beweis dieses Satzes konstruierte Gödel arithmetische Aussagen, die von sich selbst behaupten: 'Ich bin (im betrachteten System) nicht beweisbar.' Solche Gödel-Sätze sind dann tatsächlich nicht beweisbar. Somit sind sie aber wahr und belegen daher die Unvollständigkeit des betrachteten formalen Systems.John Barkley Rosser verbesserte 1936 in 'Extensions of Some Theorems of Gödel and Church' Gödels Ergebnis, wobei er statt Gödel-Sätzen so genannte Rosser-Sätze betrachtete, die ungefähr besagen: 'Wenn ich beweisbar bin, dann auch meine Negation.'Nun kann man Formeln der modalen Aussagenlogik in die Sprache der Arithmetik 'übersetzen', indem man Aussagevariablen durch arithmetische Aussagen ersetzt und den Notwendigkeitsoperator als formalisiertes Beweisbarkeitsprädikat liest.1976 bewies Robert M. Solovay ('Provability Interpretations of Modal Logic'), dass das modallogische System GL gerade diejenigen Formeln liefert, die unter allen solchen Übersetzungen beweisbar sind. Dadurch wird es möglich, das formalisierte Beweisbarkeitsprädikat mit modallogischen Mitteln zu untersuchen, d.h. Beweisbarkeitslogik zu treiben.1979 machten Solovay und D. Guaspari in 'Rosser Sentences' auch Rosser-Phänomene zugänglich für modallogische Methoden.In der vorliegenden Arbeit werden diese Resultate von Guaspari und Solovay, zusammen mit den nötigen prädikaten- und modallogischen Grundlagen, ausgeführt und etwas verallgemeinert. Ich habe versucht, den Gegenstand so darzustellen, dass er auch für interessierte LeserInnen mit Grundkenntnissen in Mathematischer Logik leicht zugänglich wird. Die Kapitel I, II und IV können für sich genommen auch als Einführung in die Beweisbarkeitslogik dienen.