Brouwer–Hilbert controversy
Encyclopedia
In a foundational controversy in twentieth-century mathematics
, L. E. J. Brouwer, a supporter of intuitionism
, opposed David Hilbert
, the founder of formalism
.
's axiomatization of geometry in the late 1890s. In his biography of Kurt Gödel
, John W. Dawson, Jr
summarizes the result as follows:
Dawson observes that "partisans of three principal philosophical positions took part in the debate" (ibid) – the logicists (Gottlob Frege
and Bertrand Russell
), the formalists (David Hilbert
and his "school" of collaborators), and the constructivists (Henri Poincaré
and Hermann Weyl
); within this constructivist school was the radical self-named "intuitionist" L.E.J. Brouwer.
The following sections will expand these disputes noted by Dawson.
as a challenge to the then-prevailing formalism
of David Hilbert and his collaborators Paul Bernays
, Wilhelm Ackermann
, John von Neumann
and others (cf. Kleene (1952), pp. 46–59). As a variety of constructive mathematics, intuitionism is essentially a philosophy of the foundations of mathematics
. It is sometimes and rather simplistically characterized by saying that its adherents refuse to use the law of excluded middle
in mathematical reasoning.
In 1908:
"After completing his dissertation (1907: see Van Dalen), Brouwer made a conscious decision temporarily to keep his contentious ideas under wraps and to concentrate on demonstrating his mathematical prowess" (Davis (2000), p. 95); by 1910 he had published a number of important papers, in particular the Fixed Point Theorem
. Hilbert – the formalist with whom the intuitionist Brouwer would ultimately spend years in conflict – admired the young man and helped him receive a regular academic appointment (1912) at the University of Amsterdam (Davis, p. 96). It was then that "Brouwer felt free to return to his revolutionary project which he was now calling intuitionism " (ibid).
In the later 1920s, Brouwer became involved in a public and demeaning controversy with Hilbert over editorial policy at Mathematische Annalen
, at that time a leading learned journal. He became relatively isolated; the development of intuitionism at its source was taken up by his student Arend Heyting
.
Not all were convinced. While Kronecker would die soon after, his constructivist
banner would be carried forward by sharp criticism from Poincaré, and later in full cry by the young Brouwer
and his developing intuitionist "school"—Weyl in particular, much to Hilbert's torment in his later years (Reid 1996, pp. 148–149). Indeed Hilbert lost his "gifted pupil" Weyl to intuitionism:
Brouwer the intuitionist in particular objected to the use of the Law of Excluded Middle over infinite sets (as Hilbert had indeed used it). Hilbert would respond:
But then Hilbert gets to the nut of it – the proscription of the Law of Excluded Middle
(LoEM):
To doubt the LoEM—when extended over the completed infinite—was to doubt Hilbert's axiomatic system, in particular his "logical ε-axiom". To take away the LoEM was to destroy the "science of mathematics." Finally, Hilbert singles out one man—by inference, not by name—for the cause of his present tribulation:
Brouwer answers pique with pique:
Hilbert's axiomatic system – his formalism – is different. At the outset it declares its axioms. But he doesn't require the selection of these axioms to be based upon either "common sense", a priori knowledge (intuitively derived understanding or awareness, innate knowledge seen as "truth without requiring any proof from experience" ), or observational experience (empirical data). Rather, the mathematician in the same manner as the theoretical physicist is free to adopt any (arbitrary, abstract) collection of axioms that they so choose. Indeed Weyl asserts that Hilbert had "formaliz[ed] it [classical mathematics], thus transforming it in principle from a system of intuitive results into a game with formulas that proceeds according to fixed rules" (loc cit p. 483). So, Weyl asks, what might guide the choice of these rules? "What impels us to take as a basis precisely the particular axiom system developed by Hilbert?" (ibid). Weyl offers up "consistency is indeed a necessary but not sufficient condition" but he cannot answer more completely except to note that Hilbert's "construction" is "arbitrary and bold" (ibid). Finally he notes, in italics, that the philosophical result of Hilbert's "construction" will be the following:
In other words: the role of innate feelings and tendencies (intuition) and observational experience (empiricism) in the choice of axioms will be removed except in the global sense – the "construction" had better work when put to the test: "only the theoretical system as a whole ... can be confronted with experience" (ibid).
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 – see more below. 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". In the late 1890s Hilbert successfully axiomatized geometry. Then he went on to successfully (or so Hilbert thought) use the Cantorian-inspired notion of the completed infinity to produce elegant, radically abbreviated proofs in analysis (1896 and afterwards). In his own words of defense Hilbert believed himself quite justified in what he had done (in the following he calls this type of proof an existence proof):
What Hilbert had to give up was "constructability" – 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.
A consequence of this marvelous proof/procedure P would be the following: 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 is a perfect illustration of 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:
In his discussion before Weyl's 1927 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" (loc cit, p. 481).
If successful the quest would result in a remarkable outcome: 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.
To carry this distinction further, Kleene 1952/1977 distinguishes between three types of mathematical induction – (1) the formal Induction Rule (Peano's axiom, see the next section for an example), (2) the inductive definition (examples: counting, "Proof by induction"), and (3) the definition by induction (recursive definition of "number-theoretic functions or predicates). With regards to (3), Kleene considers primitive recursive function
s:
and Gödel. Ultimately Gödel would "numeralize" his formulae; Gödel 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 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 does include the formalist's symbol-version of the Peano Induction Axiom; it looks like this, where "." is the logical AND, f is the successor-sign, x2 is a function, x1 is a variable, x1Π designates "for all values of variable x1":
But he does not appear to use this in the formalist's sense.
Note that there is contention around this point. Gödel specifies this symbol string in his I.3. (p. 600 in van Heijenoort), 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, we are left to assume that his use of the "induction hypothesis" is the intuitive version, not the symbolic axiom. His recursion simply steps up the degree of the functions, an intuitive act, ad infinitum. But Nagel and Newman note that Gödel's proofs are infinitary in nature (cf Nagel and Newman p. 98), not finitary as Hilbert requested (see Hilbert's second problem
) while Gödel insisted that they are intuitionistically satisfactory. These are not incompatible truths, as long as the LoEM over the infinite isn't invoked anywhere in the proofs.
Despite the last-half-twentieth century's continued abstraction of mathematics, the issue has not entirely gone away. Here are two examples. First, the premises of an argument – even ones considered beyond questioning – are always fair game. A hard look at the premises of Turing's 1936–7 led Robin Gandy (1980) to propose his "principles for mechanisms" that throw in the speed of light as a constraint. Secondly, 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. He examines a core problem: in axiomatic proofs the tacit assumption of an experienced, thinking mind: to be successful it 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).
History of mathematics
The area of study known as the history of mathematics is primarily an investigation into the origin of discoveries in mathematics and, to a lesser extent, an investigation into the mathematical methods and notation of the past....
, L. E. J. Brouwer, a supporter of intuitionism
Intuitionism
In the philosophy of mathematics, intuitionism, or neointuitionism , is an approach to mathematics as the constructive mental activity of humans. That is, mathematics does not consist of analytic activities wherein deep properties of existence are revealed and applied...
, opposed David Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
, the founder of formalism
Formalism (mathematics)
In foundations of mathematics, philosophy of mathematics, and philosophy of logic, formalism is a theory that holds that statements of mathematics and logic can be thought of as statements about the consequences of certain string manipulation rules....
.
Background
The background for the controversy was set with David HilbertDavid Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
's axiomatization of geometry in the late 1890s. In his biography of Kurt Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
, John W. Dawson, Jr
John W. Dawson, Jr
John W. Dawson, Jr. is Professor of Mathematics, Emeritus at Pennsylvania State University at York. Born in Wichita, Kansas, he attended M.I.T. as a National Merit Scholar before earning a doctorate in mathematical logic from the University of Michigan in 1972...
summarizes the result as follows:
- "At issue in the sometimes bitter disputes was the relation of mathematics to logic, as well as fundamental questions of methodology, such as how quantifiers were to be construed, to what extent, if at all, nonconstructive methods were justified, and whether there were important connections to be made between syntactic and semantic notions." (Dawson 1997:48)
Dawson observes that "partisans of three principal philosophical positions took part in the debate" (ibid) – the logicists (Gottlob Frege
Gottlob Frege
Friedrich Ludwig Gottlob Frege was a German mathematician, logician and philosopher. He is considered to be one of the founders of modern logic, and made major contributions to the foundations of mathematics. He is generally considered to be the father of analytic philosophy, for his writings on...
and Bertrand Russell
Bertrand Russell
Bertrand Arthur William Russell, 3rd Earl Russell, OM, FRS was a British philosopher, logician, mathematician, historian, and social critic. At various points in his life he considered himself a liberal, a socialist, and a pacifist, but he also admitted that he had never been any of these things...
), the formalists (David Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
and his "school" of collaborators), and the constructivists (Henri Poincaré
Henri Poincaré
Jules Henri Poincaré was a French mathematician, theoretical physicist, engineer, and a philosopher of science...
and Hermann Weyl
Hermann Weyl
Hermann Klaus Hugo Weyl was a German mathematician and theoretical physicist. Although much of his working life was spent in Zürich, Switzerland and then Princeton, he is associated with the University of Göttingen tradition of mathematics, represented by David Hilbert and Hermann Minkowski.His...
); within this constructivist school was the radical self-named "intuitionist" L.E.J. Brouwer.
The following sections will expand these disputes noted by Dawson.
Brief history of Brouwer and Intuitionism
Brouwer in effect founded the mathematical philosophy of intuitionismIntuitionism
In the philosophy of mathematics, intuitionism, or neointuitionism , is an approach to mathematics as the constructive mental activity of humans. That is, mathematics does not consist of analytic activities wherein deep properties of existence are revealed and applied...
as a challenge to the then-prevailing formalism
Formalism (mathematics)
In foundations of mathematics, philosophy of mathematics, and philosophy of logic, formalism is a theory that holds that statements of mathematics and logic can be thought of as statements about the consequences of certain string manipulation rules....
of David Hilbert and his collaborators Paul Bernays
Paul Bernays
Paul Isaac Bernays was a Swiss mathematician, who made significant contributions to mathematical logic, axiomatic set theory, and the philosophy of mathematics. He was an assistant to, and close collaborator of, David Hilbert.-Biography:Bernays spent his childhood in Berlin. Bernays attended the...
, Wilhelm Ackermann
Wilhelm Ackermann
Wilhelm Friedrich Ackermann was a German mathematician best known for the Ackermann function, an important example in the theory of computation....
, John von Neumann
John von Neumann
John von Neumann was a Hungarian-American mathematician and polymath who made major contributions to a vast number of fields, including set theory, functional analysis, quantum mechanics, ergodic theory, geometry, fluid dynamics, economics and game theory, computer science, numerical analysis,...
and others (cf. Kleene (1952), pp. 46–59). As a variety of constructive mathematics, intuitionism is essentially a philosophy of the foundations of mathematics
Foundations of mathematics
Foundations of mathematics is a term sometimes used for certain fields of mathematics, such as mathematical logic, axiomatic set theory, proof theory, model theory, type theory and recursion theory...
. It is sometimes and rather simplistically characterized by saying that its adherents refuse to use the law of excluded middle
Law of excluded middle
In logic, the law of excluded middle is the third of the so-called three classic laws of thought. It states that for any proposition, either that proposition is true, or its negation is....
in mathematical reasoning.
In 1908:
- "... Brouwer, in a paper entitled "The untrustworthiness of the principles of logic", challenged the belief that the rules of the classical logic, which have come down to us essentially from Aristotle (384–322 B.C.) have an absolute validity, independent of the subject matter to which they are applied" (Kleene (1952), p. 46).
"After completing his dissertation (1907: see Van Dalen), Brouwer made a conscious decision temporarily to keep his contentious ideas under wraps and to concentrate on demonstrating his mathematical prowess" (Davis (2000), p. 95); by 1910 he had published a number of important papers, in particular the Fixed Point Theorem
Brouwer fixed point theorem
Brouwer's fixed-point theorem is a fixed-point theorem in topology, named after Luitzen Brouwer. It states that for any continuous function f with certain properties there is a point x0 such that f = x0. The simplest form of Brouwer's theorem is for continuous functions f from a disk D to...
. Hilbert – the formalist with whom the intuitionist Brouwer would ultimately spend years in conflict – admired the young man and helped him receive a regular academic appointment (1912) at the University of Amsterdam (Davis, p. 96). It was then that "Brouwer felt free to return to his revolutionary project which he was now calling intuitionism " (ibid).
In the later 1920s, Brouwer became involved in a public and demeaning controversy with Hilbert over editorial policy at Mathematische Annalen
Mathematische Annalen
Mathematische Annalen is a German mathematical research journal founded in 1868 by Alfred Clebsch and Carl Neumann...
, at that time a leading learned journal. He became relatively isolated; the development of intuitionism at its source was taken up by his student Arend Heyting
Arend Heyting
Arend Heyting was a Dutch mathematician and logician. He was a student of Luitzen Egbertus Jan Brouwer at the University of Amsterdam, and did much to put intuitionistic logic on a footing where it could become part of mathematical logic...
.
Origins of disagreement
The nature of Hilbert's proof of the Hilbert basis theorem (dating from 1888) turned out to be more controversial than Hilbert could have imagined at the time. Although Kronecker 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 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". (Reid 1996, p. 37.)
Not all were convinced. While Kronecker would die soon after, his constructivist
Constructivism (mathematics)
In the philosophy of mathematics, constructivism asserts that it is necessary to find a mathematical object to prove that it exists. When one assumes that an object does not exist and derives a contradiction from that assumption, one still has not found the object and therefore not proved its...
banner would be carried forward by sharp criticism from Poincaré, and later in full cry by the young Brouwer
Luitzen Egbertus Jan Brouwer
Luitzen Egbertus Jan Brouwer FRS , usually cited as L. E. J. Brouwer but known to his friends as Bertus, was a Dutch mathematician and philosopher, a graduate of the University of Amsterdam, who worked in topology, set theory, measure theory and complex analysis.-Biography:Early in his career,...
and his developing intuitionist "school"—Weyl in particular, much to Hilbert's torment in his later years (Reid 1996, pp. 148–149). Indeed Hilbert lost his "gifted pupil" Weyl to intuitionism:
- "Hilbert was disturbed by his former student's fascination with the ideas of Brouwer, which aroused in Hilbert the memory of Kronecker". (Reid 1996, p. 148.)
Brouwer the intuitionist in particular objected to the use of the Law of Excluded Middle over infinite sets (as Hilbert had indeed used it). Hilbert would respond:
-
- " 'Taking the Principle of the Excluded Middle from the mathematician ... is the same as ... prohibiting the boxer the use of his fists.'
- "The possible loss did not seem to bother Weyl." (Reid 1996, p. 150.)
Validity of Law of excluded middle
In the same paper – the text of an address delivered in 1927 (cf van Heijenoort: Hilbert (1927)) – Hilbert clearly expresses himself. At first he attempts to defend his axiomatic system as having "important general philosophical significance" (van Heijenoort: Hilbert 1927 p. 475). For him, the statement of "definite rules" expresses "the technique of our thinking". Nothing is hidden, no tacit assumptions are admitted: "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." (ibid).But then Hilbert gets to the nut of it – the proscription of the Law of Excluded Middle
Law of excluded middle
In logic, the law of excluded middle is the third of the so-called three classic laws of thought. It states that for any proposition, either that proposition is true, or its negation is....
(LoEM):
- "Intuitionism's sharpest and most passionate challenge is the one it flings at the validity of the principle of excluded middle ..." (ibid)
To doubt the LoEM—when extended over the completed infinite—was to doubt Hilbert's axiomatic system, in particular his "logical ε-axiom". To take away the LoEM was to destroy the "science of mathematics." Finally, Hilbert singles out one man—by inference, not by name—for 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." (loc cit p. 476)
Brouwer answers pique with pique:
- "...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." (van Heijenoort: Brouwer 1927b published in 1928, p. 492)
A philosophical defeat in the quest for "truth" in the choice of axioms
However "truth" is ultimately defined, for a few mathematicians Hilbert's formalism seemed to eschew the notion. And at least with respect to his choice of axioms the case can be made that indeed he does eschew the notion. The fundamental issue is just how does one choose "the axioms"? Until Hilbert proposed his formalism, the axioms were chosen on an "intuitive" (experiential) basis. Aristotelian logic is a good example – based on one's life-experiences it just seems "logical" that an object of discourse 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 Excluded Middle). The primitive form of the induction axiom is another – if a predicate P(n) is true for n = 0 and if for all natural numbers n it is true that P(n) => P(n+1), then P(n) is true for all natural numbers n.Hilbert's axiomatic system – his formalism – is different. At the outset it declares its axioms. But he doesn't require the selection of these axioms to be based upon either "common sense", a priori knowledge (intuitively derived understanding or awareness, innate knowledge seen as "truth without requiring any proof from experience" ), or observational experience (empirical data). Rather, the mathematician in the same manner as the theoretical physicist is free to adopt any (arbitrary, abstract) collection of axioms that they so choose. Indeed Weyl asserts that Hilbert had "formaliz[ed] it [classical mathematics], thus transforming it in principle from a system of intuitive results into a game with formulas that proceeds according to fixed rules" (loc cit p. 483). So, Weyl asks, what might guide the choice of these rules? "What impels us to take as a basis precisely the particular axiom system developed by Hilbert?" (ibid). Weyl offers up "consistency is indeed a necessary but not sufficient condition" but he cannot answer more completely except to note that Hilbert's "construction" is "arbitrary and bold" (ibid). Finally he notes, in italics, that the philosophical result of Hilbert's "construction" will be the following:
- "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." (ibid)
In other words: the role of innate feelings and tendencies (intuition) and observational experience (empiricism) in the choice of axioms will be removed except in the global sense – the "construction" had better work when put to the test: "only the theoretical system as a whole ... can be confronted with experience" (ibid).
The law of excluded middle extended to the infinite
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 ℵ0 (aleph-null). Hilbert's adoption of the notion wholesale was "thoughtless", Brouwer believed. 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" (van Heijenoort, p. 491).
This THIRD INSIGHT is referring to Hilbert's second problem
Hilbert's second problem
In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his 23 problems. It asks for a proof that arithmetic is consistent – free of any internal contradictions....
and Hilbert's ongoing attempt to axiomatize all of arithmetic, and with this system, to discover a "consistency proof" for all of mathematics – see more below. 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". In the late 1890s Hilbert successfully axiomatized geometry. Then he went on to successfully (or so Hilbert thought) use the Cantorian-inspired notion of the completed infinity to produce elegant, radically abbreviated proofs in analysis (1896 and afterwards). In his own words of defense Hilbert believed himself quite 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 constructability. 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 and formulated by Weierstrass and Dedekind."(loc cit p. 474)
- "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 on 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." (loc cit p. 475)
What Hilbert had to give up was "constructability" – 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
Reductio ad absurdum
In logic, proof by contradiction is a form of proof that establishes the truth or validity of a proposition by showing that the proposition's being false would imply a contradiction...
extended over the infinite.
Hilbert's quest for a generalized proof of consistency of the axioms of arithmetic
Brouwer viewed this loss of constructability 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.A consequence of this marvelous proof/procedure P would be the following: 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 is a perfect illustration of 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:
- "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." (Weyl 1927, van Heijenoort p. 483)
In his discussion before Weyl's 1927 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" (loc cit, p. 481).
- "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 ..." (ibid).
If successful the quest would result in a remarkable outcome: 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.
The problem of the law of excluded middle with respect to induction
In van Heijenoort's commentary preceding Weyl's (1927) "Comments on Hilbert's second lecture on the foundations of mathematics" Poincaré points out to Hilbert (1905) that there are two types of "induction" (1) the intuitive animal-logic foot-following-foot version that gives us a sense that there's always another footstep after the last footstep, and (2) the formal version – e.g. Peano's version: a string of symbols. The gang of three – Poincaré, Weyl and Brouwer – claimed that Hilbert tacitly, and unjustifiably, adopted as one of his premises formal induction (the symbol string). Poincaré (1905) asserted that, by doing this, Hilbert's reasoning became circular. Weyl's (1927) agreement and Brouwer's polemics ultimately forced Hilbert and his disciples Herbrand, Bernays and Ackermann to reexamine their notion of "induction" – to eschew the assumption of a "totality of all the objects x of an infinite collection" and (intuitionistically) assume that the general argument proceeds one x after another, ad infinitum (van Heijenoort p. 481, footnote a). This is in fact the so-called "induction schema" used in the notion of "recursion" that was still in development at this time (cf van H. p. 493) – this schema was acceptable to the intuitionists because it had been derived from "the intuition".To carry this distinction further, Kleene 1952/1977 distinguishes between three types of mathematical induction – (1) the formal Induction Rule (Peano's axiom, see the next section for an example), (2) the inductive definition (examples: counting, "Proof by induction"), and (3) the definition by induction (recursive definition of "number-theoretic functions or predicates). With regards to (3), Kleene considers primitive recursive function
Primitive recursive function
The primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the total µ-recursive functions...
s:
Echos of the controversy
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 FinslerPaul Finsler
Paul Finsler was a German and Swiss mathematician.Finsler did his undergraduate studies at the Technische Hochschule Stuttgart, and his graduate studies at the University of Göttingen, where he received his Ph.D. in 1919 under the supervision of Constantin Carathéodory...
and Gödel. Ultimately Gödel would "numeralize" his formulae; Gödel 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 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 does include the formalist's symbol-version of the Peano Induction Axiom; it looks like this, where "." is the logical AND, f is the successor-sign, x2 is a function, x1 is a variable, x1Π designates "for all values of variable x1":
- (x2(0).x1Π(x2(x1)⊃x2(fx1))⊃x1Π(x2(x1))
But he does not appear to use this in the formalist's sense.
Note that there is contention around this point. Gödel specifies this symbol string in his I.3. (p. 600 in van Heijenoort), 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, we are left to assume that his use of the "induction hypothesis" is the intuitive version, not the symbolic axiom. His recursion simply steps up the degree of the functions, an intuitive act, ad infinitum. But Nagel and Newman note that Gödel's proofs are infinitary in nature (cf Nagel and Newman p. 98), not finitary as Hilbert requested (see Hilbert's second problem
Hilbert's second problem
In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his 23 problems. It asks for a proof that arithmetic is consistent – free of any internal contradictions....
) while Gödel insisted that they are intuitionistically satisfactory. These are not incompatible truths, as long as the LoEM over the infinite isn't invoked anywhere in the proofs.
Despite the last-half-twentieth century's continued abstraction of mathematics, the issue has not entirely gone away. Here are two examples. First, the premises of an argument – even ones considered beyond questioning – are always fair game. A hard look at the premises of Turing's 1936–7 led Robin Gandy (1980) to propose his "principles for mechanisms" that throw in the speed of light as a constraint. Secondly, 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. He examines a core problem: in axiomatic proofs the tacit assumption of an experienced, thinking mind: to be successful it 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).