Functions

Abstract

We start our overview of the basic axioms and inference of higher-order logic by studying the rules for reasoning about functions. These are essentially the rules of simply typed lambda calculus. A method of extending the logic by defining new constants is described. In association with this we also describe two ways of introducing new notation without extending the logic: abbreviations (syntactic sugaring) and local definitions. Furthermore, we consider an important practical issue: how to present proofs in a simple and readable way. The natural deduction style is the traditional way of presenting proofs and is the one that we have described in Chapter 3. However, we prefer an alternative derivational proof style, because we find it more readable and it scales up better to large proofs. The natural deduction style and the derivational proof style are just two different ways of writing proofs; the underlying notion of a proof is the same in both styles. Finally, we postulate a new type constructor that denotes a Cartesian product and investigate its basic properties.