# [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^
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.

that I see where.  And I prefer not to guess.

To be continued.

With best regards,

Gabriel

```