We denote the Peano axioms with $\mathsf {PA}$ and $S=\{0,1,+,\cdot,<\}$ denotes the language of number theory.
Let $\varphi$ be the formula $$(1+1)\cdot v_2\equiv(v_0+v_1)\cdot(v_0+v_1+1)+(1+1)\cdot v_0$$
I have to prove that $$\mathsf {PA}\vdash\forall x\forall y\exists z[\varphi(x,y,z)\wedge\forall u(\varphi(x,y,z)\longrightarrow u\equiv z)]$$
Now I thought about using Herbrand's theorem by proving that the negation of $\varphi$, which is equivalent to
$$\forall x\forall y\forall z\exists u\hspace{3pt}\psi$$
where $$\psi=\neg(\varphi(x,y,z)\wedge\varphi(x,y,u)\longrightarrow u\equiv z)$$
is inconsistent.
(so if i can get rid of that $\exists$ quantifier, i could do the following)
For this I have to find variable free terms $t_i^j\in T^S$ such that
$$\bigwedge_{j=0}^N \psi\frac{t_0^j,t_1^j,t_2^j,t_3^j}{x,y,z,u}$$
is inconsistent.
But i do not know how to find these terms.
any help would be very much appreciated.
edit: i just realized that the $\forall u$ becomes $\exists u$ in the negation, which would be bad because i would have to get rid of the $\exists$ in order to use Herbrand.
and if i want to get rid of that $\exists$, i would get an extra negation in the front, which would not work with Herbrand (i think)
so first of all much thanks to Mauro ALLEGRANZA.
for anyone who may stumble across this, here is my attempted solution (it might be a little messy, but i hope it is all correct):
First note that by induction we get $\forall x\hspace{5pt} 1\cdot x=x$, since $0\cdot 1=0$ and $1\cdot(x+1)=1\cdot x+1$.
Secondly, we show that $\forall y\exists z[(1+1)\cdot z=y\cdot(y+1)]$ by induction over $y$. Clearly $(1+1)\cdot 0=0\cdot(0+1)$ Furthermore $(y+1)\cdot(y+1+1)=(y+1)\cdot(y+1)+y+1=y\cdot(y+1)+y+1+y+1=y\cdot(y+1)+(1+1)\cdot(y+1)=(1+1)\cdot(z+y+1)$.
Now we use induction over $x$ to show $\forall x\forall y\exists z[(1+1)\cdot z=(x+y)\cdot(x+y+1)]$.
The case $x=0$ follows from our previous result. Furthermore \begin{align*} (x+1+y)\cdot(x+1+y+1)&=(x+y+1)\cdot(x+y+1)+x+y+1 \\ &=\underbrace{(x+y)\cdot(x+y+1)}_{=(1+1)\cdot z}+(1+1)\cdot(x+y+1) \\ &=(1+1)\cdot(x+y+z+1) \end{align*} Then we have $\forall x\forall y\exists z[(1+1)\cdot z+(1+1)\cdot x\overset{2.}{=}(x+y)\cdot(x+y+1)+(1+1)\cdot x]$.
Therefore, by putting $z=z+x$ and with part 2, we get $$\forall x\forall y\exists z[(1+1)\cdot z\overset{2.}{=}(x+y)\cdot(x+y+1)+(1+1)\cdot x]$$ It remains to show uniqueness. Use induction over $u$. We have
$\varphi(x,y,z)\wedge\varphi(x,y,0)\longrightarrow 0=(x+y)\cdot(x+y+1)+(1+1)\cdot x\longrightarrow x=0\wedge y=0\longrightarrow z=0\longrightarrow u=z$
The induction step yields \begin{align*} \varphi(x,y,u+1)&\longrightarrow(1+1)\cdot(u+1)=(x+y)\cdot(x+y+1)+(1+1)\cdot x \\ &\longrightarrow(1+1)\cdot u+1+1=(x+y)\cdot(x+y+1)+(1+1)\cdot x \\ &\overset{\text{induction step}}{\longrightarrow}(1+1)\cdot z+1+1=(x+y)\cdot(x+y+1)+(1+1)\cdot x \\ &\longrightarrow z+1=u+1 \end{align*} This yields our desired result.