 For example, in the formula \((\forall\)x(Axy \(\vee Bx) \amp Bx)\), the occurrences of “\(x\)” in Axy and in the first \(Bx\) are bound by the quantifier. The occurrence of “\(y\)” and last occurrence of “\(x\)” are free. In \(\forall x(Ax \rightarrow \exists\)xBx), the “\(x\)” in \(Ax\) is bound by the initial universal quantifier, while the other occurrence of \(x\) is bound by the existential quantifier. The above syntax allows this “double-binding”. Although it does not create any ambiguities (see below), we will avoid such formulas, as a matter of taste and clarity.