So I have a question regarding natural deduction, are we allowed to "copy" our previous assumption inside a new assumption. I will use an example to illustrate.
$\vdash$ $P\Rightarrow(Q\Rightarrow P)$
So here are my steps.
1.) $P$ Assumption
2.)$Q$ Assumption
3.)$P$ Copy (1)
4.)$Q \Rightarrow P$ Implication Introduction
5.)$P \Rightarrow (Q \Rightarrow P)$ Implication Introduction
Is my proof correct, or is there something missing.
On
Just to make it clear why your solution is correct, here it is in Fitch-style: $\def\imp{\Rightarrow}$
Solution
If $P$: [(1)]
If $Q$:
$P$. [(2); copy from (1)]
$Q \imp P$. [(3); implication introduction from (2)]
$P \imp ( Q \imp P )$. [implication introduction from (3)]
Notes
Intuitively it is obviously correct because whatever you can assert outside of any assumption is still true inside the assumption. That allows you to copy the outer assumption under the inner assumption as you did. The rest is just implication introduction as you did, which is nothing more than collapsing the assumption structure into a single line.
Yes, your proof is correct (modulo $P$ is added using a different rule than $Q$).
In natural deduction you have structural rules called contraction, weakening, and exchange. $$ \frac{S,P,P,T \vdash Q}{S,P,T \vdash Q}\ \text{contraction} \quad \frac{S,T \vdash Q}{S, P, T \vdash Q}\ \text{weakening} \quad \frac{S,P,Q,T \vdash R}{S,Q,P,T \vdash R}\ \text{exchange} $$
Usually, these rules are used silently by saying that the collection of assumptions forms a set. You can imagine not having these as structural rules which leads to substructural logic, the most notable of which is linear logic which drops contraction and weakening.
We can now describe your proof (with the minor correction): $P$ is introduced via $P \vdash P$, then $Q$ is added to the assumptions via weakening ($P,Q \vdash P$), then you use contraction to duplicate $P$ ($P,P,Q \vdash P$) and exchange to bring it to the front of the context($P,Q,P\vdash P$), then two uses of implication introduction.