Understand "i-Equivalent Valuation" that satisfies formula 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.
 A: 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)$.

This leaves the issue of how to interpret formulas of the form ∀ x φ(x) and ∃ x φ(x). The domain of discourse forms the range for these quantifiers. The idea is that the sentence ∀ x φ(x) is true under an interpretation exactly when every substitution instance of φ(x), where x is replaced by some element of the domain, is satisfied. The formula ∃ x φ(x) is satisfied if there is at least one element d of the domain such that φ(d) is satisfied. — Interpretations of a first-order language

The problem arises however, that we can't actually talk about $\phi(d)$, because that isn't actually a formula:

Strictly speaking, a substitution instance such as the formula φ(d) mentioned above is not a formula in the original formal language of φ, because d is an element of the domain. There are two ways of handling this technical issue. The first is to pass to a larger language in which each element of the domain is named by a constant symbol. The second is to add to the interpretation a function that assigns each variable to an element of the domain. Then the T-schema can quantify over variations of the original interpretation in which this variable assignment function is changed, instead of quantifying over substitution instances. — Interpretations of a first-order language

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.

Interpretation $\cal I$ and valuation $v$ satisfy $\forall x_1.\exists x_2.(x_1 = s(x_2))$ if and only if $\cal I$ and every 1-equivalent valuation $v'$ satisfy $\exists x_2.(x_1 = s(x_2))$.  The interpretation $\cal I$ and valuation $v'$ satisfy $\exists x_2.(x_1 = s(x_2))$ if and only if there is some valuation $v''$ that is 2-equivalent to $v'$ such that $\cal I$ and $v''$ satisfy $x_1 = s(x_2)$.
Consider an arbitrary valuation $v$.  Let $v'$ be an arbitary valuation that is 1-equivalent to $v$.  Then let $n = v'(x_1)$. Let $v''$ be the valuation that agrees with $v'$ on every value except $x_2$, which it maps to $n-1$.  Observe that $\cal I$ and $v''$ satisfy $x_1 = s(x_2)$.  Then, since there is some valuation (viz., $v''$) that is 2-equivalent to $v'$ which, with $\cal I$, satisfies $x_1 = s(x_2)$, then $\cal I$ and $v'$ satisfy $\exists x_2.(x_1 = s(x_2))$.  Then, since $v'$ is an arbitrary valuation 1-equivalent to $v$, every valuation 1-equivalent to $v$, with $\cal I$, satisfies $\exists x_2.(x_1 = s(x_2))$, so $\cal I$ and $v$ satisfy $\forall x_1.\exists x_2.(x_1 = s(x_2))$.

