 Propositional functions of type \((\iota)\) are often called “first order”; hence the name “first order logic” for the familiar logic where the variables only range over arguments of first order functions. A monadic function of arguments of type \(\tau\) are of type \((\tau)\) and so functions of such functions are of type \(((\tau))\). “Second order logic” will have variables for the arguments of such functions (as well as variables for individuals). Binary relations between functions of type \(\tau\) are of type \((\tau,\tau)\), and so on, for relations of having more than 2 arguments. Mixed types are defined by the above. A relation between an individual and a proposition (such as “\(\hat{x}\) believes that \(\hat{P}\)”) will be of type \((\iota\),( )).