\chapter{Quantifier-elimination}

In general, if we have some sentences, how might we show that the theory
that they axiomatize is complete?  If the theory is \emph{not}
complete, this is easy to show:

\begin{example}
  The theory of groups is not complete, since the sentence 
  \begin{equation*}
    \Forall x\Forall y xy=yx
  \end{equation*}
is true (by definition) only in abelian groups, but there are
non-abelian groups (such as the group of permutations of three
objects).  The theory of abelian groups is not complete either, since
(in the signature $\{+,-,0\}$) the sentence
  \begin{equation*}
      \Forall x (x+x=0\to x=0) 
  \end{equation*}
is true in $(\Z,+,-,0)$, but false in $(\Z/2\Z,+,-,0)$.
\end{example}

Let $\TO$ be the theory of \emph{strict} total orders; this is
axiomatized by the universal generalizations of:
\begin{gather*}
  \lnot(x< x),\\
x< y\to\lnot(y< x),\\
x< y\land y< z\to x< z,\\
x< y\lor y< x\lor x=y.
\end{gather*}
This theory is not complete, since $(\varN,<)$ and $(\Z,<)$ are
models of $\TO$ with different complete theories (\textbf{exercise}).

Let $\TO^*$ be the theory of \defn{dense total orders without
  endpoints}, namely, $\TO^*$ has the axioms of $\TO$, along with the
  universal generalizations of:
\begin{gather*}
  \Exists z (x<z\land z<y),\\
\Exists y y<x,\\
\Exists y x<y.
\end{gather*}
The theory $\TO^*$ has a model, namely $(\Q,<)$.
We shall show that $\TO^*$ is complete.  In order to do this, we shall
first show that the theory admits \tech{(full) elimination of quantifiers}.

An arbitrary theory $T$ admits
 \defn{(full) elimination of quantifiers} if, for every formula $\phi$
 of $\lang$, there is an \emph{open} formula $\chi$ of $\lang$ such that
 \begin{equation*}
   T\models(\phi\iff\chi)
 \end{equation*}
---in words, \defn{$\phi$ is equivalent to $\chi$ \emph{modulo} $T$}.

\begin{lemma}\label{lem:QE}
  An $\lang$-theory $T$ admits quantifier-elimination, provided that,
  if $\phi$ is an open formula, and $v$ is a variable, then $\Exists
  v\phi$ is equivalent \emph{modulo} $T$ to an open formula.
\end{lemma}

\begin{proof}
  Use induction on formulas.  Specifically:

Every atomic formula is equivalent \emph{modulo} $T$ to an open
formula, namely itself.

Suppose $\phi$ is equivalent \emph{modulo} $T$ to an open
formula $\alpha$.  Then $T\models(\lnot\phi\iff\lnot\alpha)$; but
$\lnot\alpha$ is open.

Suppose also $\chi$ is equivalent \emph{modulo} $T$ to an open formula
$\beta$.  Then 
\begin{equation*}
  T\models((\phi\to\chi)\iff(\alpha\to\beta));
\end{equation*}
but $(\alpha\to\beta)$ is open.

Finally, $T\models(\Exists v\phi\iff\Exists v\alpha)$
(\textbf{exercise}); but by
assumption, $\Exists v\alpha$ is equivalent to an open formula
$\gamma$; so $T\models(\Exists v\phi\iff\gamma)$ (\textbf{exercise}).
This completes the induction. 
\end{proof}

The lemma can be improved slightly.  Every open formula is logically
equivalent to a formula
in \emph{disjunctive normal form}:
\begin{equation*}
  \bigvee_{i<m}\bigwedge_{j<n}\alpha_i^{(j)},
\end{equation*}
where each $\alpha_i^{(j)}$ is either an atomic or a negated atomic
formula.  (See \S~2.6 of this year's notes for Math 111.)  This
formula in disjunctive normal form can also be written
\begin{equation*}
  \bigvee_{i<m}\bigwedge \Sigma_i
\end{equation*}
where $\Sigma_i=\{a_i^{(j)}:j<n\}$.  Note that
\begin{equation}\label{eqn:Ednf}
\models  (\Exists v\bigvee_{i<m}\bigwedge \Sigma_i \iff
\bigvee_{i<m}\Exists v\bigwedge \Sigma_i)
\end{equation}
(\textbf{exercise}).
The formulas $\Exists v\bigwedge\Sigma_i$ are said to be
\tech{primitive}.  In general, a \defn{primitive} formula is a formula
\begin{equation*}
  \Exists {u_0}\dotsb\Exists{u_{n-1}}\bigwedge \Sigma,
\end{equation*}
where $\Sigma$ is a \emph{finite} non-empty set of atomic and negated atomic
formulas.  (Remember that $\bigwedge\Sigma$ is just an abbreviation
for $\phi_0\land\dots\land\phi_{n-1}$, where the formulas $\phi_i$
compose $\Sigma$; so $\Sigma$ must be finite since formulas must have
finite length.  Also, formulas have \emph{positive} length, so
$\Sigma$ must be non-empty.  However, the notation
$\bigwedge\emptyset$ could be understood to stand for a validity.)

Using \eqref{eqn:Ednf}, we can adjust the induction above to show that
\emph{$T$ admits quantifier-elimination, provided that
every primitive formula with one (existential) quantifier is equivalent
\emph{modulo} $T$ to an open formula.}

Henceforth suppose $\lang$ is $\{<\}$, and $\TO\included T$; so $T$ is
\emph{a} theory of total orders.  Then we can
improve Lemma~\ref{lem:QE} even more.
Indeed, the atomic formulas of $\lang$ now are $x=y$ and $x<y$, where
$x$ and $y$ are variables.  Moreover,
\begin{gather*}
  \TO\models (\lnot (x<y)\iff (x=y\lor y<x)),\\
\TO\models (\lnot(x=y)\iff (x<y\lor y<x)).
\end{gather*}
Hence, in $\lang$, any formula is equivalent, \emph{modulo} $\TO$, to
the result of replacing each negated atomic sub-formula with the
appropriate disjunction of atomic formulas.  If this replacement is
done to a formula in disjunctive normal form, then the new formula
will have a disjunctive
normal form that involves no negations.  So $T$ admits
quantifier-elimination, 
provided that every formula
\begin{equation*}
  \Exists v\bigwedge\Sigma
\end{equation*}
is equivalent, \emph{modulo} $T$, to an open formula, where now
$\Sigma$ is a set of atomic formulas.

Using this criterion, we shall show that $\TO^*$ admits
quantifier-elimination:

\begin{theorem}\label{thm:TO-QE}
  $\TO^*$ admits (full) elimination of quantifiers.
\end{theorem}

\begin{proof}
Let $\Sigma$ be a finite, non-empty set of atomic formulas (in the
signature $\{<\}$).
Let $X$ be the set of variables appearing in
formulas in $\Sigma$; that is,
\begin{equation*}
  X=\bigcup_{\alpha\in\Sigma}\fv{\alpha}.
\end{equation*}
  Then $X$ is a finite non-empty set; say 
\begin{equation*}
  X=\{x_0,\dots,x_{n}\}.
\end{equation*}
Suppose $\str A$ is an $\lang$-structure, and $\tuple a\in A^{n+1}$.  If
$\alpha$ is an atomic formula of $\lang$ with variables from $X$,
we can let $\alpha(\tuple a)$ be the result of replacing each $x_i$ in
$\alpha$ with $a_i$.  Then we can let
\begin{equation*}
  \Sigma(\tuple a)=\{\alpha(\tuple a):\alpha\in\Sigma\}.
\end{equation*}
Suppose in fact 
\begin{equation*}
  \str A\models\TO\cup\{\bigwedge\Sigma(\tuple a)\}.
\end{equation*}
Let us define
  $\Sigma_{(\str A,\tuple a)}$ as the set of atomic formulas $\alpha$
  such that $\fv{\alpha}\included X$ and $\str A\models\alpha(\tuple
  a)$.  Then
  \begin{equation*}
    \Sigma\included\Sigma_{(\str A,\tuple a)}.
  \end{equation*}
Moreover, once $\Sigma$ has been chosen, \emph{there are only finitely
  many possibilities for the set $\Sigma_{(\str A,\tuple a)}$.}  Let
  us list these possibilities as
  \begin{equation*}
    \Sigma_0,\dots,\Sigma_{m-1}.
  \end{equation*}
Now, possibly $m=0$ here.  In this case,
\begin{equation*}
  \TO\models(\Exists v\bigwedge\Sigma\iff v\neq v),
\end{equation*}
so we are done.
Henceforth we may assume $m>0$.
If $\str B\models\TO\cup\{\bigwedge\Sigma(\tuple b)\}$, then
\begin{equation*}
  \str B\models\bigwedge\Sigma_i(\tuple b)
\end{equation*}
for some $i$ in $m$.
Therefore
\begin{equation*}
  \TO\models(\bigwedge\Sigma\iff\bigvee_{i<m}\bigwedge\Sigma_{i}),
\end{equation*}
and hence
\begin{equation*}
  \TO\models(\Exists v\bigwedge\Sigma\iff \bigvee_{i<m}\Exists
  v\bigwedge\Sigma_i). 
\end{equation*}
Therefore, for our proof of quantifier-elimination, we may assume that
$\Sigma$ \emph{is} one of the sets $\Sigma_{(\str A,\tuple a)}$ (so
that, in particular, $m=1$).

Now partition $\Sigma$ as $\Gamma\cup\Delta$, where no formula in
$\Gamma$, but every formula in $\Delta$, contains $v$.  
There are two extreme possibilities:
\begin{mylist}
  \item
Suppose $\Gamma=\emptyset$.  Then $X=\{v\}$ (since if $x\in
X\setminus\{v\}$, then $(x=x)\in\Gamma$).   Also,
$\Sigma=\Delta=\{v=v\}$, so
\begin{equation*}
  \models(\Exists v\bigwedge\Sigma\iff v=v),
\end{equation*}
and we are done in this case.
\item
Suppose $\Delta=\emptyset$.  Then $v\notin X$, and
\begin{equation*}
  \models(\Exists v\bigwedge\Sigma\iff\bigwedge\Sigma),
\end{equation*}
so we are done in \emph{this} case.
\end{mylist}
Henceforth, suppose neither $\Gamma$ nor $\Delta$ is empty.
Then
\begin{equation*}
  \models(\Exists v\bigwedge\Sigma\iff\bigwedge\Gamma\land\Exists
  v\bigwedge\Delta). 
\end{equation*}
We shall show that 
\begin{equation}\label{eqn:goal}
  \TO^*\models(\Exists
v\bigwedge\Sigma\iff\bigwedge\Gamma),
\end{equation}
 which will complete the proof.  To show \eqref{eqn:goal}, it is
 enough to show
 \begin{equation*}
   \TO^*\models(\bigwedge\Gamma\to\Exists v\bigwedge\Delta).
 \end{equation*}
But this follows from the definition of $\TO^*$:

Indeed, remember
that $\Sigma$ is $\Sigma_{(\str A,\tuple a)}$.  Hence, for all $i$ and
$j$ in $n+1$, we have
\begin{gather*}
  a_i<a_j\Iff (x_i<x_j)\in\Sigma;\\
a_i=a_j\Iff (x_i=x_j)\in\Sigma.
\end{gather*}


We have $v\in X$.  We can relabel the elements of $X$ as necessary so
that $v$ is $x_{n}$ and
\begin{equation*}
  a_0\leq\dots\leq a_{n-1}.
\end{equation*}
(Here, $a_i\leq a_{i+1}$ means $a_i<a_{i+1}$ or $a_i=a_{i+1}$ as
usual.)  Suppose $\str 
B\models\TO^*$, and $B^n$ contains $\tuple b$ such that $\str
B\models\bigwedge\Gamma(\tuple b)$.  We have to show that there is $c$
in $B$ such that $\str B\models\bigwedge\Delta(\tuple b,c)$.
Now, for all $i$ and $j$ in $n$, we have
\begin{gather*}
  b_i<b_j\Iff a_i<a_j;\\
b_i=b_j\Iff a_i=a_j.
\end{gather*}
Because $\str B$ is a model of $\TO^*$ (and not just $\TO$), we can
find $c$ as needed according to the relation of $a_n$ with the other
$a_i$: 
\begin{mylist}
  \item
If $a_n=a_i$ for some $i$ in $n$, then let $c=b_i$.
\item
If $a_{n-1}<a_n$, then let $c$ be greater than $b_{n-1}$.
\item
If $a_n<a_0$, then let $c$ be less than $b_0$.
\item
If $a_k<a_n<a_{k+1}$, then we can let $c$ be such
that $b_k<c<b_{k+1}$.
\end{mylist}
This completes the proof that $\TO^*$ admits quantifier-elimination.
\end{proof}

We have proved more than quantifier-elimination: we have
shown that, \emph{modulo} $\TO^*$, the formula $\Exists
v\bigwedge\Sigma$ is equivalent to $v\neq v$ or $v=v$ or an open
formula \emph{with the same free variables as $\Exists
  v\bigwedge\Sigma$}.  In the proof, we introduced $v\neq v$ simply
as a formula $\phi$ such that $\str A\nmodels\phi$ for every
structure $\str A$.  Such a formula corresponds to a nullary Boolean
connective, namely an \defn{absurdity} (the negation of a validity).
We used $0$ as such a connective; but let us now use $\bot$.

Likewise, instead of $v=v$, we can use, as a validity, the nullary
Boolean connective $\top$.  From the last proof, therefore, we have: 

\begin{porism}
In the signature $\{<\}$, with the nullary connectives $\bot$ and
  $\top$ allowed, every formula is equivalent \emph{modulo} $\TO^*$ to
an open formula with the same free variables.
\end{porism}

In a signature of first-order logic without constants, an open
\emph{sentence} consists
entirely of Boolean connectives, with no propositional variables; so
it is either an absurdity or a validity.
As a consequence, we have:

\begin{theorem}
  $\TO^*$ is a complete theory.
\end{theorem}

\begin{proof}
  By the porism, every \emph{sentence} is equivalent to an open
  \emph{sentence}; as just noted, such a sentence is an absurdity or a
  validity.  Suppose $\TO^*\models(\sigma\iff\bot)$.  But
  $\models(\sigma\iff\bot)\iff \lnot\sigma$; so
  $\TO^*\models\lnot\sigma$.  Similarly, if
  $\TO^*\models(\sigma\iff\top)$, then $\TO^*\models\sigma$.  Hence,
  for all sentences $\sigma$, if $\TO^*\nmodels\sigma$, then
  $\TO^*\models\lnot\sigma$.  Therefore $\TO^*$ is complete by
  Lemma~\ref{lem:complete}. 
\end{proof}