Page 13 - Textos de Matemática Vol. 40

Introduction
The purpose of this Habilitationsschrift is to provide different applicative the- ories and related systems and to investigate them from a metamathematical point of view. Applicative theories form the first order part of systems of explicit mathematics which were introduced by Solomon Feferman in [Fef75, Fef79] in order to give a logical account to Bishop-style constructive mathematics. These theories provide a formal framework, of strong expressive power, which may be used to study properties of mathematical concepts as they appear in computer science and in the mathematical practice. Here, “expressive power” is not meant in the sense of mathematical strength (which is provided, for instance, by extensions of Zermelo-Fraenkel set theory), but in the sense of syntactical expressiveness.
Within mathematics, there are three major formal frameworks in use: Peano arithmetic, second-order analysis, and Zermelo-Fraenkel set theory. All of them have been proven highly successful in the formalization of (parts of) mathematics. However, while they are absolutely adequate with respect to their original purposes, they show some technical limitations if applied, for instance, to “new” concepts as used in computer science. We would like to mention three of these limitations, which applicative theories overcome: 1) the—at least, implicitly—typed languages; 2) the restriction to a single datatype as in Peano arithmetic; and 3) the problem of partiality which is not directly expressible in the usual mathematical language.
Typed vs. untyped languages. Formalizing a certain domain of entities, one has in principle two possibilities: On the one hand, we may restrict— somehow from the outside—the language in a way that certain terms belong automatically to the domain in question provided that they are well-formed. On the other hand, we may leave the language unrestricted, but then we need afterwards a formal mechanism to ensure that a particular term belongs to the desired domain. The former method may be implemented, for instance, by use of a typed language. In contrast, the latter one, might use an untyped language. In this case, one needs a predicate (or more generally, a formula) to express that a term belongs to the domain, and the fact, that a term indeed belongs to the domain, has to be proven afterwards. The assets and drawbacks of these two approaches are well-known in computer science, and we do not have to repeat
1