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: