Every derivation is a term

Natural deduction proves an implication by assuming its antecedent, deriving its consequent, and then withdrawing the assumption. The bookkeeping is the hard part — which assumptions are still open at each step, and which step withdraws which — and a derivation is only correct if every assumption it made has been paid back by the end.

That bookkeeping has a notation of its own, and the notation turns out to be more than bookkeeping.

A derivation in this fragment of logic is a term, and the formula it proves is the term’s type. The term at the bottom of the figure, $\lambda h_1.\ \lambda h_2.\ (\pi_2\, h_1)\,((\pi_1\, h_1)\, h_2)$, is the whole derivation written on one line, and it can be read back into the tree without losing anything. That is the correspondence named after Haskell Curry and William Howard, and the figure measures it rather than quoting it.

A name for every assumption #

The translation is one rule per rule of inference, and each is short.

An assumption is a variable. The derivation’s assumptions are already named — $h_1$, $h_2$ — so that a discharge can say which one it withdraws, and the name is the term.

Using an implication is applying it. The rule that takes $A \to B$ and $A$ and concludes $B$ becomes the term $f\,a$, where $f$ is the term for the implication and $a$ the term for its antecedent. Modus ponens, the oldest rule in logic, is function application.

Discharging an assumption is abstracting over it. The rule that derives $B$ from an assumption $h$ of $A$ and concludes $A \to B$ becomes $\lambda h.\ b$. The variable $h$ is free in $b$, where the assumption was open, and bound in $\lambda h.\ b$, where it has been withdrawn. An open assumption is a free variable, and a derivation with nothing left open is a term with no free variables at all.

A conjunction is a pair, $\langle a, b \rangle$, and its two elimination rules are the two projections. A disjunction is a tagged value — $\iota_1\, a$ or $\iota_2\, b$, saying which side was proved — and using one is a case analysis with a branch for each tag.

Checked twice, by procedures that share nothing #

The figures do not build the term and then trust it. They check the derivation by the rules of natural deduction, tracking which assumptions are open, exactly as the derivation checker does. Separately, they compute a type for every term by a procedure that reads only the term and the types written on its λs: a variable’s type is looked up, an application’s is read off the function’s type, a pair’s is the conjunction of its parts.

At every node, the type computed from the term is required to be the formula the derivation has there, with the assumptions still open at that node as the only context. In the first figure that is nine agreements and in the second fourteen. A derivation with a misapplied rule would fail the first check and a term with a type error would fail the second, and neither check looks at the other’s material.

That agreement is the correspondence, and it says something more practical than it sounds. Checking a proof and checking the type of a term are the same work. A system that can decide whether a term has a given type can decide whether a derivation proves a given formula, which is how proof assistants built on this idea check proofs: the proof is written as a term, and the checker type-checks it.

Where the correspondence stops #

The fragment is implication, conjunction and disjunction, and the figures enforce the boundary.

The derivation of contraposition uses the negation rule, which concludes $\lnot A$ from a derivation of a formula and its denial under the assumption $A$. Asked to write that derivation’s term, the figure refuses, and the refusal names the rule: the negation rule has no term in this fragment. It is not that nobody wrote one down. The rules that have terms are exactly the ones whose conclusions carry the evidence for themselves — a pair carries both halves, a tagged value carries one side — and a classical negation rule concludes something without any such evidence.

The correspondence is with intuitionistic logic, the logic without the law of excluded middle, and the proofs it leaves out are exactly the ones that establish a disjunction without saying which side holds or an existence without exhibiting a witness. Classical reasoning can be given terms, but only by adding constructs that do something other than build and take apart values, and the clean correspondence with a derivation checked by the ordinary rules is lost in the process.

That makes the refusal informative rather than a gap. The fragment in which every proof is a term is the fragment in which every proof contains its own evidence, and the negation rule is the first rule outside it.

Two proofs that the tree cannot tell apart #

The term records something the drawn derivation leaves to its labels, and it is the thing that makes proofs countable objects rather than yes-or-no facts.

Take the formula $p \to (p \to p)$. A derivation of it assumes $p$, assumes $p$ again, and concludes $p$. Drawn as a tree, that is two discharges over a single leaf $[p]$ — and nothing in the shape of the tree says which assumption the leaf is. The labels do, and the two choices give the terms $\lambda x.\ \lambda y.\ x$ and $\lambda x.\ \lambda y.\ y$. They are two different proofs of the same formula: one uses the first assumption and ignores the second, the other the reverse. Neither contains a detour, and they are the only two proofs of that formula that do not.

