Differences

This shows you the differences between two versions of the page.

--- sav08:axioms_for_equality [2008/04/01 23:27]
vkuncak
+++ sav08:axioms_for_equality [2008/04/02 22:46]
vkuncak
@@ Line 7: / Line 7: @@
   * Congruence for function symbols: for $f \in {\cal L}$ function symbol with $ar(f)=n$, ++ |
 \[
-   \forall x_1,\ldots,x_n, y_1,\ldots,y_n.\ (\bigwedge_{i=1}^n x_i = y_i) \rightarrow f(x_1,\ldots,x_n) = f(y_1,\ldots,y_n)
+   \forall x_1,\ldots,x_n, y_1,\ldots,y_n.\ (\bigwedge_{i=1}^n eq(x_i,y_i)) \rightarrow eq(f(x_1,\ldots,x_n),f(y_1,\ldots,y_n))
 \]
 ++
   * Congruence for relation symbols: for $R \in {\cal L}$ relation symbol with $ar(R)=n$, ++ |
 \[
-   \forall x_1,\ldots,x_n, y_1,\ldots,y_n.\ (\bigwedge_{i=1}^n x_i = y_i) \rightarrow (R(x_1,\ldots,x_n) \leftrightarrow R(y_1,\ldots,y_n))
+   \forall x_1,\ldots,x_n, y_1,\ldots,y_n.\ (\bigwedge_{i=1}^n eq(x_i,y_i)) \rightarrow (R(x_1,\ldots,x_n) \leftrightarrow R(y_1,\ldots,y_n))
 \]
 ++
+**Definition:** if an interpretation $I = (D,\alpha)$ the axioms $AxEq$ are true, then we call $\alpha(eq)$ (the interpretation of eq) a //congruence// relation for interpretation $I$.
+**Remark:** Functions are a special case of relations.  However, the condition above for function symbols is weaker than the condition for relation symbols.  If $f$ is a function, then the relation $\{(x_1,\ldots,x_n,f(x_1,\ldots,x_n)) \mid x_1,\ldots,x_n \in D \}$ does not satisfy the congruence condition because it only has one result, namely $f(x_1,\ldots,x_n)$, and not all the results that are in relation eq with $f(x_1,\ldots,x_n)$.
 ===== References =====
   * [[Calculus of Computation Textbook]], Section 3.1