Beweisbarkeitslogik
-- Gödel, Rosser, Solovay --
Christopher von Bülow
Kurt Gödel erschütterte 1931 die mathematische Welt mit seinem Unvollständigkeitssatz. Gödel zeigte, wie für jedes noch so starke formale System der Arithmetik ein Satz konstruiert werden kann, der besagt: „Ich bin nicht beweisbar.“ Würde das System diesen Satz beweisen, so würde es sich damit selbst Lügen strafen. Also ist dies ein wahrer Satz, den es nicht beweisen kann: Es ist unvollständig. John Barkley Rosser verstärkte später Gödels Ergebnisse, wobei er die Reihenfolge miteinbezog, in der Sätze bewiesen werden, gegeben irgendeine Auffassung von „Beweis“. In der Beweisbarkeitslogik werden die formalen Eigenschaften der Begriffe „beweisbar“ und „wird früher bewiesen als“ mit modallogischen Mitteln untersucht: Man liest den notwendig – Operator als beweisbar und gibt formale Systeme an, die die Modallogik der Beweisbarkeit erfassen.
Diese Arbeit richtet sich sowohl an Logik-Experten wie an durchschnittlich vorgebildete Leser. Ihr Ziel ist es, in die Beweisbarkeitslogik einzuführen und deren wesentliche Resultate, insbesondere die Solovayschen Vollständigkeitssätze, präzise, aber leicht zugänglich zu präsentieren.
