Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
Theorem 4: ∼P ⇒ (P ⇒ Q)
∀[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
 View the proof in PDF format
 Step through the proof in the frame:
Table of Contents