I am trying to rove Proposition $2.2.12$ in Terence Tao's analysis text. I am a bit stick on part a, which states that for any $a \in \mathbb{N}$, $a \geq a$, a fact I need to prove using only the properties of the natural numbers and their addition. Here is what I have been able to put together so far. I am going to insert parenthetical comments where necessary that hopefully best convey where I am stuck at.
Proof. Let $a \in \mathbb{N}$. Suppose toward a contradiction that reflexivity fails and $a < a$. By definition of $<$, this means that $a \leq a$ and $a \neq a$.
This is surely a contradiction. It seems rather obvious that $a = a$, but then am I assuming reflexivity or that "$=$" is an equivalence relation? I don't seem to have an axiom for the natural numbers that allows me to assert equality unless two natural numbers, $n$ and $m$, have the same successor. Then, again, both have the successor which Tao denotes $(a++)$, so perhaps I am free to assert that $a = a$.
I suppose the remainder of the proof with this in mind would take the form:
Two natural numbers, $n$ and $m$, are equivalent if their successors are equal: if $(n++) = (m++)$. Clearly, $(a++) = (a++)$, so $a = a$. This contradicts the definition of $<$, as we have shown both that $a = a$ and $a \neq a$. Thus, our supposition fails, and we have $a \geq a$.
How is this? It seems somewhat circular, so I am not sure whether I need to justify that $a = a$, a rather trivial fact.
I wanted to assert something to the effect of $a < a$ implies $a = d + a$ for some positive natural $d$, and since $a + 0 = a$, we have $a + 0 = d + a$, and by cancellation $d = 0$, a contradiction. I believe I am able to assert the latter via Tao's definition of the positive numbers, but the former is an order axiom by itself. It seems that I am only able to assert, via his given foundations, that $d$ is a natural number: it could be zero itself.
I'd greatly appreciate any feedback on this.
Note that equality is defined within the realms of set theory.
Since the natural numbers are usually constructed as John von Neumann ordinals, it is obvious that $a=a$ for every natural number $a$ already from set theory.
Equality has nothing to do with natural numbers in specific (and in particular it is completely independent from Peano arithmetic). For instance, Bourbaki has written a very rigorous book (N. Bourbaki: Theory of sets) in which $\forall a: a=a$ is proven already within predicate logic.
Note that the equal sign is oftentimes used not to denote equality, but also in equations, as a substitute of “corresponds to”, $\dots$. But here we are indeed talking about formal equality.