Matpic
mathematics, in pictures
Series

Proof systems — the series

6 essays on one idea, from the one that introduces it to the one that assumes the rest.
  1. 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.

    part 1 · logic
  2. 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.

    part 2 · logic
  3. 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.

    part 3 · logic
  4. 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.

    part 4 · logic
  5. 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.

    part 5 · logic
  6. 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.

    part 6 · logic

All series