[FOM] constructive impredicativity?

[Gabriel Stolzenberg]

   The remarks below border on the simplistic.  (I'm not sure on
which side.)  Read them as a failed first attempt to discuss the
"deep issue" to which I alluded in "re Harvey on 'a very exciting
claim.'"

   I did, initially, have a problem with impredicativity.  Sort of.

   I had always been able to spot a construction in a classical proof
of a certain kind of assertion.  When Harvey showed me cases where I
couldn't, among them ones in which impredicativity figured prominently,
I was conflicted.  On the one hand, I was tempted to say that if I
couldn't spot a construction, then I couldn't say that there was one.
On the other hand, who said that if there is one, I should be able to
spot it?

   That was then.  Now, I am very comfortable with impredicative
definitions.  In fact, I think some of them are marvelous.  But I
have no metaphysical justification for this view.  I suspect that
it is something that I carried along unthinkingly from my classical
mindset and, now that I've lived with it in my constructive one, I
like what I see.

   To pursue this more seriously, I would vote for first reviewing
Goedel's argument against constructive impredicativity in "Russell's
mathematical logic" (reprinted in Benacerraf and Putnam, "Philosophy
of mathematics: selected readings" 1983).  Because if it's good, then
that's it.

   In a different direction, I would recommend looking at the role
of impredicative definitions in constructive high level programming
languages/formal systems like ALF, Coq or LEGO.

   I'm going to stop here and read Harvey's latest message before I
continue.

      Gabriel Stolzenberg