In quantifier logic, one quantified statement can be substituted for another that is logically equivalent to the original. A universally quantified statement is equivalent to an existentially quantified statement (and vice versa), provided the relevant negations are added or removed:
∀x P(x) :: ¬ ∃x ¬P(x)
¬∀x P(x) :: ∃x ¬P(x)
∃x P(x) :: ¬ ∀x ¬P(x)
¬∃x P(x) :: ∀x ¬P(x)
The statements in each pair can be substituted for each other in a proof. The ordinary language version of the equivalences is as follows:
“Everything is P” is equivalent to “It’s not the case that something is not P.”
“It’s not the case that everything is P” is equivalent to “Something is not P.”
“Something is P” is equivalent to “It’s not the case that everything is not P.”
“It’s not the case that there is P” is equivalent to “Everything is not P” or “Nothing is P.”
