//
Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

Theorem 6: (PQ) ⇒ (∼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




Previous Page Next Page


Table of Contents