How is variable substitution taken into account in natural deduction?

Question

My question concerns variable substitution in natural deduction. As an example, if one wants to prove:

$T_R, ((a + c = b + c) \to a = b) \vdash (a = b \to (a + c = b + c))$

where $T_R$ is the axioms of the real numbers, then I suppose one would write the proof something like this:

1. $(a + c = b + c) \to a = b \vdash (a + c = b + c) \to a = b$ --- [Axiom rule]
2. $x = a + c \vdash x = a + c$ --- [Axiom rule]
3. $y = b + c \vdash y = b + c$ --- [Axiom rule]
4. $T_R, x = a + c \vdash a = x + (-c)$ --- [Derivable from field axioms]
5. $T_R, y = b + c \vdash b = y + (-c)$ --- [Derivable from field axioms]
6. $a = b \vdash a = b$ --- [Axiom rule]
7. $T_R, x = a + c, y = b + c, a = b \vdash x + (-c) = b$ --- [=E: 4, 6]
8. $T_R, x = a + c, y = b + c, a = b \vdash x + (-c) = y + (-c)$ --- [=E: 5, 7]
9. $T_R, x = a + c, y = b + c, ((a + c = b + c) \to a = b), a = b \vdash x = y$ --- [Modus ponens from 1 and 8]
10. $T_R, x = a + c, y = b + c, ((a + c = b + c) \to a = b), a = b \vdash a + c = y$ --- [=E: 4, 9]
11. $T_R, x = a + c, y = b + c, ((a + c = b + c) \to a = b), a = b \vdash a + c = b + c$ --- [=E: 5, 10]
12. $T_R, x = a + c, y = b + c, ((a + c = b + c) \to a = b) \vdash a = b \to (a + c = b + c)$ --- [${\to}I$: 11]

The problem obviously is how to discharge the $x = a + c$ and $y = b + c$ conditions. Some have told me that such statements do not need to be introduced as assumptions, you just wave your hand somehow and it works. This doesn't seem satisfactory to me. How can you get to lines 7 and 8 without introducing the assumptions in 2 and 3? And if this is correct, then how do I discharge them? If not correct, what is the actual mechanism that allows us to go to lines 7 and 8. Surely there must be some law or rule of inference that validates this move.

Answer 1

I think that you can simplify it:

1) $a=b$ --- assumption [a]

2) $\vdash a+c=a+c$ --- $=$I (no assumptions)

3) $a+c=b+c$ --- from 1) and 2) by $=$E, where $a+c=x+c$ is $\phi$, 2) is $\phi[a/x]$ and 3) is $\phi[b/x]$

4) $\vdash a=b \to (a+c=b+c)$ --- from 1) and 3) by $\to$-intro, discharging [a].

As you can see, we need only the rules for $=$ and no non-logical axioms.

---

There is nothing peculiar regardind substitution in Natural Deduction.

We have only to avoid being misleaded by the symbolism; usually, when we write $\phi[t/x]$ we are meaning that all the free occurrences of $x$ in $\phi$ are replaced with $t$.

This symbolism may "force" us to an unnecessary restriction in the substitution rule for formulas that, in axiomatic form, is:

$x = y → (\phi → \phi')$, where $\phi'$ is obtained by replacing any number [i.e. zero or more, but not necessarily all] of free occurrences of $x$ in $\phi$ with $y$.