nLab real number

Idea

A real number is a number that may be approximated by rational numbers. Equipped with the operations of addition and multiplication induced from the rational numbers, real numbers form a field, commonly denoted $\mathbb{R}$. The underlying set is the completion of the ordered field $\mathbb{Q}$ of rational numbers: the result of adjoining to $\mathbb{Q}$ suprema for every inhabited bounded subset with respect to the natural ordering of rational numbers.

The set of real numbers also carries naturally the structure of a topological space and as such $\mathbb{R}$ is called the real line also known as the continuum. Equipped with both the topology and the field structure, $\mathbb{R}$ is a topological field and as such is the uniform completion of $\mathbb{Q}$ equipped with the absolute value metric.

Together with its cartesian products – the Cartesian spaces $\mathbb{R}^n$ for natural numbers $n \in \mathbb{N}$ – the real line $\mathbb{R}$ is a standard formalization of the idea of continuous space. The more general concept of (smooth) manifold is modeled on these Cartesian spaces. These, in turn are standard models for the notion of space in particular in physics (see spacetime), or at least in classical physics. See at geometry of physics for more on this.

History

The original idea of a real number came from geometry; one thinks of a real number as specifying a point on a line, with line understood as the abstract idea of the object that a pencil and a ruler draw on a piece of paper. (More precisely, given two distinct points on the line, called $0$ and $1$, you get a bijection between the points and the real numbers.)

Euclid (citing Eudoxus) dealt with ratios of geometric magnitudes, which give positive real numbers; an arbitrary real number is then a difference of ratios of magnitudes. However, the Greeks did not think of such ratios as numbers; that appears to have been an insight of the Arabs. See more at Eudoxus real number.

A big project of the 19th century (at least in hindsight) was the ‘arithmetisation of analysis’: showing how real numbers could be defined completely in terms of rational numbers (and the desired classes of functions on them could be defined in terms of the general point-set notion of function). Two successful approaches were developed in 1872, Richard Dedekind's definition of real numbers as certain sets of rational numbers (called Dedekind cuts) and Georg Cantor's definition as certain sequences of rational numbers (called Cauchy sequences).

A more modern approach is instead to characterise the properties that the set of real numbers must have and to prove that this is categorical (unique up to a unique bijection preserving those properties). Then the important result of the 19th-century programme is simply that this is consistent (that there exists at least one such set). One can even use Hilbert's or Tarski's axioms for geometry to do this characterisation, coming full circle back to geometry.

Exactly how to define or characterise real numbers is still important in constructive mathematics and topos theory with its internal logic. For more on this, see real numbers object and the examples below.

Definitions and characterizations

There are two basic approaches possible: to define what a real number is as a mathematical object, or to define the real line as a specific object in some previously known category.

The terminal Archimedean ordered field

There is a well-known algebraic (more or less) characterisation of the real line as the ‘terminal Archimedean ordered field’ (cf. Richman08) This can be interpreted as follows:

• A field is well known in algebra; if it matters, we mean a Heyting field.
• An ordered field means a strictly totally ordered field.
• An Archimedean ordered field is an ordered field satisfying the Archimedean property.
• An Archimedean ordered field is terminal if it is a terminal object in the category of Archimedean ordered fields.

We speak of the such field because it is unique up to unique isomorphism by definition of terminal object.

In predicative mathematics, one can define $\mathbf{R}$ by fiat via the universal property of the real numbers as the terminal Archimedean ordered field. From this characterization, the real numbers are a terminal coalgebra of the identity endofunctor $X \mapsto X$ on the category of Archimedean ordered fields.

If quotient sets exist and sequence algebras of Archimedean ordered fields exist, then it is provable that $\mathbf{R}$ is Cauchy complete. From the definition of terminal object, $\mathbf{R}$ is an algebra of the endofunctor $X \mapsto \mathcal{C}(X)$ in the category of Archimedean ordered fields which takes Archimedean ordered fields $X$ to the Archimedean ordered field $\mathcal{C}(X)$ of equivalence classes of Cauchy sequences in $X$. Every algebra of the endofunctor $X \mapsto \mathcal{C}(X)$ in the category of Archimedean ordered fields is a Cauchy complete Archimedean ordered field.

