Without referring to the apparatus of (primitive) recursive functions one can introduce addition into the language of successor arithmetic by two additional axioms which naturally reflect the essence of recursion:
- $(\forall n)\ n + 0 = n$
- $(\forall n, m)\ n+ m' = (n+m)'$
When we already have addition, it is easy to re-define $<$ explicitely:
- $n < m :\equiv (\exists x \neq 0)\ n + x = m$
I wonder if the following is a sound recursive definition of $<$ only using the successor function:
- $(\forall n)\ n < n'$
- $(\forall n,m)\ n < m \rightarrow n < m'$
Other than the usual recursive definitions this one does not involve $0$, but it seems to work anyway. A proof that $0 < 2$ (with $2=1'=0''$) goes like this: Assume that $\neg(0 < 2)$. Since $\neg(n < m') \rightarrow \neg(n < m)$ it follows $\neg(0 < 0')$. Contradiction.
Note that the successor function could in turn be re-defined explicitely by the given relation $<$:
- $m = n' :\equiv n < m \wedge \neg(\exists x)\ n < x < m$
I'd like to drive this further: Before defining multiplication (recursively) I'd like to define the intermediate relation $n \mid m$ ("$n$ divides $m$") and function $n\bmod m$ ("the remainder of $n$ divided by $m$") in a similar recursive fashion as $n < m$, especially without using multiplication (only addition).
The $n\mid m$ case seems easy:
- $(\forall n \neq 0)\ n \mid n$
- $(\forall n \neq 0,m \geq n)\ n \mid m \rightarrow n \mid (m + n)$
But I get stuck trying to define $n\bmod m$ in a similar fashion. Other than $n<m$ and $n\mid m$ it is a function, not a relation, but it should be possible, shouldn't it?
Any hint is welcome.
[Addendum]
Supposed that $n \bmod m$ can be defined by additional axioms in a recursive fashion, can addition be re-defined explicitely by $\bmod$ - just like the successor function can be re-defined explicitely by $<$?
Maybe it's easier than I thought it is?