//
Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

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




Previous Page Next Page


Table of Contents