Chapter 3: Natural Deduction

Baker works on the payments service of an online shop, and at ten past ten a support ticket lands in her queue: a customer has been charged twice for one order. She doesn’t know why. She has two things to go on. The runbook says that when an attempt to charge a card times out, the app retries it, and that a retry goes to the card network as a fresh charge. The order record says the customer paid at nine fifty-two. So she reasons:

1. The first attempt timed out. supposed

2. If an attempt times out, the app retries it. runbook

3. So the app retried. from 2 and 1

4. If the app retries, the card is charged a second time. runbook

5. So the card was charged twice. from 4 and 3

6. So, if the first attempt timed out, the card was charged twice. from 1–5; the supposition paid off

Look at line 1, and then at line 6. Baker has not found out whether the first attempt timed out. She has found out what follows if it did, and line 6 says so without depending on line 1 at all. It is a rule. She files it in the runbook and goes to look for a timeout in the gateway’s log. That’s how people reason when they don’t know the cause: suppose one, follow it to something you can check, and keep the if when you’re done with the supposition. The clerk, who checks a proof by matching the shape of each line and understands nothing, can’t do this. A hypothesis, for him, is for keeps. The Deduction Theorem lets him pretend otherwise, but each supposition he pays off triples the proof.

In 1934 a young man in Göttingen, Gerhard Gentzen, published a different account of what a proof is, in which line 1 is a permitted move and line 6 is the rule that pays it off.¹ What matters is where he stood in relation to Hilbert. Hilbert had made proofs into mathematical objects and fixed their form as a list. Gentzen was hired to prove theorems about proofs, found the list unusable for the purpose, and built another form. In his own words:²

The formalization of logical deduction, especially as it has been developed by Frege, Russell, and Hilbert, is rather far removed from the forms of deduction used in practice in mathematical proofs. Considerable formal advantages are achieved in return. In contrast, I intended first to set up a formal system which comes as close as possible to actual reasoning. The result was a “calculus of natural deduction”.

“Frege, Russell, and Hilbert” are the three names behind the clerk, and “considerable formal advantages” is a fair description of what the clerk has: three kinds of line and one rule. Gentzen gave those up, and this chapter is about what he got in return. In his system Baker’s six lines are a proof as she wrote them. Put the programs beside the lines and it’s the calculus your compiler reads. And it gives a short answer to the question Gentzen was actually hired to settle: can a logic prove everything, every formula there is, contradictions included? Nearly everything proof theory has done since 1934 has been done in his systems.

3.1 From axioms to rules

Where do Gentzen’s rules come from? From the Deduction Theorem, read backwards. I want to do the reading in public, because it explains both what the rules are and why no axioms are left when it’s done. Nothing in this section is a new definition. We’re still inside the Hilbert system, with its nine axiom schemas and its one rule, modus ponens, and we are proving facts about what it can prove, as we did for reflexivity, monotonicity and transitivity.

Start with how people actually reason. At twenty past ten Baker has checked two things about the first attempt: the card was authorised ($a$), and the capture was posted ($p$). The runbook says that a charge has settled exactly when both hold, so what she needs, to show that the first attempt took the money, is $a\wedge p$, and she gets it the way anyone would:

1. The card was authorised. checked

2. The capture was posted. checked

3. So both. from 1 and 2

The clerk may cite only hypotheses, axioms and modus ponens, so he has to write this:

Nobody thinks of an axiom when they say “so both”. Is Baker’s line 3 a legitimate move all the same? The Deduction Theorem says that it is, and the way it says so is the subject of this section.

Take the schema (pair), $\phi \to (\psi \to \phi \wedge \psi )$: given $\phi$, and then $\psi$, you may have $\phi \wedge \psi$. An axiom is a one-line proof, so $\mathrm{\Gamma }⊢\phi \to (\psi \to \phi \wedge \psi )$ for every $\mathrm{\Gamma }$ at all. Recall the Deduction Theorem:

where $\mathrm{\Gamma },\phi$ is short for $\mathrm{\Gamma }\cup \{\phi \}$. Apply it to the axiom, taking $\psi \to \phi \wedge \psi$ for $\chi$, and then once more:

The arrows have come out of the formula and gone above the line, among the hypotheses. Now suppose Baker has proved both halves, $\mathrm{\Gamma }⊢\phi$ and $\mathrm{\Gamma }⊢\psi$. Transitivity says that a hypothesis you can prove may be replaced by its proof, so she splices each proof in for its hypothesis, and what is left is

