# How do you prove (p => q => r) => (p => q) => p => r using the Fitch system?

I'm quite new to logic. Thank you for taking the time to review this post. I tried the following and got to the conclusion I wanted but I was never able to prove the statement. • It needs more parentheses. Does p => q => r mean p => (q => r) or (p => q) => r? – Conifold Jul 20 '19 at 5:43

## 1 Answer

As Conifold suggests in a comment you may be having trouble because of ambiguity. I will assume what you are trying to prove is (P→(Q→R))→((P→Q)→(P→R)) without premises.

What you seem to be doing wrong is assuming r on the first line of your proof. This is what you have to derive if I understand the goal correctly.

Here is how this could be done in a different proof checker: Note that the goal is a conditional with antecedent (P→(Q→R)) and consequent ((P→Q)→(P→R)). To derive this I assume the antecedent on line 1 and try to derive the consequent which I succeed in doing on line 8. Then on line 9 I can introduce the conditional (→I) and reach the goal.

For the intermediate steps I realize the consequent is also a conditional. That means it also has an antecedent P→Q and a consequent P→R. So I assume that antecedent on line 2 and try to derive the consequent which I do on line 7. Then using conditional introduction I reach that subgoal on line 8.

Even that consequent is a conditional with antecedent P and consequent R, so I do the same for that conditional as I did for those above. I assume that antecedent on line 3 and derive its consequent on line 6. To do that I used conditional elimination (→E) (modus ponens) three times on lines 4, 5 and 6.

The proof checker I am using and the corresponding textbook are linked below. How you enter this into the proof checker you are using will likely be different, but the steps should be similar.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf