We introduce a second-order system V/sub 1/-Horn of bounded arithmetic formalizing polynomial-time reasoning, based on Gradel's (1992) second-order Horn characterization of P. Our system has comprehension over P predicates (defined by Gradel's second-order Horn formulas), and only finitely, many function symbols. Other systems of polynomial-time reasoning either allow induction on NP predicates (such as Buss's (1986) S/sub 2//sup 1/ or the second-order V/sub 1//sup 1/), and hence are more powerful than our system (assuming the polynomial hierarchy does not collapse), or use Cobham's theorem to introduce function symbols for all polynomial-time functions (such as Cook's PV and Zambella's P-def). We prove that our system is equivalent to QPV and Zambella's (1996) P-def. Using our techniques, we also show that V/sub 1/-Horn is finitely, axiomatizable, and, as a corollary, that the class of /spl forall//spl Sigma//sub 1//sup b/ consequences of S/sub 2//sup 1/ is finitely axiomatizable as well, thus answering an open question.
展开▼
机译：我们基于Gradel（1992）对P的二阶Horn表征，引入了有界算术形式化多项式时间推理的二阶系统V / sub 1 / -Horn。我们的系统对P谓词（由Gradel的第二阶（仅适用于Horn公式），并且只能有限地包含许多功能符号。其他多项式时间推理系统允许对NP谓词进行归纳（例如Buss（1986）S / sub 2 // sup 1 /或二阶V / sub 1 // sup 1 /），因此功能更强大。比我们的系统（假设多项式层次结构不会崩溃），或使用Cobham定理为所有多项式时间函数（例如Cook的PV和Zambella的P-def）引入函数符号。我们证明我们的系统等效于QPV和Zambella（1996）的P-def。使用我们的技术，我们还证明了V / sub 1 / -Horn是有限的，公理化的，并且作为推论，/ spl forall // spl Sigma // sub 1 // sup b / S /的后果sub 2 // sup 1 /也可以有限地公理化，因此回答了一个悬而未决的问题。
展开▼
