Definition of Quantifier Elimination

In this section, we will consider some language ${\cal L}$ and some set $T$ of formulas such that $Conseq(T)=T$ (see First-Order Logic Semantics).

Informal summary: the meaning of relations and functions such as <,+, can be defined by starting from first-order logic, and then introducing a set of axioms in first-order logic that they satisfy, and taking also their consequences. The set of axioms and consequences that define the operations and relations of interest is the theory. Formally, the theory is simply any set of fully quantified formulas (often the theory is understood to also include all of its consequences).

As a special case, we can have

$\begin{equation*} T = \{ F \mid \forall I \in {\cal I}. e_F(F)(I) \} \end{equation*}$

where ${\cal I}$ is a set of interpretations of interest. Then $\models F$ reduces to $\forall I \in {\cal I}. e_F(F)(I)$ . If we look at one interpretation, then ${\cal I}$ contains only that interpretation and the condition $\models F$ means $e_F(F)(I)$ .

Shorthand: We will generally fix $T$ and write $\models F$ as a shorthand for $T \models F$ .

Example: Let $M = ({\cal Z},+)$ be the structure of integers with addition. If we let ${\cal I} = \{ M \}$ then $T$ in the definition above is the set of all formulas involving only $+$ that are true about integers. In this example,

$T$ contains e.g. formulas
- $(\forall x. x = x)$
- $(\forall x.\forall y. x+y=y+x)$
- $(\forall x.\forall y. \forall z. (x+y=z \rightarrow z+x = x+x+y)$
- $(\exists y. \forall x. x + y = x)$
$T$ does not contain e.g. formula $(\forall x. x + x = x)$

Definition: We say that $T$ admits quantifier elimination iff for every FOL formula $F$ in ${\cal L}$ there exists some formula $qe(F)$ such that

$\models (F \leftrightarrow qe(F))$
$qe(F)$ has no quantifiers
$FV(qe(F)) \subseteq FV(F)$

(In words: for every formula there exists an equivalent quantifier-free formula with same free variables.)

Definition: We say that $T$ admits effective quantifier elimination if there is an effectively computable function $qe$ with the property in the previous definition.

Definition: A ground formula is a formula $F$ such that

$F$ contains no quantifiers and
$FV(F)=\emptyset$ .

Example: in language ${\cal L} = \{0,1,+\}$ where $0,1$ are constants and $+$ is a binary operation, an example of a ground formula is

$\begin{equation*} \lnot (0 = 1) \rightarrow \lnot (0 + 1 = 1 + 1) \end{equation*}$

Lemma: Suppose that

$T$ has effective quantifier elimination;
there is an algorithm for deciding $F \in T$ when $F$ is a ground formula.

Then there is an algorithm for deciding, given a sentence $F$ , whether $F \in T$ .

Proof: