Hi! I'm currently reading Edmund Landau's book Foundation of Analysis. I kinda got stuck right at the beggining where the author tries to develop the natural numbers theory from axioms. Theorem 4 states the following:

(where x' denotes the successor of x)

The following proof is quite hard to grasp (at least for me), so I'd be very grateful if anyone of you could post a link with a proof of this theorem or propose their own proof. Thanks very much.

P.S. If needed, I can post Landau's axioms & his proof.

In questions like these it is vital that you post the axioms that you're supposed to deduce things from since they are *not* automatically something anyone else will know. For me, in many a case like this, I would assume that the definition of successor x is x+1, if it isn't what is your definition of successor? So, what is your definition of the set of natural numbers?

Axiom 1 - 1 is a natural number
Axiom 2 - For each x there exists exactly one natural number, called the successor of x, which will be denoted by x'
Axiom 3 - We always have x' (not)= 1
Axiom 4 - If x' = y' then x = y. That is, for any given number there exists either no number or exactly one number whose successor is the given number.
Axiom 5 (Axiom of Induction) - Let there be given a set M of natural numbers, with the following properties:

I) 1 belongs to M.
II) If x belongs to M then so does x'.

Well, it is rather clear, that we can define at least one operation that satisfies the properties: define x+1 to be x'+1. It is the uniqueness that might trouble you, perhaps. Why not post the proof, and indicate the points that trouble you?

My problem with the proof is that I do not really understand the significance of a_{y} and b_{y} in part A of the proof. From this stems the complete confusion.

It's proving the uniqueness part. The recursion theorem says that there's exactly one function satisfying the recursion. So, you have to prove that if you have two functions satisfying the recursion, then the two functions must be equal.

Yes, more or less; a_y and b_y are both defined to satisfy the recursion by which we will eventually define x + y.

We don't yet know that a_y = x + y until we're done proving (the relevant parts of) this theorem, for two reasons:
(1) We don't yet know that x+y is well-defined.
(2) We don't yet know that the solution to the recursion is unique.

i.e. by repetitive use of Part b) of the definition (plus bearing in mind that e.g. 4 =_{df} 3' =_{df} (2')' =_{df} (1')')') we must arive at a step (((x + 1)')')' that is by definition identical with (((x')')')'. And Axiom 2 assures that the result is unique - a natural number.

The definition satisfies the recursion when (x + y') and (x + y)' are equal. He shows that both of them are equal to (y')', which - in my opinion - does not follow from the previous Part of Proof/Theorems/Axioms. The line (x + 1 = 1' = x') is quite clear, but the one below is not.