9 February 2021, The Utrecht Logic in Progress Series (TULIPS), Emil Jerabek

Abstract: When studying the proof complexity of classical logic, one of the basic tools is feasible interpolation, which gives a way to transform circuit lower bounds into length-of-proof lower bounds. A similar role in the proof complexity of modal logics is played by the feasible disjuction property, which is at the core of known lower bounds on modal Frege and extended Frege (EF) proof systems.

In this talk, we will discuss the feasibility of variants of the disjunction property (and more general extension rules) in some modal logics, and its application for length-of-proof separation of EF from SF (substitution Frege) proof systems for modal logics of unbounded branching. Finally, we will have a look at the complexity of the disjunction property in basic logics of bounded branching.