Database: De Morgan’s laws for disjuncted negations and negated conjunctions

Theorem 83: De Morgan’s laws for disjuncted negations and negated conjunctions (inference rules)

Recall the usual notation for negation, conjunction and disjunction.

(a) Given that \neg \phi \vee \neg \psi holds, we may infer that \neg (\phi \wedge \psi) holds: \cfrac{\vdash (\neg \phi \vee \neg \psi)}{\vdash \neg (\phi \wedge \psi)}. (b) Given that \neg (\phi \wedge \psi) holds, we may infer that \neg \phi \vee \neg \psi holds: \cfrac{\vdash \neg (\phi \wedge \psi)}{\vdash (\neg \phi \vee \neg \psi)}.

Verification: (a): By conjunction elimination, we infer from the assumption \phi \wedge \psi that \phi holds and \psi holds; hence, \phi \wedge \psi entails \phi and also entails \psi .

Assume \neg \phi . By weakening, we infer \phi \wedge \psi entails \neg \phi . But then, by negation introduction, we infer (still under the assumption \neg \phi ) that \neg (\phi \wedge \psi) holds. This has showed \neg \phi entails \neg (\phi \wedge \psi) .

We show in the same way that \neg \psi entails \neg (\phi \wedge \psi) . But our original premise was \neg \phi \vee \neg \psi ; with the entailments we have obtained, we therefore infer by disjunction elimination that \neg (\phi \wedge \psi) holds.

(b): Using weakening, we infer that \neg (\neg \phi \vee \neg \psi) entails \neg (\phi \wedge \psi) . Assume now \neg (\neg \phi \vee \neg \psi) . By weakening, we infer \neg \phi entails \neg (\neg \phi \vee \neg \psi) .

Assume now additionally \neg \phi . By disjunction introduction, \neg \phi \vee \neg \psi holds. By negation introduction we infer, still keeping the assumption \neg (\neg \phi \vee \neg \psi) , that \neg \neg \phi holds. A very similar argument shows that \neg \neg \psi also holds under the same assumption. Using double negation elimination twice, we get that \phi and \psi hold under the assumption \neg (\neg \phi \vee \neg \psi) .

Next, using conjunction introduction, \neg (\neg \phi \vee \neg \psi) entails \phi \wedge \psi . As we also found \neg (\neg \phi \vee \neg \psi) entails \neg (\phi \wedge \psi) , we infer using negation introduction (with no assumptions left) that \neg \neg (\neg \phi \vee \neg \psi) holds. Finally, using double negation elimination, we infer that \neg \phi \vee \neg \psi holds. \square

This database entry builds on the following:

  1. Definition: Conjunction
  2. Definition: Negation
  3. Definition: Disjunction
  4. Terminology: Inference, entailment
  5. Terminology: Inference rule
  6. Inference rule: Conjunction introduction
  7. Inference rule: Conjunction elimination
  8. Theorem: The weakening rule
  9. Inference rule: Negation introduction
  10. Theorem: Disjunction introduction
  11. Inference rule: Double negation elimination
  12. Theorem: Disjunction elimination