Preprint:

    Arnold Beckmann and Samuel R. Buss
    "Improved Witnessing and Local Improvement Principles for Second-Order Bounded Arithmetic"
    ACM Transactions on Computational Logic 15, 1 (2014) Article 2, 35 pages.

    Download manuscript: PDF.

Abstract:  This paper concerns the second order systems $U^1_2$ and $V^1_2$ of bounded arithmetic. 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{\l}odziejczyk, Nguyen, and Thapen 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.

Back to Sam Buss's publications page.