Preservation theorems for some special classes of first-order formulas (e.g.
existential formulas) are well-known in classical model theory. Notions like
quantifier elimination or model completeness are also well studied in
model theory.
We define similar notions and prove similar theorems for bounded formulas of
bounded theories (i.e. theories axiomatizable by bounded formulas). We
naturally define when a bounded theory has bounded quantifier elimination,
is bounded model complete, or has bounded model companion. We also prove some
basic
theorems on these notions. These provide natural extensions of
questions like P=NP or NP=coNP in the context of bounded theories.
We also study applications of these general results on some well-known theories
of classical bounded arithmetic like PV and CPV, and some intuitionistic
versions of them (via Kripke models).
These results are based on a paper to appear in AML, and also a
work in progress.