[proofplan] We prove quantifier elimination for $\operatorname{DLO}$ directly. The key point is that an existential condition on one variable in a dense linear order without endpoints is determined entirely by the relative positions of its lower and upper parameter bounds. Once every formula is equivalent modulo $\operatorname{DLO}$ to a quantifier-free formula, every sentence is equivalent to a quantifier-free sentence with no variables; since the language $\{<\}$ has no constant symbols, such a sentence has a fixed truth value in every model. This gives completeness. [/proofplan]

[step:Reduce completeness to quantifier elimination for $\operatorname{DLO}$]We first show that every $\mathcal{L}$-formula is equivalent modulo $\operatorname{DLO}$ to a quantifier-free $\mathcal{L}$-formula. Assuming this, let $\varphi$ be an $\mathcal{L}$-sentence. Then there is a quantifier-free sentence $\psi$ such that \begin{align*} \operatorname{DLO} \models \varphi \leftrightarrow \psi. \end{align*} Because $\mathcal{L} = \{<\}$ has no constant symbols, there are no closed terms. Hence there are no atomic $\mathcal{L}$-sentences of the forms $t = s$ or $t < s$. Therefore a quantifier-free sentence is a Boolean combination of no atomic sentences, and so is logically equivalent to either $\top$ or $\bot$. Thus every model of $\operatorname{DLO}$ satisfies the same truth value for $\varphi$. Equivalently, either $\operatorname{DLO} \models \varphi$ or $\operatorname{DLO} \models \neg \varphi$.[/step]

[guided]The reason quantifier elimination implies completeness here is special to the language. If there were constant symbols, then a quantifier-free sentence could still say something nontrivial about those constants. In the language $\mathcal{L} = \{<\}$, however, the only terms are variables. A sentence has no free variables, so after eliminating quantifiers there are no terms left from which to form atomic sentences. Formally, suppose every $\mathcal{L}$-formula is equivalent over $\operatorname{DLO}$ to a quantifier-free formula. Given an $\mathcal{L}$-sentence $\varphi$, choose a quantifier-free sentence $\psi$ with \begin{align*} \operatorname{DLO} \models \varphi \leftrightarrow \psi. \end{align*} Since $\psi$ has no free variables and the language has no constant symbols, $\psi$ contains no atomic formulas. Therefore $\psi$ is just a propositional truth value built from $\top$, $\bot$, and Boolean connectives. It is logically equivalent to either $\top$ or $\bot$. Hence every model of $\operatorname{DLO}$ gives $\varphi$ the same truth value, which is exactly completeness.[/guided]

[step:Put the matrix of one existential formula into a finite disjunction of conjunctions of literals]Let $\theta(x, y_1,\dots,y_n)$ be a quantifier-free $\mathcal{L}$-formula, where $x,y_1,\dots,y_n$ are variables. By propositional disjunctive normal form, $\theta$ is logically equivalent to a finite disjunction \begin{align*} \bigvee_{r=1}^m \Theta_r(x,y_1,\dots,y_n), \end{align*} where each $\Theta_r$ is a finite conjunction of literals, and each literal is one of \begin{align*} u = v,\qquad u \neq v,\qquad u < v,\qquad \neg(u < v), \end{align*} with $u,v \in \{x,y_1,\dots,y_n\}$. Therefore \begin{align*} \exists x\,\theta(x,y_1,\dots,y_n) \end{align*} is equivalent to the finite disjunction of the formulas $\exists x\,\Theta_r(x,y_1,\dots,y_n)$. It is enough to eliminate $x$ from one such conjunction.[/step]

[guided]We first reduce the quantifier-elimination problem to the case where the matrix is a conjunction of simple atomic or negated atomic conditions. Let $\theta(x,y_1,\dots,y_n)$ be a quantifier-free $\mathcal{L}$-formula. Since $\theta$ is built from atomic formulas using Boolean connectives, propositional disjunctive normal form gives a logically equivalent finite disjunction \begin{align*} \bigvee_{r=1}^m \Theta_r(x,y_1,\dots,y_n), \end{align*} where each $\Theta_r$ is a finite conjunction of literals. In the language $\mathcal{L}=\{<\}$, the atomic formulas are exactly $u=v$ and $u<v$ for variables $u,v\in\{x,y_1,\dots,y_n\}$, so the possible literals are \begin{align*} u = v,\qquad u \neq v,\qquad u < v,\qquad \neg(u < v). \end{align*} Existential quantification distributes over a finite disjunction because an element satisfies at least one disjunct exactly when it witnesses the existential formula for at least one disjunct. Thus \begin{align*} \exists x\,\theta(x,y_1,\dots,y_n) \end{align*} is equivalent to \begin{align*} \bigvee_{r=1}^m \exists x\,\Theta_r(x,y_1,\dots,y_n). \end{align*} Therefore it is enough to eliminate $x$ from a single conjunction of literals; the final quantifier-free formula is obtained by taking the finite disjunction of the resulting quantifier-free formulas.[/guided]

