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

DOI10.1016/S0022-4049(96)00007-2MaRDI QIDQ674480zbMATH OpenFDO

Publication date 24 April 1997

Published in Journal of Pure and Applied Algebra (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0022-4049(96)00007-2

category of sketches models of sketches sketch-semantics syntactic calculus

Model theory (03C99) Proof theory and constructive mathematics (03F99) Categorical logic, topoi (03G30) Theories (e.g., algebraic theories), structure, and semantics (18C10)

Review text

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'.

Recommendations

Cites work

Cited in

(22)

This page was built for publication: Generalized sketches as a framework for completeness theorems. I-III

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q674480)