The axiom has become a fact with two conditions: a rule, in the sense in which modus ponens is a rule, something you do rather than something you’re told. Every schema can be read this way. Here’s the whole list. The three facts that aren’t readings of axioms — reflexivity, modus ponens and the Deduction Theorem itself — come first.

Read in Baker’s terms, with $t$ for “the first attempt timed out”, $r$ for “the app retried” and $d$ for “the card was charged twice”: item 1 says that what the runbook tells her may be used; item 2, modus ponens, is her lines 3 and 5, from $t\to r$ and $t$ to $r$; and item 3, which turns $\mathrm{\Gamma },t⊢d$ into $\mathrm{\Gamma }⊢t\to d$, is her line 6, the thing the clerk couldn’t do, now a fact about what the clerk can do. If the morning’s reasoning needs and, or and not, as it will, the rest of the list says how: to establish both, establish each; to use a disjunction, handle both cases; from an impossibility, anything.

Look at the proof again, because there’s something in it. Most of the facts were cheap. Those for and, for proving an or, and for $\mathrm{\perp }$ (items 4–8 and 10) cost one schema and a modus ponens or two: the easy half of the Deduction Theorem, and not really the theorem at all. The expensive construction in its proof, the one that triples a proof for every supposition it pays off, was spent in exactly two places: item 3 itself, and the two branches of item 9, proof by cases. Here they are, with the hypothesis in question underlined:

In each, a hypothesis is in a condition and gone from the conclusion. These are the only such facts. They are the facts that discharge a hypothesis. What the Deduction Theorem costs is the cost of discharging. Item 11 is on the list for a different reason. It shows that the two original schemas, read as rules, follow from modus ponens and the Deduction Theorem, so once those two facts are on the list, (I) and (II) aren’t needed.

Gentzen’s observation was this. The facts on the list are how people actually reason: to establish both, establish each; to use an implication, apply it; to prove one, suppose and then discharge. In the Hilbert system they are theorems about proofs, each paid for with axioms and the Deduction Theorem’s construction. He wanted a notation in which they are the proofs, so that an argument set out the way Baker sets hers out is a proof as it stands. The first ten facts are all you need; the eleventh, as we’ve just seen, follows from two of them. Prove with them, cite no axiom ever, and nothing is lost. That’s a theorem, and we’ll prove it as soon as there’s a notation to state it in. And the list has a shape. Each connective appears in two kinds of fact: one that says how to prove a statement with that connective on the outside, and one that says how to use such a statement once you have it.

Nothing proves $\mathrm{\perp }$ outright, so it has only the second kind. Gentzen called the first kind introduction rules and the second elimination rules, and remarked that the eliminations are, in a sense he could not yet make exact, consequences of the introductions: once you know how a statement is established, you know what may be got out of it.³ A logic with no axioms: nine rules for going on, and no way to start except by supposing something. He called the system NJ. The N is for natürlich; the J we’ll come to in Part 2.

3.2 Derivations as trees

A fact such as “if $\mathrm{\Gamma }⊢\phi$ and $\mathrm{\Gamma }⊢\psi$ then $\mathrm{\Gamma }⊢\phi \wedge \psi$” is about three proofs: two given and one built. Gentzen’s notation draws the three as one picture. The two premisses stand side by side above a horizontal bar, the conclusion stands below it, and the bar is labelled on the right with the rule used:

The turnstiles and the $\mathrm{\Gamma }$ are not written. A proof is a tree of such bars, read downwards, and the $\mathrm{\Gamma }$ is whatever sits at its leaves, at the top, written once each; the thing proved is the single formula at the root; and the shape of the tree is the shape of the argument. Here are Baker’s lines 1 to 5, with the supposition still in force, first with the hypotheses $\mathrm{\Gamma }=\{t,t\to r,r\to d\}$ written at every node, and then as Gentzen draws it:

Two bars, both modus ponens (from $A\to B$ and $A$, conclude $B$), which in Gentzen’s names is the elimination rule for $\to$, ($\to$E). Three leaves: $t$, which she supposed, and $t\to r$ and $r\to d$, which the runbook told her. The leaves on the right are the $\mathrm{\Gamma }$ on the left. Nothing in the tree says which of the three she supposed and which she was told, and the next step needs it to.

