Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
Theorem 5: P ⇒ ∼∼P
∀[P:ℙ].(P ⇒ (¬ ¬P))
Extract: λp,np.(np p)
where p : P
np : ¬P ≡ (P ⇒ False)
Nuprl Proof
Once we unfold the double negation and decompose the implications, we have hypothetical evidence for both P and (P ⇒ False), and we need to show False. This can be done using the application rule. Notice that we don't need to use the False elimination rule in this proof.
⊢ ∀[P:ℙ]. (P ⇒ (¬ ¬P))
|
BY (UD THENA Auto)
|
[1]. P: ℙ
⊢ P ⇒ (¬ ¬P)
|
BY (D 0 THENA Auto) Construction rule
|
2. P
⊢ ¬ ¬P
|
BY Unfold `not` 0
|
⊢ (P ⇒ False) ⇒ False Definition of negation
|
BY (D 0 THENA Auto) Construction rule
|
3. P ⇒ False
⊢ False
|
BY D 3 Application rule on (P ⇒ False)
|\
| ⊢ P Subgoal 1: Prove P
| |
1 BY NthHyp 2 Hypothesis rule
\
3. False
⊢ False Subgoal 2: Show False, with the assumption of False now available
|
BY NthHyp 3 Hypothesis rule
- View the proof in PDF format
- Step through the proof in the frame:
Table of Contents