Matpic
mathematics, in pictures
Concept

Cut elimination

The theorem that any sequent-calculus proof using the cut rule, which applies a proved lemma, can be rewritten as one that never does. The lemma-free proof may be far longer, but every formula in it is part of what it proves.

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

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 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 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

Named alongside it

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

Proof systemSubformula propertyImplicationNatural deductionCompletenessComputationDecision procedureDischargeNormal formPolynomialRefutationSatisfiability

All concepts