Equality not decidable on the real numbers about dedekind-reals

[andrejbauer]

The files are in whatever state they were left by my students when they attempted to formalize the reals. They did not have a good understanding of the role of excluded middle and they naturally assumed it in several places. I would be very happy if anyone cleaned it up.

As for Cauchy-completeness: yes, the Dedekind reals are Cauchy complete, and the proof of this has nothing to do with what form the locatedness axiom takes. Given a Cauchy sequence, we can simply define its limit in terms of a cut. Recent work of @abooij shows that putting locateness into Type (with a sum) gets us precisely the Cauchy reals, instead of the Dedekind reals, at least in the context of homotopy type theory.

[andrejbauer]

This issue was more or less closed by #9. I also cleaned up the repository a bit and included in Cut.v a reference to @abooij's paper.

[VincentSe]

If I have time I'll send you a pull request with constructive versions of your theorems.

I actually meant isomorphic to the Cauchy reals. You do not need HOTT, or univalence or any axiom outside plain Coq. You almost have the isomorphism in your lemma archimedean. It asserts in sort Prop that there exist rational numbers arbitrarily close to any real number. If you put the sumbool in located, lemma archimedean lifts to sort Set and any real number gets a converging sequence of rational numbers.

Then why not put the sumbool ? It seems a low price to pay to get many usual properties of the real numbers. Or if you want something bigger than Cauchy reals, then why use locatedness instead of 1-sided (lower) reals ?

[abooij]

@VincentSe: The Cauchy reals and the Dedekind reals are different objects, and this is a well-known phenomenon that I don't think we fully understand. Indeed, a Dedekind real with locatedness in sumbool is the limit of a sequence of rationals (with modulus), so that we have not defined the Dedekind reals but the Cauchy reals.

Edited: Initially I claimed that the proposed isomorphisms would violate the equivalence relation on the sets of reals involved, but this need not be the case.

[VincentSe]

@abooij Yes, I have the full proof in standard Coq that the isomorphism works and respects the setoid equalities, on both the Dedekind and Cauchy sides. I was about to send it to you :)

So we all agree that the difference between Dedekind and Cauchy reals is the difference between or and sumbool. Then again, why not put the sumbool ? I mean in terms of the properties we can prove about the real numbers.

To me it looks similar to moving from classical to constructive logic : you can prove less things, but you are more confident in the things you do prove, and you have more tools that operate on the proofs, such as extraction. But here I don't see what we gain from weakening a sumbool to an or. More confidence that a Dedekind real is a number ? I hardly think so : you cannot extract its digits.

[abooij]

@VincentSe I believe that with sumbool this gives the Cauchy reals, yes, although I'm not entirely sure about some details (e.g. universe level), but it seems to work out.

The Dedekind reals are preferable over Cauchy reals for some purposes, such as their less intensional definition. (The Cauchy reals, in their usual presentation, are given by Cauchy sequences of rationals, which one may have philosophical objections to.) In non-setoid approaches (e.g. univalent foundations), there are properties that hold for the Dedekind reals but not for the Cauchy reals. For example, ironically, the Cauchy reals are not Cauchy complete in general, whereas the Dedekind reals are. In some foundational systems, the Cauchy reals are generally preferred even if the Dedekind reals can be defined. But then one shouldn't call such Cauchy reals "Dedekind reals", as the name of this repository does. We want to study in detail how the Cauchy and Dedekind reals are related, and so the Coq definitions should be accurate.

You mention extracting digits. In fact, extracting digits from your sumbool reals would violate the equivalence relation. It cannot be done in a way that respects the intended equality of the reals.

Yes, certain modifications to basic definitions allow proving more things. But that does not imply that they are better, because the definitions (i.e. assumptions) are also stronger. A whole lot of interesting math can be developed for Dedekind reals, so why focus on Cauchy reals?

[VincentSe]

@abooij I guess it means that the difference between sumbool and or is deeper than it looks. And this is interesting already. I do not see why extracting digits would violate an equivalence relation : the digits of a real number are unique (although there are different Cauchy sequences of rational numbers that converge to the same real number).

I won't argue this issue further. I have sent a pull request that corrects a constructive inconsistency in this repo, and proves 10 admitted lemmas. I will close this issue when it is merged.

[abooij]

@VincentSe Consider the digit expansion of the number 3/3. What is the integer part of this number? Is it 0, to obtain the digit expansion 0.999...? Or is it 1, to obtain the digit expansion 1.000...? Well, if you want to make the digit expansions unique, you probably want to exclude a tail of 9's. So you'd have to decide whether the digits are all 9's from some point onwards, or not, which sounds like an instance of LLPO.

This game shows that to compute digit expansions requires deciding an inequality (in the above example, to decide x<1), which cannot be done for arbitrary reals.

So if you want to output one sequence which is the digit expansion of a given real, you have to decide inequalities. And if you can decide inequalities, you can decide equalities (modulo getting the exact statement of this claim right).

One solution is to work instead with signed digit expansions, as is often done in computable and constructive analysis (and in fact Turing's famed paper which introduced computability made this same mistake, and a later correction used exactly this solution). In signed digit expansions, the digits of the (decimal, say) digit expansion range from -9 to +9, rather than from 0 to +9. So the number 1 can be represented as 1.000... or 0.999... or 2.(-9)(-9)(-9)... or 1.1(-9)(-9)(-9)..., etc.

[VincentSe]

@abooij ok fair point

[VincentSe]

@abooij Can you develop how you decide equalities if you know how to decide inequalities ?

[abooij]

@VincentSe: Suppose we can decide x<y and y<x. If one of them is true, then certainly x and y are apart. The remaining case is that both of them are false, that is, ¬(x<y)∧¬(y<x). But this is equivalent to (x≤y)∧(y≤x), i.e., x=y.

This argument shows that if x<y is decidable for all x,y, then apartness is decidable, which iin particular implies that equality is decidable (since the negation of apartness is equality, and apartness implies the negation of equality).

[VincentSe]

@abooij thanks

[VincentSe]

@abooij I found a question more interesting about Dedekind reals and Cauchy reals : can this implementation of Dedekind reals construct a real number and prove that it is not a Cauchy real ?

I suspect it cannot, because the effective topos is a model of constructive logic where all real numbers are computable, ie Cauchy reals.

To define a non computable Dedekind real, we would need an axiom on top of standard Coq, for example the excluded middle. I read you work on HoTT, so maybe univalence allows to construct such a number too. Do you know what axioms work ?

[abooij]

@VincentSe: Univalence does not suffice, because it is compatible with excluded middle, which implies that the Dedekind reals and the Cauchy reals coincide. You would need what some refer to as a constructive fetish, namely an axiom that contradicts classical axioms.