Skip to main content
PRL Project

Constructive reading of classical logic
Table of Contents

Previous Page Next Page

Kleene 49: {~~AA}


∀[A: ℙ]. {¬¬A ⇔ A}
{A ⇒ ¬¬A} ⇐ Extract: λa.λna.ap(na.a)
A ⇒ ¬¬Aby λ(a.___)
a : A ⊢ ¬¬Aby λ(na.___)
a : A, na : A ⊢ Falseby ap(na.___)
a : A ⊢ Aby 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 ⊢ ¬Aby 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

Previous Page Next Page


Table of Contents