Editing Hilbert's second problem (section)

== Gödel's incompleteness theorem ==
{{main|Gödel's incompleteness theorems}}

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 {{harvtxt|Nagel|Newman|1958}} explain, there is still room for a proof that cannot be formalized in arithmetic:{{sfnp|Nagel|Newman|1958|p=96&ndash;99}}

:"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. ... 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."<ref>A similar quotation with minor variations in wording appears in {{harvtxt|Nagel|Newman|2001}}, p. 107&ndash;108, as revised by [[Douglas R. Hofstadter]].</ref>