[FOM] re Harvey on "a very exciting claim."

[Harvey Friedman]

On 3/26/06 1:17 PM, "Gabriel Stolzenberg" <gstolzen at math.bu.edu> wrote:


> 
>> THEOREM 8. Corollary 7 can be proved in strictly finite mathematics.
>> However, any such proof in Pi12-TI_0 must use at least 2^[1000]
>> symbols.
> 
>>  Here 2^[1000] is an exponential stack of 2's of height 1000.
> 
>  Harvey, I don't understand what this has to do with my remark about
> your claim.
> 

Pi12-TI_0 is certainly far stronger than normal accounts of constructivity,
and in particular anything that Bishop used in his book.

So Corollary 7 can be proved constructively (under normal accounts), but any
proof must be grotesque - in that it must use at least 2^[1000] symbols.

If Pi12-TI_0 is not regarded by some parties as encompassing constructivity,
in an appropriate sense, then for such parties, instead of Corollary 7, one
can use Sigma01 forms of stronger theorems such as the graph minor theorem.

And for parties that have an even wider view of constructivity, there are
some additional approaches that illustrate the same phenomenon.

Harvey Friedman