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

[Timothy Y. Chow]

Here are a few addenda to my previous post on this topic.

Recall that I asked whether anything can be made of the fact that
Brouwer's fixed-point theorem shows up both in the context of WKL_0
and in the context of Papadimitriou's complexity class PPAD.  I still
think that there is something interesting going on here, but I currently
can't see what to do.  Recall the familiar analogy

   polynomial : superpolynomial  ::  decidable : undecidable

as exemplified, for instance, in the analogy between the polynomial
hierarchy and the arithmetical hierarchy.  Michael Freedman has speculated
that there might be a geometric or topological way of understanding this
analogy, and that if one were able to figure out how to connect the two
sides of the analogy with a suitable limiting process, then this might
help prove that the polynomial hierarchy doesn't collapse.  Well,
Brouwer's fixed-point theorem is topological, its being unprovable in
RAC_0 says roughly that the fixed points aren't necessarily computable
even if the defining function is, and one suspects that P != PPAD.
So this looks like a possible instance of Freedman's paradigm.  But so
what?  I don't know.

Regarding extending Papadimitriou's framework to probabilistic
combinatorics: I overlooked that Papadimitriou makes some preliminary
comments on the subject at the end of his paper.  For example, he
introduces the class PLL (LL = "local lemma"); Lovasz's local lemma
is perhaps the best-known method of giving probabilistic existence
proofs in which the probabilities are exponentially small.  I'm still
trying to digest Papadimitriou's remarks so I'm not sure yet what can
be said about the Ramsey graphs and nearly-Ramanujan graphs that I
mentioned previously.

Finally, I recall that there has been some work establishing lower
bounds on resolution proofs of the pigeonhole principle.  Does this
work also provide similar lower bounds for proofs of other combinatorial
lemmas underlying NP search problems?

Tim