This web page gives the official definition of what it means for a variable $v$ to be free in a formula $\varphi $ of a first-order language $L$.

The definition of what it means for
$v$ to be free in $\varphi $ or term $t$
of a
first-order language $L$ is y induction on terms
and formulas. We shall specify what it means for
$v$ to be free in each of the constructions of
terms and formulas, and assume that
it is already understood what
$v$ is free in $\varphi $
[or term $t$]

is already understood for all subformulas and subterms.

Most syntactical definitions in first order logic are of this kind: such definitions implicitly require the Theorem on Unique Readability, which says that for any term or formula there is a unique way of reading it as built from subformulas and subterms, and therefore exactly one of our inductive clauses applies.

Fix a first order language $L$ and variable $v$ of $L$. Here are the clauses defining what it means for $v$ to be free in $\varphi $.

- $v$ is free in $v$
- $v$ is not free in $c$ for a constant symbol $c$
- $v$ is free in $F({t}_{1},\dots ,{t}_{k})$ (where $F$ is a $k$-ary function symbol) if and only if $v$ is free in at least one of ${t}_{1},\dots ,{t}_{k}$
- $v$ is not free in $\top $ nor in $\perp $
- $v$ is free in $({t}_{1}={t}_{2})$ if and only if $v$ is free in at least one of ${t}_{1},{t}_{2}$
- $v$ is free in $R({t}_{1},\dots ,{t}_{k})$ (where $R$ is a $k$-ary relation symbol) if and only if $v$ is free in at least one of ${t}_{1},\dots ,{t}_{k}$
- $v$ is free in $\neg \varphi $ if and only if $v$ is free in $\varphi $
- $v$ is free in $({\varphi}_{1}\vee {\varphi}_{2})$ if and only if $v$ is free in at least one of ${\varphi}_{1},{\varphi}_{2}$
- $v$ is free in $({\varphi}_{1}\wedge {\varphi}_{2})$ if and only if $v$ is free in at least one of ${\varphi}_{1},{\varphi}_{2}$
- $v$ is free in $({\varphi}_{1}\to {\varphi}_{2})$ if and only if $v$ is free in at least one of ${\varphi}_{1},{\varphi}_{2}$
- $v$ is free in $\forall w\varphi $ if and only if $v$ is not the same variable as $w$ and $v$ is free in $\varphi $
- $v$ is free in $w\varphi $ if and only if $v$ is not the same variable as $w$ and $v$ is free in $\varphi $

That's it. You should be able to check that this defines
$v$ is free in $\varphi $

for all $\varphi $. Readers
with some programming experience will recognise the definition just given
as a recursive definition, and will easily be able to write a subroutine
or function in their favourite language that computes whether
$v$ is free in $\varphi $. In other words, this notion is
(rather easily) computable.

Exercise.

Show that
$v$ is not free in $\varphi $

is equivalent
to the statement that Each occurence of $v$ in $\varphi $ is in the
scope of a quantifier $\forall v$ or $v$.

It is common to write a formula $\varphi $ or term $t$ with arguments displayed as $\varphi ({v}_{1},\dots ,{v}_{k})$ or $t({v}_{1},\dots ,{v}_{k})$. When so-doing it is important to list all of the variables that occur free in $\varphi $ or $t$. It is always OK to include additional variables, however, and this sometimes saves a lot of writing. The reason for this is that there is little difference between $\varphi ({v}_{1},{v}_{2})$ and $\varphi ({v}_{1},{v}_{2})\wedge ({v}_{3}={v}_{3})$ so it is OK to write the former as $\varphi ({v}_{1},{v}_{2},{v}_{3})$. But it would be a mistake to write $\varphi ({v}_{1},{v}_{2})\wedge ({v}_{3}={v}_{3})$ as $\varphi ({v}_{1},{v}_{2})$ as the ${v}_{3}$ does play a role and must not be forgotten.

Definition.

A closed term is a term which has no free variables (and hence has no variables at all). A sentence is a formula which has no free variables. Sentences are sometimes called closed formulas.