摘要：This paper is a contribution to our understanding of the relationship between uniform and nonuniform proof complexity. The latter studies the lengths of proofs in various propositional proof systems such as Frege and bounded-depth Frege systems, and the former studies the strength of the corresponding logical theories such as VNC1 and V0 in [Cook/Nguyen, 2010]. A superpolynomial lower bound on the length of proofs in a propositional proof system for a family of tautologies expressing a result like the pigeonhole principle implies that the result is not provable in the theory associated with the propositional proof system. We define a new class of bounded arithmetic theories n^epsilon-ioV^\infinity for epsilon 0.
