Differences

This shows you the differences between two versions of the page.

--- sav08:extending_languages_of_decidable_theories [2008/04/15 14:25]
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.
-**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:**
+How to define $L'$?
 ++++|
 Fix an ordering on the set $V$ of all first-order variables.  If $G$ is a term, formula, or a set of formulas, let $fv(G)$ denote the ordered list of its free variables.
@@ Line 28: / Line 29: @@
 \]
 in the last definition, $F$ is a formula in $L$ and $fv(F) = x_1,\ldots,x_n$ is the sorted list of its free variables.
+++++
-We then let
+How to define $T'$?
+++++|
+We let
 \[
    T' = \{ F \mid rf(F) \in Conseq(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).
 ++++