[Proof Complexity] preprint

[Emil Jerabek]

Dear colleagues,

a new paper "On the proof complexity of logics of bounded branching"
is available on my web page at https://math.cas.cz/~jerabek/ .
Corrections, suggestions, and comments are welcome.

Best regards,
Emil Jerabek

Abstract:
We investigate the proof complexity of extended Frege (EF) systems for
basic transitive modal logics (K4, S4, GL, ...) augmented with the
bounded branching axioms BB_k. First, we study feasibility of the
disjunction property and more general extension rules in EF systems
for these logics: we show that the corresponding decision problems
reduce to total coNP search problems (or equivalently, disjoint NP
pairs, in the binary case); more precisely, the decision problem for
extension rules is equivalent to a certain special case of
interpolation for the classical EF system. Next, we use this
characterization to prove superpolynomial (or even exponential, with
stronger hypotheses) separations between EF and substitution Frege
(SF) systems for all transitive logics contained in S4.2GrzBB_2 or
GL.2BB_2 under some assumptions weaker than PSPACE \ne NP. We also prove
analogous results for superintuitionistic logics: we characterize the
decision complexity of multi-conclusion Visser's rules in EF systems
for Gabbay--de Jongh logics T_k, and we show conditional separations
between EF and SF for all intermediate logics contained in T_2 + KC.