4
$\begingroup$

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.

$\endgroup$
  • $\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
4
$\begingroup$

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

$\endgroup$
  • $\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

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.