The language theory of Automath : Chapter VIII, 1 and 2 (AUT-II)

There are two languages of the Automath family that have been developed for practical (in contrast with, say, language theoretical) purposes and have actually been applied in extensive formalization projects. On the one hand there is AUT-QE, used by L.S. van Benthem Jutting in his Landau translation [van Benthem Jutting ‘77]. The latter reference also contains an informal introduction to the language [van Daalen 73 (A.3)]. The theory of AUT-QE is to be found in [van Daalen 80, Ch. IV to VI] [large parts of which are included in this Volume]. On the other hand there is AUT-il, invented by J. Zucker, and employed by Zucker and A. Kornaat for the formalization of classical analysis and some related topics. In [Zucker 77 (A.4)] one finds a short account of both the language and the formalization project. This chapter is devoted to the theory of AUT-il, which is not quite as complete as the theory of AUT-QE. Some work remains to be done, notably on the extensional version of the language (see [C.5, VIII.6]).