Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style


Antonina Kolokolova

Systems of bounded arithmetic from descriptive complexity


University of Toronto


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.

Number of pages: 155

ISSN 1433-8092 | Imprint