## Theorem 4: ∼*P* ⇒ (*P* ⇒ *Q*)

### 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.

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*.

*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*

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

Table of Contents