[FOM] Re Harvey Friedman's "Sigma01/optimal" 24 Mar (I)
friedman at math.ohio-state.edu
Thu Mar 30 01:54:24 EST 2006
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
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
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.
More information about the FOM