Re: Dedekind versus Cauchy reals

[gcuri@math.unipd.it]

Quoting Paul Taylor <pt09@PaulTaylor.EU>:

>
>
> Toby has also said a lot of interesting things about many different
> systems.  These illustrate my point that it is essential to state
> which system, or which notion of "constructivity" you intend.
>
> He has said, for example
> * 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).
> * 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 [he] can tell, do not; excluded
>    middle, power sets, fullness, or countable choice would each do the
>    job, but you need ~something~.
>
> I would challenge someone to consider the last of these questions
> seriously, maybe taking a hint from the second.   ASD provides another,
> as it uses lambda term over a special object instead of talking about
> "sets" of rational numbers.

A note concerning the possibility of constructing the Dedekind reals without
fullness, etc:
the Dedekind reals can be defined in constructive set theory  even without
excluded middle, power sets, fullness, or countable choice. The point is that
they then form a class and not a set.
Class-sized objects are however the norm in a constructive predicative setting.
For instance, a (non-trivial) locale is carried by a class that is never a set;
in general a formal space or formal topology is a large object too, so that one
often deals with superlarge "categories" with large homsets.


Giovanni Curi



Dipartimento di Matematica Pura ed Applicata
Universita' degli Studi di Padova
www.math.unipd.it