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