# The problem of bound variables in mathematical definitions

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?

-
While it is a valid question, I hope that you are aware that there are only finitely many symbols we can use. It is often understood that if you do this sort of trickery then you can assume the variables in the formula are not $x$. Just rewrite them with different letters. –  Asaf Karagila Jan 23 '13 at 7:36
@Asaf: Sure, I am aware of the limited number of practical symbols that we can use. I am just surprised that Bernays does this sort of thing when the overall style of his book is close to being completely formal. I am pretty sure that this is to be avoided when one subjects a formal proof to the scrutiny of an automated proof checker. –  Haskell Curry Jan 23 '13 at 7:46

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)$.

-
Hagen, this is almost exactly what I had in mind, but your act of writing it down so nicely has made things crystal clear. –  Haskell Curry Jan 23 '13 at 7:58
This is called $\alpha$-equivalence in computer science. –  Zhen Lin Jan 23 '13 at 8:14
@ZhenLin: After you mentioned ‘$\alpha$-equivalence’, I now have an even clearer understanding of the problem. The variable $x$ in the first-order formula ‘$\text{On}(x)$’ is unquestionably free, and this freeness should not be affected by whether or not $x$ appears as a bound variable in a particular definition of $\text{On}$, because another definition, up to logical equivalence, may be found that avoids using $x$ as a bound variable. –  Haskell Curry Jan 23 '13 at 8:41
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.
See the example at: en.wikipedia.org/wiki/Variable_shadowing In that example, inside the function $f$ it is not possible to refer to the outside $x$. But if we renamed the inner $x$ to another variable, then we could refer to the outside $x$. –  Ted Jan 23 '13 at 8:11