## Kleene 56: {(A ∨ B) ⇔ ~(~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 ⊢ False by spread(g; na,nb.___) f : A ∨ B, na : ¬A, nb : ¬B ⊢ False by decide(f;a. slot1 ; b. slot2 ) a : A B, na : ¬A, nb : ¬B ⊢ False by ap(na.a) for slot1 b : B, na : ¬A, nb : ¬B ⊢ False by 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 ∧ ¬B by pair( slot1 ; slot2 ) g : ¬(A ∨ B) ⊢ ¬A by λ(a.___) for slot1 g : ¬(A ∨ B), a : A ⊢ False by ap(g.___) a : A ⊢ A ∨ B by inl(___) a : A ⊢ A by a naob : ¬(A ∨ B) ⊢ ¬B by λ(b.___) for slot2 naob : ¬(A ∨ B), b : B ⊢ False by ap(g.___) b : B ⊢ A ∨ B by 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