In predicate calculus, a universal 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 universally quantified.
Every universal formula is logically equivalent to the negation of some existential
formula (and vice-versa).
When there are no free variables (i.e., when all the variables are bound) in a universal
formula, it is called a universal sentence.
