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.
    – E...
    Commented Aug 21, 2016 at 17:23
  • When wishing to deduce P->Q you should assume P aiming to derive Q. Commented May 20, 2019 at 3:03

2 Answers 2


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/

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .