Foundations must be built on a sound layer of ballast. The edifice of mathematics rests on calculi of expressions composed of symbols written on paper or coded in a computer. To make a mathematical study of this edifice itself, or of the ways of handling expressions mechanically, we must consider the completed infinities of formulae, such as N. Since these completed infinities have no existence as objects in the real world, but only as characters in the drama of mathematics, this kind of study ( meta-mathematics) must be made within a pre-existing mathematical context. This is why we are doing it in Chapter VI and not Chapter I.
Mathematically, the algebras of formulae are free for certain free theories, whose operations are the connectives and proof rules of logic and type theory. In the category-theoretic tradition, a free algebra is the initial object in the category of all algebras. However, the very general nature of universal properties - the fact that this mode of description applies to so many other mathematical phenomena, as we have seen - means that this does not give a ``hands on'' appreciation of term algebras.
In formal languages, terms cannot be equal unless they have been built in the same way. Since they are put together with connectives such as +, Ù and $, they form an algebra, but, unlike the arithmetical examples which motivated Section 4.6, they can also be taken apart - parsed by analysis into cases. This leads to the techniques of structural recursion, which we have been using from the first page of this book, and unification, the subject of Section 6.5. We shall characterise, and thereby construct, the free algebras for free theories, by the property that the parsing operation is well defined and well founded, ie that it terminates (Section 6.3).
Section 6.4 specialises to tail recursion, which can be implemented more efficiently using imperative while programs. The interpretation in this case is described in terms of coequalisers, from the previous chapter.
The properties of term algebras also hold for infinitary operations. More careful consideration, indeed, shows that notions of induction are needed to capture finiteness, and not vice versa (Section 6.6).
The mathematisation of symbolism also gives us the means to create new mathematical worlds inside existing ones, for example in a model of set theory or in a topos of sheaves. In this book we have been careful to make clear which logical connectives are needed for each application, rather than rely globally on higher order logic: cartesian closed categories are used in functional programming, and pretoposes serve many of the purposes of universal algebra. Certain other structure is needed in the meta-logic to express or construct these features, so for example we might treat the l-calculus symbolically using algebraic tools. Category theory, unlike symbolic logic, is well adapted to the parallel treatment of different fragments, because it can both represent logical structure very naturally and also be represented in a clear combinatorial way.
Set theory tried to deal with both the internal and external structure, though it was particularly ill suited to universal algebra. The inductive hierarchy of sets, on which mathematics was allegedly founded, is defined using the quantifiers, and Lemma 6.3.12 shows that it also relies on the Pasting Lemma 5.8.9. Nevertheless, set theory does throw some light on induction: Section 6.3 uses category theory to generalise some of its ideas and apply them to new inductive situations.
One reason for the difficulty in understanding set-theoretic induction was that the ordinals, as traditionally presented, depend heavily on excluded middle. My original draft of this chapter contained material from set theory which was embarrassingly old fashioned. I tried to develop a simple intuitionistic account of the ordinals; such an account now exists in [ JM95], [Tay96a] and [Tay96b], and is summarised at the end of the chapter, though it is hardly simple. But the motivating problem was solved in the mean time in a more elementary way (Exercise 3.45 ).
The sections of this chapter depend very little on one another.