
Can L(<) be the language of the naturals?
Posted:
Sep 1, 2013 12:27 PM


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 Nampositive or Namnegative.
If I say that I have a set with a semiinfinite, discrete, linear order, (N, <), is that enough to define the naturals?
Specifically, if I say
Ax Ay Az (x<y)&(y<z) > (x<z)
Ax Ay ( (x<y) > (~ x=y)&(~ y<x) ) & ( (x=y) > (~ x<y)&(~ y<x) ) & ( (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 wellknown 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?

