[FOM] reading the bible with Bill: hermeneutics with Gabriel

[William Tait]

Concerning my objection to Bishop's 'definition' of a function as an  
(extensional) effective rule,
on Feb 24, 2006, at 12:30 PM, Gabriel Stolzenberg wrote

>    More important, although this quote may have the grammatical form
> of a definition, it is not one.  Moreover, it wouldn't make sense for
> it to be one.  Think about it.

Thank you, I did. That is why I had come to the same conclusion.

> maybe the best way to make my point is for you to show me,
> if you can, where, if anywhere, Bishop makes use of this alleged
> definition of "operation."  Do you agree that if he never uses it
> as a definition, that's pretty good evidence that it isn't meant as
> one?

You are making the additional point that Bishop didn't really intend  
it as a definition. Fair enough. Then perhaps we are in agreement  
(and maybe Bishop, too?) that what concepts in constructive  
mathematics 'mean' is shown by how they are used in constructive  
mathematics, and so, to the extent that these methods, with suitable  
coding, are also methods of classical mathematics, constructive  
mathematics can be regarded as part of classical mathematics. And  
that, after all was the message of my (poor;y written "Against  
intuitionism" to which you referred. By 'suitable coding', i refer to  
the fact that, e.g., 'continuous function' must be understood as  
'locally uniformly continuous function' in order that the  
constructive proof not appear to have a gap in it (filled by Heine- 
Borel). Or, in the case of the intuitionists, free variables over  
choice sequences (say of natural numbers) have to be understood as a  
notation indicating that natural number-valued functions of these  
variables must be locally uniformly continuous (or, equivalently,  
their unsecured sequences must be well-founded).

>> constructive mathematics has to build properties into definitions
>> that classical math gets free (e.g. local uniform continuity from
>> continuity).
>
>    Think of it this way, if you have a function that is obviously
> uniformly continuous, it doesn't advance the ball to prove that it
> is pointwise continuous and then invoke the Heine-Borel theorem to
> conclude that it is uniformly continuous.  But, in the classical
> mind set that is, in effect, what often happens because it's not
> noticed at the start that the function in question is obviously
> uniformly continuous.

This seems to me to be a misleading way to put the point, which is:  
Using H-B does not in general yield an effective modulus of uniform  
continuity and so invoking it may loose information that a direct  
constructive proof of luc would yield---IN THOSE CASES in which there  
is a constructive proof of luc. It is a good example, illustrating  
the general---and well-known---fact that general non-constructive  
existence proofs often lose the information in particular cases that  
there is an algorithm for determining the object.  Agreed, agreed,  
agreed. But it doesn't justify a new metaphysics of mathematics. The  
objects that the classical proof fails to compute and the  
constructive one does are the same objects---reals, real functions,  
whatever.

> It's only in a constructive mindset that
> this is obvious. In different mindsets, different phenomena are
> obvious.  But I forgot, you think you don't care about mindsets.

I have no problem with mind sets: they just don't determine what is  
true or false. In this case I think that all you mean is that if one  
is acquainted with the idea of proving things constructively and  
maybe have had some practice at it, then in some cases it will be  
clear that a constructive modulus can be determined.

>    Also, re "constructive mathematics has to build properties into
> definitions that classical math gets free," aren't you conflating
> classical properties with constructive ones?

I mean only that, if one reads a proof in Bishop, for example, one  
has to know that luc is built into the use of the term 'continuous'.  
I hope that this is all that you are referring to: If you really  
mean  that there are 'constructive properties' not intelligible in a  
'classical mindset', then we are really not on the same page.

> If you are, that
> suggests that you're looking at constructive mathematics only in
> a classical mindset.  But, however common it may be to do so, it's
> perverse.

It is possible to understand both classical and constructive  
mathematics without wearing the blinkers that you call 'mindsets'.

Best regards,

Bill