Introduced by the mathematician David Hilbert, it is a significant effort to establish a complete and consistent foundation for all mathematics.1
Origin
It was a proposed solution to the foundational crisis of mathematics. Hilbert proposed to ground all existing theories to a finite, complete set of axioms, and to provide a proof that these axioms were consistent (i.e they do not contradict themselves).
Statement
The main statements of Hilbert’s program was:
- a formulation of all mathematics: mathematical statements should be written in a precise formal language and be manipulated according to defined rules
- completeness: all true mathematical statements can be proved in the formalism
- consistency: no contradiction can be obtained in the formalism of mathematics (hence addressing the crisis)
- decidability: there should be an algorithm for deciding the ruth or falsity of any mathematical statement. This is the Entscheidungsproblem.
Gödel’s incompleteness theorems
Kurt Gödel showed the most of the goals of Hilbert’s program was impossible to achieve:
- Gödel’s first theorem: any consistent formal system powerful enough to do basic arithmetic, there will always be true statements that the system cannot prove.
- Gödel’s second theorem: it is not possible to formalise all mathematical true statements within a formal system, as there will always be true statements that we cant prove using the formal system (using the first theorem)
Link to Computer Science
- Hilbert’s Program created the Entscheidungsproblem. It was later proved unsolvable by Turing and Church.
- Gödel’s theorem unveils the fundamental limits to what any formal system can prove. This parallels with Turing’s Halting Problem.