Similarly, if power sets of Archimedean ordered fields exist, then it is provable that $\mathbf{R}$ is Dedekind complete. From the definition of terminal object, $\mathbf{R}$ is an algebra of the endofunctor $X \mapsto \mathcal{D}(X)$ in the category of Archimedean ordered fields which takes Archimedean ordered fields $X$ to the Archimedean ordered field $\mathcal{C}(X)$ of two-sided Dedekind cuts in $X$. Every algebra of the endofunctor $X \mapsto \mathcal{D}(X)$ in the category of Archimedean ordered fields is a Dedekind complete Archimedean ordered field.

Dedekind cuts

Consider two inhabited subsets, $L$ and $U$, of a countable unbounded dense linear order, such as $\mathbb{Q}$ (the set of rational numbers) or $\mathbb{Z}[1/10]$ (the set of decimal fractions), such that:

• If $a \in L$, then $b \in L$ for some $b \gt a$.
• If $b \in U$, then $a \in U$ for some $a \lt b$.
• If $a \lt b$ are rational numbers, then $a \in L$ or $b \in U$. (*)
• If $a \in L$ and $b \in U$, then $a \lt b$.

We may define a Dedekind real number to be such a pair, which is also called a Dedekind cut.

If $x \coloneqq (L,U)$ is a Dedekind cut, then we write $a \lt x$ to mean that $a \in L$ and $x \lt b$ to mean that $b \in U$.

We may approximate a Dedekind cut $x$ as closely as we like by applying (*) as often as necessary. This will be only finitely often, for any fixed positive level of approximation, given initial upper and lower bounds (which exist since $L$ and $U$ are inhabited).

See Dedekind completion for more.

Cauchy sequences

Classically, a real number can be given by an infinite Cauchy sequence of decimal fractions $\mathbb{Z}[1/10]$, each of which is a decimal fraction that approximates the real number to a given number of decimal places. However, many real numbers have several representations, i.e.

$$1/10 = 0.099999... = 0.10000...$$

so we need to specify an equivalence relation on the Cauchy sequences. Thus, $\mathbb{R}$ is constructed as a subquotient of the function set $\mathbb{Z}[1/10]^{\mathbb{N}}$.

We can generalise this to any Cauchy sequence of rational numbers, and $\mathbb{R}$ is constructed as a subquotient of the function set $\mathbb{Q}^{\mathbb{N}}$.

This construction is equivalent to the construction by Dedekind cuts, at least assuming the weak countable choice principle $\mathrm{AC}_{\mathbb{N}2}$ (which also follows from excluded middle). Thus it is popular in both classical mathematics and traditional constructive mathematics (which accepts countable choice). However, in stricter forms of constructive mathematics, including those used as internal languages in topos theory, the Cauchy reals and Dedekind reals are not equivalent. (On the other hand, by generalising to Cauchy nets, we recover the Dedekind reals again.)

See Cauchy real number and generalized Cauchy real number for more.

The initial sequentially modulated Cauchy complete archimedean field

There is an algebraic (more or less) characterisation of the real line as the ‘initial sequentially modulated Cauchy complete archimedean field’. This can be interpreted as follows:

• A field is well known in algebra; if it matters, we mean a Heyting field.
• An ordered field means a strictly totally ordered field.
• An archimedean field is an ordered field satisfying the archimedean property.
• An archimedean field is sequentially modulated Cauchy complete if all Cauchy sequences in the field with a $\mathbb{N}$-modulus of convergence converge.
• A sequentially modulated Cauchy complete archimedean field is initial if it is an initial object in the category of sequentially modulated Cauchy complete archimedean fields.

The initial sequentially modulated Cauchy complete ordered field results in the HoTT book real numbers.

The Dedekind complete ordered field

There is a well-known algebraic (more or less) characterisation of the real line as the ‘Dedekind complete ordered field’, or sometimes the ‘Dedekind complete archimedean field’. This can be interpreted as follows:

