Generalized sketches as a framework for completeness theorems. Part I

AbstractThe concept of sketch is generalized. Morphisms of finite (generalized) sketches are used as sketch-entailments. A semantics and a deductive calculus of sketch-entailments are developed. A General Completeness Theorem (GCT) shows that the deductive calculus is adequate for the semantics. In each of a number of categories of sketches, a particular set of sketch-entailments is singled out as a set of axioms used to specify a particular kind of structured category. The specification yields an adequate proof-system to derive sketch-entailments valid in structured categories of the given kind. Classical, Tarski-type semantics is related to the sketch-semantics of the paper. Specific completeness theorems are given in the sketch-based formalism, and they are related to representation theorems of categorical logic, and known completeness theorems of logic