Constructive reading of classical logic
Table of Contents
Kleene 97: {∃x:T.(A ⇒ (B x)) ⇔ (A ⇒ (∃x:T.(B x)))}
| ∃x:T.(A ⇒ (B x)) ⇒ A ⇒ ∃x:T.(B x) | by λ(f.___) |
| f : ∃x:T.(A ⇒ (B x)) ⊢ A ⇒ ∃x:T.(B x) | by λ(a.___) |
| f : ∃x:T.(A ⇒ (B x)), a : A ⊢ ∃x:T.(B x) | by spread(f; x, g.____) |
| x : T, g : A ⇒ (B x), a : A ⊢ ∃x:T.(B x) | by pair(x;___) |
| x : T, g : A ⇒ (B x), a : A ⊢ (B x) | by apseq(g;a;bx.bx) |
{A ⇒ ∃x:T.(B x) ⇒∃x:T.(A ⇒ (B x))}
⇐ Extract: λf.(CC;g.<x;λa.spread(ap(f.a); x1,bx1.any(ap(g.<x1;λa.bx1>)))>)
| (T ⇒ (∀[A:ℙ]. ∀[B: T → ℙ]. {(A ⇒ (∃x:T.(B x))) ⇒ ∃x:T.(A ⇒ (B x)} | |
| t : T ⊢ {(A ⇒ (∃x:T.(B x))) ⇒ ∃x:T.(A ⇒ (B x)} | by λ(f.____) |
| t : T, f : A ⇒ ∃x:T.(B x) ⊢ {∃x:T.(A ⇒ (B x)} | by (CC{∃x:T.(A ⇒ (B x)};g.___) Classical contradiction |
| t : T, f : A ⇒ ∃x:T.(B x), g : ¬(∃x:T.(A ⇒ (B x)) ⊢ {∃x:T.(A ⇒ (B x)} | by Rename 't' to 'x', then unsquash goal |
| x : T, f : A ⇒ ∃x:T.(B x), g : ¬(∃x:T.(A ⇒ (B x)) ⊢ ∃x:T.(A ⇒ (B x) | by pair(x;____) |
| x : T, f : A ⇒ ∃x:T.(B x), g : ¬(∃x:T.(A ⇒ (B x)) ⊢ A ⇒ (B x) | by λ(a.___) |
| x : T, f : A ⇒ ∃x:T.(B x), g : ¬(∃x:T.(A ⇒ (B x)), a : A ⊢ (B x) | by seqap(f;a;h.___) |
| x : T, h : ∃x:T.(B x), g : ¬(∃x:T.(A ⇒ (B x)), a : A ⊢ (B x) | by spread(h; x1,bx1.___) |
| x : T, x1 : T, bx1 : (B x1), g : ¬(∃x:T.(A ⇒ (B x)), a : A ⊢ (B x) | by seqap(g;___;False.any(..)) |
| x : T, x1 : T, bx1 : (B x1), a : A ⊢ ∃x:T.(A ⇒ (B x) | by pair(x1;___) |
| x : T, x1 : T, bx1 : (B x1), a : A ⊢ A ⇒ (B x1) | by λ(a.___) |
| x : T, x1 : T, bx1 : (B x1), a : A ⊢ (B x1) | by bx1 |
Nuprl Proof
⊢ ∀[T:Type]. (T ⇒ (∀[B:T → ℙ]. ∀[A:ℙ]. {∃x:T.(A ⇒ (B x)) ⇔ (A ⇒ (∃x:T.(B x)))}
|
BY Auto
|
1. T: Type
2. T
3. A: ℙ
4. B: T → ℙ
⊢ {∃x:T.(A ⇒ (B x)) ⇔ (A ⇒ (∃x:T.(B x)))}
|
BY RepeatFor 4 ((D 0 THENA Auto))
|\
| 5. ∃x:T.(A ⇒ (B x))
| ⊢ {A ⇒ (∃x:T. (B x))}
| |
1 BY RepeatFor 2 ((D 0 THENA Auto))
| |
| 6. A
| ⊢ {∃x:T. (B x)}
| |
1 BY D 5
| |
| 5. x: T
| 6. A ⇒ (B x)
| 7. A
| ⊢ {∃x:T. (B x)}
| |
1 BY (ElimClassical THENA Auto) Unsquash goal
| |
| ⊢ ∃x:T. (B x)
| |
1 BY (InstConcl [⌈x⌉]· THENA Auto)
| |
| ⊢ B x
| |
1 BY D 6
| |\
| | 6. A
| | ⊢ A
| | |
1 2 BY Hypothesis
| \
| 6. A
| 7. B x
| ⊢ B x
| |
1 BY Hypothesis
\
5. A ⇒ (∃x:T. (B x))
⊢ {∃x:T.(A ⇒ (B x))}
|
BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses
|
6. ¬(∃x:T. (A ⇒ (B x)))
⊢ {∃x:T.(A ⇒ (B x))}
|
1
BY RenameVar 'x' 2
|
2. x: T
⊢ {∃x:T.(A ⇒ (B x))}
|
BY (ElimClassical THENA Auto) Unsquash goal
|
⊢ ∃x:T.(A ⇒ (B x))
|
BY (InstConcl [⌈x⌉]· THENA Auto)
|
⊢ A ⇒ (B x)
|
BY (D 0 THENA Auto)
|
7. A
⊢ B x
|
BY D 5
|\
| 5. ¬(∃x:T. (A ⇒ (B x)))
| 6. A
| ⊢ A
| |
1 BY Hypothesis
\
5. ¬(∃x:T. (A ⇒ (B x)))
6. A
7. ∃x:T. (B x)
⊢ B x
|
BY D 7
|
7. x1: T
8. B x1
⊢ B x
|
BY D 5
|
5. A
6. x1: T
7. B x1
⊢ ∃x:T. (A ⇒ (B x))
|
BY (InstConcl [⌈x1⌉]· THENA Auto)
|
⊢ A ⇒ (B x1)
|
BY (D 0 THENA Auto)
|
8. A
⊢ B x1
|
BY Hypothesis
PDF version of proof
Table of Contents