Talk:Hilbert's second problem

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)[reply]

The current content of the article appears to be identical to Section 2.37 "Hilbert's second problem" in Unsolved Problems in Mathematics by Fredrick Kennard (2015). What's up? Whayes43 (talk) 17:01, 2 June 2015 (UTC)[reply]

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: "⁷In 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.³⁰ 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.

"³⁰Gentzen'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 e_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 e_o as a finitary method (Cf. end § 81.)

"Gentzen in 1938a speculates that the use of transfinite induction up to some ordinal greater than e_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 a, induction up to the least Cantor e-number greater than a cannot be reduced to induction up to a (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)[reply]

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)[reply]

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 integers⁴" "⁴This 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)[reply]

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)[reply]

Hilbert's finitism

Seeing the emphasis placed in this article prompted me to look over (Zach 2001) again. Zach's discussion of the origins of Hilbert's finitism states that the first appearance of finitistic ideas in Hilbert's ideas appeared in 1905, and the first fully fleshed-out account of finitism appeared in 1917. It looks implausible to claim that Hilbert's 2nd problem demands a finitistic consistency proof; rather this is what later commentators have read into the problem.

Richard Zach (2001). [http://www.ucalgary.ca/~rzach/static/hilbert.pdf Hilbert's Finitism: Historical, Philosophical, and Metamathematical Perspectives]. PhD dissertation, UC Berkeley.

I'm hesitant to work this point into the article, because I rather think that other editors will have differing views on the significance of this historical account. --- Charles Stewart(talk) 17:38, 25 February 2009 (UTC)[reply]

Arithmetic of natural numbers or of real numbers?

To CRGreathouse (talk · contribs) and David Eppstein (talk · contribs): I looked at the text of Hilbert's speech (both the English translation and the original German, as linked at the bottom of this article). It appears to me that Motomuku (talk · contribs) is correct. Hilbert was referring to the theory of the real numbers (including the natural numbers as a distinguished subset) rather than the theory of the natural numbers alone. JRSpriggs (talk) 23:42, 23 December 2009 (UTC)[reply]

However, this should be equivalent to applying higher-order logic to the natural numbers. JRSpriggs (talk) 23:47, 23 December 2009 (UTC)[reply]

It seems clear to me also that Hilbert was not talking about consistency of PA, as this article assumes. I don't currently have access to Franzen's book, which the article cites as backing up its interpretation - does he really do so?Mbays (talk) 14:41, 2 September 2012 (UTC)[reply]

Another relevant reference is Kreisel's article "What have we learnt from Hilbert's second problem?". On p. 94, Kreisel writes that Hilbert "had left open (i) exactly which axioms are to be considered, except that arithmetic was to include the theory of real numbers ...". The issue which can cause confusion is that Tarski's work on real closed fields was not known until the 1950s, but I have not seen anyone claim that this gave a positive answer to Hilbert's second problem. Instead, people generally seem to view the problem as requiring "at least" a proof of the consistency of PA, and possibly requiring the proof of a stronger theory, so that the incompleteness theorems apply. (Of course we know now that ACA₀ is arithmetically conservative over PA and includes all the usual facts about the arithmetic of the reals, so a proof of the consistency of PA would go farther than it might seem). Kreisel on pp. 93-94 argues that the statement of the second problem had "serious ambiguities" whose clarification led to Hilbert's program. — Carl (CBM · talk) 21:16, 2 September 2012 (UTC)[reply]

I checked the Franzen reference, and he does not back up the article's interpretation. I am correspondingly deleting the reference to Franzen, and inserting a crucial "in particular". I'll leave any further reworking of the article to those more familiar with it, but it now seems not to be misleading. Mbays (talk) 14:28, 6 September 2012 (UTC)[reply]

Yes, surely Hilbert was not considering Peano Arithmetic (perhaps not even defined, at the time!), but at least some theory of the real numbers (at the end he even mentions "Cantor’s higher classes of numbers and cardinal numbers"). Hence a large part of the article is not relevant to the Second Problem. However (at a very first reading) the article seems quite accurate; could we create an article about Peano Arithmetic and move the material there? Probably Hilbert would not have considered Gentzen proof as finitistic; anyway, the main point is that Gentzen result deals with a very weak theory, and analogue results for, say, second order arithmetic seem unreachable, with our present methods [1].

By the way, a problem about considering Gödel 2nd incompleteness as a negative solution is that the theorem actually depends on the exact formulation of the sentence which is said to "assert consistency". For example, details can be found in [2], [3]. Paolo Lipparini (talk) 18:55, 11 October 2015 (UTC)[reply]

proof theoretic ordinal

"Gentzen's proof shows that a theory will be able to prove the consistency of arithmetic if and only if its proof theoretic ordinal is larger than e0."

Is the "only if" part really right? What is the proof theoretic ordinal of a theory whose only axiom is CON(PA)? Heck, it could even additionally assert the falsehood of PA. 66.127.55.192 (talk) 08:10, 19 February 2010 (UTC)[reply]

Yes, that material was wrong. Actually the ordinal of PA + Con(PA) is the same as the ordinal of PA. — Carl (CBM · talk) 12:31, 19 February 2010 (UTC)[reply]

Yes. But, I doubt that it makes sense to talk about the proof theoretic ordinal of a theory which is not true like PA + ¬con(PA) even though it is consistent. JRSpriggs (talk) 16:29, 19 February 2010 (UTC)[reply]

Huang’s Hilbert logic and his universal consistent theorem

I have removed this material since it appears to be sourced only to one person. It may be WP:FRINGE, it seems WP:UNDUE, there may be WP:COI and/or WP:OR issues. Mention in independent reliable sources is needed. Deltahedron (talk) 06:42, 1 October 2012 (UTC)[reply]

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Hilbert's second problem. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

Added archive https://web.archive.org/web/20060705205103/http://home.ddc.net/ygg/etext/godel/ to http://home.ddc.net/ygg/etext/godel/

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 5 June 2024).

If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 22:31, 3 November 2017 (UTC)[reply]