22
$\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$
4
  • 3
    $\begingroup$ If I'm not mistaken, $=$ is defined as a relation that is symmetric, transitive and reflexive. $\endgroup$ Nov 6, 2015 at 17:25
  • 2
    $\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$ Nov 6, 2015 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, 2015 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$ Nov 6, 2015 at 17:46

4 Answers 4

30
$\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
  • 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$ Nov 6, 2015 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, 2015 at 19:48
  • 4
    $\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, 2015 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$ Nov 7, 2015 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$ Nov 7, 2015 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$
1
  • $\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$ Jun 14, 2016 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$
1
$\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$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .