I am reading https://www.math.toronto.edu/weiss/set_theory.pdf. Page 14 asserts the following algorithm is executed on a formula $\Phi$ when substituting a variable $v_j$ for each free occurrence of a variable $v_i$ in $\Phi$:
- Substitute a new variable $v_l$ for all bound occurrences of a $v_i$ in $\Phi$
- Substitute a new variable $v_k$ for all bound occurrences of a $v_j$ in the result of (1)
- Directly substitute $v_j$ for each occurrence of $v_i$ in the result of (2)
Now suppose $\Phi$ is $(¬(v_i = v_j))$ and we would like to substitute $v_j$ for all free occurrences of $v_i$. Steps (1) and (2) does nothing because neither $v_i$ nor $v_j$ are bound in $\Phi$. (3) produces $(¬(v_j = v_j))$, which changes $\Phi$'s meaning. Is this supposed to happen or did I make a mistake? The new formula doesn't make sense logically.