Discharge

Baker’s line 6 pays off the supposition, and in the Hilbert system it is the Deduction Theorem, with $\mathrm{\Gamma }=\{t\to r,r\to d\}$, the runbook alone. Gentzen draws it as one more bar under the tree:

The new bar is the Deduction Theorem used as a rule, Gentzen’s introduction rule for $\to$, ($\to$I): from a proof of $d$ that supposes $t$, conclude $t\to d$ and stop supposing. The square brackets round the leaf $t$ are a receipt. They say: this was supposed, and the bar marked 1 has paid for it. A leaf in brackets is discharged, as $t$ has left the left of the turnstile. The two runbook sentences are open: they are not in brackets, no bar has paid for them, and the conclusion $t\to d$ rests on them. So the tree establishes $t\to d$ from $\{t\to r,r\to d\}$ and from nothing else. That’s exactly what Baker filed. Which leaves are open and which are discharged is the whole content of the turnstile; the brackets are where the tree keeps it.

And that’s all the notation there is. A proof is a tree. Each bar is one of the facts of the list, drawn as a rule. A leaf is open until a bar below it pays for it, and only two kinds of bar can. What the tree proves is its root, from its open leaves. The definition below says the same thing by recursion on the tree, computing as it goes the set of leaves still open.

Clauses 2 and 7, for ($\to$I) and ($\vee$E), are the only two that take something away from $\mathrm{OH}$: they are the Deduction Theorem and proof by cases, the two facts that discharge. The receipt is clause 2 removing $\phi$ from a set. Every open leaf labelled $\phi$ goes at once, and when $\phi$ was never there, $\mathrm{OH}(\mathcal{D})\setminus \{\phi \}$ is just $\mathrm{OH}(\mathcal{D})$; the examples below show both.⁴ The numbers on the brackets and bars aren’t part of the definition, which says exactly which leaves each clause discharges and needs no labels. They appear in practice because a drawn tree may contain several discharging bars, and the reader has to see which receipt belongs to which. Gentzen numbered his discharges, and so has everyone since.⁵

Examples

Each of the following says which claim $\mathrm{\Gamma }{⊢}_{\mathrm{N}}\phi$ it witnesses, with the open hypotheses computed from the clauses. Where the Hilbert system has a proof to compare, it comes first.

First, the smallest proof there is, $p\to p$. In the Hilbert system it takes five lines, the first of which nobody would write unprompted:

In natural deduction it is one leaf and one bar:

The leaf has $\mathrm{OH}=\{p\}$ by clause 1, and the bar takes $p$ away by clause 2, leaving $\mathrm{OH}=\varnothing$. So the tree witnesses ${⊢}_{\mathrm{N}}p\to p$: it depends on nothing at all. That’s what a theorem is.

Second, swapping a conjunction. In the Hilbert system, from the hypothesis $p\wedge q$:

In natural deduction, three bars, one for each step of the argument:

Both leaves are $p\wedge q$, so $\mathrm{OH}=\{p\wedge q\}$, and the tree witnesses $\{p\wedge q\}{⊢}_{\mathrm{N}}q\wedge p$. Now put one more bar under it, supposing $p\wedge q$ and discharging it:

The supposition appears at two leaves, because it was used twice, and one bar discharges both; they carry the same number. There is nothing to choose here. The supposition was one supposition, however many times it was consulted, and clause 2 removes it from $\mathrm{OH}$ once and for all: $\mathrm{OH}=\varnothing$, and the tree witnesses ${⊢}_{\mathrm{N}}p\wedge q\to q\wedge p$. The Hilbert system gets there from the eight lines only through the Deduction Theorem, which roughly triples them.

Two trees that look like mistakes belong here. Take the last tree and leave the brackets off:

This is still a derivation — the ($\to$I) clause doesn’t require that anything be discharged — but its $\mathrm{OH}$ is $\{p\wedge q\}$, and so it witnesses only $\{p\wedge q\}{⊢}_{\mathrm{N}}p\wedge q\to q\wedge p$, a weaker and sillier claim than the one with the brackets. Forget to discharge and the proof is still right; it just proves less. Next, a tree that looks as if it ought to be wrong:

