[FOM] Ham sandwiches and expanders

[Timothy Y. Chow]

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?

More generally, in the spirit of Harvey Friedman's conjecture
( http://www.cs.nyu.edu/pipermail/fom/1999-April/003063.html ),
I wonder if it's possible to draw up a list of theorems whose
proofs seem to embody some interesting principle but whose exact
proof-theoretic strength hasn't yet been clarified.  I think
Fermat's Last Theorem is too ambitious to be on such a list but
there ought to be others.  Perhaps someone has already drawn up
such a list?

Tim