Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
Theorem 19b: (∃x:T. (C ⇒ (P x))) ⇒ (C ⇒ (∃x:T. (P x)))
∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((∃x:T. (C ⇒ (P x))) ⇒ C ⇒ (∃x:T. (P x)))
Extract: λf,c. let x,g = f in <x, g c>
where f : ∃x:T. (C ⇒ (P x))
c : C
g : C ⇒ (P x)
The reverse direction of the third transformation can be proved constructively without any extra assumptions, as shown in the following proof.
Nuprl Proof
⊢ ∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((∃x:T. (C ⇒ (P x))) ⇒ C ⇒ (∃x:T. (P x)))
|
BY RepeatFor 3 ((UD THENA Auto))
|
[1]. T: Type
[2]. P: T → ℙ
[3]. C: ℙ
⊢ (∃x:T. (C ⇒ (P x))) ⇒ C ⇒ (∃x:T. (P x))
|
BY RepeatFor 2 ((D 0 THENA Auto)) ⇒ Construction rule, 2 times
|
4. ∃x:T. (C ⇒ (P x))
5. C
⊢ ∃x:T. (P x)
|
BY D 4 ∃ Application rule on (∃x:T. (C ⇒ (P x)))
|
4. x: T
5. C ⇒ (P x)
6. C
⊢ ∃x:T. (P x)
|
BY (InstConcl [⌈x⌉] THENA Auto) ∃ Construction rule, using x
|
⊢ P x
|
BY D 5 ⇒ Application rule on (C ⇒ (P x))
|\
| 5. C
| ⊢ C Subgoal 1: Prove C
| |
1 BY NthHyp 5 Hypothesis rule
\
5. C
6. P x
⊢ P x Subgoal 2: Prove (P x), with evidence for (P x) now available
|
BY NthHyp 6 Hypothesis rule
- View the proof in PDF format
- Step through the proof in the frame:
Table of Contents