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:axioms_for_equality [2008/04/02 00:42] vkuncak |
sav08:axioms_for_equality [2009/05/05 23:21] vkuncak |
||
---|---|---|---|
Line 7: | Line 7: | ||
* Congruence for function symbols: for $f \in {\cal L}$ function symbol with $ar(f)=n$, ++ | | * 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$, ++ | | * 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)) |
\] | \] | ||
++ | ++ | ||
- | Note: if an interpretation $(D,I)$ satisfies $AxEq$, then we call $e_F(I)(eq)$ (the interpretation of eq) a //congruence// relation for $(D,I)$. | + | **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$. |
- | === Example: quotient on pairs of natural numbers === | + | **Side remark:** Functions are 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)$. However, if we start from the condition for functions and treat relations as functions that return true or false, we obtain the condition for relations. So, it makes sense here to treat relations as a special case of functions. |
- | + | ||
- | Let ${\cal N} = \{0,1,2,\ldots, \}$. Consider a structure with domain $N^2$, with functions | + | |
- | \[ | + | |
- | p((x_1,y_1),(x_2,y_2)) = (x_1 + x_2, y_1 + y_2) | + | |
- | \] | + | |
- | \[ | + | |
- | m((x_1,y_1),(x_2,y_2)) = (x_1 + y_2, y_1 + x_2) | + | |
- | \] | + | |
- | Relation $r$ defined by | + | |
- | \[ | + | |
- | r = \{((x_1,y_1),(x_2,y_2)) \mid x_1 + y_2 = x_2 + y_1 \} | + | |
- | \] | + | |
- | is a congruence with respect to operations $p$ and $m$. | + | |
- | + | ||
- | Congruence is an equivalence relation. What is the equivalence class for element $(1,1)$? | + | |
- | + | ||
- | $[(1,1)] = $ ++| $\{ (x,y) \mid x=y \}$ | + | |
- | + | ||
- | $[(10,1)] = $ ++| $\{ (x,y) \mid x=y+9 \}$ | + | |
- | + | ||
- | $[(1,10)] = $ ++| $\{ (x,y) \mid x+9=y \}$ | + | |
- | + | ||
- | Whenever we have a congruence in an interpretation, we can shrink the structure to a smaller one by merging elements that are in congruence. In the resulting structure we can define operations $p$ and $m$ such that the following holds: | + | |
- | \[ | + | |
- | \begin{array}{l} | + | |
- | p( [(x_1,y_1)] , [(x_2,y_2)] ) = [(x_1 + x_2, y_1 + y_2)] \\ | + | |
- | m( [(x_1,y_1)] , [(x_2,y_2)] ) = [(x_1 + y_2, y_1 + x_2)] | + | |
- | \end{array} | + | |
- | \] | + | |
- | This construction is an algebraic approach to construct from natural numbers one well-known structure. Which one? ++| $({\cal Z}, + , -)$ where ${\cal Z}$ is the set of integers.$ | + | |
===== References ===== | ===== References ===== | ||
* [[Calculus of Computation Textbook]], Section 3.1 | * [[Calculus of Computation Textbook]], Section 3.1 | ||