[FOM] Re: Absoluteness of Clay prize problems

[Timothy Y. Chow]

Harvey Friedman wrote:
> In the same way, I believe that in your second category, "the study of
> real numbers and certain well-behaved functions on real numbers", you
> will find the following phenomena.  When a celebrated theorem of this
> kind is proved, mathematicians will quickly and fruitfully dissect it
> into the trivial component and the nontrivial novel component. The
> trivial component will generally involve nonarithmetical statements.
> However, the nontrivial novel component will be Pi-0-1 or maybe Pi-0-2.

Dave Marker and I both asked for an example and I am eagerly awaiting
Harvey Friedman's reply.  In the meantime, though, it occurred to me that
maybe Brouwer's fixed-point theorem is sort of an example.  It is
something of a folklore belief that Brouwer's fixed-point theorem
"follows" from the combinatorial theorem known as Sperner's lemma.  
However, as we know from Simpson's book, Brouwer's FPT is not provable in
RCA_0 while Sperner's lemma is.  So at least in some people's eyes, the
transition from Sperner to Brouwer is relatively "trivial" compared to
Sperner's lemma itself, even though this "trivial" step involves a
proof-theoretical ascent from RCA_0 to WKL_0.  Sperner's lemma, of course,
is Pi^0_1.

But maybe "trivial" is the wrong word here.  A recent article in the 
American Mathematical Monthly by Jarvis and Tanton describes how to
prove the hairy ball theorem via Sperner's lemma.  This inference is
interesting enough for a publishable paper and hence in some sense is
definitely not "trivial"; nevertheless, there is still a residual feeling
that Sperner's lemma is capturing some essential insight here and that
it "implies" the hairy ball theorem.  It's intriguing to me that we have
a pretty clear case here where "implication" as informally used by 
mathematicians is in a certain precise sense *not* a direct proof-
theoretic implication (by the way, am I right in assuming that the
hairy ball theorem is equivalent to Brouwer's fixed-point theorem over
RCA_0?).

Tim