Skip to main content
PRL Project

Constructive reading of classical logic
Table of Contents

Previous Page Next Page

Kleene 85: {~(∀x:T.{A x}) ⇔ ∃x:T.~(A x)}


∀[T:Type]. ∀[A: T → ℙ]. {¬(∀x:T.{A x}) ⇔ ∃x:T.¬(A x)}
{∃x:T.¬(A x) ⇒ ¬(∀x:T.{A x})} ⇐ Extract: λf.λg.spread(f; x,nax.ap(nax.ap(g.x)))
∃x:T.¬(A x) ⇒ ¬(∀x:T.{A x})by λ(f.___)
f : ∃x:T.¬(A x) ⊢ ¬(∀x:T.{A x})by λ(g.___)
f : ∃x:T.¬(A x), g : ∀x:T.{A x} ⊢ Falseby spread(f; x,nax.___)
g : ∀x:T.{A x}, x : T, nax : ¬(A x) ⊢ Falseby apseq(g;x;ax.___)
ax : {A x}, x : T, nax : ¬(A x) ⊢ Falseby Open {A x} with False
ax : (A x), x : T, nax : ¬(A x) ⊢ Falseby ap(nax.___)
ax : (A x), x : T ⊢ (A x)by ax

{¬(∀x:T.{A x}) ⇒ ∃x:T.¬(A x)} ⇒ Extract: λf.(CC;g.any(ap(f.λx.(CC;nax.any(ap(g;<x;nax>))))))
{¬(∀x:T.{A x}) ⇒ ∃x:T.¬(A x)}by λ(f.___)
f : ¬(∀x:T.{A x}) ⊢ {∃x.T:¬(A x)}by (CC{∃x.T:¬(A x)};g.___) Classical contradiction
f : ¬(∀x:T.{A x}), g : ¬(∃x:T.¬(A x)) ⊢ {∃x.T:¬(A x)}by seqap(f;___;False.any(..))
g : ¬(∃x:T.¬(A x)) ⊢ ∀x:T.{A x}by λ(x.___)
g : ¬(∃x:T.¬(A x)), x : T ⊢ {A x}by (CC{A x};nax.___) Classical contradiction
g : ¬(∃x:T.¬(A x)), x : T, nax : ¬(A x) ⊢ {A x}by seqap(g;___;False;any(..))
x : T, nax : ¬(A x) ⊢ ∃x:T.¬(A x)by pair(x;___)
x : T, nax : ¬(A x) ⊢ ¬(A x)by nax

Nuprl Proof

⊢ ∀[T:Type]. ∀[A:T → ℙ]. {¬(∀x:T.{A x}) ⇔ ∃x:T.(¬(A x))} | BY (D 0 THENA Auto) |\ | 1. T: Type | ⊢ ∀[A:T → P]. {¬(∀x:T. {A x}) ⇔ ∃x:T. (¬(A x))} | | 1 BY (D 0 THENA Auto) | |\ | | 2. A: T → P | | ⊢ {¬(∀x:T. {A x}) ⇔ ∃x:T. (¬(A x))} | | | 1 2 BY RepeatFor 4 ((D 0 THENA Auto)) | | |\ | | | 3. ¬(∀x:T. {A x}) | | | ⊢ {∃x:T. (¬(A x))} | | | | 1 2 3 BY (ClassicalContradiction THENA Auto) | | | | | | | 4. ¬(∃x:T. (¬(A x))) | | | ⊢ {∃x:T. (¬(A x))} | | | | 1 2 3 BY D 3 | | | | | | | 3. ¬(∃x:T. (¬(A x))) | | | ⊢ ∀x:T. {A x} | | | | 1 2 3 BY (D 0 THENA Auto) | | | | | | | 4. x: T | | | ⊢ {A x} | | | | 1 2 3 BY (ClassicalContradiction¬∑ THENA Auto) | | | | | | | 5. ¬(A x) | | | ⊢ {A x} | | | | 1 2 3 BY D 3 | | | | | | | 3. x: T | | | 4. ¬(A x) | | | ⊢ ∃x:T. (¬(A x)) | | | | 1 2 3 BY (InstConcl [dxe]¬∑ THENA Auto) | | | | | | | ⊢ ¬(A x) | | | | 1 2 3 BY Hypothesis | | \ | | 3. ∃x:T. (¬(A x)) | | ⊢ {¬(∀x:T. {A x})} | | | 1 2 BY (ElimClassical THENA Auto) | | | | | ⊢ ¬(∀x:T. {A x}) | | | 1 2 BY (D 0 THENA Auto) | | | | | 4. ∀x:T. {A x} | | ⊢ False | | | 1 2 BY D 3 | | | | | 3. x: T | | 4. ¬(A x) | | 5. ∀x:T. {A x} | | ⊢ False | | | 1 2 BY (InstHyp [dxe] 5¬∑ THENA Auto) | | | | | 6. {A x} | | ⊢ False | | | 1 2 BY D 6 | | | | | 6. x@0: Unit | | 7. A x | | ⊢ False | | | 1 2 BY D 4 | | | | | 4. ∀x:T. {A x} | | 5. x@0: Unit | | 6. A x | | ⊢ A x | | | 1 2 BY Hypothesis | \ | 2. A: T → P | 3. {x:Unit| ¬(∀x:T. {A x}) ⇔ ∃x:T. (¬(A x))} | ⊢ Ax ∈ {x:Unit| ¬(∀x:T. {A x}) ⇔ ∃x:T. (¬(A x))} | | 1 BY Auto \ 1. T: Type 2. A: T → P 3. {x:Unit| ¬(∀x:T. {A x}) ⇔ ∃x:T. (¬(A x))} ⊢ Ax ∈ {x:Unit| ¬(∀x:T. {A x}) ⇔ ∃x:T. (¬(A x))} | BY Auto Proof


Previous Page Next Page


Table of Contents