Logical Investigations, with the Nuprl Proof Assistant

Theorem 19a: (C ∨ (∼C)) ⇒ (∃x:T. True) ⇒                                       (C ⇒ (∃x:T. (Px))) ⇒ (∃x:T. (C ⇒ (Px)))

∀[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