[step:Eliminate equalities involving the quantified variable] Fix one conjunction of literals $\Theta(x,y_1,\dots,y_n)$. First rewrite every equality literal $y_i = x$ as $x = y_i$, and rewrite every disequality literal $y_i \neq x$ as $x \neq y_i$, using symmetry of equality. If $\Theta$ contains a literal $x = y_i$, then \begin{align*} \exists x\,\Theta(x,y_1,\dots,y_n) \end{align*} is equivalent to the quantifier-free formula obtained by substituting $y_i$ for every occurrence of $x$ in $\Theta$. If $\Theta$ contains the literal $x \neq x$ or $x < x$, then it is inconsistent with the strict-order axioms and is equivalent to $\bot$. If it contains $\neg(x=x)$, it is also equivalent to $\bot$. Thus, after splitting into cases when necessary, it remains to handle conjunctions in which no equality literal identifies $x$ with one of the parameter variables. [/step]

[step:Refine negated order literals into lower and upper bound cases] We now remove negated order literals involving $x$. In every strict linear order, trichotomy gives the equivalences \begin{align*} \neg(x < y_i) &\leftrightarrow (x = y_i \vee y_i < x),\\ \neg(y_i < x) &\leftrightarrow (y_i = x \vee x < y_i). \end{align*} For each negated order literal involving $x$, replace it by the corresponding disjunction above and distribute finite conjunction over finite disjunction. This transforms the original conjunction into a finite disjunction of conjunctions. Any resulting disjunct containing an equality $x = y_i$ is eliminated by the substitution argument from the preceding step. Any resulting disjunct containing $x \neq x$ or $x < x$ is inconsistent, and any disjunct containing $\neg(x=x)$ is inconsistent. Therefore it remains to eliminate $x$ from conjunctions in which every literal involving $x$ has one of the forms \begin{align*} y_i < x,\qquad x < y_j,\qquad x \neq y_k. \end{align*} [/step]

[step:Describe the remaining constraints on the quantified variable by lower and upper bounds]After the previous normalization, we may consider a conjunction $\Theta(x,y_1,\dots,y_n)$ in which every remaining literal involving $x$ has one of the forms \begin{align*} y_i < x,\qquad x < y_j,\qquad x \neq y_k. \end{align*} Let $L \subseteq \{1,\dots,n\}$ be the finite set of indices $i$ for which $y_i < x$ occurs in $\Theta$. Let $U \subseteq \{1,\dots,n\}$ be the finite set of indices $j$ for which $x < y_j$ occurs in $\Theta$. Let $N \subseteq \{1,\dots,n\}$ be the finite set of indices $k$ for which $x \neq y_k$ occurs in $\Theta$. Let $\Theta_0(y_1,\dots,y_n)$ be the conjunction of all literals in $\Theta$ that do not involve $x$. We claim that, modulo $\operatorname{DLO}$, \begin{align*} \exists x\,\Theta(x,y_1,\dots,y_n) \end{align*} is equivalent to \begin{align*} \Theta_0(y_1,\dots,y_n) \wedge \bigwedge_{i \in L}\bigwedge_{j \in U} y_i < y_j. \end{align*}[/step]

[guided]At this stage, the quantified variable $x$ is only being asked to sit somewhere in the order. The literals $y_i < x$ say that $x$ must lie above the parameters indexed by $L$, and the literals $x < y_j$ say that $x$ must lie below the parameters indexed by $U$. The disequalities $x \neq y_k$ do not create an obstruction in a dense order without endpoints, because whenever an interval is nonempty it contains points different from finitely many specified parameters. Let $\Theta_0(y_1,\dots,y_n)$ denote the part of $\Theta$ that does not mention $x$. Define \begin{align*} L &= \{i \in \{1,\dots,n\} : y_i < x \text{ occurs in } \Theta\},\\ U &= \{j \in \{1,\dots,n\} : x < y_j \text{ occurs in } \Theta\},\\ N &= \{k \in \{1,\dots,n\} : x \neq y_k \text{ occurs in } \Theta\}. \end{align*} The only necessary compatibility condition is that every lower bound be below every upper bound: \begin{align*} \bigwedge_{i \in L}\bigwedge_{j \in U} y_i < y_j. \end{align*} We will prove that this condition is also sufficient in every dense linear order without endpoints.[/guided]

