Systems of bounded arithmetic from descriptive complexity
Antonina Kolokolova · Medical Entomology and Zoology · 2005
In this thesis we discuss a general method of constructing systems of bounded arithmetic from descriptive complexity logics of known complexity. We discuss the conditions under which the resulting systems capture the same complexity class in the bounded arithmetic setting as the corresponding logic in the descriptive complexity setting. Our method works for small complexity classes (P and below) which have simple proofs of closure under complementation. Additionally, we require proofs of membership and co-membership for instances of decision problems to be constructible within the same complexity class. More formally, given a logic L capturing complexity class C, the corresponding second-order system V-L of arithmetic consists of a system for AC 0 together with comprehension over L-formulae. If the class is provably in V-L closed under AC 0 reductions and every formula or its (possibly semantic) negation can be witnessed in C, then the resulting system captures C. Based on this general theorem, we discuss systems of arithmetic for classes P and NL. We also give a system of arithmetic for SL, although the definability theorem for SL is weaker.