Page 15 - Textos de Matemática Vol. 40

Introduction 3
several other approaches which use applicative theories or related systems in con- nection with functional programming, cf. e.g., Feferman [Fef90, Fef91a, Fef92], Hayashi and Nakano [HN88], Kahle [Kah92], Sta¨rk [St¨a97, St¨a98, St¨a05], Talcott [Tal92], Tatsuta [Tat91, Tat98], and Turner [Tur91, Tur96]. More recently, Studer used this framework to study object-oriented programming, see [Stu01c, Stu01a, Stu01b, Stu05].
In the metamathematical investigations we focus on proof-theoretic strength and syntactic expressiveness. Applicative theories and explicit mathematics play an important role in mathematical proof theory. This started with the use of Feferman’s theory T0 in the proof-theoretic analysis of the theory (∆12-CA) + (BI) which was, for a long time, the strongest subsystem of anal- ysis accessible to an ordinal analysis, cf. Section 2.3.2. Nowadays, applicative theories and explicit mathematics can provide theories for almost the complete proof-theoretic spectrum accessible to an ordinal analysis. Another example is the relation to theories with ordinals. These theories, introduced by Ja¨ger, cf. [J¨ag93, JS95a], add an extra ordinal structure to given theories like Peano arith- metic without extra costs in terms of proof-theoretic strength. Such theories are very useful in the analysis of applicative theories and explicit mathematics, cf. [FJ93, JS95a, JS95b, FJ96, GS96, JS96, MS98, FS00, Str00b]. We will use such theories here for the study of truth theories, cf. Section 3.1.4.
Applicative theories also played an important role in the introduction of metapredicative proof-theory. Metapredicative theories distinguish them- selves by exceeding the proof-theoretic strength of predicativity, but the proof- theoretic analysis does not require tools of impredicative proof theory, like col- lapsing, cf. [J¨ag05]. In fact, the theories presented in Section 3.4 were among the first metapredicative theories, and they have been the reason for the proof- theoretic analysis of IDα in [JKSS99]. Since then, metapredicativity became a flourishing branch of proof theory, cf. e.g., [JKSS99, Set99, Str00a, JS01, J¨ag05]. In particular, the concept of superuniverse in Martin-L¨of’s type theory, inves- tigated by Rathjen [Rat00, Rat01], and metapredicative versions of explicit mathematics with universes are closely related to our approach. The latter ones have been studied by Strahm [Str99] and, in fact, his work and the work presented here were discussed in parallel and have profited from each other. Metapredicative subsystems of analysis are studied, for instance, in the PhD thesis of Ru¨ede [Ru¨e00], see also [Ru¨e02, Ru¨e03a, Ru¨e03b]. For a study of metapredicative set theories see Thiel [Thi03].
Contents
Now, we give a brief review of the content of this work.
In the first Chapter we present applicative theories. Applicative theories
are untyped first order theories, whose logic is partial, and which are based on combinatory logic. Additional structure may be added axiomatically. We outline the basic properties of these theories, including a discussion of their