Page 18 - Textos de Matemática Vol. 40

6 Introduction
Explicit mathematics with a restricted form of comprehension is studied in the Master thesis of Kra¨henbu¨hl, [Kr¨a06].
Research papers. The continuously growing research in this area makes it practically impossible to give a complete list of publications. In the following we refer to some key publications.
The roots of explicit mathematics are in the two papers of Feferman [Fef75, Fef79], already mentioned.
While the modern formulation of the applicative theories is given by Bee- son in his book [Bee85], the modern formulation of explicit mathematics, based on a naming relation, is due to Ja¨ger, [J¨ag88].
The two papers of Feferman and Ja¨ger [FJ93, FJ96] and the follow-ups by Glaß and Strahm [GS96], Marzetta and Strahm [MS98], and Strahm [Str00b] about applicative theories and explicit mathematics extended by the non-constructive μ operator, provide new techniques in the proof-theoretic treat- ment of such theories which nowadays are considered as standard techniques.
One obtains proof-theoretically very strong systems by adding a principle for monotone inductive definitions. After some work by Takahashi [Tak89], such theories were mainly investigated by Rathjen, cf. [Rat96, GRS97, Rat98a, Rat99a, Rat02]. In the context of intuitionistic logic they are studied by Tu- pailo in [Tup04]. These theories are mainly based on strong second order axioms and, therefore, somehow outside of the applicative realm (although, the difference between the non-uniform and uniform version of the axiom for mono- tone inductive definitions is crucial in this context).
While the original formulation of applicative theories is intuitionistic, nowa- days they are mainly studied based on classical logic. For results based on in- tuitionistic logic we can refer not only to the original articles of Feferman and the books of Beeson and Troelstra/van Dalen, but also to Gordeev [Gor88] and, more recently, to Tupailo [Tup01, Tup03, Tup04].
An interesting relation of explicit mathematics with Quine’s New Foun- dations is observed by Cantini, cf. [Can99].
Applicative theories characterizing classes of restricted computational com- plexity are studied by Cantini [Can00, Can05a] and Strahm [Str97, Str01, Str03, Str04].
References to the use of applicative theories in connection with functional and object-oriented programming were already given above.
Finally, we can refer to applications of explicit mathematics and, at one place also Frege structures, in linguistics by Hamm, van Lambalgen, and Kamp to model nominalizations [Ham99, HvL03, vLH05] or to construct models for discourse representation structures [HKvL06].