PA with successor not being a function

Question

The Peano axioms refer to the successor function $s$. What happens if we make $s$ non-deterministic, that is, when some natural numbers are allowed to have more than one successor? The resulting structure is an infinite tree, for example, $s(x)=s(y) \implies x=y$, but $x=y \ \,\not\!\!\!\!\implies s(x)=s(y)$. Is this theory consistent? If yes, what kind of statements are provable there? Also, what kind of statements were provable in PA, but not here? Finally, are there any statements that are provable here, but not in PA?

My intuition is that PA is stronger (in fact we don't know if there is any $n$ with two successors, i.e. any model of PA would be a model for this theory), so it should be consistent and no theorem of PA is disprovable.

Any references, hints, etc. will be greatly appreciated ;-)

Edit: As there were some concerns about the axioms in general, here they are. I'm using $\newcommand{\Mat}{\mathbb{M}}\Mat$ to denote the set of nodes of my tree. As pointed out in the illuminating comment by Rob Arthan, I do define my own equality relation $\bumpeq$. The successor relation (not function) will be denoted by $\prec$ (inspired by post of MJD).

1. $0 \in \Mat$.
2. $\forall x \in \Mat.\ x \bumpeq x$.
3. $\forall x,y \in \Mat.\ x \bumpeq y \implies y \bumpeq x$.
4. $\forall x,y,z \in \Mat.\ x \bumpeq y \land y \bumpeq z \implies x \bumpeq z$.
5. $\forall x \in \Mat.\ \forall y.\ x \bumpeq y \implies y \in \Mat$.
6. $\forall x \in \Mat.\ \Big(\exists y. x \prec y \land (x \bumpeq y \implies \bot) \Big) \land \Big( \forall z.\ x \prec z \implies z \in \Mat\Big)$.
7. $\forall x \in \Mat.\ x \prec 0 \implies \bot$.
8. $\forall x,y,z_x,z_y \in \Mat. x \prec z_x \land y \prec z_y \land x_z \bumpeq z_y \implies x \bumpeq y$.
9. Let $\phi$ be any unary predicate such that $\phi(0)$ and $$\forall x \in \Mat.\ \phi(x) \implies \forall y. x \prec y \implies \phi(y),$$ then $\forall x \in \Mat.\ \phi(x)$.

Addition:

• $\forall x_1,x_2,y_1,y_2 \in \Mat.\ x_1 \bumpeq x_2 \land y_1 \bumpeq y_2 \implies x_1 + y_1 \bumpeq x_2 + y_2$,
• $\forall x \in \Mat.\ x+0 \bumpeq x$,
• $\forall x,y,z \in \Mat.\ x \prec z \implies \exists v.\ x+y \prec v \land x+z \bumpeq v$.

Multiplication:

• $\forall x_1,x_2,y_1,y_2 \in \Mat.\ x_1 \bumpeq x_2 \land y_1 \bumpeq y_2 \implies x_1 \cdot y_1 \bumpeq x_2 \cdot y_2$,
• $\forall x \in \Mat.\ x \cdot 0 \bumpeq 0$,
• $\forall x,y,z \in \Mat.\ y \prec z \implies x \cdot z \bumpeq x + (x \cdot y)$.

Answer 1

I'm just thinking out loud, so made this CW, as it is too long for a comment. Let's write $a\prec b$ to mean that $b$ is a successor of $a$. Then we might axiomatize the proposed system as follows:

1. $\forall n. \lnot(n\prec 0)$
2. $\forall m n s. m\prec s \land n\prec s \implies m=n$.
3. $\forall m\exists s. m\prec s$ (I suppose this one is optional, but if you omit it you can get some degenerate models.)
4. For each one-place predicate $\Phi$, we have $(\Phi(0) \land (\forall k s. \Phi(k)\land k\prec s \implies \Phi(s)))\implies \forall n.\Phi(n)$.

Any model of the Peano axioms should model this as well, since we can take $a\prec b$ to mean $S(a) = b$.

I suppose you could add the axiom $\forall m s s'. m\prec s\land m\prec s'\implies s=s'$ and show that the resulting system is equivalent to the usual Peano axioms.