Hilbert's program
Encyclopedia
In mathematics
, Hilbert's program, formulated by German
mathematician David Hilbert
, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics
were found to suffer from paradoxes and inconsistencies. As a solution, Hilbert proposed to ground all existing theories to a finite, complete set of axiom
s, 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, some argue that Gödel's incompleteness theorems
showed in 1931 that Hilbert's program was unattainable. In his first theorem, Gödel showed that any consistent system with a computable set of axioms which is capable of expressing arithmetic can never be complete: it is possible to construct a statement that can be shown to be true, but that cannot be derived from the formal rules of the system. In his second theorem, he showed that such a system could not prove its own consistency, so it certainly cannot be used to prove the consistency of anything stronger. This refuted Hilbert's assumption that a finitistic system could be used to prove the consistency of a stronger theory.
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:
, proof theory
and reverse mathematics
can be viewed as natural continuations of Hilbert's original program. Much of it can be salvaged by changing its goals slightly (Zach 2005), and with the following modifications some of it was successfully completed:
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 (Hilbert 1931, p. 215).
This process proves the consistency of Peano Arithmetic (Gentzen 1936), but it is an open question, with both mathematical and philosophical difficulties, whether it is capable of proving the consistency of ZFC.
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, Hilbert's program, formulated by German
Germans
The Germans are a Germanic ethnic group native to Central Europe. The English term Germans has referred to the German-speaking population of the Holy Roman Empire since the Late Middle Ages....
mathematician David Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics
Foundations of mathematics
Foundations of mathematics is a term sometimes used for certain fields of mathematics, such as mathematical logic, axiomatic set theory, proof theory, model theory, type theory and recursion theory...
were found to suffer from paradoxes and inconsistencies. As a solution, Hilbert proposed to ground all existing theories to a finite, complete set of axiom
Axiom
In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
s, and provide a proof that these axioms were consistent. Hilbert proposed that the consistency of more complicated systems, such as real analysis
Real analysis
Real analysis, is a branch of mathematical analysis dealing with the set of real numbers and functions of a real variable. In particular, it deals with the analytic properties of real functions and sequences, including convergence and limits of sequences of real numbers, the calculus of the real...
, could be proven in terms of simpler systems. Ultimately, the consistency of all of mathematics could be reduced to basic arithmetic.
However, some argue that Gödel's incompleteness theorems
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
showed in 1931 that Hilbert's program was unattainable. In his first theorem, Gödel showed that any consistent system with a computable set of axioms which is capable of expressing arithmetic can never be complete: it is possible to construct a statement that can be shown to be true, but that cannot be derived from the formal rules of the system. In his second theorem, he showed that such a system could not prove its own consistency, so it certainly cannot be used to prove the consistency of anything stronger. This refuted Hilbert's assumption that a finitistic system could be used to prove the consistency of a stronger theory.
Statement 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
Kurt GödelKurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
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.
- An easy consequence of Gödel's incompleteness theorem is that there is no complete consistent extension of even Peano arithmeticPeano axiomsIn mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano...
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
Many current lines of research in mathematical logicMathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
and reverse mathematics
Reverse mathematics
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of...
can be viewed as natural continuations of Hilbert's original program. Much of it can be salvaged by changing its goals slightly (Zach 2005), 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 theoryZermelo–Fraenkel set theoryIn mathematics, Zermelo–Fraenkel set theory with the axiom of choice, named after mathematicians Ernst Zermelo and Abraham Fraenkel and commonly abbreviated ZFC, is one of several axiomatic systems that were proposed in the early twentieth century to formulate a theory of sets without the paradoxes...
, combined with first-order logicFirst-order logicFirst-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate 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 theoremGödel's completeness theoremGödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....
for first-order logicFirst-order logicFirst-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate 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, GentzenGerhard GentzenGerhard Karl Erich Gentzen was a German mathematician and logician. He had his major contributions in the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus...
gave a consistency proofGentzen's consistency proofGentzen's consistency proof is a result of proof theory in mathematical logic. It "reduces" the consistency of a simplified part of mathematics, not to something that could be proved , but to clarified logical principles.-Gentzen's theorem:In 1936 Gerhard Gentzen proved the consistency of...
for Peano arithmetic. The only part of this proof that was not clearly finitary was a certain transfinite inductionTransfinite inductionTransfinite induction is an extension of mathematical induction to well-ordered sets, for instance to sets of ordinal numbers or cardinal numbers.- Transfinite induction :Let P be a property defined for all ordinals α...
up to the ordinalOrdinal numberIn set theory, an ordinal number, or just ordinal, is the order type of a well-ordered set. They are usually identified with hereditarily transitive sets. Ordinals are an extension of the natural numbers different from integers and from cardinals...
ε0. 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 TakeutiGaisi Takeutiis a Japanese mathematician, known for his work in proof theory.After graduating from Tokyo University, he went to Princeton to study under Kurt Gödel.He later became a professor at the University of Illinois at Urbana-Champaign...
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 geometryAnalytic geometryAnalytic geometry, or analytical geometry has two different meanings in mathematics. The modern and advanced meaning refers to the geometry of analytic varieties...
(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 geometryEuclidean geometryEuclidean geometry is a mathematical system attributed to the Alexandrian Greek mathematician Euclid, which he described in his textbook on geometry: the Elements. Euclid's method consists in assuming a small set of intuitively appealing axioms, and deducing many other propositions from these...
. 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 (Hilbert 1931, p. 215).
This process proves the consistency of Peano Arithmetic (Gentzen 1936), but it is an open question, with both mathematical and philosophical difficulties, whether it is capable of proving the consistency of ZFC.
External links
- Entry on Hilbert's program at the Stanford Encyclopedia of Philosophy.