# Definition of Quantifier Elimination

In this section, we will consider some language and some set of formulas such that (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 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 .

Shorthand: We will generally fix and write as a shorthand for .

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

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

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 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: Take a sentence. Note . Compute . Note that also . So is a ground formula and there is an algorithm to check . But is equivalent to .