Logical Studies

Bounded Model Theory and its Applications to Bounded Arithmetic

Document Type : Review

Authors

Abolfazl Alam
Morteza Moniri

Department of Mathematics, Shahid Beheshti University, Tehran, Iran

https://doi.org/10.30465/lsj.2021.36251.1358
Abstract
Bounded model theory can be considered as part of first-order model theory, which its aim is to study model-theoretic notions in a language consisting of an order relation where all quantifiers are restricted to the bounded ones. One can apply bounded model theory to study some problems in bounded arithmetic. Bounded arithmetic can be considered as a sub-theory of first-order Peano arithmetic in an extended language. Bounded arithmetic has some applications in computational complexity theory. There are already some related bounded model-theoretic concepts like bounded quantifier elimination and bounded model completeness which has been applied to bounded arithmetic and complexity theory. In this article, we review some known results and prove some new ones in bounded model theory and use them to obtain certain results in bounded arithmetic and complexity theory. In particular, we define the notion of bounded model companion and study its relations to some fundamental problems in complexity theory.

Keywords

Bounded Arithmetic
Bounded formula
Bounded model complete
Bounded model companion
Bounded quantifier elimination
منیری، مرتضی (1384). «نظریة مرتبة اول پئانو و زیرنظریه‌های آن همراه باچند مسئلة مرتبط در نظریة پیچیدگی»، فرهنگ و اندیشة ریاضی، ۲۴، صص. ۳۳-۵۵.
Buss, S‎. ‎R‎. (1986).‎‎Bounded Arithmetic‎, Napoli: Bibliopolis.
‎Buss,‎S‎. ‎R‎. (1995). ‎Relating the Bounded Arithmetic and ‎‎Polynomial Time Hierarchy. ‎Annals of Pure and Applied Logic‎, ‎75‎, ‎pp.67-77‎.
‎‎Buss,‎S‎. ‎R. (1998).‎ Handbook of Proof Theory‎.‎Amsterdam: ‎Elsevier.
‎Chang‎, C. C., ‎Keisler‎, J. (1990).‎Model theory‎, ‎‎Amsterdam: North-Holland‎.
‎‎Cook‎, S. A. (1975). Feasibly Constructive Proofs and the Propositional Calculus‎(preliminary version). ‎Seventh Annual ACM Symposium on Theory of ‎‎Computing,‎83-97‎.
‎Cook‎,‎S‎. ‎A. (2009). ‎Review of Three‎‎Papers Relating the Collapse of the Polynomial Hierarchy to the Collapse of Bounded Arithmetic‎.‎‎http://www.cs.toronto.edu/~sacook/‎.
‎Cook‎,‎S‎. ‎A., ‎Urquhart‎,‎A. (1993). Functional Interpretations‎‎ of Feasibly Constructive Arithmetic‎. Annals of Pure and Applied ‎‎Logic‎, ‎63‎, pp. ‎103-200.
‎‎Hajek‎, ‎P.,‎Pudlak‎, P. (1993).‎Metamathematics of First-order Arithmetic‎. Berlin: ‎Springer-Verlag.
Hodges‎, H. (1997). ‎A Shorter Model Theory‎. ‎Cambridge: ‎Cambridge University Press.
Kaye‎, R. (1991).‎Models of Peano Arithmetic‎. ‎Oxford: Oxford University Press.
‎Krajicek‎, J. (1995). Bounded Arithmetic‎, ‎Propositional Logic‎,‎and Complexity Theory. ‎Cambridge‎: ‎Cambridge University Press‎.
‎Krajicek‎, J. ,‎Pudlak‎, P., ‎‎Takeuti, G. (1991).‎Bounded Arithmetic and the Polynomial Hierarchy‎. ‎Annals of Pure and Applied Logic‎, ‎52‎, pp. ‎143-153.
‎Marker‎, D. (2002). Model Theory‎: ‎An Introduction‎. ‎New York: ‎Springer-Verlag.
Moniri‎, M‎. (2006). An independence result for intuitionistic bounded arithmetic. Journal of Logic and Computation, 16, pp. 199-204.
Moniri‎, M‎. (2007). ‎Preservation Theorems for Bounded Formulas. ‎Archive for Mathematical Logic‎, ‎46‎, pp. ‎9-14.
Parikh, R. J. (1971). Existence and feasibility in arithmetic, Journal of Symbolic Logic, 36, pp. 494–508.
Parikh, R. J. (1973). Some results on the lengths of proofs, Transactions of the American Mathematical Society, 177, pp. 29–36.
‎‎Zambella‎, D. (1996). Notes on Polynomially Bounded Arithmetic‎, ‎Journal of Symbolic Logic‎, ‎61‎, pp. ‎942-966.
Logical Studies
Volume 12, Issue 2
September 2021
Pages 193-211

Home

Guide for Authors

Submit Manuscript

Reviewers

Contact Us