Improved Witnessing and Local Improvement Principles for Second-Order Bounded Arithmetic

摘要

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. Kolodziejczyk 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.