Differences
This shows you the differences between two versions of the page.
sav08:quantifier_elimination_definition [2009/04/22 10:07] vkuncak |
sav08:quantifier_elimination_definition [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Definition of Quantifier Elimination ====== | ||
- | |||
- | In this section, we will consider some language ${\cal L}$ and some set $T$ of formulas (see [[sav08: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 be fixing $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:** | ||
- | ++++| | ||
- | Take $F$ a sentence. Note $FV(F)=\emptyset$. Compute $qe(F)$. Note that also $FV(qe(F)) \subseteq FV(F) = \emptyset$. So $qe(F)$ is a ground formula and there is an algorithm to check $\models qe(F)$. But $\models F$ is equivalent to $\models qe(F)$. | ||
- | ++++ | ||