The last bar concludes $p\to q\wedge p$ by ($\to$I). The clause asks only that the subtree above it conclude $q\wedge p$, which it does, and it discharges $p$, of which there is no leaf. So this is a derivation, by a vacuous discharge, and its $\mathrm{OH}$ is still $\{p\wedge q\}$: it witnesses $\{p\wedge q\}{⊢}_{\mathrm{N}}p\to q\wedge p$, which is right. A tree that is not a derivation has a bar whose premisses do not have the shape its clause requires: a bar labelled $\to$E under $q$ and $p$, say, or $\wedge$I with one premiss. The definition refuses those by having no clause for them, and the clerk refuses them by failing to match a shape.

Next, proof by cases. At half past ten the app’s log says that the gateway answered the second attempt, and the entry is truncated: the answer was a decline or an approval, and the log doesn’t say which. The runbook says that an attempt the gateway has answered, either way, is written to the ledger. With $n$ for “the gateway declined”, $o$ for “the gateway approved”, and $l$ for “the attempt is in the ledger”:

This is proof by cases, ($\vee$E), and here the bracket notation does something no other clause does: it discharges a different formula in each branch, $n$ in the first and $o$ in the second, and neither supposition leaks into the other branch. $\mathrm{OH}=\{n\vee o,n\to l,o\to l\}$: three things the log and the runbook said, and The tree witnesses $\{n\vee o,n\to l,o\to l\}{⊢}_{\mathrm{N}}l$, and Baker goes to the ledger without ever learning which it was.

Then $p\vee q\to q\vee p$, the same shape with the disjunction itself discharged at the end, so that nothing is left open:

witnessing ${⊢}_{\mathrm{N}}p\vee q\to q\vee p$. Next, the move that debugging is mostly made of. There is a rival explanation: the customer clicked “pay” twice. But a second click makes a second order, so if the customer had clicked twice, the two charges would carry different order numbers; Baker looks at the ledger, and they carry the same one; so the customer didn’t click twice, and the rule she filed at ten past ten is still the one to chase. With $b$ for “the customer clicked twice” and $g$ for “the two charges carry different order numbers”, she has $b\to g$ and $\mathrm{\neg }g$, and she wants $\mathrm{\neg }b$. Since $\mathrm{\neg }g$ is $g\to \mathrm{\perp }$ and $\mathrm{\neg }b$ is $b\to \mathrm{\perp }$, the rules for $\to$ do the whole job:

$\mathrm{OH}=\{b\to g,\mathrm{\neg }g\}$, so the tree witnesses $\{b\to g,\mathrm{\neg }g\}{⊢}_{\mathrm{N}}\mathrm{\neg }b$. The Latin name is modus tollens, the mood that denies, and the tree is the one a person would draw: suppose the cause, derive the symptom, observe the symptom absent, and conclude that the cause is absent.

Next, what happens when the observations disagree. The retry was sent, says the app’s log; the runbook says a sent retry is received by the gateway; the gateway’s log says nothing was received. With $h$ for “the retry was sent” and $m$ for “the gateway received it”, Baker has $h$, $h\to m$ and $\mathrm{\neg }m$, and from them she can conclude $l$, or anything else:

All three leaves are open: the tree witnesses $\{h,h\to m,\mathrm{\neg }m\}{⊢}_{\mathrm{N}}l$. It is correct and useless, and that’s the point. A contradiction among the observations ends the reasoning until it’s resolved, because once you have one, every tree can be completed. One of the logs is wrong, and finding out which is the next thing to do.

Last, currying, which Chapter 2 met as an example (Example 2.11): turning a function on pairs into a function that takes its two arguments one at a time, and back.⁶ Here is $(p\wedge q\to r)\to p\to q\to r$:

and the other way, $(p\to q\to r)\to p\wedge q\to r$, in which one supposition is taken apart twice:

Both have $\mathrm{OH}=\varnothing$, so each witnesses ${⊢}_{\mathrm{N}}$ its formula. Each has one discharge per arrow in the conclusion. That’s the rule of thumb for finding these: count the arrows on the outside, suppose that many things, and reason.

Induction over derivations

The definition buys more than a notation. It is inductive, built the way the combinator terms were built: a base case, nine rules for building a bigger derivation from smaller ones (clauses 5 and 6 give two each), and a “nothing else”. So it comes with a principle of proof, the one every theorem in the rest of this chapter uses.

To show that every derivation has a property $P$, it is enough to show that each one-node derivation has $P$, and that for each of the nine rules, if the derivations the clause uses have $P$ then so does the derivation the clause builds.

