11.3.2 Induction and recursion on Cauchy reals

In order to do anything useful with ℝ𝖼, of course, we need to give its inductionMathworldPlanetmath principle. As is the case whenever we inductively define two or more objects at once, the basic induction principle for ℝ𝖼 and ∼ requires a simultaneous induction over both at once. Thus, we should expect it to say that assuming two type families over ℝ𝖼 and ∼, respectively, together with data corresponding to each constructor, there exist sectionsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath of both of these families. However, since ∼ is indexed on two copies of ℝ𝖼, the precise dependencies of these families is a bit subtle. The induction principle will apply to any pair of type families:

A :ℝ𝖼→𝒰
B :∏x,y:ℝ𝖼A(x)β†’A(y)β†’βˆΟ΅:β„š+(x∼ϡy)→𝒰.

The type of A is obvious, but the type of B requires a little thought. Since B must depend on ∼, but ∼ in turn depends on two copies of ℝ𝖼 and one copy of β„š+, it is fairly obvious that B must also depend on the variables x,y:ℝ𝖼 and Ο΅:β„š+ as well as an element of (x∼ϡy). What is slightly less obvious is that B must also depend on A⁒(x) and A⁒(y).

This may be more evident if we consider the non-dependent case (the recursion principle), where A is a simple type (rather than a type family). In this case we would expect B not to depend on x,y:ℝ𝖼 or x∼ϡy. But the recursion principle (along with its associated uniqueness principle) is supposed to say that ℝ𝖼 with ∼ϡ is an β€œinitial objectMathworldPlanetmath” in some categoryMathworldPlanetmath, so in this case the dependency structureMathworldPlanetmath of A and B should mirror that of ℝ𝖼 and ∼ϡ: that is, we should have B:Aβ†’Aβ†’β„š+→𝒰. Combining this observation with the fact that, in the dependent case, B must also depend on x,y:ℝ𝖼 and x∼ϡy, leads inevitably to the type given above for B.

It is helpful to think of B as an ϡ-indexed family of relationsMathworldPlanetmathPlanetmath between the types A⁒(x) and A⁒(y). With this in mind, we may write B⁒(x,y,a,b,ϡ,ξ) as (x,a)⌒ϡξ(y,b). Since ξ:x∼ϡy is unique when it exists, we generally omit it from the notation and write (x,a)⌒ϡ(y,b); this is harmless as long as we keep in mind that this relation is only defined when x∼ϡy. We may also sometimes simplify further and write a⌒ϡb, with x and y inferred from the types of a and b, but sometimes it will be necessary to include them for clarity.

Now, given a type family A:ℝ𝖼→𝒰 and a family of relations ⌒ as above, the hypotheses of the induction principle consist of the following data, one for each constructor of ℝ𝖼 or ∼:

  • β€’

    For any q:β„š, an element fq:A⁒(𝗋𝖺𝗍⁒(q)).

  • β€’

    For any Cauchy approximation x, and any a:∏(Ο΅:β„š+)A⁒(xΟ΅) such that

    βˆ€(Ξ΄,Ο΅:β„š+).(xΞ΄,aΞ΄)⌒δ+Ο΅(xΟ΅,aΟ΅), (11.3.1)

    an element fx,a:A⁒(𝗅𝗂𝗆⁒(x)). We call such a a dependent Cauchy approximation over x.

  • β€’

    For u,v:ℝ𝖼 such that h:βˆ€(Ο΅:β„š+).u∼ϡv, and all a:A⁒(u) and b:A⁒(v) such that βˆ€(Ο΅:β„š+).(u,a)⌒ϡ(v,b), a dependent path a=π–Ύπ—Šβ„π–Όβ’(u,v)Ab.

  • β€’

    For q,r:β„š and Ο΅:β„š+, if -Ο΅<q-r<Ο΅, we have (𝗋𝖺𝗍⁒(q),fq)⌒ϡ(𝗋𝖺𝗍⁒(r),fr).

  • β€’

    For q:β„š and Ξ΄,Ο΅:β„š+ and y a Cauchy approximation, and b a dependent Cauchy approximation over y, if 𝗋𝖺𝗍⁒(q)∼ϡ-Ξ΄yΞ΄, then

  • β€’

    Similarly, for r:β„š and Ξ΄,Ο΅:β„š+ and x a Cauchy approximation, and a a dependent Cauchy approximation over x, if xδ∼ϡ-δ𝗋𝖺𝗍⁒(r), then

  • β€’

    For Ο΅,Ξ΄,Ξ·:β„š+ and x,y Cauchy approximations, and a and b dependent Cauchy approximations over x and y respectively, if we have xδ∼ϡ-Ξ΄-Ξ·yΞ·, then

  • β€’

    For Ο΅:β„š+ and x,y:ℝ𝖼 and ΞΎ,ΞΆ:x∼ϡy, and a:A⁒(x) and b:A⁒(y), any two elements of (x,a)⌒ϡξ(y,b) and (x,a)⌒ϡ΢(y,b) are dependently equal over ΞΎ=ΞΆ. Note that as usual, this is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to asking that ⌒ takes values in mere propositions.

Under these hypotheses, we deduce functions

f :∏x:ℝ𝖼A⁒(x)
g :∏(x,y:ℝ𝖼)∏(Ο΅:β„š+)∏(ΞΎ:x∼ϡy)(x,f⁒(x))⌒ϡξ(y,f⁒(y))

which compute as expected:

f⁒(𝗋𝖺𝗍⁒(q)) :≑fq, (11.3.2)
f⁒(𝗅𝗂𝗆⁒(x)) :≑fx,(f,g)⁒[x]. (11.3.2)

