Substitution Frege and extended Frege proof systems in non-classical logics (Q1023047)

Substitution Frege (SF) proof systems have the substitution rule \(\phi\vdash \phi[p_1/\phi_1,\ldots,p_n/\phi_n]\) in addition to axiom schemata and the rule of modus ponens. Extended Frege (EF) systems have extension axioms \(q\Leftrightarrow \psi\) for a fresh propositional letter \(q\) instead of the substitution rule. It was known that SF and EF are polynomially equivalent for the classical propositional logic. The author proves the same result for all extensions of KB, all tabular logics, all logics of finite depth and width, in most cases by a polynomial intertranslation with the classical logic. For all modal and superintuitionistic logics of infinite branching a polynomial speed-up of SF over EF is established, extending recent result by P. Hrubeš.