Gentzen and the Structure of Proof

The early study of formal proof often treated a derivation as a sequence of formulas following from axioms. Gerhard Gentzen developed calculi that exposed more of a proof's internal organization. His work of 1934–1935 introduced natural deduction and sequent calculi, making the use of assumptions and the structure of inference more visible.

This provided new methods after the limitations established by Gödel. A proof could be transformed, simplified, and assigned a measure. The strength needed to justify those transformations could itself be investigated.

The connection with the theory of computation would become increasingly important, but Gentzen's immediate questions concerned deduction and consistency.

Natural deduction and temporary assumptions

Ordinary mathematical arguments frequently begin by making a temporary assumption. To prove $A\to B$, assume $A$, derive $B$, and discharge the assumption.

Natural deduction records that organization explicitly. In a simple example, assume $A$, then assume $B$. The original assumption $A$ remains available. Discharging $B$ gives $B\to A$; discharging $A$ gives

The point is not that the formula was previously unknown. The proof's structure now mirrors the introduction of its logical operations.

Each connective has characteristic rules. To introduce $A\land B$, supply proofs of $A$ and $B$. To eliminate a conjunction, extract a conjunct. To introduce $A\to B$, construct a derivation of $B$ under assumption $A$. To eliminate an implication, apply it to a proof of its antecedent.

Stanisław Jaśkowski independently developed a natural-deduction approach in the same period. His contribution is an important reminder that the move toward explicit management of assumptions was not confined to one calculus or one researcher.

A proof detour and its removal

Suppose we have derivations of $A$ and $B$. Introduce $A\land B$, then immediately eliminate the conjunction to obtain $A$:

The intermediate conjunction is unnecessary. The original derivation of $A$ already supplies the conclusion.

Implication gives a more informative example. Suppose a derivation of $B$ uses a temporary assumption $A$. We discharge that assumption to obtain $A\to B$, then apply the implication to a separate proof of $A$.

The detour can be removed by substituting the separate proof of $A$ into each relevant use of the temporary assumption. The result is a direct derivation of $B$.

This substitution may duplicate parts of a proof when an assumption is used more than once. It may also eliminate a supplied proof when the assumption was unused. Such details become central in the later analysis of normalization and resource-sensitive logics.

Natural-deduction normalization establishes, for specified calculi, that proofs can be transformed to remove relevant detours. It is a theorem about a system with precise rules, not a claim that every informal mathematical argument has one uniquely simplest presentation.

The following exercise puts these rules to work in a proof tree. Begin with the conclusion, apply a rule to expose its premises, and close each branch with an assumption that is in scope. A separate example shows an introduction–elimination detour and its removal.

Sequents display the inferential context

A sequent has the form

In a classical interpretation, it says that if all formulas in the antecedent $\Gamma$ hold, at least one formula in the succedent $\Delta$ holds. An empty succedent therefore expresses that the antecedent assumptions cannot all hold.

Gentzen's classical calculus permits multiple formulas on the right. His intuitionistic calculus restricts the right side to at most one formula. The difference gives a structural way to distinguish the logics.

Rules describe how a connective is introduced on either side of a sequent. Structural rules describe how assumptions and conclusions may be rearranged, duplicated, or weakened.

The separation matters. Some logical systems alter the connectives or their semantics; others restrict structural rules. Linear logic will exploit this latter possibility.

The cut rule

A simple form of cut is

It expresses the use of an intermediate result. Derive $A$, then use $A$ as a lemma in obtaining $B$.

Lemma use is indispensable to readable mathematics. Why investigate a calculus without cut?

The question concerns what the rule adds to derivability. Gentzen's cut-elimination theorem shows that, for the relevant pure logical calculi, a derivation using cut can be transformed into a derivation without it.

The proof proceeds by reorganizing cuts and reducing their complexity. If a cut formula has just been introduced on both sides, the compound cut can often be replaced by cuts involving simpler formulas. Other cases move a cut through surrounding inferences. A suitable induction shows that the process can be completed.

The theorem does not recommend that working mathematicians eliminate every lemma from exposition. The transformed proof can be much larger. Its value is analytical: it reveals that the intermediate rule is not needed to obtain the final consequence.

Subformulas and consistency

Cut-free proofs in suitable calculi have a subformula property, with the appropriate qualifications for quantified formulas and substitution. Their formulas are controlled by the structure of the end sequent.

This can establish consistency for pure logic. There is no cut-free proof of the empty sequent from no assumptions in the standard system: neither an initial identity sequent nor the logical rules supplies such a conclusion.

