Constructive reading of classical logic
Table of Contents
Kleene 85: {~(∀x:T.{A x}) ⇔ ∃x:T.~(A x)}
| ∃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} ⊢ False | by spread(f; x,nax.___) |
| g : ∀x:T.{A x}, x : T, nax : ¬(A x) ⊢ False | by apseq(g;x;ax.___) |
| ax : {A x}, x : T, nax : ¬(A x) ⊢ False | by Open {A x} with False |
| ax : (A x), x : T, nax : ¬(A x) ⊢ False | by ap(nax.___) |
| ax : (A x), x : T ⊢ (A x) | by ax |
{¬(∀x:T.{A x}) ⇒ ∃x:T.¬(A x)}
⇒ Extract: λf.(CC;g.any(ap(f.λx.(CC;nax.any(ap(g;<x;nax>))))))
| {¬(∀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 seqap(f;___;False.any(..)) |
| g : ¬(∃x:T.¬(A x)) ⊢ ∀x:T.{A x} | by λ(x.___) |
| g : ¬(∃x:T.¬(A x)), x : T ⊢ {A x} | by (CC{A x};nax.___) Classical contradiction |
| g : ¬(∃x:T.¬(A x)), x : T, nax : ¬(A x) ⊢ {A x} | by seqap(g;___;False;any(..)) |
| x : T, nax : ¬(A x) ⊢ ∃x:T.¬(A x) | by pair(x;___) |
| x : T, nax : ¬(A x) ⊢ ¬(A x) | by nax |
Nuprl Proof
⊢ ∀[T:Type]. ∀[A:T → ℙ]. {¬(∀x:T.{A x}) ⇔ ∃x:T.(¬(A x))}
|
BY (D 0 THENA Auto)
|\
| 1. T: Type
| ⊢ ∀[A:T → P]. {¬(∀x:T. {A x}) ⇔ ∃x:T. (¬(A x))}
| |
1 BY (D 0 THENA Auto)
| |\
| | 2. A: T → P
| | ⊢ {¬(∀x:T. {A x}) ⇔ ∃x:T. (¬(A x))}
| | |
1 2 BY RepeatFor 4 ((D 0 THENA Auto))
| | |\
| | | 3. ¬(∀x:T. {A x})
| | | ⊢ {∃x:T. (¬(A x))}
| | | |
1 2 3 BY (ClassicalContradiction THENA Auto)
| | | |
| | | 4. ¬(∃x:T. (¬(A x)))
| | | ⊢ {∃x:T. (¬(A x))}
| | | |
1 2 3 BY D 3
| | | |
| | | 3. ¬(∃x:T. (¬(A x)))
| | | ⊢ ∀x:T. {A x}
| | | |
1 2 3 BY (D 0 THENA Auto)
| | | |
| | | 4. x: T
| | | ⊢ {A x}
| | | |
1 2 3 BY (ClassicalContradiction· THENA Auto)
| | | |
| | | 5. ¬(A x)
| | | ⊢ {A x}
| | | |
1 2 3 BY D 3
| | | |
| | | 3. x: T
| | | 4. ¬(A x)
| | | ⊢ ∃x:T. (¬(A x))
| | | |
1 2 3 BY (InstConcl [dxe]· THENA Auto)
| | | |
| | | ⊢ ¬(A x)
| | | |
1 2 3 BY Hypothesis
| | \
| | 3. ∃x:T. (¬(A x))
| | ⊢ {¬(∀x:T. {A x})}
| | |
1 2 BY (ElimClassical THENA Auto)
| | |
| | ⊢ ¬(∀x:T. {A x})
| | |
1 2 BY (D 0 THENA Auto)
| | |
| | 4. ∀x:T. {A x}
| | ⊢ False
| | |
1 2 BY D 3
| | |
| | 3. x: T
| | 4. ¬(A x)
| | 5. ∀x:T. {A x}
| | ⊢ False
| | |
1 2 BY (InstHyp [dxe] 5· THENA Auto)
| | |
| | 6. {A x}
| | ⊢ False
| | |
1 2 BY D 6
| | |
| | 6. x@0: Unit
| | 7. A x
| | ⊢ False
| | |
1 2 BY D 4
| | |
| | 4. ∀x:T. {A x}
| | 5. x@0: Unit
| | 6. A x
| | ⊢ A x
| | |
1 2 BY Hypothesis
| \
| 2. A: T → P
| 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 → P
3. {x:Unit| ¬(∀x:T. {A x}) ⇔ ∃x:T. (¬(A x))}
⊢ Ax ∈ {x:Unit| ¬(∀x:T. {A x}) ⇔ ∃x:T. (¬(A x))}
|
BY Auto
Proof
Table of Contents