# Quick question on discharging assumptions

Could someone explain conceptually what the consequences are of assumptions NOT being discharged in a natural deduction ? Suppose the objective is to establish a claim of the form : 'If A,then B.' Further,suppose one proves B by assuming A, then one concludes that 'if A,then B' without the assumption A (i.e the assumption is discharged).Presumably this means that the veracity of 'if A,then B' does not depend on assuming A ? What happens when one does not discharge A? What is the harm in having 'if A,then B' be dependent on the assumption A?

Hopefully this question makes sense! Thank you for your time.

• The typical context is that after assuming A one also assumes some E somewhere in the course of the proof. If E is discharged before B is derived (e.g. by showing that not-E is impossible) then "if A then B" has been proved. If not, then E becomes an additional assumption upon which the proof depends, so only "if A and E then B" has been proved. – Conifold Jul 2 '19 at 20:19

As Conifold notes in a comment, if you made an assumption that you used to derive the conclusion, but you did not discharge that assumption, then you need to add that assumption to the premises.

Some (if not all) proof checkers will not allow you to proceed in that case, requiring that you restart the problem with new premises.

However, if you made assumptions that you did not need, that is, you did not need them to derive the goal, then you can consider the proof complete even with those assumptions not discharged. For example, consider this proof in the forallx proof checker:

I could have derived P from P on line 2 using reiteration (R) and referencing line 1. This would make for a shorter proof. However, I made some unnecessary assumptions, A on line 2, B on line 3, and C on line 4. I would not know how to discharge such assumptions even if I tried. I would have to start over if I were forced to discharge them. But all I have to do is derive P from line 1 on line 5. Since I did not use any of those three assumptions, but I only used the premise P to derive P, the proof checker reported: "This proof is correct."

Other proof checkers may behave differently, but I used only the premises I started with and so it seems reasonable for a proof checker to accept the proof at that point. Those three assumptions are like premises that I did not use.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf

• Thank you! Is this correct : if one does NOT discharge assumptions used in a ND proof, one is magically using information NOT contained in the premisses of the argument to establish validity.Therefore, even if one can construct a proof with these assumptions drawn from beyond the set of premisses, one has not established the argument itself which involves moving from the set of premisses to the conclusion. However, if one could link the assumptions made, back to premisses residing in the permissable set,the conlusion would depend on precisely those premisses and not the discharged assumption? – HalfAFoot Jul 3 '19 at 5:55
• @HalfAFoot If one uses an assumption to reach the conclusion, that is, there is a derived line leading to the conclusion that references that assumption, then one has to do one of two things: (1) discharge that assumption to complete the ND proof, or (2) start over with that assumption as one of the premises. However, if one doesn't use the assumption then one doesn't need to discharge it. Actually there is no point in making an assumption that one doesn't use just like there is no point in listing a premise that one doesn't need. Those extra premises or assumptions just make the proof longer. – Frank Hubeny Jul 3 '19 at 10:55
• Yes thanks again. – HalfAFoot Jul 3 '19 at 14:08