Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:axioms_for_equality [2009/05/05 23:16] vkuncak |
sav08:axioms_for_equality [2009/05/06 09:52] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Axioms for Equality ====== | ====== Axioms for Equality ====== | ||
| + | |||
| + | //The following definitions are useful when axiomatizing equality in a logic that does not have equality built in. It is also useful when discussing algorithms that automate reasoning about equality.// | ||
| For language ${\cal L}$ and a relation symbol $eq \notin {\cal L}$, the theory of equality, denoted AxEq, is the following set of formulas: | For language ${\cal L}$ and a relation symbol $eq \notin {\cal L}$, the theory of equality, denoted AxEq, is the following set of formulas: | ||
| Line 18: | Line 20: | ||
| **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$. | **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$. | ||
| - | **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)$. | + | **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. |
| ===== References ===== | ===== References ===== | ||
| * [[Calculus of Computation Textbook]], Section 3.1 | * [[Calculus of Computation Textbook]], Section 3.1 | ||