nLab number




Throughout mathematics there are various entities referred to as “numbers”; in modern mathematics it would be more accurate to refer to any one of various types called “number systems”, and simply define a number to be a term of such a type.

A numeral on the other hand is a syntactic representation of a number, part of a system of numeration.

It is interesting to try to describe the general conditions under which something comes to be designated as a “number”. After all, such number systems tend to form commutative rings or at least commutative rigs, but not all commutative rigs are considered to consist of “numbers”, or at least that is not how the language is used in practice.

The root notion, known to the great ancient civilizations and particularly ancient Hellenic civilization, is that of (the system of) natural numbers, and in some way or other each of the various number systems are extensions of that one. If we may attempt a broad classification, qualitatively there are two broad types of number systems:

Roughly speaking, transfinite numbers tend to be quantities that measure sizes of elements in ZF-type structures (as in algebraic set theory, or in the study of games in the sense of Conway), sometimes arising through a process of decategorification.

In algebraic number theory, there seem to be two distinct general trends in the creation of new number systems from old (starting from the natural numbers):

    • Passing to a finite extension of some sort

For example, one passes from the rig of natural numbers to the ring of integers through additive group completion, or from the integral domain of integers to the field of rationals through a field of fractions completion. Or, one constructs number fields as finite extensions of the field of rational numbers (similarly, algebraic integers α\alpha inside such a number field K/K/\mathbb{Q} as those elements such that [α]\mathbb{Z}[\alpha] is a finite rank extension of \mathbb{Z}). Or, one constructs various local field completions of number fields, based on the valuations one can define on them; these include the real numbers and complex numbers and pp-adic numbers. Or, one has various finite-dimensional algebra extensions such systems, including for example the quaternions (aka Hamiltonian numbers) and octonions (aka Cayley numbers), and various pp-adic relatives of these.

Sometimes one singles out subtypes of such types; for example, the field of all algebraic numbers is the union of all number fields considered within the type of complex numbers. Sometimes numbers are designated according to what they are not, for example one speaks of irrational (= non-rational) numbers and of transcendental (= non-algebraic complex) numbers.

In dependent type theory

Assuming the type of natural numbers, we display the construction of, consecutively, the rings of

in dependent type theory with quotient types (such as homotopy type theory with the univalence axiom), as terms of ring structure (see there):

Here we use the notation for dependent functions, dependent pairs and their type telescopes from dependent functions and dependent pairs – table.

Throughout we omit displaying the certificates of identification type involved (associativity etc.). Mostly their construction is immediate, a little thought is required only for the convergence certificates of the operations on the real numbers: We show the “regular Cauchy real number type” due to Bishop (1967); the ideas for obtaining the required identification certificates may be found in Bishop (1967, pp. 15) and Bishop & Bridges (1985, pp. 18), full formalization in Agda is in Lundfall (2015), Murray (2022).

For X:SetX \,\colon\, Set and P:XPropP \colon X \to Prop an equivalence relation with corresponding R(x:X)×P(x)R \,\coloneqq\, (x \colon X) \times P(x), we write

X/R:Set X / R \,\colon\, Set

for the corresponding quotient type.

We display functions on such quotient sets as operations on the quotiened set XX, leaving again implicit the certificates that these functions do respect the relations and hence do restrict to the quotient.

The natural numbers

Here we assume the type of natural numbers, for detailed discussion see there.

Just briefly:

:Type \mathbb{N} \;\colon\; Type

denotes the inductive type generated from

0:,succ:. 0 \,\colon\, \mathbb{N} ,\;\;\;\; succ \,\colon\, \mathbb{N} \to \mathbb{N} \,.

By recursion this induces the usual operations of addition and multiplication, which we denote as usual:

+ : × : ×. \begin{array}{ccl} + &\colon& \mathbb{N} \times \mathbb{N} \to \mathbb{N} \\ \cdot &\colon& \mathbb{N} \times \mathbb{N} \to \mathbb{N} \,. \end{array}

Not to clutter the notation, we will consecutively overload this notation in the following. For example, the addition of integer numbers in the following is defined on representatives as

(n 1,m 1)+(n 2,m 2)=(n 1+n 2,m 1+m 2) (n_1 ,\, m_1) \;+\; (n_2 ,\, m_2) \;\; = \;\; \big( n_1 + n_2 ,\, m_1 + m_2 \big)

and it is tacitly understood that the addition symbol operation on the left goes ×\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}, while that on the right is the one from above: ×\mathbb{N} \times \mathbb{N} \to \mathbb{N}.

The integer numbers

The ring of integer numbers:

(1)(,0,+,,1,):Ring where ×/((n 1,m 1),(n 2,m 2):×)×Id (n 1+m 2,m 1+n 2) 0 (0,0) + : ((n 1,m 1),(n 2,m 2))(n 1+n 2,m 1+m 2) : (n,m)(m,n) 1 (succ(0),0) : ((n 1,m 1),(n 1,m 2))(n 1n 2+m 1m 2,m 1n 2+n 1m 2) \begin{array}{l} \mathllap{ \vdash \;\;\;\;\;\; } \big( \mathbb{Z} ,\, 0 ,\, + ,\, - ,\, 1 ,\, \cdot \big) \;\colon\; Ring \\ \text{where} \\ \begin{array}{ccl} \mathbb{Z} &\coloneqq& \mathbb{N} \times \mathbb{N} \;\bigg/\; \big( (n_1,\,m_1) ,\, (n_2,\,m_2) \;\colon\; \mathbb{N} \times \mathbb{N} \big) \times Id_{\mathbb{N}} \big( n_1 + m_2 ,\; m_1 + n_2 \big) \\ 0 &\coloneqq& (0,0) \\ + &\colon& \big( (n_1,\,m_1) ,\, (n_2,\,m_2) \big) \;\mapsto\; \big( n_1 + n_2 ,\, m_1 + m_2 \big) \\ - &\colon& (n,\, m) \;\mapsto\; (m,\, n) \\ 1 &\coloneqq& \big( \mathrm{succ}(0) ,\, 0 \big) \\ \cdot &\colon& \big( (n_1,\,m_1) ,\, (n_1,\,m_2) \big) \;\mapsto\; \big( n_1 \cdot n_2 + m_1 \cdot m_2 ,\;\; m_1 \cdot n_2 + n_1 \cdot m_2 \big) \end{array} \end{array}

The inclusion of natural numbers into integer numbers:

ι: n (n,0) \begin{array}{rcl} \iota \;\colon & \mathbb{N} &\longrightarrow& \mathbb{Z} \\ & n &\mapsto& (n,\,0) \end{array}

The ordering of integer numbers:

(2): × Prop (n 1,n 2) (k:)×Id (n 2,n 1+ι(k)) \begin{array}{rrcl} \leq \;\colon & \mathbb{Z} \times \mathbb{Z} &\longrightarrow& Prop \\ & (n_1 ,\, n_2) &\mapsto& (k \colon \mathbb{N}) \times Id_{\mathbb{Z}} \big( n_2 ,\; n_1 + \iota(k) \big) \end{array}

The positive integer numbers:

(3) +(n:)×(1n) \mathbb{Z}_+ \;\coloneqq\; (n \,\colon\, \mathbb{Z}) \times (1 \leq n)

The rational numbers

The ring of rational numbers:

(4)(,0,+,,1,):Ring where × +/((p 1,q 1),(p 1,q 2):× +)×Id (p 1q 2,q 1p 2) 0 (0,1) + : ((p 1,q 1),(p 2,q 2))(p 1q 2+p 2q 1,q 1q 2) : (p,q)(p,q) 1 (1,1) : ((p 1,q 1),(p ,q 2))(p 1p 2,q 1q 2) \begin{array}{l} \mathllap{ \vdash \;\;\;\;\;\; } \big( \mathbb{Q} ,\, 0 ,\, + ,\, - ,\, 1 ,\, \cdot \big) \;\colon\; Ring \\ \text{where} \\ \begin{array}{ccl} \mathbb{Q} &\coloneqq& \mathbb{Z} \times \mathbb{Z}_+ \;\bigg/\; \big( (p_1 ,\, q_1) ,\, (p_1 ,\, q_2) \,:\, \mathbb{Z} \times \mathbb{Z}_+ \big) \times \Id_{\mathbb{Z}} \big( p_1 \cdot q_2 ,\; q_1 \cdot p_2 \big) \\ 0 &\coloneqq& (0,1) \\ + &:& \big( (p_1 ,\, q_1) ,\, (p_2 ,\,q_2) \big) \;\;\mapsto\;\; \big( p_1 \cdot q_2 \,+\, p_2 \cdot q_1 ,\;\; q_1 \cdot q_2 \big) \\ - &\colon& (p,\,q) \;\mapsto\; (-p,\, q) \\ 1 &\coloneqq& (1,\, 1) \\ \cdot &\colon& \big( (p_1,\, q_1) ,\, (p_,\,q_2) \big) \;\mapsto\; \big( p_1 \cdot p_2 ,\; q_1 \cdot q_2 \big) \end{array} \end{array}

ordering of the rational numbers induced from the ordering (2) of the integer numbers:

(5): × Prop ((q 1,p 1),(q 2,p 2)) (q 1p 2q 2p 1) \begin{array}{rrcl} \leq \;\colon & \mathbb{Q} \times \mathbb{Q} &\longrightarrow& Prop \\ & \big( (q_1 ,\, p_1) ,\, (q_2 ,\, p_2) \big) &\mapsto& \big( q_1 \cdot p_2 \,\leq\, q_2 \cdot p_1 \big) \end{array}

When constructing the real numbers in (8) below, we use the following common abbreviations:

The multiplicative inverse of a positive natural number:

(6)1(): + n (1,n) \begin{array}{rrcl} \frac{1}{(-)} \;\colon & \mathbb{N}_+ &\longrightarrow& \mathbb{Q} \\ & n &\mapsto& (1,\,n) \end{array}

