Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
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
- View the proof in PDF format
- Step through the proof in the frame:
Table of Contents