Natural Deducion: assumptions can be used more than once?

Question

Im trying to prove: $ \forall{x}\forall{y}(P(x,y)\rightarrow{}\sim P(y,x)) \vdash \forall{x} \sim P(x,x)$

What i have:

1. $\forall{x}\forall{y}(P(x,y)\rightarrow{}\sim P(y,x))\;$ Premise
2. $ \forall{y}(P(x,y)\rightarrow{}\sim P(y,x)) \;\;\;\;\;$ $\forall{}E\;1$
3. $ P(x,x)\rightarrow{}\sim P(x,x)) \;\;\;\;\;\;\;\;\;\;$ $\forall{}E\;2$
4. --- $P(x,x)\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$ Assumption H1
5. --- $ P(x,x)\rightarrow{}\sim P(x,x)) \;\;\;\;\;$ It 3
6. --- $\sim P(x,x)\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$ $\rightarrow{}E\;4,5$ (is H1 discharged?)
7. --- $ \perp \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$ Contradiction 4,6
8. $\sim P(x,x)$
9. $\forall{x} \sim P(x,x)$

Im not sure this is correct. I know premises can be used anywhere, but im not sure if the assumption H1 can be used twice. If that is the case, then H1 must be discharged twice?, or it can be discharged when the subproof is over?

Answer 1

The assumption is not discharged on line 5.   This is merely a redundant repetition of line 3.   That is okay, however it is redundant and repeated.

Line 7 is the statement that line 4 and 6 are contradictory. $A, \neg A\vdash \bot$ .   The assumption is not yet discharged; though it is set up.

The assumption is discharged on line 8 with   $\Gamma, (\Gamma\wedge A)\to\bot~\vdash~ \neg A~$ (Contradiction Elimination).   The premise and the assumption infers a contradiction, therefore the premise entails that the assumption is false.

$$\dfrac{\Gamma, A\vdash\bot}{\Gamma \vdash \neg A}{\small(\bot\mathsf E)}$$

Answer 2

When you make an assumption, you're creating a mini universe in which the assumption is true. In that universe, you can reference the assumption as much as you want, just like you can reference premises and other statements as much as you like throughout the proof. Then, when you have done everything you need to with the assumption - either you've reached a contradiction, or you develop a statement of the form (Assumption -> Conclusion), and at that point you dismiss the assumption because the universe has done its job and can be returned to the aether again.