Substitution In Logic

Question

I am trying to understand how substitution of variables with terms works in Toposes and Local Set Theories by Bell. However I don't think the details of that book are important for my question, and I imagine my question can answered based on most systems involving logic and substitution.

For a term $\tau$ we write $\tau(x / \sigma)$ to denote the term obtained by taking $\tau$ and substituting every free occurrence of variable $x$ with term $\sigma$.

Suppose $\alpha$ is a formula. I have two questions.

(1) What is $(\alpha(x/y))(x/z)$ for variables $x,y,z$ ?

I presume the answer is $\alpha(x/y).$ But maybe a case could be made for the answer being $\alpha(z/y),$ so I would appreciate clarification.

(2) What is $(\{y : \alpha(x/y) \}) (x/z)$ ? Again I can imagine the answer being $\{y : \alpha(x/y) \}$ or $\{y : \alpha(z/y) \},$ but I am not sure which is the correct answer.

The reason I ask is that I want to understand the meaning of $(\exists ! x ) \alpha,$ which is shorthand for $(\exists x) (\alpha \wedge (\forall y)(\alpha (x / y) \Rightarrow x = y )).$ This relates to (2) since $(\forall y) \beta$ is shorthand for $\{ y : \beta \} = \{ y : true \}.$

All this relates to another question I asked before:

Unique Existence In Local Set Theories

Answer 1

Substitution is a "meta" operation that acts on terms, so the term $\alpha(x/y)$ represents a term with no (free) occurrences of $x$. Furthermore, if a term $\beta$ contains no (free) occurrence of $x$, then $\beta(x/y) = \beta$. Therefore,

1. $(\alpha(x/y))(x/z) = \alpha(x/y)$
2. For comprehension, $\{y : \alpha\}$ is a term that binds the variable $y$ in $\alpha$. So $\{y : \alpha(x/y)\}(x/z) = \{y : \alpha(x/y)\}$ because $\{y :\alpha(x/y)\}$ does not contain any occurrence of $x$.