Some formulas have infinitely many. A proof of $(p \to p) \to (p \to p)$ without detours assumes a way $f$ of getting from $p$ to $p$ and a $p$ called $x$, and must produce a $p$. It can return $x$ itself; it can apply $f$ once, $f\,x$; or twice, $f\,(f\,x)$; or any number of times. The terms $\lambda f.\ \lambda x.\ f\,(f\,(\cdots(f\,x)\cdots))$ are all proofs of the formula, all different, and every proof without detours is one of them — so the proofs of this one small formula are exactly the whole numbers, each counting how often the assumed implication is used.

Truth tables see none of this. Both formulas are true in every row, and a formula is either a theorem or not. The term reading makes a proof an object with parts that can be counted and compared, and it is what gives the question of when two proofs are the same — the last question on this page — something to be about.

A detour is a lemma used once #

A derivation can prove an implication and then immediately use it. That is legal, and it is a detour: the proof introduces $A \to B$ only to eliminate it on the next line.

In the term, a detour is visible at a glance: an abstraction applied directly to an argument, $(\lambda f.\ \ldots)\, (\ldots)$. A detour in the derivation is exactly a term that can be simplified, and the simplification is the one every reader of algebra already knows — substitute the argument for the variable. The same holds for the other connectives: a pair built and immediately projected, $\pi_1 \langle a, b\rangle$, simplifies to $a$, and a tagged value immediately taken apart by cases simplifies to its branch.

This is the natural-deduction form of the cut the sequent calculus removes. A cut proves a lemma and then uses it; a detour introduces a formula and then eliminates it. The formula $(p \to p) \to p$ in the figure is such a lemma, and it is not a subformula of the goal $p \to p$ — which is exactly the property the cut-free proof was defined by having.

Removing the detours, one at a time #

Each step replaces a rule immediately undone by the rule after it with the direct derivation the pair was hiding. The formula proved never changes — removing a detour is a rewrite of the proof, not of what it proves — and the figure checks that by type-checking every intermediate term against the goal.

When no detour is left, the derivation has the subformula property: every formula in it is a part of the goal or of an open assumption. The figure checks that too, reading the formulas off the final term. That is Dag Prawitz’s normalisation theorem for natural deduction, from 1965, and it is Gerhard Gentzen’s elimination of cuts restated for the system Gentzen designed first and set aside because he could not prove the result for it directly.

What a proof without detours cannot be #

The theorem that detours can be removed has a consequence that was, for Gentzen, the point of the whole enterprise.

Look at how a term with no detour and no free variable can begin. It cannot be a variable, because a closed term has none free. It cannot be an application, a projection or a case analysis, because each of those takes apart something — an implication, a pair, a tagged value — and in a term with no detours and no free variables the thing being taken apart would itself have to be built by an introduction, which would make the combination a detour. So a closed term with no detours begins with an introduction: a $\lambda$, a pair or a tag. Its type is therefore an implication, a conjunction or a disjunction — never a bare atom.

That settles two questions at once. No derivation proves an atom from no assumptions, since its term would have to simplify to a closed term with no detours whose type is an atom, and there is no such term. The fragment cannot prove $p$ outright, and in particular it cannot prove everything: it is consistent, and the proof is a statement about the shape of normal terms rather than about any model. Gentzen proved the consistency of arithmetic in 1936 by an argument of the same kind, carried much further, which is the result the sentence that says it has no proof is the limit of.

And a proof of a disjunction says which side holds. A closed term of type $A \lor B$ with no detours begins with a tag, so it is $\iota_1\, a$ with $a$ a proof of $A$, or $\iota_2\, b$ with $b$ a proof of $B$. Every proof of $A \lor B$ simplifies to a proof of one of the two. That is the disjunction property of intuitionistic logic, and it is the formal version of the sentence above about proofs carrying their evidence: classical logic proves $p \lor \lnot p$ for every $p$ without proving either side, and the property fails there for exactly that reason.

Longer before shorter #

Removing a detour does not always shorten the term.