The property also supports interpolation results and organized proof search. It limits which logical shapes must be considered when searching backward from a goal.

It does not make arbitrary first-order reasoning decidable. Quantified reasoning can require infinitely many candidate term instances, and the search need not terminate. Nor can a theorem about pure logical cut elimination be transferred without argument to an arbitrary theory with additional axioms and induction principles.

The relationship between proof transformation and mathematical strength becomes especially clear in arithmetic.

Ordinal measures and Gentzen's consistency proof

Gentzen's 1936 consistency proof for arithmetic used transfinite induction along an ordering of ordinal notations below epsilon-zero, written $\varepsilon_0$.

Ordinals describe order types of well-ordered structures. After the finite ordinals comes $\omega$, followed by order types such as $\omega+1$, $\omega\cdot2$, and $\omega^2$. Their arithmetic describes the organization of well-orders and is not generally commutative.

The ordinal $\varepsilon_0$ is the least fixed point of

It is approached by the sequence

Finite notations can represent the ordinals needed in the proof. Gentzen assigns measures of this kind to derivations and shows that appropriate reductions decrease the measure.

The contradiction would require an impossible reduction behavior if the notation ordering is well founded. The external transfinite-induction principle therefore supplies the crucial justification.

This is not a counterexample to the second incompleteness theorem. The uniform well-foundedness principle used in the argument is stronger than what Peano arithmetic can establish in the required form. The proof explains a relative justification and identifies its additional strength.

Proof theory after Gentzen

Later ordinal analysis investigated stronger systems and more elaborate measures. Kurt Schütte and Gaisi Takeuti developed methods for analyzing substantial fragments of mathematics. Solomon Feferman and Schütte's work made $\Gamma_0$ a landmark in formal analyses of predicativity.

Such ordinals should not be presented as universal numerical scores assigned to philosophical positions without qualification. A proof-theoretic ordinal depends on the formal system and on how the analysis relates its principles to well-ordering claims.

Another line studies interpretations that extract information from proofs. Gödel's Dialectica interpretation reorganizes statements of arithmetic through functionals. Georg Kreisel developed influential approaches to unwinding proofs and understanding the constructive content of classical arguments.

Later proof mining uses such methods to obtain effective bounds and quantitative information. A proof that establishes existence by classical means may still contain extractable information, provided the interpretation and the form of the conclusion are examined carefully.

This complicates the simple opposition between constructive and nonconstructive mathematics. Computational information can sometimes be recovered through a transformation of a proof, rather than being displayed directly in its original presentation.

Reverse mathematics: which axioms does a theorem need?

Reverse mathematics changes the direction of the usual foundational question. Instead of selecting a strong axiom system and deriving many theorems, begin with an ordinary theorem and ask which additional axioms are equivalent to it over a weak base.

Harvey Friedman initiated the program in the 1970s; Stephen Simpson and many others developed its systematic form in subsystems of second-order arithmetic.

For example, weak König's lemma asserts that every infinite binary tree has an infinite path. Over a standard weak base such as $\mathsf{RCA}_0$, this principle is equivalent to appropriately formalized compactness results, including a form of the Heine–Borel theorem for countable rational-open covers of a closed interval.

The significance is not merely that compactness can be proved from a tree principle. The reverse implication shows that the theorem already contains the strength of that principle relative to the chosen base.

The base theory and coding conventions are essential. An equivalence established there is more informative than an unrestricted claim that two theorems “say the same thing.”

Proof structure as a source of information

Gentzen's work made the organization of a derivation mathematically productive. A proof could reveal which formulas are necessary, which rules are eliminable, which induction principles justify its transformations, and what computational information can be extracted.

These questions remain distinct from whether a sentence is true in a structure. The semantic side also developed into an independent mathematical field with its own methods and applications.

The next note follows that development: how first-order tools came to illuminate algebraic structures, definability, and classification rather than only the limits of formal foundations.

Sources and further reading

• Gerhard Gentzen, “Untersuchungen über das logische Schließen” (1934–1935) and “Die Widerspruchsfreiheit der reinen Zahlentheorie” (1936).
• Stanisław Jaśkowski, “On the Rules of Suppositions in Formal Logic” (1934).
• Kurt Gödel, “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes” (1958), for the Dialectica interpretation.
• Kurt Schütte, Proof Theory; Gaisi Takeuti, Proof Theory; and the work of Feferman and Kreisel on predicativity and proof interpretation.
• Stephen G. Simpson, Subsystems of Second Order Arithmetic, for the precise setting of reverse-mathematical equivalences.
• The Development of Proof Theory, for the connections and differences among these programs.