FOM: Effective Bounds in Core Mathematics

[Harvey Friedman]

Richman 2:14PM 6/29/00 writes:

"I think that it is more accurate to say that constructive
mathematicians and classical mathematicians are talking about the same
things."

Do you really want to say this? Isn't the constructive mathematician
tempted to accept or regard as plausible, a statement like:

*if x is a real number then there is a recursive sequence of rationals
q1,q2,... such that for all i, |qi - x| < 1/i?

If the constructive mathematician regards this as at least plausible, and
the classical mathematician regards this as absurd (they consider it
refuted), then how can you maintain that they are "talking about the same
things"?

OK, one can defend this as follows. The constructivist may not think that
one can pass from a real number x to an algorithm for producing the
recursive sequence. But then I can come back with the weaker statement:

**if x is a real number then it is absurd that there is no recursive
sequence of rationals q1,q2,... such that for all i, |qi - x| < 1/i

or even the yet weaker statement

***if x is a real number then it is absurd that for any partial recursive
sequence of rationals q1,q2,..., there is an i such that qi is undefined or
|qi - x| >1/i***

which is also classically absurd. But doesn't the constructive
mathematician think this is extremely plausible as a constructive assertion?

By the way, are you a constructive mathematician?