• A field is well known in algebra; if it matters, we mean a Heyting field.
• An ordered field means a linearly ordered field.
• An archimedean field is an ordered field satisfying the archimedean property.
• An ordered field is Dedekind complete if it is Dedekind-complete:

1. For all elements $a \in F$, the upwards unbounded open interval $(a,\infty)$ is inhabited.
2. For all elements $a \in F$, the downwards unbounded open interval $(-\infty,a)$ is inhabited.
3. For all elements $a \in F$ and $b \in F$, $a \lt b$ if and only if $(b,\infty)$ is a subinterval of $(a,\infty)$
4. For all elements $a \in F$ and $b \in F$, $b \lt a$ if and only if $(-\infty,b)$ is a subinterval of $(-\infty,a)$
5. For all elements $a \in F$ and $b \in F$, if $a \lt b$, then $F$ is a subinterval of the union of $(a, \infty)$ and $(-\infty, b)$
6. For all elements $a \in F$ and $b \in F$, the intersection of $(a,\infty)$ and $(-\infty,b)$ is a subinterval of $(a,b)$

In impredicative mathematics, we speak of the such field because it is unique up to unique isomorphism.

Theorem

Assuming impredicative foundations, there is an archimedean field $\mathbb{R}$ which is Dedekind-complete, and into which every archimedean field embeds. Furthermore, every Dedekind-complete ordered field is isomorphic to $\mathbb{R}$, and uniquely so.

Proof

Construct $\mathbb{R}$ using, say, Dedekind cuts of rational numbers. Then it is well known how to prove these facts about $\mathbb{R}$, so we omit the proof for now.

However, we note that the proof is valid in weak foundations, in particular internal to any topos with a natural numbers object. One can actually work in even weaker foundations than that; see the constructions at real numbers object.

Even weaker foundations are possible if one allows the underlying set of $\mathbb{R}$ to be large.

However, if we are working in predicative mathematics with multiple universes in the foundation, the Dedekind real numbers would no longer be unique up to unique isomorphism, but rather there would be a set of Dedekind real numbers for each universe.

The Cauchy complete ordered field

There is a well-known algebraic (more or less) characterisation of the real line as the ‘Cauchy complete ordered field’, or sometimes the ‘Cauchy complete archimedean field’. This can be interpreted as follows:

• A field is well known in algebra; if it matters, we mean a Heyting field.
• An ordered field means a linearly ordered field.
• An archimedean field is an ordered field satisfying the archimedean property.
• An ordered field is Cauchy complete if every Cauchy net in the field converges.

In impredicative mathematics, we speak of the such field because it is unique up to unique isomorphism.

Theorem

Assuming impredicative foundations, there is an archimedean field $\mathbb{R}$ which is Cauchy-complete, and into which every archimedean field embeds. Furthermore, every Cauchy-complete ordered field is isomorphic to $\mathbb{R}$, and uniquely so.

Proof

Construct $\mathbb{R}$ using, say, Cauchy nets of rational numbers. Then it is well known how to prove these facts about $\mathbb{R}$, so we omit the proof for now.

However, we note that the proof is valid in weak foundations, in particular internal to any topos with a natural numbers object. One can actually work in even weaker foundations than that; see the constructions at real numbers object.

Even weaker foundations are possible if one allows the underlying set of $\mathbb{R}$ to be large.

However, if we are working in predicative mathematics with multiple universes in the foundation, the Cauchy real numbers would no longer be unique up to unique isomorphism, but rather there would be a set of Cauchy real numbers for each universe.

As an archimedean Tarski group

There is a characterisation of the real line as the ‘complete archimedean Tarski group’ due to Alfred Tarski. This can be interpreted as follows:

• An abelian group is well known in algebra.
• An linearly ordered abelian group is an abelian group with a linear order.
• A densely linearly ordered abelian group is an linearly ordered abelian group that is also a dense linear order.
• A Tarski group is a densely linearly ordered abelian group with a point $1$ such that $1 \lt 1 + 1$.
• An archimedean Tarski group is a Tarski group satisfying the archimedean property.
• An archimedean Tarski group is complete if it is Dedekind-complete.

See Tarski's axiomatization of the real numbers for more information.

The locale of real numbers

