How do I prove the tautology $\vdash((p\rightarrow q)\rightarrow p)\rightarrow p$ using natural deduction? I'm trying to prove $\vdash((p\rightarrow q)\rightarrow p)\rightarrow p$.
The best attempt I can come up with is as follows:


*

*$((p\to q)\to p)$     Assumption

*$p\to q$            Assumption

*$p$               $\to$ Elimination 1,2

*$((p\to q)\to p)\to p$  $\to$ Introduction 1,2-3


But I'm sure it's completely invalid as the ways the implications are eliminated and introduced don't match the way they are in other examples I've seen.
Also, am I correct in saying that this is a tautology? Or is it a theorem? I get the two confused.
 A: I'll start answering from the bottom.
The mathematical object $((p\rightarrow q)\rightarrow p)\rightarrow p$ is both a tautology and a theorem. In principle they are different concepts (check the definitions), but the completeness theorem for propositional calculus tells you that every tautology is a theorem and vice-versa.
As for the proof, what you're doing doesn't work. The second assumption isn't wrong per se, but it's odd. The very last step is wrong because the $p$ you inferred on the third step is 'inside' yet another assumption, it's not at the same level as the first assumption which is what you desire.
Here's an idea for proving it. The details will depend on which rules you have available. Start by assuming $(p\to q)\to p$. Next, hoping to find a contradiction, suppose $\color{red}{\neg p}$ holds. From this new assumption prove that $p\to q$ holds, then eliminate $\to$ in $(p\to q)\to p$ and get $p$. Careful, this $p$ you infer here is not at the appropriate level. Here you get a contradiction and are able to deduce $\neg \neg p$ from the red assumption.
A: Here's the proof you are looking for. You can find more information here.

This proof was constructed using the Panda Proof assistant.
Or in Fitch format: $$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{}{\fitch{~~1.~~(p\to q)\to p\hspace{8ex}:\text{assumption}}{\fitch{~~2.~~\lnot p\hspace{8ex}:\text{assumption}}{\fitch{~~3.~~p\hspace{8ex}:\text{assumption}}{~~4.~~p\land\lnot p\hspace{8ex}:\text{conjunction introduction}\\~~5.~~q\hspace{8ex}:\text{explosion (ex falso quodlibet}}\\~~6.~~p\to q\hspace{8ex}:\text{conditional introduction}\\~~7.~~p\hspace{8ex}:\text{conditional elimination (modus ponens)}\\~~8.~~p\land\lnot p\hspace{8ex}:\text{conjunction introduction}}\\~~9.~~\lnot\lnot p\hspace{8ex}:\text{negation introduction}\\10.~~p\hspace{8ex}:\text{double negation elimination}}\\11.~~((p\to q)\to p)\to p\hspace{8ex}:\text{conditional introduction}}$$
