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

Question

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.

Answer 1

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