That’s rule induction, and it’s the same move as induction on the natural numbers with the clauses in place of zero and successor. When you meet “by induction on the derivation” in a book on proof theory, this is what it means.

3.3 Equivalence with the Hilbert system

We can now state the theorem promised at the start of the chapter: Gentzen’s rules lose nothing. NJ has no axioms and nine rules; the Hilbert system has nine schemas and one rule. They prove the same things.

So the two systems are one logic in two notations, and the Deduction Theorem is what makes them so. It is the ($\to$I) rule of natural deduction, proved admissible for the Hilbert system: adopting it as a rule would let the Hilbert system prove nothing it can’t prove already. And it is used again inside ($\vee$E), whose two branches are suppositions. From here on I write $⊢$ for both. Nothing proved about the Hilbert system has to be proved again, and nothing in this chapter will ever cite an axiom.

3.4 The $\lambda$-calculus

Everything so far has been about proofs. But a Hilbert proof is a typed program with the program rubbed out: Curry’s correspondence (Theorem 2.4) puts a combinator term beside every line, $\mathsf{K}$ for (I), $\mathsf{S}$ for (II), a variable for a hypothesis and an application for a modus ponens. We have now changed what a proof is. So what is the matching notion of typed program?

Look at the one move the new proofs have that the Hilbert system has only as a theorem: discharge, which is the Deduction Theorem. In natural deduction it is a rule, so the new programs need a term constructor to go with it, a step that turns a program using a parameter into a function:

Above the line is a program $M$ that uses a parameter $x$ of type $A$; below it, the function that takes an $x$ and returns $M$. The Hilbert system has no such step. The Deduction Theorem’s construction would compute one, compiling the parameter away into $\mathsf{K}$ and $\mathsf{S}$ — for Baker’s rule, $\lambda x.g(fx)$, it gives $\mathsf{S}(\mathsf{K}g)f$ — but that’s a translation of what we want, at the tripling cost we’ve already met. What we want is the thing itself: a notation that binds a variable, so that “the function of $x$ given by $M$” is a term in its own right. That is what the $\lambda$ of Alonzo Church does. And the question “which programs are natural deduction proofs?” gets the answer “the ones with parameters”. Which is every program you’ve ever written.

The notation already existed, invented for another purpose. In 1932 Church, a Princeton mathematician not yet thirty, published a logic meant to carry the whole of mathematics, built, like Curry’s, from functions rather than from sets.⁷ Watch what he did with the variable. Curry did away with variables by building everything from constants. Church kept them, but only one kind: every variable in a formula had to be bound by a $\lambda$, and the free variable, the $x$ left dangling in $x+1=1+x$, was to go. His paper calls this “the complete abandonment of the free variable”, and a page later it states the spirit in which the whole system was offered:⁸

We do not attach any character of uniqueness or absolute truth to any particular system of logic. The entities of formal logic are abstractions, invented because of their use in describing and systematizing facts of experience or observation …

Just as well he didn’t. Within three years his own students, Kleene and Rosser, had shown the logic inconsistent, by the self-application of the Monster. What survived was the part that handled variables: a small calculus of functions, which Church and his students went on to show could compute anything that can be computed at all. Here are its terms.

You’ve written the third form many times. It is \x -> M in Haskell, lambda x: M in Python, x => M in JavaScript;⁹ every def f(x): return M is one with a name attached. These terms, with the one rule of computation given below, are Church’s $\lambda$-calculus. The logic did not survive; the calculus did.¹⁰

Free variables and substitution

The $x$ in $\lambda x.M$ is the function’s parameter: the $\lambda$ binds it, and its scope is the body $M$. An occurrence of a variable is bound if it lies in the scope of a $\lambda$ on that variable and free otherwise. In $(\lambda x.xy)x$ the first two occurrences of $x$ are bound and the last, like the $y$, is free. The set $\mathrm{FV}(M)$ of free variables of $M$ is defined by recursion on the shape of $M$, one clause for each of the three forms:

1. $M$ is a variable $x$: $\mathrm{FV}(x)=\{x\}$.

2. $M$ is an application $M_1{M}_2$: $\mathrm{FV}(M_1{M}_2)=\mathrm{FV}(M_1)\cup \mathrm{FV}(M_2)$.

3. $M$ is an abstraction $\lambda x.M_1$: $\mathrm{FV}(\lambda x.M_1)=\mathrm{FV}(M_1)\setminus \{x\}$.

