Kleene 98

PRL Home Introduction Math Library Publications Projects System

Seminar People The Book Lectures Other Groups

Constructive reading of classical logic

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

The extract of the forward direction shows the constructive part of the proof. We can deconstruct the proof to yield {B} as our goal. We will need to keep this squashed until we are able to open the inner squashed term. We can then further decompose the hypotheses so we're left with x: T, f : (A x)⇒B, and {A x}. We then open the squashed hypothesis and apply f to get evidence for B.

The backwards direction can not be proved constructively. We must use classical contradiction in two instances for this proof. The first instance we must use classical contradiction is at the goal {∃x:T.((A x) ⇒ B)}. We need to use classical contradiction here because we need to later apply that instantiated term. However right after we use the classical contradiction, we apply f : ∀x:T.{A x} ⇒ B, which will give use two subgoals, prove the assertion then the implication. To solve the assertion we need to use another classical contradiction on the inner squashed term. Then we can apply our first classical contradiction instantiated term. We ultimately prove this subgoal but applying ¬(A x) to (A x) and by ex falso quodlibet we can prove any goal. The second subgoal falls out without having to use the classical contradiction term. Kleene theorem 99 is similar to this.

∀[T:Type]. (T ⇒ (∀[A:T → ℙ]. ∀[B: ℙ]. {∃x:T.((A x) ⇒ B) ⇔ (∀x:T. {A x}) ⇒ B} {∃x:T.((A x) ⇒ B) ⇒ ∀x:T.{A x} ⇒ B} ⇒ Extract: λf.λg.spread(f; x,h.ap(h.ap(g.x)))

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

{∀x:T.{A x} ⇒ B ⇒ ∃x:T.((A x) ⇒ B)}
⇐ Extract: λf.(CC;h.<x;λax.ap(f.λx.(CC;na.any(ap(h.<x;λax.any(ap(nax.ax))>))))>).
  
(T ⇒ (∀[A:T → ℙ]. ∀[B: ℙ]. {∀x:T.{A x} ⇒ B ⇒ ∃x:T.((A x) ⇒ B)}
t : T ⊢ {∀x:T.{A x} ⇒ B ⇒ ∃x:T.((A x) ⇒ B)}by λ(f.___)
t : T, f : ∀x:T.{A x} ⇒ B ⊢ {∃x:T.((A x) ⇒ B)}by (CC{∃x:T.((A x) ⇒ B);h.____)    Classical contradiction 
t : T, f : ∀x:T.{A x} ⇒ B, h : ¬(∃x:T.((A x) ⇒ B) ⊢ {∃x:T.((A x) ⇒ B)}by apseq(f;  slot1  ;b.  slot2  )
t : T, h : ¬(∃x:T.((A x) ⇒ B) ⊢ ∀x:T.{A x}by λ(x.___)  for slot1
t : T, h : ¬(∃x:T.((A x) ⇒ B) ⊢ {A x}by (CC{A};na.___)   Classical contradiction 
t : T, h : ¬(∃x:T.((A x) ⇒ B), na : ¬A ⊢ {A x}by apseq(h;___;False.any(..))
t : T, nax : ¬(A x) ⊢ ∃x:T.((A x) ⇒ Bby pair(x;___)
t : T, nax : ¬(A x) ⊢ (A x) ⇒ Bby λ(ax.___)
t : T, nax : ¬(A x), ax : (A x) ⊢ Bby apseq(nax;ax;False.any(..))
t : T, b : B, h : ¬(∃x:T.((A x) ⇒ B) ⊢ {∃x:T.((A x) ⇒ B)}by Rename 't' to 'x' then unsquash goal  for slot2
x : T, b : B, h : ¬(∃x:T.((A x) ⇒ B) ⊢ ∃x:T.((A x) ⇒ B)by pair(x;___)
x : T, b : B, h : ¬(∃x:T.((A x) ⇒ B) ⊢ (A x) ⇒ Bby λ(ax.___)
x : T, b : B, h : ¬(∃x:T.((A x) ⇒ B), ax : (A x) ⊢ Bby b

Nuprl Proof

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

Table of Contents

(T ⇒ (∀[A:T → ℙ]. ∀[B: ℙ]. {∀x:T.{A x} ⇒ B ⇒ ∃x:T.((A x) ⇒ B)}
t : T ⊢ {∀x:T.{A x} ⇒ B ⇒ ∃x:T.((A x) ⇒ B)}	by λ(f.___)
t : T, f : ∀x:T.{A x} ⇒ B ⊢ {∃x:T.((A x) ⇒ B)}	by (CC{∃x:T.((A x) ⇒ B);h.____) Classical contradiction
t : T, f : ∀x:T.{A x} ⇒ B, h : ¬(∃x:T.((A x) ⇒ B) ⊢ {∃x:T.((A x) ⇒ B)}	by apseq(f; slot1 ;b. slot2 )
t : T, h : ¬(∃x:T.((A x) ⇒ B) ⊢ ∀x:T.{A x}	by λ(x.___) for slot1
t : T, h : ¬(∃x:T.((A x) ⇒ B) ⊢ {A x}	by (CC{A};na.___) Classical contradiction
t : T, h : ¬(∃x:T.((A x) ⇒ B), na : ¬A ⊢ {A x}	by apseq(h;___;False.any(..))
t : T, nax : ¬(A x) ⊢ ∃x:T.((A x) ⇒ B	by pair(x;___)
t : T, nax : ¬(A x) ⊢ (A x) ⇒ B	by λ(ax.___)
t : T, nax : ¬(A x), ax : (A x) ⊢ B	by apseq(nax;ax;False.any(..))
t : T, b : B, h : ¬(∃x:T.((A x) ⇒ B) ⊢ {∃x:T.((A x) ⇒ B)}	by Rename 't' to 'x' then unsquash goal for slot2
x : T, b : B, h : ¬(∃x:T.((A x) ⇒ B) ⊢ ∃x:T.((A x) ⇒ B)	by pair(x;___)
x : T, b : B, h : ¬(∃x:T.((A x) ⇒ B) ⊢ (A x) ⇒ B	by λ(ax.___)
x : T, b : B, h : ¬(∃x:T.((A x) ⇒ B), ax : (A x) ⊢ B	by b