Arnold Beckmann's Pages

Uniform proof complexity

File: PDF-File
DOI: 10.1093/logcom/exi035
Journal: Journal of Logic and Computation 2005, 15: 433-446


We define the notion of the uniform reduct of a propositional proof system as the set of those bounded formulas in the language of Peano Arithmetic which have polynomial size proofs under the Paris-Wilkie-translation. With respect to the arithmetic complexity of uniform reducts, we show that uniform reducts are \Pi^0_1-hard and obviously in \Sigma^0_2. We also show under certain regularity conditions that each uniform reduct is closed under bounded generalisation; that in the case the language includes a symbol for exponentiation, a uniform reduct is closed under modus ponens if and only if it already contains all true bounded formulas; and that each uniform reduct contains all true \Pi^b_1(\alpha)-formulas.


Steve Cook made a comment on Problem 2. He showed that the existence of a proof system whose uniform reduct equals the set of all true bounded formulas is equivalent to the existence of an optimal proof system.
Cook's Comments (ps-file), in arXiv

Arnold's homepage