Generalized sketches as a framework for completeness theorems. I-III (Q674480)

Although this paper has appeared in serial form to suit the convenience of the journal, it is really a connected whole and must be reviewed as such. The first part contains a spacious Introduction to the whole, as well as a bibliography for all three parts; the other two lack these features. The work is founded on a substantial generalization of Ehresmann's notion of a sketch, the basic idea being that, in addition to specifying certain particular diagrams which are intended to become limit or colimit diagrams in the models of the sketch, we are allowed to specify other diagrams with particular `qualities' which translate into universal properties in the categories where the sketch is modelled: a simple example would be the quality of `being an exponential'. Similar generalizations have been considered by other authors, including C. Lair and C. Wells. However, a novel feature of the present approach is the use of the category of sketches itself as a vehicle for specifying `axioms' which the sketches in a particular doctrine (and the categories in which they are to be modelled) are required to satisfy. Within this context the author develops a syntactic calculus and proves that it provides a sound and complete formalization of sketch-semantics as generalized here. Whilst the paper is not easy reading (on account of its length and the number of new concepts introduced, not because of any lack of clarity in the exposition), it does (in the reviewer's opinion) go a long way to substantiate the author's claim that `categorical logic is, to a great degree, autonomous, even in matters syntactical'.