### arnold beckmann's pages

## Characterising Definable Search Problems in Bounded Arithmetic
via Proof Notations

**File:** PDF-File

**Author:** Arnold Beckmann and Sam Buss

**Title:** Characterising Definable Search Problems in Bounded Arithmetic
via Proof Notations

**Series:** In: *Ways of Proof Theory*, ed. R. Schindler,
Ontos Series on Mathematical Logic,
pp. 65-134, 2010.

**ISBN:** 978-3-86838-087-3.

**DOI:** 10.1515/9783110324907.65

**Abstract:**
The complexity class of
Π
p
k
- Polynomial Local Search (PLS)
problems with
Π
p
l
- goal is introduced, and is used to give
new characterisations of definable search problems in fragments of Bounded
Arithmetic.
The characterisations are established via notations for propositional proofs
obtained by translating Bounded Arithmetic proofs using the
Paris-Wilkie-translation.
For
l ≤ i ≤ k
, the
Σ
b
i
- definable
search problems of
T
k+1
2
are exactly characterised by
Π
p
k
- PLS problems with
Π
p
l
- goals.
These
Π
p
k
- PLS problems can be defined in a weak base
theory such as
S
1
2
, and proved to be total in
T
k+1
2
.
Furthermore, the
Π
p
k
- PLS definitions can be Skolemised
with simple polynomial time functions.
The Skolemised
Π
p
k
- PLS definitions give rise to a new
∀Σ
b
1
(α)
- principle
conjectured to separate
T
k
2
(α)
and
T
k+1
2
(α)
.