Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
Theorem 18b: (∀x:T. ((P x) ⇒ C)) ⇒ ((∃x:T. (P x)) ⇒ C)
∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((∀x:T. ((P x) ⇒ C)) ⇒ (∃x:T. (P x)) ⇒ C)
Extract: λf,g. let x,p = g in f x p
where f : ∀x:T. ((P x) ⇒ C)
g : ∃x:T. (P x)
p : P x
Nuprl Proof
⊢ ∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((∀x:T. ((P x) ⇒ C)) ⇒ (∃x:T. (P x)) ⇒ C)
|
BY RepeatFor 3 ((UD THENA Auto))
|
[1]. T: Type
[2]. P: T → ℙ
[3]. C: ℙ
⊢ (∀x:T. ((P x) ⇒ C)) ⇒ (∃x:T. (P x)) ⇒ C
|
BY RepeatFor 2 ((D 0 THENA Auto)) ⇒ Construction rule, 2 times
|
4. ∀x:T. ((P x) ⇒ C)
5. ∃x:T. (P x)
⊢ C
|
BY D 5 ∃ Application rule on (∃x:T. (P x))
|
5. x: T
6. P x
⊢ C
|
BY (SimpleInstHyp ⌈x⌉ 4 THENA Auto) ∀ Application rule on
| (∀x:T. ((P x) ⇒ C)), using x
|
7. (P x) ⇒ C
⊢ C
|
BY D 7 ⇒ Application rule on ((P x) ⇒ C)
|\
| ⊢ P x Subgoal 1: Prove (P x)
| |
1 BY NthHyp 6 Hypothesis rule
\
7. C
⊢ C Subgoal 2: Prove C, with evidence for C now available
|
BY NthHyp 7 Hypothesis rule
- View the proof in PDF format
- Step through the proof in the frame:
Table of Contents