[FOM] Ham sandwiches and expanders

Harvey Friedman friedman at math.ohio-state.edu
Sat Nov 15 09:09:56 EST 2003

Reply to Chow.

On 10/8/03 4:21 PM, "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:

> I am starting to learn a little about reverse mathematics and I am curious
> about the status of certain combinatorial theorems in this context.

> 1. Combinatorial consequences of the ham sandwich theorem.  For
> concreteness, let's take the following result of Akiyama and Alon.
> Let A_1, A_2, ..., A_d be pairwise disjoint sets of n points each
> in R^d, whose union is a set of nd points in general position.  Then
> there exist n pairwise disjoint (d-1)-dimensional simplices such that
> each simplex intersects each A_i in one of its vertices.
> 2. Existence of expanders.  Again for concreteness, let's take the
> following theorem due independently to Lubotzky et al. and Margulis.
> For every prime p = 1 (mod 4) there exist arbitrarily large (p+1)-regular
> graphs whose second largest eigenvalue is bounded in absolute value by
> 2*sqrt(p).
> These seem to me to be expressible in first-order arithmetic.  Are they
> known to be provable in EFA?  Or in one of the systems described in
> Simpson's book?

First of all, the most standard version of RM = reverse mathematics, is done
over the base theory RCA0. Anything that is provable in RCA0 is beneath the
radar screen for the standard RM.

However, if RM is interpreted more broadly, we do consider what happens over
weaker base theories than RCA0.

In the realm of finite mathematics, EFA = exponential function arithmetic,
is a good base theory for many purposes.

E.g., look at the usual finite Ramsey theorem. This is not provable in EFA,
and using EFA as the base theory, we know that the finite Ramsey theorem is
provably equivalent to "base 2 exponentiation can be iterated any finite
number of times starting at zero".

However, a great deal of finite mathematics can be done in EFA, and so for a
reverse mathematics study of a lot of finite mathematics, one needs a weaker
base theory than EFA. Here things start to get a bit controversial. E.g.,
there is PFA = polynomial function arithmetic, often just called bounded
arithmetic. Here one aims at proving equivalence with EFA over PFA. This can
be done, e.g., with the finite Ramsey theorem for 3-tuples.

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,

Without looking, I would guess that this is the situation that prevails in
your two examples. Is this correct?

Of course, it would be very interesting if there really is a problem in
carrying this out, even if the bounds are known. There could be a problem if
the proofs involve logically high powered methods - in particular, serious
use of real numbers - that cannot be straightforwardly eliminated by
obvious, but maybe very ugly, approximations by rationals.

Another example is Szemeredi's theorem, which has been shown by Gowers to
have a bound of a few exponentials. It is strongly believed that his proof
can be done in EFA, as one would expect. I haven't looked, but it is
virtually certain then that Szemeredi's theorem is provably equivalent to
EFA over PFA.  

On 10/27/03 4:34 PM, "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:

> Some weeks ago I asked about the reverse-mathematical status of the ham
> sandwich theorem and of the existence of Ramanujan graphs.  Here's a third
> item I'd like to ask about: the zero-one law for finite random graphs.
> Let G_{n,p} be the finite random graph with n vertices, whose edges each
> exist independently with probability p.  Then for any sentence phi in the
> first-order language of graphs, the limit as n goes to infinity of the
> probability that G_{n,p} satisfies phi is either 0 or 1.
> I *think* this theorem can be stated in the first-order language of
> arithmetic, but the usual proof proceeds by first showing that there
> is a unique (up to isomorphism) countable random graph---an infinitary
> argument.  (Thanks to Peter Cameron for pointing out this example to me.)
> Is this use of infinity eliminable?  I would think that the answer to
> this must be known.

I thought of this in 1967(!) for p = 1/2, and was persuaded (wrongly) by one
of my seniors at Stanford that this was not interesting, and so I dropped
it, and consequently never received any credit. I was preparing to think
about 0 < p < 1. 

First of all, the theorem can be formulated in a way that makes perfectly
good sense in RCA0, and then proved in RCA0. This is not completely obvious,
since one superficially needs the truth definition for predicate calculus of
an arbitrary structure. But in this case, one actually proves in RCA0 that

1) all graphs whose vertex set is the set of all natural numbers, satisfying
some simple saturation condition, are isomorphic;

2) for all such graphs, the truth set for predicate calculus exists.

3) the graphs in question can be represented by infinite paths through a
very explicit infinitely branching tree of finite sequences of natural

4) the notion of measure of the traces on the Cantor set of the infinite
paths through such trees can be appropriately explicitly defined, agreeing
with the usual measure;

5) the measure is 1.

On 10/31/03 9:43 AM, "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:

> First of all, my choice of theorems (0-1 law for graphs, ham sandwiches,
> Ramanujan graphs) wasn't arbitrary.  One way to try to find theorems that
> can't be proved using weak axioms is to try to construct them specifically
> with that purpose in mind. The other way is to look around for "naturally
> occurring" theorems that might fit the bill.

The classic example of a *purely finitary* theorem FROM THE LITERATURE where
we know that there is some strength, is the finite Ramsey theorem (reverses
to EFA over, say, PFA).

Semifinitary usually means that there is a given infinite object. E.g., for
all infinite sequences of blah blah blah, something happens in some finite
initial segment of the terms.

Semifinitary statements FROM THE LITERATURE are now known to be sometimes
very strong. In fact, all proofs must use quantification over uncountably
many infinite objects.

This is the case with KRUSKAL's theorem, and the more recent GRAPH MINOR

H. Friedman, Internal Finite Tree Embeddings, in: Reflections on the
foundations of mathematics, Essays in Honor of Solomon Feferman, Ed. Sieg,
Sommer, Talcott, Lecture Notes in Logic, ASL, 2002.

> Combinatorialists, particularly algebraic combinatorialists,
> spend a fair amount of their time considering theorems that have been
> proved using techniques from other areas of mathematics and trying to find
> new proofs that are more combinatorial.  ... I decided to look for
> theorems that so far have resisted people's attempts to find combinatorial
> proofs for them.

The problem is that we don't have an example where core mathematicians use
some high powered machinery to prove something combinatorial, YET one cannot
straightforwardly remove the machinery FROM THE LOGICAL POINT OF VIEW -
i.e., keep the machinery, but remove the infinitary aspects of it, replacing
it by finite approximations.

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.

Harvey Friedman

More information about the FOM mailing list