Theorem 9: (P ∨ ∼P) ⇒ (∼∼P ⇒ P)
∀[P:ℙ].((P ∨ (¬P)) ⇒ (¬ ¬P) ⇒ P)
Extract: λf,g. case f of inl(p) => p  inr(np) => any (g np)
where f : P ∨ (¬P)
g : ¬ ¬P ≡ ((¬P) ⇒ False)
p : P
np : ¬P
In the world of decidable propositions, it is interesting that many
people believe that we know this remarkable proposition
(∼∼P ⇒ P).
This asserts that if we know P is not empty, then
we expect that we can find evidence for P or even more strongly,
that there is an operation on this negative evidence that will find
the positive evidence.
When we assume that P is decidable, i.e. that we know (P ∨ ∼P), we can prove (∼∼P ⇒ P) with the use of the False elimination rule.
Nuprl Proof
⊢ ∀[P:ℙ]. ((P ∨ (¬P)) ⇒ (¬ ¬P) ⇒ P)

BY (UD THENA Auto)

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

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

2. P ∨ (¬P)
3. ¬ ¬P
⊢ P

BY D 2 ∨ Application rule on (P ∨ (¬P))
\
 2. P
 ⊢ P Subgoal 1: Prove P, assuming P
 
1 BY NthHyp 2 Hypothesis rule
\
2. ¬P
⊢ P Subgoal 2: Prove P, assuming ¬P

BY Unfold `not` 3

3. (P ⇒ False) ⇒ False Definition of negation
⊢ P

BY D 3 ⇒ Application rule on ((P ⇒ False) ⇒ False)
\
 ⊢ P ⇒ False Subgoal 2.1: Prove (P ⇒ False)
 
1 BY (Unfold `not` 2 THEN NthHyp 2) Definition of negation; hypothesis rule
\
3. False
⊢ P Subgoal 2.2: Prove P, with assumption of False now available

BY FalseHD 3 False elimination rule
Table of Contents