Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
Theorem 17b: (∀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,x. (f x c)
where f : ∀x:T. (C ⇒ (P x))
c : C
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 0 THENA Auto) ∀ Construction rule
|
6. x: T
⊢ P x
|
BY (SimpleInstHyp ⌈x⌉ 4 THENA Auto) ∀ Application rule on
| (∀x:T. (C ⇒ (P x))), using x
|
7. C ⇒ (P x)
⊢ P x
|
BY D 7 ⇒ Application rule on (C ⇒ (P x))
|\
| ⊢ C Subgoal 1: Prove C
| |
1 BY NthHyp 5 Hypothesis rule
\
7. P x
⊢ P x Subgoal 2: Prove (P x), with evidence for (P x) now available
|
BY NthHyp 7 Hypothesis rule
- View the proof in PDF format
- Step through the proof in the frame:
Table of Contents