Eindhoven, 11 March 1996.
Dear Florian,
In your email of 7 March you inquire about formalism
that can handle theories and complex notions, like the
notion "group".
This is something we felt the need for in the Automath
project in the middle seventies. The name invented for the
notion was "telescope". A telescope is a sequence of typed
abstactors, where in each abstractors the type
can depend on the variables introduced by the preceding
abstractors of the sequence. The name "telescope" was chosen
since the old-fashioned optical telescope used to be built
as a sequence of segments sliding into one another.
J. Zucker used telescopes on a large scale when writing
an introduction into analysis in his own version of
Automath. Unfortunately this work remained unimplemented
and unpublished because of the lack of finatial support in
those days. A short description can be found in Zucker's paper
J. Zucker,
Formalization of classical mathematics in AUTOMATH,
Colloque International de Logique, Clermont-Ferrand,
In: Colloques Internationaux du Centre National de la
Recherche Scientifique, 249, (July 1975) pp 135-145.
My own work on telescopes was published much later:
N.G. de Bruijn. Telescopic mappings in typed lambda calculus.
Information and Computation, vol 91, 189-204 (1991).
In order to see the subject of this paper one might think
of an operator that attaches a ring to every abelian group.
It is a kind of mapping from the telescope "abelian group"
to the telescope "ring". The paper shows that such mappings
can be treated by a calculus that copies the lambda
calculus on a higher level, again with both abstraction and
application, very similar to what we have with ordinary
functions. For the connection with Zucker see p. 192 of
this paper.
For extensive information on the Automath project, see:
Selected Papers on Automath,
edited by R.P. Nederpelt, J.H. Geuvers and R.C. de Vrijer,
Studies in Logic, vol. 133, North-Holland 1994.
Yours sincerely, N.G. de Bruijn
Eindhoven University of Technology,
Department of Mathematics and Computing Science,
PO Box 513, Eindhoven, The Netherlands.