Automath Type Inclusion in Barendregt’s Cube

The introduction of a general definition of function was key to Frege’s formalisation of logic. Self-application of functions was at the heart of Russell’s paradox. Russell introduced type theory to control the application of functions and avoid the paradox. Since, different type systems have been introduced, each allowing different functional power. Most of these systems use the two binders λ and Π to distinguish between functions and types, and allow β-reduction but not Π-reduction. That is, (Formula Presented.) is only allowed when π is λ but not when it is Π. Since Π-reduction is not allowed, these systems cannot allow unreduced typing. Hence types do not have the same instantiation right as functions. In particular, when b has type B, the type of (Formula Presented.) is immediately given as B[x := C] instead of keeping it as (λ_x:A.B)C to be Π-reduced to B[x := C] later. Extensions of modern type systems with both β- and Π-reduction and unreduced typing have appeared in [11,12] and lead naturally to unifying the λ and Π abstractions [9,10]. The Automath system combined the unification of binders λ and Π with β- and Π-reduction together with a type inclusion rule that allows the different expressions that define the same term to share the same type. In this paper we extend the cube of 8 influential type systems [3] with the Automath notion of type inclusion [5] and study its properties.