V-Horn: A Horn-based second-order theory of arithmetic

In this thesis we present a second-order theory of arithmetic V-Horn, which encompasses polytime reasoning. It is equivalent in power to Zambella's P-def and Cook's QPV or PV₁; however, whereas those systems contain function symbols for all polytime functions, V-Horn achieves the same power by restricting the comprehension scheme to SO-Horn (as defined by Grädel) formulae. Our theory is possibly weaker than $V11$ and, equivalently, $S12$, in that it does not necessarily prove their comprehension (or induction) schemes.; We describe how to encode a run of Horn-SAT algorithm on a SO -Horn formula by a $SO\exists$-Horn formula, and use this result to demonstrate that SO-Horn is probably closed under complementation. The same method can be used to show that V-Horn provably defines all polytime functions.; We also show that some descriptive complexity results about SO-Horn logic, in particular the collapse of SO-Horn to its existential fragment, are formalizable in V₁ -Horn, a restriction of V-Horn.