ABSTRACT
The types and the syntax of first order logic are mismatched in several ways. There are constants and variables of type 1 and of type [], but only type 1 variables can be quantified. There are constants of type [P] for any n > 1, and a single constant 3 of type [[1]], but there are no variables of these types. Further if the variables of these types are to be quantified, the constant 3 will have to also be of any type [[l72]] and of type [[[1]]]. But no matter what type of predicate is admitted, it is possible to consider a higher type predicate of predicates of the given type. The logic Type Theory, abbreviated TT, is a logic with all such possible types.
