# The Real Numbers

The real numbers constitute a completion of the rational numbers, ratios of whole numbers, by filling in the gaps so as to obtain a continuum. There are several equivalent ways to do this; I chose a variant of the Dedekind cut approach, performed before the application of the standard completion of addition by introduction of negative values.

## Preliminaries

Given the natural numbers, we must first establish the multiplication and addition they support, then prove (multiply, add) that both are Abelian, the addition is cancellable and that the multiplication's restriction to positive naturals is cancellable. From this, one can build a representation of ratios, the results of dividing a natural by a positive natural, without needing the latter to be a factor of the former. There are various ways to do that, so I've picked one that happens to have some convenient properties when I come to consider linear spaces. This gives us natural ratios of form n/m = m\n for m, n natural with m non-zero (so positive); when n is also non-zero, n/m is a positive ratio.

Orthodoxy generally formulates ratios as pairs of whole numbers subject to an equivalence, [n, p] ~ [m, q] precisely if n.q = p.m, which allows a definition of multiplication as [n, p].[m, q] = [n.m, p.q] and of addition as [n, p] +[m, q] = [n.q +p.m, p.q], yielding the familiar world of ratios if we interpret [m, q] as m/q. One can do essentially the same trick – with [n, p] ~ [m, q] precisely if n+q = m+p and suitably amended addition and multiplication – to complete an abelian cancellable addition, such as that on {naturals} or on {natural ratios}, so as to obtain an additive identity (if one was previously lacking) and additive inverses. I deliberately opt to not do this until later because working only with positives saves a whole lot of fiddly complications.

Between any two distinct natural ratios, no matter how close, there are as many positive ratios as {naturals} has members; all the same, it turns out that there are not enough of them. If we complete their addition and try to use the result to define a two-dimensional plane, we can define a squared distance function (: x.x+y.y ←[x,y] :) and thus the notion of an isometry, a linear map that preserves squared distance. We discover that we only get a rather limited set of rotations (specifically, those through angles seen in pythagorean triangles or obtained from these by addition and subtraction). In particular, we can't rotate through turn / n for any natural n other than 1, 2 and 4; we can construct plenty of pairs of lines that meet in angles through which we can't rotate; and thus there are many radial lines, e.g. {[x,x]: x is a natural ratio} which manage to pass from inside the unit circle, {[x,y]: x.x+y.y=1}, to outside it without ever intersecting it. The purpose of the real numbers is to provide a way to fill in the gaps so as to avoid these deficiencies. (Technically, the algebraic numbers suffice to fill in the gaps I've actually mentioned here; but there are other gaps, that it's harder to explain, for which one needs the reals.)

## Initial sub-sets

Let a sub-set Q of {positive ratios} be termed initial precisely if x in Q implies Q subsumes {positive ratio y: x > y}; and understand two such subsets as equivalent precisely if there is at most one ratio in one of them but not in the other. (One could equally say only finitely many in place of at most one, as it happens.) Every non-empty initial has infinitely many members. I shall refer to a non-empty proper initial sub-set of {positive ratios}, understood modulo this equivalence, simply as a positive; the collection of such is then {positives}. The empty set is an initial sub-set of {positive ratios} and serves as a zero; the set {positive ratios} is also initial in itself and serves as an infinity; the former is empty and the latter is not proper, so neither is included in {positives}.

When two positives are equivalent but distinct, with the single ratio in one but not the other being some r, then the two positives are necessarily {x: x < r} and {x: x ≤ r}, from the specification of their being initial; these shall represent the positive ratio r within {positives}. When an initial sub-set of the positive ratios is {x: x ≤ r} for some r, I shall refer to it as a rational positive and to r as its maximum; it should be evident that an initial sub-set of the positives has a maximal element precisely if it is a rational positive and this element is its maximum. I shall refer to the rational positive that represents any (positive) natural as a positive ratio as a natural positive (not to be confused with the positive natural that it represents).

We may define addition and multiplication on {positives} by the simple expedient of applying to every member: that is, x.y = {r.s: r in x, s in y} and x+y = {r+s: r in x, s in y}. We must, again, show that each is cancellable and that the multiplication is complete (hence forms a group). The latter is achieved by identifying the inverse of a positive, x, as {positive ratio r: for all s in x, r.s < 1}. We can extend the addition via {}+x = x to make {} serve as additive identity, 0; extending multiplication by using the same rule as for positives, we obtain {}.x = {} for every initial x, so 0 breaks multiplicative cancellability (as is only to be expected).

We obtain a natural order on initial subsets from: x ≥ y precisely if {r in y: r not in x} is finite; this arises precisely when x subsumes y or is equivalent to y. This leads conveniently to any non-empty set of initial subsets having a least upper bound (its union) and a greatest lower bound (its intersection), although the latter may be empty and the former might be infinity. When a set of positives thus combined is finite, these shall be maximal and minimal elements of the set (hence neither zero nor infinity). If we have an infinite sequence of initial subsets, we can derive from it two (non-strictly) monotonic sequences, one increasing, the other decreasing, by taking the intersection and union (respectively) of all entries in the sequence past each given point in it. By taking the union of the former and the intersection of the latter we obtain lower and upper bounds (respectively) on what values sub-sequences of the original sequence can converge to. If the original sequence does converge, these two bounds shall coincide and give us the limiting value. In particular, whenever a sequence is convergent, we are assured that it does have a limit; note, however, that even the limit of a convergent sequence of positives may be {}, i.e. zero.

