nLab real number

Redirected from "located real number".
Contents

Context

Arithmetic

Analysis

Contents

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 n\mathbb{R}^n for natural numbers nn \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 00 and 11, 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:

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 R\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 XXX \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 R\mathbf{R} is Cauchy complete. From the definition of terminal object, R\mathbf{R} is an algebra of the endofunctor X𝒞(X)X \mapsto \mathcal{C}(X) in the category of Archimedean ordered fields which takes Archimedean ordered fields XX to the Archimedean ordered field 𝒞(X)\mathcal{C}(X) of equivalence classes of Cauchy sequences in XX. Every algebra of the endofunctor X𝒞(X)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 R\mathbf{R} is Dedekind complete. From the definition of terminal object, R\mathbf{R} is an algebra of the endofunctor X𝒟(X)X \mapsto \mathcal{D}(X) in the category of Archimedean ordered fields which takes Archimedean ordered fields XX to the Archimedean ordered field 𝒞(X)\mathcal{C}(X) of two-sided Dedekind cuts in XX. Every algebra of the endofunctor X𝒟(X)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, LL and UU, of a countable unbounded dense linear order, such as \mathbb{Q} (the set of rational numbers) or [1/10]\mathbb{Z}[1/10] (the set of decimal fractions), such that:

  • If aLa \in L, then bLb \in L for some b>ab \gt a.
  • If bUb \in U, then aUa \in U for some a<ba \lt b.
  • If a<ba \lt b are rational numbers, then aLa \in L or bUb \in U. (*)
  • If aLa \in L and bUb \in U, then a<ba \lt b.

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

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

We may approximate a Dedekind cut xx 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 LL and UU are inhabited).

See Dedekind completion for more.

Cauchy sequences

Classically, a real number can be given by an infinite Cauchy sequence of decimal fractions [1/10]\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...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 [1/10] \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 AC 2\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:

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:

  1. For all elements aFa \in F, the upwards unbounded open interval (a,)(a,\infty) is inhabited.
  2. For all elements aFa \in F, the downwards unbounded open interval (,a)(-\infty,a) is inhabited.
  3. For all elements aFa \in F and bFb \in F, a<ba \lt b if and only if (b,)(b,\infty) is a subinterval of (a,)(a,\infty)
  4. For all elements aFa \in F and bFb \in F, b<ab \lt a if and only if (,b)(-\infty,b) is a subinterval of (,a)(-\infty,a)
  5. For all elements aFa \in F and bFb \in F, if a<ba \lt b, then FF is a subinterval of the union of (a,)(a, \infty) and (,b)(-\infty, b)
  6. For all elements aFa \in F and bFb \in F, the intersection of (a,)(a,\infty) and (,b)(-\infty,b) is a subinterval of (a,b)(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:

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 11 such that 1<1+11 \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 aba \geq b, then aba \sim b.
  • If abcda \geq b \sim c \geq d, then ada \sim d.
  • If ab>cda \sim b \gt c \sim d, then ada \sim d.
  • If bcb \sim c whenever a<ba \lt b and c<dc \lt d, then ada \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][0,1] could be constructed as a terminal coalgebra of an endofunctor in the category of intervals. Let (,0,+,,1,,<)(\mathbb{R},0,+,-,1,\cdot,\lt) be an ordered field where 0<10 \lt 1, with a monotone f:[0,1]f:[0,1]\to \mathbb{R} such that f(0)=0f(0) = 0 and f(1)=1f(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:PosSet U\colon Pos \to Set

Consider the endofunctor

F 1:PosPos F_1\colon Pos \to Pos

defined as the ordinal product?

F 1:XωX, F_1\colon X \mapsto \omega \cdot X,

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

Proposition

The terminal coalgebra of F 1F_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 +[1,)\mathbb{R}^+ \cong [1, \infty) and ω 2={n:n2}\omega \cong \mathbb{N}_{\geq 2} = \{n \in \mathbb{N}: n \geq 2\}. Define a map

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

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

x=a 01a 11a 2,x = a_0 - \frac1{a_1 - \frac1{a_2 - \ldots}},

and the resulting bijection [1,) 2× 2×[1, \infty) \to \mathbb{N}_{\geq 2} \times \mathbb{N}_{\geq 2} \times \ldots, sending xx to (a 0,a 1,)(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 +[1,)\mathbb{R}^+ \cong [1, \infty) and ω 2\omega \cong \mathbb{N}_{\geq 2}, is to define

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

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

x=a 0+11+1a 1+11+1a 2+,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 xx to (a 0,a 1,)(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

Topologies

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

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

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 pp-adic numbers for various prime numbers pp are variations on the theme of real numbers; real numbers may be thought of as 00-adic numbers. Similarly, the real numbers are characteristic-00 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, 00-adic, characteristic-00, commutative numbers.

exceptional spinors and real normed division algebras

Lorentzian
spacetime
dimension
AA\phantom{AA}spin groupnormed division algebra\,\, brane scan entry
3=2+13 = 2+1Spin(2,1)SL(2,)Spin(2,1) \simeq SL(2,\mathbb{R})A\phantom{A} \mathbb{R} the real numberssuper 1-brane in 3d
4=3+14 = 3+1Spin(3,1)SL(2,)Spin(3,1) \simeq SL(2, \mathbb{C})A\phantom{A} \mathbb{C} the complex numberssuper 2-brane in 4d
6=5+16 = 5+1Spin(5,1)Spin(5,1) \simeq SL(2,H)A\phantom{A} \mathbb{H} the quaternionslittle string
10=9+110 = 9+1Spin(9,1) {\simeq}SL(2,O)A\phantom{A} 𝕆\mathbb{O} the octonionsheterotic/type II string

References

For more see the references at analysis.

Review and history:

As the coalgebra of the real interval:

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

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

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

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

review:

and closely related constructions in Coq have been implemented in

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

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

Something like this has been implemented in Coq:

Last revised on September 18, 2024 at 18:16:13. See the history of this page for a list of all contributions to it.