Logic seminar

Proof complexity of logics of bounded branching, Part 2

We revisit the problem of Frege and extended Frege (EF) lower bounds for transitive modal logics. Hrubes proved an exponential lower bound on the number of lines in Frege proofs, or equivalently, on the size of EF proofs, for some basic modal logics such as K, K4, S4, and GL. This was extended by Jerabek to an exponential separation between EF and substitution Frege (SF) systems for all transitive logics of unbounded branching.

On the other hand, for typical logics of bounded width, the EF and SF systems are p-equivalent, and they are in a certain sense p-equivalent to the classical EF system, for which we do not know any lower bounds, and even candidate hard tautologies are scarce.

The main ingredients in all the lower bounds above (as well as similar bounds for superintuitionistic logics) were variants of the feasible disjunction property (DP), playing a role similar to feasible interpolation in classical proof systems.

This raises the question what happens for logics with bounded branching but unbounded width, such as K4BB_k, S4BB_k, and GLBB_k. In this talk, I will show that while these logics apparently do not have feasible DP as such, they have DP (and more general extension rules) decidable in ZPP^{NP}, and for k=2, even in promise-S_2^P. Moreover, one can also adapt Hrubes's form of "monotone interpolation" to this setting.

As a consequence, we prove superpolynomial speedup of SF over EF assuming PSPACE \ne NP (possibly exponential under a stronger hypothesis) for all modal logics included in GLBB_2 or S4GrzBB_2, and more generally, for all logics L that, in a certain sense, admit all finite binary trees (with reflexive or irreflexive points as convenient) to appear inside L-frames.