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)

My attempt

  • 1
    You tried to deduce (12) ~Q from (9) ~Q->~P and (11) ~P. That's not a correct usage of implication elimination. – Eliran Aug 21 '16 at 17:23
  • When wishing to deduce P->Q you should assume P aiming to derive Q. – Graham Kemp May 20 '19 at 3:03

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

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:

enter image description 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/

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.