Frege systems for extensible modal logics

By a well-known result of Cook and Reckhow [S.A. Cook, R.A. Reckhow, The relative efficiency of propositional proof systems, Journal of Symbolic Logic 44 (1) (1979) 36–50; R.A. Reckhow, On the lengths of proofs in the propositional calculus, Ph.D. Thesis, Department of Computer Science, University of Toronto, 1976], all Frege systems for the classical propositional calculus (CPC) are polynomially equivalent. Mints and Kojevnikov [G. Mints, A. Kojevnikov, Intuitionistic Frege systems are polynomially equivalent, Zapiski Nauchnyh Seminarov POMI 316 (2004) 129–146] have recently shown p-equivalence of Frege systems for the intuitionistic propositional calculus (IPC) in the standard language, building on a description of admissible rules of IPC by Iemhoff [R. Iemhoff, On the admissible rules of intuitionistic propositional logic, Journal of Symbolic Logic 66 (1) (2001) 281–294]. We prove a similar result for an infinite family of normal modal logics, including K 4 , G L , S 4 , and S 4 Grz .