[step:Prove necessity of the bound conditions] Let $M \models \operatorname{DLO}$, and let $a_1,\dots,a_n \in M$. Suppose there is an element $b \in M$ such that \begin{align*} M \models \Theta(b,a_1,\dots,a_n). \end{align*} Then $M \models \Theta_0(a_1,\dots,a_n)$, because $\Theta_0$ is a sub-conjunction of $\Theta$. Also, for every $i \in L$ and $j \in U$, the literals $a_i < b$ and $b < a_j$ hold in $M$. By transitivity of the strict linear order, \begin{align*} M \models a_i < a_j. \end{align*} Hence \begin{align*} M \models \Theta_0(a_1,\dots,a_n) \wedge \bigwedge_{i \in L}\bigwedge_{j \in U} a_i < a_j. \end{align*} [/step]

[step:Use density and no endpoints to find a point satisfying the bound conditions]Conversely, let $M \models \operatorname{DLO}$ and let $a_1,\dots,a_n \in M$ satisfy \begin{align*} M \models \Theta_0(a_1,\dots,a_n) \wedge \bigwedge_{i \in L}\bigwedge_{j \in U} a_i < a_j. \end{align*} We construct $b \in M$ satisfying all literals involving $x$. For elements $u,v \in M$, write $u \leq v$ to mean $u < v$ or $u=v$. If $L$ and $U$ are both nonempty, choose $i_0 \in L$ such that $a_i \leq a_{i_0}$ for all $i \in L$, and choose $j_0 \in U$ such that $a_{j_0} \leq a_j$ for all $j \in U$. These extrema exist because $L$ and $U$ are finite and $M$ is linearly ordered. The bound condition gives $a_{i_0} < a_{j_0}$. By density, there exists $b \in M$ such that \begin{align*} a_{i_0} < b < a_{j_0}. \end{align*} We use the following finite consequence of density: every nonempty open interval in $M$ contains more than $q$ points for each $q \in \mathbb{N}$. This is proved by induction on $q$: density gives one point for $q=1$, and applying density to one of the subintervals created by the existing finite set adds a new point. Since $N$ is finite, the interval $(a_{i_0},a_{j_0})$ contains an element $b$ with $b \neq a_k$ for every $k \in N$. If $L$ is nonempty and $U$ is empty, choose $i_0 \in L$ with $a_i \leq a_{i_0}$ for all $i \in L$. Since $M$ has no greatest element, choose $c \in M$ with $a_{i_0} < c$. Repeatedly using density in the interval $(a_{i_0},c)$, choose $b \in M$ such that \begin{align*} a_{i_0} < b < c \end{align*} and $b \neq a_k$ for every $k \in N$. If $L$ is empty and $U$ is nonempty, choose $j_0 \in U$ with $a_{j_0} \leq a_j$ for all $j \in U$. Since $M$ has no least element, choose $c \in M$ with $c < a_{j_0}$. Repeatedly using density in the interval $(c,a_{j_0})$, choose $b \in M$ such that \begin{align*} c < b < a_{j_0} \end{align*} and $b \neq a_k$ for every $k \in N$. If $L$ and $U$ are both empty, choose any $c_0 \in M$. Since $M$ has no greatest element and is dense, it has infinitely many elements above $c_0$; hence choose $b \in M$ with $b \neq a_k$ for every $k \in N$. In each case, $b$ satisfies all lower-bound literals, all upper-bound literals, and all disequality literals involving $x$. Since $\Theta_0(a_1,\dots,a_n)$ also holds, we get \begin{align*} M \models \Theta(b,a_1,\dots,a_n). \end{align*} Therefore the claimed quantifier-free equivalence holds.[/step]

