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.

  • 2
    $\begingroup$ As far as I am aware, no such connection has been spelled out, except for the one mentioned in the original Berarducci-Verbrugge paper: if bounded arithmetic proves NP=coNP, then its provability logic is GL (this a rather tenuous connection as the premise is widely assumed to be false, while the conclusion may well be true). There was really nothing published about this problem at all besides that single paper. $\endgroup$ – Emil Jeřábek Jul 6 '20 at 14:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.