LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Next revision Both sides next revision
sav08:axioms_for_equality [2008/04/02 00:43]
vkuncak
sav08:axioms_for_equality [2008/04/02 21:27]
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$. 
 + 
 +**A terminological note:** in algebra, an interpretation is often called a //​structure//​. Instead of using $\alpha$ mapping language ${\cal L} = \{ f_1,​\ldots,​f_n,​ R_1,​\ldots,​R_m\}$ to interpretation of its symbols, the structure is denoted by a tuple $(D,\alpha(f_1),​\ldots,​\alpha(f_n),​\alpha(R_1),​\ldots,​\alpha(R_n))$.  For example, an interpretation with domain ${\can N}$, with one binary operation whose interpretation is $+$ and one binary relation whose interpretation is $\leq$ can be written as $({\cal N},​+,​\leq)$. ​ This way we avoid writing $\alpha$ all the time, but it becomes more cumbersome to describe correspondence between structures.
  
 === Example: quotient on pairs of natural numbers === === Example: quotient on pairs of natural numbers ===
Line 33: Line 35:
 is a congruence with respect to operations $p$ and $m$.  ​ is a congruence with respect to operations $p$ and $m$.  ​
  
-Congruence is an equivalence relation. ​ What is the equivalence ​class for element $(1,​1)$?  ​+Congruence is an equivalence relation. ​ What are equivalence ​classes ​for elements:
  
-$[(1,1)] = $ ++| $\{ (x,y) \mid x=y \}$+$[(1,1)] = $ ++| $\{ (x,y) \mid x=y \}$++
  
-$[(10,1)] = $ ++| $\{ (x,y) \mid x=y+9 \}$+$[(10,1)] = $ ++| $\{ (x,y) \mid x=y+9 \}$++
  
-$[(1,10)] = $ ++| $\{ (x,y) \mid x+9=y \}$+$[(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:+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 ​$([N^2], I_Q)$ we define operations $p$ and $m$ such that the following holds:
 \[ \[
 \begin{array}{l} \begin{array}{l}
-   p( [(x_1,y_1)] , [(x_2,y_2)] ) = [(x_1 + x_2, y_1 + y_2)] \\ +   I_Q(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)] +   I_Q(m)( [(x_1,y_1)] , [(x_2,y_2)] ) = [(x_1 + y_2, y_1 + x_2)] 
 \end{array} \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. ++ 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. ++
 +
 +Note: this construction can be applied whenever we have an associative and commutative operation $*$ satisfying the cancelation law $x * z = y * z \rightarrow x=y$.  It allows us to contruct a structure where operation $*$ has an inverse. ​ What do we obtain if we apply this construction to multiplication of strictly positive integers?
  
 ===== References ===== ===== References =====
   * [[Calculus of Computation Textbook]], Section 3.1   * [[Calculus of Computation Textbook]], Section 3.1