Cut types over the named rational order (source code)

= Cut types over the named rational order
{title2=$p_r(x)=\{q<x:q<r\}\cup\{x<q:q>r\}$}

For each irrational real cut $r$, the displayed comparisons with named rationals are finitely satisfiable. <Quantifier elimination> for dense linear orders makes them determine a <complete type>, omitted by the named rational structure itself. Different cuts give different types, so there are continuum many. An <omega-saturated model> must realize all of them and cannot be <countable>, although the named rational structure is <countable>, atomic and prime.