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