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.

A model is strongly $\kappa$-homogeneous when every partial elementary map between its subsets of size less than $\kappa$ extends to an automorphism. Here the unqualified expression homogeneous model uses this automorphism extension convention. For finite parameter tuples it says, in particular, that equal complete types can be carried to one another by an automorphism.

A weaker local convention asks only for one-point extensions of small partial elementary maps. A $\kappa$-saturated model always has that local property. If its cardinality is $\kappa$, the back-and-forth method yields the strong version too. For example, order-preserving maps between finite subsets of the rational dense linear order without endpoints extend to automorphisms by back-and-forth.

Yes. The usual order on the rational numbers is strict and linear. Between $a<b$ lies the rational midpoint $(a+b)/2$, and $a-1,a+1$ witness absence of endpoints. Thus it is a dense linear order without endpoints.

Yes. The usual order on the real numbers is strict and linear, midpoints witness density, and translation by $\pm 1$ supplies points on either side. It therefore satisfies the same dense linear order without endpoints axioms.

Yes. The induced order is strict and linear and remains dense. For $0<x<1$, the points $x/2$ and $(x+1)/2$ lie in the domain and are strictly below and above $x$. Hence the open interval is a dense linear order without endpoints.

Use the axioms for a strict dense linear order without endpoints:The first three give strict linear order; the next gives density; the final two exclude endpoints. Domains are nonempty under the adopted first-order semantics, and these axioms force them to be infinite.

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.

In a countable first-order model, the finitely many named constants split the order into the open intervalstogether with the $n$ named points. Each interval is a countable dense linear order without endpoints in its induced order. It is nonempty and infinite by density and the absence of endpoints.

Use Cantor's classification of countable dense linear orders without endpoints: each such interval is isomorphic to the rational order. It follows by a back-and-forth method extending finite increasing partial bijections alternately along enumerations of the two orders. Given two first-order models of ${\mathrm{DLO}}_n$, choose isomorphisms between their corresponding intervals and send each named point to its counterpart. Their union is an increasing bijection preserving all constants, hence an isomorphism in $L_n$.

There are countable first-order models, for example any finite increasing list in the rational order. ThereforeFor $n=0$, the same argument is just the classification theorem for the whole order.

The countable omitting types theorem says that for a consistent theory in a countable language and countably many nonprincipal types of finite arities, there is a countable model omitting all those types. In particular a nonisolated complete type of $T$ can be omitted in a countable model.

Interpret “definable” here as without parameters. If parameters were allowed freely, every infinite structure would have infinitely many definable singleton sets, and the claimed implication would be false even for a dense linear order without endpoints.

Infinitely many distinct parameter-free definable subsets of $A^n$ imply infinitely many complete $n$-types: if there were only $r$ such types, each formula would select a subset of those $r$ types, giving at most $2^r$ distinct definable subsets. There must also be a nonisolated complete type. To see this, suppose each complete type $p$ had an isolator ${\theta }_p$. The family of their basic open sets covers the type space. Its compactness theorem gives a finite subcover, which would account for only finitely many complete types, a contradiction. Equivalently apply logical compactness theorem to $T\cup \{\neg {\theta }_p(c):p\text{ complete}\}$.

Choose a nonisolated type $p$. The omitting types theorem gives a countable model omitting it, while part (d) gives a countable model realizing it. An isomorphism of structures preserves realization of parameter-free types, so these models are not isomorphic. Thus $\boxed{T\text{ is not }{\aleph }_0\text{-categorical}}$.

An atomic model is a model in which every finite tuple realizes an isolated complete type over the empty set. For a complete theory in a countable language, every countable atomic model is prime. The underlying argument is a back-and-forth method in the one-sided form needed for an embedding: enumerate the atomic model, and extend a finite partial elementary map one element at a time using an isolating formula for the enlarged tuple. The target model has the required witness because the already matched tuple has the same complete type.

Thus property (iii) implies property (iv). It need not imply pointwise definability or term-generation. The countable dense linear order without endpoints with a single named point, for example $(\mathbb{Q},<,0)$, is atomic: quantifier elimination for dense linear orders without endpoints isolates a tuple by its finite order-and-equality pattern relative to zero. But order structure automorphisms fixing zero move every nonzero rational. Such elements are not parameter-free definable, and no closed term names them. This supplies the failed implications (iii)$\nRightarrow$(ii) and (iii)$\nRightarrow$(i).

Yes. The pure order on the reals is a dense linear order without endpoints and has quantifier elimination for dense linear orders without endpoints. Over a finite parameter set $a_1<\cdots <a_m$, a complete one-variable type either specifies equality to one of these points or specifies one of the open intervals and exterior rays they determine.

Each such interval or ray contains a real number. Hence every complete one-variable type over a finite parameter set is realized. The successive-coordinate characterization gives saturation for all finite tuples. This uses finite parameter sets; it does not say that arbitrary types over a countably infinite set of parameters are realized.

Every element of a pointwise definable model is uniquely specified by a formula with no added parameters. Finite tuples are then uniquely specified by conjunctions of their defining formulas. For a complete theory these formulas isolate the tuple types, so such a model is an atomic model. The converse fails: a countable dense linear order without endpoints with a named point is atomic, while its other points are moved by structure automorphisms fixing that point.

A complete theory $T$ is $\kappa$-stable, for an infinite cardinal $\kappa \ge |T|$, when $|S_1(A)|\le \kappa$ for every parameter set $A$ of cardinality $\kappa$ in a model of $T$. Here $S_1(A)$ is the type space of complete one-variable types. The theory is stable if this holds for some such $\kappa$; it is omega-stable if it holds for ${\aleph }_0$.

For the theory of an infinite set with equality alone, a type over $A$ either names one element of $A$ or says that it differs from every member of $A$. There are only $|A|+1$ possibilities. By contrast, a dense linear order without endpoints has the order property, producing many types corresponding to cuts and hence instability. Stability measures the number of ways a new element can relate to existing parameters, rather than simply the number of models.

A complete theory with infinite models is strongly minimal when, in every model, each definable subset in one variable, with parameters allowed, is finite or cofinite. The requirement applies to all models and all parameter choices. The infinite-universe condition excludes trivial finite theories.

For an infinite set in the language of equality, a one-variable formula with finitely many parameters can only distinguish those named elements from the remaining elements, so every definable subset is finite or cofinite. In an algebraically closed field, quantifier elimination likewise makes every one-variable definable subset finite or cofinite, since a nonzero polynomial has finitely many roots. A dense linear order without endpoints fails this property: a proper open interval and its complement are both infinite. Strong minimality is a particularly restrictive source of omega-stability.

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