Inference in natural deduction proofs: $(p \to q) \to r \vdash p \to (q \to r).$

Question

I have been tasked by my professor to provide a proof of the following logic statement, including all necessary justifications and claims:

$$(p \to q) \to r \vdash p \to (q \to r)$$

I have applied the rules of inference to break the given premise down into its components, but have made no headway towards a solution. Thus far in the course I haven't been given any other method of proving this statement, so I know it should be solvable using these rules.

What am I missing?

Answer 1

Since what you are trying to prove is a conditional ($\to$), you should use the $\to$ Intro rule.

Now, I don't know exactly how that is defined in your system, but typically that rule implements the 'conditional proof' technique where you assume the antecedent (the 'if' part) of the conditional you are trying to prove, and then show that given that additional assumption, you can derive the consequent (the 'then' part).

So, in your case, given that you want to show $p \to (q \to r)$, you should assume $p$, and try to derive $q \to r$.

And, given that you now want to show $q \to r$, which is another conditional, you set up another $\to$ Intro proof: Assume $q$, and try and get to $r$.

I don't want to give the whole proof away yet ... but does this basic set-up help?

Answer 2

Here is a proof using a Fitch-style natural deduction proof checker which you can use to check your work. The proof checker will make sure you use correct syntax and follow the inference rules which are listed on the right panel. An associated textbook is also available at the link below which may be used as a supplement to the text in your class.

Besides inference introduction and elimination, it uses reiteration (R) which allows me to repeat line 3 on line 5.

---

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