imported>MrBenjo: Normdaten

2025-07-24T20:57:33Z

Normdaten

Neue Seite

Die '''Beweistheorie''' ist ein Teilgebiet der [[Mathematische Logik|mathematischen Logik]], das [[Beweis (Mathematik)|Beweise]] als formale mathematische Objekte behandelt, was deren Analyse mit mathematischen Techniken ermöglicht. Beweise werden üblicherweise als induktiv definierte [[Datenstruktur]]en dargestellt, wie [[Liste (Datenstruktur)|Listen]] oder [[Baum (Graphentheorie)|Bäume]]. Diese werden gemäß den [[Axiom]]en und [[Schlussregel]]n des betrachteten logischen Systems konstruiert. Die Beweistheorie ist von [[Syntax|syntaktischer]] Natur im Gegensatz zur [[Modelltheorie]], die von [[Semantik|semantischer]] Natur ist.

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

== 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 [[Grundlagenkrise der Mathematik|Grundlagenstreits]] systematisch ausbaute. [[Kurt Gödel]]s 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 [[Finitismus|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 [[Systeme natürlichen Schließens|natürlichen Schließens]] (gleichzeitig mit und unabhängig von Jaskowski) und des [[Sequenzenkalkül]]s ein und machte wesentliche Fortschritte bei der Formalisierung der [[Intuitionistische Logik|intuitionistischen Logik]]. Des Weiteren führte er die wichtige Idee des [[Analytischer Beweis|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ütztes Beweisen|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:

* der [[Hilbert-Kalkül]]
* die [[Systeme natürlichen Schließens]]
* der [[Sequenzenkalkül]]

Jeder dieser Kalküle kann für eine axiomatische Formalisierung der [[Aussagenlogik]] oder [[Prädikatenlogik]] der [[Klassische Logik|klassischen]] oder [[Intuitionistische Logik|intuitionistischen]] Art benutzt werden. Die meisten Kalküle eignen sich zudem auch für die meisten [[Modallogik]]en und für viele [[substrukturelle Logik]]en, 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 (gemeint sind die beweisbaren <math>\Pi^0_1</math>-Sätze der [[Arithmetische Hierarchie|Arithmetischen Hierarchie]]) finitistisch wahr sind.

Das Scheitern des Programms wurde durch Gödels [[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 <math>\Pi^0_1</math>-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üfende Theorie|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 [[Analytischer Beweis|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 [[Gentzenscher Hauptsatz|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 Girard]]s [[Beweisnetz]]e ermöglichen auch eine Definition des Begriffs 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 [[Typisierter Lambdakalkül|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 Kategorie|kartesisch abgeschlossene Kategorien]] ausgeweitet werden.

In der [[Linguistik]], [[Typen-logische Grammatik|Typen-logischen Grammatik]], [[Kategorische Grammatik|kategorischen Grammatik]] und der [[Montague-Grammatik]] werden Formalismen, welche aus der strukturellen Beweistheorie stammen, benutzt, um eine formale Semantik der natürlichen Sprache zu finden.

== Weitere ==
* Tableau- oder [[Baumkalkül]]e 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 Logik]]en verfügen über weniger strukturelle Regeln.

== Literatur ==
* J. Avigad, E. H. Reck: [https://www.andrew.cmu.edu/user/avigad/Papers/infinite.pdf ''“Clarifying the nature of the infinite”: the development of metamathematics and proof theory''.] (PDF; 318 kB). Carnegie-Mellon Technical Report CMU-PHIL-120, 2001 .
* [[Karel Berka]], Lothar Kreiser: ''Logik-Texte. Kommentierte Auswahl zur Geschichte der modernen Logik''. 4. Auflage. Akademie, Berlin 1986
* [[Stephen Cole Kleene]]: ''Introduction to Metamathematics''. Amsterdam / Groningen 1952
* [[Paul Lorenzen]]: ''Metamathematik''. Mannheim 1962
* [[Gerhard Gentzen]]: ''The Collected Papers of Gerhard Gentzen''. Hrsg.: M. E. Szabo. Amsterdam 1969
* {{Literatur
|Autor=Wolfram Pohlers
|Titel=Proof theory: the first step into impredicativity
|Verlag=Springer
|Ort=Berlin / Heidelberg
|Datum=2009
|ISBN=978-3-540-69318-5}}
* {{Literatur
|Autor=Kurt Schütte
|Titel=Proof theory
|Reihe=Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen
|BandReihe=225
|Verlag=Springer
|Ort=Berlin / Heidelberg
|Datum=1977
|ISBN=3-540-07911-4}}
* {{Literatur
|Autor=Gaisi Takeuti
|Titel=Proof theory
|Reihe=Studies in logic and the foundations of mathematics
|BandReihe=81
|Auflage=2
|Verlag=North-Holland
|Ort=Amsterdam
|Datum=1987
|ISBN=0-444-87943-9}}
* A. S. Troelstra, [[Helmut Schwichtenberg|H. Schwichtenberg]]. ''Basic Proof Theory'' (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press, ISBN 0-521-77911-1

== Weblinks ==
* {{SEP|https://plato.stanford.edu/entries/proof-theory/|Proof Theory|Michael Rathjen, Wilfried Sieg}}
* {{SEP|https://plato.stanford.edu/entries/proof-theory-development/|The Development of Proof Theory|[[Jan von Plato]]}}

{{Normdaten|TYP=s|GND=4145177-6|LCCN=sh85107437|NDL=01190375}}

[[Kategorie:Mathematische Logik]]
[[Kategorie:Beweis (Mathematik)]]
[[Kategorie:Teilgebiet der Mathematik]]

Beweistheorie - Versionsgeschichte

imported>MrBenjo: Normdaten