5.3 KiB
| title | chunk | source | category | tags | date_saved | instance |
|---|---|---|---|---|---|---|
| Brouwer–Hilbert controversy | 3/5 | https://en.wikipedia.org/wiki/Brouwer–Hilbert_controversy | reference | science, encyclopedia | 2026-05-05T16:20:08.121681+00:00 | kb-cron |
=== Objections related to the law of the excluded middle and 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. Poincaré, Weyl, and Brouwer claimed that Hilbert tacitly, and unjustifiably, adopted formal induction as one of his premises. 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 (van Heijenoort 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); (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 functions:
"an intuitive theory about a certain class of number theoretic functions and predicates ... In this theory, as in metamathematics, we shall use only finitary methods. The series of the natural numbers 0, 0', 0'', 0''', ..., or 0, 1, 2, 3, ... we described as the class of the objects generated from one primitive object 0 by means of one primitive operation ' or +1. This constitutes an inductive definition of the class of the natural numbers.
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)
=== Echoes 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 Finsler and Gödel. 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, x2 is a function, x1 is a variable, x1Π designates "for all values of variable x1" and
⊃
{\displaystyle \supset }
denotes implication:
x
2
(
0
)
.
x
1
Π
(
x
2
(
x
1
)
⊃
x
2
(
f
x
1
)
)
⊃
x
1
Π
(
x
2
(
x
1
)
)
{\displaystyle x_{2}(0).x_{1}\Pi (x_{2}(x_{1})\supset x_{2}(fx_{1}))\supset x_{1}\Pi (x_{2}(x_{1}))}