//
Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

Theorem 20a: (C ∨ (∼C)) ⇒ (∃x:T. True) ⇒                   
                  ((∼(∀x:T. (P x))) ⇒ (∃x:T. (∼(P x)))) ⇒
                     ((∀x:T. (P x)) ⇒ C) ⇒ (∃x:T. ((P x) ⇒ C))


∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((C ∨ (¬C)) ⇒ (∃x:T. True) ⇒ ((¬(∀x:T. (P x))) ⇒ (∃x:T. (¬(P x)))) ⇒ ((∀x:T. (P x)) ⇒ C) ⇒ (∃x:T. ((P x) ⇒ C))) Extract: λd,e,f,g. case d of inl(c) => let x,true = e in <x, λp.c> | inr(nc) => let x,np = f (λp1.(nc (g p1))) in <x, λp2.any (np p2)> where d : C ∨ (¬C) e : ∃x:T. True f : (¬(∀x:T. (P x))) ⇒ (∃x:T. (¬(P x))) g : (∀x:T. (P x)) ⇒ C c : C p : P x nc : ¬C ≡ (C ⇒ False) np : ¬(P x) p1 : ∀x:T. (P x) p2 : P x

The forward direction of the fourth transformation has no constructive proof in general and is the most difficult to discuss constructively. The classical proof can be accomplished by assuming that C is decidable (C ∨ ∼C), the domain is inhabited (x:T. True), and by assuming a "Markovian domain" in which (∼∀x. (P x)) (∃x.∼(P x)). So in cases when these classical assumptions hold constructively, the transformation is justified. The proof shown below also requires ex falso quodlibet by way of the False elimination rule.


Nuprl Proof


⊢ ∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. | ((C ∨ (¬C)) ⇒ (∃x:T. True) ⇒ | ((¬(∀x:T. (P x))) ⇒ (∃x:T. (¬(P x)))) ⇒ | ((∀x:T. (P x)) ⇒ C) ⇒ (∃x:T. ((P x) ⇒ C))) | BY RepeatFor 3 ((UD THENA Auto)) | [1]. T: Type [2]. P: T → ℙ [3]. C: ℙ ⊢ (C ∨ (¬C)) ⇒ (∃x:T. True) ⇒ | ((¬(∀x:T. (P x))) ⇒ (∃x:T. (¬(P x)))) ⇒ | ((∀x:T. (P x)) ⇒ C) ⇒ (∃x:T. ((P x) ⇒ C)) | BY RepeatFor 4 ((D 0 THENA Auto)) ⇒ Construction rule, 4 times | 4. C ∨ (¬C) 5. ∃x:T. True 6. (¬(∀x:T. (P x))) ⇒ (∃x:T. (¬(P x))) 7. (∀x:T. (P x)) ⇒ C ⊢ ∃x:T. ((P x) ⇒ C) | BY D 4 ∨ Application rule on (C ∨ (¬C)) |\ | 4. C | ⊢ ∃x:T. ((P x) ⇒ C) Subgoal 1: Prove (∃x:T. ((P x) ⇒ C)), | | assuming evidence for C | | 1 BY D 5 ∃ Application rule on (∃x:T. True) | | | 5. x: T | 6. True | 7. (¬(∀x:T. (P x))) ⇒ (∃x:T. (¬(P x))) | 8. (∀x:T. (P x)) ⇒ C | ⊢ ∃x:T. ((P x) ⇒ C) | | 1 BY (InstConcl [⌈x⌉] THENA Auto) ∃ Construction rule, using x | | | ⊢ (P x) ⇒ C | | 1 BY (D 0 THENA Auto) ⇒ Construction rule | | | 9. P x | ⊢ C | | 1 BY NthHyp 4 Hypothesis rule \ 4. ¬C ⊢ ∃x:T. ((P x) ⇒ C) Subgoal 2: Prove (∃x:T. ((P x) ⇒ C)), | assuming evidence for (¬C) | BY D 6 ⇒ Application rule on (¬(∀x:T. (P x))) ⇒ (∃x:T. (¬(P x))) |\ | 6. (∀x:T. (P x)) ⇒ C | ⊢ ¬(∀x:T. (P x)) Subgoal 2.1: Prove ¬(∀x:T. (P x)) | | 1 BY (D 0 THENA Auto) ⇒ Construction rule; definition of negation | | | 7. ∀x:T. (P x) | ⊢ False | | 1 BY D 6 ⇒ Application rule on ((∀x:T. (P x)) ⇒ C) | |\ | | 6. ∀x:T. (P x) | | ⊢ ∀x:T. (P x) Subgoal 2.1.1: Prove (∀x:T. (P x)) | | | 1 2 BY NthHyp 6 Hypothesis rule | \ | 6. ∀x:T. (P x) | 7. C | ⊢ False Subgoal 2.1.2: Show False, with evidence for C now available | | 1 BY (Unfold `not` 4 THEN D 4) ⇒ Application rule on (C ⇒ False) | |\ | | 4. ∃x:T. True | | 5. ∀x:T. (P x) | | 6. C | | ⊢ C Subgoal 2.1.2.1: Prove C | | | 1 2 BY NthHyp 6 Hypothesis rule | \ | 4. ∃x:T. True | 5. ∀x:T. (P x) | 6. C | 7. False | ⊢ False Subgoal 2.1.2.2: Show False, | | with assumption of False now available | | 1 BY NthHyp 7 Hypothesis rule \ 6. (∀x:T. (P x)) ⇒ C 7. ∃x:T. (¬(P x)) ⊢ ∃x:T. ((P x) ⇒ C) Subgoal 2.2: Prove (∃x:T. ((P x) ⇒ C)), | with evidence for (∃x:T. (¬(P x))) now available | BY D 7 ∃ Application rule on (∃x:T. (¬(P x))) | 7. x: T 8. ¬(P x) ⊢ ∃x:T. ((P x) ⇒ C) | BY (InstConcl [⌈x⌉] THENA Auto) ∃ Construction rule, using x | ⊢ (P x) ⇒ C | BY (D 0 THENA Auto) ⇒ Construction rule | 9. P x ⊢ C | BY (Unfold `not` 8 THEN D 8) ⇒ Application rule on ((P x) ⇒ False) |\ | 8. P x | ⊢ P x Subgoal 2.2.1: Prove (P x) | | 1 BY NthHyp 8 Hypothesis rule \ 8. P x 9. False ⊢ C Subgoal 2.2.2: Prove C, with assumption of False now available | BY FalseHD 9 False elimination rule




Previous Page Next Page


Table of Contents