//

Logical Investigations, with the Nuprl Proof Assistant

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

Website feedback
PRL Project   |   Computer Science Department   |   Cornell University
nuprl@cs.cornell.edu   |   320 Gates Hall, Ithaca, NY 14853   |   © 2014 Cornell University
site admin | Prof Constable's Library