[FOM] Re Re on Bas Spitters on "constructive impredicativity?" 31 Mar

[Gabriel Stolzenberg]

   This is a reply to parts of Bas Spitters' "Re on Bas Spitters
on "constructive impredicativity?" (March 31), which is mainly an
exchange with Harvey Friedman.

    Bas quotes Harvey saying,

(HF) > > I always viewed Bishop style constructivity as entirely
     > > predicative under the Feferman/Schutte elucidation. In
     > > fact, I always viewed Bishop style constructivity as living
     > > comfortably within a conservative extension of HA.

(GS)  There was no concern about making impredicative definitions.
Which is not to deny that there should have been.  Maybe our lack of
concern merely reflected our naivete.  Maybe.  Who knows?  If there
were few such definitions in FCA, that's just how it was.

   If Bishop thought there was a problem, he would surely have said
so.  (He would surely have said so to me!)  If not in the book, then
in one of his survey lectures.  He liked to talk about such things.
But what reason might he have had for thinking there was a problem?
Goedel gave one but it seems to have been the result of taking the
create/discover metaphor too literally (which is, to say, literally).

   In my view, what, if anything, Bishop thought about these matters
is now of limited scientific or even philosophical interest.  FCA was
a wonderful first try, good mainly for critiquing and starting again.
(But not as in the revised version!)

(HF) > > Where in Bishop do you see any substantial logical strength
     > > beyond that of HA?

(BS) > I came across two instances where Bishop seems to be
     > "impredicative".  To be precise, I mean where he uses the power
     > set in an essential way.

(GS)  Again, I would caution against attaching too much importance to
what is and is not in FCA.  It has the effect of making it out to be
something that it is not and was never meant to be.  There are much
better ways of using this book to understand constructive math and
even better ways of mastering it without it.

   Finally, notwithstanding what I say above, in my view, there seem
to be extremely interesting and philosophically important questions
concerning impredicativity.  I find them very difficult to talk about
but maybe a good place to start is with Goedel's metaphysical critique
in "Russell's mathematical logic.".

.
   Gabriel Stolzenberg