Constructive reading of classical logic
Table of Contents
Kleene 83: {∃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,ax.___) |
| x : T, ax : (A x), g : ∀x:T.¬(A x)⊢ False | by apseq(g;x;nax.___) |
| x : T, ax : (A x), nax : ¬(A x)⊢ False | by ap(nax.__) |
| x : T, ax : (A x) ⊢ (A x) | by ax |
{¬(∀x:T.¬(A x)) ⇒ ∃x.T:(A x)}
⇐ Extract: λf.(CC;g.any(ap(f.λx.λax.ap(g.<x;ax>))))
| {¬(∀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 apseq(f;___;False.any(..)) |
| g : ¬(∃x.T:(A x)) ⊢ ∀x:T.¬(A x) | by λ(x.___) |
| g : ¬(∃x.T:(A x)), x : T ⊢ ¬(A x) | by λ(ax.___) |
| g : ¬(∃x.T:(A x)), x : T, ax : (A x) ⊢ False | by ap(g.___) |
| x : T, ax : (A x) ⊢ ∃x.T:(A x) | by pair(x;___) |
| x : T, ax : (A x) ⊢ (A x) | by ax |
Nuprl Proof
⊢ ∀[T:Type]. ∀[A:T → ℙ]. {∃x:T.(A x) ⇔ ¬(forall;x:T.¬(A x))}
|
BY (D 0 THENA Auto)
|\
| 1. T: Type
| ⊢ ∀[A:T → ℙ]. {∃x:T. (A x) ⇔ ¬(∀x:T. (¬(A x)))}
| |
1 BY (D 0 THENA Auto)
| |\
| | 2. A: T → ℙ
| | ⊢ {∃x:T. (A x) ⇔ ¬(∀x:T. (¬(A x)))}
| | |
1 2 BY (D 0 THENA Auto)
| | |
| | ⊢ {(∃x:T. (A x)) ⇒ (¬(∀x:T. (¬(A x))))} ∧ {(∃x:T. (A x)) ⇐ ¬(∀x:T. (¬(A x)))}
| | |
1 2 BY (RepeatFor 2 (D 0) THENA Auto)
| | |\
| | | ⊢ (∃x:T. (A x)) ⇒ {¬(∀x:T. (¬(A x)))}
| | | |
1 2 3 BY (D 0 THENA Auto)
| | | |
| | | 3. ∃x:T. (A x)
| | | ⊢ {¬(∀x:T. (¬(A x)))}
| | | |
1 2 3 BY (ElimClassical THENA Auto) Unsquash goal
| | | |
| | | ⊢ ¬(∀x:T. (¬(A x)))
| | | |
1 2 3 BY (D 0 THENA Auto)
| | | |
| | | 4. ∀x:T. (¬(A x))
| | | ⊢ False
| | | |
1 2 3 BY D 3
| | | |
| | | 3. x: T
| | | 4. A x
| | | 5. ∀x:T. (¬(A x))
| | | ⊢ False
| | | |
1 2 3 BY (InstHyp [⌈x⌉] THENA Auto)
| | | |
| | | 6. ¬(A x)
| | | ⊢ False
| | | |
1 2 3 BY D 6
| | | |
| | | ⊢ A x
| | | |
1 2 3 BY Hypothesis
| | \
| | ⊢ (¬(∀x:T. (¬(A x)))) ⇒ {∃x:T. (A x)}
| | |
1 2 BY (D 0 THENA Auto)
| | |
| | 3. ¬(∀x:T. (¬(A x)))
| | ⊢ {∃x:T. (A x)}
| | |
1 2 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses
| | |
| | 4. ¬(∃x:T. (A x))
| | ⊢ {∃x:T. (A x)}
| | |
1 2 BY D 3
| | |
| | 3. ¬(∃x:T. (A x))
| | ⊢ ∀x:T. (¬(A x))
| | |
1 2 BY (D 0 THENA Auto)
| | |
| | 4. x: T
| | ⊢ ¬(A x)
| | |
1 2 BY (D 0 THENA Auto)
| | |
| | 5. A x
| | ⊢ False
| | |
1 2 BY D 3
| | |
| | 3. x: T
| | 4. A x
| | ⊢ ∃x:T. (A x)
| | |
1 2 BY (InstConcl [⌈x⌉] THENA Auto)
| | |
| | ⊢ A x
| | |
1 2 BY Hypothesis
| \
| 2. A: T → ℙ
| 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 → ℙ
3. {x:Unit| ∃x:T. (A x) ⇔ ¬(∀x:T. (¬(A x)))}
⊢ Ax ∈ {x:Unit| ∃x:T. (A x) ⇔ ¬(∀x:T. (¬(A x)))}
|
BY Auto
PDF version of proof
Table of Contents