Constructive reading of classical logic
Table of Contents
Kleene 92: {(A ∨ ∀x:T.(B x)) ⇔ ∀x:T. (A ∨ (B 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
Table of Contents