Notes - Logic and Proof MT24, Unbounded dense linear orders
Flashcards
Consider a signature with a single binary relation $<$. The theory $\pmb T _ {UDLO}$ is the set of sentences entailed by the axioms:
\[\begin{aligned}
F_1 &: \forall x \lnot(x < x) \\\\
F_2 &: \forall x \forall y \forall z(x < y \land y < z \to x < z) \\\\
F_3 &: \forall x \forall y (x < y \lor y < x \lor x = y) \\\\
F_4 &: \forall x \forall y (x < y \to \exists z(x < z \land z <y)) \\\\
F_5 &: \forall x \exists y \exists z (y < x < z)
\end{aligned}\]
@Prove that $\pmb T _ {UDLO}$ is complete, decidable and has quantifier elimination.
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$.