# What exactly are the numbers we use everyday?

Pi can be defined as diameter / circunference of a circle. But what is a circle? You can't tell a computer: "build a circle and divide its diameter by its circumference". You need to define what a circle is. Wikipedia defines a circle as: It is the set of all points in a plane that are at a given distance from a given point, the centre. But that is just a statement about a property that circles have that allows us to uniquely identify them among the space of existing mathematical ideas. How do you actually build that circle? And how do actually find pi from that definition? There are no instructions on this definition. This definition doesn't explain how to build a circle, just identifies what it is.

As an example, lets talk about trees. Trees are well-understood structures with an obvious computational representation. There are even many kind of trees and I can actually write down all of them how they truly are. Using the λ-calculus, for example, I can represent a complete, untagged binary tree of depth 2 using the lambda-church encoding:

tree : (∀ (t : *) -> (t -> t -> t) -> t -> t)
tree = (λ branch tip . branch (branch tip tip) (branch tip tip))


That is a tree, on its true form. It doesn't just "identify" the essence of a tree by listing an unique property it has. I actually defines it. The type above perfectly captures the set of untagged binary trees, and the element I wrote is a member of that set. You can see it, you can inspect its structure and you can use it to do meaningful computation. If you study that type, you are studying untagged binary trees; it has all the properties you could expect from an untagged binary tree, because it is the actual definition of an untagged binary tree.

Now, when it comes to numbers, we don't have that. If we ask a mathematician what is a natural number, or a real number, or a fractiona lnumber, he will keep proposing "wordy" statements that uniquely identify those sets, but he won't show you how to actually build those things. If you ask him to write down a number on paper, he will write 5, or 6. But that isn't a number. That is a decimal representation of a number that humans happen to like. Similarly, if you ask a computer scientist, he will talk about properties numbers have. If you ask him to show you how a number actually looks like, he might show you a 64-bit vectors. But those vectors aren't numbers too. Those only represent numbers.

If we wanted to study bit vectors, we could, too:

bits : (∀ (t : *) -> (t -> t) -> (t -> t) -> t -> t)
bits = (λ o z e . (o (z (o (o (z (z (z (z e)))))))))


That is as good a definition of a bitvector as the definition above is of a tree. But it says nothing about numbers. It is, at most, isomorphic to the set of natural numbers. But that's where it ends. It doesn't say anything about natural numbers because it doesn't capture its essence in any meaningful way. Studying numbers through that definition would be like studying Japanese grammar in english. It is a layer of indirection.

So, what is a number? What is its structure like? How do you represent, computationally, syntactically, the phenomena of a real number, of a complex number, a tensor? What algebraic structure has all the properties that a quaternion has, without layers of indirections?

