Theorem 90: De Morgan’s laws for conjuncted negations and negated disjunctions (inference rules)

Recall the usual notation for negation, conjunction and disjunction.

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

Proof: (a): Using conjunction elimination twice, we infer that \neg \phi holds and \neg \psi holds. Using negation elimination twice, we infer \phi entails \neg (\phi \vee \psi) and that \psi entails \neg (\phi \vee \psi) .

Assume \phi \vee \psi . By disjunction elimination, using the above entailments, we infer that \neg (\phi \vee \psi) holds. But then we have proved \phi \vee \psi entails \neg (\phi \vee \psi) . With no assumptions left, we conclude by [66] that \neg (\phi \vee \psi) holds.

(b): By weakening, \phi entails \neg (\phi \vee \psi) and \psi entails \neg (\phi \vee \psi) . Assume \phi . By disjunction introduction, \phi \vee \psi holds. Thus, we have showed \phi entails \phi \vee \psi . But then, by negation introduction, \neg \phi holds.

We show in the same way, assuming \psi , that \psi entails \phi \vee \psi , hence \neg \psi holds. But then, by conjunction introduction, \neg \phi \wedge \neg \psi holds. \square