# Verifying axiom of substitution?

In Tao's analysis volume 1, I am introduced to this thing called the axiom of substitution. While constructing real numbers from rationals, he defined reals to be formal limits of Cauchy sequences of rationals. He said $$\lim a_n=\lim b_n$$ iff $$(a_n)$$ and $$(b_n)$$ are equivalent sequences. Then he defines addition of reals as - $$\lim a_n + \lim b_n=\lim(a_n+b_n)$$. Then he verifies that the axiom of substitution is not violated i.e. if $$x=x'$$ then $$x+y=x'+y$$. (I like to state this as "addition is well-defined").

My question : It seems that the axiom of substitution is a rather fundamental one that one needs to verify whenever a binary operation (such as addition) is introduced. However, not once in our course on group theory did we verify this axiom when we defined a binary operation on a set (and tried to show it forms a group). Shouldn't it be the first step?

• Based on this construction, you need to verify it when performing operations (or defining relations) on the real numbers because you've defined them via equivalence classes. But there are short cuts available. For example, if you define multiplication inductively from addition (I recognize you probably didn't do so for the reals), then the result you need for multiplication follows immediately from the result for addition. – Robert Shore Mar 7 at 16:48
• @RobertShore my question is that if $*$ is a binary operation given to us on a known set $S$ don't we have to verify that if $x=x'$ then $x*y=x'*y$? – Hrit Roy Mar 7 at 16:52
• In general no; if you have an operation $\text{op}$ defined between the elements of a mathematical structure, it is part of the underlying logic that the axioms for $=$ apply, and thus that we can freely substitute equals. – Mauro ALLEGRANZA Mar 7 at 17:02
• In the case above (as per previous comment) the issue is with the peculiar def of sum of limits; it is not evident that different "equivalent" sequences are interchangeable. – Mauro ALLEGRANZA Mar 7 at 17:04
• @MauroALLEGRANZA I'm sorry, I don't understand why we don't have to verify it. – Hrit Roy Mar 7 at 17:05

In this definition, real numbers are defined as equivalence classes of Cauchy sequences under an equivalence relation $$\sim$$, and then addition of real numbers is defined by first defining it on Cauchy sequences and then showing that it respects the equivalence relation (this is what "well-defined" means), so that it "descends" to equivalence classes.
If you're in a situation where you also need to define an operation on a set of equivalence classes $$X/\sim$$ by first defining it on $$X$$ and then showing that it respects $$\sim$$, then you also need to do this. But you don't always need to do this, because you aren't always working with equivalence classes. For example, the natural numbers $$\mathbb{N}$$ aren't defined in this way, and addition of natural numbers is formally defined in a completely different way, via induction.