Here (f,g)⁒[x] denotes the result of applying f and g to a Cauchy approximation x to obtain a dependent Cauchy approximation over x. That is, we define (f,g)[x]Ο΅:≑f(xΟ΅):A(xΟ΅), and then for any Ο΅,Ξ΄:β„š+ we have g⁒(xΟ΅,xΞ΄,Ο΅+Ξ΄,ΞΎ) to witness the fact that (f,g)⁒[x] is a dependent Cauchy approximation, where ΞΎ:xϡ∼ϡ+Ξ΄xΞ΄ arises from the assumptionPlanetmathPlanetmath that x is a Cauchy approximation.

We will never use this notation again, so don’t worry about remembering it. Generally we use the pattern-matching convention, where f is defined by equations such asΒ (11.3.2) andΒ (11.3.2) in which the right-hand side ofΒ (11.3.2) may involve the symbols f⁒(xΟ΅) and an assumption that they form a dependent Cauchy approximation.

However, this induction principle is admittedly still quite a mouthful. To help make sense of it, we observe that it contains as special cases two separate induction principles for ℝ𝖼 and for ∼. Firstly, suppose given only a type family A:ℝ𝖼→𝒰, and define ⌒ to be constant at 𝟏. Then much of the required data becomes trivial, and we are left with:

  • β€’

    for any q:β„š, an element fq:A⁒(𝗋𝖺𝗍⁒(q)),

  • β€’

    for any Cauchy approximation x, and any a:∏(Ο΅:β„š+)A⁒(xΟ΅), an element fx,a:A⁒(𝗅𝗂𝗆⁒(x)),

  • β€’

    for u,v:ℝ𝖼 and h:βˆ€(Ο΅:β„š+).u∼ϡv, and a:A⁒(u) and b:A⁒(v), we have a=π–Ύπ—Šβ„π–Όβ’(u,v)Ab.

Given these data, the induction principle yields a function f:∏(x:ℝ𝖼)A⁒(x) such that

f⁒(𝗋𝖺𝗍⁒(q)) :≑fq,
f⁒(𝗅𝗂𝗆⁒(x)) :≑fx,f⁒(x).

We call this principle ℝ𝖼-induction; it says essentially that if we take ∼ϡ as given, then ℝ𝖼 is inductively generated by its constructors.

In particular, if A is a mere property, the third hypothesisMathworldPlanetmath in ℝ𝖼-induction is trivial. Thus, we may prove mere properties of real numbers by simply proving them for rationals and for limits of Cauchy approximations. Here is an example.

Lemma 11.3.2.

For any u:Rc and ϡ:Q+, we have u∼ϡu.


Define A(u):β‰‘βˆ€(Ο΅:β„š+).(u∼ϡu). Since this is a mere proposition (by the last constructor of ∼), by ℝ𝖼-induction, it suffices to prove it when u is 𝗋𝖺𝗍⁒(q) and when u is 𝗅𝗂𝗆⁒(x). In the first case, we obviously have |q-q|<Ο΅ for any Ο΅, hence 𝗋𝖺𝗍⁒(q)βˆΌΟ΅π—‹π–Ίπ—β’(q) by the first constructor of ∼. And in the second case, we may assume inductively that xδ∼ϡxΞ΄ for all Ξ΄,Ο΅:β„š+. Then in particular, we have xΟ΅/3∼ϡ/3xΟ΅/3, whence 𝗅𝗂𝗆⁒(x)βˆΌΟ΅π—…π—‚π—†β’(x) by the fourth constructor of ∼. ∎

Theorem 11.3.3.

ℝ𝖼 is a set.


We have just shown that the mere relation P(u,v):β‰‘βˆ€(Ο΅:β„š+).(u∼ϡv) is reflexiveMathworldPlanetmathPlanetmath. Since it implies identity, by the path constructor of ℝ𝖼, the result follows from \autorefthm:h-set-refrel-in-paths-sets. ∎

We can also show that although ℝ𝖼 may not be a quotient of the set of Cauchy sequencesPlanetmathPlanetmath of rationals, it is nevertheless a quotient of the set of Cauchy sequences of reals. (Of course, this is not a valid definition of ℝ𝖼, but it is a useful property.) We define the type of Cauchy approximations to be


The second constructor of ℝ𝖼 gives a function 𝗅𝗂𝗆:π’žβ†’β„π–Ό.

Lemma 11.3.4.

Every real merely is a limit pointMathworldPlanetmathPlanetmath: βˆ€(u:Rc).βˆƒ(x:C).u=lim(x). In other words, lim:Cβ†’Rc is surjective.


By ℝ𝖼-induction, we may divide into cases on u. Of course, if u is a limit 𝗅𝗂𝗆⁒(x), the statement is trivial. So suppose u is a rational point 𝗋𝖺𝗍⁒(q); we claim u is equal to 𝗅𝗂𝗆(λϡ.𝗋𝖺𝗍(q)). By the path constructor of ℝ𝖼, it suffices to show 𝗋𝖺𝗍(q)βˆΌΟ΅π—…π—‚π—†(λϡ.𝗋𝖺𝗍(q)) for all Ο΅:β„š+. And by the second constructor of ∼, for this it suffices to find Ξ΄:β„š+ such that 𝗋𝖺𝗍⁒(q)∼ϡ-δ𝗋𝖺𝗍⁒(q). But by the first constructor of ∼, we may take any Ξ΄:β„š+ with Ξ΄<Ο΅. ∎

Lemma 11.3.5.

If A is a set and f:C→A respects coincidence of Cauchy approximations, in the sense that


then f factors uniquely through lim:C→Rc.


Since 𝗅𝗂𝗆 is surjective, by \autoreflem:images_are_coequalizers, ℝ𝖼 is the quotient of π’ž by the kernel pair of 𝗅𝗂𝗆. But this is exactly the statement of the lemma. ∎

