## Kleene 57: {(*A* ∧ *B*) ⇔ ~(~*A* ∨ ~*B*)}

This theorem is interesting because we have to use classical contradiction twice in order to prove the non constructive direction. At the squashed goal {A ∧ B}, we have the hypothesis ¬(¬A ∨ ¬B), which by DeMorgan's law, is equivalent to (A ∧ B). However we couldn't prove our goal without the classical contradicion because we lack the necessary evidence; we omit the details here and leave it as an exercise for the reader. We must therefore use the new rule to prove this. We first separate the ∧ and are left with two goals, ⊢{A} and ⊢{B}. We will only consider the {A} case here, as the {B} case proceeds similarly -- see the full proof below. We can use classical contradiction to get evidence for ¬A. Then we use the application rule on ¬(¬A ∨ ¬ B), taking advantage of *ex falso quodlibit*. We choose the left disjunctive because we know we have evidence for ¬A. The {B} case proceeds exactly the same except we would choose the right disjunctive since our evidence is ¬B.

If we had done classical contradiction on (A ∧ B) without splitting the pair, then we would have come to an impass in the proof where we would be missing evidence for either A or B. This is the only proof of Kleene's that is not doubly squashed that requires two instances of classical contradiction.

**∀[A,B: ℙ]. {(A ∧ B) ⇔ ¬(¬A ∨ ¬B)}**

A ∧ B ⇒ ¬(¬A ∨ ¬B) | by λ(f.___) |

f : A ∧ B ⊢ ¬(¬A ∨ ¬B) | by λ(g.___) |

f : A ∧ B, g : ¬A ∨ ¬ B ⊢ False | by spread(f; a,b.___) |

a : A, b : B, g : ¬A ∨ ¬ B ⊢ False | by decide(g; na. slot1 ; nb. slot2 ) |

a : A, b : B, na: ¬A ⊢ False | by ap(na.a) for slot1 |

a : A, b : B, nb : ¬ B ⊢ False | by ap(nb.b) for slot2 |

{¬(¬A ∨ ¬B) ⇒ (A ∧ B)} | by λ(f.___) |

f : ¬(¬A ∨ ¬B) ⊢ {A ∧ B} | by pair( slot1 ; slot2 ) |

f : ¬(¬A ∨ ¬B) ⊢ {A} | by (CC{A};na.___) Classical contradiction, for slot1 |

f : ¬(¬A ∨ ¬B), na : ¬A ⊢ {A} | by ap(f.___) |

na : ¬A ⊢ ¬A ∨ ¬B | by inl(___) |

na : ¬A ⊢ ¬A | by na |

f : ¬(¬A ∨ ¬B) ⊢ {B} | by (CC{B};nb.___) Classical contradiction, for slot2 |

f : ¬(¬A ∨ ¬B), nb : ¬B ⊢ {B} | by ap(f.___) |

nb : ¬B ⊢ ¬A ∨ ¬B | by inr(___) |

nb: ¬B ⊢ ¬B | by nb |

### Nuprl Proof

Table of Contents