Peano axioms and Herbrand's theorem

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)

• I imagine that $\equiv$ must be $=$... Commented Jun 19, 2018 at 12:00
• well in the language of first order logic we were using the $\equiv$ symbol, but yes it is basically the same i guess Commented Jun 19, 2018 at 12:01
• Basically, you have to prove that : $∀x∀y∃!zφ(x,y,z)$ where $φ(x,y,z)$ says that $(x+y)⋅(x+y+1)+(1+1)⋅x$ is even. Commented Jun 19, 2018 at 12:09
• i see, i think i got on the right track now. i was not entirely sure why i can use the fact that $1\cdot x=x$, but it is just simple induction. Commented Jun 19, 2018 at 12:15
• If so, we have to prove that : $(x+y)⋅(x+y+1)$ is even. Commented Jun 19, 2018 at 12:20

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.