Natural deduction of (p->(p->q))->q on the hypothesis that p

Question

I am struggling with natural deduction. I am doing the exercises in Fitch's book and now I am supposed to give an intelim proof of the theorem above (an intelim proof is one that uses only introduction and elimination rules and certain axioms).

I understand that it will be by implication introduction that I prove this. But I find it hard because I become entangled in the subproofs. Is this attempt below correct?

1. p hypothesis
   2. p->(p->q) hypothesis of subproof
   3. p->q by 1,2, modus ponens
   4. p reiteration of 1
   5. q
2. (p->(p->q)->q by 2-5 implication introduction

Help much appreciated!

Answer 1

$\newcommand\lthen{\Rightarrow}$ \begin{align} p&\vdash p&&\text{by assumption}\\ p\lthen(p\lthen q)&\vdash p\lthen(p\lthen q)&&\text{by assumption}\\ p,p\lthen(p\lthen q)&\vdash p\lthen q&&\text{by $\lthen$-elimination}\\ p,p\lthen(p\lthen q)&\vdash q&&\text{by $\lthen$-elimination}\\ p&\vdash(p\lthen(p\lthen q))\lthen q&&\text{by $\lthen$-introduction}\\ \end{align}

Answer 2

Yes, that is okay.   With a minor note that if you may use modus ponens on line 3 without reiterating the premise, you do not need to reiterate the premise to do so the second time.   (Well, it is not wrong to do so, just unnecessary.) $$\def\fitch#1#2{\hspace{2ex}\begin{array}{|l} #1\\\hline #2\end{array}} {\fitch{1.~p\hspace{18ex}\textsf{Premise (Hypothesis of the proof)}}{\fitch{2.~p\to(p\to q)\hspace{4ex}\textsf{Assumption (Hypothesis for the conditional subproof)}}{3.~p\to q\hspace{10.5ex}\textsf{Conditional Elimination 1, 2 (aka modus ponens)}\\4.~q\hspace{15.5ex}\textsf{Conditional Elimination 1, 3}}\\5.~(p\to(p\to q))\to q\hspace{1ex}\textsf{Conditional Introduction 2-4 (aka deduction)}}\\\blacksquare\quad p\vdash (p\to (p\to q))\to q}$$