V-Horn, a Horn-based second-order theory of arithmetic
Antonina Kolokolova · Library and Archives Canada (Government of Canada) · 2000
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 QP V or P V1; 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"adel) formulae. Our theory is possibly weaker than V 11 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 SO9-Horn formula, and use this result to demonstrate that SO-Horn is provably 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 V1-Horn, a restriction of V-Horn.