Hilbert's program

David Hilbert’s project aimed to formalize mathematics in axiomatic systems, prove those systems complete and consistent, and establish their consistency by finitistic reasoning.

Formal system: A formal system consists of symbols, axioms, and rules for deriving theorems. Hilbert sought to encode mathematics as explicit axioms and derivation rules.
Gödel's incompleteness theorems: Two theorems showing that sufficiently expressive, consistent formal systems cannot prove every truth about arithmetic or establish their own consistency. They ruled out key ambitions of Hilbert's program for arithmetic-capable systems.
David Hilbert: David Hilbert was a German mathematician whose work shaped geometry, algebra, and the foundations of mathematics. He formulated and led the project to secure mathematics through formalization and consistency proofs.
Intuitionism: Intuitionism is a philosophy of mathematics that accepts constructions as mathematical objects and rejects unrestricted classical principles. Its rejection of some classical proofs opposed Hilbert's defense of classical mathematics.
Consistency: A formal system is consistent if no statement and its negation are both derivable within it. Proving consistency was a central aim of Hilbert's project.
Consistency proof: A mathematical proof that a specified formal system does not derive a contradiction. Gödel's second theorem showed why a system of sufficient strength cannot prove its own consistency.
Grundlagen der Geometrie: David Hilbert's 1899 book axiomatized Euclidean geometry and examined the independence and consistency of its axioms. Its axiomatic method provided a model for Hilbert's broader foundational ambitions.
Set-theoretic foundations: Set-theoretic foundations represent mathematical objects and structures within axiomatic theories of sets. Set theory became a competing framework for grounding mathematics rather than Hilbert's proof-theoretic strategy.
Completeness (logic): A formal theory is syntactically complete when it proves or refutes every sentence in its language. Hilbert wanted axiomatic mathematics to settle every well-formed mathematical question.
Hilbert's second problem: A 1900 challenge asking for a proof that the axioms of arithmetic are consistent. It became the program's central test case for proving consistency by finitistic means.

Linked from 27 pages