The growth has a plain cause. The variable $k$ occurs twice in $\langle \pi_2\, k,\ \pi_1\, k\rangle$, and substituting $\langle \pi_1\, h,\ \pi_2\, h\rangle$ for it copies the argument into both places. A proof that uses a lemma twice, once the lemma is expanded in place, contains its proof twice.

So the obvious measure of progress — the size of the proof — does not fall at every step, and the standard way to show a process stops, a quantity that always decreases, needs a subtler quantity. The one that works is the size of the largest formula that is introduced and at once eliminated. Removing a detour of that size, chosen so that nothing inside its argument is a detour of the same size, can create new detours, but only on smaller formulas, and a count of the largest detours by size falls with every step. The proof may get longer; its worst detour never gets worse, and that is enough for the process to end.

In a richer logic the cost of ending can be enormous. Expanding every lemma in place can multiply a proof’s length by a tower of exponentials, and that growth is not a defect of the method: a short proof with lemmas and a proof without any are genuinely different objects, as the number of pieces a dissection needs and the existence of a dissection are different facts.

Where the correspondence came from #

Curry noticed in 1934 that the types of two basic combinators — one that discards an argument and one that distributes an argument over an application — are exactly the two axioms of the usual Hilbert-style system for implication, and that the rule combining combinators matches modus ponens. That is the correspondence for the axiomatic system, stated as a curiosity.

Howard wrote it down for natural deduction in a manuscript circulated in 1969 and published in 1980, and he added the observation that makes it a theorem rather than a matching of tables: reducing a term corresponds step for step to Prawitz’s normalisation of the derivation. Around the same time Nicolaas de Bruijn built the Automath system in the Netherlands, in which mathematical proofs were written as typed terms and checked by a machine, and Per Martin-Löf extended the correspondence to quantifiers with types that depend on terms.

What was a pair of parallel formal systems became a single system with two readings. A derivation read one way is a proof, read the other way a term, and the rules of each are the rules of the other.

Where the account needs care #

The terms carry their types on their abstractions. Every $\lambda$ in the figures is annotated with the formula of the assumption it discharges, taken from the derivation. Without the annotations a term can have many types or none, and recovering them is a separate problem.

Substitution must not capture a variable. Substituting a term into the body of an abstraction whose bound variable is free in that term would change its meaning. The figures refuse such a substitution rather than renaming, and none of their examples needs one; a general implementation renames.

The reductions are done in one order. The figures always simplify the leftmost outermost detour. That every order ends, and that every order ends at the same term, are theorems — strong normalisation and confluence — which the figures quote and do not show.

And the correspondence has been drawn for propositional logic only. Quantifiers have terms too, in type theories where a type can mention a term, and the essay on the universal that has to be instantiated is where that setting’s difficulties start.

Five derivations drawn, and an induction for the rest #

Five derivations are drawn, and the correspondence is a statement about every derivation in the fragment. The node-by-node agreement is checked for the five; the theorem that it holds for all is the definition of the translation plus an induction on derivations, which is prose.

The pictures also show terms as text. The structure a term shares with its derivation — a subterm for each subderivation — is drawn only by writing each subterm under its own formula, and the reader has to see that the root’s term contains all the others.

Still open: when two proofs are the same proof #

The correspondence gives a natural answer to a question that sounds as if it should have one: two derivations are the same proof if their terms simplify to the same term. For intuitionistic logic that criterion is well behaved and matches a precise mathematical structure.

For classical logic no comparably satisfactory answer is known. Every obvious way of extending the criterion to classical derivations identifies far too much — in one standard framework it makes all proofs of the same formula equal, so the notion of proof collapses to the notion of provability. Rüdiger Thiele found in David Hilbert’s notebooks a problem Hilbert had considered adding to his famous list of 1900, asking for criteria of simplicity of proofs and for when two proofs are essentially the same; it is now called Hilbert’s twenty-fourth problem, and it has no accepted solution.

Two checks that were one check #

The habit is about noticing when agreement is identity.

The figures check each derivation twice, once by the rules of inference and once by typing its term, and the two checks agree at every node. It would be possible to treat that as reassurance — two independent methods confirming each other. But the agreement is not a coincidence to be grateful for; it is a sign that the two checks are one procedure written twice, and the correspondence is the statement of which pieces match.

When two methods that were designed separately agree on every case, the useful question is not how likely that was but what single structure both are describing. Here the answer turned proofs into objects that can be computed with, simplified and compared — and it came from taking a coincidence of notation seriously.