Axioms necessary for theoretical computer science This question is inspired by a similar question about applied mathematics on mathoverflow, and that nagging thought that important questions of TCS such as P vs. NP might be independent of ZFC (or other systems). As a little background, reverse mathematics is the project of finding the axioms necessary to prove certain important theorems. In other words, we start at a set of theorems we expect to be true and try to derive the minimal set of 'natural' axioms that make them so. 

I was wondering if the reverse mathematics approach has been applied to any important theorems of TCS. In particular to complexity theory. With deadlock on many open questions in TCS it seems natural to ask "what axioms have we not tried using?". Alternatively, have any important questions in TCS been shown to be independent of certain simple subsystems of second-order arithmetic?
Yes, the topic has been studied in proof complexity. It is called Bounded Reverse Mathematics. You can find a table containing some reverse mathematics results on page 8 of Cook and Nguyen's book, "Logical Foundations of Proof Complexity",  2010. Some of Steve Cook's previous students have worked on similar topics, e.g. Nguyen's thesis, "Bounded Reverse Mathematics", University of Toronto, 2008.

Alexander Razborov (also other proof complexity theorists) has some results on the weak theories needed to formalize the circuit complexity techniques and prove circuit complexity lowerbounds. He obtains some unprovability results for weak theories, but the theories are considered too weak.

All of these results are provable in $RCA_0$ (Simpson's base theory for Reverse Mathematics), so AFAIK we don't have independence results from strong theories (and in fact such independence results would have strong consequences as Neel has mentioned, see Ben-David's work (and related results) on independence of $\mathbf{P} vs. \mathbf{NP}$ from $PA_1$ where $PA_1$ is an extension of $PA$).