Kleene 99

PRL Home Introduction Math Library Publications Projects System

Seminar People The Book Lectures Other Groups

Constructive reading of classical logic

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

This proposition is intuitively "true" in the standard classical semantics. We imagine that ∀x:T.(A x) is either true or false. If it is true, then we know Exists x:T.(B x). Call this element of T, t. We can use that t as the witness for the conclusion: ∃x:T.((A x) ⇒ (B x)).

If ~(∀x:T.(A x)), then by another classical fact, we know Exists x:T. ~ Ax. Let t' be that value, so we know ~At', and which means At' ⇒ Bt' by simple classical propositional logic. Thus ∃x:T.((A x) ⇒ (B x)).

As a constructive argument using virtual evidence, this is a bit delicate, nevertheless correct, and we show the extract below.

There is another constructive argument using Brouwer's Continuity Principle, that gives a real construction for this proposition for certain kinds of types T, such as the natural numbers, N, establishing its limited constructive validity in an elegant way. This topic will be discussed in a forthcoming note referencing new results of the PRL group published in 2015.

∀[T:Type]. ∀[A, B:T → ℙ]. {∃x:T.((A x) ⇒ (B x)) ⇔ ∀x.T:{A x} ⇒ ∃x:T.(B x)}
{∃x:T.((A x) ⇒ (B x)) ⇒ ∀x.T:{A x} ⇒ ∃x:T.(B x)}    
⇒ Extract:λf.λg.spread(f; x,h.<x;ap(h.ap(g.x))>)  
  
{∃x:T.((A x) ⇒ (B x)) ⇒ ∀x.T:{A x} ⇒ ∃x:T.(B x)}by λ(f.____)
f : ∃x:T.((A x) ⇒ (B x)) ⊢ {∀x.T:{A x} ⇒ ∃x:T.(B x)}by λ(g.___)
f : ∃x:T.((A x) ⇒ (B x)), g : ∀x.T:{A x} ⊢ {∃x:T.(B x)}by spread(f; x,h.____)
x : T, h : (A x) ⇒ (B x), g : ∀x.T:{A x} ⊢ {∃x:T.(B x)}by apseq(g;x;ax.___)
x : T, h : (A x) ⇒ (B x), ax : {A x} ⊢ {∃x:T.(B x)}by Open {A x} and then {∃x:T.(B x)}
x : T, h : (A x) ⇒ (B x), ax : A x ⊢ ∃x:T.(B x)by pair(x;___)
x : T, h : (A x) ⇒ (B x), ax : A x ⊢ (B x)by apseq(h;ax;bx.bx)

{∀x.T:{A x} ⇒ ∃x:T.(B x) ⇒ ∃x:T.((A x) ⇒ (B x))}
⇐ Extract: λf.(CC;g.spread(ap(f.λx.(CC;nax.any(ap(g.<x;λax.any(ap(nax.ax))>)))); x,bx.<x;λax.bx>))
  
