3
$\begingroup$

I don't think a particular choice of such type theory matters much. Extensional MLTT, SetoidTT, OTT, HoTT, HOTT, CuTT -- they all support quotient types. Reals is supposed to be a Set (in HoTT terminology) so in all "higher" type-theories we just add in truncations to the HIT signature representing Reals to collapse the higher structure.

So what's the general well-established state-of-the-art here, if there is one, in a constructive setting?

$\endgroup$
6
  • $\begingroup$ "State of the art" refers to the highest level of development. What is the notion of "high" in your question? Is Dedekind reals at a higher level of development than Cauchy reals or the other way round? $\endgroup$
    – Trebor
    May 20, 2023 at 7:49
  • $\begingroup$ I've heard there are some unexpected (for me at least) results concerning different encodings of Reals. E.g. Dedekind reals are not isomorphic to Cauchy reals in a constructive setting. That said it actually means there are many "Reals", not one, as we are used to think in classical math. $\endgroup$
    – Russoul
    May 20, 2023 at 15:42
  • $\begingroup$ Maybe this "issue" can be somehow resolved. Or maybe there is a different encoding I should use. How do I choose? What construction of Reals is the Reals? So I'd say "state of the art" here should mean "what's the current status of Reals in constructive type theories". $\endgroup$
    – Russoul
    May 20, 2023 at 15:43
  • $\begingroup$ In what sense does extensional MLTT support quotients? $\endgroup$ May 20, 2023 at 21:13
  • $\begingroup$ I do not understand this question. At last for me, it would help if you explained your motivation for asking the question, as well as what it is that you intend to do, once you've got reals in a proof assistant. $\endgroup$ May 20, 2023 at 21:21

2 Answers 2

2
$\begingroup$

Here are some formalizations of constructive reals that you can build on, roughly by decreasing level of "state-of-the-art". Some come equipped with a considerable amount of real analysis, which you can then help improve (rather than formalize everything from scratch):

  1. Good old C-CoRN, a large Coq library of reals, algebra and analysis, based on setoids.
  2. If you follow the work of Assia Mahboubi, Cyril Cohen and their coworkers, for example Formally Verified Approximations of Definite Integral and Formalization Techniques for Asymptotic Reasoning in Classical Analysis, you will find how world-experts approach formalization of analysis. (Do not dismiss some of this work just because it says it's "classical". Their approach is equally useful for constructive analysis.)
  3. UniMath has a section on Dedekind reals which goes some way. It flirts with excluded middle but stops short of going to bed with it.
  4. dedekind-reals, a construction of Dedekind reals in Coq with proof that they form an ordered Dedekind-complete archimedean field, and a lattice.
  5. Agda standard library has a definition of Cauchy reals but nothing about their structure (as far as I can tell).
  6. agda-unimath has a definition of Dedekind cuts but not much more than that.

In addition to consulting formalizatins of reals, one should also consult constructive literature. Not all constructive approaches are equally suited for formalization. For instance, Bishop's definition of Cauchy reals (which can be found in Agda's standard library) is not that practical. In general, abstract approaches tend to formalize well – this is a general feature of formalized mathematics.

$\endgroup$
9
  • $\begingroup$ I am confused about the following: some formalisations here define "Reals" as Cauchy(ℚ)/≈. E.g. the Bishops "Constructive mathematics" uses that definition. But without axiom of countable choice those "Reals" are not Cauchy-complete. So are they worthy of their name? What kind of constructive mathematics can one develop without completeness? What kind of constructive mathematics one cannot develop without completeness? $\endgroup$
    – Russoul
    May 21, 2023 at 17:13
  • $\begingroup$ If you use setoids in place of quotients you will get Cauchy-complete reals (see this gist for a proof that in setoids countable choice holds). The C-CoRN library does so. The definition in Agda standard library is just a stub that someone stuck in without considering what will happen when you actually try to use the definition. The others use Dedekind reals. $\endgroup$ May 21, 2023 at 17:51
  • $\begingroup$ Does it mean that Cauchy(ℚ)/≈ is Cauchy-complete in SetoidTT/OTT? And that SetoidTT/OTT has countable choice? $\endgroup$
    – Russoul
    May 21, 2023 at 19:33
  • $\begingroup$ Yes on both counts (In my comment above II explicitly stated that setoids has countable choice and pointed you to a formalization of this fact). MLTT has countable choice too – it has all choice. $\endgroup$ May 22, 2023 at 12:16
  • $\begingroup$ I am even more confused now. So in type theory we have two statements of choice. One which is "type-theoretic" and is a theorem in MLTT, SetoidTT, HoTT, etc. Another is "set-theoretic" and is not provable in MLTT nor SetoidTT nor HoTT. The latter one involves prop. truncation. I thought the choice (countable version thereof) needed to prove Cauchy-completeness of Cauchy(ℚ)/≈ is the "set-theoretic" one. But your gist seems to prove countable "type-theoretic" choice. I don't see the connection. $\endgroup$
    – Russoul
    May 23, 2023 at 18:18
