The Hilbert Program is a research program proposed by mathematician David Hilbert in the 1920s. It aims to prove the consistency of the axiom systems of mathematics with finite methods . Even if the Hilbert program has proven to be impracticable in its original claim, it nevertheless made a decisive contribution to clarifying the fundamentals and limits of mathematical knowledge.
Already Hilbert's list of 23 mathematical problems dating back to 1900 called the consistency of arithmetic as a second unsolved problem and encouraged in this direction for research. However, he only formulated the actual Hilbert program with concrete methods for solving the contradiction problem in the years 1918–1922. Hilbert was reacting to the antinomies of naive set theory and wanted to try to preserve all of “classical” mathematics and logic without foregoing Cantor's set theory .
"Nobody should be able to drive us out of the paradise that Cantor created for us."
Hilbert's program is at the same time a defense of the classical standpoint against intuitionism , which viewed some classical methods of proof such as indirect proof ( reductio ad absurdum ) or the theorem of the excluded third (tertium non datur) as questionable.
"Taking this Tertium non datur away from the mathematician would be like prohibiting the astronomer from using his telescope or the boxer from using his fists."
Hilbert therefore wanted to redefine mathematics as a formal system . The usual methods of proof should be allowed within this system. It should be ensured that outside the formal system, in the area of metamathematics , the consistency of the formally derivable sentences is proven; He restricted the outer, metalogical area to finite evidence, which the intuitionists also recognized and which were above any suspicion of generating antinomies. The aim of the program was to find a strictly formalized calculus or a system of axioms with simple, immediately plausible axioms that put mathematics and logic on a common, demonstrably consistent basis. In particular, the calculus should be powerful enough to be able to prove for any mathematical proposition whether it is true or false, and all true propositions should be deducible from the axiom system. So this had to be free of contradictions and complete .
The Hilbert program received widespread attention. Many well-known logicians and mathematicians took part, including Paul Bernays , Wilhelm Ackermann , John von Neumann , Jacques Herbrand and Kurt Gödel . They showed the consistency and completeness for central areas of logic, namely for classical propositional and predicate logic . Most of these logicians referred to partial axiom systems from the Principia Mathematica by Russell / Whitehead, the standard work of logic at the time.
With regard to the entire Principia Mathematica and all of mathematics, however, Hilbert's program failed: Kurt Gödel proved in 1930 in his incompleteness theorems that there are always sentences in the Principia Mathematica and related systems, including Cantor's set theory, which correspond to the Means of the same system are neither provable nor refutable, and that such systems cannot prove their own consistency. ( Alan Turing came to a similar conclusion with the closely related holding problem of machines .)
The Hilbert program, even if it did not prove to be feasible to the full extent originally intended, was a success for mathematics and logic, as it led to deeper insights into how formal systems work, what they can achieve and where their limits are. Important areas of modern mathematics and computer science emerged from the Hilbert program and its metamathematics, in particular modern formalized axiomatic set theory , proof theory , model theory and computability theory . It was also shown that the modified Hilbert program with extended (transfinite) evidence enabled proofs of freedom from contradiction for other areas of mathematics. This led Gerhard Gentzen with his consistency proof before the arithmetic of the 1936th Based on his proof, Wilhelm Ackermann showed in the same year the consistency of general set theory (without the axiom of infinity ) and in 1951 Paul Lorenzen that of branched type theory and classical analysis .
With the Metamath project, a database exists today (as of early 2020) with 23,000 theorems that have been strictly formally proven from ZFC , as well as proof verifiers written in several programming languages and thus multiple redundant proof verifiers, in order to be able to quickly verify formal evidence.
- Erhard Scholz: Gödel's incompleteness theorems and Hilbert's program of a “finite” proof theory . In: Wolfgang Achtner: Artificial Intelligence and Human Person , Marburg 2006, pp. 15–38 ( PDF ; 208 kB).
- Christian Tapp: At the limits of the finite. The Hilbert program in the context of formalism and finitism. Springer, Heidelberg 2013, ISBN 978-3-642-29654-3 .
- Max Urchs: Classic Logic: An Introduction . Berlin 1993, ISBN 3-05-002228-0 , chapter first-order theories , pp. 137-149.
- Richard Zach: Hilbert's Program. In: Edward N. Zalta (Ed.): Stanford Encyclopedia of Philosophy .
- Richard Zach: Hilbert's Program Then and Now . In: Dov M. Gabbay, Paul Thagard and John Woods: Handbook of the Philosophy of Science . Volume 5: Dale Jacquette (Ed.): Philosophy of Logic . 2006.
- ^ Metamath Proof Explorer metamath.org