Gödel theorems for nonconstructive logics. (Q2603369)

Bekanntlich gilt nach \textit{Gödel} (Mh. Math. Phys. 38 (1931), 173-198; F.~d.~M. 57\(_{\text{I}}\), 54): Falls ein logisches System die Arithmetik umfaßt, so folgt aus der Annahme seiner Widerspruchsfreiheit die Existenz einer Aussagenfunktion \(f(x)\) derart, daß \(f(0),f(1),f(2),\dots\) alle im System beweisbar sind, dagegen \((x)f(x)\) darin nicht beweisbar ist. Verf. studiert im vorliegenden Aufsatz logische Systeme, die sich von dem l.~c. von \textit{Gödel} betrachteten dadurch unterscheiden, daß die folgende nicht-konstruktive Regel von \textit{Carnap} benutzt wird: Gehören \(f(0),f(1),f(2),\dots\) alle zu den ``beweisbaren Formeln'', so gehört \((x)f(x)\) auch dazu. Er definiert mittels transfiniter Induktion eine Reihe von Systemen \(P_\alpha\), wo \(\alpha\) eine beliebige Ordnungszahl sein kann, nämlich so: \(P_0\) ist das logische System von \textit{Gödel}; \(P_{\alpha+1}\) entsteht aus \(P_\alpha\) durch Anwendung der \textit{Carnap}schen Regel, indem \(f(0),f(1),\dots\) alle in \(P_\alpha\) beweisbar sind. Ist \(\alpha\) eine Limeszahl, so ist \(P_\alpha\) die Vereinigungsmenge aller \(P_\beta\), wo \(\beta<\alpha\) ist. Verf. beweist, daß für jedes \(P_n\) und jedes \(P_{\omega+n}\), \(n\) endlich, ähnliche Theoreme gelten, wie die von \textit{Gödel} für \(P_0\) bewiesenen. Insbesondere gibt es in diesen Systemen, falls sie widerspruchsfrei sind, unentscheidbare Aussagen, und weder die beweisbaren noch die nicht-beweisbaren Aussagen sind rekursiv abzählbar. Außerdem ist die Widerspruchsfreiheit von \(P_n\) bzw. \(P_{\omega+n}\) erst in \(P_{n+1}\) bzw. \(P_{\omega+n+1}\) beweisbar. Verf. beweist sogar ähnliche Sätze für \(P_\varOmega\), das in bezug auf \textit{Carnap}s Regel abgeschlossen ist.