I've been trying to understand better some of the research on forcing over bounded arithmetic and its connections with lower bounds in complexity theory. For example, Takeuti and Yasumoto have some papers where they prove results such as, for certain $M$ and certain $G$, if $M[G]$ doesn't satisfy Buss's $S_2$, then NP ≠ co−NP. Krajíček's book Bounded Arithmetic, Propositional Logic, and Complexity Theory also touches on this topic, showing how to recast some lower-bound proofs in complexity theory as forcing arguments.
These connections are intriguing but I don't understand them well enough yet to be able to make up my mind whether this is mostly a curiosity or whether it has the potential to lead somewhere new and interesting. One thing that I'd like to know is the degree to which constructions in set theory carry over (or are likely to carry over) to arithmetic. Perhaps a slightly more precise phrasing is,
Where and how does the parallel between forcing over set theory (ZFC, say) and forcing over arithmetic (or bounded arithmetic) break down?
Another way to put it might be, is there any sketch of a program (even if a wildly optimistic one) for carrying over ideas from set theory to arithmetic in such a way as to prove new lower bounds in complexity theory? A result like the theorem by Takeuti and Yasumoto that I cited above is a start, but doesn't quite count in my mind unless we have some reason to think that insights from set theory will help us understand the properties of $M[G]$. Can we hope for this or are there some basic obstacles that make this approach highly unpromising?