• English only

# Differences

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

 sav08:extending_languages_of_decidable_theories [2008/04/15 14:27]vkuncak sav08:extending_languages_of_decidable_theories [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/04/17 10:36 david 2008/04/15 14:27 vkuncak 2008/04/15 14:27 vkuncak 2008/04/15 14:27 vkuncak 2008/04/15 14:26 vkuncak 2008/04/15 14:25 vkuncak 2008/04/15 14:25 vkuncak 2008/04/15 14:24 vkuncak 2008/04/15 14:21 vkuncak 2008/04/15 14:00 vkuncak 2008/04/15 11:55 vkuncak created Next revision Previous revision 2008/04/17 10:36 david 2008/04/15 14:27 vkuncak 2008/04/15 14:27 vkuncak 2008/04/15 14:27 vkuncak 2008/04/15 14:26 vkuncak 2008/04/15 14:25 vkuncak 2008/04/15 14:25 vkuncak 2008/04/15 14:24 vkuncak 2008/04/15 14:21 vkuncak 2008/04/15 14:00 vkuncak 2008/04/15 11:55 vkuncak created 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 12: Line 12: Let ${\cal F}$ denote the set of formulas in language ${\cal L}$.  Define Let ${\cal F}$ denote the set of formulas in language ${\cal L}$.  Define - $+ \begin{equation*} L' = \{ R_{F} \mid F \in {\cal F} \} L' = \{ R_{F} \mid F \in {\cal F} \} -$ + \end{equation*} where $R_{F}$ is a new relation symbol whose arity is equal to $|FV(F)|$. ​ In other words, we introduce a relation symbol for each formula of the original language. where $R_{F}$ is a new relation symbol whose arity is equal to $|FV(F)|$. ​ In other words, we introduce a relation symbol for each formula of the original language. For each formula $F$ in language $L'$ we define relation-form of $F$, denoted $rf(F)$, which is a formula in the original language $L$ given by For each formula $F$ in language $L'$ we define relation-form of $F$, denoted $rf(F)$, which is a formula in the original language $L$ given by - $+ \begin{equation*} \begin{array}{l} \begin{array}{l} ​rf(F_1 \land F_2) = R_{rf(F_1) \land rf(F_2)} \\ ​rf(F_1 \land F_2) = R_{rf(F_1) \land rf(F_2)} \\ Line 27: Line 27: rf(\, R_{F(x_1,​\ldots,​x_n)}(t_1,​\ldots,​t_n) \,) = R_{F(t_1,​\ldots,​t_n)} ​ rf(\, R_{F(x_1,​\ldots,​x_n)}(t_1,​\ldots,​t_n) \,) = R_{F(t_1,​\ldots,​t_n)} ​ \end{array} \end{array} -$ + \end{equation*} 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. 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. ++++ ++++ Line 34: Line 34: ++++| ++++| We let We let - $+ \begin{equation*} ​T'​ = \{ F \mid rf(F) \in Conseq(T) \} ​T'​ = \{ F \mid rf(F) \in Conseq(T) \} -$ + \end{equation*} ++++ ++++