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 of real numbers is consistent.

In the 1930s, Kurt Gödel and Gerhard Gentzen proved results that cast new light on the problem. Some feel that these results resolved the problem, while others feel that the problem is still open.

Hilbert's problem and its interpretation

In one English translation, Hilbert asks::"When we are engaged in investigating the foundations of a science, we must set up a system of axioms which contains an exact and complete description of the relations subsisting between the elementary ideas of that science. ... But above all I wish to designate the following as the most important among the numerous questions which can be asked with regard to the axioms: To prove that they are not contradictory, that is, that a definite number of logical steps based upon them can never lead to contradictory results. In geometry, the proof of the compatibility of the axioms can be effected by constructing a suitable field of numbers, such that analogous relations between the numbers of this field correspond to the geometrical axioms. ... On the other hand a direct method is needed for the proof of the compatibility of the arithmetical axioms." [From the English translation by M. Newson, 1902 provided by http://aleph0.clarku.edu/~djoyce/hilbert/problems.html .] It is now common to interpret Hilbert's second question to ask for a proof that the Peano arithmetic is consistent (Franzen 2005:p. 39).

There are many known proofs that Peano arithmetic is consistent that can be carried out in strong systems such as Zermelo-Frankel set theory. These do not provide a resolution to Hilbert's second question, however, because someone who doubts the consistency of Peano arithmetic is unlikely to accept the axioms of set theory (which is much stronger) to prove its consistency. Thus a satisfactory answer to Hilbert's problem must be carried out using principles that would be acceptable to someone who does not already believe PA is consistent. Such principles are often called finitistic because they are completely constructive and do not presuppose a completed infinity of natural numbers. Gödel's incompleteness theorem places a severe limit on how weak a finitistic system can be while still proving the consistency of Peano arithmetic.

Gödel's incompleteness theorem

Gödel's second incompleteness theorem shows that it is not possible for any proof that Peano Arithmetic is consistent to be carried out within Peano arithmetic itself. This theorem shows that if the only acceptable proof procedures are those that can be formalized within arithmetic then Hilbert's call for a consistency proof cannot be answered. However, as Nagel and Newman (1958:96–97) explain, there is still room for a proof that cannot be formalized in arithmetic:

:"This imposing result of Godel's analysis should not be misunderstood: it does not exclude a meta-mathematical proof of the consistency of arithmetic. What it excludes is a proof of consistency that can be mirrored by the formal deductions of arithmetic. 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. ... But these meta-mathematical 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 consistency proof

In 1936, Gentzen published a proof that Peano Arithmetic is consistent. Gentzen's result shows that a consistency proof can be obtained in a system that is much weaker than set theory.

Gentzen's proof proceeds by assigning to each proof in Peano arithmetic an ordinal number, based on the structure of the proof, with each of these ordinals less than ε₀. [Actually, the proof assigns a "notation" for an ordinal number to each proof. The notation is a finite string of symbols that intuitively stands for an ordinal number. By representing the ordinal in a finite way, Gentzen's proof does not presuppose strong axioms regarding ordinal numbers.] He then proves by transfinite induction on these ordinals that no proof can conclude in a contradiction. The method used in this proof can also be used to prove a cut elimination result for Peano arithmetic in a stronger logic than first-order logic, but the consistency proof itself can be carried out in ordinary first-order logic using the axioms of primitive recursive arithmetic and a transfinite induction principle. Tait (2005) gives a game-theoretic interpretation of Gentzen's method.

Gentzen's consistency proof initiated the program of ordinal analysis in proof theory. In this program, formal theories of arithmetic or set theory are assigned ordinal numbers in a manner that one theory will be able to prove the consistency of a second if and only if the ordinal assigned to the first is larger than the ordinal assigned to the second. These ordinals give a measure of the consistency strength of the theories. 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 ε₀.

Modern viewpoints on the status of the problem

