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:25] 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 28: | Line 29: | ||
| \] | \] | ||
| 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. | ||
| + | ++++ | ||
| - | We then let | + | How to define $T'$? |
| + | ++++| | ||
| + | We let | ||
| \[ | \[ | ||
| T' = \{ F \mid rf(F) \in Conseq(T) \} | T' = \{ F \mid rf(F) \in Conseq(T) \} | ||