When constructing proofs using [natural deduction](http://en.wikipedia.org/wiki/Natural_deduction) what does it mean to say that an assumption or premise is *discharged*? In what circumstances would I want to, or need to, use such a mechanism?


The reason I'm asking this question is that many texts on logic use this term as understood by the reader and don't take the time to adequately explain the technical sense in which they are using it.



What does it mean to 'discharge assumptions or premises'?
As I understand it, to discharging a premise or assumption is the opposite of introducing it: you absorb it (for example) into the antecedent of an implication --- this means that it is no longer an assumption. A trivial example:


P 1. Assume P


\_\_


P 2. From 1


\_\_


P->P 3. Discharging 1


Thus I have concluded that P->P without any assumptions (iow |- P->P). If we didn't discharge the assumption, we would have P|-P


