Almost 30 years ago, a number of folks in provability logic tried to show that GL (see for instance the excellent survey by Rineke Verbrugge here) is indeed the logic of $I\Delta_0+\Omega_1$ (in the following I refer to it as bounded arithmetics, though technically speaking there are various sub-systems of PA which are also entitled to this label).
If Rineke's revised article (2017) has not missed some very latest breakthrough, looks like whether GL is the provability logic of bounded arithmetic is still quite open.
Now, there was already a sense from the beginning that the reason why lifting the classical proof by Bob Solovay for PA's provability logic to bounded arithmetic is not viable (at least not by brute force), is that this seemingly sedate question is somehow related to deep complexity problems, perhaps even with the infamous P vs NP.
Here is then my question:
has there been any work on the above geared at making fully explicit the felt connection with complexity theory? By fully explicit I mean a result such as " if GL is the provability logic of bounded arithmetic then $\ldots$" (where the dots stand for some complexity theory's open question). Or perhaps the converse.
Any reference and/or comments will be deeply appreciated.
