 Gödel considers the quantifier free theory of these functionals of finite type, denoted by T. T has the following features: the language of T contains variables of each type, constants for distinguished types, and a ternary predicate =σ for equality for type σ. Equality between terms of the same type is decidable. The non-logical axioms and rules for T include the classical arithmetic axioms for 0 and successor, and the induction rule: