1

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

Improve this question

2 Answers 2

Reset to default
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

Improve this answer
1

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

Done

Improve this answer

You must log in to answer this question.

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