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.
