Is equality inherently defined?
Solution 1:
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.
Solution 2:
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.
Solution 3:
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.