Talk:Hilbert's second problem

From Wikipedia, the free encyclopedia

[edit] Created article

There are several, and it should be easy to find sources for all of them:

  • Godel shows PA cannot prove its own consistency
  • Gentzen showed that PRA together with an induction principle is able to prove the consistency of PA
  • Some people believe that Godel's proof shows that no reasonable solution to the 2nd question is possible; this resolves the question by showing it is impossible to achieve finitistically
  • Some people believe that Gentzen's proof gives a positive answer to Hilbert's question, because they don't object to the transfinite induction principle
  • Some people believe that the second problem has not been answered, but hold out the possibility that a proof using new techniques may one day be obtained
  • Some people feel the problem is meaningless because we no longer doubt the consistency of arithmetic.

Feel free to add more issues to the list. CMummert 17:11, 6 January 2007 (UTC)

[edit] Quotations around the notion of "finitary methods"

The following is from Reid (1996 p. 156). Reid's biography is marred by lack of references -- apparently she got her information from letters, published papers, and from talking to mathematicians alive at the time of the first edition (1965). She is the sister of (Julia?) Robinson the mathematician -- a contemporary of Martin Davis, Stephen Kleene etc. Her's is the only biography re Hilbert. This is what she has to say with reference to a talk in 1922 in Hamburg, where he criticized intuitionism re his former student Weyl the convert to the dark side of Brouwer's intuitionism, etc.:

"He proposed to formalize mathematics into a system in which the objects of the system -- the mathematical theorems and their proofs -- were expressed in the language of symbolic logic as sentences which have a logical structure but no content. These objects of the formal system would be chosen in such a way as to represent faithfully mathematical theory as far as the totality of theorems was concerned. The consistency of the formal system -- that is, mathematics -- would then be established by what Hilbert called finitary methods. 'Finitary' was defined as meaning that "the discussion, assertion or definition in question is kept within the boundaries of thorough-going producibility of objects and thorough-going practicality of methods and may be accordingly be carried out within the domain of concrete inspection." (p. 156)

Goldstein 2005 defines finitary systems in a footnote on page 144: "7In speaking of formal systems so far in this book, we've been speaking of finitary formal systems only, i.e. formal systems with a finite or denumerable (or countable) alphabet of symbols, wffs of finite length, and rules of inference involving only finitely many premises. (Logicians also work with formal systems with uncountable alphabets, with infinitely long wffs, and with proofs having finitely many premises).

The quote from Nagel and Newman that disavows Gentzen's proof as a finitary proof:

"Meta-mathematical proofs of the consistency of arithmetic have, in fact, been constructed, notably by Gerhard Gentzen, a member of the Hilbert school, in 1936, and by others since then.30 These proofs are of great logical significance, among other reasons because they propose new forms of meta-mathematical constructions, and because they thereby help make clear how the class of rules of inference needs to be enlarged if the consistency of arithmetic is to be established. But these proofs cannot be represented within the arithmetical calculus; and, since they are not finitistic, they do not achieve the proclaimed objectives of Hilbert's original program.
"30Gentzen's proof depends on arranging all the demonstrations of arithmetic in a linear order according to their degree of 'simplicity.' This arrangement turns out to have a pattern that is of a certain 'transfinite ordinal' type. (The theory of transfinite ordinal numbers was created by the German mathematician Georg Cantor in the nineteenth century). The proof of consistency is obtained by applying to this linear order a rule of inference known as "the principle of transfinite induction." Gentzen's argument cannot be mapped onto the formalism of arithmetic. Moreover, although most students do not question the cogency of the proof, it is not finitistic in the sense of Hilbert's original stipulations for an absolute proof of consistency." (p. 97)

Definition of finitary method from Kleene (1952, 1971) in the chapter 15 called Formalization of a theory". In this the use of "intuitively" means, as noted in the page before "The metatheory belongs to intuitive and informal mathematics... [it] will be expressed in ordinary language":

"The methods used in the metatheory shall be restricted to methods, called finitary by the formalists, which employ only intuitively conceivable objects and performable processes. (We translate the German "finit" as "finitary", since the English "finite" is used for the German "endlich".) No finite class may be regarded as a completed whole. Proofs of existence shall give, at least implicitly, a method for constructing the object which is being proved to exist. (Cf. § 13.)
"This restriction is requisite for the purpose for which Hilbert introduces metamathematics.... The finitary methods are of sorts used in intuitionistic elementary number theory. Some formalists attempt to circumscribe them still more narrowly (Hilbert and Bernays 1943 p. 43, and Bernays 1935, 1938)." (p. 63)
"The original proposals of the formalists to make classical mathematics secure by a consistency proof (§§ 14, 15) did not contemplate that such a method as transfinite induction up to εo would have to be used. To what extent the Gentzen proof can be accepted as securing classical number theory in the sense of that problem formulation is in the present state of affairs [1952, presumably] a matter for individual judgment, depending on how ready one is to accept induction up to εo as a finitary method (Cf. end § 81.)
"Gentzen in 1938a speculates that the use of transfinite induction up to some ordinal greater than εo may enable the consistency of analysis to be proved. By a result of Schutte 1951, stronger forms of induction are obtainable thus; in fact for any ordinal α, induction up to the least Cantor ε-number greater than α cannot be reduced to induction up to α (but induction up to any intermediate ordinal can be)." (p. 479)

