 All occurrences of variables in an atomic formula are free. The free occurrences of variables in the negation of a formula \(\lnot B\) are the free occurrences of variables in \(B\). The free occurrences of variables in a formula of the form \((B \rightarrow C)\) are the free occurrences of variables in \(B\) and \(C\). Finally, the free occurrences of variables in a quantified formula \(\forall xB\) are the variables other than \(x\) that are free in \(B\). We call \(B\) the scope of the initial occurrence of the quantifier \(\forall x\) in \(\forall xB\). If an occurrence of a variable is not free in a formula \(A\), then it is bound; all occurrences of \(x\) in \(B\) are bound in the quantified formula \(\forall xB\). In fact, we will often write that they lie within the scope of the initial quantifier.