Some further remarks: you'll find that deriving mathematical theorems is strikingly similar to doing natural deduction (not by chance: Gentzen was inspired by actual mathematical reasoning in setting up his system). So, if you really want to, you can try to convert an informal proof into a natural deduction one. For instance, let's analyze your little deduction a bit more closely. Step 2, which you called "Subtraction Introduction", is actually an instantiation of a general logic rule, which can be formally states as:
$\forall x \forall y \forall z (y = z \rightarrow f(x, y) = f (x, z))$
(The above rule is given as an "equality axiom" in Shoenfield's *Mathematical Logic", for instance; cf. p. 21).
So, in your above proof, you could introduce this axiom as a premiss in your preferred natural deduction system, signaling the dependence of what comes next on this line (that's generally not a problem, as your derivations will typically depend on the axioms of whatever theory you're working with plus the logical axioms).
Now, going to step three, there are actually two steps there: you are instantiating a field axiom to $7$ (specifically, the existence of an inverse axiom: $\forall x \exists y (x + y = 0)$) and then using term substitution (I think Shoenfield calls it the "equality theorem" in his book; cf. p. 35) to replace $+(7, -7)$ by $0$; similarly, in step 4, you're substituting $+(11, -7)$ by $4$. On step 5, you're using another field axiom, namely the existence of an identity element ($\exists x \forall y (x + y = y)$), and again substitution, to obtain $2x$ from $+(2x, 0)$. On step 6., you're using the existence of an inverse to multiplication and the logical rule referred above to introduce division. Finally, both step 7 and 8 use substitution. Let's try to put this into a natural deduction system (I'll just sketch a more or less Fitch style deduction here).
So, in order to codify this more neatly into a natural deduction, I'll take the above equality axiom (let's call it EA) also substitution (let's call it SUB) as rules of inference. I'll also use the following axioms, listed above (let's assume that the underlying theory is the field of reals; for simplicity, let's also assume that the language has constants to denote all the real numbers; I'll not use all of the field axioms, just the relevant ones).
A1. $\forall x \forall y \forall z ((x + y) + z = x + (y + z))$;
A2. $\forall y (0 + y = y)$;
A3. $\forall x \exists y (x + y = 0)$;
A4. $\forall x (x \not = 0 \rightarrow (\exists y (x \cdot y = 1)))$
Now, from the above axioms and the rules of inference it's possible to show that the $y$ in both A3. and A4. is unique for each real number, so we can introduce constants to denote them. It's also possible to show that subtraction and division are possible by carefully choosing our substitution instances (e.g. the possibility of subtraction can be said to consist in the fact that the following sentence holds in the structure: $\forall x \forall y \exists z (x + z = y)$; we can show that this holds by choosing $z = (-x + y)$). Here, I'll just assume that this can be all be "read off" from those axioms.
So we would have something like:
- $\exists x (2x + 7 = 11)$ Assumption;
2.$2a + 7 = 11$ 1, Existential Elimination;
- $(2a + 7) + (-7) = 11 + (-7)$ 2, EA;
- $2a + (7 + (-7)) = 11 + (-7)$ 3, A1;
- $7 + (-7) = 0$ A3 (by definition, (-7) denotes the inverse of 7);
- $2a + 0 = 11 + (-7)$ 4, 5, SUB;
- $2a = 11 + (-7)$ 6, A2
- $11 + (-7) = 4$ A2, A3 (by the theorem which states the possibility of subtraction,
- $2a = 4$ 7, 8, SUB;
- $2a/2 = 4/2$ 9, EA;
- $2a/2 = a$ A4 (by the possibility of division, actually);
- $4/2 = 2$ A4 (same as above)
- $a = 4/2$ 10, 11, SUB;
- $a = 2$ 12, 13, SUB;
Anyway, that was a bit rough, but it should give you some idea about how to do it. As I said, I strongly recommend reading chapter 7 of Suppes's book, which provides a nice transition from natural deduction proofs (which are dealt with in a more relaxed manner in his book) to informal mathematical proofs.