Matpic
mathematics, in pictures
Concept

Discharge

In natural deduction, the step that withdraws an assumption once a conclusion has been reached from it. It is what turns a derivation of B from A into a proof of the implication A → B that depends on nothing.

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

Named alongside it

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

ImplicationNatural deductionProof systemBranchingCompletenessCut eliminationSoundnessSubformula propertyTableau

All concepts