This is how the forallx text describes free and bound variables (page 223, section 26.3):
A bound variable is an occurrence of a variable x that
is within the scope of either ∀x or ∃x.
A free variable is any occurrence of a variable that is not
As an example to illustrate bound and free variables and the scope of quantifiers, they provide the following
∀x(E(x) ∨ D(y)) → ∃z(E(x) → L(z, x))
The scope of the universal quantifier ‘∀x’ is ‘∀x(E(x) ∨ D(y))’,
so the first ‘x’ is bound by the universal quantifier. However, the
second and third occurrence of ‘x’ are free. Equally, the ‘y’ is free.
The scope of the existential quantifier ‘∃z’ is ‘(E(x) → L(z, x))’,
so ‘z’ is bound.
Note how the ‘x’ is free in the consequent, but bound in the antecedent. Furthermore formulas need not be sentences in the context of the forallx text:
A sentence of FOL is any formula of FOL that contains
no free variables.
It is important to be aware of the definitions of the logic text you are using and when reading a different text to note any differences one might find.
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf