[FOM] Re: Ham sandwiches and expanders

[Timothy Y. Chow]

Harvey Friedman <friedman at math.ohio-state.edu> wrote:
> The two examples you give are, or can easily be naturally put into, AE
> form over the natural numbers. For reasonably natural AE sentences, we
> have found that once one has an upper bound on the growth rate involved,
> one gets a proof in the obvious formal system associated with that
> growth rate. Also, once one has a lower bound on the growth rate
> involved, one gets a reversal to the obvious formal system associated
> with that growth rate.
>
> Most commonly, one has an exponential lower bound, and a short stack of
> exponentials for an upper bound. Then one has reversal to EFA over, say,
> PFA.
>
> Without looking, I would guess that this is the situation that prevails in
> your two examples. Is this correct?

Thanks for your detailed reply.  I can't answer your question off the top
of my head, but it would certainly seem plausible for at least the ham
sandwich case.  At any rate, I now have a better sense of what sorts of
things to keep an eye out for when looking for proofs that potentially
use strong logical assumptions.

> On the other hand, we have never been able to get any meaningful help
> from mathematicians outside logic to investigate these matters. So there
> may be high powered machinery proofs lying around, done by the core
> mathematicians, that resist finite approximation. I am not willing to
> investigate such matters without help from people who are expert in
> those contexts. Without such collaboration, I have decided that it is
> not a productive use of my time, given what else I could be doing.

Although I have never personally studied it, I am told that SGA4 is
written with a background of strong set-theoretic assumptions.  This
machinery has been used to derive a variety of highly non-trivial finitary
consequences.  So it would seem to be a natural place to look.  However,
the chances are that in most if not all cases, the finitary consequences
can be derived without using the fancy set theory.  (The Ramanujan graph
example most likely falls into this category; it certainly doesn't even
need all the SGA machinery.)  See

http://www.google.com/groups?selm=TEKE.93Jun28213131%40insanus.nada.kth.se
http://www.google.com/groups?selm=TEKE.93Jun30110305%40insanus.nada.kth.se

for one educated opinion along these lines.

So, given the amount of effort it would take to wade through SGA4, not to
mention all the prerequisites for it, it's not clear that it's worth the
effort.  Even those who have already invested the effort to learn this
stuff may feel that they have more productive uses of their time than to
spend a lot of effort verifying what is probably a foregone conclusion.

The so-called "core mathematicians" might be enticed if there were some
likely, tangible payoff for pursuing these questions.  For example, have
these kinds of reverse-mathematical investigations ever led to the
discovery of new, simpler proofs of the theorems in question---where
here I use the words "new" and "simpler" the way a "core mathematician"
would use them?  A new and simpler proof of the Weil conjectures would
be of great interest to many "core mathematicians."

Tim