• I think your issue here is not so much about numbers as it is about structures which really only have meaning up to isomorphism. With that in mind, I don't think you're going to get a satisfactory answer, because these structures really are only usefully defined up to isomorphism. Any definition of them which pins down which isomorphism class you are talking about adds redundant information (e.g., set theoretic definition of the real numbers necessarily answers the question "is $\pi \in e$?"
– Ian
Mar 23 '16 at 14:11
• My issue here is that I have a very convincing definition of what a tree is justified on Type Theory. I can study trees through that definition. I don't have a convincing type-theoretic definition of what a "real number" is. The usual definition go through obvious layers of indirection (floating point arithmetics). I don't want to study real numbers through the lens of a human-defined format. There must be something better. Mar 23 '16 at 14:13
• No, your issue really is what I just said. If you're looking at real numbers, there are two canonical explicit constructions (equivalence classes of Cauchy sequences of rational numbers and Dedekind cuts). There is also a "synthetic" presentation, wherein we define the real numbers based on properties they should satisfy and then prove they are unique up to isomorphism. Whichever way you proceed, "the real numbers" only live in this peculiar up-to-isomorphism world. They are not really given by any of their constructions.
– Ian
Mar 23 '16 at 14:16
• That said, the equivalence classes of Cauchy sequences construction is explicit in the sense that you seem to intend. But working directly in that format is far too cumbersome.
– Ian
Mar 23 '16 at 14:18
• How there are "two" definitions? That would mean there are two kinds of real numbers that we happen to address with the same name? And do you mean "Cauchy" sequences are what real numbers truly are, in the same sense the untagged trees proposed on this question? If so, why would be cumbersome to work on them directly - it isn't cumbersome to work on binary trees. Moreover, what about Quaternions, Tensors and all other mathematical objects? If you know where I can find resources that justify those structures in the sense I mention, that'd be a really appreciated answer. Mar 23 '16 at 14:24

Real numbers can be approximated by rational numbers. Rational numbers can be "constructed" explicitly once we've constructed the integers. We can construct the integers once we have the natural numbers.

And there's a perfectly simple definition of what the natural numbers are, entirely analogous to the way people specify grammars in computer science. A grammar is specified by an alphabet and a set of production rules, allowing you to build valid formulas from shorter valid formulas. The corresponding definition of a natural number is this:

1. $0$ is a natural number.

2. If $n$ is a natural number then $Sn$ is a natural number.

So the first few natural numbers are $0$, $S0$, $SS0$, etc. More commonly written as $0$, $1$, $2$, etc. See here for more details.

You can even calculate $2+2$:

class Int:
def __init__(self, pred=None):
self.pred = pred

def __str__(self):
if self.pred:
return 'S' + str(self.pred)
else:
return '0'

if m.pred:
return S(n) + m.pred
else:
return n

def S(n):
return Int(n)

Zero = Int()

print S(S(Zero)) + S(S(Zero))

• I agree this is a perfect simple definition of what a natural number is, but I'm not so sure a tuple with "sign" and "natural number" is the perfect definition of an integer. The type of natural numbers clearly has all the properties of natural numbers, and you can implement numeric functions such as multiply and exponentiate with very low complexity and no explicit branching. Implementing numeric functions operating on your proposed datatype needs a lot of branching to treat the sign correctly. It looks all but natural. Mar 23 '16 at 14:27
• You're not being reasonable. Of course there are much more efficient implementations - that question is orthogonal to the question of how one can give a representation of the sort you seemed to want. The "natural" implementation is far from being efficient - all that branching is natural. Mar 23 '16 at 14:33

The question "what is a number" is not an easy one to answer, even in reference to the natural numbers as you mention in your question.

Unlike a finite tree, dealing with the collection of natural numbers involves infinitary issues. Within the usual set-theoretic foundations of mathematics the numbers are defined by declaring $0$ to be the empty set $\emptyset$, $1$ to be the set $\{\emptyset\}$, $2$ to be the set $\{\emptyset,\{\emptyset\}\}$, etcetera. Soon enough in a set-theoretic context you obtain the set $\mathbb{N}$.

Most mathematicians adhere to the view that $\mathbb{N}$ corresponds to the intuitive counting numbers. Such an identification is sometimes referred to as the Intended Interpretation (as opposed to the usual meaning of the term interpretation when certain syntactic structures are mapped onto semantic ones, usually in a set-theoretic context). An extensive discussion of this issue can be found here.

Circle's actually do have representation in Lambda Calculus.

circle : distance -> point -> (point -> point -> distance) -> *
circle = (λ (r : distance). λ (c : point) . λ (d : point -> point -> distance). forall (x : *) . (forall (p : point). d c p = r -> x))


Where point is a data type for points, distance is a data type for lengths, d is a metric, and = is a type for equality (such as defined here.) circle r c d is the type for points that lie on a circle with center c and radius r with metric d.

• How do you define distance and point? Mar 23 '16 at 15:58
• Depends on the metric space. For a regular circle, distance would be a real number, and point would be a pair of real numbers. Mar 23 '16 at 16:11