The square of a rational number:

(7)() 2: r rr \begin{array}{rrcl} (-)^2 \;\colon & \mathbb{Q} &\longrightarrow& \mathbb{Q} \\ & r &\mapsto& r \cdot r \end{array}

The real numbers

The real numbers:

(8)(,0,+,,1,):Ring where (x (): +)×((n,m: +)((x nx m) 2(1n+1m) 2)) /(x (),y ())×((n: +)((x ny b) 2(2n) 2)) 0 : n0 + : (x (),y ())(nx n+y n) : x ()(nx n) 1 : n1 : (x (),y ())(nx ny n) \begin{array}{l} \mathllap{ \vdash \;\;\;\;\;\; } \big( \mathbb{R} ,\, 0 ,\, + ,\, - ,\, 1 ,\, \cdot \big) \;\colon\; Ring \\ \text{where} \\ \begin{array}{ccl} \mathbb{R} &\coloneqq& \Big( x_{(-)} : \mathbb{Z}_+ \to \mathbb{Q} \Big) \times \bigg( ( n,\,m \,\colon\, \mathbb{Z}_+ ) \to \Big( (x_n - x_m)^2 \,\leq\, \big( \frac{1}{n} + \frac{1}{m} \big)^2 \Big) \bigg) \\ && \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \bigg/ \Big( x_{(-)} ,\, y_{(-)} \Big) \times \bigg( (n \colon \mathbb{Z}_{+}) \to \Big( (x_n - y_b)^2 \,\leq\, \big(\frac{2}{n}\big)^2 \Big) \bigg) \\ 0 &\colon& n \mapsto 0 \\ + &\colon& \big( x_{(-)} ,\, y_{(-)} \big) \;\mapsto\; \big( n \,\mapsto\, x_n + y_n \big) \\ - &\colon& x_{(-)} \,\mapsto\, \big( n \,\mapsto\, - x_n \big) \\ 1 &\colon& n \,\mapsto\, 1 \\ \cdot &\colon& \big( x_{(-)} ,\, y_{(-)} \big) \;\mapsto\; \big( n \,\mapsto\, x_n \cdot y_n \big) \end{array} \end{array}

The complex numbers

The complex numbers:

(,0,+,,1,):Ring where (z:) (Re(z),Im(z)):× 0 (0,0) + : ((Re(z 1),Im(z 1)),(Re(z 2),Im(z 2)))(Re(z 1)+Re(z 2),Re(z 1)+Re(z 2)) : (Re(z),Im(z))(Re(z),Im(z)) 1 (1,0) : ((Re(z 1),Im(z 1)),(Re(z 2),Im(z 2))) (Re(z 1)Re(z 2)Im(z 1)Im(z 2),Re(z 1)Im(z 2)+Im(z 1)Re(z 2)) \begin{array}{l} \mathllap{ \vdash \;\;\;\;\;\; } \big( \mathbb{C} ,\, 0 ,\, + ,\, - ,\, 1 ,\, \cdot \big) \;\colon\; Ring \\ \text{where} \\ \begin{array}{rcl} \big( z \colon \mathbb{C} \big) &\coloneqq& \big( \mathrm{Re}(z) ,\, \mathrm{Im}(z) \big) \,:\, \mathbb{R} \times \mathbb{R} \\ 0 &\coloneqq& (0,\,0) \\ + &\colon& \Big( \big( \mathrm{Re}(z_1) ,\, \mathrm{Im}(z_1) \big) ,\, \big( \mathrm{Re}(z_2) ,\, \mathrm{Im}(z_2) \big) \Big) \;\;\mapsto\;\; \big( \mathrm{Re}(z_1) + \mathrm{Re}(z_2) ,\, \mathrm{Re}(z_1) + \mathrm{Re}(z_2) \big) \\ - &\colon& \big( \mathrm{Re}(z) ,\, \mathrm{Im}(z) \big) \;\mapsto\; \big( - \mathrm{Re}(z) ,\, - \mathrm{Im}(z) \big) \\ 1 &\coloneqq& (1,\, 0) \\ \cdot &\colon& \Big( \big( \mathrm{Re}(z_1) ,\, \mathrm{Im}(z_1) \big) ,\, \big( \mathrm{Re}(z_2) ,\, \mathrm{Im}(z_2) \big) \Big) \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; && \;\;\mapsto\;\; \Big( \mathrm{Re}(z_1) \cdot \mathrm{Re}(z_2) - \mathrm{Im}(z_1) \cdot \mathrm{Im}(z_2) ,\;\; \mathrm{Re}(z_1) \cdot \mathrm{Im}(z_2) + \mathrm{Im}(z_1) \cdot \mathrm{Re}(z_2) \Big) \end{array} \end{array}




Construction of the number systems up to the real numbers in constructive analysis:

Formalization in Agda:

Last revised on February 10, 2023 at 14:23:15. See the history of this page for a list of all contributions to it.