## Theorem 10: ∼∼(*P* ∨ ∼*P*)

As discussed earlier, when we assume propositions are decidable such as the case in a *finitary world*, we know (*P* ∨ ∼*P*). Outside of this world of decidable propositions, we can prove constructively that we know (∼∼(*P* ∨ ∼*P*)).

### Nuprl Proof

By the definition of negation, we can rewrite the goal as (¬(*P* ∨ (¬*P*)) ⇒ *False*) and use the construction rule to decompose this implication. In the proof, we will need to use the hypothesis ¬(*P* ∨ (¬*P*)) twice, in two separate application steps. In Nuprl, once we apply this hypothesis, it will be decomposed and removed. Therefore, we need to duplicate the hypothesis using the tactic Duplicate i, where i is the index of the hypothesis, so that we can use it again later in the proof.

Since ¬(*P* ∨ (¬*P*)) is the same as ((*P* ∨ (¬*P*)) ⇒ *False*), we can reach the goal of *False* if we can prove (*P* ∨ (¬*P*)). We don't have evidence for *P*, so we choose to prove the right side of the disjunction, i.e. (¬*P*) or (*P* ⇒ *False*). Within this subgoal, we decompose the implication and assume evidence for *P* and then show *False*. Once again, we realize that we can reach the goal of *False* if we can prove (*P* ∨ (¬*P*)) and apply the duplicated hypothesis, ¬(*P* ∨ (¬*P*)). Since we have hypothetical evidence for *P* at this point, we can prove (*P* ∨ (¬*P*)) using the left side of the disjunction. The rest of the proof then falls into place.

- View the proof in PDF format
- Step through the proof in the frame:

Table of Contents