Natural deduction proof for $(a\to(b\to c))\to((a\to b)\to(a\to c))$

Question

I am trying to prove that

$(a\to(b\to c))\to((a\to b)\to(a\to c))$

holds in natural deduction, in particular when I work backwards from a Fitch style proof I can only get so far:

How can I prove it?

Answer 1

You have only to remove the unnecessary LEM application : lines 3,9,10,11, and you will get the correct derivation :

1) $a \to (b \to c)$ --- assumed [a]

2) $a \to b$ --- assumed [b]

3) $a$ --- assumed [c]

4) $b$ --- from 2) and 3), by $\to$-elim

5) $b \to c$ --- from 1) and 3), by $\to$-elim

6) $c$ --- from 5) and 4), by $\to$-elim

7) $a \to c$ --- from 3) and 6), by $\to$-intro, discharging [c]

8) $(a \to b) \to (a \to c)$ --- from 2) and 7) by $\to$-intro, discharging [b]

9) $\vdash (a \to (b \to c)) \to ((a \to b) \to (a \to c))$ --- from 1) and 8) by $\to$-intro, discharging [a].

Answer 2

In line 7. you Hypothesize B.

Don't Hypothesize when you can prove.

You have 4: $A\to B$. and 5: $A$ so you know $B$ via "elim 4, 5".

Replace "7. B Hyp" with "7. B elim 4,5"

Then 9, and 10 are unnecessary. (Not to mention there is no rule and you can't conclude $C$ from $\lnot B$. It's just that $\lnot B$ is impossible if $A$ and $A\to B$. And if $\lnot A$ or $\lnot (A \to B)$ then it doesn't matter if $C$ is true or not.)

===

Oh, yeah remove 11 as 8 is suplants it. And remove 3 as it isn't necessary (and it can't prove the result anyway).

Remove 3. Replace 7. with "B elim 4,5" remove 9,10,11. Then your proof is good. And shorter.

Answer 3

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}$ How exactly does one go about proving a conditional statement?   A Conditional Proof is usually used.   Step one: assume the antecedant.   Step two: derive the consequent.   Step three: introduce the conditional.

Here we have a nesting of conditionals, so we need to nest Conditional Proofs. $$\fitch{}{\fitch{a\to(b\to c)}{\fitch{a\to b}{\fitch{a}{\vdots\\c}\\a\to c}\\(a\to b)\to(a\to c)}\\(a\to(b\to c))\to((a\to b)\to(a\to c))}$$

Well, you understand that, I see, but your trouble is how do we get from $a$ to $c$?   Now, the assumptions we have made are $a$ and two condtionals with $a$ as an antecedant.   This indicates that both those conditionals may be eliminated, and doing so gives $b$ and $b\to c$.

One more elimination and we are done.

$$\fitch{}{\fitch{~~1.~a\to(b\to c)~;\textsf{assumption}}{\fitch{~~2.~a\to b~;\textsf{assumption}}{\fitch{~~3.~a~;\textsf{assumption}}{~~4.~b~: \textsf{conditional elimination (2,3)}\\~~5.~b\to c~: \textsf{conditional elimination (1,3)}\\~~6.~c~: \textsf{conditional elimination (4,5)}}\\~~7.~a\to c~: \textsf{conditional introduction (3-6)}}\\~~8.~(a\to b)\to(a\to c)~: \textsf{conditional introduction (2-7)}}\\~~9.~(a\to(b\to c))\to((a\to b)\to(a\to c))~: \textsf{cond. intro. (1-8)}}$$