Constructive reading of classical logic
Table of Contents
Kleene 49: {~~A ⇔ A}
| A ⇒ ¬¬A | by λ(a.___) |
| a : A ⊢ ¬¬A | by λ(na.___) |
| a : A, na : A ⊢ False | by ap(na.___) |
| a : A ⊢ A | by a |
{¬¬A ⇒ A}
⇒ Extract: λnna.(CC;na.any(ap(nna.na)))
| {¬¬A ⇒ A} | by λ(nna.___) |
| nna : ¬¬A ⊢ {A} | by (CC{A};na.___) Classical contradiction |
| nna : ¬¬A, na : ¬A ⊢ {A} | by apseq(nna;___;False.any(..)) |
| na : ¬A ⊢ ¬A | by na |
Nuprl Proof
⊢ ∀[A:ℙ]. {¬¬A ⇔ A}
|
BY (D 0 THENA Auto)
|\
| 1. A: ℙ
| ⊢ {¬¬A ⇐⇒ A}
| |
1 BY RepeatFor 4 ((D 0 THENA Auto))
| |\
| | 2. ¬¬A
| | ⊢ {A}
| | |
1 2 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses
| | |
| | 3. ¬A
| | ⊢ {A}
| | |
1 2 BY D 2
| | |
| | 2. ¬A
| | ⊢ ¬A
| | |
1 2 BY Hypothesis
| \
| 2. A
| ⊢ {¬¬A}
| |
1 BY (ElimClassical THENA Auto) Unsquash goal
| |
| ⊢ ¬¬A
| |
1 BY (D 0 THENA Auto)
| |
| 3. ¬A
| ⊢ False
| |
1 BY D 3
| |
| ⊢ A
| |
1 BY Hypothesis
\
1. A: ℙ
2. {x:Unit| ¬¬A ⇔ A}
⊢ Ax ∈ {x:Unit| ¬¬A ⇔ A}
|
BY Auto
PDF version of proof
Table of Contents