Vol. 15 No. 4, © The Author, 2005. Published by Oxford University Press. All rights reserved.
Original Articles |
Uniform Proof Complexity
University of Wales Swansea, Singleton Park, Swansea, SA2 8PP, UK. Email: A.Beckmann{at}swansea.ac.uk
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
10-hard and obviously in
20. 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
1b(
)-formulas.
Keywords: Length of proofs, propositional calculus, translations, bounded arithmetic
Received May 2005.