\begin{definition}[Definition:Free Occurrence]
Let $\LL_1$ be the language of predicate logic.
Let $\mathbf A$ be a WFF of $\LL_1$.
An occurrence of a variable $x$ in $\mathbf A$ is said to be a '''free occurrence''' {{iff}} it is not bound.
\end{definition}