WikiDer > Beweistheorie

Beweistheorie ist ein Zweig der mathematische Logik Das beweisen als formell mathematische Objekte zeugt. Dies ermöglicht die Analyse von Beweisen mit mathematischen Techniken. Beweise werden in der Regel als induktiv definiert Algorithmen, die nach Axiom's und Ableitungsregeln des logischen Systems aufgebaut sind. Als solche ist die Beweistheorie syntaktisch Natur, im Gegensatz zu den Modelltheorie, die von Natur aus semantisch ist. Zusammen mit dem Modelltheorie, das axiomatische Mengenlehre und Rekursionstheorie gilt die Beweistheorie als eine der vier sogenannten Säulen der of Grundlagen der Mathematik.^[1]Die Beweistheorie kann auch als ein Zweig der philosophische Logik, wobei die beweistheoretische Semantik am wichtigsten ist. Es hängt davon ab, ob bestimmte Ideen der strukturellen Evidenztheorie durchführbar sind oder nicht.

Geschichte

Obwohl die Formalisierung der Logik viel der Arbeit von Gottlob Frege, Giuseppe Peano, Bertrand Russell und Richard Dedekind, wird David Hilbert wird oft als Begründer der modernen Beweistheorie angesehen. Er initiierte das nach ihm benannte Hilberts Programm in den Grundlagen der Mathematik. Dieses Programm zielt darauf ab, die gesamte Mathematik auf ein Endliches zu reduzieren formales System, die Grundlage dafür ist die Vollständigkeitssatz von Gödel. Die Arbeit wurde unter Verwendung des Beweiskalküls namens Hilbert-System durchgeführt. Hat erstmal geholfen Kurt Gödel nahm an Hilberts Programm teil, aber später widerlegte Gödel die Prämisse des Programms mit seinem unvollständige Theoreme zeigen, dass das erklärte Ziel unerreichbar war.

Parallel zu dieser beweistheoretischen Arbeit von Gödel, Gerhard Gentzen die Grundlage für das, was heute als strukturelle Evidenztheorie bekannt ist. Gentzen führte in relativ kurzer Zeit die Kernformalismen der Natur Abzug, übrigens gleichzeitig mit und unabhängig von Stanislaw Jaskowski, machte er grundlegende Fortschritte bei der Formalisierung der intuitionistischen Logik, führte die wichtige Idee eines analytischen Beweises ein und lieferte den ersten kombinatorischen Beweis für die Konsistenz der Peano-Arithmetik.

Formale und informelle Beweise

Die informellen Beweise aus der täglichen mathematischen Praxis entsprechen nicht den formelle Beweise aus der Beweistheorie. Informelle Beweise lassen sich am besten mit Skizzen vergleichen, in denen die Hauptlinien dargelegt sind, anhand derer ein Experte mit genügend Zeit und Geduld einen formalen Beweis rekonstruieren kann. Für die meisten Mathematiker hätte das Schreiben eines vollständig formalen Beweises jedoch die gleichen Nachteile wie das Schreiben eines vollständigen formalen Beweises Computerprogrammierung im Maschinensprache Für ein Computerprogrammierer.

Formale Beweise werden interaktiv mit Hilfe von Spezial Software auf der Computer konstruiert. Noch wichtiger ist jedoch, dass diese Proofs auf diesem Computer automatisch überprüft werden können. Die Prüfung formaler Beweise ist normalerweise einfach, während Sie a Computer Programm dass man in der Mathematik Beweise liefern kann, ist sehr kompliziert.

Neue Beweise in der Literatur sind informell. Diese sind so kompliziert, dass manuelle Kontrollen Wochen dauern Peer-Review notwendig.

Verweise