//
Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

Theorem 10: ∼∼(P ∨ ∼P)


∀[P:ℙ].(¬ ¬(P ∨ (¬P))) Extract: λf.(f (inr (λp.(f (inl p))))) where f : ¬(P ∨ (¬P)) ≡ ((P ∨ (¬P)) ⇒ False) 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.

⊢ ∀[P:ℙ]. (¬ ¬(P ∨ (¬P))) | BY (UD THENA Auto) | [1]. P: ℙ ⊢ ¬ ¬(P ∨ (¬P)) | BY (D 0 THENA Auto) ⇒ Construction rule; definition of negation | 2. ¬(P ∨ (¬P)) ⊢ False | BY Duplicate 2 | 3. ¬(P ∨ (¬P)) ⊢ False

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.

[1]. P: ℙ 2. ¬(P ∨ (¬P)) 3. ¬(P ∨ (¬P)) ⊢ False | BY (Unfold `not` 3 THEN D 3) ⇒ Application rule on ((P ∨ (¬P)) ⇒ False) |\ | ⊢ P ∨ (P ⇒ False) Subgoal 1: Prove (P ∨ (¬P)), i.e. (P ∨ (P ⇒ False)) | | 1 BY (OrRight THENA Auto) ∨ Construction rule: Prove the right side | | | ⊢ P ⇒ False | | 1 BY (D 0 THENA Auto) ⇒ Construction rule | | | 3. P | ⊢ False | | 1 BY (Unfold `not` 2 THEN D 2) ⇒ Application rule on ((P ∨ (¬P)) ⇒ False) | |\ | | 2. P | | ⊢ P ∨ (P ⇒ False) Subgoal 1.1: Prove (P ∨ (¬P)), i.e. (P ∨ (P ⇒ False)) | | | 1 2 BY (OrLeft THENA Auto) ∨ Construction rule: Prove the left side | | | | | ⊢ P | | | 1 2 BY NthHyp 2 Hypothesis rule | \ | 2. P | 3. False | ⊢ False Subgoal 1.2: Show False, with the assumption of False now available | | 1 BY NthHyp 3 Hypothesis rule \ 3. False ⊢ False Subgoal 2: Show False, with the assumption of False now available | BY NthHyp 3 Hypothesis rule




Previous Page Next Page


Table of Contents