[FOM] Parallels between SOSOA and complexity theory?

[Timothy Y. Chow]

Some years ago on FOM I posed a vague and ignorant question about possible 
parallels between subsystems of second-order arithmetic and subclasses of 
the computational complexity class NP.

I would like to pose a hopefully slightly less ignorant, but still vague, 
question along similar lines.  Daskalakis, Goldberg, and Papadimitriou 
proved that a certain problem they dubbed NASH is PPAD-complete.  NASH is 
the following problem: Given the description of a game (by explicitly 
giving the utility of each player corresponding to each strategy profile), 
and a rational number epsilon > 0, compute an epsilon-approximate Nash 
equilibrium.

http://people.csail.mit.edu/costis/simplified.pdf

This negative computational result reminds me of the unprovability of 
Brouwer's fixed-point theorem in RCA_0, which in some sense boils down to 
Orevkov's example of an uncomputable fixed point.  What I'm wondering is, 
is this an isolated coincidence, or can we expect more parallels of this 
sort, between an unprovability result in reverse mathematics and a 
hardness result in complexity theory?  Maybe by bounding the quantifiers, 
since there are known parallels between computational complexity and 
bounded arithmetic?

Tim