For the second special case of the induction principle, suppose instead that we take A to be constant at 𝟏. In this case, ⌒ is simply an Ο΅-indexed family of relations on Ο΅-close pairs of real numbers, so we may write u⌒ϡv instead of (u,⋆)⌒ϡ(v,⋆). Then the required data reduces to the following, where q,r denote rational numbers, Ο΅,Ξ΄,Ξ· positive rational numbers, and x,y Cauchy approximations:

  • β€’

    if -Ο΅<q-r<Ο΅, then 𝗋𝖺𝗍⁒(q)βŒ’Ο΅π—‹π–Ίπ—β’(r),

  • β€’

    if 𝗋𝖺𝗍⁒(q)∼ϡ-Ξ΄yΞ΄ and 𝗋𝖺𝗍⁒(q)⌒ϡ-Ξ΄yΞ΄, then 𝗋𝖺𝗍⁒(q)βŒ’Ο΅π—…π—‚π—†β’(y),

  • β€’

    if xδ∼ϡ-δ𝗋𝖺𝗍⁒(r) and xδ⌒ϡ-δ𝗋𝖺𝗍⁒(r), then 𝗅𝗂𝗆⁒(y)βŒ’Ο΅π—‹π–Ίπ—β’(q),

  • β€’

    if xδ∼ϡ-Ξ΄-Ξ·yΞ· and xδ⌒ϡ-Ξ΄-Ξ·yΞ·, then 𝗅𝗂𝗆⁒(x)βŒ’Ο΅π—…π—‚π—†β’(y).

The resulting conclusionMathworldPlanetmath is βˆ€(u,v:ℝ𝖼).βˆ€(Ο΅:β„š+).(u∼ϡv)β†’(u⌒ϡv). We call this principle ∼-induction; it says essentially that if we take ℝ𝖼 as given, then ∼ϡ is inductively generated (as a family of types) by its constructors. For example, we can use this to show that ∼ is symmetric.

Lemma 11.3.6.

For any u,v:Rc and ϡ:Q+, we have (u∼ϡv)=(v∼ϡu).


Since both are mere propositions, by symmetry it suffices to show one implicationMathworldPlanetmath. Thus, let (u⌒ϡv):≑(v∼ϡu). By ∼-induction, we may reduce to the case that u∼ϡv is derived from one of the four interesting constructors of ∼. In the first case when u and v are both rational, the result is trivial (we can apply the first constructor again). In the other three cases, the inductive hypothesis (together with commutativity of additionPlanetmathPlanetmath in β„š) yields exactly the input to another of the constructors of ∼ (the second and third constructors switch, while the fourth stays put). ∎

The general induction principle, which we may call (ℝ𝖼,∼)-induction, is therefore a sort of joint ℝ𝖼-induction and ∼-induction. Consider, for instance, its non-dependent version, which we call (ℝ𝖼,∼)-recursion, which is the one that we will have the most use for. Ordinary ℝ𝖼-recursion tells us that to define a function f:ℝ𝖼→A it suffices to:

  1. 1.

    for every q:β„š construct f⁒(𝗋𝖺𝗍⁒(q)):A,

  2. 2.

    for every Cauchy approximation x:β„š+→ℝ𝖼, construct f⁒(x):A, assuming that f⁒(xΟ΅) has already been defined for all Ο΅:β„š+,

  3. 3.

    prove f⁒(u)=f⁒(v) for all u,v:ℝ𝖼 satisfying βˆ€(Ο΅:β„š+).u∼ϡv.

However, it is generally quite difficult to showΒ 3 without knowing something about how f acts on Ο΅-close Cauchy reals. The enhanced principle of (ℝ𝖼,∼)-recursion remedies this deficiency, allowing us to specify an arbitrary β€œway in which f acts on Ο΅-close Cauchy reals”, which we can then prove to be the case by a simultaneous induction with the definition of f. This is the family of relations ⌒. Since A is independent of ℝ𝖼, we may assume for simplicity that ⌒ depends only on A and β„š+, and thus there is no ambiguity in writing a⌒ϡb instead of (u,a)⌒ϡ(v,b). In this case, defining a function f:ℝ𝖼→A by (ℝ𝖼,∼)-recursion requires the following cases (which we now write using the pattern-matching convention).

  • β€’

    For every q:β„š, construct f⁒(𝗋𝖺𝗍⁒(q)):A.

  • β€’

    For every Cauchy approximation x:β„š+→ℝ𝖼, construct f⁒(x):A, assuming inductively that f⁒(xΟ΅) has already been defined for all Ο΅:β„š+ and form a β€œCauchy approximation with respect to βŒ’β€, i.e.Β that βˆ€(Ο΅,Ξ΄:β„š+).(f(xΟ΅)⌒ϡ+Ξ΄f(xΞ΄)).

  • β€’

    Prove that the relations ⌒ are separated, i.e.Β that, for any a,b:A, (βˆ€(Ο΅:β„š+).a⌒ϡb)β‡’(a=b).

  • β€’

    Prove that if -Ο΅<q-r<Ο΅ for q,r:β„š, then f⁒(𝗋𝖺𝗍⁒(q))⌒ϡf⁒(𝗋𝖺𝗍⁒(r)).

  • β€’

    For any q:β„š and any Cauchy approximation y, prove that f⁒(𝗋𝖺𝗍⁒(q))⌒ϡf⁒(𝗅𝗂𝗆⁒(y)), assuming inductively that 𝗋𝖺𝗍⁒(q)∼ϡ-Ξ΄yΞ΄ and f⁒(𝗋𝖺𝗍⁒(q))⌒ϡ-Ξ΄f⁒(yΞ΄) for some Ξ΄:β„š+, and that η↦f⁒(xΞ·) is a Cauchy approximation with respect to ⌒.

  • β€’

    For any Cauchy approximation x and any r:β„š, prove that f⁒(𝗅𝗂𝗆⁒(x))⌒ϡf⁒(𝗋𝖺𝗍⁒(r)), assuming inductively that xδ∼ϡ-δ𝗋𝖺𝗍⁒(r) and f⁒(xΞ΄)⌒ϡ-Ξ΄f⁒(𝗋𝖺𝗍⁒(r)) for some Ξ΄:β„š+, and that η↦f⁒(xΞ·) is a Cauchy approximation with respect to ⌒.

  • β€’

    For any Cauchy approximations x,y, prove that f⁒(𝗅𝗂𝗆⁒(x))⌒ϡf⁒(𝗅𝗂𝗆⁒(y)), assuming inductively that xδ∼ϡ-Ξ΄-Ξ·yΞ· and f⁒(xΞ΄)⌒ϡ-Ξ΄-Ξ·f⁒(yΞ·) for some Ξ΄,Ξ·:β„š+, and that θ↦f⁒(xΞΈ) and θ↦f⁒(yΞΈ) are Cauchy approximations with respect to ⌒.

