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 73: | Line 73: | ||
**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)]$. | ||
- | **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$. |