Hilbert's program

Hilbert's program, formulated by German mathematician David Hilbert in the 1920s, was to formalize all existing theories to a finite, complete set of axioms, and provide a proof that these axioms were consistent.

Hilbert proposed that the consistency of more complicated systems, such as real analysis, could be proven in terms of simpler systems. Ultimately, the consistency of all of mathematics could be reduced to basic arithmetic. However Gödel's second incompleteness theorem showed in 1931 that basic arithmetic cannot be used to prove its own consistency, so it certainly cannot be used to prove the consistency of anything stronger.

tatement of Hilbert's program

The main goal of Hilbert's program was to provide secure foundations for all mathematics. In particular this should include:
*A formalization of all mathematics; in other words all mathematical statements should be written in a precise formal language, and manipulated according to well defined rules.
*Completeness: a proof that all true mathematical statements can be proved in the formalism.
*Consistency: a proof that no contradiction can be obtained in the formalism of mathematics. This consistency proof should preferably use only "finitistic" reasoning about finite mathematical objects.
*Conservation: a proof that any result about "real objects" obtained using reasoning about "ideal objects" (such as uncountable sets) can be proved without using ideal objects.
*Decidability: there should be an algorithm for deciding the truth or falsity of any mathematical statement.

Gödel's incompleteness theorems

Gödel showed that most of the goals of Hilbert's program were impossible to achieve, at least if interpreted in the most obvious way. His second incompleteness theorem stated that any consistent theory powerful enough to encode addition and multiplication of integers cannot prove its own consistency. This wipes out most of Hilbert's program as follows:

*It is not possible to formalize all of mathematics, as any attempt at such a formalism will omit some true mathematical statements, such as consistency of the formalism.
*An easy consequence of Gödel's incompleteness theorem is that there is no complete consistent extension of even Peano arithmetic with a recursively enumerable set of axioms, so in particular most interesting mathematical theories are not complete.
*A theory such as Peano arithmetic cannot even prove its own consistency, so a restricted "finitistic" subset of it certainly cannot prove the consistency of more powerful theories such as set theory.
*There is no algorithm to decide the truth (or provability) of statements in any consistent extension of Peano arithmetic. (Strictly speaking this result only appeared a few years after Gödel's theorem, because at the time the notion of an algorithm had not been precisely defined.)

Hilbert's program after Gödel

Much of Hilbert's program can be salvaged by changing its goals slightly, and with the following modifications some of it was successfully completed.
*Although it is not possible to formalize all mathematics, it is possible to formalize essentially all the mathematics that anyone uses. In particular Zermelo–Fraenkel set theory, combined with first-order logic, gives a satisfactory and generally accepted formalism for essentially all current mathematics.
*Although it is not possible to prove completeness for systems at least as powerful as Peano arithmetic (at least if they have a computable set of axioms), it is possible to prove forms of completeness for many interesting systems. The first big success was by Gödel himself (before he proved the incompleteness theorems) who proved the completeness theorem for first-order logic, showing that any logical consequence of a series of axioms is provable. An example of a non-trivial theory for which completeness has been proved is the theory of algebraically closed fields of given characteristic.
*The question of whether there are finitary consistency proofs of strong theories is difficult to answer, mainly because there is no generally accepted definition of a "finitary proof". Most mathematicians in proof theory seem to regard finitary mathematics as being contained in Peano arithmetic, and in this case it is not possible to give finitary proofs of reasonably strong theories. On the other hand Gödel himself suggested the possibility of giving finitary consistency proofs using finitary methods that cannot be formalized in Peano arithmetic, so he seems to have had a more liberal view of what finitary methods might be allowed. A few years later, Gentzen gave a consistency proof for Peano arithmetic. The only part of this proof that was not clearly finitary was a certain transfinite induction up to the ordinal ε₀. If this transfinite induction is accepted as a finitary method, then one can assert that there is a finitary proof of the consistency of Peano arithmetic. More powerful subsets of second order arithmetic have been given consistency proofs by Gaisi Takeuti and others, and one can again debate about exactly how finitary or constructive these proofs are. (The theories that have been proved consistent by these methods are quite strong, and include most "ordinary" mathematics.)
*Although there is no algorithm for deciding the truth of statements in Peano arithmetic, there are many interesting and non-trivial theories for which such algorithms have been found. For example, Tarski found an algorithm that can decide the truth of any statement in analytic geometry (more precisely, he proved that the theory of real closed fields is decidable). Given the Cantor-Dedekind axiom, this algorithm can be regarded as an algorithm to decide the truth of any statement in Euclidean geometry. This is substantial as few people would consider Euclidean geometry a trivial theory.

Hilbert wrote about Gödel's theorem. Since he was concerned with justifying the consistency of set theory, to make sure that infinite set operations do not produce false theorems, Gödel's theorem was not an "obstacle", but a method.

Gödel proved that Peano Arithmetic could not prove its own consistency, by constructing a deduction program which obviously does not halt but cannot be proven not to halt without contradiction. But the consistency of Peano arithmetic is itself intuitively obvious, and could be added to Peano Arithmetic as an axiom. The justification for the axiom is contained in Gödel's proof: the deduction program obviously does not halt.

The resulting system of axioms is also incomplete, but its consistency is obvious again, because the only new assertion is the correct statement that the previous theory was consistent, or that the deduction program does not halt. Hilbert interpreted a method as "finitary" when it produced deductions from extensions of Peano arithmetic by this process of adding consistency axioms countably many times up to a fixed computable countable ordinal [ D. Hilbert. "Die Grundlagen Der Elementaren Zahlentheorie" p. 215] .

This process proves the consistency of Peano Arithmetic [G. Gentzen, 1936. "Die Widerspruchfreiheit der reinen Zahlentheorie". Mathematische Annalen, 112:493–565. Translated as "The consistency of arithmetic", in ("The collected papers of Gerhard Gentzen", M. E. Szabo (ed.), 1969)] , but it is an open question, with both mathematical and philosophical difficulties, whether it is capable of proving the consistency of ZFC.

ee also

*Foundational crisis of mathematics

References

External links

*Entry on [http://plato.stanford.edu/entries/hilbert-program/ Hilbert's program] at the Stanford Encyclopedia of Philosophy.