Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

Theorem 5: P ⇒ ∼∼P


∀[P:ℙ].(P ⇒ (¬ ¬P)) Extract: λp,np.(np p) where p : P np : ¬P ≡ (P ⇒ False)

Nuprl Proof

Once we unfold the double negation and decompose the implications, we have hypothetical evidence for both P and (P False), and we need to show False. This can be done using the application rule. Notice that we don't need to use the False elimination rule in this proof.

⊢ ∀[P:ℙ]. (P ⇒ (¬ ¬P)) | BY (UD THENA Auto) | [1]. P: ℙ ⊢ P ⇒ (¬ ¬P) | BY (D 0 THENA Auto) Construction rule | 2. P ⊢ ¬ ¬P | BY Unfold `not` 0 | ⊢ (P ⇒ False) ⇒ False Definition of negation | BY (D 0 THENA Auto) Construction rule | 3. P ⇒ False ⊢ False | BY D 3 Application rule on (P ⇒ False) |\ | ⊢ P Subgoal 1: Prove P | | 1 BY NthHyp 2 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