Re: "Kantor dust"

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

Paul Taylor wrote in part:

>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.

Besides the case that you present briefly in your slides,
there is this:  The Cauchy reals exist an a Pi-W-pretopos
(equivalently, in a constructive set or type theory
with exponentiation but no power sets or even fullness
and with infinity but no countable choice).
But the Dedekind reals, as far as I can tell, do not;
excluded middle, power sets, fullness, or countable choice
would each do the job, but you need ~something~.
(ASD takes another approach, of course.)

And while I don't know any non-finitist practising constructivists
that doubt all of these, I do know at least one that doubts each.
Thus practising constructivists may happily use the Dedekind reals,
while formalists that want to cover all practising schools
find that they are not quite available in the obvious common denominator.
(Actually, Brouwer intuitionists don't really even accept exponenenation,
although they do accept N^N and AC_00 so do have Cauchy = Dedekind reals.)

I don't find this argument conclusive; the proper course is either
to accept the existence of the Dedekind reals as an axiom
(since everybody believes it, even if for different reasons)
or just to give up on point-set topology and use locales
(although these require subtlety to use predicatively).
But it's there, and it probably explains some logicians' positions.

>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.

But ASD with the underlying-set axiom is impredicative, yes?

I really like ASD, so don't interpet my post as opposition to your position,
but rather an attempt to clarify what the opposition may be thinking.


--Toby