Consider binary relations $\sim$ on a countable inhabited dense linear order without endpoints, such as the rational numbers, satisfying these four properties:

• If $a \geq b$, then $a \sim b$.
• If $a \geq b \sim c \geq d$, then $a \sim d$.
• If $a \sim b \gt c \sim d$, then $a \sim d$.
• If $b \sim c$ whenever $a \lt b$ and $c \lt d$, then $a \sim d$.

The collection of all such relations form a frame, which we may interpret (by definition) as the locale of real numbers. It can also be defined as the localic completion of the rational numbers.

We may then define a localic real number to be a point of this locale.

This agrees with the notion of Dedekind real number, even in very weak (predicative and constructive) foundations.

See locale of real numbers for more.

Unit intervals

The unit interval of the real numbers $[0,1]$ could be constructed as a terminal coalgebra of an endofunctor in the category of intervals. Let $(\mathbb{R},0,+,-,1,\cdot,\lt)$ be an ordered field where $0 \lt 1$, with a monotone $f:[0,1]\to \mathbb{R}$ such that $f(0) = 0$ and $f(1) = 1$. The set $\mathbb{R}$ of real numbers is the initial such ordered field.

See also: dyadic interval coalgebra, decimal interval coalgebra, rational interval coalgebra.

$\mathbb{R}^+$ as a terminal coalgebra

The positive real line $\mathbb{R}^+$ may be characterized as the terminal coalgebra for an endofunctor

Let Pos be the category of posets with a forgetful functor

$$U\colon Pos \to Set$$

Consider the endofunctor

$$F_1\colon Pos \to Pos$$

defined as the ordinal product?

$$F_1\colon X \mapsto \omega \cdot X,$$

for $\omega \in Pos$, where $\omega \cdot X$ is the cartesian product $U(\omega) \times U(X)$ with the lexicographic order.

Proposition

The terminal coalgebra of $F_1$ is order isomorphic to the non-negative real line $\mathbb{R}^+$, with its standard order.

Proof

This is theorem 5.1 in (Pavlovic–Pratt 1999).

There are many ways of setting up this description of $\mathbb{R}^+$, depending on the coalgebra structure $\mathbb{R}^+ \to \omega \cdot \mathbb{R}^+$ chosen. Here is one: there are evident poset isomorphisms $\mathbb{R}^+ \cong [1, \infty)$ and $\omega \cong \mathbb{N}_{\geq 2} = \{n \in \mathbb{N}: n \geq 2\}$. Define a map

$$(\alpha, \beta): [1, \infty) \to \mathbb{N}_{\geq 2} \cdot [1, \infty)$$

where $\alpha(x)$ is the smallest integer strictly greater than $x$, and $\beta(x) = 1/(\alpha(x) - x)$. The stream of integers $a_n = \alpha(\beta^n(x))$ gives a continued fraction representation of $x$ in the form

$$x = a_0 - \frac1{a_1 - \frac1{a_2 - \ldots}},$$

and the resulting bijection $[1, \infty) \to \mathbb{N}_{\geq 2} \times \mathbb{N}_{\geq 2} \times \ldots$, sending $x$ to $(a_0, a_1, \ldots)$, is in fact a poset isomorphism if we endow the right-hand side with the lexicographic order.

Another way, which circumvents the use of isomorphisms $\mathbb{R}^+ \cong [1, \infty)$ and $\omega \cong \mathbb{N}_{\geq 2}$, is to define

$$(\alpha, \beta): \mathbb{R}^+ \to \omega \cdot \mathbb{R}^+$$

where $\alpha(x)$ is the floor of $x$, and $\beta(x) = 1/(1 - x + \alpha(x)) - 1$. Then $a_n = \alpha(\beta^n(x))$ gives a continued fraction representation of $x$ in the form

$$x = a_0 + \frac1{1 + \frac1{a_1 + \frac1{1 + \frac1{a_2 + \ldots}}}},$$

and the resulting bijection $\mathbb{R}_+ \to \omega \times \omega \times \ldots$, sending $x$ to $(a_0, a_1, \ldots)$, is again a poset isomorphism if we endow the right-hand side with the lexicographic order.

