Impredicative Overloading in Explicit Mathematics

Thomas Studer

Castagna, Ghelli and Longo [1] provide a theoretical foundation for object-oriented programming via λ-calculi with overloading. However, their full calculus exposes a new form of impredicativity for which no denotational semantics was available.

In this talk we introduce the system OTN of explicit mathematics based on elementary separation, product, join and weak power types. In such theories types are represented by names, and these are first order values. Hence they can be used in computations which is the key to model overloading. We present a set-theoretical model for OTN, and we develop in OTN a theory of impredicative overloading. Together this yields a solution to the problem of impredicativity mentioned above.

The use of power types in explicit mathematics has always been doubted. Glass [2] showed that weak power types add nothing to the proof-theoretic strength of various systems of explicit mathematics without join, and Jäger[3] proved the inconsistency of strong power types with elementary comprehension. Our work also provides a first example of an application of power types in explicit mathematics.

[1] Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions with subtyping. Information and Computation, 117(1):115–135, 1995.

[2] Thomas Glass. On power set in explicit mathematics. The Journal of Symbolic Logic, 61(2):468–489, 1996.

[3] Gerhard Jäger. Power types in explicit mathematics? The Journal of Symbolic Logic, 62(4):1142– 1146, 1997.

Address: Institut für Informatik und angewandte Mathematik, Universität Bern, Neubrückstr. 10, CH-3012 Bern, Switzerland

E-mail: tstuder@iam.unibe.ch