What is really happening when we do substitution in math

Question

Consider a toy case. Suppose we have a+b=10. This basically informs us a relation between two unknown variables a and b, however there is not enough information for us to tell what values do a and b take.

Now suppose we have another piece of information a=4. The standard way of combining the two pieces is by substitution into a+b=10 and we get 4+b=10. Then through math manipulation we can conclude b=6.

But what exactly is happening when we do the substitution? Intuitively if when we substitute a math object in a math statement with another equivalent object the resulting new math statement should be equivalent as before. Is there a better or simpler explanation for this? And is there an axiom?

Answer 1

The "equation":

$a + b =10$

is ambiguous. What are we asserting, when stating it ?

Probably not: $\forall a \ \forall b \ (a+b=10)$, which is quite useless.

Stating the problem as: "given $a + b =10$ and let $a=4$, find $b$", sounds like:

check if $\exists b \ (a+b=10)$ is satisfiable in a certain domain (like e.g. $\mathbb N$) when $a=4$.

In this case the question is meaningful; we substitute $4$ for $a$ (foramlly: we instantiate a free variable with a value) and get: $\exists b \ (4+b=10)$ which is satisfied in $\mathbb N$ for $b=6$.

---

In a formal way, we have to use (as per comment above) the first-order logic with equality substitution axiom (for formulas):

$x=y \to (\varphi \to \varphi')$

where $\varphi'$ is obtained by replacing any number (not necessarily all) of the free occurrences of $x$ in $\varphi$ with $y$.

To be pedantic, we have first to prove (by induction) the "generalized form":

$t_1=t_2 \to (\varphi \to \varphi')$

with $t_i$ terms, because $4$ is not a variable in the language of first-order arithmetic.

Now the substitution will be:

1) $a+b=10$ --- it is $\varphi$

2) $a=4$

3) $\vdash a=4 \to ((a+b=10) \to (4+b=10))$ ---suitable instance of the equality substituion axiom

4) $4+b=10$ --- it is $\varphi'$ : from 1),2) and 3) by modus ponens twice.