Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
Theorem 20b: (∃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,h = f in h (g x)
where f : ∃x:T. ((P x) ⇒ C)
g : ∀x:T. (P x)
h : (P x) ⇒ C
The reverse direction of the fourth transformation can be proved constructively without any additional assumptions, as shown in the following proof.
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 4 ∃ Application rule on (∃x:T. ((P x) ⇒ C))
|
4. x: T
5. (P x) ⇒ C
6. ∀x:T. (P x)
⊢ C
|
BY (SimpleInstHyp ⌈x⌉ 6 THENA Auto) ∀ Application rule on (∀x:T. (P x)),
| using x
|
7. P x
⊢ C
|
BY D 5 ⇒ Application rule on ((P x) ⇒ C)
|\
| 5. ∀x:T. (P x)
| 6. P x
| ⊢ P x Subgoal 1: Prove (P x)
| |
1 BY NthHyp 6 Hypothesis rule
\
5. ∀x:T. (P x)
6. P x
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