Abstract   We investigate the substitution Frege (   SF   ) proof system and its relationship to extended Frege (   EF   ) in the context of modal and superintuitionistic (si) propositional logics. We show that    EF    is p-equivalent to  tree-like     SF   , and we develop a “normal form” for    SF   -proofs. We establish connections between    SF    for a logic   L  , and    EF    for certain bimodal expansions of   L  .  We then turn attention to specific families of modal and si logics. We prove p-equivalence of    EF    and    SF    for all extensions of    KB   , all tabular logics, all logics of finite depth and width, and typical examples of logics of finite width and infinite depth. In most cases, we actually show an equivalence with the usual    EF    system for classical logic with respect to a naturally defined translation.  On the other hand, we establish exponential speed-up of    SF    over    EF    for all modal and si logics of infinite branching, extending recent lower bounds by P. Hrubes. We develop a model-theoretical characterization of maximal logics of infinite branching to prove this result.
['Emil Jeřábek']
Substitution Frege and extended Frege proof systems in non-classical logics