Hilbert's Program and the Study of Proof

The responses to the paradoxes offered different ways to restrict mathematical reasoning. A further question remained: how could one justify confidence in a proposed system as a whole?

David Hilbert sought an answer that would preserve the power of classical mathematics. The program associated with his name aimed to represent mathematical reasoning formally and then establish, using secure finitary methods, that its powerful ideal principles could not lead to contradiction.

This required a new division of labor. Within a mathematical theory, one proves statements about numbers, sets, or functions. Outside it, one studies the expressions and derivations of the theory itself. The latter investigation became known as metamathematics or proof theory.

From an axiomatic problem to a program

Hilbert's second problem, presented in 1900, called for a consistency proof for arithmetic. His work on the foundations of geometry had shown the importance of models and relative consistency arguments. But interpreting one theory in another leaves a question about the background theory that performs the interpretation.

The proof-theoretic program took a more developed form during the 1920s. Hilbert and his collaborators sought to analyze mathematical proofs as finite configurations of symbols. Paul Bernays was central to both the technical development and the clarification of the program's aims. Wilhelm Ackermann pursued difficult consistency arguments, including work using Hilbert's epsilon calculus.

It is therefore misleading to describe the program as one proposal made in a single year. The 1900 problem, Hilbert's earlier foundational work, and the mature metamathematical project are connected stages with different formulations.

The broader setting also mattered. Foundational disagreement was not confined to whether a particular formal axiom was safe. Brouwer's intuitionism challenged accepted uses of classical logic in infinite mathematics. Hilbert wanted to explain why the existing mathematical methods could be retained.

Real and ideal mathematics

Hilbert distinguished a secure domain of finitary reasoning from stronger ideal methods. The precise boundary of finitism was debated and remains a subject of historical interpretation. At its center were concrete finite expressions and elementary operations on them.

For example, one can inspect a finite sequence of strokes, append another stroke, compare two sequences, or carry out a calculation on numerals. One can also reason generally about such operations without assuming an already completed universe of arbitrary infinite objects.

Ideal mathematics includes principles that range over infinite domains and make possible concise, systematic theories. Hilbert's proposal was not simply to declare these expressions meaningless and stop. Their use was to be justified by showing that the ideal apparatus could not produce unacceptable consequences for the secure part.

A consistency proof is one version of this ambition: demonstrate that the formalized ideal theory cannot derive a contradiction. Stronger formulations seek a form of conservativity, showing that ideal reasoning proves no new statements of a specified real kind beyond those already justified by the secure methods.

Consistency and conservativity must be distinguished. A theory can be consistent while proving new arithmetical statements. To prove conservativity, one must specify both the weaker theory and the class of statements whose consequences are being compared.

Proofs as finite objects

Consider a formal language with symbols for zero, successor, addition, equality, variables, and logical operations. The well-formed expressions are generated by explicit rules. A formal proof is then a finite sequence or tree of formulas in which each step is an axiom or follows by an allowed inference.

Even a theory containing infinitely many axioms can have effective proof checking if its axioms are given by a recognizable schema. For example, the induction schema supplies an instance for each formula. A particular proposed proof uses only finitely many such instances, and each can be checked against the schema.

This distinction is crucial. Infinitely many possible derivations do not make the checking of one finite derivation an infinite task. The metamathematician can ask what an arbitrary finite proof must look like and whether its structure permits a contradiction.

The proof is now data for another mathematical investigation. Its formulas need not be interpreted as true assertions in an intended infinite structure at every stage of that investigation. One may instead establish a syntactic invariant preserved by every inference.

A consistency proof for a small calculus

A simple example shows the method without claiming to reproduce the difficulty of arithmetic.

Take closed terms built from $0$, successor $S$, and addition. Allow the equations

along with reflexivity of equality and the usual rules of symmetry, transitivity, and replacement of equals inside terms.

Assign a natural-number value to every closed term by recursion:

Every initial equation has equal values on its two sides. Reflexivity, symmetry, and transitivity preserve that property. Replacing one subterm by another of the same value also preserves the value of the complete term.

Induction on the finite derivation therefore proves:

Since $v(0)\neq v(S(0))$, the calculus cannot derive $0=S(0)$.

The argument uses a semantic invariant for a deliberately weak equational calculus. It illustrates the structure of a consistency proof: inspect the axioms, inspect the rules, and establish a property that excludes the designated contradiction.

