Hilbert's program

In mathematics, Hilbert's program was an important idea created by the German mathematician David Hilbert in the early 1920s. At that time, mathematics was facing a crisis because new attempts to explain the basics of math led to problems and contradictions. Hilbert wanted to solve this by creating a solid set of rules, called axioms, that all math could be based on. He believed these axioms could be shown to not lead to any contradictions, and that more complex parts of math, like the study of real numbers, could be proven correct using these basic rules.

However, in 1931, another mathematician named Kurt Gödel showed that Hilbert's program would not work for important parts of math. Gödel proved that in any system with basic rules that can handle arithmetic, there will always be true statements that cannot be proven using those rules. He also showed that such a system cannot prove that it itself is correct, meaning it cannot be used to prove the correctness of more complicated math. This was a big discovery because it meant Hilbert's hope of proving all of mathematics was not possible.

Statement of Hilbert's program

The main goal of Hilbert's program was to create strong, safe rules for all of mathematics. This meant writing every math idea in a clear way, using special steps to work with them.

Hilbert wanted proofs to show that these rules were complete, meaning every true math idea could be shown, and consistent, meaning no mistakes or opposite answers could happen. He also hoped to find a way to decide if any math statement was true or false using a set of steps.

Gödel's incompleteness theorems

Main article: Gödel's incompleteness theorems

Kurt Gödel showed that many of the ideas from Hilbert's plan for mathematics could not work in the way Hilbert hoped. Gödel's work proved that a mathematical system strong enough to handle basic number operations cannot show that it itself is correct. This means it is not possible to capture all true math facts in one system, as some true facts will always be left out. Also, a system like Peano arithmetic cannot prove its own correctness, so it cannot prove that more complex theories are correct either.

Hilbert's program after Gödel

Many current areas of study in mathematical logic, such as proof theory and reverse mathematics, can be seen as continuing ideas from Hilbert's original plan. Much of Hilbert's plan can still be useful with some changes to its goals.

Although it isn't possible to organize all of mathematics into one system, it is possible to organize nearly all the math that people use. For example, Zermelo–Fraenkel set theory, together with first-order logic, provides a good and widely accepted way to structure most of today's mathematics. While we cannot prove completeness for systems that include basic number theory, we can prove completeness for many other important systems. One example is the theory of algebraically closed fields with a specific characteristic.

It is challenging to know whether there are simple proofs showing that strong theories are consistent, mainly because there is no clear agreement on what a "simple proof" means. Most experts in proof theory think simple mathematics is included in basic number theory, and with this view, it isn't possible to give simple proofs for very strong theories. However, some believe simpler methods can be used that go beyond basic number theory. Later, Gentzen provided a consistency proof for basic number theory. The only part of this proof that might not be simple was a certain type of reasoning called transfinite induction up to the ordinal ε₀. If this reasoning is considered simple, then we can say there is a simple proof showing that basic number theory is consistent. Other mathematicians have also provided consistency proofs for stronger systems, and there is discussion about how simple or constructive these proofs are.

While there is no universal method to determine the truth of statements in basic number theory, there are many interesting theories for which such methods have been developed. For example, Tarski created a method to decide the truth of any statement in analytic geometry. With the Cantor–Dedekind axiom, this method can also decide the truth of statements in Euclidean geometry, which is important since many people would not consider Euclidean geometry a simple theory.