In predicate calculus, an existential formula is a prenex normal form formula (i.e., a formula written as a string of quantifiers
and bound variables followed by a quantifier-free part) in which the quantified variables
are existentially quantified.
Every existential formula is logically equivalent to the negation of some universal
formula (and vice-versa).
When there are no free variables (i.e., when all the variables are bound) in an existential
formula, it is called an existential sentence.
