We introduce a second-order system V_1-Horn of bounded arithmetic formalizing polynomial-time reasoning, based on Graedel's second-order Horn characterization of P. Our system has comprehension over P predicates (defined by Graedel's second-order Horn formulas), and only finitely many function symbols. Other systems of polynomial-time reasoning either allow induction on NP predicates ... more >>>