Matpic
mathematics, in pictures
Concept

Natural deduction

A proof system whose rules come in pairs, one saying how to make a formula with a given connective and one saying how to use one. Its distinguishing feature is the discharge, which withdraws an assumption once its consequence has been derived and so turns a conditional derivation into a proof of an implication.

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

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

Named alongside it

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

CompletenessProof systemSoundnessTableauBranchingCut eliminationDecision procedureDischargeImplicationSubformula property

All concepts