proof by induction that every non-zero natural number has a predecessor

I am trying to prove by induction that every non-zero natural number has at least one predecessor. However, I don't know what to use as a base case, since 0 is not non-zero and I haven't yet established that 1 is the number following zero.

My axioms are:

1. $0$ is a natural number.


2. if $b$ is a natural number then $S(b)$ is also a natural number.


3. $0$ is not a successor of any natural number.



4. different numbers have different successors.

Any advice?

Answer

The fact that every number is either 0 or a successor follows almost embarrassingly quickly from induction on the predicate
$$P(x) \equiv (x = 0 ) \lor (\exists y)[x = S(y)].$$

Clearly $P(0)$ holds. Also $P(S(y))$ holds for all $y$, so $(\forall y)[P(y) \to P(S(y))]$ also holds. Now apply induction.

As you can see, the only axiom that is required here is the induction axiom for $P(x)$, along with usual first-order logic. The numerical axioms of $PA^{-}$ are entirely irrelevant.