There are more and similar characterizations along these lines. An interesting application of the coalgebraic views is that they allow defining morphisms between the reals. A coalgebaic version Dedekind cuts or Conway numbers makes $\mathbb{R}$ into a compact category where the addition arises as the biproduct. The real vector spaces are the $\mathbb{R}$-enriched bicompletions and linear operators arise as the $\mathbb{R}$-enriched Kan extensions. (Pavlovic 2020)

Smooth real numbers

The smooth real numbers (say in a smooth topos) are only an ordered local ring rather than an ordered field, because there might be non-zero non-invertible nilpotent infinitesimals in the smooth real numbers. Nevertheless, the quotient of the smooth real numbers by the ideal of non-invertible elements is one of the ordered field of real numbers as defined above.

Other definitions

• Eudoxus real number
• prealgebra real number

Topologies

There are alternative topologies on $\mathbb{R}$ sometimes considered:

• the discrete topology (not very interesting),
• the order topology or absolute-value topology? (the usual topology of a Euclidean metric space),
• the upper-interval topology? or the lower-interval topology?,
• the lower semicontinuous topology or the upper semicontinuous topology,
• the K-topology.

Another variant of $\mathbb{R}$ as a topological space is the

• long line.

Generalisations

The term ‘real number’ was originally introduced to indicate that one is not considering the generalistion to complex numbers or other kinds of hypercomplex numbers. Accordingly, that term ‘real’ may sometimes be used for another generalisation of real numbers to indicate again that one is not considering a complexification.

The extended real numbers include $\pm\infty$ as well as the real numbers; one may speak of finite numbers or bounded numbers to indicate that one is not considering this extension. Lower reals, upper reals, and MacNeille reals are related generalisations studied in constructive mathematics, although with excluded middle they are (at least if bounded) the same as ordinary real numbers; one may speak of located numbers to indicate that one is not considering such extensions.

Surreal numbers and the hyperreal numbers of nonstandard analysis are two ways to include infinite and infinitesimal versions of real numbers (besides the trivial case of $\pm\infty$); one may speak of standard numbers to indicate that one is not considering such extensions (although the precise meaning of ‘standard’ depends on the universe that one is working in).

In descriptive set theory, one often says ‘real number’ for an element of Baire space $\mathbb{N}^{\mathbb{N}}$. This is not really a generalisation; by the Schroeder-Bernstein theorem, the underlying sets of $\mathbb{R}$ and $\mathbb{N}^{\mathbb{N}}$ are isomorphic. Constructively, $\mathbb{N}^{\mathbb{N}}$ can still be thought of as the set of irrational numbers, so this use of the term may actually be a restriction.

Floating-point numbers? are often used in computer programming to represent real numbers, but they do not behave very well; one may speak of infinite-precision numbers to indicate that one's programming environment models ‘real real numbers’.

As mentioned above, the $p$-adic numbers for various prime numbers $p$ are variations on the theme of real numbers; real numbers may be thought of as $0$-adic numbers. Similarly, the real numbers are characteristic-$0$ numbers since they are based on the prime field $\mathbb{Q}$; one could also start the construction with a different characteristic (although it makes more sense to get analogues of complex numbers than of real numbers).

Finally, one can consider points on a noncommutative line instead of the usual commutative numbers.

So in summary, this page is about the real, finite, located, standard, analytic, infinite-precision, $0$-adic, characteristic-$0$, commutative numbers.

Related concepts

• real numbers object

• computable real number

• Cauchy real number

• Dedekind real number

• real cohomology, real homotopy theory

• p-adic numbers

• in constructive analysis one may use the completion monad for dealing with real numbers

• exact real computer arithmetic

• real-cohesive homotopy type theory

exceptional spinors and real normed division algebras

