Bounded Applicative Theories

Thomas Strahm

Theories with self-application form the operational core of systems of explicit mathematics, which have been introduced by Feferman in [3]. In an applicative universe of discourse, all objects may be thought of as operations or rules, which can freely be applied to each other: self-application is meaningful, though not necessarily total. It has turned out that applicative theories provide a natural framework for studying notions of abstract computability, especially from a proof-theoretic perspective, cf. [4] for a recent survey.

This contribution is concerned with the study of (unramified) bounded applicative systems which have a strong relationship to classes of computational complexity. We provide new applicative theories whose provably total functions coincide with the functions computable in polynomial time, polynomial space, polynomial time and linear space, as well as linear space. Our theories can be seen as natural applicative analogues of systems of bounded arithmetic, cf. Buss’ monograph [1]. We are also interested in higher type aspects of our systems; in particular, it is shown that Cook and Urquhart’s system PV^{ω} (cf. [2]) is directly contained in a natural applicative theory of polynomial strength.

[1] Buss, S. R. Bounded Arithmetic. Bibliopolis, Napoli, 1986.

[2] Cook, S. A., and Urquhart, A. Functional interpretations of feasibly constructive arithmetic. Annals of Pure and Applied Logic 63, 2 (1993), 103–200.

[3] Feferman, S. A language and axioms for explicit mathematics. In Algebra and Logic, J. Crossley, Ed., vol. 450 of Lecture Notes in Mathematics. Springer, Berlin, 1975, pp. 87–139.

[4] Jäger, G., Kahle, R., and Strahm, T. On applicative theories. In Logic and Foundations of Mathematics, A. Cantini, E. Casari, and P. Minari, Eds. Kluwer, 1999, pp. 83–92.

Address: Institut für Informatik und angewandte Mathematik, University of Bern, Neubrückstr. 10, CH-3012 Bern, Switzerland

E-mail: strahm@iam.unibe.ch