//
Skip to main content
PRL Project

Constructive reading of classical logic
Table of Contents

Previous Page Next Page

Kleene 61: {(AB) ⇔ (~AB)}


∀[A,B: ℙ]. {(A ∨ B) ⇔ (¬A ⇒ B)}
{(A ∨ B) ⇒ (¬A ⇒ B)} ⇒ Extract: λf.λna.decide(f; a.any(na(a)); b.b)
A ∨ B ⇒ (¬A ⇒ B)by λ(f.___)
aob : A ∨ B ⊢ ¬A ⇒ Bby λ(na.___)
aob : A ∨ B, na : ¬A ⊢ Bby decide(f; a. slot1 ; b. slot2 )
a : A, na : ¬A ⊢ Bby apseq(na.__;False.any(..)) for slot1
a : A ⊢ Aby a
b : B, na : ¬A ⊢ Bby b for slot2
{(¬A ⇒ B) ⇒ (A ∨ B)} ⇐ Extract: λf.(CC;g.inr(ap(f.λa.ap(f.λa.ap(g.inl(a))))))
(¬A ⇒ B) ⇒ A ∨ Bby λ(f.___)
f : ¬A ⇒ B ⊢ A ∨ Bby (CC{A ∨ B};g.___) Classical contradiction
f : ¬A ⇒ B, g : ¬(A ∨ B) ⊢ A ∨ Bby inr(___)
f : ¬A ⇒ B, g : ¬(A ∨ B) ⊢ Bby apseq(f;___;b.b)
g : ¬(A ∨ B) ⊢ ¬Aby λ(a.___)
g : ¬(A ∨ B), a : A ⊢ Falseby ap(g.___)
a : A ⊢ A ∨ Bby inl(a)


Nuprl Proof


⊢ ∀[A,B:ℙ]. {(A ∨ B) ⇔ (¬A ⇒ B)} | BY (D 0 THENA Auto) |\ | 1. A: ℙ | ⊢ ∀[B:ℙ]. {(A ∨ B) ⇔ (¬A ⇒ B)} | | 1 BY (D 0 THENA Auto) | |\ | | 2. B: ℙ | | ⊢ {A ∨ B ⇔ (¬A) ⇒ B} | | | 1 2 BY RepeatFor 4 ((D 0 THENA Auto)) | | |\ | | | 3. A ∨ B | | | ⊢ {(¬A) ⇒ B} | | | | 1 2 3 BY RepeatFor 2 ((D 0 THENA Auto)) | | | | | | | 4. ¬A | | | ⊢ {B} | | | | 1 2 3 BY D 3 | | | |\ | | | | 3. A | | | | ⊢ {B} | | | | | 1 2 3 4 BY D 4 | | | | | | | | | ⊢ A | | | | | 1 2 3 4 BY Hypothesis | | | \ | | | 3. B | | | ⊢ {B} | | | | 1 2 3 BY ElimClassical Unsquash goal | | | | | | | ⊢ B | | | | 1 2 3 BY Hypothesis | | \ | | 3. (¬A) ⇒ B | | ⊢ {A ∨ B} | | | 1 2 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses | | | | | 4. ¬(A ∨ B) | | ⊢ {A ∨ B} | | | 1 2 BY (ElimClassical THENA Auto) Unsquash goal | | | | | ⊢ A ∨ B | | | 1 2 BY D 3 | | |\ | | | 3. ¬(A ∨ B) | | | ⊢ ¬A | | | | 1 2 3 BY (D 0 THENA Auto) | | | | | | | 4. A | | | ⊢ False | | | | 1 2 3 BY D 3 | | | | | | | 3. A | | | ⊢ A ∨ B | | | | 1 2 3 BY (OrLeft THENA Auto) | | | | | | | ⊢ A | | | | 1 2 3 BY Hypothesis | | \ | | 3. ¬(A ∨ B) | | 4. B | | ⊢ A ∨ B | | | 1 2 BY (OrRight THENA Auto) | | | | | ⊢ B | | | 1 2 BY Hypothesis | \ | 2. B: ℙ | 3. {x:Unit| A ∨ B ⇔ (¬A) ⇒ B} | ⊢ Ax ∈ {x:Unit| A ∨ B ⇔ (¬A) ⇒ B} | | 1 BY Auto \ 1. A: ℙ 2. B: ℙ 3. {x:Unit| A ∨ B ⇔ (¬A) ⇒ B} ⊢ Ax ∈ {x:Unit| A ∨ B ⇔ (¬A) ⇒ B} | BY Auto PDF version of proof

Previous Page Next Page


Table of Contents