Computability in Europe 2006
Logical Approaches to Computational Barriers

Regular Talk:
Basic Model Theory for Bounded Theories

Speaker: Morteza Moniri
Author(s): Morteza Moniri


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.

websites: Arnold Beckmann 2006-06-15