Chapter 2: Hilbert Proofs

In 1936, to say what it means for something to be computable, Turing did not describe a machine. He described a person (Turing, 1937): a clerk with a pencil, a supply of squared paper, a finite alphabet of symbols, and a small number of states of mind, who at each moment looks at one square, and according to what is there and the state he is in, writes a symbol or rubs one out, moves one square left or right, and changes state. That is all the clerk may do. Turing’s claim was that whatever a human being can calculate, a clerk so restricted can calculate, and the machine that bears his name is the clerk with the person taken out. In the same year, independently, Emil Post described a “worker” moving along a row of boxes, marking and unmarking them (Post, 1936), and arrived at the same place.

Now do the same for proving. Imagine a person who has a language of statements — letters standing for claims whose insides we do not look at, and a way of building “if this then that” from two statements — and who is permitted exactly one act: to write down a new line, provided it is one of a few fixed shapes agreed in advance, or follows from lines already written by one fixed rule. Nothing else. No insight, no appeal to what the letters mean, no step that cannot be checked by looking at the shapes of the lines on the page. A proof is what such a person produces, and the question this chapter asks of it is Turing’s question turned around: not “what can this clerk compute?” but “why should anyone believe the last line?” We shall find that the clerk has been in your compiler all along.

2.1 Formulas

First the language.

That is Definition 1.9 with the word “type” replaced by the word “formula” and the word “basic type” by the word “letter”: the same grammar, the same bracket convention, the same strings. For now treat the two as different things that happen to be spelled alike, and read $A\to B$ as a statement — a claim that $B$ follows from $A$ — and not as a contract. (There is more to logic than $\to$: and, or and not arrive in Chapter 3, and for all in Chapter 4. One connective is enough to see the shape of a proof, and it is the one that matters most.)

2.2 Axioms, rules, and proofs

A proof is a list of lines, and a line may be written only if it has one of a few fixed shapes or follows from earlier lines by one fixed rule. Which shapes? Two will do, and they were chosen so that one particular theorem about proofs would hold — the theorem of §2.7, which is the one your compiler relies on. The first shape says that a claim is implied by anything: if $A$ holds, then $A$ holds whatever else does. The second is modus ponens carried out under a hypothesis: if, given $A$, you have $B\to C$, and, given $A$, you have $B$, then, given $A$, you have $C$. The rule is modus ponens itself: from an implication and its antecedent, write the consequent. Here are the two shapes and the rule; the design is Frege’s, and systems of this kind carry Hilbert’s name.

Each schema stands for infinitely many axioms, all of one shape. Both of

are instances of (I), the first with $p$ and $q$ for $A$ and $B$, the second with $r\to s$ and $p$. A simple parser can test whether a given formula matches one of the two shapes, which is all the checker needs. To check an application of modus ponens a clerk finds the two cited lines and confirms, symbol for symbol, that one is exactly the other with an arrow and the new line attached. Pattern matching; no understanding required.

Here, built from the two shapes and the one rule, is the certificate.

In words: go down the list; every line must match one of the two shapes, or be one of the hypotheses, or be the $B$ of a modus ponens whose two premises, $A\to B$ and $A$, both appear higher up. Higher up is the force of $i,j<k$: a line may cite only lines already written, which is what makes the check a single pass down the page. On the right of each line I write its justification, and “MP $i$, $j$” means modus ponens applied to line $i$ as the implication and line $j$ as its antecedent — the implication first, as the function came first in “(app) $i$, $j$”.

This is the definition the chapter rests on, and it is syntactic through and through: a rule is applied by matching the shapes of formulas, never by asking what they mean, and that is what makes checking mechanical. A hypothesis is used exactly like a proved line. The hypotheses are what you have been told; a proof from $\mathrm{\Gamma }$ says what follows from what you have been told; and the special case of nothing told at all is what we call a theorem. A function does not know its inputs either: it is told what kind of thing each will be — that was the context $\mathrm{\Gamma }$ of Definition 1.10 — and on that basis does its work for every input of that kind at once. We write the same symbol $⊢$ in both places, and that is not an accident.

Now put the two definitions side by side. A typing, by Definition 1.11, is a list of judgements of which each line is a $𝖪$, an $𝖲$, a variable from the context, or an application built from two earlier lines. A proof, by Definition 2.3, is a list of formulas of which each line is an instance of (I), an instance of (II), a hypothesis from $\mathrm{\Gamma }$, or a modus ponens on two earlier lines. Four cases and three, in the same order, of the same shapes — and the shapes themselves match, since (I) is (1.1), the type the checker gives $𝖪$, and (II) is (1.2), the type it gives $𝖲$. Checking a typing and constructing a proof are one activity.

