One-types over the natural numbers in the rational order (source code)

= One-types over the natural numbers in the rational order
{title2=$S_1^{(\mathbb Q,<)}(\mathbb N)$}

Quantifier elimination for dense linear orders shows that the one-types over $\mathbb N\subset\mathbb Q$ are determined by cuts: equality to a natural number, one of the intervals between consecutive natural numbers, the ray below zero, or the cut above every natural number. Only the last type is non-isolated.