PA with successor not being a function 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).


*

*$0 \in \Mat$.

*$\forall x \in \Mat.\ x \bumpeq x$.

*$\forall x,y \in \Mat.\ x \bumpeq y \implies y \bumpeq x$.

*$\forall x,y,z \in \Mat.\ x \bumpeq y \land y \bumpeq z \implies x \bumpeq z$.

*$\forall x \in \Mat.\ \forall y.\ x \bumpeq y \implies y \in \Mat$.

*$\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)$.

*$\forall x \in \Mat.\ x \prec 0 \implies \bot$.

*$\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$.

*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)$.

 A: 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:


*

*$\forall n. \lnot(n\prec 0)$ 

*$\forall m n s. m\prec s \land n\prec s \implies m=n$. 

*$\forall m\exists s. m\prec s$ (I suppose this one is optional, but if you omit it you can get some degenerate models.)

*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.
A: $\newcommand{\Mat}{\mathbb{M}}\Mat$I think the situation you have in mind is a common situation in model theory, where a definable equivalence relation $R$ on some subset of the universe of a structure $\cal M$, say, is respected by the interpretations of the function and predicate symbols. This lets you define a quotient structure ${\cal M}/R$ whose universe comprises the equivalence classes of $R$ in which the interpretations of the function and predicate symbols are induced from their interpretations in $\cal M$. For a reference, see section 1.3 of David Marker's Model Theory: an Introduction.
You seem want to run this construction backwards, and axiomatize structures $\cal M$ that admit an equivalence relation $R$ such that ${\cal M}/R$ is a model of $PA$. Essentially such an $\cal M$ is just a model of $PA$ where each number can have many different names (and some names, namely those outside $\Mat$, may not denote numbers at all). (So that's just like linguistic reality for someone who speaks more than one language!) Every model of $PA$ will give rise to a model of your axiomatisation, but the converse is also true, so the latter is not really weaker than $PA$ in any essential way.
Even if you do not require that $\prec$ respects the equivalence relation, you can still extract a model of $PA$ from a model of your axioms: given such a model $\cal M$ say with universe $M$. As MJD has pointed out, the induction principle implies, that for any $x \in M$, either $x = 0$ or $\exists a.a \prec x$. From this it follows that the relation $\simeq$ defined by $x \simeq y$ iff $x \bumpeq y \lor \exists a b.a \bumpeq b \land a \prec x \land b \prec y$ is an equivalence relation and ${\cal M}/{\simeq}$ is a model of $PA$.
A: Here's a model of these axioms in which addition and multiplication aren't commutative.
Let $\mathbb M$ be the set of strings over the alphabet $\{0,1\}$, that is:
 $$\mathbb M = \bigcup_{i=0,1,2,...}\{0,1\}^i = \{(),(0),(1),(00),(10),(10),(11),(000),...\}$$
We define addition over M as concatenation of strings, that is for $x\in\{0,1\}^i$ and $y\in\{0,1\}^j$ we define $x+y\in\{0,1\}^{i+j}$ as:
$$(x+y)_k=\begin{cases}
x_k, & k\le i \\
y_{k-i} & k > i \\
\end{cases}$$
We then define $x \prec y \iff y = x + (0) \lor y = x+(1)$, notice that if $x\in\{0,1\}^i$ and $x\prec y$ then $y\in\{0,1\}^{i+1}$, where $i+1\gt i\ge0$ so in particular we have $y\neq()$.
We define the constant 0 to be (), and the previous claim becomes axiom 7.
Now we have $0 = () \in \mathbb M$ which is axiom 1, we obviously have axioms 1–5 since we use standard equality. We have 6 since for $x\prec y$ there exists $i$ such that $x\in\{0,1\}^i \land y\in\{0,1\}^{i+1}$ and we know that $\{0,1\}^i \cap \{0,1\}^{i+1} = \emptyset$. We've already seen axiom 7 above.
If I understand axiom 8 correctly we have that too since for every $x\prec y$ we can express $x$ in terms of $y$:
$$\forall 1 \le i \le length(x) = length(y)-1: x_i = y_i$$
Axiom 9 is shown true by induction on the length of the strings.
The first and second axioms of addition are easy from our definition, the third can be shown from associativity of concatenation:
$$y\prec z \implies z = y+(0) \lor z = y+(1) \implies \\(x+y\prec (x+y)+(0)=x+(y+(0))=x+z) \lor (x+y\prec (x+y)+(1)=x+(y+(1))=x+z)$$
We define $xy$ as $x$ concatenated to itself $length(y)$ times, that is for $x\in\{0,1\}^i$ and $y\in\{0,1\}^j$ we define $xy\in\{0,1\}^{ij}$ as
$$xy = repeat(x,j), \text{where we define repeat to be,}\\
repeat(x,j) = \begin{cases}
(), & j = 0 \\
x+repeat(x,j'), & j = j' + 1 \ge 1 \\
\end{cases}
$$
The first and second multiplication axioms seem to follow from the definition, let us prove the third, if $y\prec z$ then $length(z) = length(y)+1$ so we have:
$$xz = repeat(x,length(z)) = repeat(x,length(y)+1) = x+repeat(x,length(y)) = x+(xy)$$
