//
Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

Theorem 18b: (∀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,p = g in f x p where f : ∀x:T. ((P x) ⇒ C) g : ∃x:T. (P x) p : P x

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 5 ∃ Application rule on (∃x:T. (P x)) | 5. x: T 6. P x ⊢ C | BY (SimpleInstHyp ⌈x⌉ 4 THENA Auto) ∀ Application rule on | (∀x:T. ((P x) ⇒ C)), using x | 7. (P x) ⇒ C ⊢ C | BY D 7 ⇒ Application rule on ((P x) ⇒ C) |\ | ⊢ P x Subgoal 1: Prove (P x) | | 1 BY NthHyp 6 Hypothesis rule \ 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