Currently, I am self-teaching myself formal logic from E.J. Lemmon's Beginning Logic. So far, the book is discussing the rules of derivation for propositional logic, and I've struggled to fully understand the conditional proof rule.
The book gives a proof of P->Q |- (-Q)->(-P)
1 (1) P->Q assumption
2 (2) -Q assumption
1,2 (3) -P 1, 2 modus tollens
1 (4) -Q-> -P 2, 3 Conditional Proof
Since the negation of P is obtained by assuming the negation of Q, the negation of Q implies the negation of P; I understand how the rule allows one to put an implication into a conditional. However, what I fail to understand is why the assumption of 2 is discharged. Isn't it necessary to assume the negation of Q? Why does line 4 not depend upon the assumption of -Q? Lemmons says that when one uses conditional proof, there is always a discharged assumption. Why can one discharge an assumption in proving a conditional?