### arnold beckmann's pages

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

**File:** PDF-File

**Author:** Arnold Beckmann and Samuel R. Buss

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

**Journal:** ACM TOCL 2014, **15**(1): 2:1-2:35

**Pages:** 35

**DOI:** 10.1145/2559950

**Abstract:**
This paper 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 in
U
1
2
.
Koł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
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.