Matpic
mathematics, in pictures
Concept

Proof system

A fixed stock of axioms and inference rules together with a definition of what counts as a derivation. Its value is measured twice: whether everything true is derivable in it, and how long the derivations are forced to be.

Named by 14 essays across one field — each of them below, with the objects they name alongside it.

A tableau for ((p → q) ∧ (q → r)) → (p → r). A branching tree of formulas, each branch ending in a contradiction or in a description of a counterexample.

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.

logic · Proof systems A resolution refutation of four clauses on three variables. A derivation tree: the given clauses at the top, each later clause obtained by cancelling one variable between two clauses above it, ending in the empty clause.

A proof with one rule

Two clauses that disagree about exactly one variable can be combined into a third that forgets it; repeat, and if the clauses cannot all be true the empty clause eventually appears — a complete proof system with a single move.

logic · Resolution A model whose worlds are sets of sentences. Worlds labelled by which of a fixed finite set of formulas they accept, with an arrow wherever every boxed formula accepted by one has its inside accepted by the other.

Worlds built out of sentences

A Kripke model needs worlds, and nothing so far has said where worlds come from. They can be made of the syntax: a world is a set of formulas it commits to, one world sees another when the boxed commitments line up, and in the model that results every formula is true exactly where it was assumed.

logic · Modal logic 7 steps and 3 withdrawn assumptions. A natural-deduction derivation of (p → q) → (¬q → ¬p). Each horizontal bar is one inference, named on its right; the bracketed formulas are assumptions, and each is withdrawn at the step that names it.

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.

logic · Proof systems A lemma, and the proof that never mentions one. Two derivations of ((p → q) ∧ (q → r)) → (p → r) compared: the cut-free one uses 8 nodes and only subformulas of the goal, and the one through a lemma uses 21 and mentions a formula the goal does not contain.

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.

logic · Proof systems Closed after 3 uses of the universal. The Herbrand expansion of a first-order question at 5 stages, with the number of remaining models at each. It reaches nought after 3 instantiations.

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.

logic · Proof systems A derivation of ((p → q) ∧ (q → r)) → (p → r), and the term it is. A natural-deduction derivation of ((p → q) ∧ (q → r)) → (p → r) with a lambda term written under each formula. The whole derivation is the term λh₁. λh₂. (π₂ h₁) ((π₁ h₁) h₂), and at every node the type of the term is the formula the derivation proves there.

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.

logic · Proof systems A implies B, and r ∨ s sits between them. A = ((p ∨ q) ∧ (p → r)) ∧ (q → s) implies B = (r ∨ s) ∨ t. A resolution refutation of A with the negation of B yields the interpolant r ∨ s. It uses only the shared atoms r, s, follows from A and implies B, and lies between the strongest and weakest interpolants.

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.

logic · Proof systems A failed search on four clauses, read as a resolution refutation. A binary search tree branching on variables, each branch ending at a clause the partial assignment makes false, with every branch point labelled by the resolvent of the clauses below it, the top label being the empty clause.

A failed search is a proof

Search for an assignment by branching on variables and backing up whenever a clause turns false. If every branch fails, the tree the search leaves behind is itself a resolution refutation: write at each branch point the resolvent of the clauses below it, and the top of the tree is the empty clause. So every limit on short refutations is a limit on every such search — and the pigeonhole clauses, whose refutations are long, defeat them all.

logic · Resolution Tseitin's clauses on the cube. the cube with a variable on each edge and a charge of 0 or 1 at each vertex, exactly one vertex charged 1. The parity demands give 32 clauses that cannot all be true.

A contradiction that is only a sum

Put a variable on every edge of a graph and ask each vertex for an odd or an even number of true edges, with the demands adding up to odd. Add all the demands and every edge is counted twice, so the left side is zero and the right side is one: the contradiction is a single sum. Resolution cannot add. It has to reach the same conclusion clause by clause, and on a graph where every group of vertices has many edges leaving it, that takes exponentially long.

logic · Resolution Unifying f(x, g(x)) with f(h(y), g(z)). Three term trees: f(x, g(x)), f(h(y), g(z)), and their common instance f(h(y), g(h(y))) under the most general unifier x ↦ h(y), z ↦ h(y).

Two terms made equal, and no more

Resolution with variables needs two literals to clash, and they clash only after something has been substituted for their variables. There are infinitely many substitutions that would do. One of them is the most general — every other is it followed by something more — and an algorithm of four rewriting rules finds it or proves there is none. That single computation turns the search for instances from guessing into arithmetic.

logic · Resolution Four proofs about numbers, and what they compute. λn f x. n (λy. f y) (f x) computes n + 1; λn f x. n (λy. f (f y)) x computes 2n; λn f x. n (λy. n (λz. f z) y) x computes n²; λn f x. n (λy. x) (f x) computes 1 at 0, else 0.

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.

logic · Proof systems Raising the input's type, and what becomes computable. N[o]: 299 functions, 0 not extended polynomials; N[o → o]: 163 functions, 42 not extended polynomials; N[(o → o) → o]: 128 functions, 46 not extended polynomials; N[o → o → o]: 72 functions, 33 not extended polynomials.

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.

logic · Proof systems Ackermann's function as one polymorphic term. A : N → N → N; A(0,0)=1 in 6 steps, A(0,1)=2 in 6 steps, A(0,2)=3 in 6 steps, A(0,3)=4 in 6 steps, A(0,4)=5 in 6 steps, A(0,5)=6 in 6 steps, A(1,0)=2 in 10 steps, A(1,1)=3 in 13 steps, A(1,2)=4 in 16 steps, A(1,3)=5 in 19 steps, A(1,4)=6 in 22 steps, A(1,5)=7 in 25 steps, A(2,0)=3 in 17 steps, A(2,1)=5 in 33 steps, A(2,2)=7 in 55 steps, A(2,3)=9 in 83 steps, A(2,4)=11 in 117 steps, A(2,5)=13 in 157 steps, A(3,0)=5 in 37 steps, A(3,1)=13 in 191 steps, A(3,2)=29 in 881 steps, A(3,3)=61 in 3795 steps, A(3,4)=125 in 15765 steps.

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.

logic · Proof systems

Named alongside it

The objects these essays reach for when they reach for this one.

SatisfiabilityCompletenessRefutationSoundnessCut eliminationDecision procedureNormal formResolutionTableauTerminationComplexityComputation

All concepts