[FOM] re reading the bible with Bill: hermenutics with Gabriel

[Gabriel Stolzenberg]

   Before I begin my response to Bill Tait's February 25 reply to
"reading the bible with Bill," I want to say something about the
character of the exchange.

   Although I hope very much that we will reach an understanding
(not necessarily an agreement), most likely by one or both of us
discovering that he had been misreading the other, from where
I now stand, it seems no less likely that at least one of us is
mistaken about the nature of constructive mathematics and its
relationship to classical mathematics.  (And if Kreisel was right,
it's me!)

   So, both in the spirit of full disclosure and as a caution to
the reader, I wish to report that when, about 25 years ago, I
submitted an NSF proposal to continue a project on the philosophy
of constructive mathematics that I had begun with the support of
a Guggenheim fellowship, one reviewer said that I knew nothing
about constructive mathematics and must not apply again until I
learn something about it.  Another faulted me for not knowing the
current literature, when the reason I had ignored it was that,
insofar as it had any relevance, I didn't find it interesting
enough to criticize.  (As a physicist might have put it, "It wasn't
even wrong.")  And those were the good reviews!  So, caveat lector.

   Now for my reply to Bill.

> Concerning my objection to Bishop's 'definition' of a function as an
> (extensional) effective rule,

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

   I'm sorry, but from the way you introduced the quote, it sounded
as if you had assumed that Bishop meant it as a definition.  Here is
what you said:

> > > I was/am not concerned with mindsets or intentions; I was
> > > concerned with definitions.  Let me quote from the bible:

   Also, Bishop did not talk about an "effective" rule for doing
something.  Such talk is loaded because its home is in classical
talk about Turing "machines," which we're supposed to think of as
"performing" one step after another, maybe terminating, maybe not.
(Isn't it marvelous that a set can do such things?  Can your set
do that?)  In a constructive mindset, there is no such thing as
an ineffective rule or procedure for doing something.  If it's
ineffective, it doesn't do it.  ("Hi, I'd like to buy a car."  "Do
you want one that works?")

> You are making the additional point that Bishop didn't really
> intend it as a definition.

   It's not an additional point.  It's just another way of making
the same point.

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

   I doubt very much that we are in agreement, if only because I
would never talk this way.  More precisely, when I do, I don't
expect it to be taken too seriously.

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

    These methods?  Doesn't "these" refer to concepts?

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

   The constructive proof of what?  The only candidate I see here
is the theorem that a uniformly continuous function is uniformly
continuous.  I assume that this is not what you mean.  Also, to
whom might the proof that you have in mind appear to have a gap?
And why should we care?

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

   It's just a word.  Bishop didn't have to call it "continuous."  No
more than classical mathematicians have to call pointwise continuous
"continuous."

> I have no problem with mind sets: they just don't determine what is
> true or false.

   I don't know why you want to get into this.  Whether a statement
is true or false depends on what it means and meaning has its home
in a mindset.  Now, "depends on" is not the same as "determine."  But
if the mindsets don't determine what is true or false in mathematics,
what does?  Perhaps you will persuade me otherwise, but I don't see
any evidence that talk of "true and false" of the kind that you seem
to want is available for classical mathematics.  Isn't this why God
invented formal systems?

> >   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 lose information that a
>  direct constructive proof of luc would yield---IN THOSE CASES in
>  which there is a constructive proof of luc.

  Bill, if that was my point, it would indeed be misleading.  You're
saying that, when a classical mathematician invokes H-B to prove that
some function is uniformly continuous, he risks "losing" information
that a constructive proof (perhaps valid only for some cases) would
possess--if there were such a  constructive proof.  Something like
that, right?

   But my point has nothing to do with either H-B or with "losing"
information that some other proof might possess.  I'm talking about
a classical proof of the pointwise continuity of a function that can
be seen at the start to be uniformly continuous but is not recognized
as such because the classical mindset encourages the idea that the
pointwise proof cannot be seen this way.

   Also, I prefer to focus on the "correction" that I made (in the
beginning of "intuitions of intuition in Chicago and Cambridge" Feb 26)
to what I say above, not because it is wrong (it's not) but because
it's not the kind of case I meant to talk about.  I will not rehearse
this here except to note that, in some cases of the kind I did mean to
talk about, the constructivist recognizes a "hidden" proof of uniform
continuity even though the proof is not constructive.

   Finally, unlike Bill, I am interested in this only as a cognitive
phenomenon, not as a mathematical one.  As mathematics, it's on the
level of a party trick.  I offer it here solely as a bit of evidence
for the existence of the two different mindsets and the difference in
their character.

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

   To repeat, a classical proof of the kind I'm talking about does
not "lose" information.  It's rather that, in a classical mindset,
it often isn't noticed and, hence, is assumed to be lost.  There
are many good examples of this.  (Bill might remember one in which
he was a participant.)

    E.g,, why do classical mathematicians who should know better
still offer Euclid's proof of the infinitude of primes--the one
that consists in making a construction, pasting on "Suppose not"
in front and then noticing that there is a contradiction--as an
example of the power of the indirect method?  Why don't they see
the construction that is staring them in the face?  I think it's
because the classical mindset encourages the idea that it is not
there and this is a case in which disbelieving is not seeing.

> > It's only in a constructive mindset that this is obvious.  In
> > different mindsets, different phenomena are obvious.

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

   I'm sorry but this is painfully simplistic.  If you're a classical
mathematician, you first have to learn how to undo (but not abandon)
your classical mindset.  Until you can do this, you can't learn the
other one.  It's like a duck/rabbit drawing.  If you're seeing it as
a duck, you can't see it as a rabbit until you're able to stop seeing
it as a duck.  And this is only the beginning.

   As for the mathematical practice of which you speak dismissively,
it is not merely a matter of "maybe have had some practice at it,"
as if it doesn't matter how much or what kind.  On the contrary, it
takes discipline and guidance, without both of which there are many
ways one can go wrong, primarily because of the residual influence of
one's classical mindset.  (I speak here from my own experience, as
someone who had only the discipline, not the guidance.)

   As for the mathematics in your remark, you seem to be talking
about constructing a modulus of continuity, whereas I'm not talking
about constructing anything.  As for what I am talking about, see
above.

   Finally, maybe another anecdote will help.  About thirty years ago,
the Princeton differential topologist, John Mather, gave the weekly
mathematics colloquium here.  His object of study was a certain kind
of stratification of a diferentiable manifold, a certain sequence of
subsets, each a closed subset of its predecessor.  Although I knew
nothing about the subject, when, during the lecture, I shifted into
my constructive mindset, I found myself wondering how John, in his
classical one, could make use of the assumption that the sets were
closed.  (If you had asked me why I was wondering this, I couldn't
have told you.  I just was.)  At the end of the talk, I asked the
only question.  "Where do you use the assumption that the sets are
closed?"  John turned to the blackboard, thought about it a while,
then turned back and said, "I don't."

   Bill may not be impressed but other people were.  (To which he
might reply, "Other people believe that they were sexually abused
by aliens.")

   To be continued.

     Gabriel