### 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

** Abstract: **

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.

** Comments: **

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