Abstract:
Bounded arithmetic is designed to characterize low complexity
computability, i.e., the polynomial hierarchy. The main open
problem for bounded arithmetic is the question if bounded arithmetic
is finitely axiomatizable, which is equivalent to asking if the
levels of bounded arithmetic S^i_2, T^i_2 collapse. Furthermore,
this question is also connected to the open problem whether the
polynomial hierarchy collapses. The precise connection is that
bounded arithmetic is finitely axiomatized if and only if bounded
arithmetic can prove that the polynomial hierarchy collapses
[Buss 1995, Zambella 1996].
In this talk we will give model-theoretic
characterizations of
the separation problem of bounded arithmetic. The main tool will
be
restricted consistency statements, whose complexity is captured by
a
bounded analog of Pi_1. Our characterizations will be similar
to
the following one:
Two levels of bounded arithmetic -- say S^i_2 vs. T^j_2 for
j >= i
-- are separated by a bounded Pi_1 sentence if and only if there
exists a model of the smaller theory (i.e., S^i_2) without proper
bounded-elementary extensions to a model of the stronger theory
(i.e., T^j_2).
Remark for experts: By "bounded Pi_1"
we mean the universal
closure of Pi^b_1, and "bounded-elementary extensions" is the
restriction of elementary extensions to sharply bounded formulas.