This installment of the notes is no longer used in the course. Originally it was used as a precursor to the section on natural language syntax and semantics. However, it was later realized that one could teach Montague grammar directly by assuming an intuitive understanding of lambda notation for functions. Most computer science graduate students understand lambda notation for functions. However, the basics of higher order logic, and in particular the emphasis on lambda as the only binding construct, is useful in the construction of automated reasoning and formal verification systems. Hence the notes on higher order logic seem worth preserving.
Node by David McAllester