I generally prefer to work with {positives} rather than {reals} wherever I can; it remains that the reals do have a proper place in mathematics and so it is desirable to actually show how they may be obtained from the positives.

### Positive power

Given our multiplication on {positives}, we can use repeated multiplication to induce powers in the usual way. Initially this gives us (: ({positives}: power(n) |{positives}) ←n |{naturals}) with power(0, x) = 1 and power(1+n, x) = x.power(n, x) for each natural n and positive x. Because multiplication on positives respects their ordering, i.e. a > b implies x.a > x.b for every positive x, each power aside from power(0) is monotonically strictly increasing – for natural n > 0, with positives x > y, we know power(n, x) > power(n, y). We can thus define, for each positive natural n, ({positives}: power(1/n) |{positives}) by power(1/n, x) = {positive ratio r: power(n, r) < x}; because power(n) is monotonic, this is an initial sub-set of {positive ratios} which we can duly interpret as a positive real.

Furthermore, because each power(n) is continuous on {positives}, we can infer that power(1/n) is in fact reverse(power(n)). As composing powers corresponds to multiplying exponents, power(n)∘power(m) = power(n.m), we can duly construct power(n/m) = power(1/m)∘power(n) and extend power to (: ({positives}: power(r) |{positives}) ←r |{natural ratios}). This still has every power except power(0) strictly monotonically increasing. Furthermore, for each positive x, (: power(r, x) ←r |{positive ratios}) is also monotonically strictly increasing, which enables us to define, for positive p and x, power(p, x) = {positive ratio q: q < power(r, s) for some r in p, s in x} and, again, infer that this is an initial sub-set of {positive ratios} that we can interpret as a positive real. We are thus able to extend the definition of power to (: ({positives}: power(p) |{positives}) ←p |{positives}), every output of which is monotonically increasing, as is every output of its transpose.

## The real numbers

Finally, we are ready to obtain the real numbers by completing the addition; a real number, or simply real, is a pair x←y of positives, understood modulo the equivalence (: (x←y)←(u←v); x+v = y+u :). The pair x←y, understood modulo this equivalence, is denoted x−y. We can induce addition, multiplication and an ordering on {reals}, from those on {positives}, as

• (x←y)+(u←v) = (x+u)←(y+v),
• (x←y).(u←v) = (x.u +y.v)←(y.u +x.v) and
• (x←y) < (u←v) precisely if x+v < y+u.

Then (: (x+a←a) ←x, a in positives :) embeds the initial sub-sets of {positive ratios} in {reals} while preserving arithmetic structure and ordering. We can extend − to apply to reals via (x←y)−(u←v) = (x+v)←(y+u), which naturally interacts faithfully with this embedding.

Each natural number is the set of earlier naturals; thus the natural 0 is {} and the natural 1 is {0} = {{}} = (: {}←{} :). Among subsets of {positive ratios}, {} does indeed again serve as the additive identity, although the multiplicative identity, the rational positive that represents the natural 1, is {n/m: 0 in n in natural m}; the ratio that represents 1 is repeat(1) = {relations}. We could define a real to be a pair of initial sub-sets of {positive ratios} subject to the same equivalence, but this would then have left us with the natural 1 = {}←{} as one of the pairs we can interpret as a real serving to represent 0. Rather than overly encumber contexts with the need to be clear about how to read {}←{}, I chose to have reals be pairs of positives; then no real happens to be equal, as a relation, to any natural or ratio (since no positive is a natural; indeed, every positive is an infinite collection of positive ratios).

The real a−a, for arbitrary positive a (all such reals are trivially equivalent), serves as additive identity and (: (x←y)←(y←x) :) equips every real with an additive inverse. A real that is > the additive identity is described as positive (and is the real which represents some positive); a real that is < the additive identity is described as negative (and is the additive inverse of some positive real).

The embedding of initial subsets of {positive ratios} in {reals} embeds {}, the additive identity, as a←a for arbitrary positive a; for any positive ratio r, using our prior embedding in {positives} as {x: x≤r} (or, equivalently, {x: x<r}) we thus obtain a real ({x: x≤r}+a)←a, for arbitrary positive a, that represents the ratio r. I refer to the additive identity of the reals, the images of rational positives under the embedding of positives in {reals} and the additive inverses of these as rational; a positive rational is then always the real that represents some rational positive. I refer to the images of natural positives, as embedded in {reals}, along with their additive inverses and the additive identity, as whole (the whole reals are the integers, in effect).

In practice it is seldom interesting to distinguish a whole positive real, a natural positive or a natural ratio from the (positive) natural they represent; nor to distinguish a positive rational or a rational positive from the positive ratio they represent. None the less, it is technically necessary to draw these distinctions: they are distinct relations, so it is important to be specific about which of them any given relation accepts as a left or right value; and it is at least desirable that an entity of one type should not also be understandable as an entity of another type unless it, via relevant embedding, represents the same value either way (as {} does when understood as the additive identity both among initial sub-sets of {positive ratios} and among naturals).

## The continuum

Classically, one would define continuity of a function, ({reals}: f :{reals}), at a given input, x, by specifying that: for every positive real e, there is some positive real h such that, for all real y satisfying y+h > x and x+h > y, y is a right value of f with f(y)+e > f(x) and f(x)+e > f(y). However, I have an intense dislike of the challenge-response protocol involved here, due to there being no way to prove any result of this kind without use of reductio ad absurdum. So I'm trying to find an alternative.  Written by Eddy.