Lab for Automated Reasoning and Analysis 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] (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*}
 ++++ ++++
  
 
sav08/extending_languages_of_decidable_theories.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice