Does CZF prove there is a minimal cauchy completion of the rationals?

Question

In IZF, we can easily prove there is a minimal cauchy complete field extending the rationals: the dedekind reals are cauchy complete, so just intersect all of its cauchy complete subfields.

CZF can still prove that there are dedekind reals, and that they are cauchy complete, but intersecting all of its cauchy complete subfields is impredicative (i.e. CZF doesn't have the powerset axiom). Also keep in mind that, without countable choice, you can't prove the cauchy reals are cauchy complete (but if they were they'd be minimal).

So, can CZF prove that there is a minimal extension of the rationals that is cauchy complete?

---

Another approach I thought of is taking the set of dedekind reals that can be formed using a well founded tree of cauchy sequences whose leaves are rational numbers. But I'm pretty sure the property of being a well founded tree has unbounded quantifiers, so we can't form a subset using it.

A set that I think is minimal is if we take the set of trees as above, but instead of requiring it to be well founded, we just require that the values at the nodes are determined by the leaves (i.e. for every other tree that has the same structure and leaves, it will also have the same internal nodes). But I couldn't figure out how to prove that this gives the minimal subfield we are looking for.

Answer 1

You can prove this from the regular extension axiom $\mathbf{REA}$ using the general theory of inductive definitions. See e.g. Theorem 5.11 in Aczel & Rathjen, Notes on Constructive Set Theory. I suspect that $\mathbf{REA}$ is strictly necessary, although I don't think anyone has proved that specifically. A relevant paper on this kind of thing is Curi & Rathjen, Formal Baire Space in Constructive Set Theory.

$\mathbf{REA}$ is usually seen as a safe axiom to assume if you need it for something. It isn't strictly predicative, but sits proof theoretically at the same level as inductive types regularly used in type theory. It's sometimes referred to as "semi-predicative."