Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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