- English only

# Lab for Automated Reasoning and Analysis LARA

# 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*} |

++++ | ++++ | ||