Editing John von Neumann (section)

=== Proof theory ===
{{See also|Hilbert's program}}

With the contributions of von Neumann to sets, the axiomatic system of the theory of sets avoided the contradictions of earlier systems and became usable as a foundation for mathematics, despite the lack of a proof of its [[consistency]]. The next question was whether it provided definitive answers to all mathematical questions that could be posed in it, or whether it might be improved by adding stronger [[Axiom#Mathematical logic|axioms]] that could be used to prove a broader class of theorems.<ref>{{cite encyclopedia |last=Von Plato |first=Jan |title=The Development of Proof Theory |encyclopedia=The Stanford Encyclopedia of Philosophy |year=2018 |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/entries/proof-theory-development/ |publisher=Stanford University |edition=Winter 2018 |access-date=2023-09-25 }}</ref>

By 1927, von Neumann was involving himself in discussions in Göttingen on whether [[elementary arithmetic]] followed from [[Peano axioms]].<ref>{{cite journal |last1=van der Waerden |first1=B. L. |author-link1=Bartel Leendert van der Waerden |title=On the sources of my book Moderne algebra |journal=Historia Mathematica |date=1975 |volume=2 |issue=1 |pages=31–40 |doi=10.1016/0315-0860(75)90034-8 |doi-access=free }}</ref> Building on the work of [[Wilhelm Ackermann|Ackermann]], he began attempting to prove (using the [[Finitism|finistic]] methods of [[Hilbert's program|Hilbert's school]]) the consistency of [[Peano axioms#Peano arithmetic as first-order theory|first-order arithmetic]]. He succeeded in proving the consistency of a fragment of arithmetic of natural numbers (through the use of restrictions on [[Mathematical induction|induction]]).<ref>{{cite journal |last1=Neumann |first1=J. v. |title=Zur Hilbertschen Beweistheorie |journal=Mathematische Zeitschrift |date=1927 |volume=24 |pages=1–46 |language=German |doi=10.1007/BF01475439 |s2cid=122617390 |url=https://eudml.org/doc/167910}}</ref> He continued looking for a more general proof of the consistency of classical mathematics using methods from [[proof theory]].{{sfn|Murawski|2010|pp=204-206}}

A strongly negative answer to whether it was definitive arrived in September 1930 at the [[Second Conference on the Epistemology of the Exact Sciences]], in which [[Kurt Gödel]] announced his [[Gödel's incompleteness theorems|first theorem of incompleteness]]: the usual axiomatic systems are incomplete, in the sense that they cannot prove every truth expressible in their language. Moreover, every consistent extension of these systems necessarily remains incomplete.{{sfn|Rédei|2005|p=123}} At the conference, von Neumann suggested to Gödel that he should try to transform his results for undecidable propositions about integers.{{sfn|von Plato|2018|p=4080}}

Less than a month later, von Neumann communicated to Gödel an interesting consequence of his theorem: the usual axiomatic systems are unable to demonstrate their own consistency.{{sfn|Rédei|2005|p=123}} Gödel replied that he had already discovered this consequence, now known as his [[second incompleteness theorem]], and that he would send a preprint of his article containing both results, which never appeared.<ref>{{cite book |last=Dawson |first=John W. Jr. |author-link=John W. Dawson, Jr. |year=1997 |title=Logical Dilemmas: The Life and Work of Kurt Gödel |location=Wellesley, Massachusetts |publisher=A. K. Peters |isbn=978-1-56881-256-4 |page=70}}</ref>{{sfn|von Plato|2018|pp=4083-4088}}{{sfn|von Plato|2020|pp=24-28}} Von Neumann acknowledged Gödel's priority in his next letter.{{sfn|Rédei|2005|p=124}} However, von Neumann's method of proof differed from Gödel's, and he was also of the opinion that the second incompleteness theorem had dealt a much stronger blow to Hilbert's program than Gödel thought it did.{{sfn|von Plato|2020|p=22}}<ref>{{cite book |last1=Sieg |first1=Wilfried |title=Hilbert's Programs and Beyond |date=2013 |publisher=Oxford University Press |isbn=978-0195372229 |url=https://books.google.com/books?id=4lDrwqo-8TkC&pg=PA149 |page=149}}</ref> With this discovery, which drastically changed his views on mathematical rigor, von Neumann ceased research in the [[foundations of mathematics]] and [[metamathematics]] and instead spent time on problems connected with applications.{{sfn|Murawski|2010|p=209}}