It does not establish the consistency of full arithmetic with unrestricted induction. We have used ordinary reasoning about natural numbers in the metatheory and must assess that background separately if we want to claim a particular finitary reduction. The example makes the dependence visible instead of concealing it.

The epsilon calculus

Hilbert's epsilon notation offered a way to analyze quantificational reasoning through terms that act as potential witnesses. An expression

is intended to select an $x$ satisfying $A$, if one exists. A characteristic principle is

If some supplied term satisfies the condition, the selected witness must satisfy it as well. The notation permits quantified reasoning to be reorganized around terms and substitution.

The difficult part is not the informal idea of choosing a witness. Epsilon expressions can be nested, and changing the value assigned to one expression can affect conditions involving others. A procedure that repairs one failed condition may disturb another.

The epsilon-substitution approach sought to replace these expressions by numerical values in a way that satisfies the finite collection of relevant conditions extracted from a proof. If the repair process could always be shown to terminate by permitted methods, it could support a consistency argument.

Ackermann's work demonstrates why early proof theory was technically demanding. The obstacle was not a lack of symbolic notation but the control of interacting dependencies in arbitrary proofs. Later developments clarified which termination arguments require principles stronger than those first envisaged.

What does the metatheory assume?

A formal system cannot introduce its own notation to a reader who lacks any prior ability to distinguish expressions and follow rules. Describing a formal theory therefore begins with some background reasoning.

This observation does not make formalization circular. We distinguish the mathematical theory under investigation from the methods used to specify and study it. The important question is how much strength a particular metatheorem requires.

Primitive recursive arithmetic, or PRA, is a prominent formal account of a substantial portion of finitary reasoning. William Tait later defended an influential identification of finitist reasoning with primitive recursive methods. Other analyses have drawn the boundary differently.

It is consequently better to say that PRA is a significant precise account used in assessing the program than to say that Hilbert simply defined finitism to mean PRA. Historical intentions and later formal reconstructions are related but not identical.

The note on apparent circularity in logic textbooks develops the distinction between object theory and metatheory. Here its role is specific: the credibility and strength of a consistency proof depend on the resources permitted in the external argument.

The impact of incompleteness

Gödel's 1931 results imposed a severe limitation on the original ambition. Under the appropriate hypotheses, a consistent effectively axiomatized theory sufficiently strong for arithmetic cannot prove its own standard consistency statement.

To connect this with Hilbert's program, an additional step is needed. If the proposed finitary consistency argument can be formalized inside the theory being justified, then such an argument would yield the forbidden internal consistency proof. The assessment therefore depends partly on the relationship between the proposed finitary methods and the formal resources of the object theory.

This is more precise than saying that Gödel proved mathematics could never be justified. Stronger theories can establish consistency statements for weaker ones. Restricted programs of reduction, conservativity, and proof interpretation remain possible. The question becomes which resources justify which systems.

Gentzen's later consistency proof for arithmetic illustrates the change. It uses a form of transfinite induction whose strength must be examined openly. The proof provides important information even though it does not satisfy the original hope for a straightforward finitary justification of all the desired mathematics.

A continuing research program

Hilbert's program did not achieve its original objective in its unrestricted form. It nevertheless transformed what could count as a mathematical question.

Proofs could be compared by strength and transformed by explicit procedures. Logical systems could be studied for conservativity and interpretability. Particular mathematical theorems could be analyzed to determine which axioms they actually need.

The resulting methods contributed to proof theory, computability, and eventually mechanized reasoning. Their value does not depend on presenting later proof assistants as the inevitable fulfillment of Hilbert's intentions.

The competing constructive response also remained productive. Rather than justify unrestricted classical reasoning from outside, it reconsidered the meaning of mathematical assertion itself. The next note follows that change in the understanding of proof and existence.

Sources and further reading

• David Hilbert, “Mathematical Problems” (1900), especially the second problem; “Neubegründung der Mathematik” (1922); and “Über das Unendliche” (1926).
• David Hilbert and Paul Bernays, Grundlagen der Mathematik, volumes I and II (1934, 1939).
• Wilhelm Ackermann, “Begründung des ‘tertium non datur’ mittels der Hilbertschen Theorie der Widerspruchsfreiheit” (1924).
• William W. Tait, “Finitism” (1981), for an influential later analysis rather than a definition simply attributed to Hilbert.
• Hilbert's Program, for the changing formulations, collaboration, and assessment of the program.