[proofplan] We first use [quantifier elimination for dense linear orders without endpoints](/theorems/4273) to replace the defining formula by a Boolean combination of atomic order comparisons involving $x$ and the named parameters. We then list the distinct parameters in increasing order; these parameters cut the order into finitely many singleton parameter cells and finitely many open convex interval cells. On each open cell, every comparison between $x$ and a parameter has a constant truth value, so the whole Boolean combination is constant there. The definable set is therefore the union of exactly those cells on which the formula is true. [/proofplan]

[step:Replace the formula by a Boolean combination of parameter comparisons]By [quantifier elimination for dense linear orders](/theorems/4305) without endpoints (citing a result not yet in the wiki: Quantifier Elimination for Dense Linear Orders without Endpoints), the formula $\varphi(x,a_1,\dots,a_n)$ is equivalent in $\mathcal{M}$ to a quantifier-free $\mathcal{L}_{<}$-formula $\psi(x,a_1,\dots,a_n)$. Since $\mathcal{L}_{<}$ has only the binary relation symbol $<$ and equality, every atomic formula appearing in $\psi$ is one of the forms \begin{align*} x<a_i, \qquad a_i<x, \qquad x=a_i, \qquad a_i<a_j, \qquad a_i=a_j, \qquad x=x, \qquad x<x \end{align*} for indices $i,j \in \{1,\dots,n\}$. The formulas involving no genuine comparison between $x$ and a parameter, namely $a_i<a_j$, $a_i=a_j$, $x=x$, and $x<x$, have fixed truth values in $\mathcal{M}$: the first two because the parameters are fixed, $x=x$ because equality is reflexive, and $x<x$ because $<$ is irreflexive. Hence $\psi(x,a_1,\dots,a_n)$ determines the same subset of $M$ as a Boolean combination of formulas of the forms \begin{align*} x<a_i, \qquad a_i<x, \qquad x=a_i. \end{align*}[/step]

[guided]The model-theoretic input is quantifier elimination for dense linear orders without endpoints: every formula in the language $\{<\}$ is equivalent, in every dense linear order without endpoints, to a quantifier-free formula. Applying this to $\varphi(x,a_1,\dots,a_n)$ gives a quantifier-free formula $\psi(x,a_1,\dots,a_n)$ defining the same subset of $M$. Now we inspect what quantifier-free formulas can say. The language has no function symbols and no constant symbols except the named parameters we have inserted. Therefore, once the parameters $a_1,\dots,a_n$ are fixed, the atomic formulas involving the variable $x$ are comparisons between $x$ and one of the parameters, together with the two parameter-free-in-effect formulas $x=x$ and $x<x$: \begin{align*} x<a_i, \qquad a_i<x, \qquad x=a_i, \qquad x=x, \qquad x<x. \end{align*} The formulas $x=x$ and $x<x$ have fixed truth values in a linear order: $x=x$ is always true, and $x<x$ is always false because $<$ is irreflexive. Atomic formulas involving only parameters, such as $a_i<a_j$ or $a_i=a_j$, also do not depend on $x$. Since the parameters are already fixed elements of $M$, each such formula is either always true or always false. Replacing these fixed-truth-value atoms by their truth values leaves a Boolean combination whose $x$-dependence comes only from comparisons of $x$ with the named parameters.[/guided]

[step:Partition the order into finitely many parameter cells]Let \begin{align*} C := \{a_1,\dots,a_n\} \subset M. \end{align*} Write the distinct elements of $C$ in increasing order as \begin{align*} c_1 < c_2 < \cdots < c_m, \end{align*} where $m \in \mathbb{N} \cup \{0\}$. If $m=0$, set $\mathcal{P}:=\{M\}$. If $m\geq 1$, define the finite family of cells $\mathcal{P}$ by \begin{align*} \mathcal{P} := \{(-\infty,c_1)\} \cup \{\{c_j\}:1\leq j\leq m\} \cup \{(c_j,c_{j+1}):1\leq j<m\} \cup \{(c_m,\infty)\}. \end{align*} These cells are pairwise disjoint and their union is $M$.[/step]