Only the third clause does anything: a $\lambda$ removes its own parameter from the list, and nothing else removes anything. A term with no free variables is closed: a whole program rather than a fragment of one. Two terms that differ only in the names of their bound variables, like $\lambda x.x$ and $\lambda y.y$, describe the same function, and we treat them as the same term: a bound variable may be renamed at will. Notice that clause 3, $\mathrm{FV}(\lambda x.M_1)=\mathrm{FV}(M_1)\setminus \{x\}$, has the shape of the ($\to$I) clause for derivations, $\mathrm{OH}=\mathrm{OH}(\mathcal{D})\setminus \{A\}$, with a variable in place of a formula. That’s no accident, and the next section makes it exact.

Substitution $M(N/x)$ replaces the free occurrences of $x$ in $M$ by $N$, and nothing else. In a language with no binders this would be simple replacement. Here it has to step around binders, and that is where substitution gets complicated: it is the rule that Curry, reading Principia in the 1920s, found far more complicated than modus ponens, and set out to take apart. It too is defined by recursion on the shape of $M$, one clause per form, except that the variable and abstraction cases each split in two, according to whether the variable met is the very one being replaced:

1. $M$ is the variable $x$ itself: $x(N/x)=N$.

2. $M$ is a variable $y$ other than $x$: $y(N/x)=y$.

3. $M$ is an application $M_1{M}_2$: $(M_1{M}_2)(N/x)=M_1(N/x)M_2(N/x)$.

4. $M$ is an abstraction on $x$ itself: $(\lambda x.M_1)(N/x)=\lambda x.M_1$.

5. $M$ is an abstraction on some other variable $y$:

   $$(\lambda y.M_1)(N/x)=\lambda y.M_1(N/x),\text{provided }y\notin \mathrm{FV}(N).$$

Clauses 1 to 3 replace the variable when you meet it and otherwise pass the substitution down. Clause 4 stops at a $\lambda x$ because every $x$ inside it is bound: there is nothing to replace. The side condition on clause 5 is the one subtlety. Pushing $N$ under a $\lambda y$ when $y$ is free in $N$ would turn that free $y$ into a bound one and change what $N$ means, so the clause declines. The remedy is to rename the $y$ of $\lambda y.M_1$ to a letter that occurs nowhere else, and then substitute. Rename first.¹¹ Chapter 4 shows what goes wrong when a substitution skips that step, and shows the same bug on the logic side, where it has been known for a century.

Reduction

There is one rule of computation. To apply a function to an argument, substitute the argument for the parameter:

anywhere inside a term; the pair on the left is a redex, and the step is called $\beta$. That’s what a function call does, and it’s all a function call does. A term with no redex is in normal form, and running means taking $\beta$ steps until there is none to take. A term may have several redexes. Does it matter which is taken first?

However far two runs of the same term have gone apart, they can be brought back together. So a term has at most one normal form: the order of the steps can change whether it is reached, not what it is. Church and Rosser proved this for the calculus in 1936.¹² Not every term gets there. With $\omega$ for $\lambda x.xx$, the term $\mathrm{\Omega }=\omega \omega$ has one redex, and the step gives $\mathrm{\Omega }$ back, for ever: nothing in the definition of $\lambda$-terms says what may be applied to what. The two combinators are terms too:

The step $\mathsf{K}MN⇝M$ is two $\beta$ steps on $(\lambda x.\lambda y.x)MN$, and the step $\mathsf{S}MNP⇝MP(NP)$ is three. So every combinator term is a $\lambda$-term, and the two constants need no longer be taken as given.

That’s the order natural to these notes, which built the combinators first. History went the other way round. In 1936 Church proposed that “computable” should mean “definable by a $\lambda$-term”, and used that definition to show that no procedure decides whether two terms have the same normal form. That September Turing, who had never heard of the calculus, arrived at Princeton to study with Church, and in an appendix of 1937 he proved that his machines and Church’s terms compute the same functions (Turing, 1937a). Curry and his students showed the combinators equivalent to both.¹³ One theorem, proved by three groups of people about three notations: that’s a large part of why the history is confusing, and the end of the chapter draws it as a picture.

Example: factorial

Let’s send something ordinary the whole way round, so you can believe the three notations are one. Factorial, as you would write it on a whiteboard:

