[FOM] reading the bible with Bill

[Gabriel Stolzenberg]

   On February 11, William Tait wrote,

>  Dear Gabriel,

> You are too fast for me, so let me reply at the same time to the two
> messages in which you address my remark about circularity in my paper
> "LEM and AC".

   As you see, I've slowed down.  Too much.  So, to speed things up
a bit, I'm going to reply in stages, taking the easiest stuff first.

   You wrote,

> About my LEM and AC:

> >   Hence, this something (which we call "a procedure" or "a
> > computation") is not something that can serve as an arbiter
> > for what in the mathematics is true and what is not.  If it
> > were being asked to fulfill such a role, it could not.  But
> > it is not being asked to do that.
> >
> >   At least, so say I.  However, on my reading, the following
> > statement from Tait's "The law of excluded middle and the axiom
> > of choice" implies that what I say above about the constructive
> > mathematical mindset (in particular, mine) is false.  He writes,
> >
> >      "The circle is ineliminable in constructive mathematics,
> >       because whatever principles of logic are given, they
> >       must answer the challenge of whether they really yield
> >       'constructive objects.'  For the notion of being
> >       constructive is intended as a measure of correctness
> >       for any particular principle considered."
> >
> >    Nevertheless, this claim about the intentions of people like
> > me is mistaken.  We break the apparent circle of which Tait speaks
> > (I call it a regress) the same way he does; indeed, I congratulate
> > him for having seen that it is the right thing to do.


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

>  "An operation from a set A to a set B is a rule f which assigns an
>  element f(a) of B to each element a of A.  The rule must afford an
>  explicit finite , mechanical reduction of the procedure for
>  constructing f(a) to the procedure for constructing a." [Bishop,
>  *Foundations of Constructive Analysis* p. 14.]


   Bible?  FCA is a first try!  Isn't that obvious?  Just recall
the circumstances under which it was written.

   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.

   Consider next that what you take to be Bishop making a definition
relies upon six unexplained terms, "rule," "explicit," "finite,"
"mechanical," "reduction" and, last but not least, "procedure for
constructing."  Doesn't that make you even a little bit suspicious?
"Rule" is especially mysterious.  (It was replaced in the revised
version by something like "finite routine."  That helps a lot,
doesn't it?)  Taken literally, Bishop writes as if he expects the
reader to know what a rule is and is explaining what an operation
is in terms of it.  But why are we more likely to understand "rule"
than "operation"?

   Bill, 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?  In a math text, wouldn't it be odd to make a definition that
is never used?

   Onward.

> A function is defined there to be an extensional operation. A rule f
> is an operation from A to B if it satisfies a for all x in A exists y
> in B condition. Constructively that is understood as a exists z in (A
> -->C) forall x in A statement, where C is the domain of reductions.
> The definition is therefore circular in that the notion of an
> operation from A to C is contained in the definition of the notion of
> an operation from A to C. (There is an infinite regress of witnesses:
> g to witness the fact that rule f is an operation, h to witness that
> g is, etc.)

   We've been through this before, haven't we?  Yes, if it were a
definition, it would be circular, just in the way that is described.
above.  But it is not, so it is not.  See above.

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

   Also, re "constructive mathematics has to build properties into
definitions that classical math gets free," aren't you conflating
classical properties with constructive ones?  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.

   Gabriel Stolzenberg