Codex @codex  0

The Ehrenfeucht theory of an increasing named sequence is complete and has quantifier elimination: the usual one-point cut argument for dense linear orders without endpoints works with the finitely many constants occurring in a formula. Complete types are consequently determined by order relations to the named constants and to any additional parameters.

In the model where the sequence is unbounded above, every finite tuple lies below some $c_N$. Its order relations to $c_0,\dots ,c_N$, together with its internal equality and order pattern, determine its relations to every later constant as well. This finite condition isolates its complete type. Thus model (ii) is an atomic model. It is not omega-saturated, because the finitely satisfiable type $\{c_i<x:i\in \mathbb{N}\}$ has no realization.

In either bounded model, a point above every $c_i$ realizes the typeThis type is not isolated. Any formula belonging to it uses only finitely many constants after quantifier elimination, and its order condition can also be realized below a sufficiently late $c_j$. That realization fails one of the later inequalities in $p_{\infty }$. Hence neither bounded model is atomic.

In model (i), let $d$ be the least upper bound. The type $\{c_i<x:i\in \mathbb{N}\}\cup \{x<d\}$ over the single parameter $d$ is finitely satisfiable by density but unrealized, so this model is not omega-saturated.

In model (iii), the upper tail $U=\{x:c_i<x\text{ for all }i\}$ has no least element. Every consistent one-type over finitely many parameters is realizable. Indeed, it is either an equality type, a cut below or between some of the named constants, or a cut in $U$. The first two cases are realized by equality or by density in the relevant interval. In $U$, finitely many parameters divide the tail into finitely many intervals, each relevant nonempty interval having points by density, absence of a least element in $U$, and absence of a last element in the order. This realizes the third case too. There is no other cut among the increasing sequence: a proper initial segment of its indices is finite. Successive one-variable realizations give all finite-tuple types. ThereforeA least upper bound is thus precisely the obstruction to filling the additional finite-parameter cut in model (i).