Logic and Proof MT24, Unbounded dense linear orders

We first show that $\pmb T _ {UDLO}$ has an effective quantifier-elimination procedure. It suffices to be able to eliminate the quantifier $\exists x$ in the case where $F$ is a conjunction of atomic formulas all of which mention $x$ (a justification is given at the end, here it’s possible to just consider conjunctions of atomic formulas rather than literals, since the negation of an atomic formula can be written as disjuncts of other atomic formulas).

Each conjunct in such formulas have the form:

• $x = y$
• $x < y$
• $y < x$

for some variable $y$.

If $F$ contains a conjunct $x < x$, then we have $G = \mathbf{false}$.

If $F$ contains a conjunct $x = y$ for some variable $y$, then we have $G = F[y/x]$.

If neither of the above applies then (after deleting conjuncts of the form $x = x$ if present), we can write $F$ in the form:

\[F = \bigwedge^m_{i = 1} l_i < x \land \bigwedge^n_{j = 1} x < u_j\]

where $l _ i$ and $u _ j$ are variables different from $x$. If $m = 0$, then there are no lower bounds on $x$ and $G = \mathbf{true}$ since the order relation is unbounded. If $n = 0$, then $G = \mathbf{true}$ also. Otherwise, by the density of the order relation,

\[G = \bigwedge^m_{i = 1} \bigwedge^n_{j = 1} l_i < u_j\]

Decidability of $\pmb T _ {UDLO}$ follows from the existence of this procedure, since we can remove the quantifiers from the inside out, and each inner proposition is equivalent to either $\mathbf{true}$ or $\mathbf{false}$.

$T _ {UDLO}$ is also complete for the same reason, since this shows every formula holds or its negation holds.

---

Consider a formula $\exists x F$ where $F$ is quantifier free. We aim to construct a quantifier formula $G$ with the same free variables as $\exists x F$ such that for any structure $\mathcal A$ that satisfies all sentences in $\pmb T _ {UDLO}$ and any valuation $\pmb a$ in $\mathcal A$ of the free variables, we have $\mathcal A \models \exists x F(\pmb a)$ if and only if $\mathcal A \models G(\pmb a)$.

Firstly, convert $F$ into a logically equivalent formula in DNF. Furthermore, we can eliminate negative literals by replacing the sub-formula $\lnot (x _ i < x _ j)$ with $x _ i = x _ j \lor x _ j < x _ i$ and replacing $\lnot (x _ i = x _ j)$ with $x _ i < x _ j \lor x _ j < x _ i$.

So we may assume $F$ is in DNF and is negation-free. Then using the equivalence

\[\exists x (F_1 \lor F_2) \equiv \exists x F_1 \lor \exists x F_2\]

it suffices to show how to eliminate the quantifier $\exists x$ in the case $F$ is a conjunction of atomic formulas. And using the equivalence $\exists x (F _ 1 \land F _ 2) \equiv \exists x F _ 1 \land F _ 2$ where $x$ is not free in $F _ 2$, so it suffices to be able to eliminate the quantifier $\exists x$ in the case where $F$ is a conjunction of atomic formulas all of which mention $x$.

Overall idea: Build up two enumerations of the orderings which have the desired properties, switching between making one enumeration and then the other. Since the ordering is unbounded and dense, we always have “enough” elements that we can match up elements from each of the orderings.

Let

\[\begin{aligned} &a _ 1, a _ 2, a _ 3, \ldots \\\\ &b _ 1, b _ 2, b _ 3, \ldots \end{aligned}\]

are two enumerations of the elements of $A$ and $B$ without repetitions. We aim to find two new enumerations

\[\begin{aligned} &a' _ 1, a' _ 2, a' _ 3, \ldots \\\\ &b' _ 1, b' _ 2, b' _ 3, \ldots \end{aligned}\]

such that for any pair of indices $i$ and $j$,

\[a _ i' < a _ j' \iff b _ i' < b _ j'\]

Then the bijection can be defined by $f(a _ i’) = b _ i’$ for each $i$.

To do this, define $a _ i’$ and $b _ i’$ by strong induction.

Suppose we have defined

\[\begin{aligned} &a' _ 1, a' _ 2, \ldots, a' _ n \\\\ &b' _ 1, b' _ 2, \ldots, b' _ n \end{aligned}\]

We consider two cases.

If $n$ is even, define $a’ _ {n+1}$ to be the first element of the original enumeration $a _ 1, a _ 2, \ldots$ that does not appear among $a _ 1’, \ldots, a _ n’$. Then define $b’ _ {n+1}$ such that $a _ i’ < a’ _ {n+1}$ if and only if $b _ i’ < b’ _ {n+1}$ for $1 \le i \le n$. This is possible because $(B, <)$ is a dense linear order: if there exists some $j$ such that $a _ i’ < a _ {n+1}’ < a _ j’$, then by density, there must be a corresponding $b’ _ {n+1}$ between $b _ i’$ and $b _ j’$. If there is no such $a _ i’$ and $b _ j’$, then we can take $b _ {n+1}’$ to be very big or small, using the fact that the ordering is unbounded.

If $n$ is odd, make the same definition but switch the roles of $A$ and $B$.

Proceeding this way, we obtain the new enumeration with the desired properties, and then can define $f$ as necessary.