Improved witnessing and local improvement principles for second-order bounded arithmetic
Arnold Beckmann, Samuel R. Buss · ACM Transactions on Computational Logic · 2014
This article concerns the second-order systems U 1 2 and V 1 2 of bounded arithmetic, which have proof-theoretic strengths corresponding to polynomial-space and exponential-time computation. We formulate improved witnessing theorems for these two theories by using S 1 2 as a base theory for proving the correctness of the polynomial-space or exponential-time witnessing functions. We develop the theory of nondeterministic polynomial-space computation, including Savitch's theorem, in U 1 2 . Kołodziejczyk et al. [2011] have introduced local improvement properties to characterize the provably total NP functions of these second-order theories. We show that the strengths of their local improvement principles over U 1 2 and V 1 2 depend primarily on the topology of the underlying graph, not the number of rounds in the local improvement games. The theory U 1 2 proves the local improvement principle for linear graphs even without restricting to logarithmically many rounds. The local improvement principle for grid graphs with only logarithmically-many rounds is complete for the provably total NP search problems of V 1 2 . Related results are obtained for local improvement principles with one improvement round and for local improvement over rectangular grids.