fact(n):
    if n = 0 then return 1
    else return n * fact(n - 1)

Four things in it are not in the combinator language: a parameter, a name that calls itself, a conditional, and arithmetic. Take them away one at a time. The parameter becomes a $\lambda$, which is what this section was for. Write $\mathit{isZero}$, $\mathit{mult}$ and $\mathit{pred}$ for the test, the product and the predecessor, and use a boolean as its own conditional, so that “if $b$ then $M$ else $N$” is $bMN$. Then

Nothing has really happened yet, because $\mathit{fact}$ still occurs on the right-hand side, and a term may not refer to itself. So make the recursive call a parameter too:

$F$ mentions nothing but its own two parameters: give it the function to call and a number, and it does one layer of the work. What we want is a term $\mathit{fact}$ with $\mathit{fact}=F\mathit{fact}$, a fixed point of $F$. A constant $\mathit{fix}$ added to the combinators, with the single step $\mathit{fix}F⇝F(\mathit{fix}F)$, is just what we want. So define $\mathit{fact}:=\mathit{fix}F$. One step shows how it runs:

and on the right $F$’s parameter $r$ is $\mathit{fix}F$ again: the recursive call, ready to unfold once more when it is needed and no sooner.¹⁴ The arithmetic was combinators already: the numerals, addition and multiplication were all built from $\mathsf{K}$ and $\mathsf{S}$, and the predecessor is Kleene’s. We keep the three as names only to keep the term on the page.

One thing remains, the two $\lambda$s, and the translation $[x]P$ removes them. Write $B$ for the body, so that $F=\lambda r.\lambda n.B$, and read $B$ as the application $(\mathit{isZero}n1)(\mathit{mult}n(r(\mathit{pred}n)))$. The clause for an application splits it, the other two clauses finish each half, and with $\mathsf{I}$ written for $\mathsf{S}\mathsf{K}\mathsf{K}$,

twenty-six symbols, with $r$ still free. Abstract $r$ out of that by the same three clauses and every variable is gone:

where $A=\mathsf{S}(\mathsf{S}(\mathsf{K}\mathit{isZero})\mathsf{I})(\mathsf{K}1)$, $C=\mathsf{S}(\mathsf{K}\mathit{mult})\mathsf{I}$ and $E=\mathsf{S}(\mathsf{K}\mathit{pred})\mathsf{I}$. There is not a variable, a parameter, a conditional or a recursive call anywhere in it, only $\mathsf{K}$, $\mathsf{S}$, three arithmetic constants and juxtaposition. Yet $\mathit{fix}{F}^{\circ }$ applied to $\bar{4}$ runs to $24$, by the $\mathsf{K}$ and $\mathsf{S}$ steps and the steps of the constants. A program you could have written in your first week sits on two constants in exactly this way, and so does every program you’ll ever compile.

Baker’s runbook, for what it’s worth, is code of the same kind. The rule she filed is a function of its supposition,

timeoutMeansTwice = \timeout -> chargedAgain (retried timeout)

and the gateway’s “declined or approved” is a case with two branches; we’ll see the compiler check both in the next section.

3.5 The simply typed $\lambda$-calculus

On to the checker, and first to the Monster: the function that applies its argument to itself, applied to itself. In $\lambda$ notation,

and each step gives back the term it started from. Self-application of this kind sank both of the logics these calculi were built for. The combinators came first: Schönfinkel had them in 1924 (Schönfinkel, 1924), and Curry, finding them again in the 1920s, built a logic on them in his thesis of 1929 (Curry, 1930). Church’s logic, with its variables bound by $\lambda$, followed in 1932. In 1935 Kleene and Rosser showed both inconsistent (Kleene and Rosser, 1935). The repair was the same in both cases: types. Curry gave his combinators types in 1934 (Curry, 1934), and Church gave his calculus types in 1940. Church’s typed calculus is the language of this section, the simply typed $\lambda$-calculus. Its types, contexts and judgements are those of the combinator checker: a type is a basic type or a function type $A\to B$; a context $\mathrm{\Gamma }$ lists the variables in scope with their types, $x_1:A_1,\dots ,x_n:A_n$; and the judgement $\mathrm{\Gamma }⊢M:A$ says that $M$ has type $A$ when its variables have the types $\mathrm{\Gamma }$ gives them. Two of the rules are also the checker’s, for variables and for applications. The third is the Deduction Theorem, which the Hilbert system had to prove, adopted as a rule with the program written on:

