Page 16 - Textos de Matemática Vol. 40

4 Introduction
models. As extensions we discuss the research on quantification operators and combinatorial properties based on the axiom of N strictness. In a case study we show, as a special application in computer science, how least fixed points can be formalized in an applicative theory.
The second Chapter contains a discussion of some theories in explicit math- ematics. Explicit mathematics extends applicative theories by a second order structure for types. By use of a naming relation we can associate individual terms as names to types, which serve as intensional objects to represent ex- tensional types—heuristically, these terms may be considered, for instance, as characteristic functions of the types. With this link between the second and first order level of explicit mathematics, we may use the full machinery of applica- tive theories to work with the names and to prove, for instance, the existence of certain types. In this work we focus on certain concepts—name induction and universes given by a uniform limit axiom—which are based on the applicative ground structure.
In the third Chapter we discuss truth theories over applicative theories— also called Frege structures—, which provide, as first order theories, a very elegant alternative to standard truth theories. In particular, they dispense with the arithmetization of the underlying language. It turns out that these truth theories have a special syntactical expressive power since they are not only proof- theoretically equivalent to certain fixed point theories, but allow syntactical embeddings of them.
In the appendix we provide a historical note on self-application—a concept incorporated in applicative theories.
Literature
Here we give a short review of the relevant literature in the field of applicative theories. This includes also literature about explicit mathematics, which is, due to the naming relation, often directly tied to the applicative basis. Let us start with the two first papers of Feferman, [Fef75, Fef79]. They already contain a good part of the basic results about applicative theories.
Books. The main reference is still the monograph of Beeson [Bee85]. It contains the first definition of applicative theories based on the logic of partial terms. Together with a comprehensive presentation of results and models of applicative theories, it discusses the relation to other constructive approaches, from a technical as well as from a philosophical point of view.
The book [Can96], of Cantini, deals with truth theories over (total) ap- plicative theories. It is based on an earlier monograph of the same author in Italian, [Can83], and it can be taken as the basis of the results given in the third Chapter of this work.
Hayashi and Nakano present in [HN88] an experimental implementation for extracting programs from constructive proofs in an explicit mathematics setting. Unfortunately, this line of investigation was discontinued.