While the theorems of Gödel and Gentzen are now well understood by the mathematical logic community, no consensus has formed on whether (or in what way) these theorems answer Hilbert's second problem. Simpson (1988:sec. 3) argues that Gödel's incompleteness theorem shows that it is not possible to produce finitistic consistency proofs of strong theories. Kreisel (1976) states that although Gödel's results imply that no finitistic syntactic consistency proof can be obtained, semantic (in particular, second-order) arguments can be used to give convincing consistency proofs. Detlefsen (1990:p. 65) argues that Gödel's theorem does not prevent a consistency proof because its hypotheses might not apply to all the systems in which a consistency proof could be carried out. Dawson (2006:sec. 2) calls the belief that Gödel's theorem eliminates the possibility of a persuasive consistency proof "erroneous", citing the consistency proof given by Gentzen and a later one given by Gödel in 1958.

Notes

References

* Dawson, John W. (2006) "Shaken foundations or groundbreaking realignment? A Centennial Assessment of Kurt Gödel’s Impact on Logic, Mathematics, and Computer Science". "2006 21st Annual IEEE Symposium on Logic in Computer Science", IEEE, pp. 339–341. ISBN 0-7695-2631-4 DOI|10.1109/LICS.2006.47
* cite journal
title = On an alleged refutation of Hilbert's Program using Gödel's First Incompleteness Theorem
journal = Journal of Philosophical Logic
id = ISSN 0022-3611 (Print) 1573-0433 (Online) DOI 10.1007/BF00263316
volume = 19
number = 4
date = 1990
pages = 343–377
author = Michael Detlefsen
doi = 10.1007/BF00263316
volume = 19
number = 4
date = 1990
pages = 343–377
author = Michael Detlefsen
unused_data = |Publisher Springer
unused_data = |Publisher Springer
* Torkel Franzen (2005), "Godel's theorem: An Incomplete Guide to its Use and Abuse", A.K. Peters, Wellesley MA. ISBN 1-56881-238-8
*Gerhard Gentzen (1936). "Die Widerspruchfreheit der reinen Zalenlehre." "Mathematische Annalen", v. 112, pp. 493–565.
* Kurt Gödel (1931), " [http://home.ddc.net/ygg/etext/godel/ Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.] " "Monatshefte für Mathematik und Physik 38": 173-98. Translated in Jean van Heijenoort, 1967. "From Frege to Gödel: A Source Book on Mathematical Logic". Harvard University Press: 596-616.
*David Hilbert [1900] (1901) "Mathematische Probleme". "Archiv der Mathematik und Physik", v. 3 n. 1, pp. 44–63 and 213–237. English translation, Maby Winton, "Bulletin of the American Mathematical Society" 8 (1902), 437–479. Available online at http://aleph0.clarku.edu/~djoyce/hilbert/problems.html .
* cite conference
author = George Kreisel
title = What have we learnt from Hilbert's second problem?
booktitle = Mathematical developments arising from Hilbert problems (Proc. Sympos. Pure Math., Northern Illinois Univ., De Kalb, Ill.,)
pages = 93–130
publisher = Amer. Math. Soc.
date = 1976
location = Providence, R. I.
id = ISBN 0-8218-1428-1
* Nagel, Ernest and Newman, James R., "Godel's Proof", New York University Press, 1958.
*cite journal | author = Stephen G. Simpson
title = Partial realizations of Hilbert's Program
journal = Journal of Symbolic Logic
volume = 53
number = 2
date = 1988
pages = 349–363
id = ISSN = 0022-4812 Available online at http://www.math.psu.edu/simpson/papers/hilbert.pdf .
* William W. Tait (2005). "Gödel's reformulation of Gentzen's first consistency proof of arithmetic: the no-counterexample interpretation." "Bulletin of Symbolic Logic" v. 11 n. 2, pp. 225–238.

External links

* [http://www.mathematik.uni-bielefeld.de/~kersten/hilbert/rede.html Original text of Hilbert's talk, in German]
* [http://aleph0.clarku.edu/~djoyce/hilbert/toc.html English translation of Hilbert's 1900 address]