Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

Theorem 17a: (C ⇒ (∀x:T. (P x))) ⇒ (∀x:T. (C ⇒ (P x)))


∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((C ⇒ (∀x:T. (P x))) ⇒ (∀x:T. (C ⇒ (P x)))) Extract: λf,x,c. (f c x) where f : (C ⇒ (∀x:T. (P x))) c : C

Nuprl Proof

Proving this first transformation is straightforward and shows how to use the construction and application rules for universal quantification. As we'll see in the next theorem, proving this transformation in the reverse direction is also straightforward. Neither direction requires any additional assumptions for a constructive proof.


⊢ ∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((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 ⇒ (∀x:T. (P x))) ⇒ (∀x:T. (C ⇒ (P x))) | BY (D 0 THENA Auto) ⇒ Construction rule | 4. C ⇒ (∀x:T. (P x)) ⊢ ∀x:T. (C ⇒ (P x)) | BY (D 0 THENA Auto) ∀ Construction rule | 5. x: T ⊢ C ⇒ (P x) | BY (D 0 THENA Auto) ⇒ Construction rule | 6. C ⊢ P x | BY D 4 ⇒ Application rule |\ | 4. x: T | 5. C | ⊢ C Subgoal 1: Prove C | | 1 BY NthHyp 5 Hypothesis rule \ 4. x: T 5. C 6. ∀x:T. (P x) ⊢ P x Subgoal 2: Prove (P x), with evidence for (∀x:T. (P x)) | now available | BY (SimpleInstHyp ⌈x⌉ 6 THENA Auto) ∀ Application rule on (∀x:T. (P x)), | using x | 7. P x ⊢ P x | BY NthHyp 7 Hypothesis rule




Previous Page Next Page


Table of Contents