Note that in the last four proofs, we are free to use the specific definitions of f⁒(𝗋𝖺𝗍⁒(q)) and f⁒(𝗅𝗂𝗆⁒(x)) given in the first two data. However, the proof of separatedness must apply to any two elements of A, without any relation to f: it is a sort of β€œadmissibility” condition on the family of relations ⌒. Thus, we often verify it first, immediately after defining ⌒, before going on to define f⁒(𝗋𝖺𝗍⁒(q)) and f⁒(𝗅𝗂𝗆⁒(x)).

Under the above hypotheses, (ℝ𝖼,∼)-recursion yields a function f:ℝ𝖼→A such that f⁒(𝗋𝖺𝗍⁒(q)) and f⁒(𝗅𝗂𝗆⁒(x)) are judgmentally equal to the definitions given for them in the first two clauses. Moreover, we may also conclude

βˆ€(u,v:ℝ𝖼).βˆ€(Ο΅:β„š+).(u∼ϡv)β†’(f(u)⌒ϡf(v)). (11.3.7)

As a paradigmatic example, (ℝ𝖼,∼)-recursion allows us to extend functions defined on β„š to all of ℝ𝖼, as long as they are sufficiently continuousMathworldPlanetmathPlanetmath.

Definition 11.3.8.

A function f:Q→Rc is LipschitzPlanetmathPlanetmath if there exists L:Q+ (the Lipschitz constant) such that


for all ϡ:Q+ and q,r:Q. Similarly, g:Rc→Rc is Lipschitz if there exists L:Q+ such that


for all Ο΅:Q+ and u,v:Rc..

In particular, note that by the first constructor of ∼, if f:β„šβ†’β„š is Lipschitz in the obvious sense, then so is the composite β„šβ†’π‘“β„šβ†’β„π–Ό.

Lemma 11.3.9.

Suppose f:Qβ†’Rc is Lipschitz with constant L:Q+. Then there exists a Lipschitz map fΒ―:Rcβ†’Rc, also with constant L, such that f¯⁒(rat⁒(q))≑f⁒(q) for all q:Q.


We define fΒ― by (ℝ𝖼,∼)-recursion, with codomain A:≑ℝ𝖼. We define the relation ⌒:β„π–Όβ†’β„π–Όβ†’β„š+β†’π–―π—‹π—ˆπ—‰ to be

(u⌒ϡv) :≑(u∼L⁒ϡv).

For q:β„š, we define


For a Cauchy approximation x:β„š+→ℝ𝖼, we define


For this to make sense, we must verify that y:≑λϡ.fΒ―(xΟ΅/L) is a Cauchy approximation. However, the inductive hypothesis for this step is that for any Ξ΄,Ο΅:β„š+ we have f¯⁒(xΞ΄)⌒δ+Ο΅f¯⁒(xΟ΅), i.e.Β f¯⁒(xΞ΄)∼L⁒δ+L⁒ϡf¯⁒(xΟ΅). Thus we have


For proving separatedness, we simply observe that βˆ€(Ο΅:β„š+).a⌒ϡb means βˆ€(Ο΅:β„š+).a∼L⁒ϡb, which implies βˆ€(Ο΅:β„š+).a∼ϡb and thus a=b.

To completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath the (ℝ𝖼,∼)-recursion, it remains to verify the four conditions on ⌒. This basically amounts to proving that fΒ― is Lipschitz for all the four constructors of ∼.

  1. 1.

    When u is 𝗋𝖺𝗍⁒(q) and v is 𝗋𝖺𝗍⁒(r) with -Ο΅<|q-r|<Ο΅, the assumption that f is Lipschitz yields f⁒(q)∼L⁒ϡf⁒(r), hence f¯⁒(𝗋𝖺𝗍⁒(q))⌒ϡf¯⁒(𝗋𝖺𝗍⁒(r)) by definition.

  2. 2.

    When u is 𝗅𝗂𝗆⁒(x) and v is 𝗋𝖺𝗍⁒(q) with xη∼ϡ-η𝗋𝖺𝗍⁒(q), then the inductive hypothesis is f¯⁒(xΞ·)∼L⁒ϡ-L⁒η𝗋𝖺𝗍⁒(f⁒(q)), which proves f¯⁒(𝗅𝗂𝗆⁒(x))∼L⁒ϡf¯⁒(𝗋𝖺𝗍⁒(q)) by the third constructor of ∼.

  3. 3.

    The symmetric case when u is rational and v is a limit is essentially identical.

  4. 4.

    When u is 𝗅𝗂𝗆⁒(x) and v is 𝗅𝗂𝗆⁒(y), with Ξ΄,Ξ·:β„š+ such that xδ∼ϡ-Ξ΄-Ξ·yΞ·, the inductive hypothesis is f¯⁒(xΞ΄)∼L⁒ϡ-L⁒δ-L⁒ηf¯⁒(yΞ·), which proves f¯⁒(𝗅𝗂𝗆⁒(x))∼L⁒ϡf¯⁒(𝗅𝗂𝗆⁒(y)) by the fourth constructor of ∼.

