Proving $n+n=2n$ step-by-step My kids asked me a simple question, to prove step-by-step with no "leaps" that:
$$n+n=2n$$
(I think they heard about Bertrand Russell's hundred-page proof of $1+1=2$ and wanted to troll me). So here's my first attempt…

Assuming $n$, $a$, and $b$ are members of a ring with two binary operators $+$ and $×$ denoting addition and multiplication, then:
$n+n$
$\quad=n×1+n×1\qquad$ Multiplicative Identity: $n=n×1$
$\quad=n×(1+1)\qquad\qquad$ Distributivity Property: $n×a+n×b=n×(a+b)$
$\quad=n×(2)\qquad\qquad\qquad$ Conventional Addition Operation: $1+1=2$
$\quad=n×2\qquad\qquad\qquad$ ??? Property: $(a)=a$ ①
$\quad=2×n\qquad\qquad\qquad$ Multiplicative Commutativity: $a×b=b×a$
$\quad=2n\qquad\qquad\qquad\qquad$ Notation Convention: $a×b=ab$
Obviously, starting with a ring gets me to a good place right away, but otherwise am I making any "leaps"? Is there a specific name for ①? (Also is there a way to format a straight edge for the rules?)
 A: My understanding is that ① is the basic of multiplication, and can be referred to as such. There don't seem to be any leaps in logic, but proving 1+1=2 would help support your proof.
A: Your property ① is not really a theorem you can quote or anything, it's really
just what this parenthesis notation means by definition. If you wanted to
completely avoid this ambiguity, you could just use some notation other than
infix notation. In postfix notation, for example, you could write
n n + = n 1 × n 1 × +
      = n 1 1 + ×
      = n 2 ×
      = 2 n ×

although that's obviously
quite ugly. Perhaps more naturally, you could let $A(a, b) := a + b$, and
$M(a, b) := a \cdot b$. Then your argument becomes
\begin{align*}
 A(n, n)
  &= A(M(n, 1), M(n, 1)) \\
  &= M(n, A(1, 1)) \\
  &= M(n, 2) \\
  &= M(2, n)
\end{align*}
Neither of these alternatives really add anything to your proof though, this is
purely a matter of notation.
Your approach is good, but I think it would be a bit closer to Russel's work to
just prove this for the natural numbers. This is also more fun if you have the
inclination because it really involves (partially) proving $\mathbb N$ is a
(semi-)ring in the first place.
Here I present a somewhat legible way you might do something like this. This is
a bit less formal than some might like, but my thinking was that in making this
too formal, little rigour is gained, and it just becomes harder to understand.
Definitions
The natural numbers are a set $\mathbb N$ such that


*

*There is a number $0 \in \mathbb N$

*There is a bijective "successor" function
$S: \mathbb N \to \mathbb N \setminus \{0\}$. (Think of $S(n)$ as $n + 1$ even
though we haven't defined that yet).

*If $P(n)$ is some statement about numbers, then if $P(0)$, and
$\forall n \in \mathbb N, P(n) \implies P(S(n))$, it must be the case that
$\forall n \in \mathbb N, P(n)$. This tells us proof by induction works, and
importantly, this is an axiom of the natural numbers. It's a fundamental
truth you're allowed to assume.
What motivates induction is that it sort of formalises the idea of "doing
something $n$ times" (which isn't rigorously defined). You'll notice that in
my proofs here I never say "and so on" or "repeat this $n$ times" or
"$\dots$". Intuitively, induction is just the formal way to express any of
those ideas.

*There is a binary operation $+: \mathbb N^2 \to \mathbb N$ defined recursively
by $a + 0 := 0$, $a + S(b) := S(a + b)$. This indeed gives rise to the
addition you know and love, but because our definition is so rigorous, we will
need to
prove obvious properties about it.

*There is a binary operation $\cdot: \mathbb N^2 \to \mathbb N$ defined
recursively by $a \cdot 0 := 0$, $a \cdot S(b) := a + (a \cdot b)$. (This is
multiplication)


By the way, $2$ and $1$ are just labels we use for $S(S(0))$ and $S(0)$
respectively. This makes it quite easy to prove $1 + 1 = 2$, just by applying
the definition of $+$. Most of Russel's work was in defining the logical system
(his type theory) that he was using to express all of these concepts.
Another fundamental thing we need to assume is that if $x = y$, then whenever
$x$ occurs, we can replace it with $y$, and vice versa. There are in fact a lot
of underlying assumptions, like $=$ being an equivalence relation, or how you
prove implications or statements involving quantifiers, but I am assuming that
you don't actually want to build up all of mathematics from the ground up.
If you were paying attention, you might have noticed that $n + n = n \cdot 2$ is
actually very easy to prove, since by definition,
\begin{align*}
n \cdot 2
  &= n \cdot S(S(0)) \\
  &= n + n \cdot S(0) \\
  &= n + (n + n \cdot 0) \\
  &= n + (n + 0) \\
  &= n + n
\end{align*}
However, I have graciously decided to define multiplication recursively on the
right argument, so that there is actually something to prove.
Lemma 1: $\forall a, b \in \mathbb N, S(a) + b = S(a + b)$
By induction on $b$. Given $a \in \mathbb N$, indeed
$S(a) + 0 = S(a) = S(a + 0)$, applying the definition of $+$. This establishes
the base case.
Given $b \in \mathbb N$, and supposing that $S(a) + b = S(a + b)$, we then have
$S(a) + S(b) = S(S(a) + b) = S(S(a + b)) = S(a + S(b))$, applying the inductive
hypothesis and definition of $+$. Hence, by induction, we are done.
Lemma 2: $\forall n \in \mathbb N, 0 + n = n$
By induction on $n$. Certainly $0 + 0 = 0$, by definition of $+$.
Given $n \in \mathbb N$, and supposing that $0 + n = n$, we then have
$0 + S(n) = S(0 + n) = S(n)$, by definition of addition and inductive
hypothesis. So by induction, we are done.
Lemma 3: $\forall a, b \in \mathbb N, a + b = b + a$
By induction on $b$. Given $a \in \mathbb N$, indeed $a + 0 = a = 0 + a$, by
Lemma 2.
Given $b \in \mathbb N$, and supposing that $a + b = b + a$, we then have that
$a + S(b) = S(a + b) = S(b + a) = S(b) + a$, applying the definition of $+$, the
inductive hypothesis, and Lemma 1. So by induction, we are done.
Lemma 4: $\forall a, b, c \in \mathbb N, a + (b + c) = (a + b) + c$
By induction on $c$. Given $a, b \in \mathbb N$, certainly we have
$a + (b + 0) = a + b = (a + b) + 0$, by definition of $+$.
Then given $c \in \mathbb N$, and supposing that $a + (b + c) = (a + b) + c$, we
have
\begin{align*}
a + (b + S(c))
  &= a + S(b + c) \\
  &= S(a + (b + c)) \\
  &= S((a + b) + c) \\
  &= (a + b) + S(c)
\end{align*}
by definition of $+$ and by inductive hypothesis. So by induction, we are done.
Lemma 5: $\forall a, b \in \mathbb N, S(a) \cdot b = b + (a \cdot b)$
By induction on $b$. Given $a \in \mathbb N$, indeed
$S(a) \cdot 0 = 0 = 0 + 0 = 0 + (a \cdot 0)$, by definition of $\cdot$,
definition of $+$, and Lemma 2.
Then given $b \in \mathbb N$, and supposing that
$S(a) \cdot b = b + (a \cdot b)$, we have
\begin{align*}
S(a) \cdot S(b)
 &= S(a) + (S(a) \cdot b) && \text{(defn. of $\cdot$)} \\
 &= S(a) + (b + (a \cdot b)) && \text{(IH)} \\
 &= (S(a) + b) + (a \cdot b) && \text{(Lemma 4)}\\
 &= (b + S(a)) + (a \cdot b) && \text{(Lemma 3)} \\
 &= S(b + a) + (a \cdot b) && \text{(defn. of $+$)} \\
 &= (S(b) + a) + (a \cdot b) && \text{(Lemma 1)} \\
 &= S(b) + (a + (a \cdot b)) && \text{(Lemma 4)} \\
 &= S(b) + (a \cdot S(b)) && \text{(defn. of $\cdot$)}
\end{align*}
So by induction, we are done.
(This part may also answer your question about how to align the rules. The
site's formatting works in LaTeX, and allows some useful environments like
align. You can view the source by right-clicking on the maths, or you can just
look at my answer's Markdown source directly).
Lemma 6: $\forall n \in \mathbb N, 0 \cdot n = 0$
By induction on $n$. Certainly $0 \cdot 0 = 0$, by definition.
Then given $n \in \mathbb N$ and supposing $0 \cdot n = 0$,
$0 \cdot S(n) = 0 + (0 \cdot n) = 0 + 0 = 0$ by definition of $\cdot$, inductive
hypothesis, and definition of $+$. So by induction, we are done.
Lemma 7: $\forall a, b \in \mathbb N, a \cdot b = b \cdot a$
By induction on $b$. Given $a \in \mathbb N$, certainly
$a \cdot 0 = 0 = 0 \cdot b$, applying the definition of $\cdot$ and Lemma 6.
Given $b \in \mathbb N$, and supposing that $a \cdot b = b \cdot a$,
$a \cdot S(b)
 = a + (a \cdot b)
 = a + (b \cdot a)
 = S(b) \cdot a$,
by definition of $\cdot$, inductive hypothesis, and Lemma $5$.
By induction, we are done for the last time.
Corollary: $\forall n \in \mathbb N, n + n = 2 \cdot n$
As discussed earlier, $n + n = n \cdot 2$. By Lemma 7, we must then have
$n + n = 2 \cdot n$. QED.
Postscript
I hope this gave you some (perhaps enjoyable) insight into how these silly
rigorous foundational proofs about arithmetic might look.
I haven't proofread it very thoroughly, so excuse me if there are some typos.
The broad strokes are definitely correct.
It is quite funny how much induction is happening here. When you first meet
proof by induction, you rarely need more than one "layer" of induction (eg you
might be proving something like $\sum_{k = 1}^n k = \frac 12 n(n + 1)$ by a
single induction on $n$). But here we've had to organise everything into
different lemmas just to keep our sanity. Of course, wherever we say "by Lemma
$n$", we could also just substitute the proof of Lemma $n$, but it doesn't bear
thinking about how many induction in a row this would lead to.
I first got really familiar with these sorts of proofs when I was playing around
with proof assistants (or more sensationally, automated theorem proving). If you
find this kind of maths interesting, but you also like computers and
programming, it turns out that there's a big intersection. Formal mathematics
turns out to correspond quite well to the notion of statically typed programming
languages, allowing proofs to be written as programs, and checked by
(specialised) compilers.
Particularly, I recommend Kevin Buzzard's
Natural Number Game.
It's very friendly, so don't worry if any of my answer seemed too intimidating.
It's also very very addictive. The idea is that it turns proving theorems into a
sort of game, with levels and abilities that you unlock. Much of my answer was
actually based on exercises from the Natural Number Game. There are many
theorems I have not yet proved that you can go on to prove in the Natural Number
Game (eg associativity of multiplication, or distributivity of multiplication
over addition).
(I have no affiliation with the Natural Number Game other than liking maths and
thinking it's very good).
You might also be interested to see a sort of project me and a friend of mine
started after completing the natural number game, trying to formalise some more
of the maths we've learned in Lean. You can find it
here
(this is a permalink to the theorem stating multiplication is commutative).
Apologies if any of my notation or terminology is unfamiliar. I am happy to
clarify, but I am not going to be online for the next few hours, so there may be
a slight delay.
