LARA

Differences

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

Link to this comparison view

sav08:extending_languages_of_decidable_theories [2008/04/15 14:27]
vkuncak
sav08:extending_languages_of_decidable_theories [2015/04/21 17:30]
Line 1: Line 1:
-===== Extending Languages of Decidable Theories ===== 
- 
-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}$. 
- 
-**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. 
- 
-Let ${\cal F}$ denote the set of formulas in language ${\cal L}$.  Define 
-\[ 
-    L' = \{ R_{F} \mid F \in {\cal F} \} 
-\] 
-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 
-\[ 
-\begin{array}{l} 
-   ​rf(F_1 \land F_2) = R_{rf(F_1) \land rf(F_2)} \\ 
-   ​rf(F_1 \lor F_2) = R_{rf(F_1) \lor rf(F_2)} \\ 
-   ​rf(\lnot F_1) = R_{\lnot rf(F_1)} \\ 
-   ​rf(\forall x. F_1) = R_{\forall x.rf(F_1)} \\ 
-   ​rf(\exists x. F_1) = R_{\exists x.rf(F_1)} \\ 
-   rf(\, R_{F(x_1,​\ldots,​x_n)}(t_1,​\ldots,​t_n) \,) = R_{F(t_1,​\ldots,​t_n)} ​ 
-\end{array} 
-\] 
-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. 
-++++ 
- 
-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). 
-++++ 
- 
-**End Proof.** 
- 
-Question: When is the question $F \in Conseq(T'​)$ for $T'$ from the proof decidable for ground formulas? ++|exactly when $F \in Conseq(T)$ is decidable.++ 
- 
-Note: often we can have nicer representations instead of $R_F$, but this depends on particular theory.