This completes the (ℝ𝖼,∼)-recursion, and hence the construction of fΒ―. The desired equality f¯⁒(𝗋𝖺𝗍⁒(q))≑f⁒(q) is exactly the first computation rule for (ℝ𝖼,∼)-recursion, and the additional conditionΒ (11.3.7) says exactly that fΒ― is Lipschitz with constant L. ∎

At this point we have gone about as far as we can without a better characterizationMathworldPlanetmath of ∼. We have specified, in the constructors of ∼, the conditions under which we want Cauchy reals of the two different forms to be Ο΅-close. However, how do we know that in the resulting inductive-inductive type family, these are the only witnesses to this fact? We have seen that inductive type families (such as identity types, see \autorefsec:identity-systems) and higher inductive types have a tendency to contain β€œmore than was put into them”, so this is not an idle question.

In order to characterize ∼ more precisely, we will define a family of relations β‰ˆΟ΅ on ℝ𝖼 recursively, so that they will compute on constructors, and prove that this family is equivalent to ∼ϡ.

Theorem 11.3.10.

There is a family of mere relations β‰ˆ:Rcβ†’Rcβ†’Q+β†’Prop such that

(𝗋𝖺𝗍⁒(q)β‰ˆΟ΅π—‹π–Ίπ—β’(r)) :≑(-Ο΅<q-r<Ο΅) (11.3.10)
(𝗋𝖺𝗍⁒(q)β‰ˆΟ΅π—…π—‚π—†β’(y)) :β‰‘βˆƒ(Ξ΄:β„š+).𝗋𝖺𝗍(q)β‰ˆΟ΅-Ξ΄yΞ΄ (11.3.10)
(𝗅𝗂𝗆⁒(x)β‰ˆΟ΅π—‹π–Ίπ—β’(r)) :β‰‘βˆƒ(Ξ΄:β„š+).xΞ΄β‰ˆΟ΅-δ𝗋𝖺𝗍(r) (11.3.10)
(𝗅𝗂𝗆⁒(x)β‰ˆΟ΅π—…π—‚π—†β’(y)) :β‰‘βˆƒ(Ξ΄,Ξ·:β„š+).xΞ΄β‰ˆΟ΅-Ξ΄-Ξ·yΞ·. (11.3.10)

Moreover, we have

(uβ‰ˆΟ΅v)β‡”βˆƒ(ΞΈ:β„š+).(uβ‰ˆΟ΅-ΞΈv) (11.3.10)
(uβ‰ˆΟ΅v)β†’(v∼δw)β†’(uβ‰ˆΟ΅+Ξ΄w) (11.3.10)
(u∼ϡv)β†’(vβ‰ˆΞ΄w)β†’(uβ‰ˆΟ΅+Ξ΄w). (11.3.10)

The additional conditionsΒ (11.3.10)–(11.3.10) turn out to be required in order to make the inductive definition go through. ConditionΒ (11.3.10) is called being rounded. Reading it from right to left gives monotonicity of β‰ˆ,


while reading it left to right to openness of β‰ˆ,


ConditionsΒ (11.3.10) andΒ (11.3.10) are forms of the triangle inequalityMathworldMathworldPlanetmath, which say that β‰ˆ is a β€œmodule” over ∼ on both sides.


We will define β‰ˆ:β„π–Όβ†’β„π–Όβ†’β„š+β†’π–―π—‹π—ˆπ—‰ by double (ℝ𝖼,∼)-recursion. First we will apply (ℝ𝖼,∼)-recursion with codomain the subset of β„π–Όβ†’β„š+β†’π–―π—‹π—ˆπ—‰ consisting of those families of predicatesMathworldPlanetmath which are rounded and satisfy the one appropriate form of the triangle inequality. Thinking of these predicates as half of a binary relation, we will write them as (u,Ο΅)↦(β™’β‰ˆΟ΅u), with the symbol β™’ referring to the whole relation. Now we can write A precisely as


As usual with subsets, we will use the same notation for an inhabitant of A and its first component β™’. As the family of relations required for (ℝ𝖼,∼)-recursion, we consider the following, which will ensure the other form of the triangle inequality:


We observe that these relations are separated. For assuming βˆ€(Ο΅:β„š+).(β™’βŒ’Ο΅β™‘), to show β™’=β™‘ it suffices to show (β™’β‰ˆΟ΅u)⇔(β™‘β‰ˆΟ΅u) for all u:ℝ𝖼. But β™’β‰ˆΟ΅u implies β™’β‰ˆΟ΅-ΞΈu for some ΞΈ, by roundedness, which together with β™’βŒ’Ο΅β™‘ implies β™‘β‰ˆΟ΅u; and the converseMathworldPlanetmath is identical.

Now the first two data the recursion principle requires are the following.

  • β€’

    For any q:β„š, we must give an element of A, which we denote (𝗋𝖺𝗍⁒(q)β‰ˆ(–)–).

  • β€’

    For any Cauchy approximation x, if we assume defined a function β„š+β†’A, which we will denote by ϡ↦(xΟ΅β‰ˆ(–)–), with the property that

    βˆ€(u:ℝ𝖼).βˆ€(Ξ΄,Ο΅,Ξ·:β„š+).(xΞ΄β‰ˆΞ·u)β†’(xΟ΅β‰ˆΞ·+Ξ΄+Ο΅u), (11.3.11)

    we must give an element of A, which we write as (𝗅𝗂𝗆⁒(x)β‰ˆ(–)–).

In both cases, we give the required definition by using a nested (ℝ𝖼,∼)-recursion, with codomain the subset of β„š+β†’π–―π—‹π—ˆπ—‰ consisting of rounded families of mere propositions. Thinking of these propositionsPlanetmathPlanetmathPlanetmath as zero halves of a binary relation, we will write them as ϡ↦(βˆ™β‰ˆΟ΅β–³), with the symbol β–³ referring to the whole family. Now we can write the codomain of these inner recursions precisely as


