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?

  • $\begingroup$ Lol...Set theory is a formalization of existing mathematical ideas. $\endgroup$ Nov 26, 2017 at 3:46
  • $\begingroup$ I don't understand what you are saying with that and why you are saying that. $\endgroup$ Nov 26, 2017 at 3:47
  • 3
    $\begingroup$ You need to remember that at the time there was a "crisis of foundations"; many things that had been taken for granted had turned out to be incorrect (such as the belief that the Dirichlet principle always held, or that functions had to be differentiable at "most" points), and that certain types of arguments had been shown to lead to contradictions. There was a conscious, deliberate attempt at trying to justify even things that people had taken for granted. So, like Gauss had "constructed" the complex numbers as points on the plane, people were trying to either establish (cont) $\endgroup$ Nov 26, 2017 at 4:06
  • 1
    $\begingroup$ (cont) other constructions: the real numbers, the rationals, the integers, and try to make sure that properties that had been merely assumed to hold could actually be proven to hold. Or at least to pinpoint what assumptions were needed to ensure that such properties could be derived (e.g., Hilbert greatly expanded Euclid's axioms to help justify many properties "established" in the Elements, that simply did not follow from the axioms given). This in parallel with the Hilbert programme to try to show that certain methods of proof did not introduce contradictions. $\endgroup$ Nov 26, 2017 at 4:08
  • $\begingroup$ (cont) In particular, while you could axiomatize the integers and then derive the natural numbers, historically this is not what happened. In fact, you first had the natural numbers, then the nonnegative rationals, then the nonnegative reals, then the integers, rationals, and reals. Descartes, for instance, refers to "imaginary quantities" when talking about negative numbers. So the integers are a very late addition to the mathematical toolkit. And so, those who wanted to go back and make sure the foundations were correct started with natural numbers and derived the integers. $\endgroup$ Nov 26, 2017 at 4:10

1 Answer 1


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.


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.

  • $\begingroup$ Thanks, I am aware of most of that. But concerning keeping the number of axioms low... a construction via lambda calculus would not involve any new axioms, would it? Neither would any other ring isomorphic to $\mathbb{Z}$ constructed with what was available. So, you did not touch in that, which was the actual question: Is there a specific reason for THIS exact construction by pairs of natural numbers? The question was not "why construct the integers from existing math?" but "why construct them like THIS?" $\endgroup$ Nov 26, 2017 at 5:27
  • $\begingroup$ Can you tell me where I can read more on the fundamental theorem of calculus not being provable by lambda calculus? $\endgroup$ Nov 26, 2017 at 5:41
  • $\begingroup$ Hm, what is ATP? $\endgroup$ Nov 26, 2017 at 16:13
  • $\begingroup$ I am a computer scientist. And I don't really understand the distinction you are making between theorem proving and defining in something like lambda calculus. Isn't that what the Curry-Howard isomorphism is about? (btw. why did you delete your comments about that matter?) And I also don't understand why one would not be able to express integer arithmetic in lambda calculus (comment also deleted). Can you tell me some keywords regarding this distinction you are making so I can read up on this? $\endgroup$ Nov 26, 2017 at 17:26
  • $\begingroup$ @user3758468 I'm only deleting them because the website frequently yells at me when my comment list gets too long. You CAN express integer arithmetic in lambda calculus, but the end goal here is not to actually perform any arithmetic. I don't know that there is a keyword that would really explain this, but I will try to add some to my post $\endgroup$
    – David Reed
    Nov 26, 2017 at 17:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.