Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:extending_languages_of_decidable_theories [2008/04/15 14:27] vkuncak |
sav08:extending_languages_of_decidable_theories [2008/04/17 10:36] david |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| Recall from [[Quantifier elimination definition]] that if $T$ has effective quantifier elimination and there is an algorithm for deciding validity of ground formulas, then the theory is decidable. Now we show a sort of converse. | Recall from [[Quantifier elimination definition]] that if $T$ has effective quantifier elimination and there is an algorithm for deciding validity of ground formulas, then the theory is decidable. Now we show a sort of converse. | ||
| - | **Lemma:** Consider a set of formulas $T$. Then there exists an extended language $L' \supseteq L$ and a set of formulas $T'$ such that $T'$ has effective quantifier elimination, and such that $Conseq(T)$ is exactly the set of those formulas in $Conseq(T')$ that contain only symbols from ${\cal L}$. | + | **Lemma:** Consider a set of formulas $T$. Then there exists an extended language $L' \supseteq L$ and a set of formulas $T'$ such that $T'$ has effective quantifier elimination, and such that $Conseq(T)$ is exactly the set of those formulas in $Conseq(T')$ that contain only symbols from $L$. |
| **Proof:** | **Proof:** | ||
| Line 37: | Line 37: | ||
| T' = \{ F \mid rf(F) \in Conseq(T) \} | T' = \{ F \mid rf(F) \in Conseq(T) \} | ||
| \] | \] | ||
| + | ++++ | ||
| How to do quantifier elimination in $T'$? | How to do quantifier elimination in $T'$? | ||
| ++++| | ++++| | ||
| The quantifier-free version of $F$ is then simply $R_{rf(F)}(x_1,\ldots,x_n)$ where $fv(rf(F)) = x_1,\ldots,x_n$. This quantifier elimination is easy and effective (and trivial). | The quantifier-free version of $F$ is then simply $R_{rf(F)}(x_1,\ldots,x_n)$ where $fv(rf(F)) = x_1,\ldots,x_n$. This quantifier elimination is easy and effective (and trivial). | ||
| - | ++++ | ||
| - | |||
| ++++ | ++++ | ||