We take the required family of relations to be the remnant of the triangle inequality:


These relations are separated by the same argumentMathworldPlanetmath as for ⌒, using roundedness of all elements of C.

Note that if such an inner recursion succeeds, it will yield a family of predicates β™’:β„π–Όβ†’β„š+β†’π–―π—‹π—ˆπ—‰ which are rounded (since their image in β„š+β†’π–―π—‹π—ˆπ—‰ lies in C) and satisfy


Expanding out the definition of ⌣, this yields precisely the third condition for β™’ to belong to A; thus it is exactly what we need.

It is at this point that we can give the definitionsΒ (11.3.10)–(11.3.10), as the first two clauses of each of the two inner recursions, corresponding to rational points and limits. In each case, we must verify that the relation is rounded and hence lies in C. In the rational-rational caseΒ (11.3.10) this is clear, while in the other cases it follows from an inductive hypothesis. (InΒ (11.3.10) the relevant inductive hypothesis is that (𝗋𝖺𝗍(q)β‰ˆ(–)yΞ΄):C, while inΒ (11.3.10) andΒ (11.3.10) it is that (xΞ΄β‰ˆ(–)–):A.)

The remaining data of the sub-recursions consist of showing that (11.3.10)–(11.3.10) satisfy the triangle inequality on the right with respect to the constructors of ∼. There are eight cases β€” four in each sub-recursion β€” corresponding to the eight possible ways that u, v, and w inΒ (11.3.10) can be chosen to be rational points or limits. First we consider the cases when u is 𝗋𝖺𝗍⁒(q).

  1. 1.

    Assuming 𝗋𝖺𝗍⁒(q)β‰ˆΟ•π—‹π–Ίπ—β’(r) and -Ο΅<|r-s|<Ο΅, we must show 𝗋𝖺𝗍⁒(q)β‰ˆΟ•+ϡ𝗋𝖺𝗍⁒(s). But by definition of β‰ˆ, this reduces to the triangle inequality for rational numbers.

  2. 2.

    We assume Ο•,Ο΅,Ξ΄:β„š+ such that 𝗋𝖺𝗍⁒(q)β‰ˆΟ•π—‹π–Ίπ—β’(r) and 𝗋𝖺𝗍⁒(r)∼ϡ-Ξ΄yΞ΄, and inductively that

    βˆ€(ψ:β„š+).(𝗋𝖺𝗍(q)β‰ˆΟˆπ—‹π–Ίπ—(r))β†’(𝗋𝖺𝗍(q)β‰ˆΟˆ+Ο΅-Ξ΄yΞ΄). (11.3.12)

    We assume also that ψ,δ↦(𝗋𝖺𝗍(q)β‰ˆΟˆyΞ΄) is a Cauchy approximation with respect to ⌣, i.e.

    βˆ€(ψ,ΞΎ,ΞΆ:β„š+).(𝗋𝖺𝗍(q)β‰ˆΟˆyΞΎ)β†’(𝗋𝖺𝗍(q)β‰ˆΟˆ+ΞΎ+ΞΆyΞΆ), (11.3.13)

    although we do not need this assumption in this case. Indeed, (11.3.12) with ψ:≑ϕ yields immediately 𝗋𝖺𝗍⁒(q)β‰ˆΟ•+Ο΅-Ξ΄yΞ΄, and hence 𝗋𝖺𝗍⁒(q)β‰ˆΟ•+ϡ𝗅𝗂𝗆⁒(y) by definition of β‰ˆ.

  3. 3.

    We assume Ο•,Ο΅,Ξ΄:β„š+ such that 𝗋𝖺𝗍⁒(q)β‰ˆΟ•π—…π—‚π—†β’(y) and yδ∼ϡ-δ𝗋𝖺𝗍⁒(r), and inductively that

    βˆ€(ψ:β„š+).(𝗋𝖺𝗍(q)β‰ˆΟˆyΞ΄)β†’(𝗋𝖺𝗍(q)β‰ˆΟˆ+Ο΅-δ𝗋𝖺𝗍(r)). (11.3.14)
    βˆ€(ψ,ΞΎ,ΞΆ:β„š+).(𝗋𝖺𝗍(q)β‰ˆΟˆyΞΎ)β†’(𝗋𝖺𝗍(q)β‰ˆΟˆ+ΞΎ+ΞΆyΞΆ). (11.3.14)

    By definition, 𝗋𝖺𝗍⁒(q)β‰ˆΟ•π—…π—‚π—†β’(y) means that we have ΞΈ:β„š+ with 𝗋𝖺𝗍⁒(q)β‰ˆΟ•-ΞΈyΞΈ. By assumptionΒ (11.3.14), therefore, we have also 𝗋𝖺𝗍⁒(q)β‰ˆΟ•+Ξ΄yΞ΄, and then byΒ (11.3.14) it follows that 𝗋𝖺𝗍⁒(q)β‰ˆΟ•+ϡ𝗋𝖺𝗍⁒(r), as desired.

  4. 4.

    We assume Ο•,Ο΅,Ξ΄,Ξ·:β„š+ such that 𝗋𝖺𝗍⁒(q)β‰ˆΟ•π—…π—‚π—†β’(y) and yδ∼ϡ-Ξ΄-Ξ·zΞ·, and inductively that

    βˆ€(ψ:β„š+).(𝗋𝖺𝗍(q)β‰ˆΟˆyΞ΄)β†’(𝗋𝖺𝗍(q)β‰ˆΟˆ+Ο΅-Ξ΄-Ξ·zΞ·), (11.3.14)
    βˆ€(ψ,ΞΎ,ΞΆ:β„š+).(𝗋𝖺𝗍(q)β‰ˆΟˆyΞΎ)β†’(𝗋𝖺𝗍(q)β‰ˆΟˆ+ΞΎ+ΞΆyΞΆ), (11.3.14)
    βˆ€(ψ,ΞΎ,ΞΆ:β„š+).(𝗋𝖺𝗍(q)β‰ˆΟˆzΞΎ)β†’(𝗋𝖺𝗍(q)β‰ˆΟˆ+ΞΎ+ΞΆzΞΆ). (11.3.14)

    Again, 𝗋𝖺𝗍⁒(q)β‰ˆΟ•π—…π—‚π—†β’(y) means we have ΞΎ:β„š+ with 𝗋𝖺𝗍⁒(q)β‰ˆΟ•-ΞΎyΞΎ, whileΒ (11.3.14) then implies 𝗋𝖺𝗍⁒(q)β‰ˆΟ•+Ξ΄yΞ΄ andΒ (11.3.14) implies 𝗋𝖺𝗍⁒(q)β‰ˆΟ•+Ο΅-Ξ·zΞ·. But by definition of β‰ˆ, this implies 𝗋𝖺𝗍⁒(q)β‰ˆΟ•+ϡ𝗅𝗂𝗆⁒(z) as desired.

