Cutting plane and Frege proofs (Q1898117)

The cutting plane refutation system CP for classical propositional calculus [see \textit{W. Cook}, \textit{C. R. Coullard} and \textit{Gy. Turan}, Discrete Appl. Math. 18, 25-38 (1987; Zbl 0625.90056)], initially coming from works in operation research, can be considered as an extension of resolution based on showing the non-existence of solutions for families of integer linear inequalities. In this paper the author introduces a modification \(\text{CP}^+\) of the system CP and proves that \(\text{CP}^+\) can polynomially simulate Frege proof systems. An effective cut-elimination theorem for \(\text{CP}^+\) is obtained and a translation of Frege proofs into \(\text{CP}^+\) proofs is described. A propositional formulation of the Paris-Harrington theorem [see \textit{J. Paris} and \textit{L. Harrington}, ``A mathematical incompleteness in Peano arithmetic'', in: Handbook of mathematical logic (J. Barwise, ed.), 1133- 1142 (1977; Zbl 0443.03001)], the Kanamori-McAloon theorem [see \textit{A. Kanamori} and \textit{K. McAloon}, Ann. Pure Appl. Logic 33, 23-41 (1987; Zbl 0627.03041)] and variants are proposed as possible candidates for combinatorial tautologies which may require exponential size cutting plane and Frege proofs.