Database: De Morgan’s laws for existentially quantified negations and negated universal quantification

Theorem 99: De Morgan’s laws for existentially quantified negations and negated universal quantification (inference rules)

Recall the usual notation for negation, existence statements and universal statements.

(a) Given that \exists x \neg \phi holds, we may infer that \neg \forall x \phi holds: \cfrac{\vdash \exists x \neg \phi}{\vdash \neg \forall x \phi}. (b) Given that \neg \forall x \phi holds, we may infer that \exists x \neg \phi holds: \cfrac{\vdash \neg \forall x \phi}{\vdash \exists 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): Assume \forall x \phi . Using universal elimination, we infer that the variable substitution [\phi | x \to y] holds. Then, by double negation introduction, we infer that the double negation \neg \neg [\phi | x \to y] holds; by negation elimination, we therefore get that \neg [\phi | x \to y] entails \neg \exists x \neg \phi .

Using existential elimination (with the premise \exists x \neg \phi and the entailment we just found), we infer that \exists x \phi holds. Therefore, \forall x \phi entails \exists x \phi . But by weakening, since \vdash \exists x \neg \phi is a premise, we infer that \forall x \phi entails \exists x \neg \phi . We conclude, using negation introduction, that \neg \forall x \phi holds.

(b): Assume \neg \exists x \neg \phi . Using part (b) of [98], we infer \forall x \neg \neg \phi holds. Thus, by universal elimination, [\neg \neg \phi | x \to y] holds. This is the same as \neg \neg [\phi | x \to y ] , so we get by double negation elimination that [\phi | x \to y] holds. By universal introduction, it follows that \forall x \phi holds. Thus, \neg \exists x \neg \phi entails \forall x \phi .

But by weakening, \neg \exists x \neg \phi also entails \neg \forall x \phi ; we therefore infer using negation introduction that \neg \neg \neg \exists x \neg \phi holds. By double negation elimination, we conclude that \exists x \neg \phi holds. \square

This database entry builds on the following:

  1. Terminology: Class, statement
  2. Definition: Negation
  3. Definition: Occurrence of a variable
  4. Proposition/definition: Variable substitution
  5. Definition: Freely substitutable variable
  6. Lemma: A variable is freely substitutable for a variable not occurring in the statement
  7. Terminology: Inference, entailment
  8. Terminology: Inference rule
  9. Theorem: The weakening rule
  10. Inference rule: Negation introduction
  11. Proposition: Double negation introduction
  12. Inference rule: Double negation elimination
  13. Theorem: Negation elimination
  14. Theorem: Universal elimination
  15. Inference rule: Existential elimination
  16. Theorem: Universal introduction
  17. Theorem: De Morgan’s laws for universally quantified negations and negated existential quantification