## 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} ⊢ False by spread(f; x,nax.___) g : ∀x:T.{A x}, x : T, nax : ¬(A x) ⊢ False by apseq(g;x;ax.___) ax : {A x}, x : T, nax : ¬(A x) ⊢ False by Open {A x} with False ax : (A x), x : T, nax : ¬(A x) ⊢ False by 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