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

[Harvey Friedman]

On 3/29/06 7:16 PM, "Gabriel Stolzenberg" <gstolzen at math.bu.edu> wrote:

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.

There are some more high powered examples, which would be dissolved in the
same way ONLY if one accepts, constructively, a form of ZF and beyond. These
are more esoteric and very recent.

Harvey Friedman