nLab
extended natural number

Extended natural numbers

Idea

The extended natural number system, denoted ¯, consists of all of the natural numbers together with an extra number representing infinity.

Definition

Classically, ¯ is the disjoint union of the set of natural numbers and a point {}. That is,

¯={0,1,2,,}.\bar{\mathbb{N}} = \{0,1,2,\ldots,\infty\} .

In constructive mathematics, a more careful definition is required: an extended natural number is an infinite sequence x of binary digits (each 0 or 1) with the property that x i=1 if x j=1 for any ji; that is, the sequence is monotone. Then the natural number n is identified with a sequence of n copies of 0 followed by 1s, while infinity is identified with a sequence of all 0s. It is not constructively valid that every natural number is either finite or infinite, but it is valid that any that is not finite is infinite, while Markov's principle is the converse.

Universal property

¯ comes naturally equipped with a map pred:¯1+¯ as defined below:

pred(x)={* ifx=0, n ifx=n+1, ifx=.pred(x) = \begin{cases} * & if\; x = 0 ,\\ n & if\; x = n + 1 ,\\ \infty & if\; x = \infty .\end{cases}

Thus, it is a coalgebra for the endofunctor H(X)=1+X on Set, and indeed is the terminal coalgebra for H. That is, given any set S and map p:S1+S, there is a unique map corec Sp:S such that

S p 1+S corec Sp id 1+corec Sp ¯ pred 1+¯\array { S & \stackrel{p}\to & 1 + S \\ \downarrow_{corec_S p} & & \downarrow_{\id_1 + corec_S p} \\ \bar{\mathbb{N}} & \stackrel{pred}\to & 1 + \bar{\mathbb{N}} }

commutes. In this way, ¯ is dual to the natural number system? in its guise as a natural numbers object.

You can think of corec Sp as mapping an element a of S to the number of times that p must be applied in succession, starting from a, before being taken out of S. Since this may never occur, we need as a possible value.

Note that this universal property also holds constructively (which is why we can be sure that the constructive definition above is correct). We define pred constructively as follows:

pred(x)={* ifx 0=1, (x 1,x 2,) ifx 0=0.pred(x) = \begin{cases} * & if\; x_0 = 1 ,\\ (x_1,x_2,\ldots) & if\; x_0 = 0 .\end{cases}

Topology

We may naturally give ¯ a topology giving it the structure of a compact Hausdorff space; unusually, this works even in weak constructive foundations (without having to use the fan theorem or pass to a locale).

We may define the topology simply (and constructively) as follows: a subset G of ¯ is open if, whenever G, there is a finite n such that mG whenever mn. In other words, G is a neighbourhood of just when almost every finite number also belongs to G.

In this way, ¯ is the Alexandroff compactification of the discrete space . The space is obviously compact because, given an open cover 𝒰, we have G𝒰 for some G, so G alone contains almost every point, and only finitely many more open sets are needed.

It is sometimes convenient to represent ¯ as a subspace of the real line , which we can do by interpreting the natural number n as 2 n and as 0. Constructively, the monotone bit sequence x becomes the real number

12 i=0 x i2 i,\frac{1}{2} {\sum_{i=0}^\infty x_i 2^{-i}} ,

which always converges. Another common representation uses 1/(n+1) instead of 1/2 n.

Given any topological space X, an infinite sequence in X may be thought of as a continuous map to X from the discrete space . Then this sequence converges? iff this map can be extended to a continuous map on ¯. For this reason, ¯ is sometimes called the universal convergent sequence. (Strictly speaking, unless X is at least sequentially Hausdorff, a map to X from ¯ contains more information than a sequence in X with the property of convergence.)

This may all be generalised from sequences to other nets; given a directed set D, we form D¯ by adjoining and taking GD as a neighbourhood of iff G owns almost all of D. (Constructively, this may require using locales for the general case.)

In higher category theory

Concepts in higher category theory often come in n-versions where n is an extended natural number. (Sometimes it’s also possible to give n a few negative values as well; see negative thinking.) Typically, the -version is all-encompassing, with the n-versions as special cases. On the other hand, the 1-version is usually more familiar outside of category theory.

See also categorification.

In constructive mathematics

The claim that every extended natural number is either finite or infinite is equivalent to the limited principle of omniscience (LPO) for natural numbers. On the other hand, the LPO for extended natural numbers is simply true; given any function from ¯ to {0,1}, it is either all 0s or has a 1. See Escardó (2011).

References

Revised on September 17, 2011 08:33:34 by Toby Bartels (71.31.209.1)