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