Every mathematician's toolbox contains tuples and subsets for making ideal elements, and proofs by induction. In this chapter we bring together the traditional techniques which form the received view of the foundations of twentieth century mathematics. Afterwards they will be dismantled and reconsidered in the light of later algebraic experience.
At the beginning of his career, Georg Cantor investigated sets of points of discontinuity which functions could have whilst still admitting Fourier representations. He also gave a construction of the real numbers from the rationals, and showed that there are a lot more reals than rationals (Hermann Weyl later reproached analysts for decomposing the continuum into single points). Cantor was led to considering abstract sets, forming hierarchies under constructions such as the set of all subsets.
There are historical parallels between mathematics and programming in the development of types. Cantor was concerned with the magnitudes of sets, whereas FORTRAN distinguished between integer and real data types because they have different storage requirements. (Linear logic shows that resource analysis continues to be a fruitful idea.) Both started from the integers and real numbers alone. Bertrand Russell formulated his theory of types as a way of avoiding the vicious circles which he saw as the root of the paradoxes of set theory. On the other hand, the one lesson which the software industry has learned from informatics is that the type discipline catches a very large proportion of errors and thereby makes programs more reliable. Early calculi provided a static universe in advance, but modern type theories and programming languages create new types dynamically from old ones.
What is an abstract set? Some accounts of set theory claim that it is a voluntary conspiracy of its elements, coming together arbitrarily from independent sources (the inductive conception). But this conflicts with mathematical practice, and has little backing even in philosophical tradition. Plato held that members of a class are images of a Form; in practice, we conceive of the Form and certain of its instances first. The totality is only a semantic afterthought (and the instances are usually not themselves Forms). Indeed, from Zeno's time, points in geometry lay on lines but did not constitute them.
Gottlob Frege defined sets by comprehension of predicates, which at first he allowed to take anything as their subjects. Russell's famous {x|x Ï x} showed that things couldn't be done quite so naively , so instead we select the elements from an already given ambient set.
For us, types are not imposed afterwards to constrain the size of the world, but are a precondition of meaning. In elementary trigonometry sin is thought of as applying to angles only, which are only reduced to real numbers by choosing a unit of measurement. Physical quantities may only be added or tested for equality if they measure the same thing (length, mass, energy, electric charge, etc ) in the same units; sometimes laws of mechanics can be guessed by this dimensional analysis alone, or from a scale model which preserves the dimensionless part (such as the Reynolds number in fluid mechanics).
More complex types are formed by processes, such as the powerset, like those generating terms and logical formulae. The establishment of certain standard abstract methods of construction made it possible to state and prove results of a generality that would not have been considered in the nineteenth century. As Michael Barr [BW85, p. 88] put it, ``The idea of constructing a quotient space without having to have the ambient space including it, for example, was made possible by the introduction of set theory, in particular by the advent of the rather dubious idea that a set can be an element of another set. There is probably nothing in the introduction of topos theory as foundations more radical than that.''
On the other hand, the importance of the quotient operation is such that it should perhaps be taken as primitive instead. Modern type theory builds hierarchies as Cantor and Zermelo did, but using simpler ways of forming types, such as the product, sum and set of functions. These correspond very directly to conjunction, disjunction and implication of propositions, an analogy which will be an important guiding principle for the rest of the book. We shall find that the structure of the types is characterised, not by their set-theoretic incarnations, but by certain operations, such as projection and evaluation maps, which build terms of that type and take them apart. In particular the l-calculus handles the terms arising from the function-type.
The second half of the chapter is devoted to induction and recursion. Sections 2.5-2.6 discuss well founded relations, a notion of induction which also comes from the set-theoretic tradition, but we shall motivate it instead from the problem of proving correctness and termination of a wide class of recursive programs. There are classical idioms of induction based on minimal counterexamples and descending sequences, but we shall show how they can often be made intuitionistic. More complicated inductive arguments can be justified by constructing recursion measures using lexicographic products and other methods.
For programming (and foundations), structural recursion over lists, trees and languages is more important. In Section 2.7 we treat lists and Peano induction over the natural numbers in a similar fashion to the function-type. The last section treats second and higher order logic.