On Proof Complexities Relations in Some Systems of Propositional Calculus
Keywords:the varieties of propositional sequent systems, the varieties of Frege systems, the number of proof steps, exponential speed-up
The number of linear proofs steps for some sets of formulas is compared in the folowing systems of propositional calculus: PK – seguent system with cut rule, PK— - the same system without cut rule, SPK – the same system with substitution rule, QPK – the same system with quantifier rules. The number of steps of tree-like proofs in the same systems for some considered set of formulas is compared from Alessandra Carbone in  and some distinctive property of the system QPK is revealed: QPK has an exponential speed-up over the systems SPK and PK, which, in their turn, have an exponential speed-up over the system PK—. This result drew the heavy interest for the study of the system QPK. In this work for linear proofs steps in the same systems the other relations are received: it is showed that the system QPK has no preference over the system SPK, it is showed also that for the considered formula sets the system PK has no preference over the system PK—, which, in its turn, has no preference over the monotone system PMon. It is proved also, that the same results are reliable for some other sets of formulas and for other systems as well.
A. Carbone, “Quantified propositional logic and the number of lines of tree-like proofs”, Studia Logica, vol.. 64, pp. 315-321, 2000.
S. Cook and R. Reckhow, “The relative efficiency of propositional proof systems”, Journal of Symbolic Logic, vol. 44, pp. 36-50, 1979.
P. Pudlák, The Lengths of Proofs, in S. Buss (ed.), handbook of proof Theory, North Holland, pp. 547-637, 1998.
S. C. Kleene , Introduction to Metamathemics. D.VanNostrand Company, INC, 1952.
Г. Цейтин и Ан.Чубарян, “Некоторые оценки длин логических выводов в классическом исчислении высказываний”, ДАН Арм. ССР, т. LV, N 1, 10-12, 1972.
A. Atserias, N. Galesi and R. Gavalda, “Monotone proofs of the pigeon-hole principle”, Mathematical logic quarterly, vol. 47, no. 4, pp. 461-474, 2001.