[proofplan] We prove quantifier elimination syntactically by showing that one existential quantifier can always be removed from a quantifier-free formula. After reducing a quantifier-free formula to a finite disjunction of conjunctions of positive order and equality literals, each conjunction describes finitely many lower bounds, upper bounds, and possible equalities for the quantified variable. Density realizes the case with both lower and upper bounds, while the absence of endpoints realizes the one-sided cases. Eliminating one existential quantifier and then inducting on the number of quantifiers gives the result for all formulas. [/proofplan] [step:Reduce quantifier elimination to eliminating one existential quantifier from a quantifier-free formula] Let $\bar{y} = (y_1,\dots,y_n)$ be an $n$-tuple of variables, and let $x$ be a variable distinct from each $y_i$. It is enough to prove the following assertion: For every quantifier-free $L$-formula $\theta(x,\bar{y})$, there is a quantifier-free $L$-formula $\theta^\exists(\bar{y})$ such that \begin{align*} T_{\mathrm{DLO}} \models \forall \bar{y}\,\bigl(\exists x\,\theta(x,\bar{y}) \leftrightarrow \theta^\exists(\bar{y})\bigr). \end{align*} Indeed, once this assertion is known, an arbitrary formula is handled by induction on the number of quantifiers. Boolean connectives preserve the class of formulas equivalent over $T_{\mathrm{DLO}}$ to quantifier-free formulas. Universal quantifiers are eliminated using \begin{align*} \forall x\,\varphi(x,\bar{y}) \leftrightarrow \neg \exists x\,\neg \varphi(x,\bar{y}). \end{align*} Thus repeated elimination of innermost existential quantifiers gives a quantifier-free formula equivalent over $T_{\mathrm{DLO}}$ to the original formula. [guided] We isolate the only operation that must be proved: removing a single existential quantifier from a quantifier-free formula. Let $\bar{y} = (y_1,\dots,y_n)$ be the remaining free variables, and let $x$ be the variable to eliminate. The target statement is that every quantifier-free formula $\theta(x,\bar{y})$ has a quantifier-free replacement $\theta^\exists(\bar{y})$ satisfying \begin{align*} T_{\mathrm{DLO}} \models \forall \bar{y}\,\bigl(\exists x\,\theta(x,\bar{y}) \leftrightarrow \theta^\exists(\bar{y})\bigr). \end{align*} Why does this prove the full theorem? First eliminate the innermost quantifier of a formula. If it is existential, the assertion applies directly. If it is universal, use the logical equivalence \begin{align*} \forall x\,\varphi(x,\bar{y}) \leftrightarrow \neg \exists x\,\neg \varphi(x,\bar{y}). \end{align*} The inner formula $\neg\varphi(x,\bar{y})$ is already equivalent, by the induction hypothesis on inner quantifiers, to a quantifier-free formula, so the existential elimination step applies. Boolean combinations of quantifier-free formulas remain quantifier-free after the usual propositional simplifications. Repeating this process removes all quantifiers. [/guided] [/step] [step:Put the quantifier-free formula into positive disjunctive normal form] Every atomic $L$-formula in the variables $x,\bar{y}$ has one of the forms $u < v$ or $u = v$, where $u$ and $v$ are variables among $x,y_1,\dots,y_n$. In every model of $T_{\mathrm{DLO}}$, the negations of atomic formulas are equivalent to positive formulas: \begin{align*} \neg(u < v) &\leftrightarrow (u = v \lor v < u),\\ \neg(u = v) &\leftrightarrow (u < v \lor v < u). \end{align*} The first equivalence uses trichotomy of the strict linear order, and the second uses irreflexivity and trichotomy. Therefore, by propositional distribution, every quantifier-free $\theta(x,\bar{y})$ is equivalent over $T_{\mathrm{DLO}}$ to a finite disjunction \begin{align*} \bigvee_{r=1}^m \Gamma_r(x,\bar{y}), \end{align*} where each $\Gamma_r(x,\bar{y})$ is a finite conjunction of positive atomic formulas of the forms $u < v$ and $u = v$. We now normalize the reflexive atoms inside each conjunction. If a conjunction contains an atom $u < u$, then that conjunction is contradictory in every strict linear order, by irreflexivity of $<$. We delete that whole disjunct from the finite disjunction. If a conjunction contains an atom $u = u$, then that atom is true in every structure, by reflexivity of equality, and we delete only that atom from the conjunction. After this normalization, every remaining conjunction is a finite conjunction of positive atomic formulas $u < v$ and $u = v$ with $u$ and $v$ distinct variables. If all disjuncts are deleted, the disjunction is the contradiction formula $y_1 < y_1$ when $n \geq 1$, and the contradiction formula $x < x$ before eliminating $x$ when $n = 0$. Since \begin{align*} \exists x\,\bigvee_{r=1}^m \Gamma_r(x,\bar{y}) \leftrightarrow \bigvee_{r=1}^m \exists x\,\Gamma_r(x,\bar{y}), \end{align*} it remains to eliminate $\exists x$ from one normalized conjunction $\Gamma(x,\bar{y})$. [guided] The language has no function symbols and no constant symbols, so the only terms are variables. Hence every atomic formula involving the variables $x,y_1,\dots,y_n$ is either $u < v$ or $u = v$ for variables $u,v$ chosen from this list. We first remove negated atomic formulas. In a strict linear order, exactly one of $u < v$, $u = v$, and $v < u$ holds. Hence \begin{align*} \neg(u < v) &\leftrightarrow (u = v \lor v < u),\\ \neg(u = v) &\leftrightarrow (u < v \lor v < u). \end{align*} These equivalences are consequences of the linear-order axioms included in $T_{\mathrm{DLO}}$. After replacing all negated atoms in this way, ordinary propositional distribution writes the formula as a finite disjunction of finite conjunctions: \begin{align*} \theta(x,\bar{y}) \leftrightarrow \bigvee_{r=1}^m \Gamma_r(x,\bar{y}), \end{align*} where every literal in every $\Gamma_r$ is now a positive atomic formula. There is one syntactic case that must be handled before the lower-bound and upper-bound analysis: an atom may compare a variable with itself. If a conjunction contains $u < u$, then it is false in every model of $T_{\mathrm{DLO}}$, because $<$ is irreflexive. We may therefore delete that entire disjunct. If a conjunction contains $u = u$, then that atom is true in every structure, by reflexivity of equality, so we delete only that atom. After performing these deletions in every disjunct, each remaining conjunction contains only positive atoms $u < v$ and $u = v$ with $u$ and $v$ distinct variables. This normalization is what prevents the later case $E=L=U=\varnothing$ from incorrectly treating the contradictory formula $x < x$ as satisfiable. Existential quantification distributes over finite disjunction: \begin{align*} \exists x\,\bigvee_{r=1}^m \Gamma_r(x,\bar{y}) \leftrightarrow \bigvee_{r=1}^m \exists x\,\Gamma_r(x,\bar{y}). \end{align*} Thus it is enough to handle a single normalized conjunction $\Gamma(x,\bar{y})$. [/guided] [/step] [step:Eliminate the quantified variable when it is forced to equal a parameter] Fix a normalized finite conjunction $\Gamma(x,\bar{y})$ of positive atomic formulas, so no atom in $\Gamma$ has the same variable on both sides. Let $\Delta(\bar{y})$ be the conjunction of all atoms in $\Gamma$ that do not contain $x$. Define three finite index sets: \begin{align*} E &= \{i \in \{1,\dots,n\} : x = y_i \text{ or } y_i = x \text{ occurs in } \Gamma\},\\ L &= \{i \in \{1,\dots,n\} : y_i < x \text{ occurs in } \Gamma\},\\ U &= \{i \in \{1,\dots,n\} : x < y_i \text{ occurs in } \Gamma\}. \end{align*} Assume first that $E \neq \varnothing$, and choose $e \in E$. Define the quantifier-free formula $\Gamma^\exists(\bar{y})$ by \begin{align*} \Gamma^\exists(\bar{y}) := \Delta(\bar{y}) \land \bigwedge_{i \in E}(y_i = y_e) \land \bigwedge_{i \in L}(y_i < y_e) \land \bigwedge_{j \in U}(y_e < y_j). \end{align*} We claim that \begin{align*} T_{\mathrm{DLO}} \models \forall \bar{y}\,\bigl(\exists x\,\Gamma(x,\bar{y}) \leftrightarrow \Gamma^\exists(\bar{y})\bigr). \end{align*} Let $M \models T_{\mathrm{DLO}}$, and let $\bar{a} = (a_1,\dots,a_n) \in M^n$. If $b \in M$ satisfies $\Gamma(b,\bar{a})$, then every equality constraint in $E$ gives $b = a_i$, so $a_i = a_e$ for all $i \in E$. Every lower-bound constraint gives $a_i < b = a_e$, and every upper-bound constraint gives $a_e = b < a_j$. The $x$-free part gives $\Delta(\bar{a})$. Hence $M \models \Gamma^\exists(\bar{a})$. Conversely, if $M \models \Gamma^\exists(\bar{a})$, set $b := a_e$. Then $b = a_i$ for all $i \in E$, $a_i < b$ for all $i \in L$, $b < a_j$ for all $j \in U$, and $\Delta(\bar{a})$ holds. Therefore $M \models \Gamma(b,\bar{a})$, so $M \models \exists x\,\Gamma(x,\bar{a})$. [guided] The first case is the easiest geometrically: the conjunction tells us that $x$ must equal one of the parameters. Let \begin{align*} E &= \{i \in \{1,\dots,n\} : x = y_i \text{ or } y_i = x \text{ occurs in } \Gamma\}. \end{align*} Assume $E \neq \varnothing$, and choose one index $e \in E$. If $x$ exists, it must be equal to $y_e$. Therefore all other equality requirements $x = y_i$ force $y_i = y_e$. Similarly, every lower-bound condition $y_i < x$ becomes $y_i < y_e$, and every upper-bound condition $x < y_j$ becomes $y_e < y_j$. This motivates the definition \begin{align*} \Gamma^\exists(\bar{y}) := \Delta(\bar{y}) \land \bigwedge_{i \in E}(y_i = y_e) \land \bigwedge_{i \in L}(y_i < y_e) \land \bigwedge_{j \in U}(y_e < y_j), \end{align*} where $\Delta(\bar{y})$ records the atoms in $\Gamma$ not involving $x$. Now verify both directions. Suppose $M \models T_{\mathrm{DLO}}$, $\bar{a} \in M^n$, and $b \in M$ satisfies $\Gamma(b,\bar{a})$. Since $e \in E$, the conjunction contains an equality forcing $b = a_e$. Hence every equality $x = y_i$ or $y_i = x$ forces $a_i = a_e$. Every atom $y_i < x$ gives $a_i < b = a_e$, and every atom $x < y_j$ gives $a_e = b < a_j$. The atoms not involving $x$ give $\Delta(\bar{a})$. Thus $M \models \Gamma^\exists(\bar{a})$. Conversely, suppose $M \models \Gamma^\exists(\bar{a})$. Define $b := a_e$. Then the equalities, lower bounds, upper bounds, and $x$-free atoms required by $\Gamma$ all hold after substituting $b$ for $x$. Hence $M \models \Gamma(b,\bar{a})$, proving $M \models \exists x\,\Gamma(x,\bar{a})$. [/guided] [/step] [step:Eliminate the quantified variable when it is constrained only by lower and upper bounds] Now assume $E = \varnothing$. Define \begin{align*} \Gamma^\exists(\bar{y}) := \Delta(\bar{y}) \land \bigwedge_{i \in L}\bigwedge_{j \in U}(y_i < y_j). \end{align*} We prove that \begin{align*} T_{\mathrm{DLO}} \models \forall \bar{y}\,\bigl(\exists x\,\Gamma(x,\bar{y}) \leftrightarrow \Gamma^\exists(\bar{y})\bigr). \end{align*} Let $M \models T_{\mathrm{DLO}}$, and let $\bar{a} \in M^n$. If $b \in M$ satisfies $\Gamma(b,\bar{a})$, then $\Delta(\bar{a})$ holds. Also, for every $i \in L$ and $j \in U$, we have $a_i < b < a_j$, so $a_i < a_j$ by transitivity. Hence $M \models \Gamma^\exists(\bar{a})$. Conversely, suppose $M \models \Gamma^\exists(\bar{a})$. We must find $b \in M$ such that $a_i < b$ for all $i \in L$ and $b < a_j$ for all $j \in U$. If $L = \varnothing$ and $U = \varnothing$, choose any $b \in M$, which exists because models of $T_{\mathrm{DLO}}$ are nonempty. If $L = \varnothing$ and $U \neq \varnothing$, choose $j_0 \in U$. Among the finite set $\{a_j : j \in U\}$, choose an element $a_{j_*}$ such that $a_{j_*} \leq a_j$ for all $j \in U$; such an element exists because $<$ is a linear order and the set is finite. Since $M$ has no left endpoint, there is $b \in M$ such that $b < a_{j_*}$, and then $b < a_j$ for all $j \in U$. If $L \neq \varnothing$ and $U = \varnothing$, choose $i_0 \in L$. Among the finite set $\{a_i : i \in L\}$, choose an element $a_{i_*}$ such that $a_i \leq a_{i_*}$ for all $i \in L$. Since $M$ has no right endpoint, there is $b \in M$ such that $a_{i_*} < b$, and then $a_i < b$ for all $i \in L$. Finally, suppose $L \neq \varnothing$ and $U \neq \varnothing$. Choose $i_* \in L$ such that $a_i \leq a_{i_*}$ for all $i \in L$, and choose $j_* \in U$ such that $a_{j_*} \leq a_j$ for all $j \in U$. Since $M \models \Gamma^\exists(\bar{a})$, we have $a_{i_*} < a_{j_*}$. By density, choose $b \in M$ such that \begin{align*} a_{i_*} < b < a_{j_*}. \end{align*} Then $a_i < b$ for every $i \in L$, and $b < a_j$ for every $j \in U$. In all cases, $M \models \Gamma(b,\bar{a})$. [guided] Now $x$ is not forced to equal any parameter. The conjunction only asks $x$ to lie above some parameters and below some others. The lower-bound indices and upper-bound indices are \begin{align*} L &= \{i \in \{1,\dots,n\} : y_i < x \text{ occurs in } \Gamma\},\\ U &= \{i \in \{1,\dots,n\} : x < y_i \text{ occurs in } \Gamma\}. \end{align*} A point $x$ satisfying all these inequalities can exist only if every lower bound lies below every upper bound. This is the quantifier-free condition \begin{align*} \bigwedge_{i \in L}\bigwedge_{j \in U}(y_i < y_j). \end{align*} So we define \begin{align*} \Gamma^\exists(\bar{y}) := \Delta(\bar{y}) \land \bigwedge_{i \in L}\bigwedge_{j \in U}(y_i < y_j). \end{align*} First suppose $b \in M$ satisfies $\Gamma(b,\bar{a})$. Then every lower-bound atom gives $a_i < b$, and every upper-bound atom gives $b < a_j$. Therefore, for each $i \in L$ and $j \in U$, \begin{align*} a_i < b < a_j, \end{align*} so $a_i < a_j$ by transitivity. The $x$-free atoms also hold, so $M \models \Gamma^\exists(\bar{a})$. Conversely, suppose $M \models \Gamma^\exists(\bar{a})$. We construct a witness $b \in M$. If there are no lower bounds and no upper bounds, any element of $M$ works, and $M$ is nonempty by the definition of $T_{\mathrm{DLO}}$. If there are only upper bounds, choose a least element among the finite set $\{a_j : j \in U\}$ with respect to the linear order; call it $a_{j_*}$. The absence of left endpoints gives an element $b \in M$ with $b < a_{j_*}$. Since $a_{j_*} \leq a_j$ for every $j \in U$, transitivity gives $b < a_j$ for every $j \in U$. If there are only lower bounds, choose a greatest element among the finite set $\{a_i : i \in L\}$; call it $a_{i_*}$. The absence of right endpoints gives $b \in M$ with $a_{i_*} < b$. Since $a_i \leq a_{i_*}$ for every $i \in L$, transitivity gives $a_i < b$ for every $i \in L$. Finally, suppose both lower and upper bounds are present. Choose a greatest lower-bound parameter $a_{i_*}$ among $\{a_i : i \in L\}$ and a least upper-bound parameter $a_{j_*}$ among $\{a_j : j \in U\}$. The formula $\Gamma^\exists(\bar{a})$ includes $a_{i_*} < a_{j_*}$. Density of the order gives $b \in M$ such that \begin{align*} a_{i_*} < b < a_{j_*}. \end{align*} Then $b$ lies above every lower-bound parameter and below every upper-bound parameter. Thus $b$ satisfies all atoms of $\Gamma(b,\bar{a})$ involving $x$, and $\Delta(\bar{a})$ supplies all atoms not involving $x$. [/guided] [/step] [step:Assemble the elimination for arbitrary formulas] For each normalized conjunction $\Gamma_r(x,\bar{y})$ remaining in the finite disjunction obtained from $\theta(x,\bar{y})$, the preceding two steps produce a quantifier-free formula $\Gamma_r^\exists(\bar{y})$ such that \begin{align*} T_{\mathrm{DLO}} \models \forall \bar{y}\,\bigl(\exists x\,\Gamma_r(x,\bar{y}) \leftrightarrow \Gamma_r^\exists(\bar{y})\bigr). \end{align*} Define \begin{align*} \theta^\exists(\bar{y}) := \bigvee_{r=1}^m \Gamma_r^\exists(\bar{y}). \end{align*} Then \begin{align*} T_{\mathrm{DLO}} \models \forall \bar{y}\,\bigl(\exists x\,\theta(x,\bar{y}) \leftrightarrow \theta^\exists(\bar{y})\bigr). \end{align*} Thus every existential quantifier applied to a quantifier-free formula can be eliminated. By the reduction step, every $L$-formula is equivalent over $T_{\mathrm{DLO}}$ to a quantifier-free $L$-formula. Therefore $T_{\mathrm{DLO}}$ has quantifier elimination. [/step]