2.3 Typings are proofs

Take the typing of Example 1.12 and rub out the programs. What is left of line 1,

is the formula

which is an instance of schema (II). What is left of line 3, “(app) 1, 2”, is “MP 1, 2”. What is left of the whole list is a five-line proof of $A\to A$ from no hypotheses at all. The agreement is not a resemblance but an identity, and stating it takes two sentences: rub the programs out of a typing and what is left is a proof; write programs back onto a proof and what you get is a typing.

For a context $\mathrm{\Gamma }=x_1:A_1,\dots ,x_n:A_n$ write $|\mathrm{\Gamma }|$ for the set $\{A_1,\dots ,A_n\}$ of types in it, now read as formulas.

So types are formulas, and a typing is a proof: not resembles one, is one, line for line, justification for justification. The two constants are the two axiom schemas with programs attached; application is modus ponens with programs attached; a variable in the context is a hypothesis with a name. Now re-read Theorem 1.16 with the programs rubbed out. A $𝖪$ step rewrites $𝖪PQ$ to $P$. In the proof, the line for $𝖪PQ$ was reached as follows: a proof of $A$ (the lines for $P$), then an instance of (I) saying $A\to B\to A$, a modus ponens giving $B\to A$, a proof of $B$ (the lines for $Q$), and a modus ponens giving $A$. That is a detour: $A$ was already in hand, and the proof went out through $B$ and came back to it. The step deletes the detour and keeps the proof of $A$ that was there all along. An $𝖲$ step is a detour of the same kind through (II). So running a program is removing detours from a proof, and subject reduction is the statement that a proof with a detour removed is still a proof of the same formula. Everything the checker does with its four cases is therefore something a logician would recognise. The next two sections write proofs, and every proof written there is also a program typed.

2.4 A first proof (practice)

The point of the drill is to see what a proof looks like on the page and what checking one involves. The claim is $⊢p\to p$: that “$p$ implies $p$” is a theorem, provable from no hypotheses. Each line carries its justification on the right; the square brackets give the formulas substituted for the schema’s letters $A,B,C$, in that order.

1.

$(p\to (p\to p)\to p)\to (p\to (p\to p))\to p\to p$ (II) $[p,p\to p,p]$

2.

$p\to (p\to p)\to p$ (I) $[p,p\to p]$

3.

$(p\to (p\to p))\to p\to p$ MP 1, 2

4.

$p\to (p\to p)$ (I) $[p,p]$

5.

$p\to p$ MP 3, 4

Five lines to prove that $p$ implies $p$. Each is trivial to check: lines 1, 2 and 4 are matched against two shapes, and lines 3 and 5 against the two lines they cite.

Line 1 is not trivial to find, and it is worth seeing how one would find it, because the thinking runs backwards from the goal, which is how all proof-finding runs. The goal $p\to p$ is not an axiom, so it must come by modus ponens, from some $C$ and $C\to (p\to p)$. Could the second of these be an instance of (I)? Then $C$ would be $p$, and we would need a proof of $p$ on its own, which there cannot be — $p$ is a bare letter, and nothing in the system proves a bare letter, as Chapter 3 confirms. So try (II): its last part, $A\to C$, must be $p\to p$, which fixes $A=C=p$ and leaves $B$ free; and both premises, $p\to (B\to p)$ and $p\to B$, will be instances of (I) if we choose $B$ to be $p\to p$. That is line 1. The search took a paragraph; the check takes none.

Now put this proof beside Example 1.12, the typing of $𝖲𝖪𝖪$ at $A\to A$, and read the two lists line by line. Line 1 there was (S) at $[A,A\to A,A]$; line 1 here is (II) at $[p,p\to p,p]$. Line 3 there was (app) 1, 2; line 3 here is MP 1, 2. With $p$ for $A$, and the programs rubbed out, the two lists are the same list: Theorem 2.4 on a five-line example.

2.5 Structural facts

Two proofs from hypotheses first, both of which are wanted later. The short one: a proof that $\{p\}⊢q\to p$. The hypothesis is $p$; we are to show that $q\to p$ follows from it.

1.

$p\to q\to p$ (I) $[p,q]$

2.

$p$ hypothesis

3.

$q\to p$ MP 1, 2

Now hypothetical syllogism, the rule that chains two implications: from $p\to q$ and $q\to r$, conclude $p\to r$. As a claim about provability it is $\{p\to q,q\to r\}⊢p\to r$, and here is the proof.

