I recently pulled out my old Real Analysis textbook and noticed something that didn't stand out when I was taking the class all those years ago. When the book is listing out the axioms it seems to assume we understand what equality is.
Consider the first axiom $(A)$, which defines commutivity over addition and multiplication. It states
$x+y=y+x, \forall x,y \in \mathbb{R}$
and similiarly for multiplication. I understand that we're in process of defining how $+$ operates on $\mathbb{R}$ here, but we never defined what $=$ means. Equality seems like a crucial concept, but I never see it defined anywhere.
Is equality inherently defined or an understood concept, or does it have a more formal definition?
EDIT
It was commented that $x+y$ is not the same as $y+x$, but rather for the case above they could be considered equal if they evaluate to the same real number. My question has to do with the general sense, though. It seems this axiom is defining a property of $+$ to say that these two terms can be treated the same, an idea which could be applied in other situations outside of the example of the $+$ operation and $\mathbb{R}$.
$\endgroup$ 44 Answers
$\begingroup$You're right -- the formal properties of equality need to be defined somewhere.
The properties we need are the pure equality axioms: $$ x=x \qquad x=y\Rightarrow y=x \qquad x=y\land y=z\Rightarrow x=z, $$plus the crucial property that we're allowed to substitute equals for equals in an expression and not change the meaning: $$ x=y \Rightarrow f(x)=f(y) $$
The latter property is a bit tricky to express formally because we don't yet have the machinery to speak about arbitrary functions (and developing this machinery generally depends on having equality working already). So what one does instead is to have a whole slew of axioms for each primitive operation in our theory: $$ x=y \Rightarrow x+z=y+z \qquad x=y \Rightarrow z+x=z+y \\ x=y \Rightarrow x\times z=y\times z \qquad x=y \Rightarrow z\times x=z\times y \\ x=y \Rightarrow -x = -y \\ x=y \Rightarrow (x<z \Leftrightarrow y<z) \qquad x=y \Rightarrow (z<x \Leftrightarrow z<y) $$ and so forth. And each time we add a new operator or relation symbol this kind of equality rules should also be added for it.
Because this adding of new equality axioms for each symbol is completely mechanical, it is generally more convenient in formal logic to consider that a part of the rules of logic rather than a part of the theory we're building atop the logic, so it doesn't have to be stated each time a new symbol is introduced.
This is probably why the author of your text did not think they needed to be pointed out explicitly -- though if asked, he would probably claim he's not assuming any familiarity with formal logic.
$\endgroup$ 8 $\begingroup$Two sets are equal if they are the same, i.e. contains the same elements.
So in your context, $x+y=y+x$ for all $x,y \in \mathbb R$ means that the two sets $x+y$ and $x+y$ are the same. In fact there are many ways to define the reals. At least Dedekind cuts, or via Cauchy sequences. In all cases, a real is a set (usually a subset of the rationals)
So to prove that $x+y=y+x$ you'll have to prove that both sets (i.e. subsets of the rationals) are equal.
$\endgroup$ 1 $\begingroup$Your example uses equality of the values obtained from performing the operations. If we do not use infix notation it would read $$ +(x,y) = +(y,x) \quad (x,y \in \mathbb{R}) $$ Considered as a function, we would say that addition is symmetric.
The Wikipedia article on Equality gives a lot of contexts and their special views on equality, including a logical formalization by Lévy.
I would also like to point to Equality Comparisons and Sameness which show what practical problems arise for the object oriented part of the JavaScript language. Because for a machine every bit needs to be spelled out and this has consequences.
- We have strict equality "===" which (roughly said) insists on type equality and equal values.
- loose equality "==" which needs same values (after possible type conversion to a common type).
- same-value equality which is the "functional equality", you can switch such equal objects and they should result in the same program behaviour if they are considerd such equal (Liskov substitution)
Then there lurks the question of just comparing two objects who happen to have the same values, but are two different entities in memory vs having the same object given to both sides of an equality comparison (identity).
This relates to duck typing, where one considers objects that respond to the same messages (or method calls) the same as equal for use.
$\endgroup$ $\begingroup$In general, all you really need for $=$ (as Henning Makholm details) is (1) that it is an equivalence relation, and (2) that every function and relation agrees with equality.
However, you may also assume (as in model theory) that any list of axioms are statements about some set, or model of those axioms. In this case $=$ automatically means equality in that set--distinct elements of the set are nonequal.
This raises the question: if we assume that everything is a set, and $=$ is equality of sets, then how is $=$ defined in set theory? As it turns out, you don't need to state axioms for $=$ separately; you can just define explicitly that $X = Y$ whenever it is the case that $$ (\forall a \in X : a \in Y) \land (\forall a \in Y : a \in X). $$ You can in fact prove (say, in ZFC) that under this definition $=$ satisfies the necessary properties of (1) being an equivalence relation and (2) being able to substitute equals for equals.
