Some aspects of the problem of mathematical rigor. (Q2579573)

Die transatlantische Grundlagenforschung hat sich in den letzten 10 Jahren die Weltgeltung erkämpft, durch die sie in die vorderste Linie gerückt ist. Auf eine ungewöhnliche Art ist der Stil dieser Forschung erkennbar in der vorliegenden originellen Einführung in die exakte Formalisierungstechnik: mustermäßige Entwicklung des technischen Könnens, planmäßiges Absehen (wie in \textit{Carnap}s ``Logischer Syntax der Sprache'' (1934; JFM 60.0019.*)) von allem Zusätzlichen, also nicht nur von allen philosophischen oder halbphilosophischen Spekulationen, sondern auch von den um eine normierende Abgrenzung des inhaltlich Sinnvollen bemühten bahnbrechenden Betrachtungen im Fregeschen oder im Leśniewskisehen Sinne und ein fast ebenso planmäßiges Absehen von den durch die Tarskische Semantik auf eine epochemachende Art der Präzisierbarkeit zugeführten Deutungsfragen. An einer Axiomatisierung der Gruppentheorie durch \textit{L. E. Dickson} vom Jahre 1905 (Trans. Amer. math. Soc. 6, 198-204; F. d. M. 36, 207 (JFM 36.0207.*)) wird anschaulich gezeigt, was heute unter einer Formalisierung einer mathematischen Theorie zu verstehen ist, und wie der Begriff der mathematischen Beweisstrenge präzisiert ist in den strukturellen (den nicht explizit angegebenen Tarski-Postulaten zu unterwerfenden) Folgerungsbegriffen, die in eine solche Formalisierung eingehen. Im Anschluß an den Begriff des formalisierten Systems wird der Begriff des abstrakten Kalküls diskutiert mit dem Ergebnis, daß beide Begriffe ``im wesentlichen'' identisch sind. -- Es scheint mir, daß der hier übrig bleibende unerwünschte Rest von Unbestimmtheit durch eine Identifizierung der formalisierten Systeme mit den abstrakten Kalkülen (im Sinn von \textit{K. Schröter}, Ein allgemeiner Kalkülbegriff (Forsch. Logik Grundleg. exakt. Wiss. (2) 6 (1941); F. d. M. 67, 38)) auf eine restlos befriedigende Art zum Verschwinden gebracht werden kann. Dann muß auch die tiefliegende Frage, wann zwei abstrakte Kalküle als \textit{isomorph} gelten sollen, in einem präzisierten Sinne beantwortet werden. Es ist ferner erwünscht, daß präzisiert wird, wann ein solcher abstrakter Kalkül als \textit{gedeutet} oder als eine \textit{formalisierte Sprache} gelten soll. Dann kann auch die Frage beantwortet werden, was unter der durch eine solche Sprache darstellbaren \textit{Logik} zu verstehen ist; und mit einer mathematischen Genauigkeit, so daß der vom Verf. neben dem Formalismus und Intuitionismus als drittes abgelehnte Logizismus in den Rang eines wohldefinierten Standortes aufrückt. Endlich würde in diesem Zusammenhang auch noch die Einführung von semantischen Folgerungsbegriffen neben den semantischen Satzbegriffen zu berücksichtigen sein. Auf die wesentliche Verstärkung der nichtformalen Konstruktionsmittel, die bei dieser Durchmodellierung des angedeuteten Komplexes auch in den strengsten Formalismus entscheidend eingehen, kann hier nicht eingegangen werden. Ernste Schwierigkeiten für eine Präzisierung des Begriffs der Beweisstrenge treten auf in den metatheoretischen Untersuchungen. Es scheint mir, daß diese Schwierigkeiten unüberwindlich sind: aus dem durchschlagenden Grunde, weil wir stets irgendwo Halt machen müssen bei einer Beschreibungssprache, für welche die Logik, von der sie beherrscht ist, auf eine unvermeidliche Art \textit{nicht} mehr formalisiert ist. Hieraus folgt, daß man von einem präzisierten Begriff von Beweisstrenge in einer Metatheorie dann und nur dann wird sprechen können, wenn diese Metatheorie selbst formalisiert ist. Verf. schlägt für die metatheoretischen Beweise eine in dem angedeuteten unvermeidlichen Sinne nicht-präzisierte Aufteilung vor in konstruktive und nicht-konstruktive, und so, daß nur die konstruktiven Beweise als streng gelten sollen. Konstruktiv ist z. B. der Gödelsche Beweis des Unvollständigkeitstheorems, nicht-konstruktiv z. B. der Löwenheim-Skolemsche Beweis des Theorems, daß es zu jedem widerspruchsfreien Axiomensystem der Mengenlehre ein abzählbares Modell gibt. Mathematik ist die Wissenschaft von den formalisierten Systemen.