1.

$q\to r$ hypothesis

2.

$(q\to r)\to p\to (q\to r)$ (I) $[q\to r,p]$

3.

$p\to (q\to r)$ MP 2, 1

4.

$(p\to (q\to r))\to (p\to q)\to p\to r$ (II) $[p,q,r]$

5.

$(p\to q)\to p\to r$ MP 4, 3

6.

$p\to q$ hypothesis

7.

$p\to r$ MP 5, 6

Read the blocks, not the symbols. Lines 1–3 take the hypothesis $q\to r$ and weaken it, by (I), to $p\to (q\to r)$: a statement that says less, since it only promises $q\to r$ once $p$ is given. Lines 4–5 put that through (II), which turns “given $p$, $q$ implies $r$” into “if $p$ gives $q$ then $p$ gives $r$”. Line 7 fires the result on the other hypothesis. Every Hilbert proof has this character: a few ideas, spelled out at a length the checker can follow. (If you did Exercise 1.3, you have seen this list before, with programs on it.)

Four facts about $⊢$ follow straight from the definition, and each is used without comment from here on. They are the kind of thing a programmer takes for granted about scope, and it is worth seeing that logic has to earn them.

In the language of programs: a variable in scope may be used (1); extra names in scope do no harm (2); a helper function may be inlined at its call sites (3); and a program is a finite text (4). The third fact is the one to remember, because it says that proofs compose: a theorem, once proved, may be used as a line in any later proof, just as a function, once written, may be called. Item (4) looks trivial and will matter in Chapter 9. What the checker cannot do is type a definition with a parameter, and what we cannot yet see is what that has to do with logic. The next section shows what it costs a proof to do without such a rule, and the one after shows that the rule was there all the time.

2.6 The cost of an implication

Hypothetical syllogism in §2.5 was proved from its two implications, written down as hypotheses. Suppose instead we want it as a theorem, with no hypotheses at all: the single formula

“if $q$ implies $r$ then, if $p$ implies $q$, $p$ implies $r$”. Here is a proof from the schemas alone. To keep it legible I abbreviate

so that the goal is $P\to R$.

1.

$(P\to Q\to R)\to (P\to Q)\to P\to R$ (II) $[P,Q,R]$

2.

$Q\to R$, that is, $(p\to q\to r)\to (p\to q)\to p\to r$ (II) $[p,q,r]$

3.

$(Q\to R)\to P\to (Q\to R)$ (I) $[Q\to R,P]$

4.

$P\to Q\to R$ MP 3, 2

5.

$(P\to Q)\to P\to R$ MP 1, 4

6.

$P\to Q$, that is, $(q\to r)\to p\to (q\to r)$ (I) $[q\to r,p]$

7.

$P\to R$ MP 5, 6

Seven lines again, and each checks in a moment. But look at line 1. With the abbreviations undone it is an instance of (II) with twenty letters and nineteen arrows, and nobody finds it by thinking about what implication means. Compare it with the proof from hypotheses. There, $q\to r$ and $p\to q$ were simply written down as lines 1 and 6, and the five lines in between did the work. Here the two hypotheses have been pushed into the formula: line 6 is $q\to r$ weakened by (I) exactly as line 2 was there, line 2 here is the instance of (II) that was line 4 there, and line 1 is an instance of (II) whose only job is to carry out, under the hypothesis $P$, the modus ponens that line 5 performed in the open. The closed proof contains the open one, rebuilt one level up.

That is the cost of an implication in this system. To prove $A\to B$ outright, you cannot assume $A$ and derive $B$, because “assume” is not one of the three kinds of line; you must build the proof of $B$ with $A$ threaded through every step, by instances of (II) that grow with the formulas they carry. For a conclusion with one arrow it is a nuisance; for one with three it is unmanageable (try flip, Exercise 2.3); and every function you have ever written has an arrow in its type for every parameter. A clerk restricted to two shapes and one rule cannot prove anything of the form $A\to B$ without an instance of (II) that nobody would write down unprompted. Yet the typing of Exercise 1.3(b) is this proof — line for line, (S) for (II), (K) for (I) — and a compiler produces that typing in a microsecond. Something finds these lines. The next section says what.

2.7 The Deduction Theorem

