Formalism and the Hilbert programme
Branch · 1900s-1930s · Mathematics, stage 2: Map the branches
Formalism treats mathematics as the manipulation of symbols according to stated rules, so that a proof is a finite object that can be checked mechanically without interpreting what the symbols refer to. Hilbert built a programme on this: write all of mathematics as formal systems, then prove by simple finite reasoning that those systems can never derive a contradiction. Gödel showed in 1931 that no sufficiently strong system can prove its own consistency, and Turing showed in 1936 that no algorithm can decide which statements are provable, so the programme in its original form cannot be completed.
What it claims
- Mathematics can be presented as formal systems: symbols plus rules for combining them.
- The consistency of such a system should be provable by finite, uncontroversial means.
- That goal is unattainable in its strongest form, by the incompleteness and undecidability results.
Key ideas
People
Sources
- Formalism in the Philosophy of Mathematics Stanford Encyclopedia of Philosophy
- Hilbert's Program Stanford Encyclopedia of PhilosophyWhat the programme asked for, and exactly which part of it the 1931 result removes.
- Formalism (philosophy of mathematics) Wikipedia