[guided]The parameters are the only possible endpoints of the final decomposition, so we isolate them first. Let \begin{align*} C := \{a_1,\dots,a_n\}. \end{align*} Because the tuple of parameters is finite, the set $C$ is finite. Remove repetitions and write the resulting distinct elements in increasing order: \begin{align*} c_1<c_2<\cdots<c_m. \end{align*} These ordered parameters cut the linear order into the singleton cells $\{c_j\}$ and the open regions between or beyond them: \begin{align*} (-\infty,c_1), \qquad (c_j,c_{j+1}), \qquad (c_m,\infty). \end{align*} If there are no parameters, meaning $m=0$, then there is only one cell, namely $M$ itself. If $m\geq 1$, the family \begin{align*} \mathcal{P} := \{(-\infty,c_1)\} \cup \{\{c_j\}:1\leq j\leq m\} \cup \{(c_j,c_{j+1}):1\leq j<m\} \cup \{(c_m,\infty)\} \end{align*} is finite. The linear order property implies that every element of $M$ lies in exactly one of these cells: it is either equal to one of the listed parameters, below the first one, above the last one, or strictly between two consecutive listed parameters.[/guided]

[step:Show that the formula has constant truth value on each open cell]Let $P \in \mathcal{P}$ be one of the open interval cells, so $P$ is one of $(-\infty,c_1)$, $(c_j,c_{j+1})$ for some $1\leq j<m$, $(c_m,\infty)$, or $M$ in the case $m=0$. For any two elements $b,b' \in P$ and any parameter $a_i$, the three formulas \begin{align*} x<a_i, \qquad a_i<x, \qquad x=a_i \end{align*} have the same truth values at $x=b$ and at $x=b'$. Therefore every Boolean combination of these formulas, in particular $\psi(x,a_1,\dots,a_n)$, has the same truth value at $b$ and $b'$. Thus either $P \subset X$ or $P \cap X=\varnothing$.[/step]

[guided]Fix an open interval cell $P$. The reason for using these cells is that every element of $P$ has the same relative order with respect to each parameter. For example, if $P=(c_j,c_{j+1})$, then every $b\in P$ is greater than precisely the parameters among $c_1,\dots,c_j$ and less than precisely the parameters among $c_{j+1},\dots,c_m$. Also, no element of $P$ is equal to any parameter. The same description applies to $(-\infty,c_1)$ and $(c_m,\infty)$, with the evident modifications. Hence, for any two elements $b,b'\in P$ and every index $i\in\{1,\dots,n\}$, the atomic formulas \begin{align*} x<a_i, \qquad a_i<x, \qquad x=a_i \end{align*} have identical truth values when $x=b$ and when $x=b'$. Boolean operations preserve equality of truth values: if the inputs to a Boolean combination agree, then the output agrees. Since $\psi$ is such a Boolean combination, $\mathcal{M}\models \psi(b,a_1,\dots,a_n)$ if and only if $\mathcal{M}\models \psi(b',a_1,\dots,a_n)$. Because $\psi$ defines the same set as $\varphi$, either the whole cell $P$ is contained in $X$ or no point of $P$ belongs to $X$.[/guided]

[step:Handle singleton parameter cells]For each singleton cell $\{c_j\}$ with $1\leq j\leq m$, either \begin{align*} \mathcal{M}\models \psi(c_j,a_1,\dots,a_n) \end{align*} or not. In the first case $\{c_j\}\subset X$, and in the second case $\{c_j\}\cap X=\varnothing$.[/step]

[guided]It remains to check the cells that consist of a single parameter value. Fix an index $j\in\{1,\dots,m\}$. The singleton cell $\{c_j\}$ has only one element, so there is no constancy argument to prove across multiple points. The quantifier-free formula $\psi$ either holds at that element or it does not: \begin{align*} \mathcal{M}\models \psi(c_j,a_1,\dots,a_n) \end{align*} or \begin{align*} \mathcal{M}\not\models \psi(c_j,a_1,\dots,a_n). \end{align*} Because $\psi$ defines the same subset $X\subset M$ as the original formula $\varphi$, the first alternative says exactly that $c_j\in X$, hence $\{c_j\}\subset X$. The second alternative says exactly that $c_j\notin X$, hence $\{c_j\}\cap X=\varnothing$.[/guided]

[step:Assemble the selected cells into the required finite union] Let $\mathcal{Q}$ be the subfamily of $\mathcal{P}$ consisting of all cells $P$ such that $P\subset X$. The preceding steps show that every cell in $\mathcal{P}$ is either contained in $X$ or disjoint from $X$. Since $\mathcal{P}$ partitions $M$, we have \begin{align*} X=\bigcup_{P\in\mathcal{Q}} P. \end{align*} The family $\mathcal{Q}$ is finite, and each of its members is either a singleton $\{c_j\}$ with $c_j\in\{a_1,\dots,a_n\}$ or an interval of one of the forms \begin{align*} (-\infty,c_1), \qquad (c_j,c_{j+1}), \qquad (c_m,\infty), \qquad M. \end{align*} Thus $X$ is a finite union of points and intervals with endpoints among the named parameters, together with possible unbounded intervals. This proves the theorem. [/step]