On the proof complexity of logics of bounded branching

0560276 - MÚ 2024 RIV NL eng J - Journal Article
Jeřábek, Emil
On the proof complexity of logics of bounded branching.
Annals of Pure and Applied Logic. Roč. 174, č. 1 (2023), č. článku 103181. ISSN 0168-0072. E-ISSN 1873-2461
R&D Projects: GA ČR(CZ) GA19-05497S
Institutional support: RVO:67985840
Keywords : proof complexity * modal logic * intermediate logic * extended Frege system
OECD category: Pure mathematics
Impact factor: 0.8, year: 2022
Method of publishing: Limited access
https://doi.org/10.1016/j.apal.2022.103181

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 [...]
Permanent Link: https://hdl.handle.net/11104/0333265