Matpic
mathematics, in pictures
Ladder

Proof systems — the ladder

4 distinct arguments against 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.

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

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

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

    rung 4 · logic

All ladders