Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:extending_languages_of_decidable_theories [2008/04/15 14:26] vkuncak |
sav08:extending_languages_of_decidable_theories [2008/04/15 14:27] vkuncak |
||
---|---|---|---|
Line 7: | Line 7: | ||
**Proof:** | **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. | 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. | ||
Line 37: | Line 38: | ||
\] | \] | ||
+ | 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). | 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). | ||
+ | ++++ | ||
++++ | ++++ |