 It is a higher-order logic. Even though type logic was already an established logical framework in those days, linguists, philosophers and mathematicians were more familiar with first order logic (the logic in which there are only variables for basic entities). Since in Montague semantics the parts of expressions must have meaning too, a higher order logic was needed (we have already seen that every man denotes a set of properties).