University of Toronto
Abstract
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 AC0 together with comprehension over L-formulae. If the
class is provably in V-L closed under AC0 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.
Table of Contents
1 Introduction.
2 Descriptive complexity background.
2.1 Capturing complexity classes by logics.
2.2 Capturing feasible classes.
3 Bounded arithmetic and generalized witnessing.
3.1 Translation from descriptive complexity to bounded arithmetic.
3.2 Systems of arithmetic V-Phi.
3.3 Definability.
3.4 Witnessing.
3.5 Example: witnessing for V^0.
3.6 V-Phi is finitely axiomatizable.
3.7 History.
4 V_1-Horn: a system of arithmetic for P.
4.1 V_1-Horn extends V^0.
4.2 Encoding the Horn SAT algorithm by a Sigma _1^B-Horn formula.
4.3 Explicit definability theorem for V_1-Horn.
4.4 Finite Axiomatizability.
4.5 Equivalence of V_1-Horn, P-def and QPV.
5 V-Krom: a system of arithmetic for NL.
5.1 System V-Krom.
5.2 V-Krom extends V^0.
5.3 V-Krom(TrCl).
5.4 Normal form of TrCl.
5.5 Relating Sigma^B_1-Krom and Sigma_0^B(TrCl^+).
5.6 The Immerman-Szelepcsenyi theorem.
5.7 Definability in V-Krom.
5.8 V-Krom is finitely axiomatizable.
5.9 Equivalence with Nguyen's VNL.
6 A weakly closed system: symmetric logspace.
6.1 Symmetric transitive closure.
6.2 Simulating Sigma_0^B formulae.
6.3 Constructiveness of Sigma^B_1-SymKrom.
6.4 A weak definability theorem for V-SymKrom and finite axiomatizability.
7 Conclusion.
Bibliography.
Number of pages: 155
