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

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
1. p->(p->q) hypothesis of subproof
2. p->q by 1,2, modus ponens
3. p reiteration of 1
4. q
2. (p->(p->q)->q by 2-5 implication introduction

Help much appreciated!

• Do you mean to prove $p\vdash (p\to(p\to q))\to q$? – Fabio Lucchini Mar 23 at 8:49
• Yes, that is correct! Do say that 5 is the result of applying modus ponens on 3 and 4 – Bram28 Mar 23 at 11:55

$$\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}
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}$$