Fitch Proof - LPL Exercise 8.17

Question

I am currently finding the third part of this exercise (Conditional 3) difficult to prove. I was sure that my proof was correct, but the Fitch program is saying otherwise.

I am finding it particularly difficult to understand why my citing and rule are incorrect in line 12.

Can someone show me how to do it on fitch?

Prove: ∴ (P → Q) ↔ (¬Q → ¬P)

Answer 1

Fitch is correct.

First, you are falling for the formal fallacy affirming the consequent in your subproof at 11-13 to generate the contradiction. Denying the antecedent looks like:

1. A → B
2. B
3. Therefore, A

In your case ,

1. ~Q → ~P
2. ~P
3. Therefore, ~Q

Second, you are discharging the subproof incorrectly. At 10, you assume Q, but at 15 you discharge as P → Q. Instead, (if the inside were accurate), it would be Q → P.

If instead, you use modus tollens instead of affirming the consequent, you can reach your proof. Modus tollens is:

1. P → Q
2. ~Q
3. Therefore, ~P.

Spelled out more directly:

10. | | P
11. | | ~~P DN 10
12. | | ~~Q MT 9,11
13. | | Q DN
14. | P → Q CP 10-13

Fitch might not have MT. In which case, you can prove it:

1. A → B
2. ~B
3. | A Assumption
4. | B MP 1,3
5. | ⊥ 2,4 ⊥ Introduction
6. ~A 3-5 ¬ Intro

Answer 2

There are two questions.

I agree with virmaior's answer to what was incorrect in line 12. The problem was caused by affirming the consequent.

The second question asks how to do this using Fitch. Although I also agree with virmaior's outline of how to prove this, here is a checked solution:

References

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/