Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
Theorem 17a: (C ⇒ (∀x:T. (P x))) ⇒ (∀x:T. (C ⇒ (P x)))
∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((C ⇒ (∀x:T. (P x))) ⇒ (∀x:T. (C ⇒ (P x))))
Extract: λf,x,c. (f c x)
where f : (C ⇒ (∀x:T. (P x)))
c : C
Nuprl Proof
Proving this first transformation is straightforward and shows how to use the construction and application rules for universal quantification. As we'll see in the next theorem, proving this transformation in the reverse direction is also straightforward. Neither direction requires any additional assumptions for a constructive proof.
⊢ ∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((C ⇒ (∀x:T. (P x))) ⇒ (∀x:T. (C ⇒ (P x))))
|
BY RepeatFor 3 ((UD THENA Auto))
|
[1]. T: Type
[2]. P: T → ℙ
[3]. C: ℙ
⊢ (C ⇒ (∀x:T. (P x))) ⇒ (∀x:T. (C ⇒ (P x)))
|
BY (D 0 THENA Auto) ⇒ Construction rule
|
4. C ⇒ (∀x:T. (P x))
⊢ ∀x:T. (C ⇒ (P x))
|
BY (D 0 THENA Auto) ∀ Construction rule
|
5. x: T
⊢ C ⇒ (P x)
|
BY (D 0 THENA Auto) ⇒ Construction rule
|
6. C
⊢ P x
|
BY D 4 ⇒ Application rule
|\
| 4. x: T
| 5. C
| ⊢ C Subgoal 1: Prove C
| |
1 BY NthHyp 5 Hypothesis rule
\
4. x: T
5. C
6. ∀x:T. (P x)
⊢ P x Subgoal 2: Prove (P x), with evidence for (∀x:T. (P x))
| now available
|
BY (SimpleInstHyp ⌈x⌉ 6 THENA Auto) ∀ Application rule on (∀x:T. (P x)),
| using x
|
7. P x
⊢ P x
|
BY NthHyp 7 Hypothesis rule
- View the proof in PDF format
- Step through the proof in the frame:
Table of Contents