formal proof of $(p → q) → (¬q → ¬p)$

Question

I'm asked to give a formal proof of $(p → q) → (¬q → ¬p)$ using natural deduction. Is that like saying prove $⊢ (p → q) → (¬q → ¬p$), where it should be proved from nothing?

Answer 1

Hint: the following statements are all equivalent:

• $p\to q$
• $\neg p\lor q$
• $\neg\neg q\lor\neg p$
• $\neg q\to\neg p$

Answer 2

The following proof uses modus tollens (MT):

However, one can derive the modus tollens rule in the following way. This uses the proof provided on page 138 of forallx linked to below along with a link to the proof checker used here:

---

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, Winter 2018. http://forallx.openlogicproject.org/