Beweistheorie

Beweistheorie

Die Beweistheorie ist ein Teilgebiet der mathematischen Logik, das Beweise als formale mathematische Objekte behandelt. Dies ermöglicht ihre Analyse mit mathematischen Techniken. Beweise werden üblicherweise als induktiv definierte Datenstrukturen dargestellt, wie Listen oder Bäume. Diese werden gemäß den Axiomen und Schlussregeln des betrachteten logischen Systems konstruiert. Die Beweistheorie ist von syntaktischer Natur im Gegensatz zur Modelltheorie, die von semantischer Natur ist.

Manchmal wird die Beweistheorie auch als Teil der philosophischen Logik aufgefasst, dabei ist vor allem die Idee der beweistheoretischen Semantik von Interesse.

Inhaltsverzeichnis

Geschichte

Obwohl die Formalisierung der Logik durch die Werke von Gottlob Frege, Giuseppe Peano, Bertrand Russell, Richard Dedekind und anderen bereits weit entwickelt war, wird der Beginn der modernen Beweistheorie David Hilbert zugeschrieben, der das so genannte Hilbertprogramm initiierte und in den 1920er Jahren im Zuge des Grundlagenstreits systematisch ausbaute. Kurt Gödels Arbeiten führten zuerst zu großen Fortschritten, widerlegten aber schließlich dieses Programm: der Vollständigkeitssatz verhieß gute Aussichten für Hilberts Ziel, sämtliche Mathematik auf ein finitistisches formales System zu reduzieren; der Unvollständigkeitssatz zeigte allerdings später, dass dies unerreichbar ist. Diese Resultate wurden in einem Beweiskalkül ausgeführt, welchen man Hilbert-Kalkül nennt.

Zeitgleich mit den beweistheoretischen Arbeiten von Gödel legte Gerhard Gentzen die Grundpfeiler für das, was heute als strukturelle Beweistheorie bekannt ist. In wenigen Jahren führte Gentzen die grundlegenden Formalismen des natürlichen Schließens (gleichzeitig wie und unabhängig von Jaskowski) und des Sequenzenkalküls ein, machte wesentliche Fortschritte bei der Formalisierung der intuitionistischen Logik. Des Weiteren führte er ebenfalls die wichtige Idee des analytischen Beweises ein und gab den ersten kombinatorischen Beweis der Konsistenz der Peano-Arithmetik.

Formale und informale Beweise

Die informalen Beweise, die in der Mathematik üblicherweise benutzt werden, sind nicht mit den formalen Beweisen der Beweistheorie zu verwechseln. Die informalen Beweise gleichen Skizzen, aus denen Experten im Prinzip formale Beweise rekonstruieren könnten. Das Schreiben von formalen Beweisen würde allerdings für Mathematiker dieselben Nachteile wie das Programmieren in Maschinensprache haben.

Im Bereich des maschinengestützten Beweisens werden formale Beweise mit Hilfe von Computern erzeugt. Solche Beweise können auch automatisch mittels Computern überprüft werden. Das Überprüfen von Beweisen ist üblicherweise trivial, im Gegensatz zum Finden von Beweisen, das typischerweise sehr schwierig ist. Informale Beweise in der mathematischen Literatur hingegen werden durch Peer-Review überprüft. Dies kann mehrere Wochen dauern und solche Beweise können immer noch Fehler enthalten.

Arten von Beweiskalkülen

Die drei bekanntesten Arten von Beweiskalkülen sind:

Jeder dieser Kalküle kann für eine axiomatische Formalisierung der Aussagenlogik oder Prädikatenlogik der klassischen oder intuitionistischen Art benutzt werden. Die meisten Kalküle eignen sich zudem auch für die meisten Modallogiken und für viele substrukturelle Logiken, wie z.B. die lineare Logik oder die Relevanzlogik. Es ist eher außergewöhnlich, Logiken zu finden, die sich nicht mit einem dieser Kalküle darstellen lassen.

Konsistenzbeweise

Hauptartikel: Widerspruchsfreiheit

