//
Skip to main content
PRL Project

Constructive reading of classical logic
Table of Contents

Previous Page Next Page

Kleene 83: {∃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,ax.ap(ap(g.x).ax)))
∃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,ax.___)
x : T, ax : (A x), g : ∀x:T.¬(A x)⊢ Falseby apseq(g;x;nax.___)
x : T, ax : (A x), nax : ¬(A x)⊢ Falseby ap(nax.__)
x : T, ax : (A x) ⊢ (A x)by ax
{¬(∀x:T.¬(A x)) ⇒ ∃x.T:(A x)} ⇐ Extract: λf.(CC;g.any(ap(f.λx.λax.ap(g.<x;ax>))))
{¬(∀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 apseq(f;___;False.any(..))
g : ¬(∃x.T:(A x)) ⊢ ∀x:T.¬(A x)by λ(x.___)
g : ¬(∃x.T:(A x)), x : T ⊢ ¬(A x)by λ(ax.___)
g : ¬(∃x.T:(A x)), x : T, ax : (A x) ⊢ Falseby ap(g.___)
x : T, ax : (A x) ⊢ ∃x.T:(A x)by pair(x;___)
x : T, ax : (A x) ⊢ (A x)by ax

Nuprl Proof


⊢ ∀[T:Type]. ∀[A:T → ℙ]. {∃x:T.(A x) ⇔ ¬(forall;x:T.¬(A x))} | BY (D 0 THENA Auto) |\ | 1. T: Type | ⊢ ∀[A:T → ℙ]. {∃x:T. (A x) ⇔ ¬(∀x:T. (¬(A x)))} | | 1 BY (D 0 THENA Auto) | |\ | | 2. A: T → ℙ | | ⊢ {∃x:T. (A x) ⇔ ¬(∀x:T. (¬(A x)))} | | | 1 2 BY (D 0 THENA Auto) | | | | | ⊢ {(∃x:T. (A x)) ⇒ (¬(∀x:T. (¬(A x))))} ∧ {(∃x:T. (A x)) ⇐ ¬(∀x:T. (¬(A x)))} | | | 1 2 BY (RepeatFor 2 (D 0) THENA Auto) | | |\ | | | ⊢ (∃x:T. (A x)) ⇒ {¬(∀x:T. (¬(A x)))} | | | | 1 2 3 BY (D 0 THENA Auto) | | | | | | | 3. ∃x:T. (A x) | | | ⊢ {¬(∀x:T. (¬(A x)))} | | | | 1 2 3 BY (ElimClassical THENA Auto) Unsquash goal | | | | | | | ⊢ ¬(∀x:T. (¬(A x))) | | | | 1 2 3 BY (D 0 THENA Auto) | | | | | | | 4. ∀x:T. (¬(A x)) | | | ⊢ False | | | | 1 2 3 BY D 3 | | | | | | | 3. x: T | | | 4. A x | | | 5. ∀x:T. (¬(A x)) | | | ⊢ False | | | | 1 2 3 BY (InstHyp [⌈x⌉] THENA Auto) | | | | | | | 6. ¬(A x) | | | ⊢ False | | | | 1 2 3 BY D 6 | | | | | | | ⊢ A x | | | | 1 2 3 BY Hypothesis | | \ | | ⊢ (¬(∀x:T. (¬(A x)))) ⇒ {∃x:T. (A x)} | | | 1 2 BY (D 0 THENA Auto) | | | | | 3. ¬(∀x:T. (¬(A x))) | | ⊢ {∃x:T. (A x)} | | | 1 2 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses | | | | | 4. ¬(∃x:T. (A x)) | | ⊢ {∃x:T. (A x)} | | | 1 2 BY D 3 | | | | | 3. ¬(∃x:T. (A x)) | | ⊢ ∀x:T. (¬(A x)) | | | 1 2 BY (D 0 THENA Auto) | | | | | 4. x: T | | ⊢ ¬(A x) | | | 1 2 BY (D 0 THENA Auto) | | | | | 5. A x | | ⊢ False | | | 1 2 BY D 3 | | | | | 3. x: T | | 4. A x | | ⊢ ∃x:T. (A x) | | | 1 2 BY (InstConcl [⌈x⌉] THENA Auto) | | | | | ⊢ A x | | | 1 2 BY Hypothesis | \ | 2. A: T → ℙ | 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 → ℙ 3. {x:Unit| ∃x:T. (A x) ⇔ ¬(∀x:T. (¬(A x)))} ⊢ Ax ∈ {x:Unit| ∃x:T. (A x) ⇔ ¬(∀x:T. (¬(A x)))} | BY Auto PDF version of proof

Previous Page Next Page


Table of Contents