Here is Theorem 4 and the proof of its part 2 from E. Landau's Foundations of Analysis. ($x'$ means $s(x)$ where $s$ is the successor function).
In part 1 he proved that there is at most one way to define a + b. And now, it is my understanding, he tries to prove then a natural number denoted by $x + y$ actually exists. Why does he not keep $x$ fixed here (like he did when proving part 1)? Here he proves it for (1, 1), (1, 2), (1, ...), (2, 1), (2, 2), (2, ...) etc, instead of proving for (x, 1), (x, 2), (x, ...). Would my proof be correct, if I wrote it with x fixed?
My proof:
We take any $x$ and show that $x + y$ exists for all $y$; $x + 1 = x'$ by definition. So $x + y$ exists for $y = 1$. Now we will prove that if $x + y$ exists then $x + y'$ also exists. $x + y' = (x + y)'$, but $x + y$ exists then $(x + y)'$ also exists. Hence by induction $x + y$ exists for all $y$. QED.
Why is this simpler proof worse then the author's?
$\quad$ Theorem $\bf 4,$ and at the same time Definition $\bf 1:\;\;$ To every pair of numbers $x,y$, we may assign in exactly one way a natural number, called $x+y$ ($+$ to be read "plus"), such that
- $x+1=x'\qquad$ for every $x$.
- $x+y'=(x+y)'$ for every $x$ and every $y$
$x+y$ is called the sum of $x$ and $y$, or the number obtained by addition of $y$ to $x$.
The logic in this axiomatic approach can be quite hard to follow, since we think we know the natural numbers so well so that we already tend to assume things we are about to prove.
Let me try to point out the significance of the steps in Landau's rendering of it:
First of all Landau has NOT stated that $x+1=x'$ at this point. That is a part of what he is trying to prove is possible to consistently have for all $x$.
Landau uses induction in $x$, NOT in $y$, since the theorem states two properties regarding $x$.
The proof $x=1$
So first Landau wants to establish that addition (i.e. the two properties) can be defined for $x=1$. So he constructs the definition $$ 1+y=y' $$ and shows that it works. Working with this definition we see that $$ 1+1=1' $$ showing that the first property of addition is fulfilled. Now, by the same definition we have that $1+y=y'$ which by axiom 2 and 4 is equivalent to $(1+y)'=(y')'$. But at the same time the above definition implies that $1+y'=(y')'$. So combining those statements, the constructed definition has lead to $$ 1+y'=(y')'=(1+y)' $$ So these are not mindless calculations! They show that by defining $1+y=y'$ we have succesfully defined addition for $x=1$ such that the two properties are fulfilled.
It all comes down to that before constructing the definition $1+y=y'$ the addition $1+y$ was not defined. Also it is important that it is induction in $x$, not in $y$, since the theorem has two properties where $y$ is only involved in one of them.
After that he proceeds to prove the inductive step, that if addition can be defined for $x$ the it can be defined for it's successor. That part is pretty straight forward.