//
Skip to main content
PRL Project

Constructive reading of classical logic
Table of Contents

Previous Page Next Page

Kleene 92: {(A ∨ ∀x:T.(B x)) ⇔ ∀x:T. (A ∨ (B x))}



∀[T:Type]. ∀[B: T → ℙ]. ∀[A:ℙ]. {A ∨ ∀x:T.(B x) ⇔ ∀x:T.(A ∨ (B x))}
{A ∨ ∀x:T.(B x) ⇒ ∀x:T.(A ∨ (B x))} ⇒ Extract: λf.λx.decide(a.inl(a);g.inl(ap(g.x)))
A ∨ ∀x:T.(B x) ⇒ ∀x:T.(A ∨ (B x))by λ(f.___)
f : A ∨ ∀x:T.(B x) ⊢ ∀x:T.(A ∨ (B x))by λ(x.___)
f : A ∨ ∀x:T.(B x), x : T ⊢ A ∨ (B x)by decide(f;a. slot1 ;g. slot2 )
a : A, x : T ⊢ A ∨ (B x)by inl(a) for slot1
g : ∀x:T.(B x), x : T ⊢ A ∨ (B x)by inr(___) for slot2
g : ∀x:T.(B x), x : T ⊢ (B x)by apseq(g;x;bx.bx)

{∀x:T.(A ∨ (B x)) ⇒ A ∨ ∀x:T.(B x)} ⇐ Extract: λf.(CC;g.inr(λx.decide(ap(f.x);a.any(ap(g.inl(a)));bx.bx)))
{∀x:T.(A ∨ (B x)) ⇒ A ∨ ∀x:T.(B x)}by λ(f.___)
f : ∀x:T.(A ∨ (B x)) ⊢ {A ∨ ∀x:T.(B x)}by (CC{A ∨ ∀x:T.(B x)};g.___) Classical contradiction
f : ∀x:T.(A ∨ (B x)), g : ¬(A ∨ ∀x:T.(B x) ⊢ {A ∨ ∀x:T.(B x)}by inr(___)
f : ∀x:T.(A ∨ (B x)), g : ¬(A ∨ ∀x:T.(B x)) ⊢ {∀x:T.(B x)}by λ(x.___)
f : ∀x:T.(A ∨ (B x)), g : ¬(A ∨ ∀x:T.(B x)), x : T ⊢ {B x}by seqap(f;x;h.___)
aobx : A ∨ (B x), g : ¬(A ∨ ∀x:T.(B x)), x : T ⊢ {B x}by decide(h;a. slot1 ;bx. slot2 )
a: A, g : ¬(A ∨ ∀x:T.(B x)), x : T ⊢ {B x}by apseq(g;___;False.any(..)) for slot1
a: A, x : T ⊢ A ∨ ∀x:T.(B x)by inl(a)
bx: (B x), g : ¬(A ∨ ∀x:T.(B x)), x : T ⊢ {B x}by bx for slot2

Nuprl Proof


⊢ ∀[T:Type]. ∀[B:T → ℙ]. ∀[A:ℙ]. {A ∨ ∀x:T.(B x) ⇔ ∀x:T.(A ∨ (B x))} | BY (D 0 THENA Auto) |\ | 1. T: Type | ⊢ ∀[A:P]. ∀[B:T → P]. {A ∨ (∀x:T. (B x)) ⇔ ∀x:T. (A ∨ (B x))} | | 1 BY (D 0 THENA Auto) | |\ | | 2. A: P | | ⊢ ∀[B:T → P]. {A ∨ (∀x:T. (B x)) ⇔ ∀x:T. (A ∨ (B x))} | | | 1 2 BY (D 0 THENA Auto) | | |\ | | | 3. B: T → P | | | ⊢ {A ∨ (∀x:T. (B x)) ⇔ ∀x:T. (A ∨ (B x))} | | | | 1 2 3 BY RepeatFor 4 ((D 0 THENA Auto)) | | | |\ | | | | 4. A ∨ (∀x:T. (B x)) | | | | ⊢ {∀x:T. (A ∨ (B x))} | | | | | 1 2 3 4 BY (ElimClassical THENA Auto) Unsquash goal | | | | | | | | | ⊢ ∀x:T. (A ∨ (B x)) | | | | | 1 2 3 4 BY (D 0 THENA Auto) | | | | | | | | | 5. x: T | | | | ⊢ A ∨ (B x) | | | | | 1 2 3 4 BY D 4 | | | | |\ | | | | | 4. A | | | | | ⊢ A ∨ (B x) | | | | | | 1 2 3 4 5 BY (OrLeft THENA Auto) | | | | | | | | | | | ⊢ A | | | | | | 1 2 3 4 5 BY Hypothesis | | | | \ | | | | 4. ∀x:T. (B x) | | | | ⊢ A ∨ (B x) | | | | | 1 2 3 4 BY (OrRight THENA Auto) | | | | | | | | | ⊢ B x | | | | | 1 2 3 4 BY (InstHyp [⌈x⌉] 4· THENA Auto) | | | | | | | | | 6. B x | | | | ⊢ B x | | | | | 1 2 3 4 BY Hypothesis | | | \ | | | 4. ∀x:T. (A ∨ (B x)) | | | ⊢ {A ∨ (∀x:T. (B x))} | | | | 1 2 3 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses | | | | | | | 5. ¬(A ∨ (∀x:T. (B x))) | | | ⊢ {A ∨ (∀x:T. (B x))} | | | | 1 2 3 BY (ElimClassical THENA Auto) Unsquash goal | | | | | | | ⊢ A ∨ (∀x:T. (B x)) | | | | 1 2 3 BY (OrRight THENA Auto) | | | | | | | ⊢ ∀x:T. (B x) | | | | 1 2 3 BY (D 0 THENA Auto) | | | | | | | 6. x: T | | | ⊢ B x | | | | 1 2 3 BY (InstHyp [⌈x⌉] 4· THENA Auto) | | | | | | | 7. A ∨ (B x) | | | ⊢ B x | | | | 1 2 3 BY D 7 | | | |\ | | | | 7. A | | | | ⊢ B x | | | | | 1 2 3 4 BY D 5 | | | | | | | | | 5. x: T | | | | 6. A | | | | ⊢ A ∨ (∀x:T. (B x)) | | | | | 1 2 3 4 BY (OrLeft THENA Auto) | | | | | | | | | ⊢ A | | | | | 1 2 3 4 BY Hypothesis | | | \ | | | 7. B x | | | ⊢ B x | | | | 1 2 3 BY Hypothesis | | \ | | 3. B: T → P | | 4. {x:Unit| A ∨ (∀x:T. (B x)) ⇔ ∀x:T. (A ∨ (B x))} | | ⊢ Ax ∈ {x:Unit| A ∨ (∀x:T. (B x)) ⇔ ∀x:T. (A ∨ (B x))} | | | 1 2 BY Auto | \ | 2. A: P | 3. B: T → P | 4. {x:Unit| A ∨ (∀x:T. (B x)) ⇔ ∀x:T. (A ∨ (B x))} | ⊢ Ax ∈ {x:Unit| A ∨ (∀x:T. (B x)) ⇔ ∀x:T. (A ∨ (B x))} | | 1 BY Auto \ 1. T: Type 2. A: P 3. B: T → P 4. {x:Unit| A ∨ (∀x:T. (B x)) ⇔ ∀x:T. (A ∨ (B x))} ⊢ Ax ∈ {x:Unit| A ∨ (∀x:T. (B x)) ⇔ ∀x:T. (A ∨ (B x))} | BY Auto PDF version of proof

Previous Page Next Page


Table of Contents