On the Cauchy Completeness of the Constructive Cauchy Reals

TL;DR

This paper explores the limitations of the constructive Cauchy reals, demonstrating that under certain set-theoretic assumptions, they may not be Cauchy complete, and related convergence properties can fail.

Contribution

It shows, within constructive set theory without Countable Choice, that the Cauchy reals may lack completeness and certain convergence properties can fail.

Findings

Cauchy reals may not be Cauchy complete in constructive set theory

A Cauchy sequence of rationals may lack a modulus of convergence

A Cauchy sequence of Cauchy sequences may not converge to a Cauchy sequence

Abstract

It is consistent with constructive set theory (without Countable Choice, clearly) that the Cauchy reals (equivalence classes of Cauchy sequences of rationals) are not Cauchy complete. Related results are also shown, such as that a Cauchy sequence of rationals may not have a modulus of convergence, and that a Cauchy sequence of Cauchy sequences may not converge to a Cauchy sequence, among others.