Franzen's book is of intermediate difficulty, about the same as Nagel and Newman:

Torkel Franzen, 2005, Godel's theorem: An Incomplete Guide to its Use and Abuse", A.K. Peters, Wellesley MA, no ISBN.
"The Second Incompleteness Theorem and Hilbert's Program
"The second incompleteness theorem had profound consequences for the ideas concerning the foundations of mathematics put forward by David Hilbert, who had the goal of proving the consistency of mathematics by finitistic reasoning. What he wanted to do was to formulate formal systems within which all of ordinary mathematics could be carried out, including the mathematics of infinite sets, and to prove the consistency of these systems using only the most basic and concrete mathematical reasoning. In this sense, Hilbert intended his consistency proof to be conclusive: the consistency of, say, ZFC is proved using only reasoning of a kind that we cannot do without in science or mathematics.
"Although Hilbert did not formally specify what methods were allowed in finitistic reasoning, it seems clear that the methods Hilbert had in mind can be formalized in systems of arithmetic such as PA. And if PA cannot prove its own consistency, it follows that not even the consistency of elementary arithmetic can be proved using finitistic reasoning, so that Hilbert's program cannot be carried out (and that the finitistic consistency proof for arithmetic that Hilbert thought at the time had already been achieved, by his student and collaborator Wilhelm Ackermann, must be incorrect, as indeed it turned out to be).
"It is often said that the incompleteness theorem demolished Hilbert's program, but this was not the view of Godel himself. Rather, it showed that the means by which acceptable consistency proofs could be carried out had to be extended. Godel's own 'Dialectica interpretation,' which he developed in the early 1940s ad which was published in the journal Dialectica in 1958, gave one way of extending the notion of finitistic proof."

wvbaileyWvbailey 20:11, 12 January 2007 (UTC)

Since this article already has several long quotes, I think it would be better to prune these down to their essence, or paraphrase them, rather than adding them to the article whole. The Kleene quote is quite old, so I would prefer not to call it a "modern" opinion. We don't need to define "finitistic" here; there is a wikilink to the article finitism to handle that, so the quote by Goldstein probably is not necessary. CMummert · talk 20:49, 12 January 2007 (UTC)
Yes I agree, I am just trying to get them all in one safe place so I can look at them. The gist of the issue in the literature I quote here revolves around what the meaning of "finistic" was to Hilbert, not to us. The consensus of everything I've read is -- and the quotes above -- that Godel's proof, plus the follow-on work of Kleene and Turing, showed that a finitistic proof of the consistency of arithmetic (ZF + PM) was not possible because certain results are "undecidable within the system": to quote Godel (1931) "relatively simple problems in the theory of integers4" "4This is more precisely, there are undecidable propositions in which, besides the logical constants ~ (not), V (or), (x) (for all), and = (identical with),no others occur but + (addition) and . (multiplication), both for natural numbers, and in which the prefixes (x) apply to natural numbers only) -- ... cannot be decided on the basis of the axioms. Thus the matter of the consistency of arithmetic within ZF + PM -- is in the Hilbertian sense -- not decidable. And to append on more axioms means an infinite number are required. Even Godel uses the word "finite" in his footnote 5. I have yet to read anywhere except the writers on wiki who never quote their sources, that the matter was settled by Gentzen's proof or by any others. But on the other hand, Franzen's book is extremely new, and I don't understand his opinion (on p. 38) re Gentzen -- he throws out the phrase "Goldbach-like statements." Perhaps you know why the matter continues to be held as "open to debate". If you know of some sources let me know, because I am really curious. Thanks, wvbaileyWvbailey 21:35, 12 January 2007 (UTC)
The quote by Franzen is relevant to the sentence saying that Hlibert's problem is nowadays interpreted as asking about PA. The part about the Dialectica interpretation is interesting because the current article already alludes to it and lists it as a reference. Unfortunately the Dialectica interpretation of arithmetic is quite complicated and so it can't be presented here in any reasonable way. The last part of Franzen's quote is not so clear to me right now. Franzen's claim that PA includes all finitistic reasoning is (emphatically) not universally accepted; I have included references already that dispute it. Personally, I tend to agree with Franzen about it - I would say that primitive recursive arithmetic is, for all practical purposes, the formal counterpart of "finitistic" reasoning. CMummert · talk 04:48, 13 January 2007 (UTC)