2
$\begingroup$

First off, you need to distinguish between constructing the reals and defining the reals. Your question asks about the former, but:

  • Classically we almost never simply construct two versions of reals and then prove they are isomorphic. What we do is we prove that our definition of reals already implies that reals are unique, up to (unique) isomorphism. So encodings don't matter that much, it is the definitions that matter.
  • Constructing the reals is also a form of defining the reals, because you can always define "it is the reals iff it is isomorphic to this one I've just constructed". So the former is totally encapsulated in the latter, and we can just talk about the latter instead.

Now, we have a slick definition of what counts as a definition of the real numbers. We start with a neutral foundation, i.e. one that cannot prove or disprove the excluded middle. If a definition is equivalent to the classical reals once the excluded middle is added as an axiom, then we say this defines a notion of constructive reals. Note that adding axioms only collapses different notions of reals into one, never bifurcates them.

We immediately see that there are infinitely many versions of real numbers. This is because there are infinitely many propositions $p_i$ that are true in classical mathematics, but pairwise unprovable to be equivalent. So take the definition "A type/set is the reals if and only if $p_i$ holds and [insert the rest of the real axioms]", and you get an infinite supply of reals.

For the concrete discussion, I have nothing to add to the nLab entry.

There is one more thing I would like to point out in your question. It is not true that higher inductive types have nothing to contribute in the construction of reals, even when there are quotient types. In fact, the HoTT book gave a construction (referred to as the "HoTT reals") that is not a simple set quotient. If you insist on describing it with quotients, then consider the rationals $R_0 = \mathbb Q$, consider all the Cauchy sequences, and quotient it by an equivalence, giving $R_1 = \mathrm{Cauchy}(R_0)/\approx_0$. Now this is not Cauchy complete unless you assume some choice. So you complete it again, giving $R_2 = \mathrm{Cauchy}(R_1)/\approx_1$, and so on, giving $R_\omega = \bigcup_{k=0}^{\infty} R_k$. This is still not complete unless you assume some choice. So you do it again getting $R_{\omega+1}, R_{\omega+2}, \dots, R_{2\omega}, \dots$ Giving an infinitely ordinal-indexed tower of candidates reals. The HoTT reals just does all this in a single step: it is a higher inductive-inductive type, or quotient inductive-inductive type, which satisfies desirable properties even in the absence of countable choice.

$\endgroup$
9
  • 1
    $\begingroup$ How precisely does existence of infinitely many pairwise inequivalent propositions entail that there are infinitely many versions of the reals? You cannot just take any old set and call it "reals". it is assumed here that "reals" must form at the very least a ring, more likely a field, that there should be an order, and they should be complete (for a suitable notion of completeness). $\endgroup$ May 20, 2023 at 21:18
  • $\begingroup$ What I am saying is that the reals must satisfy certain axioms, or else they do not deserve to be called reals. If you make them contingent on some proposition $P$ then you will not be able to show that the axioms hold. $\endgroup$ May 20, 2023 at 21:44
  • $\begingroup$ @AndrejBauer I already made a definition of what counts as the reals in the answer, and it is admittedly very generous. Also, how should one define "a suitable notion of completeness"? If it is too defined as "equivalent to a classical notion given LEM", then the same trick applies, just use the notion "it is complete iff $p_n$ holds implies [insert completeness definition]". Of course one can put more stringent criteria on these if one likes, and there are likely only finitely many families of reals that are interesting, and I completely agree with that. $\endgroup$
    – Trebor
    May 21, 2023 at 4:04
  • $\begingroup$ Commonly considered are three notions of completeness: Cauchy, Dedekind and MacNeille. One can generalize some of these, for instance the Dedekind completeness can be stated relative to a dominance (the usual Dedekind completeness takes Prop as the dominance), see Davorin Lešnik's PhD thesis for background and plenty of material. Excluded middle is not a notion of completeness of reals. $\endgroup$ May 21, 2023 at 9:43
  • $\begingroup$ To be specific, suppose $P$ is something like de Morgan's Law $\forall p, q \in \Omega . \neg (p \lor q) = \neg p \land \neg q$. If you change your axioms $A_1, \ldots, A_n$ of reals to $P \Rightarrow A_1, \ldots, P \Rightarrow A_n$ you cannot even show that the "$P$-reals" form a ring. I do not see how this can be of any value, nor in what sense we have got "reals". You've just gone in the wrong direction. $\endgroup$ May 21, 2023 at 9:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.