 We next define the notion of an occurrence of a variable being free or bound in a formula. A variable that immediately follows a quantifier (as in “\(\forall x\)” and “\(\exists y\)”) is neither free nor bound. We do not even think of those as occurrences of the variable. All variables that occur in an atomic formula are free. If a variable occurs free (or bound) in \(\theta\) or in \(\psi\), then that same occurrence is free (or bound) in \(\neg \theta, (\theta \amp \psi), (\theta \vee \psi)\), and \((\theta \rightarrow \psi)\). That is, the (unary and binary) connectives do not change the status of variables that occur in them. All occurrences of the variable \(v\) in \(\theta\) are bound in \(\forall v \theta\) and \(\exists v \theta\). Any free occurrences of \(v\) in \(\theta\) are bound by the initial quantifier. All other variables that occur in \(\theta\) are free or bound in \(\forall v \theta\) and \(\exists v \theta\), as they are in \(\theta\).