GRAPH-BASED LOGIC AND SKETCHES II: FINITE-PRODUCT

CATEGORIES AND EQUATIONAL LOGIC (PRELIMINARY REPORT)

ATISH BAGCHI CHARLES WELLS

Abstract. It is shown that the proof theory for sketches and forms provided in Part I of this paper (see http://www.cwru.edu/1/class/mans/math/pub/wells) is strong enough to produce all the theorems of the entailment system for multisorted equational logic provided in Goguen and Meseguer’s article “Completeness of manysorted equational logic” (Technical Report CSL-135, SRI International Computer Science Laboratory, 333 Ravenswood Ave., Menlo Park, CA 94025, USA, 1982).