Open formula

An open formula does not have a truth value assigned to it, in contrast with a closed formula which constitutes a proposition and thus can have a truth value like true or false. An open formula can be transformed into a closed formula by applying a quantifier for each free variable. This transformation is called capture of the free variables to make them bound variables.

For example, when reasoning about natural numbers, the formula "x+2 > y" is open, since it contains the free variables x and y. In contrast, the formula "∃y ∀x: x+2 > y" is closed, and has truth value true.

Open formulas are often used in rigorous mathematical definitions of properties, like

"x is an aunt of y if, for some person z, z is a parent of y, and x is a sister of z"

(with free variables x, y, and bound variable z) defining the notion of "aunt" in terms of "parent" and "sister". Another, more formal example, which defines the property of being a prime number, is

"P(x) if ∀m,n∈: m>1 ∧ n>1 → x≠ m⋅n",

(with free variable x and bound variables m,n).

An example of a closed formula with truth value false involves the sequence of Fermat numbers

studied by Fermat in connection to the primality. The attachment of the predicate letter P (is prime) to each number from the Fermat sequence gives a set of closed formulae. While they are true for n = 0,...,4, no larger value of n is known that obtains a true formula, as of 2023; for example, is not a prime. Thus the closed formula ∀n P(F_n) is false.

In database theory, when expressing a query as an open first-order formula, the free variables represent the ones that in an SQL query would occur in the SELECT clause. For example, a formula like:

where is the only free variable, could be expressed in SQL as follows:

which selects all the people born in 2020 and having a mother born in 1999.

Formally, executing the above SQL query over a database is equivalent to look for all the substitutions of the free variables of with constants such that the Herbrand interpretation of satisfies , where is the set of ground atoms representing the database.