Now we move on to the cases when u is 𝗅𝗂𝗆⁒(x), with x a Cauchy approximation. In this case, the ambient inductive hypothesis of the definition of (𝗅𝗂𝗆(x)β‰ˆ(–)–):A is that we have (xΞ΄β‰ˆ(–)–):A, so that in addition to being rounded they satisfy the triangle inequality on the right.

  1. 5.

    Assuming 𝗅𝗂𝗆⁒(x)β‰ˆΟ•π—‹π–Ίπ—β’(r) and -Ο΅<|r-s|<Ο΅, we must show 𝗅𝗂𝗆⁒(x)β‰ˆΟ•+ϡ𝗋𝖺𝗍⁒(s). By definition of β‰ˆ, the former means xΞ΄β‰ˆΟ•-δ𝗋𝖺𝗍⁒(r), so that above triangle inequality implies xΞ΄β‰ˆΟ΅+Ο•-δ𝗋𝖺𝗍⁒(s), hence 𝗅𝗂𝗆⁒(x)β‰ˆΟ•+ϡ𝗋𝖺𝗍⁒(s) as desired.

  2. 6.

    We assume Ο•,Ο΅,Ξ΄:β„š+ such that 𝗅𝗂𝗆⁒(x)β‰ˆΟ•π—‹π–Ίπ—β’(r) and 𝗋𝖺𝗍⁒(r)∼ϡ-Ξ΄yΞ΄, and two unneeded inductive hypotheses. By definition, we have Ξ·:β„š+ such that xΞ·β‰ˆΟ•-η𝗋𝖺𝗍⁒(r), so the inductive triangle inequality gives xΞ·β‰ˆΟ•+Ο΅-Ξ·-Ξ΄yΞ΄. The definition of β‰ˆ then immediately yields 𝗅𝗂𝗆⁒(x)β‰ˆΟ•+ϡ𝗅𝗂𝗆⁒(y).

  3. 7.

    We assume Ο•,Ο΅,Ξ΄:β„š+ such that 𝗅𝗂𝗆⁒(x)β‰ˆΟ•π—…π—‚π—†β’(y) and yδ∼ϡ-δ𝗋𝖺𝗍⁒(r), and two unneeded inductive hypotheses. By definition we have ΞΎ,ΞΈ:β„š+ such that xΞΎβ‰ˆΟ•-ΞΎ-ΞΈyΞΈ. Since y is a Cauchy approximation, we have yθ∼θ+Ξ΄yΞ΄, so the inductive triangle inequality gives xΞΎβ‰ˆΟ•+Ξ΄-ΞΎyΞ΄ and then xΞΎβˆΌΟ•+Ο΅-ξ𝗋𝖺𝗍⁒(r). The definition of β‰ˆ then gives 𝗅𝗂𝗆⁒(x)β‰ˆΟ•+ϡ𝗋𝖺𝗍⁒(r), as desired.

  4. 8.

    Finally, we assume Ο•,Ο΅,Ξ΄,Ξ·:β„š+ such that 𝗅𝗂𝗆⁒(x)β‰ˆΟ•π—…π—‚π—†β’(y) and yδ∼ϡ-Ξ΄-Ξ·zΞ·. Then as before we have ΞΎ,ΞΈ:β„š+ with xΞΎβ‰ˆΟ•-ΞΎ-ΞΈyΞΈ, and two applications of the triangle inequality suffices as before.

This completes the two inner recursions, and thus the definitions of the families of relations (𝗋𝖺𝗍⁒(q)β‰ˆ(–)–) and (𝗅𝗂𝗆⁒(x)β‰ˆ(–)–). Since all are elements of A, they are rounded and satisfy the triangle inequality on the right with respect to ∼. What remains is to verify the conditions relating to ⌒, which is to say that these relations satisfy the triangle inequality on the left with respect to the constructors of ∼. The four cases correspond to the four choices of rational or limit points for u and v inΒ (11.3.10), and since they are all mere propositions, we may apply ℝ𝖼-induction and assume that w is also either rational or a limit. This yields another eight cases, whose proofs are essentially identical to those just given; so we will not subject the reader to them. ∎

We can now prove:

Theorem 11.3.14.

For any u,v:Rc and Ο΅:Q+ we have (u∼ϡv)=(uβ‰ˆΟ΅v).


Since both are mere propositions, it suffices to prove bidirectional implication. For the left-to-right direction, we use ∼-induction applied to C(u,v,Ο΅):≑(uβ‰ˆΟ΅v). Thus, it suffices to consider the four constructors of ∼. In each case, u and v are specialized to either rational points or limits, so that the definition of β‰ˆ evaluates, and the inductive hypothesis always applies.

