Say $a=b$. Is "Do the same thing to both sides of an equation, and it still holds" an axiom? [duplicate]

Recently I have started reviewing mathematical notions, that I have always just accepted. Today it is one of the fundamental ones used in equations:

If we have an equation, then the equation holds if we do the same to both sides.

This seems perfectly obvious, but it must be stated as an axiom somewhere, presumably in formal logic(?). Only, I don't know what it would be called, or indeed how to search for it - does anybody knw?

Solution 1:

This axiom is known as the substitution property of equality. It states that if $f$ is a function, and $x = y$, then $f(x) = f(y)$. See, for example, Wikipedia.

For example, if your equation is $4x = 2$, then you can apply the function $f(x) = x/2$ to both sides, and the axiom tells you that $f(4x) = f(2)$, or in other words, that $2x = 1$. You could then apply the axiom again (with the same function, even) to conclude that $x = 1/2$.

Solution 2:

"Do the same to both sides" is rather vague. What we can say is that if $f:A \rightarrow B$ is a bijection between sets $A$ and $B$ then, by definition

$\forall \space x,y \in A \space x=y \iff f(x)=f(y)$

The operation of adding $c$ (and its inverse subtracting $c$) is a bijection in groups, rings and fields, so we can conclude that

$x=y \iff x+c=y+c$

However, multiplication by $c$ is only a bijection for certain values of $c$ ($c \ne 0$ in fields, $\gcd(c,n)=1$ in $\mathbb{Z}_n$ etc.), so although we can conclude

$x=y \Rightarrow xc = yc$

it is not safe to assume the converse i.e. in general

$xc=yc \nRightarrow x = y$

and we have to take care about which values of $c$ we can "cancel" from both sides of the equation.

Some polynomial functions are bijections in $\mathbb{R}$ e.g.

$x=y \iff x^3=y^3$

but others are not e.g.

$x^2=y^2 \nRightarrow x = y$

unless we restrict the domain of $f(x)=x^2$ to, for example, non-negative reals. Similarly

$\sin(x) = \sin(y) \nRightarrow x = y$

unless we restrict the domain of $\sin(x)$.

So in general we can only "cancel" a function from both sides of an equation if we are sure it is a bijection, or if we have restricted its domain or range to create a bijection.

Solution 3:

There is a way in which it is an axiom, and another in which it isn't. I'll try to describe both.

When you do formal logic and start with variables ($x_1,...,x_n,...$), relation symbols ($R_i, i\in I$) and function symbols ($f_j, j\in J$). You build out your formulas with these. An important notion is that of a term in this language. A term is defined recursively as either a variable, or a string of the form $f_j(t_1,...,t_n)$ where $f_j$ is a function symbol of arity $n$ and $t_1,...,t_n$ are terms (this is purely syntactical).

Then you build a deduction system that consists in rules that you may apply in certain situations (for instance if you proved $A$ and $B$, you can prove $A\land B$).

One of these rules is the substitution rule: one way to define it is the following : for any terms $t_1,...,t_n, u_1,...,u_n$ and any function symbol $f$ of arity $n$, if for all $i$, $t_i = u_i$ is proved then one may deduce $f(t_1,...,t_n) = f(u_1,...,u_n)$

In this situation it is an axiom.

However in the common situation of algebra and "the working mathematician", it is a consequence of another substitution rule, the substitution rule for relation symbols. Indeed, all maths can be built from set theory with no function symbol and only one relation symbol ($\in$). In this setting a function $A\to B$ is defined (for instance) as a subset $f$ of $A\times B$ such that for all $x\in A$, there is a unique $b\in B$ such that $(a,b)\in f$. $f(a)$ is then defined as this unique $b$

Now if $x=y \in A$, $f:A\to B$ is a function, then $(x,f(x)) \in f$ and $(y,f(y))\in f$ and so by the substitution rule for relation symbols $(x,f(y))\in f$, so that $f(x)=f(y)$ (by uniqueness).

The substitution rule for relation symbols is very similar to the one for function symbols and is, again an axiom: it can be described as: if $t_1,...,t_n,u_1...,u_n$ are terms, $R$ is a relation symbol of arity $n$; if for all $i$, $t_i= u_i$ has been proved and $R(t_1,...,t_n)$ has been proved, then one may deduce $R(u_1,...,u_n)$

(you may see that the rule is not so far from an axiom, but technically it's not one in this second situation)