Prove strict well-order from Peano successor function

Question

Is there a way to prove from (a variation) of the Peano successor function without induction that < is a strict well-order? Specifically, let $m\leftarrowtail n$ represent that $n$ is the successor of $m$ and assume the axioms

1. $1\in N$
2. if $m\in N$ then $\exists! n\in N.m\leftarrowtail n$
3. $\neg \exists m.m\leftarrowtail 1$
4. if $n\in N$ and $n\ne 1$ then $\exists! m\in N.m\leftarrowtail n$

Note that I have combined two Peano axioms into one for axiom 2 (existence and uniqueness of successors), and added a new axiom for axiom 4 (you can't prove unique predecessors without induction, and you need them to prove induction from well-orderedness).

The transitive closure of the $\leftarrowtail$ relation is the normal $<$ relation from arithmetic. My question is, can you prove that this transitive closure is a well-order without induction? I think I can prove it, but I'm having trouble formalizing the idea.

Answer 1

No, those axioms aren't enough to guarantee well-orderedness.

Consider for example the linear order $$(\mathbb{N}\times\{0\})\cup(\mathbb{Z}\times \{1\})$$ ordered by setting $(a,i)<(c,j)$ iff $i<j$ or $i=j$ and $a<c$. Intuitively, this looks like a copy of $\mathbb{N}$ followed by a copy of $\mathbb{Z}$. This linear order has a first element $(1,0)$ and a successor operation which together satisfy all your axioms, but it is clearly not well-ordered.

(Indeed, it turns out that no first-order axiom system is enough to guarantee well-orderedness, by the compactness theorem.)