[FOM] Reverse mathematics, search problems, and bounded arithmetic

[Timothy Y. Chow]

Recall that a little while ago I asked about the proof-theoretic strength
of a couple of combinatorial problems.  Jeff Hirst and Harvey Friedman
gave good answers to my questions, but I have done a little more digging
and have a couple of further remarks and questions now.

One example I gave was the following theorem 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.

I picked this as a representative of a sizable class of combinatorial
theorems for which combinatorialists like to use the locution, "The only
known way to prove it uses topological methods."  The recent book by
Matousek, "Using the Borsuk-Ulam Theorem," gives a beautiful exposition of
numerous such theorems.  In the book, the Borsuk-Ulam theorem, and its
close relatives such as the Brouwer fixed-point theorem and the ham
sandwich theorem, are used to derive purely combinatorial consequences.

Leafing through Simpson's book, I found the following fact.

  WKL_0 is equivalent to the Brouwer fixed-point theorem over RCA_0.

Although I didn't see it stated explicitly in Simpson's book, it seems
plausible that the Borsuk-Ulam theorem and the ham sandwich theorem are
also equivalent to WKL_0.  This might seem to suggest that some of the
combinatorial theorems in Matousek's book aren't provable in RCA_0.
However, since the first-order parts of WKL_0 and RCA_0 are the same,
this seems highly unlikely.  Indeed, Simpson's book explicitly states
that Sperner's Lemma is provable in RCA_0.  Similarly, the other
combinatorial theorems are likely provable by suitable finite
approximations of the Borsuk-Ulam theorem.  These might still be
considered "proofs by topological methods" by combinatorialists,
even if they can be formalized in RCA_0.  However, they do raise the
possibility that maybe there are "more combinatorial" proofs of these
theorems waiting to be found.

Anyway, this just confirms Harvey Friedman's suggestion that to understand
this particular cluster of combinatorial theorems, one needs to move to
weaker systems, such as PFA and EFA.

What I would like to understand better is the relationship between what I
have just said above and the existing work in computational complexity on
search problems, particularly NP search problems.  There are some striking
(to me) analogies between the two areas that I would like to have
clarified.

To indicate what I mean by "work on NP search problems," I cite three
representative papers.

  Christos H. Papadimitriou.  On the complexity of the parity argument
  and other inefficient proofs of existence. J. Comput. System Sci. 48
  (1994) 498-532.

  Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, Toniann
  Pitassi. The Relative Complexity of NP Search Problems. J. Comput.
  System Sci. 57 (1998) 3-19.

  Tsuyoshi Morioka. Classification of Search Problems and Their
  Definability in Bounded Arithmetic. M.Sc thesis. University of
  Toronto, 2001.

This research concerns itself with existence proofs in combinatorics that
do not yield polynomial-time constructions.  The above three papers
further restrict attention to cases in which a candidate solution can
be described and verified to be correct in polynomial time (hence the
term "NP search problem").  What is rather striking, and reminiscent of
reverse mathematics as described in Simpson's book, is that there are
five classes of problems (PPP, PPA, PPAD, PPADS, PLS) that cover a wide
variety of NP search problems, and moreover many of the search problems
are complete for their classes.  The kinds of combinatorial theorems we
are talking about here include the pigeonhole principle (PPP), the fact
that every graph has an even number of odd-degree nodes (PPA), and the
fact that every directed acyclic graph with at least one edge has a sink
(PLS; this is the basis for a vast number of local search heuristics for
getting approximate solutions to NP-hard optimization problems).  Most
interestingly for my current purposes, PPAD is associated with Sperner's
Lemma and other combinatorial theorems associated with the Borsuk-Ulam
theorem and Brouwer's fixed-point theorem.

So, my first question is whether anything can be made of the fact that
Brouwer's fixed-point theorem shows up both in connection with PPAD and
with WKL_0.  If so, then are there "continuous analogues" of any of the
other NP search classes that correspond to natural subsystems of Z_2
that strictly contain RCA_0?  PLS would be my first candidate to examine,
since PLS is closely related to combinatorial optimization and there is,
analogously, a whole discipline devoted to optimization of continuous
functions.

Another question, related to the first but more concrete, is whether the
existence of Nash equilibria is equivalent to WKL_0 over RCA_0.  One can
state a suitably discretized version of the Nash equilibrium problem and
ask for its computational complexity; this is a major open problem, and in
particular, in spite of the close connections with various fixed-point
theorems, I believe that it is not known to be complete for PPAD.  If the
existence of Nash equilibria is not equivalent to WKL_0, then this would
in my opinion be another indication of a connection between WKL_0 and
PPAD.

Now let me give some "bad news."  The five aforementioned classes of NP
search problems by no means account for all the known important NP search
problems.  The most prominent examples are factorization and discrete log,
which do not seem to fit into Papadimitriou's framework.  Another class of
examples arises from probabilistic combinatorics.  Here is a concrete
example that Noga Alon suggested when I asked him about this:

  NEARLY RAMANUJAN GRAPHS: Find a 16-regular multigraph on n vertices
  whose second largest eigenvalue lambda_2 satisfies lambda_2 < 8.

This is a very special case of a deep theorem of Joel Friedman.  It turns
out that one can "construct," in polynomial time, a multigraph with the
desired property by randomly generating candidates and testing them to
see if they have the required property.  However, no explicit construction
is known, and again it does not seem to fit into Papadimitriou's framework.

Here is one more example that I thought of recently, which might fit into
Papadimitriou's framework or not (I haven't thought about it enough).
Suppose I have a polynomial identity, where one side contains polynomially
many terms while the other side contains exponentially many terms.  If I
compute the polynomial side and it comes out nonzero, then I know that at
least one of the terms on the other side is nonzero, but I don't know
which one.  (This sort of thing comes up in the study of "Rota's basis
conjecture," one of my favorite conjectures.)

Note also that not all interesting inefficient proofs of existence are NP
search problems.  For example:

  RAMSEY GRAPHS: Find a graph on n vertices that contains neither a
  clique nor an independent set of size 2 log_2 n.

One problem here is that even if I manage to generate a Ramsey graph by
chance, I have no efficient way of verifying that it is in fact a Ramsey
graph (even if I define "efficient" to mean BPP rather than P).  Or for
those of you who know the board game Hex:

  HEX: Find a winning move for the first player on an empty order-n
  Hex board.

The existence of the move is easily proved by a strategy-stealing
argument, but (generalized) Hex is PSPACE-hard.

If you still haven't had enough examples, Noga Alon's paper
"Non-constructive proofs in combinatorics" contains more
examples that may or may not categorize nicely.

So my last question (for now) is whether there is any hope of extending
Papadimitriou's classification to cover more of these cases.  Morioka's
thesis (which I've only skimmed so far) illustrates how bounded arithmetic
might provide a good framework for this project.  From the plethora of
examples I have just indicated, I would be inclined to start with trying
to make sense of probabilistic existence proofs.  What work has been done
on the logical status of these proofs, or on extending Papadimitriou's
framework to probabilistic combinatorics?

Tim