Introduction to higher order categorical logic. (English) Zbl 0596.03002

Lambek, J.; Scott, P. J.

Cambridge Studies in Advanced Mathematics, 7. Cambridge etc.: Cambridge University Press. IX, 293 p. £30.00; $ 49.50 (1986).

This is, first and foremost, an evangelizing book: its primary purpose is to convince the reader that its subject (higher-order categorical logic) exists. However, it is (paradoxically) only by failing to establish the truth of their most audacious claim for it that the authors succeed in this aim. Their view of the subject may be summarized crudely as follows: ”From the 1920s onwards, logicians have been developing the tools of \(\lambda\)-calculus, type theory and similar deductive systems, and for a rather shorter period category-theorists have studied cartesian closed categories, toposes and similar categories. The insight at the heart of categorical logic is that these two groups of people have really been talking about the same thing all along, in slightly different terminology.” But if it were literally true that the two lines of development were the same, categorical logic would have nothing to say to us; it would all have been said already by the logicians and/or the category-theorists. However, as the authors are honest enough to admit in their Preface, in their attempt ”to show that the logicians’ viewpoint is essentially equivalent to the categorists’ one, (they) have to slightly distort both”; and it is out of the creative tension (the dialectic, if you insist) between the two points of view which refuse to coincide exactly that categorical logic derives its strength and its substance.
What, then, does the book contain? It is divided into four (unequal) parts, numbered 0-3: Part 0 is a quick review of basic category theory, mostly quite conventional in style (except that it includes, for the first time in book form, A. Burroni’s proof that categories with finite limits are equational over directed graphs). It is in Part 1 that the effects of the distortion (and the interest of the subject) begin to appear: the authors introduce a notion of ”deductive system” which will be found slightly uncomfortable both by logicians (because it is not assumed to be freely generated by anything) and by category-theorists (because composition is not assumed to be associative), but which (the authors assert) forms a reasonable compromise between the traditions of the two schools. The major objective of this part is to set up the equivalence between typed \(\lambda\)-calculi and cartesian closed categories; this is handled carefully and in detail, with suitable attention paid to those categories (”C-monoids”) which correspond to untyped \(\lambda\)-calculi.
Part 2 similarly sets up the parallels between (higher-order intuitionistic) type theories and toposes. This is perhaps more familiar ground, having been carefully gone over by a number of people some ten years ago (notably by M. P. Fourman in the Handbook of Mathematical Logic). In comparison with these previous accounts, a salient (and, to most category-theorists, unwelcome) feature is the stress placed upon the notion of a topos with canonical subobjects; the need for this appears to arise from the authors’ curious reluctance to include either equalizers or pullbacks as part of the primitive structure of a topos. Having set up the correspondence, the authors apply it to derive results on the structure of various free toposes; Part 2 concludes with a brief discussion of P. Freyd’s ”sconing” technique (again, the first time this material has been presented in book form). Finally, the brief Part 3 discusses the representability of numerical functions in free cartesian closed categories and toposes. One can see the justification for postponing the discussion of recursive functions, which this part requires, until after the main results of the book have been established, but it does seem a little odd to separate the results on representability from their natural homes in Parts 1 and 2. However, their impact is not seriously diminished thereby.
The book is carefully written and (so far as this reviewer can tell) remarkably free from misprints. The slightly racy style (attributable, one suspects, to the first author) makes the book pleasant (though not, in view of its subject-matter, particularly easy) to read. Some professionals will doubtless feel that the authors have, from time to time, allowed their enthusiams for doing things in their own particular way to run away with them; but the average graduate student is far less likely to be irritated by this, and he will find that the book makes available to him a large body of material which was previously fairly inaccessible. Overall, the authors deserve our thanks for writing it.

Reviewer: P.T.Johnstone

MSC:

03-02	Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
18-02	Research exposition (monographs, survey articles) pertaining to category theory
03G30	Categorical logic, topoi
03F50	Metamathematics of constructive systems
03B40	Combinatory logic and lambda calculus
03B15	Higher-order logic; type theory (MSC2010)
18A15	Foundations, relations to logic and deductive systems
18B25	Topoi
18D15	Closed categories (closed monoidal and Cartesian closed categories, etc.)
18-01	Introductory exposition (textbooks, tutorial papers, etc.) pertaining to category theory
03-01	Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations

Keywords:

typed lambda calculus; higher-order intuitionistic type theory; cartesian closed categories; free toposes