From the book Logic for Mathematicians (A. G. Hamilton):
Definition 3.19
Two valuations $v$ and $v'$ are $i$-equivalent if $v(x_j)=v'(x_j)$ for all $j\neq i$.
(I know every single book out there have a different way to define this.)
Then consider $A= (\forall x_1)(\exists x_2) P(x_1,f(x_2))$ under the interpretation $\cal I$ with domain $\mathbb{Z}$, and $P(x_1,x_2)$ means $x_1=x_2$, and $f(x)=x+1$.
It is easy to see that $A$ is true for $\cal I$, but my goal is to write the proof in a more or less formal way (similar to the one that is handled in the same book).
This is what I have now:
Consider $v$ to be a valuation in $\cal I$, then $v(x_1), v(x_2) \in \mathbb{Z}$ and we interpret $P(x_1,f(x_2))$ as $v(x_1)=v(x_2)+1$ which is true for $v(x_1)=2$ and $v(x_2)=1$. Now we start to consider $i$-equivalent valuations. So for every valuation $v'$ 1-equivalent to $v$, there always exists a valuation $v'$ 2-equivalent to $v$ in which $v'(x_1)=v'(x_2)+1$.
I don't know if that's OK, and really I don't know if I'm understanding valuations well at all.
I think you've grasped the concept of valuations. As you've noted, not every presentation of interpretations for first-order logic does this exactly the same way. The Wikipedia article on interpretations in logic has a section interpretations of a first-order language, and you'll notice that they first describe the easy-to-grasp intuition of how to understand whether an interpretation satisfies $\forall x.\phi(x)$ and $\exists x.\phi(x)$.
The problem arises however, that we can't actually talk about $\phi(d)$, because that isn't actually a formula:
The definition given by Hamilton follows the second of these options. It does mean, however, that we no longer get to speak of an interpretation $\cal I$ satisfying a formula, but we have to speak of $\cal I$ and a valuation $v$ satisfying a formula. The alternative is to include a valuation $v$ inside an interpretation, but we still end up having to say that $\cal I = (D,\dots,v)$ (where $\dots$ is everything else that is in the interpretation) satisfies $\forall x.\phi(x)$ if and only if every $\cal I' = (D,\dots,v')$ satisfies $\forall x.\phi(x)$, where $v'$ differs from $v'$ only on $x$. This amounts to the same thing, but with more syntax.
Your proof is in pretty good shape as it is, I think. You could express some things a bit more rigorously, perhaps, but the intuition and general structure is correct. Since you're defining the domain to be $\mathbb{Z}$ and can reference mathematical functions in your semantic explanation, I think you can do something like the following. Since you are interpreting $P$ as the equality function on $\mathbb{Z}$ and $f$ as $+1$, I simply used equality in the following formula, and $s$ as the successor ($+1$) function.