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:06] vkuncak |
sav08:interpretation_quotient_under_congruence [2008/04/02 22:09] vkuncak |
||
|---|---|---|---|
| Line 74: | Line 74: | ||
| **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$, the relation $\alpha_Q(f)$ is a total function on $[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)]$. | ||
| - | **Theorem:** For each formula $F$ that contains no '=' symbol (it may contain 'eq'), we have $e_F(F)(I_Q) = e_F(F)(I)$. | + | **Theorem:** For each formula $F$ that contains no '=' symbol, we have $e_F(F)(I) = e_F(F)(I_Q) = e_F(F_0)(I_Q)$ where $F_0$ is result of replacing 'eq' with '=' in $F$. |