//
Skip to main content
PRL Project

Constructive reading of classical logic
Table of Contents

Previous Page Next Page

Kleene 56: {(AB) ⇔ ~(~A ∧ ~B)}


∀[A,B: ℙ]. {(A ∨ B) ⇔ ¬(¬A ∧ ¬B)}
{(A ∨ B) ⇒ ¬(¬A ∧ ¬B)} ⇒ Extract: λf.λg.spread(g; na,nb.decide(f;a.ap(na.a);b.ap(nb.b))
A ∨ B ⇒ ¬(¬A ∧ ¬B)by λ(f.___)
f : A ∨ B ⊢ ¬(¬A ∧ ¬B)by λ(g.____)
f : A ∨ B, g: ¬A ∧ ¬B ⊢ Falseby spread(g; na,nb.___)
f : A ∨ B, na : ¬A, nb : ¬B ⊢ Falseby decide(f;a. slot1 ; b. slot2 )
a : A B, na : ¬A, nb : ¬B ⊢ Falseby ap(na.a) for slot1
b : B, na : ¬A, nb : ¬B ⊢ Falseby ap(nb.b) for slot2

{¬(¬A ∧ ¬B) ⇒ (A ∨ B)} ⇐ Extract: λf.(CC;g.any(ap(f.<λa.ap(g.inl(a));λb.ap(g.inr(b))>)))
{¬(¬A ∧ ¬B) ⇒ A ∨ B}by λ(f.___)
f : ¬(¬A ∧ ¬B) ⊢ {A ∨ B}by (CC{A ∨ B};g.___) Classical contradiction
f : ¬(¬A ∧ ¬B), g : ¬(A ∨ B) ⊢ {A ∨ B}by apseq(f;____;False.any(..))
g : ¬(A ∨ B) ⊢ ¬A ∧ ¬Bby pair( slot1 ; slot2 )
g : ¬(A ∨ B) ⊢ ¬Aby λ(a.___) for slot1
g : ¬(A ∨ B), a : A ⊢ Falseby ap(g.___)
a : A ⊢ A ∨ Bby inl(___)
a : A ⊢ A by a
naob : ¬(A ∨ B) ⊢ ¬Bby λ(b.___) for slot2
naob : ¬(A ∨ B), b : B ⊢ Falseby ap(g.___)
b : B ⊢ A ∨ Bby inr(___)
b : B ⊢ B by b



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 ElimClassical Unsquash goal | | | |\ | | | | ⊢ ¬((¬A) ∧ (¬B)) | | | | | 1 2 3 4 BY (D 0 THENA Auto) | | | | | | | | | 4. (¬A) ∧ (¬B) | | | | ⊢ False | | | | | 1 2 3 4 BY D 4 | | | | | | | | | 4. ¬A | | | | 5. ¬B | | | | ⊢ False | | | | | 1 2 3 4 BY D 3 | | | | |\ | | | | | 3. A | | | | | ⊢ False | | | | | | 1 2 3 4 5 BY D 4 | | | | | | | | | | | 4. ¬B | | | | | ⊢ A | | | | | | 1 2 3 4 5 BY Hypothesis | | | | \ | | | | 3. B | | | | ⊢ False | | | | | 1 2 3 4 BY D 5 | | | | | | | | | ⊢ B | | | | | 1 2 3 4 BY Hypothesis | | | \ | | | 4. x: Unit | | | ⊢ (¬A) ∧ (¬B) ∈ ℙ | | | | 1 2 3 BY Auto | | \ | | 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 D 3 | | | | | 3. ¬(A ∨ B) | | ⊢ (¬A) ∧ (¬B) | | | 1 2 BY D 0 | | |\ | | | ⊢ ¬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 | | \ | | ⊢ ¬B | | | 1 2 BY (D 0 THENA Auto) | | | | | 4. B | | ⊢ False | | | 1 2 BY D 3 | | | | | 3. 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))} | | 2 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