Logical Investigations, with the Nuprl Proof Assistant  ## 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) | . 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  