Does the side of the successor function in the second postulate of the definition of addition matter?

Question

In Peano arithmetic addition is usually defined with the following two postulates:

$(1a):p + 0 = p$

$(2a):p + S(q) = S(p+q)$

Lets say I put the successor term of the second postulate on the left? Namely:

$(1b):p + 0 = p$

$(2b): S(p) + q = S(p+q)$

Are these two definitions of addition equivalent?

Answer 1

Logically perhaps. But note that it is clear that the first set (a) is consistent: the right-side addend is either $0$ or a successor, so at most one clause applies in every situation.

This is not the case for the second set (b), where there are additions to which both clauses apply and you will have to decide which one you will use. For example, consider $S(t)+0$. The first clause says that this should be reduced to $S(t)$. The second clause says that it should be reduced to $S(t+0)$. Now it is true if we kept on reducing, we would eventually get to the same place, $S(t)$, regardless of which steps we took. But to be certain that your definition makes sense, you would need an induction proof that shows that there is no reduction for any initial expression where the result depends on the particular steps taken. (This property is called “confluence”; without it we can't really say that an expression has a well-defined ‘value’.)

With (a) there are never any choices so no such proof is needed. At most one rule applies to every expression, you apply the one rule until there is no longer a $+$ sign and you have to stop.

As the comment says, you should probably change (1b) to say $0+p=p$ for this reason.

Answer 2

Well, they are certainly not logically equivalent: without making any further assumptions/axioms, you cannot derive the one from the other.

Now, if you include the axiom of induction, then you can derive the second definition from the first… but I am not sure if you can derive the first from the second even if you have the inductive axiom.

I do know that if you have the axiom of induction, you can derive the following pair of statements from the first definition:

$0+p=p$

$s(p) +q=s(p+q)$

and from this pair, you can derive the first pair using induction. So, within the context of the inductive axiom, those two pairs are equivalent.