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.

  • $\begingroup$ 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$). $\endgroup$ – Mauro ALLEGRANZA Apr 8 '17 at 12:17
  • $\begingroup$ 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". $\endgroup$ – Mauro ALLEGRANZA Apr 8 '17 at 12:20
  • $\begingroup$ 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. $\endgroup$ – 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 }$

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


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.


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.


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.