Proof Theory

What Is Proof Theory?

Every mathematical proof begins with certain assumptions from which, through extremely precise reasoning, we derive a statement with sufficient certainty. Together, these steps constitute a proof of that statement. Hilbert’s aim was to provide a rigorous definition of mathematical proof and then use it to investigate the nature and properties of the knowledge acquired through proof. If, by directing scientific inquiry toward proofs themselves, we can demonstrate that their use gives rise to a consistent system free of contradictions, then we will be able to dispel doubts concerning possible paradoxes in some of the most fertile areas of Mathematics.

Formal Mathematics

Hilbert maintains that every branch of Mathematics can be conceived as a structure of formulas expressing our knowledge of that field. Thus, a statement such as “two equal numbers have the same predecessor” can be translated into a formula such as \((a=b)\rightarrow(\delta(a)=\delta(b))\). This procedure allows us to translate the content of statements—that is, their intuitive meaning—into an ordered collection of symbols.

These formulas are themselves objects of study. In Proof Theory, deduction based on meaning is replaced within the formal system by the manipulation of symbols. Beginning with elementary formulas and applying deductive rules that specify with complete precision how such symbolic manipulation must be carried out, we can generate new formulas reflecting new mathematical content.

Thus, every provable formula results from applying the rules of inference a finite number of times, beginning from one or more axioms. Not every well-formed formula is therefore a theorem. A proof is a finite sequence of formulas: each formula is an axiom, an instance obtained by substitution, or a consequence of earlier formulas produced by an accepted rule of inference. The final formula is the statement proved. In Hilbert’s words, we transform a mathematical theory into an inventory of formulas.

Metamathematics

Once a mathematical theory has been formalized as a structure of formulas, Proof Theory seeks to study the properties of that structure, such as its consistency. For Hilbert, mathematical science therefore alternates between two modes of inquiry: a formal one, limited to the manipulation of symbols according to explicit rules, and another grounded in meaningful content and in our intuitive understanding of finite objects.

The latter is the Metamathematics to which Hilbert appeals in order to prove the consistency of formalized Mathematics. Metamathematics is not part of the system it seeks to study, but this does not mean that it may employ arbitrary forms of reasoning. Hilbert requires its proofs to use finitistic procedures: elementary operations on signs and finite sequences of signs whose correctness can be recognized directly. In this article, we will examine the different mechanisms of deduction operating at both levels.

The Consistency Problem

In classical logic, an inconsistent system allows any formula to be derived. This is the principle of ex falso quodlibet. The basic form of a contradiction is as follows:

$$A\land\neg A$$

Suppose we have proved both \(A\) and \(\neg A\). Propositional calculus includes the schema:

$$A\rightarrow(\neg A\rightarrow B)$$

Applying the rule of modus ponens twice, we first obtain \(\neg A\rightarrow B\) and then \(B\), regardless of what formula \(B\) may be. Thus, in an explosive logic, a single contradiction makes it possible to prove any statement.

In other words, either the system is consistent or, if it contains a contradiction, all its formulas become provable. A single contradiction causes the entire system to collapse. Hilbert uses a specific contradictory expression: \(0\neq0\). Proof Theory therefore aims to demonstrate metamathematically that \(0\neq0\) is unprovable in an axiomatic system formalizing Arithmetic.

The Formal System of Arithmetic

The first step in Proof Theory and in proving the consistency of Arithmetic is, as we have indicated, to transform this branch of Mathematics into a collection of formulas or strings of symbols. This requires a language that determines the possible symbols, the legitimate ways of combining them, and the rules for obtaining new expressions. All of this must reflect our intuitive understanding of the nature of numbers.

The Language of Arithmetic

The first step in constructing this repertoire of formulas reflecting the principles of Arithmetic is to determine which signs it will include and how they may be combined.

These include numerical signs (\(2\), \(15\), etc.), as well as functions (\(f(*)\), \(g(*)\), etc.) that may be completed by other numerical or functional signs. The language also incorporates signs that designate these objects indeterminately—that is, variables: Latin letters (\(a\), \(b\), \(c\), etc.) for numerical signs and Greek letters (\(\psi(*)\), \(\varphi(*)\), \(\mu(*)\), etc.) for functions. Together, all of these constitute the terms of the language.

When we place two of these terms on either side of the symbol \(=\) or \(\neq\), we obtain an elementary formula, what we ordinarily call an equation or an inequality. Hilbert’s system also includes the signs \(\rightarrow\) and \(\neg\), which, when applied to elementary formulas, make it possible to form more complex formulas. The system likewise permits the use of variables representing complete formulas. For these, we use uppercase Latin letters (\(A\), \(B\), etc.).

The Axioms of Arithmetic

Throughout the 1920s, as Hilbert developed his Proof Theory, the axiomatic systems he presented changed with each new publication. Here we reproduce the core of the system appearing in the 1923 article “The Logical Foundations of Mathematics,” by which time Proof Theory had already reached a certain degree of maturity.

