Re: "Kantor dust"

[Paul Taylor <pt09@PaulTaylor.EU>]

There have been several very interesting comments on this thread,
but I would like to repeat my request that people should be clear
about
      WHICH OF MANY "CONSTRUCTIVE" THEORIES OF MATHEMATICS
they mean as the context of their comments.   There are, as I said,
interesting mathematical points to be made, both within each of
these theories, and by comparing them.  However, without a clear
statement of the foundational context, the discussion degenerates.

The original question was about Cantor space, rather than either
the Cauchy or Dedekind reals.  If you want to construct Cantor space
from the reals by the "missing third" construction,  I would think
that it makes little difference whether you start from Cauchy or
Dedekind.  Or, indeed, from binary sequences, which of course form
a Cantor space in the first place, so that is really a question of
how to construct the reals from Cantor space rather than vice versa.

Vaughan Pratt said
> between Dedekind cuts and Cauchy sequences, the more appropriate notion
> of reals for constructive analysis would surely be the Cauchy reals
and I am certainly aware that, as a sociological fact, many type
theorists and exact real arithmetic programmers believe this.

Can anybody point me to a reasoned critique, or justification of the
view that Cauchy sequences are "more appropriate" for purposes such
as these?  All that I have ever heard is essentially a condemnation
of Dedekind for the "heresy" of impredicativity, uncountability,
non-computability, being a proper class, etc.

I gave a lecture (see PaulTaylor.EU/slides) entitled "In defence of
Dedekind and Heine--Borel", which I presented as if I were an
advocate in a court of law.  Several type theorists and constructive
analysts were present.   Beforehand, I had asked around for a statement
of "the case against Dedekind", but nobody seemed to be able to state
it for me.

Five years ago I had no opinion whatever on these matters, but, as you
gather, I now consider that both Dedekind completeness and the Heine--
Borel theorem are essential parts of "constructive" analysis.  Of
course, I think that because the reals in Abstract Stone Duality
satisfy them  (and because it puts me in agreement with mainstream
analysts).   However, ASD is a recursively axiomatised and enumerable
theory.   I don't like the notions of (un)countability or
(im)predicativity, but, if you must apply them, ASD is countable
and predicative.

Regarding computation,  last year Andrej Bauer gave a "proof of concept"
demonstration that one can compute efficiently with Dedekind reals
in the ASD language for R.  This of course uses interval arithmetic,
but in fact it also makes extremely novel use of back-to-front
("Kaucher") intervals, which appear but are very badly presented
in the interval analysis literature.   I have been trying to persuade
him to make this work publicly available.

Since I'm talking about the reals in ASD, I should say what the
difference is between the Cauchy and Dedekind reals is there.
I haven't actually written out a construction of the Cauchy reals,
but the evidence that I do have is that THEY ARE THE SAME.   More
precisely, Dedekind completeness is inter-derivable with sobriety
for R, just as definition by description is equivalent to sobriety
of N.   This means that if you construct the "Cauchy reals" as a
quotient of Cantor space by an equivalence relation (this is known
as the "signed binary" representation of reals) within ASD then
the result will be Dedekind complete.   The details of this are
set out in Section 14 of "The Dedekind reals in ASD" by Andrej and me,
www.PaulTaylor.EU/ASD/dedras

I think it is worth making a note of Vaughan's earlier comment that
> In concrete Stone duality, increasing structure on one side is offset
> by
> decreasing structure on the other.  One would hope for a similar
> phenomenon in abstract Stone duality.
>
> If we can consider constructivity as part of the structure of an
> object,
> then we should expect that the more constructive some type of object,
> the less constructive the "object of all objects of that type."   So
> for
> example if (total) recursive functions are demonstrably more
> constructive than partial recursive functions by some criterion, we
> should expect the set of all recursive functions to be *less*
> constructive than that of partial recursive functions by the same
> criterion, rather than more.
>
> The phenomena you're observing here seem entirely consistent with this
> principle, and point up the need to be clear, when judging
> constructivity in some context, whether it is the collection or the
> individuals therein being so judged, with the added complication that
> Stone duality makes the roles of collection and individual therein
> interchangeable, such as when elements of sets are understood as
> ultrafilters of Boolean algebras.

However, I think that the Galois--Stone contravariance applies WITHIN
a particular foundational system, and not to VARIATIONS of the degree
of constructivity.  Indeed, the usual experience in setting up a
Galois connection or Stone adjunction is that, in order to make the
comparison work at all, you need to make additional assumptions.

Paul Taylor