This is an old revision of the document!
Definition of Quantifier Elimination
In this section, we will consider some language and some set
of formulas such that
(see First-Order Logic Semantics). We will write
to denote
(which is equivalent to
).
As a special case, we can have \[
T = \{ F \mid \forall I \in {\cal I}. e_F(F)(I) \}
\]
where is a set of interpretations of interest.
Then
reduces to
.
If we look at one interpretation, then
contains only that interpretation and the condition
means
.
Example: Let be the structure of integers with addition. If we let
then
in the definition above is the set of all formulas involving only
that are true about integers. In this example,
contains e.g. formulas
does not contain e.g. formula
Definition: We say that admits quantifier elimination iff for every FOL formula
in
there exists some formula
such that
has no quantifiers
(In words: for every formula there exists an equivalent quantifier-free formula with same free variables.)
We say that admits effective quantifier elimination if there is an effectively computable function
with the property above.
Definition: A ground formula is a formula such that
contains no quantifiers and
.
Example: in language where
are constants and
is a binary operation, an example of a ground formula is
\[
\lnot (0 = 1) \rightarrow \lnot (0 + 1 = 1 + 1)
\]
Lemma: Suppose that
has effective quantifier elimination;
- there is an algorithm for deciding
when
is a ground formula.
Then there is an algorithm for deciding, given a sentence , whether
.
Proof: