[FOM] Re Harvey Friedman's "Sigma01/optimal" 24 Mar (I)
Gabriel Stolzenberg
gstolzen at math.bu.edu
Wed Mar 29 19:16:22 EST 2006
In this message and the next, I continue my attempt to understand
an assertion of Harvey Friedman that, in a previous message, I called
"a very exciting claim."
Dear Harvey,
I have a few elementary questions re:
PROPOSITION. (Six labels). There exists n >= 1 such that the following
holds. Let T_1,...,T_n be trees with vertices labeled from {1,...,6},
where each T_i has at most i vertices. There exists 1 <= i < j <= n
such that T_i is inf preserving and label preserving embeddable into T_j.
> THEOREM. The Proposition can be proved in strictly finite mathematics.
> However, any such proof in ACA_0 + Pi12-BI must use at least 2^[1000]
symbols.
1. What exactly do you mean here by "strictly finite" mathematics.
(Is there also "sort of finite" mathematics?) Obviously you are using
it as a technical term, but how?
2. Is strictly finite math constructive? If not, how does it fail?
3. Is strictly finite math part of ACA_0 + Pi12-BI? Again, if not,
how does it fail?
4. I understand you to say that the proposition to which you refer
has both a non-grotesque nonconstructive proof and constructive ones,
all which are grotesquely long.
Assuming I have this right, I'm trying to learn whether your proof
that there are constructive proofs of the proposition is constructive
and non-grotesque. And if it is not, whether you can rule out there
being such a proof.
You've probably answered these questions already but I'm not sure
that I see where. And I prefer not to guess.
To be continued.
With best regards,
Gabriel
More information about the FOM
mailing list