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 formulas
- does not contain e.g. formula
(e.g. structure of integers),
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, binary operation, an example of a ground formula is \[
a = b \rightarrow a + b = b
\]
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: