It is well known that Heyting algebras constitute ‘the algebra of (propositional) intuitionistic logic’ in the same sense as Boolean algebras constitute the algebra of classical propositional logic. But there is an important difference: finitely-generated Boolean algebras are finite, and hence complete as ordered sets, which means that the addition of quantifiers to classical propositional logic adds no further complication to the algebraic structures needed to model the logic. In contrast, even the free Heyting algebra on one generator is infinite; and whilst it (and the free complete Heyting algebra on one generator) can be described explicitly, the free Heyting algebra on two generators is already insanely complicated (and the free complete Heyting algebra on two generators does not even exist). Thus, at first sight, any attempt to use the category of finitely-presented Heyting algebras as a tool for studying quantification in intuitionistic logic seems doomed to failure.
In this context, A. M. Pitts in 1991 proved a very surprising result. He showed that although finitely-presented Heyting algebras are not complete, in a categorical sense they nevertheless ‘think they are’: that is, for any such algebra \(H\) the embedding \(H\to H[x]\), where \(H[x]\) denotes the coproduct of \(H\) and the free algebra on one generator, has left and right adjoints, which can be used to interpret existential and universal quantifiers respectively. In more categorical terms, Pitts’s result says that the dual of the category of finitely-presented Heyting algebras is a Heyting category; model-theoretically, it says that the first-order theory of Heyting algebras admits a model completion.
These twin observations were the starting-point for the programme of research which has culminated in the present book. The combination of a model-theorist (Ghilardi) and a categorical logician (Zawadowski) has been enormously effective in uncovering the mysteries of which Pitts’s theorem gives us a first glimpse. Their first joint paper, published in 1995, showed how to explain Pitts’s result by means of an embedding of the dual of the category of finitely-presented Heyting algebras into a suitable topos: the embedding was constructed using a novel application of Ehrenfeucht-Fraïssé games, and the topos is the classifying topos of a theory which can be regarded as the ‘constructive model completion’ of the theory of Heyting algebras (though its properties are rather different from those of the classical model completion). Subsequently, they showed that the existence of all this unexpected structure on the category of Heyting algebras is no accident: many other varieties of algebras arising from logic, in particular those arising from certain modal logics, give rise to very similar structure.
The present book is a summary of the authors’ work so far, with enough of the background sketched in to make the whole corpus accessible to readers with an understanding of the basic concepts of category theory and model theory. (The word ‘sketched’ is deliberately chosen: although the authors provide an appendix containing all the necessary categorical notions, it is unlikely to be sufficient for those who have no previous experience of categorical methods.) Although much of the material is highly technical, the authors do a very good job of making it readable by those with the necessary background; the reviewer noticed a few proofreading lapses, but none that seem likely to be actively misleading.
The story is not over yet, as will be evident from a perusal of the brief chapter headed ‘Open Problems’; but it is remarkable how much has been achieved in a relatively short time. In the reviewer’s opinion, it is well worth the effort of mastering the undoubted technical difficulties involved in this striking fusion of ideas from category theory, model theory and nonclassical logic.