//
Skip to main content
PRL Project

Constructive reading of classical logic
Table of Contents

Previous Page Next Page

Kleene 97: {∃x:T.(A ⇒ (B x)) ⇔ (A ⇒ (∃x:T.(B x)))}


∀[T:Type]. (T ⇒ (∀[A:ℙ]. ∀[B: T → ℙ]. {∃x:T.(A ⇒ (B x)) ⇔ (A ⇒ (∃x:T.(B x)))}
{∃x:T.(A ⇒ (B x)) ⇒ A ⇒ ∃x:T.(B x)} ⇒ Extract: λf.λa.spread(f; x,g.<x;ap(g.a)>)
∃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

Previous Page Next Page


Table of Contents