Hilbert's program

The Hilbert program is a research program proposed by the mathematician David Hilbert in the 1920s. It aims to demonstrate, by finite methods, the consistency of the axiom systems of mathematics. Even if the Hilbert program has proved in his original claim to be unfeasible, it nevertheless contributed greatly to clarify the foundations and limits of mathematical knowledge.

Background

Already Hilbert's list of 23 mathematical problems from 1900, called the consistency of arithmetic as a second unsolved problem and encouraged to research in this direction. But the real Hilbert program with concrete methods to solve the contradiction problem, he formulated only in the years 1918 to 1922. Hilbert was responding to the antinomies of naive set theory and wanted to try the whole "classic" to preserve mathematics and logic, without compromising on Cantor's set theory.

"From the paradise that Cantor created us, no one can sell to us."

Hilbert's program is both a defense of the classical position against intuitionism, of some classical methods of proof as indirect evidence ( reductio ad absurdum ), or looked at the law of excluded middle ( tertium non datur ) as questionable.

" This tertium non datur to take the mathematician, would be about as if you wanted to prohibit the astronomer the telescope or the boxer the use of his fists. "

Hilbert wanted therefore to redefine mathematics as a formal system. Within this system, the usual methods of proof should be permitted. It should be protected, that is, evidence outside the formal system in the field of metamathematics, the consistency of formally derivable sentences; he limited the outer metalogical area on a finite evidence which, were the intuitionists recognized and suspicion to generate antinomies sublime. The goal of the program, therefore, was to find a strictly formalized calculus or an axiom system with simple immediately obvious axioms, which focuses on the mathematics and logic to a common, detectable consistent basis. In particular, the calculus should be powerful enough to prove for each mathematical theorem can, whether it is true or false, and all true sentences should be derivable from the axiom system. So this had to be consistent and complete.

The Hilbert program received broad attention. Many well-known logicians and mathematicians involved, among other things, Paul Bernays, Wilhelm Ackermann, John von Neumann, Jacques Herbrand and Kurt Gödel. They showed the consistency and completeness of central branches of logic, namely for the classical propositional and predicate logic. In most cases, these logicians based on part - axiom systems from the Principia Mathematica of Russell / Whitehead, the former standard work of logic.

In relation to total Principia Mathematica and to all the mathematics suggested Hilbert's program, however, failed: Kurt Godel proved namely 1930 in its incompleteness that there always are sentences in the Principia Mathematica and related systems, including Cantor's set theory is one that the means of the same system are neither provable nor refutable, and that such systems have their own consistency can not prove it. ( Alan Turing was closely related with the halting problem of automatic machines for a similar result. )

The Hilbert program was, even if it is not proved in full, originally intended scope as practicable, an achievement for mathematics and logic, as it deepened insights led about how formal systems work, what they are capable of and what its limits are. Important areas of modern mathematics and computer science have emerged from the Hilbert program and its metamathematics, in particular the modern formalized axiomatic set theory, proof theory, model theory and computability theory. It was also found that the modified Hilbert program with advanced ( transfinite ) evidence allowed consistency proofs for other math areas. This led Gerhard Gentzen ago with his consistency proof of arithmetic of 1936. Based on his evidence showed Wilhelm Ackermann in the same year the consistency of general set theory with finite sets and 1951 Paul Lorenzen of the branched type theory and classical analysis.