The paper considers a commonly used axiomatization of the classical propositional logic and studies how different axiom schemata in this system contribute to proof complexity of the logic. The existence of a polynomial bound on proof complexity of every statement provable in this logic is a well-known open question.The axiomatization consists of three schemata. We show that any statement provable using unrestricted number of axioms from the first of the three schemata and polynomially-bounded in size set of axioms from the (...) other schemata, has a polynomially-bounded proof complexity. In addition, it is also established, that any statement, provable using unrestricted number of axioms from the remaining two schemata and polynomially-bounded in size set of axioms from the first scheme, also has a polynomially-bounded proof complexity. (shrink)

We investigate the substitution Frege () proof system and its relationship to extended Frege () in the context of modal and superintuitionistic propositional logics. We show that is p-equivalent to tree-like , and we develop a “normal form” for -proofs. We establish connections between for a logic L, and for certain bimodal expansions of L.We then turn attention to specific families of modal and si logics. We prove p-equivalence of and for all extensions of , 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 system for classical logic with respect to a naturally defined translation.On the other hand, we establish exponential speed-up of over for all modal and si logics of infinite branching, extending recent lower bounds by P. Hrubeš. We develop a model-theoretical characterization of maximal logics of infinite branching to prove this result. (shrink)

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. (shrink)

We give proofs of the effective monotone interpolation property for the system of modal logic K, and others, and the system IL of intuitionistic propositional logic. Hence we obtain exponential lower bounds on the number of proof-lines in those systems. The main results have been given in [P. Hrubeš, Lower bounds for modal logics, Journal of Symbolic Logic 72 941–958; P. Hrubeš, A lower bound for intuitionistic logic, Annals of Pure and Applied Logic 146 72–90]; here, we give considerably simplified (...) proofs, as well as some generalisations. (shrink)

We give an exponential lower bound on the number of proof-lines in intuitionistic propositional logic, IL, axiomatised in the usual Frege-style fashion; i.e., we give an example of IL-tautologies A1,A2,… s.t. every IL-proof of Ai must have a number of proof-lines exponential in terms of the size of Ai. We show that the results do not apply to the system of classical logic and we obtain an exponential speed-up between classical and intuitionistic logic.