• 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)
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*}
++++ ++++