Discharge Glossary
Definition
In the natural deduction calculus, an assumption is discharged when the conclusion of an inference does not depend on it, although one of the premises of the inference does.
Technically, this occurs when the conclusion is an immediate consequence not of the premise itself, but of a sub-derivation with that formula as its conclusion and the discharged one as assumption.
Comments
In annotating a line of proof to say that it comes from a sub-derivation, discharging an assumption, we cite the line number of the conclusion of the sub-derivation and mention the discharged assumption in square brackets. This is just a notational convention; other formats for laying out proofs may cite the whole sub-derivation, for instance.
Vacuous discharge: In classical logic, discharge is always optional. It does not matter whether a discharged assumption has been used more than once in the derivation, or even whether it has been used at all. If the assumption has not occurred in the derivation, the discharge is said to be vacuous. Vacuous discharge allows formulae which do not apear in the derivation at all to be treated as though the conclusion came from them. Our notation for such vacuous discharge is to write empty square brackets.
Examples
-
Discharge of the assumption p
IMP q by the
introduction rule for
implication:
SP {p ⊢ (p IMP q) IMP q} PL {1} {1} {p} {A} PL {2} {2} {p IMP q} {A} PL {1,2} {3} {q} {1, 2 IMPE} PL {1} {4} {(p IMP q) IMP q} {3 [2] IMPI} EP -
Discharge of assumed disjuncts p
and q by the
elimination rule for disjunction:
SP {p IMP r, q IMP r, p OR q ⊢ r} PL {1} {1} {p IMP r} {A} PL {2} {2} {q IMP r} {A} PL {3} {3} {p OR q} {A} PL {4} {4} {p} {A} PL {1,4} {5} {r} {1, 4 IMPE} PL {6} {6} {q} {A} PL {2,6} {7} {r} {2, 6 IMPE} PL {1,2,3} {8} {r} {3, 5 [4], 7 [6] ORE} EP -
Vacuous discharge
of NOTq by
RAA:
SP {p, NOTp ⊢ q} PL {1} {1} {p} {A} PL {2} {2} {NOTp} {A} PL {1,2} {3} {NOTNOTq} {1, 2 [ ] RAA} PL {1,2} {4} {q} {3 NOTNOTE} EP