The problem of bound variables in mathematical definitions

Question

I was reading Paul Bernays’ Axiomatic Set Theory recently; in the book, Bernays gives the following definition of ‘ordinal number’.

\begin{align} \text{On}(\alpha) \stackrel{\text{def}}{\iff} &(\forall x)(\forall y)(((x \in y) \land (y \in \alpha)) \implies (x \in \alpha)) \land \\ &(\forall x)(\forall y)(((x \in \alpha) \land (y \in \alpha) \land (x \neq y)) \implies ((x \in y) \lor (y \in x))) \land \\ &(\forall x)(((x \subseteq \alpha) \land (x \neq \varnothing)) \implies (\exists y)((y \in x) \land (y \cap x = \varnothing))). \end{align}

There is nothing wrong with this straightforward definition, of course. Rather, the problem is that a few pages later, Bernays wishes to say that ‘$ x $ is an ordinal’ and does so by writing ‘$ \text{On}(x) $’. In my opinion, this is an incorrect way of doing things because $ x $ is already a bound variable in the definition above.

More generally, when one defines new predicate symbols from those that come with a given first-order theory $ T $, must we be careful not to use, with these new symbols, variables that already appear bound in the definitions? Or can we afford to be a little sloppy and just use any variables that happen to be convenient for the occasion at hand?

Answer 1

Let $\alpha, x, y$ be different variable names. By the definition, $\operatorname{On}(\alpha)\iff \forall x\colon\phi(x,\alpha)$. By a general argument $\forall x\colon\phi(x,\alpha)\iff \forall y\colon\phi(y,\alpha)$. Therefore $\forall\alpha\colon (\operatorname{On}(\alpha)\iff \forall y\colon\phi(y,\alpha))$ and specifically $\operatorname{On}(x)\iff \forall y\colon\phi(y,x)$.

Answer 2

No, there is nothing wrong with it. The semantics of first-order logic imply that an $x$ outside the definition (as in "$x$ in an ordinal") is a "different" $x$ from any $x$ inside the definition, just like the multiple instances of $x$ that are inside the definition itself, but under different quantifiers, do not refer to the same thing.

That said, it is certainly necessary to be careful when applying the definition to the sentence "$x$ is an ordinal". You cannot just substitute $x$ for $\alpha$ everywhere in the definition. You must rename all the bound $x$'s in the definition to something else before substituting.

This is not unlike the shadowing problem in many programming languages, where if you introduce a local ("bound") variable in a context where a global ("free") variable of the same name exists, then you can no longer refer to the global variable within the scope ("quantifier") of the local variable.