11.3 Cauchy reals

The Cauchy reals are, by intent, the completion of โ„š under limits of Cauchy sequencesPlanetmathPlanetmath. In the classical construction of the Cauchy reals, we consider the set ๐’ž of all Cauchy sequences in โ„š and then form a suitable quotient ๐’ž/โ‰ˆ. Then, to show that ๐’ž/โ‰ˆ is Cauchy completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, we consider a Cauchy sequence x:โ„•โ†’๐’ž/โ‰ˆ, lift it to a sequencePlanetmathPlanetmath of sequences xยฏ:โ„•โ†’๐’ž, and construct the limit of x using xยฏ. However, the lifting ofย x to xยฏ uses the axiom of countable choice (the instance ofย (LABEL:eq:ac) where X=โ„•) or the law of excluded middleMathworldPlanetmathPlanetmath, which we may wish to avoid. Every construction of reals whose last step is a quotient suffers from this deficiency. There are three common ways out of the conundrum in constructive mathematics:

  1. 1.

    Pretend that the reals are a setoid (๐’ž,โ‰ˆ), i.e., the type of Cauchy sequences ๐’ž with a coincidence relationMathworldPlanetmathPlanetmathPlanetmath attached to it by administrative decree. A sequence of reals then simply is a sequence of Cauchy sequences representing them.

  2. 2.

    Give in to temptation and accept the axiom of countable choice. After all, the axiom is valid in most models of constructive mathematics based on a computational viewpoint, such as realizability models.

  3. 3.

    Declare the Cauchy reals unworthy and construct the Dedekind reals instead. Such a verdict is perfectly valid in certain contexts, such as in sheaf-theoretic models of constructive mathematics. However, as we saw in \autorefsec:dedekind-reals, the constructive Dedekind reals have their own problems.

Using higher inductive types, however, there is a fourth solution, which we believe to be preferable to any of the above, and interesting even to a classical mathematician. The idea is that the Cauchy real numbers should be the free complete metric space generated byย โ„š. In general, the construction of a free gadget of any sort requires applying the gadget operationsMathworldPlanetmath repeatedly many times to the generatorsPlanetmathPlanetmathPlanetmath. For instance, the elements of the free groupMathworldPlanetmath on a set X are not just binary productsPlanetmathPlanetmathPlanetmathPlanetmath and inversesMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath of elements of X, but words obtained by iterating the product and inverse constructions. Thus, we might naturally expect the same to be true for Cauchy completion, with the relevant โ€œoperationโ€ being โ€œtake the limit of a Cauchy sequenceโ€. (In this case, the iteration would have to take place transfinitely, since even after infinitely many steps there will be new Cauchy sequences to take the limit of.)

The argument referred to above shows that if excluded middle or countable choice hold, then Cauchy completion is very special: when building the completion of a space, it suffices to stop applying the operation after one step. This may be regarded as analogous to the fact that free monoids and free groups can be given explicit descriptions in terms of (reduced) words. However, we saw in \autorefsec:free-algebras that higher inductive types allow us to construct free gadgets directly, whether or not there is also an explicit description available. In this sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath we show that the same is true for the Cauchy reals (a similar technique would construct the Cauchy completion of any metric space; see \autorefex:metric-completion). Specifically, higher inductive types allow us to simultaneously add limits of Cauchy sequences and quotient by the coincidence relation, so that we can avoid the problem of lifting a sequence of reals to a sequence of representatives.

Title 11.3 Cauchy reals