Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
Theorem 6: (P ⇒ Q) ⇒ (∼Q ⇒ ∼P)
∀[P,Q:ℙ].((P ⇒ Q) ⇒ (¬Q) ⇒ (¬P))
Extract: λpq,nq,p.(nq (pq p))
where pq : P ⇒ Q
nq : ¬Q ≡ (Q ⇒ False)
p : P
This theorem is known as the contrapositive claim. It says that if we know some proposition P implies the proposition Q, then we also know that ∼Q implies ∼P. Using the contrapositive of a statement can be a useful method for proving theorems. The contrapositive claim actually has the same shape as Theorem 3, which states that (A ⇒ B) ⇒ ((B ⇒ C) ⇒ (A ⇒ C)), for propositions A, B, and C. The two theorems are the same when you replace A, B, and C with P, Q, and False, respectively.
Nuprl Proof
⊢ ∀[P,Q:ℙ]. ((P ⇒ Q) ⇒ (¬Q) ⇒ (¬P))

BY RepeatFor 2 ((UD THENA Auto))

[1]. P: ℙ
[2]. Q: ℙ
⊢ (P ⇒ Q) ⇒ (¬Q) ⇒ (¬P)

BY RepeatFor 2 ((D 0 THENA Auto)) Construction rule, 2 times

3. P ⇒ Q
4. ¬Q
⊢ ¬P

BY Unfold `not` 0

⊢ P ⇒ False Definition of negation

BY (D 0 THENA Auto) Construction rule

5. P
⊢ False

BY Unfold `not` 4

4. Q ⇒ False Definition of negation
⊢ False

BY D 3 Application rule on (P ⇒ Q)
\
 3. Q ⇒ False
 4. P
 ⊢ P Subgoal 1: Prove P
 
1 BY NthHyp 4 Hypothesis rule
\
3. Q ⇒ False
4. P
5. Q
⊢ False Subgoal 2: Show False, with evidence for Q now available

BY D 3 Application rule on (Q ⇒ False)
\
 3. P
 4. Q
 ⊢ Q Subgoal 2.1: Prove Q
 
1 BY NthHyp 4 Hypothesis rule
\
3. P
4. Q
5. False
⊢ False Subgoal 2.2: Show False, with the False assumption now available

BY NthHyp 5 Hypothesis rule
 View the proof in PDF format
 Step through the proof in the frame:
Table of Contents