We will present ten axioms combining principles of Propositional Logic and Arithmetic. The first six axioms govern the use of the logical symbols of implication \(\rightarrow\) and negation \(\neg\). The final four belong specifically to Arithmetic and regulate the signs \(=\) and \(\neq\), together with the function \(\delta(*)\), which we may interpret as “the predecessor of.”

I \(A\rightarrow(B\rightarrow A)\)

II \((A\rightarrow(A\rightarrow B))\rightarrow(A\rightarrow B)\)

III \((A\rightarrow(B\rightarrow C))\rightarrow(B\rightarrow(A\rightarrow C))\)

IV \((B\rightarrow C)\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))\)

V \(A\rightarrow(\neg A\rightarrow B)\)

VI \((A\rightarrow B)\rightarrow((\neg A\rightarrow B)\rightarrow B)\)

VII \(a=a\)

VIII \((a=b)\rightarrow(A(a)\rightarrow A(b))\)

IX \(a+1\neq0\)

X \(\delta(a+1)=a\)

Substitution

How can new formulas be generated from these axioms? Hilbert establishes two different procedures. The first consists in replacing variables with determinate terms. Thus, from axiom VII, \(a=a\), we may obtain by substitution the equation \(1=1\) or the formula \(\delta(a)=\delta(a)\).

To illustrate how substitution works, we can use axioms III and VIII. If in axiom III we replace \(A\) with \(a=b\), \(B\) with \(A(a)\), and \(C\) with \(A(b)\), we obtain:

$$\bigl((a=b)\rightarrow(A(a)\rightarrow A(b))\bigr)\rightarrow\bigl(A(a)\rightarrow((a=b)\rightarrow A(b))\bigr)$$

This new formula is an instance of axiom III obtained solely by substitution.

Modus Ponens

The second procedure consists in following the inference schema known as modus ponens, which, using Fraktur letters to denote arbitrary formulas of our language, is expressed as:

$$\frac{\mathfrak{A}\qquad\mathfrak{A}\rightarrow\mathfrak{B}}{\mathfrak{B}}$$

In ordinary language, this means that if the formula \(\mathfrak{A}\) has been proved and the implication \(\mathfrak{A}\rightarrow\mathfrak{B}\) has also been proved, then we may prove \(\mathfrak{B}\). The expressions above the line are known as premises, while the expression below it is the conclusion or final formula.

Note the use of Fraktur letters. This is because the inference schema is not a formula of the arithmetic system, but a metamathematical expression used to describe the procedure by which new formulas are generated within the system.

Continuing with the example, we first have axiom VIII:

$$(a=b)\rightarrow(A(a)\rightarrow A(b))$$

And the instance of axiom III obtained earlier:

$$\bigl((a=b)\rightarrow(A(a)\rightarrow A(b))\bigr)\rightarrow\bigl(A(a)\rightarrow((a=b)\rightarrow A(b))\bigr)$$

Applying modus ponens, we obtain:

$$A(a)\rightarrow((a=b)\rightarrow A(b))$$

The final formula has therefore been proved.

Transfinite Arithmetic

The axioms presented above make it possible to formalize an elementary part of Arithmetic, although developing the complete theory of the natural numbers requires the addition of principles of induction and rules for defining functions recursively. In any case, this language remains insufficient if we seek to extend Proof Theory to Analysis and the real numbers.

We can observe that the axioms above contain no quantifiers—that is, signs allowing statements to be made about all objects in a domain or about the existence of some object within it. Yet, as we saw in the articles devoted to Cantor and Dedekind, defining irrational numbers and the continuum requires us to work with infinite sequences and sets of rational numbers.

Transfinite Reasoning

We need to introduce a tool that allows us to represent, through finite operations on symbols, the forms of reasoning applied to infinite collections that occur in Arithmetic and Analysis. The customary resource was the use of the quantifiers “for all” \(\forall\) and “there exists” \(\exists\).

As we have repeated several times throughout this series, there is a difference between including an open formula such as \(a=a\), in which \(a\) may be replaced by any term, and explicitly asserting:

$$\forall a\lbrack a=a\rbrack$$

The latter formula is still a finite expression, but it asserts something about an infinite totality. Hilbert, like many before him, had warned of the danger of extending without justification forms of reasoning appropriate to finite collections to infinite totalities.

The Law of Excluded Middle

The Law of Excluded Middle, or tertium non datur, states that, given a proposition \(A\), \(A\lor\neg A\) holds. Applied to a property defined over a collection of objects, it allows us to assert:

$$\forall a\,A(a)\lor\exists a\,\neg A(a)$$

This principle is relatively unproblematic for finite collections and decidable properties: we can examine every object and conclude either that the property holds for each of them or that a counterexample exists.

The situation changes when the principle is applied to infinite collections. If we inspect the natural numbers one after another and there exists a number that does not satisfy \(A\), a systematic search will eventually find it. But if every number satisfies \(A\), the search for a counterexample will never, by itself, reach a final stage at which this can be established.

