p ⇒ q
¬q ⇒ ¬p
using the Fitch system.
(This being the proof of the Contraposition)
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
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
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.