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:interpretation_quotient_under_congruence [2008/04/02 22:08] vkuncak |
sav08:interpretation_quotient_under_congruence [2008/04/02 22:20] vkuncak |
||
---|---|---|---|
Line 70: | Line 70: | ||
\[ | \[ | ||
\alpha_Q(x) = [\alpha(x)] | \alpha_Q(x) = [\alpha(x)] | ||
+ | \] | ||
+ | |||
+ | **Lemma 0:** For all $x_1,\ldots,x_n \in D$, | ||
+ | \[ | ||
+ | ([x_1],\ldots,[x_n]) \in \alpha_Q(R) \mbox{ iff } (x_1,\ldots,x_n) \in \alpha(R) | ||
\] | \] | ||
**Lemma 1:** $I_Q = ([D],I_Q)$ is a well-defined interpretation, that is, | **Lemma 1:** $I_Q = ([D],I_Q)$ is a well-defined interpretation, that is, | ||
- | * $[D]$ is non-empty | + | * $[D]$ is non-empty; |
- | * for each function symbol $f$, the value $\alpha_Q(f)$ is a graph of a total function on $[D]$ | + | * for each function symbol $f$ with $ar(f)=n$, the relation $\alpha_Q(f)$ is a total function $[D]^n \to [D]$. |
**Lemma 2:** For each term $t$ we have $e_T(t)(I_Q) = [e_T(t)(I)]$. | **Lemma 2:** For each term $t$ we have $e_T(t)(I_Q) = [e_T(t)(I)]$. |