A Description of Automath and Some Aspects of its Language Theory
D.R. van Daalen · Studies in logic and the foundations of mathematics · 1994
This note presents a self-contained introduction into Automath, a formal definition and an overview of the language theory. Thus it can serve as an introduction to the papers [van Benthem Jutting 73] and [ Zandleven 73 (E.1) ]. Among the various Automath languages this paper concentrates on the original version AUT-68 (because of its relative simplicity) and one extension AUT-QE (in which most texts have been written thus far). The contents are: 1 Introductory remarks. 2 Informal description of AUT-68. 3 Mathematics in Automath: propositions and types. 4 Extension of AUT-68 to AUT-QE. 5 A formal definition of AUT-QE. 6 Some remarks on language theory.