Axioms for order relation:
- $x \not\lt x$
- $[x \lt y \land y \lt z] \Rightarrow x \lt z$
- $[x \lt y \lor x = y \lor y \lt x]$
- $x \lt y \Rightarrow x+z \lt y+z$
- $[x <y \land 0 < z] \Rightarrow x\times z < y \times z$
Question: We have that $(\mathbb{Z}, +, \times, <)$ is the ordered integral domain of integers with the usual order relation defined as $x<y \Leftrightarrow y-x \in Z^+$, we must show that if $(\mathbb{Z}, +, \times, <')$ is an ordered integral domain too, then $<'$ is identical with $<$.
Here is my short atempt:
$$(x<y) \Leftrightarrow (0 <y-x) \Leftrightarrow (y-x \in Z^+) \Leftrightarrow (0 <' y-x) \Leftrightarrow (x<'y)$$
Since $Z^+$ is unique and the order relation on integral domain should give $0<x$ for any positive $x$, I tried this approach after failing in all other paths, some of my other ideas was to assume $<$ and $<'$ as ordering relations satisfying the axioms for ordering and then trying to reach a contradiction if the relations are not identical, but I got stucked.
My atempt is correct?
It is enough to prove $1>0$ since this would imply that $x>0>-x$ for $x\in Z^+$, using $1>0$ implies $2>1$ implies ... implies $x>x-1$ and then using the second axiom, while for the other direction we get $1+(-1)>0+(-1)$ using the fourth axiom again. Since 1 is not 0 in an integral domain, we have that $1>0\vee 1<0$ and if $1<0$, using the fourth axiom, we get that $-1>0$ and using the last axiom we get $0<-1\wedge 0<-1\Rightarrow 0<1$ which is a contradiction. So $1>0$ and we are done.
EDIT: Showing the explicit induction.
Basis for $x=1$ is trivial since we showed $0<1$.
Let $x\in Z^+$ s.t. $x>1$, then $x-1\in Z^+$. Let us assume $x-1>0$ and show that $x>0$: Indeed, we get $$x=(x-1)+1>^*0+1=1>0$$ where we used the fourth axiom in the starred inequality, and $1>0$ in the last inequality. We finish by using transitivity (2nd axiom) and concluding that $x>0$.