{∀x.T:{A x} ⇒ ∃x:T.(B x) ⇒ ∃x:T.((A x) ⇒ (B x))}by λ(f.____)
f : ∀x.T:{A x} ⇒ ∃x:T.(B x) ⊢ {∃x:T.((A x) ⇒ (B x))}by (CC{∃x:T.((A x) ⇒ (B x))};g.___)  Classical contradiction
f : ∀x.T:{A x} ⇒ ∃x:T.(B x), g : ¬(∃x:T.((A x) ⇒ (B x)) ⊢ {∃x:T.((A x) ⇒ (B x))}by apseq(f;  slot1  ;h.  slot2  )
g : ¬(∃x:T.((A x) ⇒ (B x)) ⊢ ∀x.T:{A x}by λ(x.___)  for slot1
g : ¬(∃x:T.((A x) ⇒ (B x)), x : T ⊢ {A x}by (CC{A x};nax.___)   Classical contradiction
g : ¬(∃x:T.((A x) ⇒ (B x)), x : T nax : ¬(A x) ⊢ {A x}by apseq(g;___;False.any(..))
g : ¬(∃x:T.((A x) ⇒ (B x)), x : T, nax : ¬(A x) ⊢ ∃x:T.((A x) ⇒ (B x))by pair(x;___)
g : ¬(∃x:T.((A x) ⇒ (B x)), x : T, nax : ¬(A x) ⊢ (A x) ⇒ (B x)by λ(ax;___)
g : ¬(∃x:T.((A x) ⇒ (B x)), x : T, nax : ¬(A x), ax : (A x) ⊢ (B x)by apseq(nax;ax;False.any(..))
h : ∃x:T.(B x), g : ¬(∃x:T.((A x) ⇒ (B x)) ⊢ {∃x:T.((A x) ⇒ (B x))}by spread(h; x,bx.___) then unsquash goal  for slot2
x : T, bx :(B x), g : ¬(∃x:T.((A x) ⇒ (B x)) ⊢ ∃x:T.((A x) ⇒ (B x))by pair(x;___)
x : T, bx :(B x), g : ¬(∃x:T.((A x) ⇒ (B x)) ⊢ (A x) ⇒ (B x)by λ(ax.___)
x : T, bx :(B x), g : ¬(∃x:T.((A x) ⇒ (B x)), ax : (A x) ⊢ (B x)by bx

Nuprl Proof

⊢ ∀[T:Type]. ∀[A,B:T → ℙ]. {∃x:T.((A x) ⇒ (B x)) ⇔ ∀x:T.{A x} ⇒ ∃x:T.(B x)} | BY Auto | 1. T: Type 2. A: T → ℙ 3. B: T → ℙ ⊢ {∃x:T. ((A x) ⇒ (B x)) ⇔ (∀x:T. {A x}) ⇒ (∃x:T. (B x))} | BY RepeatFor 4 ((D 0 THENA Auto)) |\ | 4. ∃x:T. ((A x) ⇒ (B x)) | ⊢ {(∀x:T. {A x}) ⇒ (∃x:T. (B x))} | | 1 BY RepeatFor 2 ((D 0 THENA Auto)) | | | 5. ∀x:T. {A x} | ⊢ {∃x:T. (B x)} | | 1 BY D 4 | | | 4. x: T | 5. (A x) ⇒ (B x) | 6. ∀x:T. {A x} | ⊢ {∃x:T. (B x)} | | 1 BY (InstHyp [⌈x⌉] 6· THENA Auto) | | | 7. {A x} | ⊢ {∃x:T. (B x)} | | 1 BY (ExposeClassical THENA Auto) Open squashed hypothesis with squashed goal | | | 7. A x | ⊢ {∃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 5 | |\ | | 5. ∀x:T. {A x} | | 6. A x | | ⊢ A x | | | 1 2 BY Hypothesis | \ | 5. ∀x:T. {A x} | 6. A x | 7. B x | ⊢ B x | | 1 BY Hypothesis \ 4. (∀x:T. {A x}) ⇒ (∃x:T. (B x)) ⊢ {∃x:T. ((A x) ⇒ (B x))} | BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses | 5. ¬(∃x:T. ((A x) ⇒ (B x))) ⊢ {∃x:T. ((A x) ⇒ (B x))} | BY D 4 |\ | 4. ¬(∃x:T. ((A x) ⇒ (B x))) | ⊢ ∀x:T. {A x} | | 1 BY (D 0 THENA Auto) | | | 5. x: T | ⊢ {A x} | | 1 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses | | | 6. ¬(A x) | ⊢ {A x} | | 1 BY D 4 | | | 4. x: T | 5. ¬(A x) | ⊢ ∃x:T. ((A x) ⇒ (B x)) | | 1 BY (InstConcl [⌈x⌉] THENA Auto) | | | ⊢ (A x) ⇒ (B x) | | 1 BY (D 0 THENA Auto) | | | 6. A x | ⊢ B x | | 1 BY D 5 | | | 5. A x | ⊢ A x | | 1 BY Hypothesis \ 4. ¬(∃x:T. ((A x) ⇒ (B x))) 5. ∃x:T. (B x) ⊢ {∃x:T. ((A x) ⇒ (B x))} | BY D 5 | 5. x: T 6. B x ⊢ {∃x:T. ((A x) ⇒ (B x))} 2 | BY (ElimClassical THENA Auto) Unsquash goal | ⊢ ∃x:T. ((A x) ⇒ (B x)) | BY (InstConcl [⌈x⌉]· THENA Auto) | ⊢ (A x) ⇒ (B x) | BY (D 0 THENA Auto) | 7. A x ⊢ B x | BY Hypothesis PDF version of proof

Table of Contents

{∃x:T.((A x) ⇒ (B x)) ⇒ ∀x.T:{A x} ⇒ ∃x:T.(B x)}	by λ(f.____)
f : ∃x:T.((A x) ⇒ (B x)) ⊢ {∀x.T:{A x} ⇒ ∃x:T.(B x)}	by λ(g.___)
f : ∃x:T.((A x) ⇒ (B x)), g : ∀x.T:{A x} ⊢ {∃x:T.(B x)}	by spread(f; x,h.____)
x : T, h : (A x) ⇒ (B x), g : ∀x.T:{A x} ⊢ {∃x:T.(B x)}	by apseq(g;x;ax.___)
x : T, h : (A x) ⇒ (B x), ax : {A x} ⊢ {∃x:T.(B x)}	by Open {A x} and then {∃x:T.(B x)}
x : T, h : (A x) ⇒ (B x), ax : A x ⊢ ∃x:T.(B x)	by pair(x;___)
x : T, h : (A x) ⇒ (B x), ax : A x ⊢ (B x)	by apseq(h;ax;bx.bx)

{∀x.T:{A x} ⇒ ∃x:T.(B x) ⇒ ∃x:T.((A x) ⇒ (B x))}	by λ(f.____)
f : ∀x.T:{A x} ⇒ ∃x:T.(B x) ⊢ {∃x:T.((A x) ⇒ (B x))}	by (CC{∃x:T.((A x) ⇒ (B x))};g.___) Classical contradiction
f : ∀x.T:{A x} ⇒ ∃x:T.(B x), g : ¬(∃x:T.((A x) ⇒ (B x)) ⊢ {∃x:T.((A x) ⇒ (B x))}	by apseq(f; slot1 ;h. slot2 )
g : ¬(∃x:T.((A x) ⇒ (B x)) ⊢ ∀x.T:{A x}	by λ(x.___) for slot1
g : ¬(∃x:T.((A x) ⇒ (B x)), x : T ⊢ {A x}	by (CC{A x};nax.___) Classical contradiction
g : ¬(∃x:T.((A x) ⇒ (B x)), x : T nax : ¬(A x) ⊢ {A x}	by apseq(g;___;False.any(..))
g : ¬(∃x:T.((A x) ⇒ (B x)), x : T, nax : ¬(A x) ⊢ ∃x:T.((A x) ⇒ (B x))	by pair(x;___)
g : ¬(∃x:T.((A x) ⇒ (B x)), x : T, nax : ¬(A x) ⊢ (A x) ⇒ (B x)	by λ(ax;___)
g : ¬(∃x:T.((A x) ⇒ (B x)), x : T, nax : ¬(A x), ax : (A x) ⊢ (B x)	by apseq(nax;ax;False.any(..))
h : ∃x:T.(B x), g : ¬(∃x:T.((A x) ⇒ (B x)) ⊢ {∃x:T.((A x) ⇒ (B x))}	by spread(h; x,bx.___) then unsquash goal for slot2
x : T, bx :(B x), g : ¬(∃x:T.((A x) ⇒ (B x)) ⊢ ∃x:T.((A x) ⇒ (B x))	by pair(x;___)
x : T, bx :(B x), g : ¬(∃x:T.((A x) ⇒ (B x)) ⊢ (A x) ⇒ (B x)	by λ(ax.___)
x : T, bx :(B x), g : ¬(∃x:T.((A x) ⇒ (B x)), ax : (A x) ⊢ (B x)	by bx