[guided]We now prove that the compatibility conditions are sufficient. Let $M \models \operatorname{DLO}$ and let $a_1,\dots,a_n \in M$ satisfy \begin{align*} M \models \Theta_0(a_1,\dots,a_n) \wedge \bigwedge_{i \in L}\bigwedge_{j \in U} a_i < a_j. \end{align*} We must construct an element $b \in M$ satisfying all literals of $\Theta(b,a_1,\dots,a_n)$ that involve $x$; the literals not involving $x$ already hold because $M\models\Theta_0(a_1,\dots,a_n)$. For elements $u,v\in M$, write $u\leq v$ to mean $u<v$ or $u=v$. First consider the case where $L$ and $U$ are both nonempty. Since $L$ is finite and $M$ is linearly ordered, choose $i_0\in L$ such that \begin{align*} a_i \leq a_{i_0}\quad \text{for all } i\in L. \end{align*} Since $U$ is finite and $M$ is linearly ordered, choose $j_0\in U$ such that \begin{align*} a_{j_0}\leq a_j\quad \text{for all } j\in U. \end{align*} The assumed bound condition applies to the pair $(i_0,j_0)$, so \begin{align*} a_{i_0}<a_{j_0}. \end{align*} The density axiom for $M$ gives an element of the open interval between these two parameters. We also need to avoid the finitely many forbidden parameters $a_k$ with $k\in N$. The finite-avoidance fact we use is this: if $p,q\in M$ satisfy $p<q$, then the interval $(p,q)$ contains more than $r$ elements for every $r\in\mathbb N$. This follows by induction on $r$: density gives the case $r=1$, and if finitely many points have already been chosen in $(p,q)$, one of the subintervals determined by $p$, $q$, and those points is nonempty, so density supplies a new point in that subinterval. Applying this with $p=a_{i_0}$, $q=a_{j_0}$, and $r=|N|$, choose $b\in M$ such that \begin{align*} a_{i_0}<b<a_{j_0} \end{align*} and \begin{align*} b\neq a_k\quad \text{for every } k\in N. \end{align*} For every $i\in L$, the choice of $i_0$ gives $a_i\leq a_{i_0}$, and $a_{i_0}<b$, so transitivity of the strict order gives $a_i<b$. For every $j\in U$, the choice of $j_0$ gives $a_{j_0}\leq a_j$, and $b<a_{j_0}$, so transitivity gives $b<a_j$. Thus $b$ satisfies all lower-bound, upper-bound, and disequality literals involving $x$. Next suppose $L$ is nonempty and $U$ is empty. Choose $i_0\in L$ such that \begin{align*} a_i\leq a_{i_0}\quad \text{for all } i\in L. \end{align*} Since $M$ has no greatest element, choose $c\in M$ with \begin{align*} a_{i_0}<c. \end{align*} By the same finite-avoidance consequence of density applied to the interval $(a_{i_0},c)$, choose $b\in M$ such that \begin{align*} a_{i_0}<b<c \end{align*} and \begin{align*} b\neq a_k\quad \text{for every } k\in N. \end{align*} Then $a_i<b$ for every $i\in L$ by the maximality of $a_{i_0}$ among the listed lower bounds, there are no upper-bound literals to check, and the disequality literals hold by construction. Now suppose $L$ is empty and $U$ is nonempty. Choose $j_0\in U$ such that \begin{align*} a_{j_0}\leq a_j\quad \text{for all } j\in U. \end{align*} Since $M$ has no least element, choose $c\in M$ with \begin{align*} c<a_{j_0}. \end{align*} By finite avoidance inside the interval $(c,a_{j_0})$, choose $b\in M$ such that \begin{align*} c<b<a_{j_0} \end{align*} and \begin{align*} b\neq a_k\quad \text{for every } k\in N. \end{align*} There are no lower-bound literals to check, and for every $j\in U$ we have $b<a_j$ because $b<a_{j_0}\leq a_j$. The disequality literals hold by construction. Finally suppose $L$ and $U$ are both empty. Choose any $c_0\in M$. Since $M$ has no greatest element, choose $c_1\in M$ with $c_0<c_1$; repeatedly applying density and the no-greatest-element axiom shows that $M$ has more than $r$ elements above $c_0$ for every $r\in\mathbb N$. Since $N$ is finite, choose $b\in M$ such that \begin{align*} b\neq a_k\quad \text{for every } k\in N. \end{align*} There are no lower-bound or upper-bound literals to check in this case. In all four cases, $b$ satisfies every literal of $\Theta$ involving $x$. Since $M\models\Theta_0(a_1,\dots,a_n)$ also holds, we obtain \begin{align*} M \models \Theta(b,a_1,\dots,a_n). \end{align*} Therefore \begin{align*} M \models \exists x\,\Theta(x,a_1,\dots,a_n). \end{align*} This proves the sufficiency direction, and together with the necessity direction proves the claimed quantifier-free equivalence over $\operatorname{DLO}$.[/guided]

