LARA

This is an old revision of the document!


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).

As a special case, we can have \[

  T = \{ F \mid \forall I \in {\cal I}. e_F(F)(I) \}

\] 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 \[

  \lnot (0 = 1) \rightarrow \lnot (0 + 1 = 1 + 1)

\]

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: