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

Maybe this works for your rules?

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

• Oh my god~! You are amazing~!!! It bothers me from last night. I am so shame of myself. ;( – tang aqua Apr 6 '17 at 1:24
• @tangaqua Do not be ashamed! These logic proofs can be quite tricky! – Bram28 Apr 6 '17 at 1:25

proof

GOAL:     ((p => q) => p) => p                     conclusion


When trying to prove a conditional:

1. Assume the antecedent

2. Try and derive the consequent from your assumption.

In our case (p => q) => p is the antecendent. p is the consequent.

So now we created a separate sub-problem which we have to solve in order to solve our main problem.

Sub-proof

1. (p => q) => p             premise

...

GOAL:   p                     conclusion


How do we prove an atom p when given a conditional? Well we have to use reductio ad absurdum. We assume the negation of our atom ~p. And we attempt to derive a contradiction.

So now we have created a sub-sub-problem.

Sub-sub-proof

1. ~p             premise

...

GOAL:   ~p => z
~p => ~z                    conclusion


where z is some expression.

Instantiating our sub-sub-proof

0. (p => q) => p          premise (we are allowed to reuse this information from the main proof in this subproof)

1. ~p                     premise
2.     p                  assumption
3.         ~q             assumption
4.         p              reiteration                 2
5.     ~q => p            implication introduction    4-5
6.         ~q             assumption
7.         ~p             reiteration                 1
8.     ~q => ~p           implication introduction    6-7
9.     ~~q                negation introduction       5,8
10.    q                  negation elimination        9
11. p => q                implication introduction    1-11
12. p                     implication elimination     0,11
~p => p


Combining the conclusion of our sub-sub-proof with the tautology ~p => ~p we get our desired contradiction.

All together

1.     (p => q) => p             assumption
2.         ~p                    assumption
3.             p                 assumption
4.                 ~q            assumption
5                  p             reiteration                 2
6.             ~q => p           implication introduction    4-5
7.                 ~q            assumption
8.                 ~p            reiteration                 2
9.             ~q => ~p          implication introduction    7-8
10.            ~~q               negation introduction       6,9
11.            q                 negation elimination        10
12.        p => q                implication introduction    3-11
13.        p                     implication elimination     1,12
14.    ~p => p                   implication introduction    2,13
15.        ~p                    assumption
16.    ~p => ~p                  implication introduction    15,15
17.    ~~p                       negation introduction       14,16
18.    p                         negation elimination        17
((p => q) => p) => p           implication introduction    1,18


The issue with this problem seemed to be Stanford Fitch's approach to the negation rules, and their lack of a falsum symbol.

To prove the conditional $$(p\to(p\to q))\to p$$, assume $$(p\to q)\to p$$ aiming to derive $$p$$. IE a conditional proof.

To derive $$p$$ from that assumption, assume $$\lnot p$$ aiming to derive a contradiction. Ie a proof by contradiction.

To derive a contradiction from $$\lnot p$$ and $$(p\to q)\to p$$, seek to derive $$p\to q$$.

To derive $$p\to q$$ from those assumptions, use a conditional proof. Ie: now assume $$p$$.

To derive $$q$$ from the assumptions of $$p$$, $$\lnot p$$, and $$(p\to q)\to p$$, well, we have assumed a contradiction so explode it.

Discharge the assumptions and we are done.

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{}{\fitch{~~1.~(p\to q)\to p\hspace{5ex}\text{Assume}}{\fitch{~~2.~\lnot p\hspace{11ex}\text{Assume}}{\fitch {~3.~p\hspace{10ex}\text{Assume}}{~~4.~\bot\hspace{8ex}\lnot\,\mathsf E, 2,3\\~~5.~q\hspace{9ex}\text{EFQ}}\\~~6.~p\to q\hspace{7ex}\to\mathsf I,3{-}5\\~~7.~p\hspace{12ex}\to\mathsf E, 1,6\\~~8.~\bot\hspace{12ex}\lnot\,\mathsf E,2,7}\\~~9.~\lnot\lnot p\hspace{13ex}\lnot\,\mathsf I,2{-}8\\10.~p\hspace{16ex}\lnot\lnot\,\mathsf E, 9}\\11.~(p\to (q\to p))\to p\hspace{2ex}\to\mathsf I,1{-}10}$$

Now, the Stanford Fitch implimentation's of the negation introduction rule isn't too cumbersome (and what they call negation elimination is usually known as double negation elimination), but the lack of a falsum symbol means they do not have an explicit ex falso quodlibet rule (EFQ). You have to use a proof by contradiction using their negation rules.   It bloats the proofs somewhat.

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{}{\fitch{~~1.~(p\to q)\to p\hspace{5ex}\text{Assume}}{\fitch{~~2.~\lnot p\hspace{11ex}\text{Assume}}{\fitch {~3.~p\hspace{10ex}\text{Assume}}{\color{red}{\fitch{~~4.\lnot q\hspace{5ex}\text{Assume}}{~~5.~\lnot p\hspace{5ex}\mathsf R, 2}\\~~6.~\lnot q\to\lnot p\hspace{2ex}\to\mathsf I, 4{-}5\\\fitch{~~7.~\lnot q\hspace{5ex}\text{Assume}}{~~8.~p\hspace{7ex}\mathsf R, 3}\\~~9.~\lnot q\to p\hspace{3ex}\to\mathsf I, 7{-}8\\10.~~\lnot\lnot q\hspace{6ex}\lnot\,\mathsf I,6,9}\\11.~q\hspace{9ex}\lnot\lnot\,\mathsf E,10}\\12.~p\to q\hspace{7ex}\to\mathsf I,3{-}11\\13.~p\hspace{12ex}\to\mathsf E, 1,12}\\14.~\lnot p\to p\hspace{9ex}\to\mathsf E, 2{-}13\\\fitch{15.~\neg p\hspace{12ex}\text{Assume}}{}\\16.~\lnot p\to\lnot p\hspace{7.5ex}\to\mathsf I,15{-}15\\17.~\lnot\lnot p\hspace{13ex}\lnot\,\mathsf I,14,16\\18.~p\hspace{16ex}\lnot\lnot\,\mathsf E, 17}\\19.~(p\to (q\to p))\to p\hspace{2ex}\to\mathsf I,1{-}18}$$