I'm getting a bit stuck in a tailspin on this one. I'm quite new to logic. I'm not sure how or when we use negation to get P. How then does that connect to (¬p ⇒ q) ⇒ ((¬p ⇒ ¬q)?

my attempts so far have me in a knot

2 Answers 2


A truth table would show this is a tautology, so one can try deriving this without premises. Here is a proof using the proof checker associated with forallx. Something similar should work with Fitch:

enter image description here

On line 1, I assume the antecedent of the conditional I would like to derive. The consequent of that conditional is also a conditional so on line 2 I make another assumption assuming the antecedent of that conditional.

Then I notice that if I assume on line 3 ¬P I can derive a contradiction using modus ponens or conditional elimination (→E) which I do on lines 4 and 5. On line 6 I note that I have a contradiction. You may have to use a conjunction of lines 4 and 5 to show that in your proof checker.

With that contradiction I can use indirect proof (IP) on line 7 to discharge the assumption made on line 3 and derive P. On lines 8 and 9 I can use conditional introduction to derive the goal.

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, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf


You have assumed things in the worng order, and missed the significance of being able to derive both q and ~q .

In order to prove (~ p > q) > ((~p > ~q) > p) you must first assume (~p > q), aiming to derive ((~p > ~q) > p) , so that a conditional proof may be used (aka Implication Introduction in Stanford's Fitch system).

Likewise, in order to derive ((~p > ~q) > p) under that assumption, you must next assume (~p > ~q) aiming to derive p.

Stanford's Fitch System takes allows ~~p to be derived from the two assumptions using their version of the Negation Introduction rule, and you can then use what they call Negation Elimination to derive p.

|  |_ ~p > q                   Assumption
|  |  |_ ~p > ~q               Assumption
|  |  |  ~~p                   Negation Introduction
|  |  |  p                     Negation Elimination
|  |  (~p > ~q) > p            Implication Introduction
|  (~p > q) > ((~p > ~q) > p)  Implication Introduction 


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.