Theorem 98: De Morgan’s laws for universally quantified negations and negated existential quantification (inference rules)

We use notation for negation, existence statements and universal statements.

(a) Given that \forall x \neg \phi holds, we may infer that \neg \exists x \phi holds: \cfrac{\vdash \forall x \neg \phi}{\vdash \neg \exists x \phi}. (b) Given that \neg \exists x \phi holds, we may infer that \forall x \neg \phi holds: \cfrac{\vdash \neg \exists x \phi}{\vdash \forall x \neg \phi}.

Proof: In the below, let y be some variable which does not occur in \phi , and note that by [27], it follows that x is freely substitutable for y in \phi .

(a): By universal elimination, the variable substitution [\neg \phi | x \to y] holds. This is by definition the same as \neg [\phi | x \to y] . By negation elimination, we infer that [\phi | x \to y] entails \neg \exists x \phi .

Assume \exists x \phi . By existential elimination, we then infer (using this assumption and the entailment we found above as premises) that \neg \exists x \phi holds. Thus \exists x \phi entails its negation; we infer by [57] that \neg \exists x \phi holds.

(b): By weakening, we infer [\phi | x \to y] entails \neg \exists x \phi . Assume [\phi | x \to y] . We infer by existential introduction that \exists x \phi holds. Thus, [\phi | x \to y] entails \exists x \phi . Thus, by negation introduction, we infer that \neg [\phi | x \to y] holds. This is the same statement as [\neg \phi | x \to y] . By universal introduction, \forall x \neg \phi holds. \square