Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:quantifier_elimination_definition [2009/04/21 19:23] vkuncak |
sav08:quantifier_elimination_definition [2009/04/22 14:20] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Definition of Quantifier Elimination ====== | ====== 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 [[sav08:First-Order Logic Semantics]]). We will write $\models F$ to denote $T \models F$ (which is equivalent to $F \in T$). | + | In this section, we will consider some language ${\cal L}$ and some set $T$ of formulas such that $Conseq(T)=T$ (see [[sav08:First-Order Logic Semantics]]). |
As a special case, we can have | As a special case, we can have | ||
Line 10: | Line 10: | ||
Then $\models F$ reduces to $\forall I \in {\cal I}. e_F(F)(I)$. | 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)$. | 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, | **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, | ||
Line 24: | Line 26: | ||
* $FV(qe(F)) \subseteq FV(F)$ | * $FV(qe(F)) \subseteq FV(F)$ | ||
(In words: for every formula there exists an equivalent quantifier-free formula with same free variables.) | (In words: for every formula there exists an equivalent quantifier-free formula with same free variables.) | ||
- | We say that $T$ admits //effective quantifier elimination// if there is an //effectively computable// function $qe$ with the property above. | + | |
+ | **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 | **Definition:** A //ground formula// is a formula $F$ such that |