Page 69 - Textos de Matemática Vol. 40
P. 69

Chapter 2
Explicit Mathematics
2.1 Explicit mathematics
Explicit mathematics has been introduced in Feferman [Fef75] as a framework for Bishop-style constructive mathematics. Explicit mathematics extends ap- plicative theories by a second order part which allows the introduction of types. Although types in explicit mathematics may form rather complicated collections of objects, they are represented by an operation of the underlying applicative universe. In this respect, Ja¨ger [J¨ag88] has provided a very perspicuous for- mulation using a naming relation between objects and types. Therefore, the theories of explicit mathematics are also called theories of types and names.
2.1.1 The theory EETJ.
The language. Theories of types and names are formulated in the second order
language LEM for individuals and types. It extends Lp by
• type variables S, T, U, V, W, X, Y, Z, . . . (possibly with subscripts),
• generators which are special individual constants, namely nat (natural numbers), id (identity), co (complement), int (intersection), dom (domain), inv (inverse image) and j (join),
• binary relation symbols ∈ (membership) and R (naming or representa- tion).
Later on, we will consider extensions of EETJ which contain in addition the two generators:
• i (inductive generation) and • l (universe generator).
57


































































































   67   68   69   70   71