Differences
This shows you the differences between two versions of the page.
| Both sides previous 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:** | ||