Zur intuitionistischen Arithmetik und Zahlentheorie. (Q2624161)

Übersetzt man die Absurdität \(\neg \) durch die Negation \(\sim \), und läßt man sonst den Grundbegriffen des \textit{Heyting}schen Aussagenkalküls \(H\) die gleich bezeichneten des klassischen \(A\) entsprechen, so erscheint \(H\) als Teil von \(A\). Wie von \textit{Glivenko} gezeigt worden ist, ist aber bei anderer Übersetzung umgekehrt \(A\) ein Teil von \(H\), nämlich wenn die klassischen Begriffe \[ \sim p,\quad p\rightarrow q,\quad p\vee q,\quad p\cdot q \] durch die intuitionistischen \[ \neg p,\quad \neg (p\wedge \neg q),\quad \neg (\neg p\wedge \neg q),\quad p\wedge q \] übersetzt werden. In vorliegender Abhandlung beweist Verf., daß ähnliches auch für die Arithmetik gilt, z. B. in dem Umfang, wie sie durch die Axiome von \textit{Herbrand} (vgl. 1931; JFM 57.0056.*) gegeben ist. Er zeigt, daß man die klassischen Begriffe intuitionistisch so interpretieren kann, daß alle aus den klassischen Axiomen beweisbaren Sätze auch für den Intuitionismus gelten. Dabei wird das \textit{Heyting}sche System erweitert durch Hinzunahme der rekursiven Definition von Funktionen, die ja auch intuitionistisch einwandfrei ist. Das erweiterte \textit{Heyting}sche System wird mit \(H'\) bezeichnet. Jeder Formel des \textit{Herbrand}schen Systems wird diejenige Formel in \(H'\) zugeordnet, die entsteht, wenn die Operationen des Aussagenkalküls in der eben angegebenen Weise intuitionistisch interpretiert werden, 0 durch 1, + durch seq' ersetzt werden und jede durch Rekursion definierte Funktion \(f_i\) durch die gleich bezeichnete in \(H'\). Dann beweist Verf. den Satz: Wenn eine Formel \(A\) im \textit{Herbrand}schen System beweisbar ist, so ihre Übersetzung \(A'\) in \(H'\). Der Beweis gelingt dadurch, daß sich zuerst mittels eines Induktionsschlusses die Richtigkeit zweier Hilfssätze zeigen läßt, nämlich erstens, daß jede Formel der Gestalt \(\neg \neg A'\supset A'\) in \(H'\) beweisbar ist, und zweitens, daß immer \(A'\supset B'\,\cdot \supset \subset \cdot \neg (A'\wedge \neg B')\) in \(H'\) gilt. Danach beweist Verf., daß einerseits für jedes Axiom \(A\) des \textit{Herbrand}schen Systems die Übersetzung \(A'\) in \(H'\) beweisbar ist, und andererseits, daß bei Anwendung der Schlußregeln des \textit{Herbrand}schen Systems aus Formeln, deren Übersetzungen in \(H'\) beweisbar sind, wieder solche Formeln entstehen. Daraus folgt offenbar die Richtigkeit der obigen Behauptung, deren Inhalt auch so ausgedrückt werden kann, daß die intuitionistische Arithmetik nur scheinbar enger ist als die klassische; in Wirklichkeit enthält sie diese nur mit einer abweichenden Interpretation. Verf. erklärt diese Tatsache dadurch, daß das intuitionistische Verbot der Negation von Allsätzen in seiner Wirkung wieder aufgehoben wird durch die Anwendbarkeit des Prädikates der Absurdität auf All sätze. Dem Ref. scheint dies Ergebnis \textit{Gödel}s sehr bemerkenswert zu sein; denn es scheint ja dann wenig Grund vorzuliegen, sich mit den Gegensätzen zwischen klassischer und intuitionistischer Mathematik zu beschäftigen. Man wird allerdings einwenden, daß der Intuitionismus doch wesentliche Einschränkungen bewirkt in der Analysis und Mengenlehre; aber es ist gewiß auch hier richtig, was \textit{Gödel} sagt, daß diese nicht durch die Ablehnung des Tertium non datur, sondern durch die der imprädikativen Definition bedingt sind, und die Kritik der imprädikativen Definition rührt nicht erst von \textit{Brouwer} her.