A term t can be substituted for a variable x in a formula φ if, after one replaces x with t, none of the variables of t are in the scope of quantifiers of φ. We are trying to avoid the situation when φ has a subformula of the form ∀y. (... x ...) or ∃y. (... x ...) and t has a free variable y. Then when x is replaced by t, the previously free y incorrectly becomes bound. For example, the formula ∃y. x < y is true for any value of x, but after we replace x with y + 1, we get ∃y. y + 1 < y, which is false. Intuitively, the existentially bound y in the formula has no relationship with y in the term y + 1, so identifying them is a mistake. If we want to substitute y + 1 for x, we need to change the bound variable from y to, say, z: ∃z. x < z; then the result of the substitution ∃z. y + 1 < z is still true for any value of y.