What is the benefit in constructing the integers from natural numbers? My question is two fold:
1) So, before the integers were first proven to be constructible from the natural numbers, we already had used them. So we had a ring structure of preliminary integers with the exact properties that the ring of equivalence classes of pairs of natural numbers has that is used to construct the integers and we just modelled the latter to match the preliminary structure that already existed. Is that right? So in fact any ring that is isomorphic to the preliminary integers and constructible from set theory or natural numbers could have done the trick, is that right?
2) Why construct integers from natural numbers at all? Certainly the Peano axioms can be encoded in lambda calculus for instance. So also certainly we could encode the properties of integers with lambda calculus. For example the representation of the natural number $n$ as $s_n(s_{n-1}(\dots s_1(0)\dots))$ is basically the same as the church numeral $\lambda f. \lambda x. f^nx$.
To represented negative numbers in a Peano fashion we could introduce a function $p$ that annihilates with $s$ and likewise find some encoding for that in lambda calculus. Addition of a lambda $n$ term that represents a negative number with a term $m$ would then first strip off any $f$s from $m$ (the annihilation bit) and if necessary transform $m$ further to get to the term that represents the final difference of the two $m$ and $n$.
So therefore we could construct both the natural numbers and the integers from the same building blocks. Would such a "parallel" construction, where the integers are not derived from the natural numbers, via construction using the latter, be any less meaningful?
 A: The result comes from a strong historical desire to find a list of axioms from which all mathematical truths could be proved in a first-order system. With the advent of calculus, people began to prove all types of completely incorrect statements by their cavalier manipulation of the infinite. This fact, coupled with the discovery of Russell's Paradox, led to people to believe that there should be a more systematic way of theorem-proving. It was later proved impossible by Gödel to find such a comprehensive system, even if infinitely many axioms were allowed. Still, most results of interest can be proved from the set-theoretic construction of mathematics known as ZFC set theory. One of the axioms is the existence of the natural numbers. It is generally accepted that one should take as few axioms as possible. Also, it actually turns out proof-wise to be easier to construct the integers than assuming their existence, as it would be more difficult to define the addition and multiplication operations on them. These are the two largest reasons why. We actually construct the natural numbers in a sense as well. They are defined as follows:
$$
\begin{align}
0 &:= \emptyset \\
1 &:= \{0\} \\
2 &:= \{0,1\} \\
3 &:= \{0,1,2\} \\
\vdots
\end{align}
$$
One then proves that recursively defining a function is an acceptable way to define a function, and defines the operations of addition and multiplication recursively as follows:
$$
\begin{align}
S(x)&:= x \cup \{x\} \text{ (the successor of $x$, i.e. $x+1$)}, \\
\\
x + 0 &:= x \\
x + S(y) &:= S(x+y), \\
\\
x * 0&:= 0 \\
x * S(y)&:= (x*y) + x.
\end{align}
$$
One can also take out zero and call it the natural numbers if one then wanted.
After that one then constructs the integers as equivalence classes of ordered pairs of natural numbers, where the ordered pair $(x,y):= \{\{x\},\{x,y\}\}$, represents the number $x-y$, and so on. (Functions are also defined as sets of ordered pairs, by the way.) The case of the reals is more complicated, and also the biggest leap in turns of taking its existence as an axiom, as it is tantamount to assuming there are no holes in the number line. I know this is more than you asked for (the answer to your question is in bold above), I just thought I'd give you an idea of how this progression actually goes in terms of defining everything as a set.

Edit:
In response to your comment. You start out constructing
a system for expressing and proving logical truths. You introduce a set of logical symbols like and, or, not, etc., and a set of nonlogical symbols consisting of function symbols, relation symbols, and constants, and a syntax for them. You then find a way to actually have these statements acquire meaning by introducing a signature, consisting of a language (subset of the nonlogical symbols), a domain/universe this language means to describe, and an interpretation function that maps purely syntactical statements to what the real-world meaning of this statement would be. You then introduce Tarski semantics (see T-schema on Wikipedia), which is a way of defining what it means for these statements to be true, in such a way that a formula will be true if and only if the idea that it expresses will be true. Then you introduce rules of inference which allows you to prove things with this system. You now have a system for expressing an unbelievable quantity of statements and proving things from them. Next you want to know that you won't prove false statements from true assumptions. This is called soundness, and it turns out to be the case that FOL is sound. Then you want to know whether any logically-valid relationship capable of being expressed in your system can actually be proved in your system. This is called completeness (distinguished from the term completeness when referring to a theory), and although it is a pain in the a**, you can prove first-order logic is complete. (See completeness theorem.)
Here is the point of all of this. You ask yourself, can I prove results from real analysis in this system? That way I can be confident that I'm not proving things that are false. You introduce the language of set theory, generally either only $\{\in\}$ or $\{\in, \emptyset \}$, and the axioms of ZFC become your basis for proving things. You then crucially prove that it is possible to expand your language, by adding new symbols to it, in such a way that it is possible to remove these new symbols from any statement and replace them with your original symbols, and that by adding these new symbols you are not accidentally adding new axioms. That is, you can't prove anything with these new symbols that ultimately can't be proved from your original symbols and axioms. You then proceed to define all the number systems in your system, properties of sets, limits, functions, etc., and at each step, you are proving these theorems in first order logic, in a way that all these new symbols could be eliminated and results proved from just the axioms of ZFC. As I said, nobody actually does this anymore, people still use the same axioms, but proofs are done in paragraph form. Still, it's satisfying to know that you could do it if you wanted.
