Axiomatization of $(\mathbb Z, <)$

Question

I'm interested in the axiomatization of the total order $(\mathbb Z, <)$. My idea is to have first the axioms for a total order:

0. $\exists x : x = x$
1. $\forall x : \lnot(x < x)$
2. $\forall x : \forall y : \forall z : x < y \land y < z \to x < z$
3. $\forall x : \forall y : x < y \lor y < x \lor x = y$
4. $\forall x : \exists y : x < y \land \lnot \exists z : x < z \land z < y$
5. $\forall x : \exists y : y < x \land \lnot \exists z : y < z \land z < x$
6. (schema) $(\forall x : \forall y : (x < y \land \lnot \exists z : x < z \land z < y) \to \varphi(x) \to \varphi(y)) \to \forall u : \forall v : u < v \to \varphi(u) \to \varphi(v)$
7. (schema) $(\forall x : \forall y : (x < y \land \lnot \exists z : x < z \land z < y) \to \varphi(y) \to \varphi(x)) \to \forall u : \forall v : u < v \to \varphi(v) \to \varphi(u)$

Explanation:

• axiom 0 just avoids the empty universe (I like to be explicit about that)
• axioms 1, 2, 3 define the total order
• axioms 4 and 5 say that every element has a successor and a predecessor
• axiom schemas 6 and 7 ensure that the universe is not larger than $\mathbb Z$ via an induction-like idea which essentially says that properties $\varphi$ which transfer from any element to its successor will be satisfied by any element which is greater than an element known to satisfy $\varphi$ (axiom scheme 6) and the same for the other direction (axiom 7).

So now some questions:

1. Are there any redundant axioms in my system?
2. Are there any other models for my system other than $\mathbb Z$?
3. Are there any well-known axiomatizations for $\mathbb Z$ in the literature? Here I am interested specifically in an axiomatic approach that does not start by constructing $\mathbb N$.
4. If we remove axiom schemas 6 and 7, how would one characterize a maximal model for the remaining system? I feel like the result would be somewhat similar to ordinals, but bidirectional so no longer with the ability to distinguish individual elements in any way. Can we add axioms to describe this maximal model?

I am probably asking too many questions here, so I'll accept also suggestions for how to split this into several questions, if that seems appropriate.

Answer 1

Regarding "are there other well-known axiomizations of $\mathbb{Z}$," they satisfy canonicity in much the same way as the reals do. Much as the reals are the unique totally ordered Dedekind-complete field, the integers are the unique commutative ordered ring whose positive elements are well-ordered.