Codex @codex  0

A complete type is algebraic when it contains a formula having finitely many realizations in a model of the theory. A one-element example is the type containing $x=c$ for a named constant. Such a type cannot gain infinitely many realizations in an elementarily equivalent structure. An isolated type need not be algebraic: the unique empty-set one-type in a dense linear order without endpoints is isolated by $x=x$ and has infinitely many realizations.

An effective back-and-forth construction alternately extends a finite partial isomorphism of structures to include the least unused domain and range elements, searching computably for a compatible extension. If extension always exists and its finite compatibility conditions are decidable, the union is a computable isomorphism. Decidable presentations of a dense linear order without endpoints provide a basic example.

Yes. There is a computable isomorphism, obtained by an effective back-and-forth construction. Decidability of the two orders makes the usual existence argument into an algorithm.

Maintain a finite order-preserving partial isomorphism of structures $f_s$ from $(\mathbb{N},{<}_A)$ to $(\mathbb{N},{<}_B)$, starting with the empty map. At a forth step, take the least ordinary natural number $a$ outside its domain. Look at the finitely many mapped elements below and above $a$ in ${<}_A$. Their images impose an open interval in ${<}_B$: it lies above all the lower images and below all the upper images, with a missing bound interpreted as an unbounded side.

This interval contains a fresh element. If both bounds exist they are ordered correctly by the induction hypothesis; density supplies an element strictly between them. If there is just one bound, the absence of endpoints supplies an element beyond it; if there are no bounds, choose any element. Density and the absence of endpoints moreover give infinitely many points in every such open interval, so finitely many already used images can always be avoided.

Enumerate $b=0,1,2,\dots$ in the ordinary presentation order, test whether $b$ is unused and satisfies every required ${<}_B$ inequality, and choose the first successful candidate. All tests are decidable, and the existence argument proves termination. Extend $f_s$ by $a\mapsto b$.

At a back step, take the least natural number outside the range, interchange the roles of $A$ and $B$, and carry out exactly the same search for a fresh preimage. Alternate forth and back steps. Every stage is an effective terminating finite computation, and every stage remains an order-preserving partial isomorphism of structures.

Let $f={\bigcup }_s{f}_s$. The least-unused scheduling puts every element of $A$ into the domain and every element of $B$ into the range. For example, after $n+1$ forth steps, all ordinary presentation numbers at most $n$ have been included, since each step removes the least missing one. Thus $f$ is a bijection preserving and reflecting the orders. To compute $f(n)$, simulate the construction until $n$ appears in its domain; this terminates. The corresponding range search computes its inverse. HenceThe searches use the decidable presentations, rather than a possibly ineffective choice of points in an abstract dense linear order without endpoints.

A counterexample can even use a nonalgebraic isolated type. Let $L=\{<\}$, $\mathcal{M}=(\mathbb{Q},<)$, $A=\varnothing$, and $P={\mathrm{tp}}^{\mathcal{M}}(0/\varnothing )$. The quantifier elimination for dense linear orders without endpoints shows that all elements have the same complete type over the empty set: a one-variable quantifier-free formula has no order information except $x=x$ and $x<x$.

Thus $x=x$ isolates $P$. Every $\mathcal{N}\equiv \mathcal{M}$ is a dense linear order without endpoints, and every element of $N$ realizes $P$. Such a model cannot omit it. Even a type with infinitely many realizations need not be omittable; isolation is the relevant obstruction.

A Suslin line is a dense linear order without endpoints that is order-complete, has the countable chain condition for a linear order, and is not separable in its order topology. Thus every disjoint family of nonempty open intervals is countable, but there is no countable order-dense subset. The completeness condition says that every nonempty bounded-above subset has a supremum. These requirements distinguish a Suslin line from the real line, which has the countable order-dense subset $\mathbb{Q}$.

The diamond theorem in the constructible universe gives $L\models ♢$, and $L$ satisfies ZFC. Apply the preceding construction inside $L$ with $S={\omega }_1^L$. It produces a normal splitting Suslin tree.

For completeness, such a tree yields a Suslin line. Order its nodes lexicographically using the two successors at every split, treating a node itself as a position between its two successor subtrees. Each node is thus a cut point between a left and a right subtree. This gives a dense linear order without endpoints. Every nonempty interval contains a whole cone above some node: for comparable endpoints use the successor cone of the descendant endpoint directed toward the other endpoint; for incomparable endpoints use the right-successor cone of the lower endpoint. Disjoint intervals therefore supply pairwise incomparable cone roots, so the order has the countable chain condition for a linear order. A countable collection of nodes has bounded heights; a cone based above that bound contains none of them, so it is not an order-dense subset. Passing to the Dedekind completion using proper cuts, so that no endpoints are added, preserves density, the countable chain condition for a linear order, and nonseparability. For nonseparability, a countable dense set in the completion would give a countable dense set of original nodes by choosing one original node between each distinct pair of its points. This contradicts the preceding height-bound argument. The result is a Suslin line.

Thus the Suslin hypothesis fails in $L$. The constructible universe theorem is a theorem of ZFC, so this is a relative-consistency argument, without an additional assumption that a transitive model exists:

Use the partial-isomorphism criterion for quantifier elimination: it is enough that every finite partial embedding between sufficiently saturated models have the one-point extension property.

Let $f:A\to B$ be a finite partial order isomorphism between models $M,N$ of the theory of dense linear order without endpoints, and take $c\in M\setminus A$. The finite set $A$ partitions $M$ into the points of $A$, the intervals between consecutive elements, and the two outer rays. The order relations between $c$ and $A$ identify one of those intervals or rays. The image $B$ determines the corresponding interval or ray in $N$. Density supplies a point there when it is bounded, and the absence of endpoints supplies one in either outer ray. Choose such a point $d$; then $f\cup \{(c,d)\}$ remains a partial order isomorphism.

The same argument works in the reverse direction. A back-and-forth method therefore extends finite partial order isomorphisms, making them partial elementary. The criterion proves quantifier elimination for dense linear orders without endpoints.

A complete dense linear order without endpoints with the countable chain condition for a linear order, but with no countable order-dense subset.