TITLE: Definition of $(\exists_1x)\mathscr B(x)$
QUESTION [1 upvotes]: This question is from Introduction to Mathematical Logic by Elliot Mendelson , forth edition , page 99 about the definition of $(\exists_1x)\mathscr B(x)$. In the book , the definition is written like this:

$(\exists_1x)\mathscr B(x)$ as for $$(\exists x)\mathscr B(x) \land (\forall x)(\forall y)(\mathscr B(x) \land \mathscr B(y) \to x = y)$$
In this definition, the new variable $y$ is assumed to be the first variable that
does not occur in $\mathscr B(x)$. A similar convention is to be made in all other
definitions where new variables are introduced.

My question is , what do they exactly mean by "...assumed to be the first variable..." ?

REPLY [2 votes]: The important point is that $y$ should not clash with the free variables of $\mathscr{B}(x)$. Requiring $y$ to be the first variable in the sequence of all variables $x_1, x_2, \ldots$ that does not occur in $\mathscr{B}$ is just a definite way of ensuring that $y$ does not clash.
To see why this is necessary, take $\mathscr{B}(x) \equiv x > y$ so that, in $(\Bbb{Q}, >)$, for example, $(\exists_1 x) \mathscr{B}(x)$ is false.
Then if we allow $y$ in the definition to clash with the free variable $y$ of $\mathscr{B}(x)$, the definition would give us:
$$(\exists x)x > y \land (\forall x)(\forall y)(x > y \land y > y \to x = y)$$
which, unlike $(\exists_1 x) \mathscr{B}(x)$ is true, because $y > y$ is always false. If we avoid the clash, by picking a variable $z$ that is different from $x$ and $y$, we get the correct equivalent of $(\exists_1 x) \mathscr{B}(x)$:
$$(\exists x)x > y \land (\forall x)(\forall z)(x > y \land z > y \to x = z)$$
which is false, as we would expect.
{"set_name": "stack_exchange", "score": 1, "question_id": 4160168}