> Does it also prevent a forward fork, to two separate tails?
This is prevented by saying that the successor function is a function. If a = b, then S(a) necessarily equals S(b). (The other half of axiom 7, the statement that when S(a) = S(b) then a = b, is the definition of an injective function. It's what prevents us from saying that the successor to 9 is 3.)
There is a fun image of dominos on the wikipedia page for the Peano axioms that explains how the structure of the natural numbers is constrained by the axioms.
A backwards loop from a number in the chain of succession from zero to an earlier number in the same chain can't happen because the successor function is injective.
A backwards fork (two chains meeting) can't happen for the same reason.
A forwards fork would be invisible to us as long as our only available tool is the successor function, which will always choose the same branch of the fork. This essentially means that forwards forks don't exist. There could be a larger structure in which it is true that e.g. the "9" node has one outgoing edge pointing to "10" and another one pointing to "green", but only one of those edges can be the edge picked out by the successor function, so our structure would only include one of the "10" or "green" nodes.
A loop parallel to the chain of succession from zero [imagine the normal chain "0, 1, 2, ..." alongside the three special elements 甲 乙 丙 arranged in a three-element circle] is ruled out by axiom 9, which says that any set that contains the chain of succession from zero contains all the natural numbers.
thinking out loud...
we are free to define a predecessor function by saying it is the inverse of the successor function. That definition would immediately prove the pred_succ theorem, as long as the successor function is invertible. Half the definition of being invertible is being injective, so this doesn't let us prove succ_inj in a non-circular way.
I don't know how else we would attempt to define the predecessor function, given the algebraic structure we're working with where all values take the form "0" or "succ n".
I was very wrong earlier: characteristic is taken care of by 0 not being a successor; injectivity of succ also allows circular pseudo-nats.
PS. found Peano (1889): https://archive.org/details/arithmeticespri00peangoog/page/n...