There was some discussion recently of various subsets of "the language of arithmetic" (scare quotes because I'm not very familiar with all this). This question is part of that one, I suppose, except that I am not interested in whether the definitions are Nam-positive or Nam-negative.
If I say that I have a set with a semi-infinite, discrete, linear order, (N, <), is that enough to define the naturals?
Specifically, if I say
Ax Ay Az (x<y)&(y<z) -> (x<z)
[Second try:] Ax Ay ( (x<y)&(~ x=y)&(~ y<x) ) V ( (x=y)&(~ x<y)&(~ y<x) ) V ( (y<x)&(~ x<y)&(~ x=y) )
Ax Ay ( x < y ) -> ( Ez( ( x < z =< y ) & ~Ew( x < w < z ) ) )
Ax Ay ( x < y ) -> ( Ez( ( x =< z < y ) & ~Ew( z < w < y ) ) )
Ex Ay ( x =< y )
~Ex Ay ( y =< x )
(where there is no important difference between having a lower bound and no upper bound or vice versa), then it looks like I can define 0 and S and prove their necessary properties -- except possibly for induction.
x = 0 <-> Ay ( x =< y )
Sx = y <-> (x<y) & ~Ez( x < z < y )
E!x ( x = 0 )
Ax E!y ( Sx = y )
~Ex ( Sx = 0 )
Ax Ay ( Sx = Sy ) -> ( x = y )
I suspect that this is well-known among those who know it well.
Is this right?
Is there a better way of putting it?
Is this enough to make induction available? If not, what would I need to add in order to be able to support induction as well?