Abstract

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 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 are polynomially equivalent. Mints and Kojevnikov [G. Mints, A. Kojevnikov, Intuitionistic Frege systems are polynomially equivalent, Zapiski Nauchnyh Seminarov POMI 316 129–146] have recently shown p-equivalence of Frege systems for the intuitionistic propositional calculus 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 281–294]. We prove a similar result for an infinite family of normal modal logics, including K4, GL, S4, and