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

[Gabriel Stolzenberg]

   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