On p. 134 of A Concise Introduction to Mathematical Logic (Third Edition), the author gives an example of procedural semantics in a structure $\mathcal{A} = (\mathbb{N}^{\mathcal{A}}, 0^{\mathcal{A}}, \mathsf{S}^{\mathcal{A}}, \mathsf{Pd}^{\mathcal{A}})$. (Quantifiers are absent because we're considering this formula in the special context of procedural semantics.) I think that his definition of the predecessor function (listed in the title of this question) is defective, because there is more than one $y$ for some $x$.
Let us say that we have a variable assignment $w$ with $w(y) = y^w$ and $w(x) = \mathsf{S}^{\mathcal{A}}y^w$. Then, clearly, $(\mathcal{A}, w) \models y = \mathsf{Pd}x$, because $(\mathcal{A}, w) \models x = \mathsf{S}y$. Consider also $w'$ with $w'(y) = 0^{\mathcal{A}}$ and $w'(x)$ arbitrary. Then $(\mathcal{A}, w') \models y = \mathsf{Pd}x$, because $(\mathcal{A}, w') \models y = 0$. Clearly, this definition of the predecessor function entails that every natural number different from $0$ and $1$ has two predecessors, its actual predecessor and $0$, which makes the definition defective.
I would suggest this amendment:
$$ y = \mathsf{Pd}x \leftrightarrow (x = 0 \lor x = \mathsf{S}0 \leftrightarrow y = 0) \land (y \neq 0 \to x = \mathsf{S}y). $$
I would like to know whether my reasoning in this post is correct. I hope that I haven't made any embarrassing mistakes. Thank you for your time. :)