Wie bereits früher erwähnt wurde, war das Hilbertprogramm der Ansporn für die mathematische Untersuchung von Beweisen in formalen Theorien. Die zentrale Idee dieses Programms war, die Konsistenz der formalen Theorien, die von Mathematikern benutzt werden, mit einem finitistischen Beweis zu zeigen und so mit einem metamathematischen Argument diese Theorien zu fundieren. Genauer ausgedrückt, gilt es zu zeigen, dass rein universelle Aussagen (technischer: es sind die beweisbaren Unvollständigkeitssatz herbeigeführt. Dieser Satz zeigte, dass jede ω-konsistente Theorie, die genügend stark ist, um gewisse einfache arithmetische Aussagen auszudrücken, ihre eigene Konsistenz nicht beweisen kann. Die Aussage, dass eine Theorie konsistent ist, ist in Gödels Formulierung ein \Pi^0_1 Satz.

In diesem Bereich wurde viel Forschung betrieben und unter anderem wurden folgende Resultate gefunden:

  • Verfeinerung von Gödels Resultat, insbesondere konnte John Barkley Rosser zeigen, dass statt ω-Konsistenz die schwächere Voraussetzung Konsistenz genügt, um den Unvollständigkeitssatz zu zeigen
  • Die Axiomatisierung der Kernaussagen von Gödels Resultat mit Ausdrücken der Modallogik, Beweisbarkeitslogik
  • Transfinite Iterationen von Theorien durch Alan Turing und Solomon Feferman
  • Die Entdeckung von selbstüberprüfenden Theorien, also von Systemen, die stark genug sind, um über sich selber zu sprechen, aber zu schwach, um das Diagonalisierungsargument durchzuführen, das in Gödels Unvollständigkeitssatz benutzt wird

Strukturelle Beweistheorie

Strukturelle Beweistheorie ist ein Teilgebiet der Beweistheorie, welches Beweiskalküle studiert, in denen der Begriff des analytischen Beweises sinnvoll ist. Der Begriff des analytischen Beweises wurde von Gentzen für den Sequenzenkalkül eingeführt. In diesem Fall sind analytische Beweise diejenigen Beweise, die schnittfrei sind. In Systemen natürlichen Schließens kann man auch eine Interpretation für den Begriff des analytischen Beweises finden, wie von Dag Prawitz gezeigt wurde. In diesem Fall ist die Definition aber kompliziert. Ungewöhnlichere Beweiskalküle, wie Jean-Yves Girards Beweisnetze ermöglichen auch eine Definition des Begriff des analytischen Beweises.

Strukturelle Beweistheorie ist durch den Curry-Howard-Isomorphismus auch mit der Typentheorie verbunden. Der Curry-Howard-Isomorphismus zeigt eine Analogie zwischen der Normalisierung in Systemen natürlichen Schließens und der Beta-Reduktion im typisierten Lambdakalkül auf. Dadurch wird die Grundlage für die intuitionistische Typentheorie, welche von Per Martin-Löf entwickelt wurde, geschaffen. Dieser Zusammenhang kann auch noch auf kartesisch abgeschlossene Kategorien ausgeweitet werden.

In der Linguistik, typen-logischen Grammatik, kategorischen Grammatik und der Montague-Grammatik werden Formalismen, welche aus der strukturellen Beweitheorie stammen, benutzt, um eine formale Semantik der natürlichen Sprache zu finden.

Weitere

  • Tableau- oder Baumkalküle benutzen die zentrale Idee des analytischen Beweises aus der strukturellen Beweistheorie, um Entscheidungsverfahren und Semi-Entscheidungsverfahren für viele Logiken zur Verfügung zu stellen.
  • Die Ordinalzahlanalyse ist eine mächtige Technik, um kombinatorische Konsistenzbeweise von Theorien, die die Arithmetik oder Analysis formalisieren, zu liefern.
  • Substrukturelle Logiken verfügen über weniger strukturelle Regeln.

Literatur

Weblinks


Wikimedia Foundation.

Игры ⚽ Поможем сделать НИР

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Beweistheorie — Beweistheorie,   Teilgebiet der Metamathematik, in dem Beweissysteme für formalisierte Theorien untersucht werden. Die Beweistheorie entstand zur Realisierung des Hilbert Programms. In ihr werden z. B. die Teilgebiete der Mathematik als… …   Universal-Lexikon

  • Beweistheorie — nennt man den Inbegriff der Grundsätze, die in Ansehung der Stellung des Gerichts zu einem im Prozeß geführten Beweis oder bezüglich der sogen. Beweiswürdigung gelten. Der Beweis (s. d.) soll bei dem Richter die Überzeugung von der Wahrheit… …   Meyers Großes Konversations-Lexikon

  • Beweisbarkeit — Die Beweistheorie ist ein Teilgebiet der mathematischen Logik, das Beweise als formale mathematische Objekte behandelt. Dies ermöglicht ihre Analyse mit mathematischen Techniken. Beweise werden üblicherweise als induktiv definierte… …   Deutsch Wikipedia

  • Mathematische Logik — Die Mathematische Logik ist ein Teilgebiet der Mathematik. Oft wird sie in die Teilgebiete Modelltheorie, Beweistheorie, Mengenlehre und Rekursionstheorie aufgeteilt. Forschung im Bereich der mathematischen Logik hat zum Studium der Grundlagen… …   Deutsch Wikipedia

  • Hilbert-Programm — Das Hilbertprogramm ist ein Forschungsprogramm, das der Mathematiker David Hilbert in den 20er Jahren vorschlug. Es zielt darauf ab, mit finiten Methoden die Widerspruchsfreiheit der Axiomensysteme der Mathematik nachzuweisen. Auch wenn sich das… …   Deutsch Wikipedia

  • Hilberts Programm — Das Hilbertprogramm ist ein Forschungsprogramm, das der Mathematiker David Hilbert in den 20er Jahren vorschlug. Es zielt darauf ab, mit finiten Methoden die Widerspruchsfreiheit der Axiomensysteme der Mathematik nachzuweisen. Auch wenn sich das… …   Deutsch Wikipedia

  • Hilberts zweites Problem — Das Hilbertprogramm ist ein Forschungsprogramm, das der Mathematiker David Hilbert in den 20er Jahren vorschlug. Es zielt darauf ab, mit finiten Methoden die Widerspruchsfreiheit der Axiomensysteme der Mathematik nachzuweisen. Auch wenn sich das… …   Deutsch Wikipedia

  • Kurt Schütte — (* 14. Oktober 1909 in Salzwedel; † 18. August 1998 in München) war ein deutscher Mathematiker und Hochschullehrer. Kurt Schütte Schütte studierte Mathematik, Physik, Chemie und Philosophie in Berlin und an der Universität Göttingen, wo er 1933… …   Deutsch Wikipedia

  • L.E.J. Brouwer — Luitzen E. J. Brouwer (* 27. Februar 1881 in Overschie; † 2. Dezember 1966 in Blaricum) war ein niederländischer Mathematiker. Er schuf grundlegende topologische Methoden und Begriffe und bewies bedeutende topologische Sätze. Nach ihm ist der… …   Deutsch Wikipedia

  • L. E. J. Brouwer — Luitzen E. J. Brouwer (* 27. Februar 1881 in Overschie; † 2. Dezember 1966 in Blaricum) war ein niederländischer Mathematiker. Er schuf grundlegende topologische Methoden und Begriffe und bewies bedeutende topologische Sätze. Nach ihm ist der… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”