[FOM] Re Re: Re Harvey Friedman's "Sigma01/optimal" 24 Mar (I)
gstolzen at math.bu.edu
Wed Apr 5 14:11:01 EDT 2006
> 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
> 4. Claim 2 has a nice proof using impredicative definitions.
> 5. Any proof of claim 2 not using impredicative definitions will be of
> 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,
More information about the FOM