Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
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
- View the proof in PDF format
- Step through the proof in the frame:
Table of Contents