Despite the controversy surrounding the Law of Excluded Middle, Hilbert’s concern was not so much to resolve all its philosophical implications as to demonstrate that including it in formal mathematics posed no threat to consistency. This was one of the aims of his Proof Theory.

The Transfinite Function

Hilbert introduces a new operator representing the search for a possible counterexample to a property, whether the domain is finite or infinite. This operator is known as the transfinite function \(\tau(*)\). We may understand \(\tau(A)\) as a “counterexample-search operator”: if there is an object for which the property \(A\) fails, \(\tau(A)\) must select one; if there is none, it may designate an arbitrary object.

In Hilbert’s own words: “Let \(A\) be the predicate ‘bribable.’ Then \(\tau(A)\) would be a man defined as possessing such an unwavering sense of justice that, if he turned out to be bribable, then in fact all men would be bribable.”

Thus, \(\tau(A)\) represents the putative counterexample to the property \(A\). If the property holds even for this possible counterexample, then it holds for every object:

$$A(\tau(A))\rightarrow A(a)$$

We can use \(\tau(*)\) to construct expressions equivalent to those provided by the quantifiers of first-order logic:

$$A(\tau(A))\equiv\forall a\lbrack A(a)\rbrack$$

$$A(\tau(\neg A))\equiv\exists a\lbrack A(a)\rbrack$$

In the second expression, \(\tau(\neg A)\) searches for a counterexample to the property \(\neg A\); that is, it searches for an object satisfying \(A\).

The Transfinite Axiom

The transfinite function is incorporated into the formal system through a new axiom added to the previous ten and known as the Transfinite Axiom. Suppose we have a numerical function \(f\) and consider the property \(f(a)=0\). The term \(\tau(f)\) represents a possible counterexample to that property. If there is some number \(a\) for which \(f(a)\neq0\), \(\tau(f)\) must designate one such number. If no counterexample exists, the chosen value is irrelevant.

We may therefore interpret:

$$f(\tau(f))=0\equiv\forall a\lbrack f(a)=0\rbrack$$

$$f(\tau(f))\neq0\rightarrow\exists a\lbrack f(a)\neq0\rbrack$$

If the function returns \(0\) even when applied to the possible counterexample \(\tau(f)\), then it returns \(0\) for every number \(a\). This gives us the new axiom introduced by Hilbert:

XI \((f(\tau(f))=0)\rightarrow(f(a)=0)\)

It should be clear that this axiom does not necessarily provide an effective procedure for deciding in a finite number of steps whether \(f(a)=0\) holds for every number. Its role is to introduce into the formal system the classical reasoning associated with the tertium non datur when applied to infinite totalities.

The Epsilon Calculus in Proof Theory

Hilbert and Bernays soon replaced the counterexample-detecting operator \(\tau(*)\) with its dual operator, the “witness operator” \(\varepsilon(*)\)—epsilon. Wilhelm Ackermann, a student of Hilbert, would later develop the substitution procedure intended to eliminate these operators from proofs.

The principles motivating the \(\varepsilon\)-calculus are closely related to the Law of Excluded Middle and the Axiom of Choice. This operator makes it possible to simplify the formal logical-arithmetic system without sacrificing expressive power.

\(\varepsilon A\) designates an object satisfying the property \(A\), if one exists. If no object satisfies it, the term may designate an arbitrary object. Like \(\tau(*)\), it can be used to replace quantifiers:

$$\forall a\lbrack A(a) \rbrack \equiv A(\varepsilon\neg A)$$

$$\exists a\lbrack A(a) \rbrack \equiv A(\varepsilon A)$$

The Transfinite Axiom then takes the form:

$$A(x)\rightarrow A(\varepsilon A)$$

This formula states that if some object \(x\) satisfies \(A\), then the object selected by \(\varepsilon A\) also satisfies it.

Conclusion

During the first half of the 1920s, Hilbert outlined a strategy for proving the consistency of systems containing transfinite operators. The positive results achieved in his early work applied mainly to formalisms without quantified variables or transfinite operators, which were still too weak to capture the mathematical practice of Analysis.

The problem became far more complex because extending the axiomatic system to Analysis required the introduction of functional variables and second-order \(\varepsilon\)-operators. These resources played a role similar to that of the Principle of Comprehension and required the control of much more complex dependencies among terms.

In 1924, Ackermann believed he had provided a consistency proof for the complete formalism of Analysis. It was soon recognized, however, that his argument was incomplete and worked only under restrictions that substantially reduced the strength of the system.

In 1927, von Neumann presented a more rigorous proof for a fragment of first-order Arithmetic, with induction restricted to quantifier-free formulas. His result improved on earlier techniques, but it still did not establish the consistency of full Analysis sought by Hilbert’s Program.

In any event, by around 1930 the consistency of systems powerful enough to formalize advanced Arithmetic and Analysis remained unresolved.

Recommended Reading

– Hilbert, D. (1923). The Logical Foundations of Mathematics.