[proofplan] We prove quantifier elimination syntactically by showing that one existential quantifier can always be removed from a quantifier-free formula. Since the language $\{<\}$ has no function symbols and no constant symbols, atomic formulas only compare variables by $<$ or equality. After putting a quantifier-free formula into disjunctive normal form, each existential conjunct says that the quantified variable is equal to a parameter, lies above finitely many parameters, lies below finitely many parameters, and satisfies finitely many parameter-only order constraints. The density and no-endpoints axioms of $\operatorname{DLO}$ exactly guarantee that every consistent finite open interval condition is realised, so the existential quantifier is equivalent to a quantifier-free finite conjunction of inequalities among the parameters. [/proofplan] [step:Reduce quantifier elimination to eliminating one existential quantifier from a conjunction] It suffices to prove the following elimination step: for every quantifier-free $\mathcal{L}$-formula $\theta(x,y_1,\dots,y_n)$ there is a quantifier-free $\mathcal{L}$-formula $\theta^\exists(y_1,\dots,y_n)$ such that \begin{align*} \operatorname{DLO} \models \forall y_1 \cdots \forall y_n \, \left(\exists x \, \theta(x,y_1,\dots,y_n) \leftrightarrow \theta^\exists(y_1,\dots,y_n)\right). \end{align*} Indeed, once this is known, an induction on formulas eliminates quantifiers one at a time: Boolean connectives preserve quantifier-free equivalence, and each subformula of the form $\exists x \, \theta$ with $\theta$ already quantifier-free is replaced by $\theta^\exists$. Because the language $\mathcal{L}=\{<\}$ has no function symbols and no constant symbols, the only terms are variables. Hence every atomic formula is of the form $u<v$ or $u=v$, where $u,v$ are variables. Using the axioms of linear order, every negated atomic formula is equivalent over $\operatorname{DLO}$ to a quantifier-free positive formula: \begin{align*} \neg(u<v) &\leftrightarrow (v<u \vee u=v), \\ \neg(u=v) &\leftrightarrow (u<v \vee v<u). \end{align*} Thus every quantifier-free formula is equivalent over $\operatorname{DLO}$ to a finite disjunction of finite conjunctions of atomic formulas of the form $u<v$ or $u=v$. Since existential quantification distributes over finite disjunctions, it remains to eliminate $\exists x$ from one finite conjunction of such atomic formulas. [guided] The reason we isolate a single existential quantifier is that first-order formulas are built recursively. If every formula $\exists x\,\theta$ with $\theta$ quantifier-free can be rewritten without quantifiers, then we can start from the innermost quantifiers of an arbitrary formula and remove them one at a time. In the language $\mathcal{L}=\{<\}$, there are no function symbols and no constant symbols, so there are no complicated terms. A term is just one of the variables. Therefore every atomic formula says either $u<v$ or $u=v$ for variables $u,v$. The negations of these atoms can also be rewritten using only $<$ and equality, because linear orders satisfy trichotomy: \begin{align*} \neg(u<v) &\leftrightarrow (v<u \vee u=v), \\ \neg(u=v) &\leftrightarrow (u<v \vee v<u). \end{align*} After replacing negated atoms this way and distributing $\wedge$ over $\vee$, every quantifier-free formula becomes a finite disjunction of finite conjunctions of atoms. Since \begin{align*} \exists x \, \bigvee_{k=1}^m \alpha_k \leftrightarrow \bigvee_{k=1}^m \exists x \, \alpha_k, \end{align*} it is enough to handle one conjunction of atomic comparisons at a time. [/guided] [/step] [step:Put the conjunctive case into lower bound, upper bound, equality, and parameter-only parts] Let $\Gamma(x,y_1,\dots,y_n)$ be a finite conjunction of atomic formulas of the form $u<v$ or $u=v$. Separate the conjuncts of $\Gamma$ into four types. First, let $E$ be the finite set of indices $i \in \{1,\dots,n\}$ for which the conjunct $x=y_i$ or $y_i=x$ occurs. Second, let $L$ be the finite set of indices $i \in \{1,\dots,n\}$ for which the conjunct $y_i<x$ occurs. Third, let $U$ be the finite set of indices $j \in \{1,\dots,n\}$ for which the conjunct $x<y_j$ occurs. Finally, let $\Pi(y_1,\dots,y_n)$ denote the conjunction of all conjuncts of $\Gamma$ in which $x$ does not occur. Conjuncts $x<x$ make $\Gamma$ inconsistent over $\operatorname{DLO}$, so in that case $\exists x\,\Gamma$ is equivalent to the quantifier-free contradiction $y_1 \neq y_1$. Conjuncts $x=x$ are tautological and may be deleted. Hence assume from now on that no conjunct $x<x$ occurs and all conjuncts $x=x$ have been removed. [/step] [step:Eliminate the existential quantifier when $x$ is forced to equal a parameter] Assume $E \neq \varnothing$, and choose an index $e \in E$. Then $\Gamma$ implies $x=y_e$. Therefore $\exists x\,\Gamma(x,y_1,\dots,y_n)$ is equivalent over $\operatorname{DLO}$ to the quantifier-free formula obtained by substituting $y_e$ for $x$ throughout $\Gamma$: \begin{align*} \Gamma(y_e,y_1,\dots,y_n). \end{align*} More explicitly, the required formula is the conjunction of $\Pi(y_1,\dots,y_n)$ with the following parameter constraints: \begin{align*} y_e &= y_i &&\text{for every } i \in E,\\ y_i &< y_e &&\text{for every } i \in L,\\ y_e &< y_j &&\text{for every } j \in U. \end{align*} Thus the existential quantifier is eliminated in the equality case. [guided] If one conjunct says $x=y_e$, then there is no freedom left in choosing $x$. Any witness for $\exists x\,\Gamma$ must be exactly $y_e$. So the existential statement is true precisely when replacing $x$ by $y_e$ makes every conjunct true. The conjuncts involving only the parameters remain unchanged; their conjunction is $\Pi(y_1,\dots,y_n)$. Every other constraint involving $x$ becomes a constraint involving $y_e$: \begin{align*} x=y_i &\quad\text{becomes}\quad y_e=y_i,\\ y_i<x &\quad\text{becomes}\quad y_i<y_e,\\ x<y_j &\quad\text{becomes}\quad y_e<y_j. \end{align*} Therefore $\exists x\,\Gamma$ is equivalent to the quantifier-free conjunction of these parameter-only formulas. [/guided] [/step] [step:Eliminate the existential quantifier when $x$ is constrained only by a finite cut] Assume $E=\varnothing$. Then the conjuncts involving $x$ say exactly that $x$ must lie above every $y_i$ with $i \in L$ and below every $y_j$ with $j \in U$. Define the quantifier-free formula \begin{align*} \Theta(y_1,\dots,y_n) \end{align*} to be the conjunction of $\Pi(y_1,\dots,y_n)$ with all inequalities \begin{align*} y_i < y_j \qquad (i \in L,\ j \in U). \end{align*} We claim that \begin{align*} \operatorname{DLO} \models \forall y_1 \cdots \forall y_n \, \left(\exists x \, \Gamma(x,y_1,\dots,y_n) \leftrightarrow \Theta(y_1,\dots,y_n)\right). \end{align*} If $M \models \operatorname{DLO}$ and $a,b_1,\dots,b_n \in M$ satisfy $\Gamma(a,b_1,\dots,b_n)$, then $\Pi(b_1,\dots,b_n)$ holds, and for every $i \in L$ and $j \in U$ we have $b_i<a<b_j$. By transitivity of $<$, $b_i<b_j$. Hence $M \models \Theta(b_1,\dots,b_n)$. Conversely, suppose $M \models \operatorname{DLO}$ and $b_1,\dots,b_n \in M$ satisfy $\Theta$. We construct $a \in M$ satisfying all lower and upper bounds. If $L=\varnothing$ and $U=\varnothing$, choose any $a \in M$, using nonemptiness of models of $\operatorname{DLO}$. If $L=\varnothing$ and $U \neq \varnothing$, choose $j_0 \in U$; since $M$ has no left endpoint, there is $a \in M$ with $a<b_{j_0}$. Then $a<b_j$ for every $j \in U$ after replacing $a$ by an element below the finite minimum of $\{b_j:j\in U\}$, obtained by finite induction using linearity. The case $L \neq \varnothing$ and $U=\varnothing$ is symmetric, using absence of right endpoints. Finally, if $L \neq \varnothing$ and $U \neq \varnothing$, let $b_\ell$ be a maximum of the finite set $\{b_i:i\in L\}$ and let $b_u$ be a minimum of the finite set $\{b_j:j\in U\}$, both chosen by finite induction using linearity. Since $\Theta$ contains $b_\ell<b_u$, density gives $a \in M$ such that $b_\ell<a<b_u$. Then $b_i<a$ for all $i \in L$ and $a<b_j$ for all $j \in U$. Together with $\Pi(b_1,\dots,b_n)$, this gives $M \models \Gamma(a,b_1,\dots,b_n)$. [guided] In the case $E=\varnothing$, the variable $x$ is not forced to equal any parameter. It only has to realise a finite cut: \begin{align*} y_i < x \quad (i \in L), \qquad x < y_j \quad (j \in U). \end{align*} For such an $x$ to exist, every lower bound must lie below every upper bound. This gives the parameter-only condition \begin{align*} y_i<y_j \qquad (i\in L,\ j\in U). \end{align*} Together with the parameter-only part $\Pi$, this is the formula $\Theta$. First suppose $a$ is an actual witness. Then for each $i\in L$ and $j\in U$, \begin{align*} b_i<a<b_j. \end{align*} By transitivity of the order, $b_i<b_j$. Thus every inequality required by $\Theta$ holds, and the parameter-only part $\Pi$ also holds because it was already part of $\Gamma$. Conversely, assume the parameter tuple satisfies $\Theta$. We must find a point $a$ in the correct finite cut. There are four cases. If there are no lower and no upper bounds, any element of $M$ works, using the nonemptiness axiom. If there are only upper bounds, the finite set $\{b_j:j\in U\}$ has a minimum by induction on its size using linearity of $<$. Since $M$ has no left endpoint, choose $a$ below that minimum. Then $a$ is below every upper bound. If there are only lower bounds, the finite set $\{b_i:i\in L\}$ has a maximum by the same finite induction, and absence of right endpoints gives an $a$ above that maximum. The remaining case has both lower and upper bounds. Let $b_\ell$ be the maximum of the finite lower-bound set $\{b_i:i\in L\}$ and let $b_u$ be the minimum of the finite upper-bound set $\{b_j:j\in U\}$. Since $\Theta$ includes $b_i<b_j$ for every $i\in L$ and $j\in U$, in particular \begin{align*} b_\ell < b_u. \end{align*} Density of the order gives an element $a\in M$ with \begin{align*} b_\ell<a<b_u. \end{align*} Because $b_\ell$ is above every lower bound and $b_u$ is below every upper bound, this $a$ satisfies every conjunct $b_i<a$ and every conjunct $a<b_j$. Combining these with $\Pi(b_1,\dots,b_n)$ gives $M\models \Gamma(a,b_1,\dots,b_n)$. [/guided] [/step] [step:Conclude quantifier elimination for all formulas] The previous steps show that for every finite conjunction $\Gamma$ of atomic $\mathcal{L}$-formulas, the formula $\exists x\,\Gamma$ is equivalent over $\operatorname{DLO}$ to a quantifier-free formula. Since every quantifier-free formula is equivalent over $\operatorname{DLO}$ to a finite disjunction of such conjunctions, every existential quantification of a quantifier-free formula can be eliminated. By induction on the number of quantifiers in an arbitrary $\mathcal{L}$-formula, every formula is equivalent over $\operatorname{DLO}$ to a quantifier-free formula. Therefore $\operatorname{DLO}$ has quantifier elimination in the language $\{<\}$. [/step]