Logic deduction with Fitch system

Question

I was working through some logic and I found a difficulty I can't solve,

How can I proof from the premise p=>q, that ¬q=>¬p?

Thank you

Answer 1

Using the Fitch System:

1. p=>q............Premise
2. .| ¬q............Assumption
3. .|.| p............Assumption
4. .|.| q............Implication Elimination: 1,3
5. .|.| ¬q............Reiteration: 2
6. .| p=>¬q............Implication Introduction: 5
7. .| ¬p............Negation Introduction: 1,6
8. ¬q=>¬p............Implication Introduction: 7

Not so neat layout, but each 'indentation' represents sub-proofs done with the help of the assumptions.

Answer 2

Fine tuning with the removal of a redundant step:

Using the Fitch System:

1. p=>q............Premise
2. | ¬q............Assumption
3. |.| p............Assumption
4. |.| ¬q............Reiteration: 2
5. | p=>¬q............Implication Introduction: 4
6. | ¬p............Negation Introduction: 1,5
7. ¬q=>¬p............Implication Introduction: 6

Answer 3

Here is a proof using a Fitch-style proof checker. Explanations for the rules are in forallx. Both references are available online and listed below:

---

Reference

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/