[FOM] constructive impredicativity?
gstolzen at math.bu.edu
Mon Mar 27 15:42:45 EST 2006
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
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
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
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
More information about the FOM