Propositional Logic: How to prove the contraposition in the Fitch system?

Given that:

p ⇒ q

prove that:

¬q ⇒ ¬p

using the Fitch system.

(This being the proof of the Contraposition)

• Hello and welcome! Just a remark for the next question: Questions like these look as if you wanted to have your homework done by others. We do not encourage this, of course. Therefore, including why this is problematic for you as well as showing your own efforts and where you are stuck would probably result in better and more response. Oct 9 '16 at 0:11
• Thanks Phillip, No I'm not a philosophy -nor mathematics- student, I'm just acquainting myself with logic as an online autodidact.
– Am95
Oct 9 '16 at 12:31
• For the Stanford "Introduction to Logic" course of Michael Genesereth, I presume? An online fitch-style proof assistant can be found here if anyone is interested. That tool should really be improved mightily though. Nov 17 '16 at 16:25
• You are correct @DavidTonhofer
– Am95
Nov 17 '16 at 18:03

1. p => q         Premise
2.   | ~q         Assumption
3.      || p      Assumption
4.      || ~q     Reiteration: 2
5.   | p => ~q    Implication Introduction: 3, 4
6.   | ~p         Negation Introduction: 1, 5
7. ~q => ~p       Implication Introduction: 2, 6
• It works ....... Oct 8 '16 at 15:26

I"m not super familiar with fitch, but here's how I would do it:

First, assume the assumption we are given.

Then figure out the likely path to the conclusion. Given our conclusion is a conditional, there's two or three basic ways to wind up with that. First, there's Material Implication (~a v b |- a -> b). Second, there's conditional introduction -- take an argument that begins with an assumption and bring it down a level as a conditional. Third, there's having it come out of some larger expression.

In this case, the only viable candidate is conditional introduction. Thus, our second line should be the assumption of ~q.

Our next question is how to get to ~p. To end up with a not, we can either do something like DeMorgan's or conditional implication or discharge an assumption due to contradiction. Here, we are going to do the latter.

1. p -> q A

2. | ~q A

3. | | p A

4. | | q MP 1,3

5. | | ~q R 2

6. | | ⊥ Introduction (⊥ Intro) 4,5

7. | ~p Contra. Elim 3-5

8. ~q -> ~p Conditional Introduction 2-6

• Thanks Virmaior, the thing is with Fitch, proving a contradiction is not that simple, putting two contradictory premises following each other doesn't suffice. I tried to do a proof by contradiction like you did, but it was not accepted. It seems that the question was designed not to accept proofs by contradiction. Material Implication, DeMorgan's are not considered Fitch rules. So we don't have many tools at our hands.
– Am95
Oct 8 '16 at 10:56
• Anyways, I managed to solve it, I'll put the answer if anyone is interested.
– Am95
Oct 8 '16 at 11:00
• Corrected per fitch rules at faculty.washington.edu/smcohen/120/Chapter6.pdf . Your proof is basically my proof modified for the fiddly nature of fitch. Oct 8 '16 at 14:21

Using a Fitch-style natural deduction proof editor and checker associated with forall x: Calgary Remix, I can proceed as follows: Line 1 is the premise.

In line 2, I assume "¬Q" and so start a subproof which is indented according to Fitch notation.

In line 3, in order to ultimately arrive at a contradiction, I assume "¬¬P". I use a double negative since I want to remove one of those not-symbols (¬) when I derive a contradiction (⊥).

In line 4, I eliminate the double negative from line 3 which gives me "P".

In line 5, I use that "P" in line 4 and eliminate the conditional (→E) in line 1. This is also called modus ponens, that is, given "P" and "P → Q" I can conclude "Q".

Combining lines 5 with line 2 allows me to introduce a contradiction (⊥I) in line 6.

The contradiction in line 6 allows me to use an indirect proof (IP) to get "¬P" in line 7.

In line 8, I can close the subproof which discharges the assumption made in line 2, by introducing a conditional (→I) based on the subproof in lines 2 through 7.