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... more