[FOM] General Foundations Discussion

[richman]

Harvey Friedman wrote:

>For the purposes of constructive analysis (e.g., in the sense of
>Bishop), only Cauchy completeness is worth anything - Dedekind
>completeness is not.

That's a bit of an overstatement. In the absence of countable choice, Cauchy 
completeness is often useless. You need a stronger notion of completeness, 
which the located Dedekind real numbers satisfy. (The located Dedekind real 
numbers were described by Bishop. They are equivalent, in the presence of 
countable choice, to Cauchy real numbers.) It is true that you probably 
wouldn't want to call this stronger notion of completeness "Dedekind 
completeness". For one thing, it makes sense for an arbitrary metric space.

--Fred