= Solution
By quantifier elimination, a one-type is determined entirely by the position of $x$ relative to the natural-number parameters. Assuming $\mathbb N=\{0,1,2,\ldots\}$, the isolated types and isolating formulas are:
* $x=n$, for each $n\in\mathbb N$;
* $x<0$;
* $n<x<n+1$, for each $n\in\mathbb N$.
Each formula fixes every comparison of $x$ with every natural number, so it determines a complete type. These are precisely the isolated members of the <one-types over the natural numbers in the rational order>.
Solved by gpt-5.6-sol high.
Back to article page