Read (abs) as the checker reads a function definition: to check $\lambda x.M$, add the parameter to the context with the type it is to have, check the body, and give the function the arrow type. If $\mathrm{\Gamma }$ already declares an $x$, rename the parameter first, since a context lists each variable once. Rule (abs) is the first typing rule we have met that changes the context: above the line there is one more variable in scope than below it, exactly as above an $\to$I bar there is one more open hypothesis than below it.

A typing of combinator terms was a list of lines under one context, which was enough because no rule changed the context. Rule (abs) does change it, so from now on a typing is a tree in which every node is a whole judgement, context included, and every bar is one of the three rules, premisses above and conclusion below. This is natural deduction in sequent style: the hypotheses available at each point are written at that point, rather than read off the leaves. Here is Baker’s rule, with $f:t\to r$ and $g:r\to d$ for the two runbook functions and $x:t$ for the supposition. With every context written out, the tree is too wide for the page, so here it is in two steps. First the application $fx$:

Example: function composition

Here’s the typing of a program you’ve written in one form or another, \f -> \g -> \x -> f (g x), from the empty context. The body is checked in the context $f:B\to C,g:A\to B,x:A$, written out at every node, and again in two steps to fit the page. First $gx$:

The top is routine: three look-ups and two uses of (app), each matching an argument’s type against the type a function expects. The (abs) bars shrink the context one declaration at a time, until at the root it is empty and the program is closed. Rub out the programs. The top is a proof of $C$ from the three hypotheses $B\to C$, $A\to B$ and $A$, by two uses of modus ponens. The three (abs) bars discharge $A$, then $A\to B$, then $B\to C$. The first discharge alone gives $A\to C$ from $B\to C$ and $A\to B$: hypothetical syllogism, the rule that chains two implications. After all three, the formula at the root,

is hypothetical syllogism as a theorem, with nothing assumed. The compiler read your composition function as that proof.

The other connectives

The rules for $\wedge$, $\vee$ and $\mathrm{\perp }$ get programs in the same way, and they are programs you know: a pair, a tagged union, the empty type. Baker’s morning was made of all three. At twenty past ten her evidence for $a\wedge p$ was two pieces of evidence held together, an authorisation code and a capture id, and that pair is what a settled charge is in the payments database: one record with two fields, and to use either field you take it back out. At half past ten the gateway’s answer was a value with a tag on it, Declined with a reason or Approved with a code, and to use it she had to branch on the tag; the one thing checkout code must never do is treat an answer as approved without looking at the tag, and a tagged union is how a compiler makes that impossible. And when the logs disagreed she had, on paper, a value of the type that has none, which is why anything followed. Programs are full of all three. Pairs are tuples such as (min, max), and records and structs. Tagged unions are enums, Haskell’s Either, and Rust’s Result, a value or an error, which the compiler makes you handle both ways. The empty type is Haskell’s Void or Rust’s !, the type of a computation that never returns. A rule that introduces a connective builds a value of the type, so it is a constructor; a rule that eliminates one takes a value apart, so it is a pattern match. One thing changes on the page. A type theorist doesn’t write the pair type as $A\wedge B$, and I’ll follow the type theorists while we’re typing: the pair type is $A\times B$, the union $A+B$, and the empty type $\mathrm{\perp }$, which the two traditions happen to share, along with $\to$.

To build an $A\times B$ you build both halves; to use one you take whichever half you need. To build an $A+B$ you build one side and say which; to use one you argue by cases. The case split, ($+$E), is the one rule besides (abs) that puts a variable in scope: one in each branch, and only there. That is what “a different formula discharged in each branch” looked like on the tree. Nothing builds a $\mathrm{\perp }$, and if you ever have one you may conclude anything, which is what absurd :: Void -> a says. The whole language fits in one table: each connective, the type it is, how a value is built, how it’s taken apart.

That’s the central table of Part 1, and the one thing to carry away from it: the connectives of logic are the data types of a programming language, the introduction rules are their constructors, and the elimination rules are the pattern matches that take them apart. The first two columns are the same thing written by two trades, and the theorem below says what to do with the symbols when the programs are rubbed out: $\times$ becomes $\wedge$ and $+$ becomes $\vee$, while $\to$ and $\mathrm{\perp }$ stay as they are.