stylistic:style_transfer, structural:summarization
Free and bound variables

In a formula, a variable may occur free or bound (or both). One formalization of this notion is due to Quine, first the concept of a variable occurrence is defined, then whether a variable occurrence is free or bound, then whether a variable symbol overall is free or bound. In order to distinguish different occurrences of the identical symbol x, each occurrence of a variable symbol x in a formula φ is identified with the initial substring of φ up to the point at which said instance of the symbol x appears. Then, an occurrence of x is said to be bound if that occurrence of x lies within the scope of at least one of either ∃ x {\displaystyle \exists x} or ∀ x {\displaystyle \forall x}. Finally, x is bound in φ if all occurrences of x in φ are bound.

Intuitively, a variable symbol is free in a formula if at no point is it quantified: in ∀ y P (x, y), the sole occurrence of variable x is free while that of y is bound. The free and bound variable occurrences in a formula are defined inductively as follows.

For example, in ∀ x ∀ y (P (x) → Q (x, f (x), z)), x and y occur only bound, z occurs only free, and w is neither because it does not occur in the formula.

Free and bound variables of a formula need not be disjoint sets: in the formula P (x) → ∀ x Q (x), the first occurrence of x, as argument of P, is free while the second one, as argument of Q, is bound.

A formula in first-order logic with no free variable occurrences is called a first-order sentence. These are the formulas that will have well-defined truth values under an interpretation. For example, whether a formula such as Phil(x) is true must depend on what x represents. But the sentence ∃ x Phil(x) will be either true or false in a given interpretation.