# Hilbert's second problem

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Hilbert's_second_problem
> Markdown URL: https://mediated.wiki/source/Hilbert's_second_problem.md
> Source: https://en.wikipedia.org/wiki/Hilbert's_second_problem
> Source revision: 1333674057
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

Consistency of the axioms of arithmetic

In [mathematics](/source/Mathematics), **Hilbert's second problem** was posed by [David Hilbert](/source/David_Hilbert) in 1900 as one of his [23 problems](/source/Hilbert's_problems). It asks for a proof that arithmetic is [consistent](/source/Consistency_proof) – free of any internal contradictions. Hilbert stated that the axioms he considered for arithmetic were the ones given in [Hilbert (1900)](#CITEREFHilbert1900), which include a second order completeness axiom.

In the 1930s, [Kurt Gödel](/source/Kurt_G%C3%B6del) and [Gerhard Gentzen](/source/Gerhard_Gentzen) proved results that cast new light on the problem. Some feel that Gödel's theorems give a negative solution to the problem, while others consider Gentzen's proof as a partial positive solution.

## 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."[1]

Hilbert's statement is sometimes misunderstood, because by the "arithmetical axioms" he did not mean a system equivalent to Peano arithmetic, but a stronger system with a second-order completeness axiom. The system Hilbert asked for a completeness proof of is more like [second-order arithmetic](/source/Second-order_arithmetic) than first-order Peano arithmetic.

As a nowadays common interpretation, a positive solution to Hilbert's second question would in particular provide a proof that [Peano arithmetic](/source/Peano_arithmetic) is consistent.

There are many known proofs that Peano arithmetic is consistent that can be carried out in strong systems such as [Zermelo–Fraenkel set theory](/source/Zermelo%E2%80%93Fraenkel_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 are 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](/source/Finitism) because they are completely constructive and do not presuppose a completed infinity of natural numbers. Gödel's second incompleteness theorem (see [Gödel's incompleteness theorems](/source/G%C3%B6del's_incompleteness_theorems)) 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

Main article: [Gödel's incompleteness theorems](/source/G%C3%B6del's_incompleteness_theorems)

Gödel's [second incompleteness theorem](/source/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 & Newman (1958)](#CITEREFNagelNewman1958) explain, there is still room for a proof that cannot be formalized in arithmetic:[2]

- "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](/source/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. ... The possibility of constructing a finitistic absolute proof of consistency for arithmetic is not excluded by Gödel’s results. Gödel showed that no such proof is possible that can be represented within arithmetic. His argument does not eliminate the possibility of strictly finitistic proofs that cannot be represented within arithmetic. But no one today appears to have a clear idea of what a finitistic proof would be like that is not capable of formulation within arithmetic."[3]

## Gentzen's consistency proof

Main article: [Gentzen's consistency proof](/source/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](/source/Ordinal_number), based on the structure of the proof, with each of these ordinals less than [ε0](/source/Epsilon_numbers_(mathematics)).[4] He then proves by [transfinite induction](/source/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](/source/Cut_elimination) result for [Peano arithmetic](/source/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](/source/Primitive_recursive_arithmetic) and a transfinite induction principle. [Tait (2005)](#CITEREFTait2005) gives a game-theoretic interpretation of Gentzen's method.[5]

Gentzen's consistency proof initiated the program of [ordinal analysis](/source/Ordinal_analysis) in proof theory. In this program, formal theories of arithmetic or set theory are assigned [ordinal numbers](/source/Ordinal_numbers) that measure the [consistency strength](/source/Consistency_strength) of the theories. A theory will be unable to prove the consistency of another theory with a higher proof theoretic ordinal.

## 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)](#CITEREFSimpson1988) argues that Gödel's incompleteness theorem shows that it is not possible to produce finitistic consistency proofs of strong theories.[6] [Kreisel (1976)](#CITEREFKreisel1976) states that although Gödel's results imply that no finitistic syntactic consistency proof can be obtained, semantic (in particular, [second-order](/source/Second-order_logic)) arguments can be used to give convincing consistency proofs. [Detlefsen (1990)](#CITEREFDetlefsen1990) 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.[7] [Dawson (2006)](#CITEREFDawson2006) 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](/source/Dialectica_interpretation).[8]

## See also

- [Takeuti conjecture](/source/Takeuti_conjecture)

## Notes

1. **[^](#cite_ref-1)** [American Mathematical Society (1902)](#CITEREFAmerican_Mathematical_Society1902), translated by M. Newson. For the original version, see [Hilbert (1901)](#CITEREFHilbert1901).

1. **[^](#cite_ref-FOOTNOTENagelNewman195896–99_2-0)** [Nagel & Newman (1958)](#CITEREFNagelNewman1958), p. 96–99.

1. **[^](#cite_ref-3)** A similar quotation with minor variations in wording appears in [Nagel & Newman (2001)](#CITEREFNagelNewman2001), p. 107–108, as revised by [Douglas R. Hofstadter](/source/Douglas_R._Hofstadter).

1. **[^](#cite_ref-4)** 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.

1. **[^](#cite_ref-FOOTNOTETait2005_5-0)** [Tait (2005)](#CITEREFTait2005).

1. **[^](#cite_ref-FOOTNOTESimpson1988sec._3_6-0)** [Simpson (1988)](#CITEREFSimpson1988), sec. 3.

1. **[^](#cite_ref-FOOTNOTEDetlefsen199065_7-0)** [Detlefsen (1990)](#CITEREFDetlefsen1990), p. 65.

1. **[^](#cite_ref-FOOTNOTEDawson2006sec._2_8-0)** [Dawson (2006)](#CITEREFDawson2006), sec. 2.

## 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. [doi](/source/Doi_(identifier)):[10.1109/LICS.2006.47](https://doi.org/10.1109%2FLICS.2006.47). [ISBN](/source/ISBN_(identifier)) [0-7695-2631-4](https://en.wikipedia.org/wiki/Special:BookSources/0-7695-2631-4).

- [Detlefsen, Michael](/source/Michael_Detlefsen) (1990). "On an alleged refutation of Hilbert's Program using Gödel's First Incompleteness Theorem". *Journal of Philosophical Logic*. **19** (4). Springer: 343–377. [doi](/source/Doi_(identifier)):[10.1007/BF00263316](https://doi.org/10.1007%2FBF00263316). [S2CID](/source/S2CID_(identifier)) [44736805](https://api.semanticscholar.org/CorpusID:44736805).

- [Franzen, Torkel](/source/Torkel_Franz%C3%A9n) (2005). *Godel's theorem: An Incomplete Guide to its Use and Abuse*. [Wellesley MA](/source/Wellesley%2C_Massachusetts): [A.K. Peters](/source/A_K_Peters). [ISBN](/source/ISBN_(identifier)) [1-56881-238-8](https://en.wikipedia.org/wiki/Special:BookSources/1-56881-238-8).

- [Gentzen, Gerhard](/source/Gerhard_Gentzen) (1936). "Die Widerspruchsfreiheit der reinen Zahlentheorie". *Mathematische Annalen*. **112**. Springer: 493–565. [doi](/source/Doi_(identifier)):[10.1007/BF01565428](https://doi.org/10.1007%2FBF01565428).

- [Gödel, Kurt](/source/Kurt_G%C3%B6del) (1931). ["Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I"](https://web.archive.org/web/20060705205103/http://home.ddc.net/ygg/etext/godel/). *Monatshefte für Mathematik und Physik*. **38**: 173–98. [doi](/source/Doi_(identifier)):[10.1007/BF01700692](https://doi.org/10.1007%2FBF01700692). [S2CID](/source/S2CID_(identifier)) [197663120](https://api.semanticscholar.org/CorpusID:197663120). Archived from [the original](http://home.ddc.net/ygg/etext/godel/) on 2006-07-05.

- [Hilbert, David](/source/David_Hilbert) (1900). ["Über den Zahlbegriff"](http://resolver.sub.uni-goettingen.de/purl?PPN37721857X). *Jahresbericht der Deutschen Mathematiker-Vereinigung*. **8**: 180–184.

- ——— (1901) [1900]. "Mathematische Probleme". *Archiv der Mathematik und Physik*. **3** (1): 44–63, 213–237.

- [Kreisel, George](/source/George_Kreisel) (1976). "What have we learnt from Hilbert's second problem?". *Mathematical developments arising from Hilbert problems (Proc. Sympos. Pure Math., Northern Illinois Univ., De Kalb, Ill.,)*. Providence, R. I.: Amer. Math. Soc. pp. 93–130. [ISBN](/source/ISBN_(identifier)) [0-8218-1428-1](https://en.wikipedia.org/wiki/Special:BookSources/0-8218-1428-1).

- ["Mathematical Problems"](https://www.ams.org/journals/bull/1902-08-10/S0002-9904-1902-00923-3/S0002-9904-1902-00923-3.pdf) (PDF). *[Bulletin of the American Mathematical Society](/source/Bulletin_of_the_American_Mathematical_Society)*. **8**. [American Mathematical Society](/source/American_Mathematical_Society): 437–479. 1902.

- [Nagel, Ernest](/source/Ernest_Nagel); [Newman, James R.](/source/James_R._Newman) (1958). *Godel's Proof*. New York University Press.

- ———; ——— (2001). [Hofstadter, Douglas R.](/source/Douglas_R._Hofstadter) (ed.). [*Godel's Proof*](https://books.google.com/books?id=oQsUCgAAQBAJ&pg=PA107). New York University Press. [ISBN](/source/ISBN_(identifier)) [9780814758014](https://en.wikipedia.org/wiki/Special:BookSources/9780814758014).

- [Simpson, Stephen G.](/source/Stephen_G._Simpson) (1988). "Partial realizations of Hilbert's Program". *Journal of Symbolic Logic*. **53** (2): 349–363. [CiteSeerX](/source/CiteSeerX_(identifier)) [10.1.1.79.5808](https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.79.5808). [doi](/source/Doi_(identifier)):[10.2307/2274508](https://doi.org/10.2307%2F2274508). [ISSN](/source/ISSN_(identifier)) [0022-4812](https://search.worldcat.org/issn/0022-4812). [JSTOR](/source/JSTOR_(identifier)) [2274508](https://www.jstor.org/stable/2274508).

- [Tait, William W.](/source/William_W._Tait) (2005). "Gödel's reformulation of Gentzen's first consistency proof of arithmetic: the no-counterexample interpretation". *Bulletin of Symbolic Logic*. **11** (2): 225–238. [JSTOR](/source/JSTOR_(identifier)) [1556751](https://www.jstor.org/stable/1556751).

- [van Heijenoort, Jean](/source/Jean_van_Heijenoort) (1967). *From Frege to Gödel: A Source Book on Mathematical Logic*. Harvard University Press. pp. 596–616..

## External links

- [Original text of Hilbert's talk, in German](https://web.archive.org/web/20120205025851/http://www.mathematik.uni-bielefeld.de/~kersten/hilbert/rede.html)

- [English translation of Hilbert's 1900 address](http://aleph0.clarku.edu/~djoyce/hilbert/toc.html)

v t e Hilbert's problems 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 (24)

v t e Mathematical logic General Axiom list Cardinality First-order logic Formal proof Formal semantics Foundations of mathematics Information theory Lemma Logical consequence Model Theorem Theory Type theory Theorems (list), paradoxes Gödel's completeness – incompleteness theorems Tarski's undefinability Banach–Tarski paradox Cantor's theorem – paradox – diagonal argument Compactness Halting problem Lindström's Löwenheim–Skolem Russell's paradox Logics Traditional Classical logic Logical truth Tautology Proposition Inference Logical equivalence Consistency Equiconsistency Argument Soundness Validity Syllogism Square of opposition Venn diagram Propositional Boolean algebra Boolean functions Logical connectives Propositional calculus Propositional formula Truth tables Many-valued logic 3 finite ∞ Predicate First-order list Second-order Monadic Higher-order Fixed-point Free Quantifiers Predicate Monadic predicate calculus Set theory Set hereditary Class (Ur-)Element Ordinal number Extensionality Forcing Relation equivalence partition Set operations: intersection union complement Cartesian product power set identities Types of sets Countable Uncountable Empty Inhabited Singleton Finite Infinite Transitive Ultrafilter Recursive Fuzzy Universal Universe constructible Grothendieck Von Neumann Maps, cardinality Function/Map domain codomain image In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal inaccessible Aleph number Operation binary Theories Zermelo–Fraenkel axiom of choice continuum hypothesis General Kripke–Platek Morse–Kelley Naive New Foundations Tarski–Grothendieck Von Neumann–Bernays–Gödel Ackermann Constructive Formal systems (list), language, syntax Alphabet Arity Automata Axiom schema Expression ground Extension by definition conservative Relation Formation rule Grammar Formula atomic closed ground open Free/bound variable Language Metalanguage Logical connective ¬ ∨ ∧ → ↔ = Predicate functional variable propositional variable Proof Quantifier ∃ ! ∀ rank Sentence atomic spectrum Signature String Substitution Symbol function logical/constant non-logical variable Term Theory list Example axiomatic systems (list) of true arithmetic Peano second-order elementary function primitive recursive Robinson Skolem of the real numbers Tarski's axiomatization of Boolean algebras canonical minimal axioms of geometry Euclidean Elements Hilbert's Tarski's non-Euclidean Principia Mathematica Proof theory Formal proof Natural deduction Logical consequence Rule of inference Sequent calculus Theorem Systems axiomatic deductive Hilbert list Complete theory Independence (from ZFC) Proof of impossibility Ordinal analysis Reverse mathematics Self-verifying theories Model theory Interpretation function of models Model atomic equivalence finite prime saturated spectrum submodel Non-standard model of non-standard arithmetic Diagram elementary Categorical theory Model complete theory Satisfiability Semantics of logic Strength Theories of truth semantic Tarski's Kripke's T-schema Transfer principle Truth predicate Truth value Type Ultraproduct Validity Computability theory Church encoding Church–Turing thesis Computably enumerable Computable function Computable set Decision problem decidable undecidable P NP P versus NP problem Kolmogorov complexity Lambda calculus Primitive recursive function Recursion Recursive set Turing machine Type theory Related Abstract logic Algebraic logic Automated theorem proving Category theory Concrete/Abstract category Category of sets History of logic History of mathematical logic timeline Logicism Mathematical object Philosophy of mathematics Supertask Mathematics portal

Authority control databases GND

---
Adapted from the Wikipedia article [Hilbert's second problem](https://en.wikipedia.org/wiki/Hilbert's_second_problem) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Hilbert's_second_problem?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.