Name Induction in Explicit Mathematics

Reinhard Kahle

Systems of explicit mathematics were introduced by Feferman in the seventies [1, 2]. Using Jäger’s naming relation [3], the theories can be presented as a theory of types and names. Adding a natural induction principle for names to (meta-)predicative theories of types and name, we get, in a very uniform way, impredicate theories. From this point of view, name induction serves as an alternative for the principle of inductive generation, [4]. Moreover, it allows us the definition of a natural theory of explicit mathematics with the strength of the theory of inductive definitions ID_{1}, [5]. The presented work grows out of the close collaboration with Gerhard Jäger and Thomas Studer (IAM, Universität Bern).

[1] Solomon Feferman, A language and axioms for explicit mathematics, Algebra and logic (J. Crossley, editor), Lecture Notes in Mathematics, vol. 450, Springer, Berlin, 1975, pp. 87–139.

[2] Solomon Feferman, Constructive theories of functions and classes, Logic Colloquium 78 (M. Boffa, D. van Dalen & K. McAloon, editors), North–Holland, Amsterdam, 1979, pp.159–224.

[3] Gerhard Jäger, Induction in the elementary theory of types and names, CSL ’87 (E. Börger et. al., editor), Lecture Notes in Computer Sciences, vol. 329, Springer, Berlin, 1988, pp.118–128.

[4] Gerhard Jäger, Reinhard Kahle & Thomas Studer, Universes in explicit mathematics, Submitted.

[5] Reinhard Kahle & Thomas Studer A theory of explicit mathematics equivalent to ID_{1}, Submitted.

Address: WSI, Universität Tübingen, Sand 13, D-72076 Tübingen, Germany

E-mail: kahle@informatik.uni-tuebingen.de