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


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


  • $\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)$.
  • $\begingroup$ If $s$ is not a function, what does $s(x)$ mean? $\endgroup$ – Tobias Kildetoft Mar 26 '13 at 13:44
  • $\begingroup$ So instead consider $s$ a binary relation with what axioms? (1) $\neg ( \exists x ) ( s (x,0) )$. (2) $( \forall x ) ( \exists y ) ( s ( x , y ) )$. (3) $( \forall x ) ( \forall y ) ( \forall z ) ( ( s (x,z) \wedge s(y,z) ) \rightarrow x = y )$. Others? $\endgroup$ – user642796 Mar 26 '13 at 13:47
  • $\begingroup$ @TobiasKildetoft Some element $y$ such that $x\ S\ y$. $\endgroup$ – dtldarek Mar 26 '13 at 13:49
  • $\begingroup$ The statement "any theorem of PA cannot be false" isn't quite right; did you mean "no theorem of PA is disprovable"? $\endgroup$ – Carl Mummert Mar 26 '13 at 13:53
  • 1
    $\begingroup$ You are proposing to weaken the accepted axioms of first-order logic with equality, never mind PA, (see en.wikipedia.org/wiki/First-order_logic#Equality_and_its_axioms). Your question isn't really answerable unless you make it precise what your axiomatization of PA is and which axioms you propose to drop. $\endgroup$ – Rob Arthan Mar 26 '13 at 14:22

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.

  • $\begingroup$ The last axiom is precisely the thing I want to drop. Thank you for your "big" comment ;-) $\endgroup$ – dtldarek Mar 26 '13 at 17:14
  • $\begingroup$ I have extended my answer to allow for that. By the way, did you intend to have an axiom saying that every element is either 0 or has a predecessor? $\endgroup$ – Rob Arthan Apr 3 '13 at 8:46
  • $\begingroup$ I think there's no need. Take $\Phi(x) \equiv x=0\vee \exists y.y\prec x$ in the induction schema. $\endgroup$ – MJD Apr 3 '13 at 14:26
  • $\begingroup$ I actually meant to reply to the OP's comment on my answer, but I missed! @MJD: you are quite right that the induction principle implies every non-zero element has a predecessor, thank you. $\endgroup$ – Rob Arthan Apr 4 '13 at 9:08

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

  • $\begingroup$ I know this scheme, and if the converse would be true I wouldn't be asking this question. Here $a=b$ does not imply $s(a) = s(b)$ (using small notation abuse), this is the essential difference. My question is about, what kind of structure it is and if it was studied before. $\endgroup$ – dtldarek Apr 1 '13 at 19:56

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.