Re: "Kantor dust"

[Toby Bartels <toby+categories@ugcs.caltech.edu>]

Prof. Peter Johnstone wrote in part:

>Vaughan Pratt wrote:

>>Whose reals, Cauchy's or Dedekind's?

>Toby was of course referring to the Dedekind reals

Actually, I was trying to keep it open,
since different schools of constructivism have different opinions
about which are the correct reals (as well as which are equivalent).
But nobody uses the binary reals, since they can't subtract them.
(To get the first digit of 0.1000000000... - 0.01000000000...,
you need to know which sequence, if either, stops repeating first.)
I agree that one would default to Dedekind reals (or something equivalent),
since that seems to be agreed on by the "practising" schools
(that is, those constructivists trying to do ordinary mathematics,
 albeit constructively, rather than doing metamathematics).

>>Lubarsky and
>>Rathien in Logic and Analysis 1:2 131-152 have recently made the point
>>that whereas Cauchy reals can be understood constructively as a set, any
>>attempt to make Dedekind's reals constructive turns them into a proper
>>class.

I'll have to read what they mean, but to say ~any~ attempt seems too strong.
Even in a predicative theory, countable choice implies their equivalence,
so are they claiming that countable choice is not constructive?
(In my experience, Fred Richman is the only practising non-finitist analyst
 who doubts both excluded middle and countable choice.)
The Dedekind reals can also be constructed in CZF
(Peter Aczel's predicative constructive set theory)
even if you remove countable choice, using subset collection aka fullness.
Similarly, if you remove identity types from intensional type theory
(so breaking the justification of countable choice),
you can still justify the fullness axiom and so construct the Dedekind reals
(albeit not literally as sets of rational numbers).

>>Between Dedekind cuts and Cauchy sequences, the more appropriate notion
>>of reals for constructive analysis would surely be the Cauchy reals.

The experience in measure theory and Banach space theory since the 1980s
suggests that a Dedekind-complete ordered field is needed.
The only question is whether such a thing exists; most believe it does.
(If countable choice or excluded middle holds, the Cauchy reals work,
 which takes care of nearly every practising analyst, constructive or not.
 Fred Richman, the only exception I know, still uses the Dedekind reals,
 although that's easy for him since he is not predicativist.)

Note: everything above is about the ~located~ Dedekind reals;
a located Dedekind cut is a pair (L,U) of order-open inhabited sets
such that r in L and s in U => r < s => r in L or s in U.
This is what Freyd's coalgebra construction produces,
and it's what practising analysts want to use.


--Toby