Zielsetzungen, Methoden und Ergebnisse der Hilbertschen Beweistheorie. (Q2579574)

Voraussetzung für exakte Widerspruchsfreiheitsbeweise (WF Beweise) ist die formale Axiomatik. Es gibt relative WF Beweise (z. B. das euklidische Modell der Bólyaischen Geometrie, das Gödelsche Modell der Mengentheorie mit Auswahlund Kontinuumsaxiom in der Mengenlehre ohne diese Axiome) und ``absolute'' WF Beweise. Hier lieferten die Wertungsmethode (J. König; Herbrand, Presburger) und die Teilwertungsmethode (v. Neumann; Hilbert, Ackermann, Herbrand) die WF der Arithmetik bei eingeschränkter vollständiger Induktion. Erst Gentzen gelang unter zusätzlicher Verwendung von Beweistransformationen der WF Beweis für die Arithmetik; dieser Beweis wurde neuerdings auch von Ackermann mit Hilfe der Teilwertungsmethode geliefert. (Nach dem deutschen Auszug referiert.)