[FOM] Re Re: Re Harvey Friedman's "Sigma01/optimal" 24 Mar (I)

[Gabriel Stolzenberg]

Dear Harvey,

   Re:

> If you are going to allow impredicative definitions in constructive
> mathematics, then the examples I have been talking about DISAPPEAR.

> They can be cast in the following way.

> 1. There is a nice proof using impredicative definitions.

> 2. There is a proof without using impredicative definitions.

> 3. Any proof not using impredicative definitions will be of grostesque
size.

> 4. Claim 2 has a nice proof using impredicative definitions.

> 5. Any proof of claim 2 not using impredicative definitions will be of
grostesque size.

> 6. There is a nice proof of 3 not using impredicative definitions.

> I have no idea if you are still interested in these examples, since the
> "exciting" claims rely on the EXCLUSION of impredicativity from
> constructive mathematics.

   I think this is great.  Truly.  And, in my opinion, a much better
story.  Is there anyone who doesn't find impredicativity fascinating,
when they stop to think about it?  And, if I remember correctly, at
least in the case I know about (Kruskal's theorem), you can see the
impredicativiity at work and marvel at how, as if by magic, it takes
us places we could not have gone without it.  I say, "as if by magic,"
because it seems effortless.

   Also, in my opinion, impredicative definition, as a philosophical
theme, poses profound questions about the nature of language.  (In
particular, about what a definition is.  We all think we know!)  I
think that your remarkable examples will only add to the interest.

   With best regards,

     Gabriel







y