Proof systems — the series

1. 

   The tree that closes

   To prove a formula, assume it false and take it apart. Every branch ends in a contradiction, or one of them describes exactly how it could have been false — and either way the tree is the answer, drawn.

   part 1 · logic
2. 

   The assumption a proof pays back

   A tableau assumes the opposite once and takes it apart. Natural deduction assumes things freely, uses them, and then withdraws them — and the withdrawal is what turns a derivation of a consequence into a proof of an implication.

   part 2 · logic
3. 

   A lemma, and the proof that never mentions one

   Proving something by first proving a lemma is what makes mathematics readable, and it is exactly what makes a proof system impossible to search — because the lemma can be any formula at all. Gentzen proved the step can always be removed, and the removal is not free.

   part 3 · logic
4. 

   The instance that has to be guessed

   Every rule of a propositional tableau replaces a formula by shorter ones, which is why it stops. The rule for a universal claim does not replace it — it keeps it and adds an instance — and one word changing turns a decision procedure into a search that may run forever.

   part 4 · logic
5. 

   Every derivation is a term

   Write a variable for each assumption, an abstraction where one is discharged, and an application where an implication is used, and a natural-deduction derivation becomes a term. The formula it proves is the term's type, and checking the one is checking the other. A detour in the proof — a lemma introduced and at once used — is a term that simplifies, and simplifying it is removing the detour.

   part 5 · logic
6. 

   The sentence between a premise and its consequence

   When one formula implies another, something sits between them written only in the words the two have in common: a sentence the first implies and that implies the second. A refutation of the first together with the denial of the second hands such a sentence over, and every possible one lies between a strongest and a weakest that can be computed outright.

   part 6 · logic
7. 

   What a proof about numbers can compute

   The proofs of (o → o) → o → o without detours are the whole numbers, one for each count of how often the assumption is used. A proof of the implication from that formula to itself therefore takes a number and returns one, and removing its detours computes the answer. Enumerating all 14,659 such proofs up to size 16 finds 299 different functions — sums, products, squares, cubes, tests on zero — and not one of them subtracts. The predecessor, n − 1, is not among them, and a single line about polynomials says it never will be.

   part 7 · logic
8. 

   One type up

   A numeral is an iterator, and the formula it proves fixes what it may iterate. At the lowest type it can only repeat the successor, and every function it computes is a polynomial — no predecessor. Let the same numeral iterate a function on functions and 2ⁿ appears; let it iterate a function that takes a function and returns a value, and the predecessor appears at size 15; let it iterate a pair of values, and the predecessor, halving and parity all arrive at size 16. The trick is Kleene's, from 1932, and an exhaustive search finds it without being told.

   part 8 · logic
9. 

   One type for every use

   In the simply typed calculus a numeral must be told in advance what kind of thing it will iterate, and with input and output of one type it computes only polynomials with tests. Let a single type stand for every type — a numeral is then a term of type ∀X. (X → X) → X → X, used at whatever type each occasion needs — and the same few symbols compute subtraction, exponentials and Ackermann's function, which grows faster than anything built from primitive recursion. Every run still finishes, and the proof that it does lies just beyond the reach of second-order arithmetic.

   part 9 · logic

All series