Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
Theorem 18a: ((∃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,x,p. (f <x, p>)
where f : (∃x:T. (P x)) ⇒ C
p : P x
Nuprl Proof
Proving the second transformation is also straightforward for both directions and doesn't require any additional assumptions for a constructive proof. This proof and the next one show how to use the construction and application rules for the existential quantifier.
⊢ ∀[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 (D 0 THENA Auto) ⇒ Construction rule
|
4. (∃x:T. (P x)) ⇒ C
⊢ ∀x:T. ((P x) ⇒ C)
|
BY (D 0 THENA Auto) ∀ Construction rule
|
5. x: T
⊢ (P x) ⇒ C
|
BY (D 0 THENA Auto) ⇒ Construction rule
|
6. P x
⊢ C
|
BY D 4 ⇒ Application rule on ((∃x:T. (P x)) ⇒ C)
|\
| 4. x: T
| 5. P x
| ⊢ ∃x:T. (P x) Subgoal 1: Prove (∃x:T. (P x))
| |
1 BY (InstConcl [⌈x⌉] THENA Auto) ∃ Construction rule, using x
| |
| ⊢ P x
| |
1 BY NthHyp 5 Hypothesis rule
\
4. x: T
5. P x
6. C
⊢ C Subgoal 2: Prove C, with evidence for C now available
|
BY NthHyp 6 Hypothesis rule
- View the proof in PDF format
- Step through the proof in the frame:
Table of Contents