//
Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

Theorem 4: ∼P ⇒ (PQ)


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

Nuprl Proof

We begin the proof using the same steps as in the previous theorems, using the construction rule to decompose the implications in the goal.

⊢ ∀[P,Q:ℙ]. ((¬P) ⇒ P ⇒ Q) | BY RepeatFor 2 ((UD THENA Auto)) | [1]. P: ℙ [2]. Q: ℙ ⊢ (¬P) ⇒ P ⇒ Q | BY RepeatFor 2 ((D 0 THENA Auto)) Construction rule, 2 times | 3. ¬P 4. P ⊢ Q

Now we use the new concepts from negation. We have hypothetical evidence for both P and ¬P, but ¬P can be unfolded to mean (P False). So if we use the application rule to apply (P False) to P we get an assumption of False. By the False elimination rule, from False anything follows, including Q.

[1]. P: ℙ [2]. Q: ℙ 3. ¬P 4. P ⊢ Q | BY Unfold `not` 3 | 3. P ⇒ False Definition of negation ⊢ Q | BY D 3 Application rule on (P ⇒ False) |\ | 3. P | ⊢ P Subgoal 1: Provide evidence for P | | 1 BY NthHyp 3 Hypothesis rule \ 3. P 4. False ⊢ Q Subgoal 2: Prove Q, with the assumption of False now available | BY FalseHD 4 False elimination rule Qed




Previous Page Next Page


Table of Contents