Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
Theorem 19a: (C ∨ (∼C)) ⇒ (∃x:T. True) ⇒
(C ⇒ (∃x:T. (P x))) ⇒ (∃x:T. (C ⇒ (P x)))
∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ].
((C ∨ (¬C)) ⇒ (∃x:T. True) ⇒ (C ⇒ (∃x:T. (P x))) ⇒ (∃x:T. (C ⇒ (P x))))
Extract: λf,g,h. case f of
inl(c) => let x,p = h c in <x, λc1.p>
| inr(nc) => let x,true = g in <x, λc2.any (nc c2)>
where f : C ∨ (¬C)
g : ∃x:T. True
h : C ⇒ (∃x:T. (P x))
c : C
p : P x
c1 : C
nc : ¬C ≡ (C ⇒ False)
c2 : C
The forward direction of the third transformation is not constructively justified, but it can be proved constructively by assuming that C is decidable (C ∨ ∼C) and by assuming that the domain is inhabited (∃x:T. True). This approach also requires ex falso quodlibet by way of the False elimination rule.
Nuprl Proof
⊢ ∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ].
| ((C ∨ (¬C)) ⇒ (∃x:T. True) ⇒ (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 ∨ (¬C)) ⇒ (∃x:T. True) ⇒ (C ⇒ (∃x:T. (P x))) ⇒ (∃x:T. (C ⇒ (P x)))
|
BY RepeatFor 3 ((D 0 THENA Auto)) ⇒ Construction rule, 3 times
|
4. C ∨ (¬C)
5. ∃x:T. True
6. C ⇒ (∃x:T. (P x))
⊢ ∃x:T. (C ⇒ (P x))
|
BY D 4 ∨ Application rule on (C ∨ (¬C))
|\
| 4. C
| ⊢ ∃x:T. (C ⇒ (P x)) Subgoal 1: Prove (∃x:T. (C ⇒ (P x))),
| | assuming evidence for C
| |
1 BY D 6 ⇒ Application rule on (C ⇒ (∃x:T. (P x)))
| |\
| | ⊢ C Subgoal 1.1: Prove C
| | |
1 2 BY NthHyp 4 Hypothesis rule
| \
| 6. ∃x:T. (P x)
| ⊢ ∃x:T. (C ⇒ (P x)) Subgoal 1.2: Prove (∃x:T. (C ⇒ (P x))),
| | with evidence for (∃x:T. (P x)) now available
| |
1 BY D 6 ∃ Application rule on (∃x:T. (P x))
| |
| 6. x: T
| 7. P x
| ⊢ ∃x:T. (C ⇒ (P x))
| |
1 BY (InstConcl [⌈x⌉] THENA Auto) ∃ Construction rule, using x
| |
| ⊢ C ⇒ (P x)
| |
1 BY (D 0 THENA Auto) ⇒ Construction rule
| |
| 8. C
| ⊢ P x
| |
1 BY NthHyp 7 Hypothesis rule
\
4. ¬C
⊢ ∃x:T. (C ⇒ (P x)) Subgoal 2: Prove (∃x:T. (C ⇒ (P x))),
| assuming evidence for (¬C)
|
BY D 5 ∃ Application rule on (∃x:T. True)
|
5. x: T
6. True
7. C ⇒ (∃x:T. (P x))
⊢ ∃x:T. (C ⇒ (P x))
|
BY (InstConcl [⌈x⌉] THENA Auto) ∃ Construction rule, using x
|
⊢ C ⇒ (P x)
|
BY (D 0 THENA Auto) ⇒ Construction rule
|
8. C
⊢ P x
|
BY (Unfold `not` 4 THEN D 4) ⇒ Application rule on (C ⇒ False)
|\
| 4. x: T
| 5. True
| 6. C ⇒ (∃x:T. (P x))
| 7. C
| ⊢ C Subgoal 2.1: Prove C
| |
1 BY NthHyp 7 Hypothesis rule
\
4. x: T
5. True
6. C ⇒ (∃x:T. (P x))
7. C
8. False
⊢ P x Subgoal 2.2: Prove (P x), with assumption of False now available
|
BY FalseHD 8 False elimination rule
- View the proof in PDF format
- Step through the proof in the frame:
Table of Contents