ブロウワー＝ヒルベルト論争

ブロウワーは、デイヴィッド・ヒルベルトとその同僚であるポール・ベルネイス、ヴィルヘルム・アッカーマン、ジョン・フォン・ノイマンらの主流の形式主義に異議を唱える形で、直観主義という数学哲学を創始した。 ^{[ 2 ]}構成的数学の一種である直観主義は、数学的推論における排中律を否定する数学の基礎の哲学である。

After completing his dissertation, Brouwer decided not to share his philosophy until he had established his career. By 1910, he had published a number of important papers, in particular the fixed-point theorem. Hilbert admired Brouwer and helped him receive a regular academic appointment in 1912 at the University of Amsterdam.^[3] After becoming established, Brouwer decided to return to intuitionism.^[3] In the later 1920s, Brouwer became involved in a public controversy with Hilbert over editorial policy at Mathematische Annalen, at that time a leading learned journal.^[4] He became relatively isolated; the development of intuitionism at its source was taken up by his student Arend Heyting.

The nature of Hilbert's proof of the Hilbert basis theorem from 1888 was controversial. Although Leopold Kronecker, a constructivist, had conceded, Hilbert would later respond to others' similar criticisms that "many different constructions are subsumed under one fundamental idea" – in other words (to quote Hilbert's biographer Constance Reid): "Through a proof of existence, Hilbert had been able to obtain a construction"; "the proof" (i.e. the symbols on the page) was "the object".^[5]

Brouwer was not convinced and, in particular, objected to the use of the law of excluded middle over infinite sets. Hilbert responded: "Taking the Principle of the Excluded Middle from the mathematician... is the same as... prohibiting the boxer the use of his fists."^[6]

In an address delivered in 1927, Hilbert attempted to defend his axiomatic system as having "important general philosophical significance."^[1] Hilbert views his system as having no tacit assumptions admitted, stating, "After all, it is part of the task of science to liberate us from arbitrariness, sentiment and habit and to protect us from the subjectivism that... finds its culmination in intuitionism."^[1]

Later in the address, Hilbert deals with the rejection of the law of excluded middle: "Intuitionism's sharpest and most passionate challenge is the one it flings at the validity of the principle of excluded middle..."^[1] Rejecting the law of the excluded middle, as extended over Cantor's completed infinite, implied rejecting Hilbert's axiomatic system, in particular his "logical ε-axiom."^[2]

Finally, Hilbert singled out Brouwer, by implication rather than name, as the cause of his present tribulation: "I am astonished that a mathematician should doubt that the principle of excluded middle is strictly valid as a mode of inference. I am even more astonished that, as it seems, a whole community of mathematicians who do the same has so constituted itself. I am most astonished by the fact that even in mathematical circles, the power of suggestion of a single man, however full of temperament and inventiveness, is capable of having the most improbable and eccentric effects."^[3]

Brouwer responded to this, saying: "Formalism has received nothing but benefactions from intuitionism and may expect further benefactions. The formalistic school should therefore accord some recognition to intuitionism instead of polemicizing against it in sneering tones while not even observing proper mention of authorship."^[4]

Until Hilbert proposed his formalism, axioms of mathematics were chosen on an intuitive basis in an attempt to use mathematics to find truth. Aristotelian logic is one such example – it seems "logical" that an object either has a stated property (e.g. "This truck is yellow") or it does not have that property ("This truck is not yellow") but not both simultaneously (the Aristotelian Law of Non-Contradiction). The primitive form of the induction axiom is another example: if a predicate P(n) is true for n = 0 and if for all natural numbers n, if P(n) being true implies that P(n+1) is true, then P(n) is true for all natural numbers n.

Hilbert's axiomatic system is different. At the outset it declares its axioms,^[7] and any (arbitrary, abstract) collection of axioms is free to be chosen. Weyl criticized Hilbert's formalization, saying it transformed mathematics "from a system of intuitive results into a game with formulas that proceeds according to fixed rules" and asking what might guide the choice of these rules. Weyl concluded "consistency is indeed a necessary but not sufficient condition" and stated "If Hilbert's view prevails over intuitionism, as appears to be the case, then I see in this a decisive defeat of the philosophical attitude of pure phenomenology, which thus proves to be insufficient for the understanding of creative science even in the area of cognition that is most primal and most readily open to evidence – mathematics."^[8]

Cantor (1897) extended the intuitive notion of "the infinite" – one foot placed after the other in a never-ending march toward the horizon – to the notion of "a completed infinite" – the arrival "all the way, way out there" in one fell swoop, and he symbolized this notion with a single sign ℵ₀ (aleph-null). Hilbert's adoption of the notion wholesale was "thoughtless", Brouwer alleged. Brouwer in his (1927a) "Intuitionistic reflections on formalism" states: "SECOND INSIGHT The rejection of the thoughtless use of the logical principle of the excluded middle, as well as the recognition, first, of the fact that the investigation of the question why the principle mentioned is justified and to what extent it is valid constitutes an essential object of research in the foundations of mathematics, and, second, of the fact that in intuitive (contentual) mathematics this principle is valid only for finite systems. THIRD INSIGHT. The identification of the principle of excluded middle with the principle of the solvability of every mathematical problem."^[9]

This Third Insight is referring to Hilbert's second problem and Hilbert's ongoing attempt to axiomatize all of arithmetic, and with this system, to discover a "consistency proof" for all of mathematics. So into this fray (started by Poincaré) Brouwer plunged head-long, with Weyl as back-up.

Their first complaint (Brouwer's Second Insight, above) arose from Hilbert's extension of Aristotle's "Law of Excluded Middle" (and "double negation") – hitherto restricted to finite domains of Aristotelian discourse – to infinite domains of discourse.^[10] In the late 1890s Hilbert axiomatized geometry.^[11] Then he went on to use the Cantorian-inspired notion of the completed infinity to produce elegant, radically abbreviated proofs in analysis (1896 and afterwards).^[12] In his own words of defense, Hilbert believed himself justified in what he had done (in the following he calls this type of proof an existence proof): "...I stated a general theorem (1896) on algebraic forms that is a pure existence statement and by its very nature cannot be transformed into a statement involving constructibility. Purely by use of this existence theorem I avoided the lengthy and unclear argumentation of Weierstrass and the highly complicated calculations of Dedekind, and in addition, I believe, only my proof uncovers the inner reason for the validity of the assertions adumbrated by Gauss^[13] and formulated by Weierstrass and Dedekind."^[14] "The value of pure existence proofs consists precisely in that the individual construction is eliminated by them and that many different constructions are subsumed under one fundamental idea, so that only what is essential to the proof stands out clearly; brevity and economy of thought are the raison d'être of existence proofs."^[15]

What Hilbert had to give up was "constructibility." His proofs would not produce "objects" (except for the proofs themselves – i.e., symbol strings), but rather they would produce contradictions of the premises and have to proceed by reductio ad absurdum extended over the infinite.

Brouwer viewed this loss of constructibility as bad, but worse when applied to a generalized "proof of consistency" for all of mathematics. In his 1900 address Hilbert had specified, as the second of his 23 problems for the twentieth century, the quest for a generalized proof of (procedure for determining) the consistency of the axioms of arithmetic. Hilbert, unlike Brouwer, believed that the formalized notion of mathematical induction could be applied in the search for the generalized consistency proof.

If this proof/procedure P was found, given any arbitrary mathematical theorem T (formula, procedure, proof) put to P (thus P(T)) including P itself (thus P(P)), P would determine conclusively whether or not the theorem T (and P) was provable – i.e. derivable from its premises, the axioms of arithmetic. Thus for all T, T would be provable by P or not provable by P and under all conditions (i.e. for any assignment of numerical values to T's variables). This requires the use of the Law of Excluded Middle extended over the infinite, in fact extended twice – first over all theorems (formulas, procedures, proofs) and secondly for a given theorem, for all assignment of its variables. This point, missed by Hilbert, was first pointed out to him by Poincaré and later by Weyl in his 1927 comments on Hilbert's lecture: "For after all Hilbert, too, is not merely concerned with, say 0' or 0' ', but with any 0' ^... ', with an arbitrarily concretely given numeral. One may here stress the "concretely given"; on the other hand, it is just as essential that the contentual arguments in proof theory be carried out in hypothetical generality, on any proof, on any numeral. ... It seems to me that Hilbert's proof theory shows Poincaré to have been completely right on this point."^[16]

In his discussion preceding Weyl's 1927 comments, van Heijenoort explains that Hilbert insisted that he had addressed the issue of "whether a formula, taken as an axiom, leads to a contradiction, the question is whether a proof that leads to a contradiction can be presented to me".^[17]

"But [writes van Heijenoort] in a consistency proof the argument does not deal with one single specific formula; it has to be extended to all formulas. This is the point that Weyl has in mind ... ."^[17][18]

Given such a generalized proof, all mathematics could be replaced by an automaton consisting of two parts: (i) a formula-generator to create formulas one after the other, followed by (ii) the generalized consistency proof, which would yield "Yes – valid (i.e. provable)" or "No – not valid (not provable)" for each formula submitted to it (and every possible assignment of numbers to its variables). In other words: mathematics would cease as a creative enterprise and become a machine.^[19]

ヴァン・ヘイエノールトによるワイルの（1927）「ヒルベルトの数学の基礎に関する第2講義へのコメント」に先立つ解説の中で、ポアンカレはヒルベルト（1905）に「帰納法」には2種類あると指摘している。（1）直観的な動物論理による足が足に続くバージョンで、常に前の足の後に別の足があるという感覚を与えてくれるもの、そして（2）形式的なバージョン、例えばペアノのバージョン：記号の列である。^{[ 20 ]}ポアンカレ、ワイル、ブロウワーは、ヒルベルトが暗黙のうちに、そして不当に、形式的帰納法を前提の1つとして採用したと主張した。ポアンカレ（1905）は、そうすることでヒルベルトの推論は循環的になったと主張した。^{[ 21 ]}ワイル（1927）の同意とブロウワーの論争により、ヒルベルトとその弟子であるヘルブラント、ベルネイス、アッカーマンは最終的に「帰納」の概念を再検討せざるを得なくなった。つまり、「無限集合のすべての対象xの総体」という仮定を避け、（直観主義的に）一般的な議論がx を一つずつ無限に進んでいくと仮定することになった（ファン・ヘイエノールト p.  481、脚注 a）。これは実際には、当時まだ発展途上であった「再帰」の概念で使用されているいわゆる「帰納図式」である（ファン・ヘイエノールト p.  493）。^{[ 22 ]}この図式は「直観」から派生したものであったため、直観主義者にとって受け入れられるものであった。

この区別をさらに進めるために、クリーネ（1952/1977）は数学的帰納法を3つのタイプに区別している。（1）形式的帰納規則（ペアノの公理）、（2）帰納的定義（例：計数、「帰納による証明」）、（3）帰納による定義（数論的関数または述語の再帰的定義）。（3）に関して、クリーネは原始再帰関数を考察している。

「ある種の数論的関数と述語に関する直観的な理論...この理論では、メタ数学と同様に、有限な方法のみを使用します。」

自然数 0, 0', 0 ' ' , 0 ' ' ' , ...、または 0, 1, 2, 3, ... の系列は​​、1 つの基本オブジェクト 0 から 1 つの基本演算 ' または +1 によって生成されるオブジェクトのクラスとして記述されます。これは、自然数のクラスの帰納的定義を構成します。

Proof by induction ... corresponds immediately to this mode of generating the numbers. Definition by induction (not to be confused with 'inductive definition' ...) is the analogous method of defining a number-theoretic function φ(y) or predicate P(y). [A number-theoretic function or predicate takes as its variables only a selection from the natural numbers and produces only a single natural number in turn]. First φ(0) or P(0) (the value of the function or predicate for 0 as argument) is given. Then, for any natural number y, φ(y') or P(y') (the next value after that for y) is expressed in terms of y and φ(y) or P(y) (the value of y). ... The two parts of the definition enable us, as we generate any natural number y, at the same time to determine the value φ(y) or P(y)." (p. 217)

Brouwer's insistence on "constructibility" in the search for a "consistency proof for arithmetic" resulted in sensitivity to the issue as reflected by the work of Finsler and Gödel.^[23] Ultimately Gödel would "numeralize" his formulae; he then used primitive recursion (and its instantiation of the intuitive, constructive form of induction, i.e., counting and step-by-step evaluation) rather than a string of symbols that represent formal induction. Gödel was so sensitive to this issue that he took great pains in his 1931 paper to point out that his Theorem VI (the so-called "First incompleteness theorem") "is constructive;^45a that is, the following has been proved in an intuitionistically unobjectionable manner ... ." He then demonstrates what he believes to be the constructive nature of his "generalization formula" 17 Gen r. Footnote 45a reinforces his point.

Gödel's 1931 paper does include the formalist's symbol-version of the Peano Induction Axiom; it is presented as the following formula, where "." is the logical AND, f is the successor-sign, x₂ is a function, x₁ is a variable, x₁Π designates "for all values of variable x₁" and ${\displaystyle \supset }$ denotes implication:

${\displaystyle x_{2}(0).x_{1}\Pi (x_{2}(x_{1})\supset x_{2}(fx_{1}))\supset x_{1}\Pi (x_{2}(x_{1}))}$

He does not appear to use this in the formalist's sense, but there is some contention around this point. Gödel specifies this symbol string in his I.3.,^[24] i.e., the formalized inductive axiom appears as shown above – yet even this string can be "numeralized" using Gödel's method. On the other hand, he doesn't appear to use this axiom. Rather, his recursion steps through integers assigned to variable k (cf his (2) on page 602). His skeleton-proof of Theorem V, however, "use(s) induction on the degree of φ," and uses "the induction hypothesis." Without a full proof of this, the "induction hypothesis" could be assumed to be the intuitive version, not the symbolic axiom. His recursion simply steps up the degree of the functions, an intuitive act, ad infinitum. Gödel's proofs being intuitionistically satisfactory and infinitary are not incompatible truths, as long as the law of the excluded middle over the completed infinite isn't invoked anywhere in the proofs.

Despite the last-half-twentieth century's continued abstraction of mathematics,^[25] the issue has not entirely gone away. A hard look at the premises of Turing's 1936–1937 work led Robin Gandy (1980) to propose his "principles for mechanisms" that have speed of light as a constraint. As another example, Breger (2000) in his "Tacit Knowledge and Mathematical Progress" delves deeply into the matter of "semantics versus syntax" – in his paper Hilbert, Poincaré, Frege, and Weyl duly make their appearances. Breger asserts that axiomatic proofs assume an experienced, thinking mind. Specifically, he claims a mind must come to the argument equipped with prior knowledge of the symbols and their use (the semantics behind the mindless syntax): "Mathematics as a purely formal system of symbols without a human being possessing the know-how for dealing with the symbols is impossible [according to the chemist Polanyi (1969, 195), the ideal of a form of knowledge that is strictly explicit is contradictory because without tacit knowledge all formulas, words, and illustrations would become meaningless]" (brackets in the original, Breger 2000: 229).