# Use Fitch system to proof ((p ⇒ q) ⇒ p) ⇒ p without any premise. ONLY FOR FITCH SYSTEM.

I know here has few similar questions, but I cannot figure out with those answer. Since for Fitch system, I can only use And Intro, And Elim, Or Inro, Or Elim, Neg Intro, Neg Elim, Impl Intro, Impl Elim, Biconditional Intro, and Biconditional Elim.

I know I need to assume (p=>q)=>p then for next I need to prove p, at the end I can use Imlo Intro. But I don't know how to prove p...

I saw some answers like: (p=>q)=>p assume 1 p assume 2 ~p assume 3 q neg Elim with 2 or 3

I stop at this step..NOt sure why I can get q from 2 and 3? Since Neg Elim follows this form ( ~~p get p) and also Neg Intro follows (p=>q, p=>~q, get ~p). But from what I learn I can not get the q from just assume 2 and 3...

I tried in Fitch system, But it doesn't work with the answer from other questions. So that's right I post here again. Wish someone can help me.

• The "fine details" depend on the set of rules: unfortunately, there are some different systems called Natural Deduction and the differences are mainly located in the management of $\lnot$ (or of $\bot$, where $\lnot P$ is defined as $P \to \bot$ and thus the rules for $\lnot$ are derived from those for $\to$). – Mauro ALLEGRANZA Apr 8 '17 at 12:17
• In the rules set I've linked, we have $\lnot$-Elim: "from $p, \lnot p$, derive $\bot$" that means: from a contradiction we can derive the propositional constant "the falsum" that is always false, and $\bot$-Elim: "from $\bot$, derive $q$", called Ex Falso Quodlibet. The two together licensed the derivation: "from $p, \lnot p$, derive $q$, with $q$ whatever", called the Principle of Explosion". – Mauro ALLEGRANZA Apr 8 '17 at 12:20
• Another possibility os with Double Negation Elimination: "from $\lnot \lnot p$, derive $p$" as per answer below. See here for a review of the rules. – Mauro ALLEGRANZA Apr 8 '17 at 12:41

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$
$\fitch{}{ \fitch{ 1. (p \rightarrow q) \rightarrow p \quad Assumption}{ \fitch{ 2. \neg p \quad Assumption}{ \fitch{ 3. p \quad Assumption}{ \fitch{ 4. \neg q \quad Assumption}{ 5. p \quad Reiteration \ 3}\\ 6. \neg q \rightarrow p \quad \rightarrow Intro \ 4-5\\ \fitch{ 7. \neg q \quad Assumption}{ 8. \neg p \quad Reiteration \ 2}\\ 9. \neg q \rightarrow \neg p \quad \rightarrow Intro \ 7-8\\ 10. \neg \neg q \quad \neg Intro \ 6,9\\ 11. q \quad \neg Elim \ 10}\\ 12. \quad \quad p \rightarrow q \quad \rightarrow Intro \ 3-11\\ 13. \quad \quad p \quad \rightarrow Elim \ 1,12}\\ 14. \quad \neg p \rightarrow p \quad \rightarrow Intro \ 2-13\\ \fitch{ 15. \quad \quad \neg p \quad Assumption}{ 16. \quad \quad \neg p \quad Reiteration \ 15}\\ 17. \quad \neg p \rightarrow \neg p \quad \rightarrow Intro \ 15-16\\ 18. \quad \neg \neg p \quad \neg Intro \ 14,17\\ 19. \quad p \quad \neg Elim \ 18}\\ 20. ((p \rightarrow q) \rightarrow p) \rightarrow p \quad \rightarrow Intro \ 1-19 }$