[step:Induct on formulas to eliminate all quantifiers]We prove by induction on the construction of formulas that every $\mathcal{L}$-formula is equivalent modulo $\operatorname{DLO}$ to a quantifier-free formula. Atomic formulas are already quantifier-free. Boolean combinations are handled by applying the induction hypothesis to the component formulas and then using the same Boolean connective. For the existential case, suppose $\varphi(y_1,\dots,y_n)$ has the form \begin{align*} \exists x\,\theta(x,y_1,\dots,y_n), \end{align*} where, by the induction hypothesis, $\theta$ is equivalent modulo $\operatorname{DLO}$ to a quantifier-free formula. The preceding steps first put that quantifier-free formula into a finite disjunction of conjunctions of literals, then refine negated order literals involving $x$ into equality, lower-bound, and upper-bound cases, and finally eliminate $x$ from each resulting conjunction. Hence the existential quantifier is eliminated from the quantifier-free formula. Universal quantifiers are eliminated using \begin{align*} \forall x\,\theta \quad \leftrightarrow \quad \neg \exists x\,\neg\theta. \end{align*} Therefore $\operatorname{DLO}$ has quantifier elimination.[/step]

[guided]We now upgrade the one-variable existential elimination proved above into full quantifier elimination for every formula. The induction is on the way an $\mathcal{L}$-formula is built. If the formula is atomic, it is already quantifier-free, so there is nothing to eliminate. For Boolean combinations, assume the component formulas have already been replaced by quantifier-free equivalents modulo $\operatorname{DLO}$. If $\alpha$ and $\beta$ are equivalent over $\operatorname{DLO}$ to quantifier-free formulas $\alpha_0$ and $\beta_0$, then $\neg\alpha$, $\alpha\wedge\beta$, and $\alpha\vee\beta$ are respectively equivalent over $\operatorname{DLO}$ to $\neg\alpha_0$, $\alpha_0\wedge\beta_0$, and $\alpha_0\vee\beta_0$, which are still quantifier-free. For the existential case, suppose the formula has the form \begin{align*} \exists x\,\theta(x,y_1,\dots,y_n). \end{align*} By the induction hypothesis, choose a quantifier-free formula $\theta_0(x,y_1,\dots,y_n)$ such that \begin{align*} \operatorname{DLO}\models \theta(x,y_1,\dots,y_n) \leftrightarrow \theta_0(x,y_1,\dots,y_n). \end{align*} Then \begin{align*} \operatorname{DLO}\models \exists x\,\theta(x,y_1,\dots,y_n) \leftrightarrow \exists x\,\theta_0(x,y_1,\dots,y_n). \end{align*} The preceding steps apply to the quantifier-free matrix $\theta_0$: put it into a finite disjunction of conjunctions of literals, normalize equalities and negated order literals involving $x$, and replace each resulting existential conjunction by the corresponding quantifier-free lower-bound and upper-bound condition. Taking the finite disjunction of those quantifier-free replacements gives a quantifier-free formula equivalent to $\exists x\,\theta_0$ over $\operatorname{DLO}$. Universal quantifiers add no new case, because \begin{align*} \forall x\,\theta \quad \leftrightarrow \quad \neg \exists x\,\neg\theta. \end{align*} The right-hand side uses only negation and an existential quantifier, both already handled. Hence every $\mathcal{L}$-formula is equivalent modulo $\operatorname{DLO}$ to a quantifier-free formula, which is quantifier elimination.[/guided]

[step:Conclude that all models of $\operatorname{DLO}$ satisfy the same sentences] Let $M$ and $N$ be any two models of $\operatorname{DLO}$, and let $\varphi$ be an $\mathcal{L}$-sentence. By quantifier elimination, choose a quantifier-free sentence $\psi$ with \begin{align*} \operatorname{DLO} \models \varphi \leftrightarrow \psi. \end{align*} As shown in the first step, $\psi$ is logically equivalent to either $\top$ or $\bot$, independently of the model. Hence \begin{align*} M \models \varphi \quad \text{if and only if} \quad N \models \varphi. \end{align*} Thus all models of $\operatorname{DLO}$ are elementarily equivalent. Equivalently, for every $\mathcal{L}$-sentence $\varphi$, either $\operatorname{DLO} \models \varphi$ or $\operatorname{DLO} \models \neg\varphi$. Hence $\operatorname{DLO}$ is complete. [/step]