I am stuck proving the simple claim that $Sx \neq 0$ in say Peano Arithmetic (the first order theory of arithmetic) or Robinson Arithmetic or Presburger Arithmetic. I see that this is sometimes added as an axiom, but it seems not necessary (i.e. derivable)?
Assume we have quantifier-free induction (or at least the axiom that every number is either 0 or a successor).
I have already tried using induction along $A[x] := Sx = 0$, but the induction hypothesis $Sx \neq 0$ doesn't help me with $SSx \neq 0$.
NB. I am familiar with a system called PRA where in addition to the usual axioms of robinson arithmetic, we have quantifier free induction and function symbols of all primitive recursive functions plus their defining equations.
That means that
$isz(0) = 0$
$isz(Sx) = S0$
is an axiom of PRA. Here I can easily derive a contradiction if I assume $Sx = 0$:
$S0 = isz(Sx) = isz(0) = 0$, contradicts the axiom $S0 \neq 0$.
Maybe I can do something similar with +, which I have in the theories mentioned above, but I had no success so far.
$\forall x \in N :S(x)\ne 0$ (or some equivalent) is always given as one of Peano's axioms.
If instead, you had simply $S(0)\ne 0$ as you suggest, then your axioms would be satisfied by having $N=\{0,1\}, 0\ne 1, S(0)=1$ and $S(1)=0$. In any case, you would not be able to prove $\forall x \in N :S(x)\ne 0$ since it would not be strictly required by your axioms.