Proving the order relation in $\mathrm{PA}$ is total.

Question

Let $\mathrm{PA}$ be the first order logic axioms of Peano Arithmetic. Define an order relation by: $$ x\leq y\; \text{ if }\; (\exists z)(x+z=y). $$ Can it be proved that this relation is total?

Answer 1

Yes, you can prove the formula $(\exists z: x+z=y)\vee (\exists z: y+z=x)$ by induction on $x$, say. In the induction step, consider the two cases $\exists z: x+z=y$ or $\exists z: y+z=x$. In the first case, pick $z$ with $x+z=y$. If $z=0$, then $x=y$, so $\exists z: y+z=x+1$ holds (take $z=1$). If $z=z^{\prime}+1$, then $(x+1)+z^{\prime}=y$, so $\exists z: (x+1)+z=y$ holds. In the second case, $y+z=x$ implies $y+(z+1)=x+1$, so again $\exists z: y+z=x$ holds.