The clerk may not assume. But it turns out that the clerk does not need to, because anything that can be proved by assuming $A$ can be proved without, and there is a mechanical procedure that does the conversion. The claim is that whenever $B$ has a proof from $\mathrm{\Gamma }$ together with $A$, the implication $A\to B$ has a proof from $\mathrm{\Gamma }$ alone; and the proof of the claim is a transformation of proofs, which takes a proof of $B$ that uses $A$ as a hypothesis and rewrites it, line by line, into one that does not.

Three things follow, and the first answers the question Chapter 1 ended on.

The compiler’s missing rule is a theorem. A definition $fx=M$ has a parameter $x$ and a body $M$. To type it, a checker would want to say: suppose $x$ has type $A$; if, on that supposition, $M$ has type $B$, then $f$ has type $A\to B$. In the judgements of Chapter 1,

which, with the programs rubbed out, is: if $\mathrm{\Gamma }\cup \{A\}⊢B$ then $\mathrm{\Gamma }⊢A\to B$. That is the Deduction Theorem, left to right. The rule the checker lacked is not a rule but a theorem of the system it already has — and since the theorem’s proof is a construction, it tells the checker what to do. This is the compiler promised in Theorem 1.8. The theorem’s proof is a construction, and running it with the programs left on rather than rubbed out compiles the parameter away: its first case writes a $𝖪$ and its third an $𝖲$, and what comes out of a definition $f{x}_1\cdots x_n:=M$ is a term containing no variables at all, which runs the same way on every argument and has the type the definition should have. Chapter 3 sets the two languages side by side and finds them the same language (Theorem 3.3). This is also why the schemas are what they are: (I) and (II) are the types of the two programs that survive when every variable has been compiled away, and they were chosen — by Hilbert’s school, long before anyone compiled anything — precisely so that the Deduction Theorem would hold.

You may assume the premise. Read the theorem the other way round. To prove $A\to B$, assume $A$ and derive $B$; every such proof can be rewritten, mechanically, into a proof of the implication with no assumption. So the clerk may, after all, write “suppose $A$” — not because the rules allow it, but because a theorem about the rules says the supposition can always be compiled away. Hypothetical syllogism as a theorem, which cost a twenty-letter line in §2.6, now costs this: from the hypotheses $q\to r$, $p\to q$ and $p$, modus ponens twice gives $q$ and then $r$; discharge $p$, then $p\to q$, then $q\to r$. Three lines of thought and three discharges, and the twenty-letter line is what the third discharge writes on your behalf. It has a price: the rewritten proof is about three times as long, three lines for each original one. That is what every implication proved in the bare system costs, and it is why nobody writes such proofs by hand. And it buys this. The theorem $⊢p\to p$ took a paragraph of searching; with the theorem it is immediate from $\{p\}⊢p$, which is a one-line proof. (The theorem’s own proof uses the five-line proof once, in the case $A_k=A$; what the theorem saves you is finding it again.)

A proof is a finite list of formulas, each an axiom, a hypothesis, or modus ponens from earlier lines, and checking one is pattern matching. A typing is a proof with the programs written beside the lines (Theorem 2.4): $𝖪$ and $𝖲$ are the two schemas, application is modus ponens, a variable in the context is a hypothesis, and running a program removes detours from a proof. The rule the compiler needed for a parameter is the Deduction Theorem, $\mathrm{\Gamma }\cup \{A\}⊢B$ iff $\mathrm{\Gamma }⊢A\to B$, whose proof is the algorithm that compiles the parameter away, and whose two schemas are the types of the two constants that survive the compilation. How did the compiler know? It checked a proof.

We have been writing $𝖪$ and $𝖲$ and compiling our definitions away because that is what the checker’s four rules could type. But the Deduction Theorem says that the case for parameters is admissible: adding it as a fifth case would let nothing new be typed. So add it, and let the parameter stay. Every definition $fx:=M$ you have ever written is then a term in its own right, the checker that reads it directly has three cases, two of which are ours and the third a theorem of ours — and we have not yet asked what those three rules, with the programs rubbed out, are as a logic. Chapter 3 goes back to the computational world with the parameter in hand, and finds that a mathematician has been using exactly those three rules since 1934.

Exercises

Reading

Open Logic Project (2026, chapter 12) on axiomatic derivations: parts of §§2.2 and 2.7 adapt its text, which is free to use with attribution, and its remark that the schemas were chosen for the Deduction Theorem is the one this chapter turns into a compiler. Curry and Feys (1958) is where $𝖪$ and $𝖲$ meet (I) and (II) in print; Turner (1979) turns the Deduction Theorem’s construction into a working compiler; Wadler (2015) tells the whole story. Next, Chapter 3: the $\lambda$ put back, and the logic whose proofs are programs. References.