15
$\begingroup$

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$
  • 3
    $\begingroup$ If I'm not mistaken, $=$ is defined as a relation that is symmetric, transitive and reflexive. $\endgroup$ – MoebiusCorzer Nov 6 '15 at 17:25
  • 1
    $\begingroup$ @mvw, that's all well and good, but you still have to define what the equality operator is. After that, you can consider different types of equality. Good link, though. $\endgroup$ – gregsdennis Nov 6 '15 at 17:25
  • 1
    $\begingroup$ I removed the "operator theory" tag, since operator theory (as described in the tag) is a branch of functional analysis. I added the "logic" tag, although I am not completely sure whether it fits. $\endgroup$ – PhoemueX Nov 6 '15 at 17:32
  • 1
    $\begingroup$ @gregsdennis You can just treat it as a formal symbol, if you like, meaning nothing inherently but happening to correspond to our intuitive notion of "equality". The axioms dictate how "=" behaves. $\endgroup$ – Patrick Stevens Nov 6 '15 at 17:46
23
$\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$
  • 4
    $\begingroup$ This is excellent. I actually need this as part of a program I'm writing, and your explanation translates to programming perfectly. $\endgroup$ – gregsdennis Nov 6 '15 at 17:58
  • 1
    $\begingroup$ @gregsdennis, although it may be far above and beyond what you need right now, there's a big area of math devoted to understanding the subtleties of how equality works in programming. It's called homotopy type theory. [cont. ...] $\endgroup$ – Vectornaut Nov 6 '15 at 19:48
  • 3
    $\begingroup$ [... cont.] Unfortunately, it's hard to find references that are even remotely accessible to mortals, but the paper "Homotopical Patch Theory" (homotopytypetheory.org/2014/09/01/homotopical-patch-theory) may be within reach if you have a step ladder. This blog post (bartoszmilewski.com/2013/07/29/quantum-homotopy-computer) also has some introductory intuition mixed in with the wild speculation; see in particular sections "Relaxing Equality" through "Computers Hate Sets." $\endgroup$ – Vectornaut Nov 6 '15 at 19:49
  • 1
    $\begingroup$ I don't know whether this would help or hurt with the 'trickiness to express' or let you sidestep the writing of many nearly identical substitution rules, but what if you made substitution apply to statements (provided the thing you're renaming is not bound or something) as opposed to terms? Is there a convincing reason why not? (perhaps the two notions of equality are not themselves equivalent because 'quantifying' over predicates is somehow worse than doing so over functions? Foundations have always spelled 'here be dragons!' for me, but I wish I understood more!) $\endgroup$ – Vandermonde Nov 7 '15 at 1:43
  • 1
    $\begingroup$ @Vandermonde: Yes, with a substitution concept in place (which you need anyway to deal with quantifiers), it would certainly be viable just to have a single rule: $$ s=t \implies (\phi[x\mapsto s] \Rightarrow \phi[x\mapsto t]) $$ This might be the most convenient way to go if you're doing automated reasoning, though it may complicate how you introduce new function and relation symbols. My answer here was more from the perspective of meta-reasoning, where even a proliferation of simple equality axioms is often thought of as less onerous to deal with than a big substitution-based one. $\endgroup$ – Henning Makholm Nov 7 '15 at 1:53
1
$\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$
  • $\begingroup$ "Two sets are equal if they are the same" Isn't this statement a tautology? It's like saying that "Green objects are defined as those which are green". Let's suppose I want to know if two sets are equal. According to your (circular) definition, this question changes into finding out if they are the same. But isn't it the same question? :P Now I need the definition of "sameness", which is pretty much... the same... :P $\endgroup$ – BarbaraKwarc Jun 14 '16 at 18:48
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$
0
$\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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.