For the right-to-left direction, we use ℝ𝖼-induction to assume that u and v are rational points or limits, allowing β‰ˆ to evaluate. But now the definitions of β‰ˆ, and the inductive hypotheses, supply exactly the data required for the relevant constructors of ∼. ∎

Stretching a point, one might call β‰ˆ a fibrationMathworldPlanetmath of β€œcodes” for ∼, with the two directions of the above proof being π–Ύπ—‡π–Όπ—ˆπ–½π–Ύ and π–½π–Ύπ–Όπ—ˆπ–½π–Ύ respectively. By the definition of β‰ˆ, from \autorefthm:RC-sim-characterization we get equivalences

(𝗋𝖺𝗍⁒(q)βˆΌΟ΅π—‹π–Ίπ—β’(r)) =(-Ο΅<q-r<Ο΅)
(𝗋𝖺𝗍⁒(q)βˆΌΟ΅π—…π—‚π—†β’(y)) =βˆƒ(Ξ΄:β„š+).𝗋𝖺𝗍(q)∼ϡ-Ξ΄yΞ΄
(𝗅𝗂𝗆⁒(x)βˆΌΟ΅π—‹π–Ίπ—β’(r)) =βˆƒ(Ξ΄:β„š+).xδ∼ϡ-δ𝗋𝖺𝗍(r)
(𝗅𝗂𝗆⁒(x)βˆΌΟ΅π—…π—‚π—†β’(y)) =βˆƒ(Ξ΄,Ξ·:β„š+).xδ∼ϡ-Ξ΄-Ξ·yΞ·.

Our proof also provides the following additional information.

Corollary 11.3.15.

∼ is rounded and satisfies the triangle inequality:

(u∼ϡv)β‰ƒβˆƒ(ΞΈ:β„š+).u∼ϡ-ΞΈv (11.3.15)
(u∼ϡv)β†’(v∼δw)β†’(u∼ϡ+Ξ΄w). (11.3.15)

With the triangle inequality in hand, we can show that β€œlimits” of Cauchy approximations actually behave like limits.

Lemma 11.3.16.

For any u:Rc, Cauchy approximation y, and ϡ,δ:Q+, if u∼ϡyδ then u∼ϡ+δlim⁒(y).


We use ℝ𝖼-induction on u. If u is 𝗋𝖺𝗍⁒(q), then this is exactly the second constructor of ∼. Now suppose u is 𝗅𝗂𝗆⁒(x), and that each xΞ· has the property that for any y,Ο΅,Ξ΄, if xη∼ϡyΞ΄ then xη∼ϡ+δ𝗅𝗂𝗆⁒(y). In particular, taking y:≑x and Ξ΄:≑η in this assumption, we conclude that xη∼η+θ𝗅𝗂𝗆⁒(x) for any Ξ·,ΞΈ:β„š+.

Now let y,Ο΅,Ξ΄ be arbitrary and assume 𝗅𝗂𝗆⁒(x)∼ϡyΞ΄. By roundedness, there is a ΞΈ such that 𝗅𝗂𝗆⁒(x)∼ϡ-ΞΈyΞ΄. Then by the above observation, for any Ξ· we have xη∼η+ΞΈ/2𝗅𝗂𝗆⁒(x), and hence xη∼ϡ+Ξ·-ΞΈ/2yΞ΄ by the triangle inequality. Hence, the fourth constructor of ∼ yields 𝗅𝗂𝗆⁒(x)∼ϡ+2⁒η+Ξ΄-ΞΈ/2𝗅𝗂𝗆⁒(y). Thus, if we choose Ξ·:≑θ/4, the result follows. ∎

Lemma 11.3.17.

For any Cauchy approximation y and any δ,η:Q+ we have yδ∼δ+ηlim⁒(y).


Take u:≑yΞ΄ and Ο΅:≑η in the previous lemma. ∎

Remark 11.3.18.

We might have expected to have yδ∼δlim⁒(y), but this fails in examples. For instance, consider x defined by xΟ΅:≑ϡ. Its limit is clearly 0, but we do not have |Ο΅-0|<Ο΅, only ≀.

As an application, \autorefthm:RC-sim-lim-term enables us to show that the extensionsPlanetmathPlanetmath of Lipschitz functions from \autorefRC-extend-Q-Lipschitz are unique.

Lemma 11.3.19.

Let f,g:Rc→Rc be continuous, in the sense that


and analogously for g. If f⁒(rat⁒(q))=g⁒(rat⁒(q)) for all q:Q, then f=g.


We prove f⁒(u)=g⁒(u) for all u by ℝ𝖼-induction. The rational case is just the hypothesis. Thus, suppose f⁒(xΞ΄)=g⁒(xΞ΄) for all Ξ΄. We will show that f⁒(𝗅𝗂𝗆⁒(x))∼ϡg⁒(𝗅𝗂𝗆⁒(x)) for all Ο΅, so that the path constructor of ℝ𝖼 applies.

Since f and g are continuous, there exist ΞΈ,Ξ· such that for all v, we have

(𝗅𝗂𝗆⁒(x)∼θv) β†’(f(𝗅𝗂𝗆(x))∼ϡ/2f(v))
(𝗅𝗂𝗆⁒(x)∼ηv) β†’(g(𝗅𝗂𝗆(x))∼ϡ/2g(v)).

Choosing Ξ΄<min⁑(ΞΈ,Ξ·), by \autorefthm:RC-sim-lim-term we have both 𝗅𝗂𝗆⁒(x)∼θyΞ΄ and 𝗅𝗂𝗆⁒(x)∼ηyΞ΄. Hence


and thus f⁒(𝗅𝗂𝗆⁒(x))∼ϡg⁒(𝗅𝗂𝗆⁒(x)) by the triangle inequality. ∎

Title 11.3.2 Induction and recursion on Cauchy reals