nLab extended natural number

Redirected from "conatural numbers".
Extended natural numbers

Extended natural numbers

Idea

The extended natural number system, denoted ¯\bar{\mathbb{N}}, consists of all of the natural numbers together with an extra number representing infinity.

Definition

Classically, ¯\bar{\mathbb{N}} is the disjoint union of the set \mathbb{N} of natural numbers and a point {}\{\infty\}. 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 xx of binary digits (each 00 or 11) with the property that x i=1x_i = 1 if x j=1x_j = 1 for any jij \leq i; that is, the sequence is monotone. Then the natural number nn is identified with a sequence of nn copies of 00 followed by 11s, while infinity is identified with a sequence of all 00s. 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

¯\bar{\mathbb{N}} comes naturally equipped with a map pred:¯1+¯pred\colon \bar{\mathbb{N}} \to 1 + \bar{\mathbb{N}} 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+XH(X) = 1 + X on Set, and indeed is the terminal coalgebra for HH. That is, given any set SS and map p:S1+Sp\colon S \to 1 + S, there is a unique map corec Sp:S¯corec_S p\colon S \to \bar{\mathbb{N}} 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. Indeed, corec Spcorec_S p is defined corecursively by corec Sp(a)=0corec_S p(a) = 0 if p(a)=*p(a) = * and pred(corec Sp(a))=corec Sp(a )\pred(\corec_S p(a)) = \corec_S p(a^\prime) if p(a)=a Sp(a) = a^\prime \in S. In this way, ¯\bar{\mathbb{N}} is dual to the natural number system \mathbb{N} in its guise as a natural numbers object.

You can think of corec Spcorec_S p as mapping an element aa of SS to the maximum number of times that pp can be applied in succession, starting from aa, before being taken out of SS. Since this may never occur, we need \infty as a possible value. At the other extreme, if p(a)=*p(a) = * then pp cannot be applied at all to aa before leaving SS, so corec Sp(a)=0corec_S p(a) = 0.

Note that this universal property also holds constructively (which is why we can be sure that the constructive definition above is correct). We define predpred 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}

Formalization in proof assistants

With the Coq proof assistant:

CoInductive conat : Set :=
| cozero : conat
| cosucc : conat -> conat.

CoFixpoint omega : conat := cosucc omega.

Topology

We may naturally give ¯\bar{\mathbb{N}} 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 GG of ¯\bar{\mathbb{N}} is open if, whenever G\infty \in G, there is a finite nn such that mGm \in G whenever mnm \geq n. In other words, GG is a neighbourhood of \infty just when almost every finite number also belongs to GG.

In this way, ¯\bar{\mathbb{N}} is the Alexandroff compactification of the discrete space \mathbb{N}. The space is obviously compact because, given an open cover 𝒰\mathcal{U}, we have G𝒰\infty \in G \in \mathcal{U} for some GG, so GG alone contains almost every point, and only finitely many more open sets are needed.

It is sometimes convenient to represent ¯\bar{\mathbb{N}} as a subspace of the real line \mathbb{R}, which we can do by interpreting the natural number nn as 2 n2^{-n} and \infty as 00. Constructively, the monotone bit sequence xx 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)1/(n+1) instead of 1/2 n1/2^n.

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

This may all be generalised from sequences to other nets; given a directed set DD, we form D¯\bar{D} by adjoining \infty and taking GDG \subseteq D as a neighbourhood of \infty iff GG owns almost all of DD. (Constructively, this may require using locales for the general case.)

In higher category theory

Concepts in higher category theory often come in nn-versions where nn is an extended natural number. (Sometimes it’s also possible to give nn a few negative values as well; see negative thinking.) Typically, the \infty-version is all-encompassing, with the nn-versions as special cases. On the other hand, the 11-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 (LPOLPO) for natural numbers. On the other hand, the LPOLPO for extended natural numbers is simply true; given any function from ¯\bar{\mathbb{N}} to {0,1}\{0,1\}, it is either all 00s or has a 11. See Escardó (2011).

References

Last revised on December 16, 2023 at 10:20:21. See the history of this page for a list of all contributions to it.