Lorentzian spacetime dimension	$\phantom{AA}$spin group	normed division algebra	$\,\,$ brane scan entry
$3 = 2+1$	$Spin(2,1) \simeq SL(2,\mathbb{R})$	$\phantom{A}$ $\mathbb{R}$ the real numbers	super 1-brane in 3d
$4 = 3+1$	$Spin(3,1) \simeq SL(2, \mathbb{C})$	$\phantom{A}$ $\mathbb{C}$ the complex numbers	super 2-brane in 4d
$6 = 5+1$	$Spin(5,1) \simeq$ SL(2,H)	$\phantom{A}$ $\mathbb{H}$ the quaternions	little string
$10 = 9+1$	Spin(9,1) ${\simeq}$ “SL(2,O)”	$\phantom{A}$ $\mathbb{O}$ the octonions	heterotic/type II string

References

For more see the references at analysis.

• Nicolas Bourbaki, Real Numbers, Chapter IV in: General topology, Elements of Mathematics, Springer (1971, 1990, 1995) [doi:10.1007/978-3-642-61701-0]

Review and history:

• Leo Corry, §10.5 in: A Brief History of Numbers, Oxford University Press (2015) [ISBN:9780198702597]

As the coalgebra of the real interval:

• Dusko Pavlovic, Vaughan Pratt, On coalgebra of real numbers, Electronic Notes in Theoretical Computer Science 19 (1999) 103-117, doi:10.1016/S1571-0661(05)80272-5, CiteSeerx

A definition of the real numbers as the terminal Archimedean ordered field and as a complete Archimedean ordered field:

• Fred Richman, Real numbers and other completions, Mathematical Logic Quarterly 54 1 (2008) 98-108 [doi:10.1002/malq.200710024]

A compact category $\mathbb{R}$ making the $\mathbb{R}$-linear operators into $\mathbb{R}$-enriched Kan extensions:

• Dusko Pavlovic, From process-propositions-as-types to categorified real numbers

  and monoidal computers_, Logic and Structure in Computer Science 1000-1070, doi:10.1007/978-3-031-24117-8, arXiv:2007.10057

The definition of the real numbers in constructive analysis as Cauchy real numbers, namely as regular Cauchy sequences of rational numbers is due to:

• Errett Bishop: Foundations of Constructive Analysis, McGraw-Hill (1967)

• Errett Bishop, Douglas Bridges: Constructive Analysis, Grundlehren der mathematischen Wissenschaften 279, Springer (1985) [doi:10.1007/978-3-642-61667-9]

Direct formalization of the definition of Cauchy real numbers from Bishop (1967) in Agda:

• Martin Lundfall, Formalizing real numbers in Agda (2015) [pdf, pdf, github]

• Zachary Murray, Constructive Analysis in the Agda Proof Assistant [arXiv:2205.08354, github]

review:

• Zachary Murray, Constructive Real Numbers in the Agda Proof Assistant, talk at CQTS, (Feb 2023) [video:YT]

and closely related constructions in Coq have been implemented in

• Robbert Krebbers, Bas Spitters, Type classes for efficient exact real arithmetic in Coq, Logical Methods in Computer Science, 9 1 (2013) lmcs:958 [arXiv:1106.3448, doi:10.2168/LMCS-9(1:1)2013]

following a monadic re-formulation (via the completion monad) due to

• Russell O'Connor, A Monadic, Functional Implementation of Real Numbers, Math. Struc. Comp. Sci. 17 1 (2007) 129-159 [arXiv:cs/0605058, doi:10.1017/S0960129506005871]

Overview of implementation of real numbers in proof assistants (cf. constructive analysis):

• Sylvie Boldo, Catherine Lelay, Guillaume Melquiond, Formalization of Real Analysis: A Survey of Proof Assistants and Libraries, Mathematical Structures in Computer Science 26 7 (2016) 1196-1233 [hal:00806920, doi:10.1017/S0960129514000437]

A novel construction principle of the type of real numbers, as a higher inductive-inductive type in univalent homotopy type theory, not reliant on representatives by sequences of rational numbers, and with provable Cauchy completeness even without extra axiom of countable choice is laid out (cf. HoTT book real numbers) in

• Univalent Foundations Project: Chapter 11 of: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]

Something like this has been implemented in Coq:

• Gaëtan Gilbert, Formalising Real Numbers in Homotopy Type Theory, in CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (2017) 112–124 [arXiv:1610.05072, doi:10.1145/3018610.3018614]