Math 2.0

Mathematical logic and foundations Philosophical questions and foundational programs Problem

Hilbert's program

Builds on FormalismPeano axioms

Problem

Write all of classical mathematics as a formal system with finitely describable axioms and rules of inference. Then prove, by finitary means only, that this formal system is consistent. Here a proof is finitary when it reasons only about finite strings of symbols in a concrete, checkable way. Consistency means that no formula φ\varphi is derivable together with its negation ¬φ\neg \varphi.

Remarks

The program is the main form of formalism. It also asked for a proof of completeness: every statement of the system should be provable or refutable. Gödel's incompleteness theorems of 1931 showed that the program cannot be carried out as first intended. A consistent, effectively axiomatized system that contains enough arithmetic is incomplete. Such a system also cannot prove its own consistency. In 1936 Gerhard Gentzen proved the consistency of the Peano axioms of first-order arithmetic, see Gentzen's consistency proof. His proof uses transfinite induction up to the ordinal ε0\varepsilon_0, which goes beyond the finitary means of the original program. Partial versions of the program are studied in proof theory and in reverse mathematics.

Reading path

To understand this page from the ground up, read these 3 pages in order. The foundations come first.

Show the path as a graph
Formalism, concept, no evidence levelFormalismconceptPeano axioms, concept, no evidence levelPeano axiomsconceptHilbert's program, problem, no evidence levelHilbert's programproblem
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Formalism concept
  2. Peano axioms concept
  3. Hilbert's program problem

Further reading

  1. Web https://en.wikipedia.org/wiki/Hilbert's_program
About this page
TagP1RW6JWX73
URIm2://P1RW6JWX73
Kindproblem
WritingW0 stub
MSC03A05, 03F25, 03F30
StatusThis copy of the site has no build data. Run m2 status P1RW6JWX73.
AboutFoundations of mathematics
UsesFormalism, Peano axioms
Same as
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

No page links to this page yet.