Graph-based Logic and Sketches Atish Bagchi and Charles Wells October 9, 1992 Extended Abstract Traditional treatments of formal logic provide: 1. A syntax for formulas. The formulas are typically defined recursively by a production system (grammar). 2. An inference relation between sets of formulas. This may be given by structural induction on the syntax for the formulas. 3. A rule for assigning meaning to formulas (semantics) that is sound with respect to the inference relation. The semantics may also be given by structural induction on the syntax of the formulas. First order logic, the logic and semantics of programming languages, and the languages that have been formulated for various kinds of categories are all commonly described in this way. The formulas in those logics are strings of symbols that are ultimately modeled on the sentences mathematicians speak and write when proving theorems. Mathematicians with a categorial orientation frequently state and prove theorems using graphs and diagrams (which may be described as graphs labeled coherently by data from some category). The graph, diagrams, cones and other data of a sketch are formal objects that correspond to the graphs and diagrams used by such mathematicians in much the same way as the formulas of traditional logic correspond to the sentences mathematicians use in proofs. The functorial semantics of sketches is sound in the informal sense that it preserves (usually by definition!) the structures given in the sketch. The analogy to traditional model theory is close enough that sketches and their models fit the definition of "institution" (Goguen and Burstall [2]), which is an abstraction of model theory. The content of this paper is to exhibit the structure in sketch theory that corresponds to items 1 and 2 in the description of logic (the deductive structure) and to provide a detailed translation of a particular logic between the string-based version and the sketch-based version. This work is parametrized by the type of categorial theory being considered. We assume given a finite-limit (projective) sketch E of a particular type of category as in [5] or [7]. E presents the type of category as essentially algebraic over the theory of categories. E -categories are then the models of E in Set. The kinds of categories that can be described in this way include categories with finite products, categories with limits or colimits over any particular set of diagrams, cartesian closed categories, regular categories, toposes, and many others. A formula in this setting is a potential factorization (PF) through a subobject of the codomain: formally, a pair consisting of an arrow of E and a subobject of the codomain of the arrow. We will refer to the codomain of the arrow as the codomain of the PF, and the subobject as the "claim" of the PF. Roughly, the PF is "true" if its arrow factors through its claim. Sentences are PF's whose arrows have domain 1. We provide a general recursive construction of the objects and arrows of E (hence of the PF's in particular) which is derived from the similar recursive construction for initial algebras of FLS sketches given by Barr and the second author in [8]. Our thesis is that this recursive definition constitutes the rules of inference corresponding to item 2 above. An E-sketch is a sketch that allows the specification of any kind of construction that can be made in an E-category. This greatly enhances the expressive power of sketches when compared to Ehresmann's original definition. An E-sketch is a global element adjoined freely to E ([5] and [7]). The codomain of this adjoined arrow may be perceived as a description of the graph, diagrams and other constructions of the sketch. Adjoining such an arrow constitutes the axioms of a theory, and the factorization of arrows through subobjects in the polynomial category E[s] obtained by adjoining such an arrow constitute the formulas and sentences that can be inferred from the sketch. The resulting system of inference is sound with respect to models. This type of logic fits some of the abstractions of logic that have been given, such as that of Meseguer in [4] and the formulation in terms of closures given by Tarski [6]. As a kind of worked example, the paper will also contain a detailed description of the relationship between finite-product sketches and multisorted equational logic as given by Goguen and Meseguer [3]. It is intended that this translation be sufficiently algorithmic as to be implementable, for example in Mathematica. The equations of equational logic will be seen to correspond to a specific subset of the set of PF's; indeed, in the classifying topos of E, there is a specific object and subobject that is the common codomain and claim of the all the PF's. We will give explicit proofs of the correctness of the rules of inference given by Goguen and Meseguer in terms of the deductive system described above (the recursive construction of E). References [1]M. Barr and C. Wells, Category theory for computing science. Prentice-Hall International (1990). [2]J. A. Goguen and R. M. Burstall, A study in the foundations of programming methodology: specifications, institutions, charters and parchments. In D. Pitt et al., eds., Category Theory and Computer Programming. Lecture Notes in Computer Science 240, Springer-Verlag (1986), 313-333. [3]J. A. Goguen and J. Meseguer, Completeness of many-sorted equational logic. Technical Report CSL-135, SRI International Computer Science Laboratory, 333 Ravenswood Ave., Menlo Park, CA 94025, USA (1982). [4]J. Meseguer, General Logics. Report SRI-CSL-89-5, SRI International, Computer Science Laboratory, 333 Ravenswood Ave., Menlo Park, CA 94025, USA (1989). [5]A. J. Power and C. Wells, A formalism for the specification of essentially-algebraic structures in 2-categories. Mathematical Structures in Computer Science 2 (1992), 1-28. [6]A. Tarski, On some fundamental concepts of metamathematics. In Logic, Semantics, Metamathematics, Oxford University Press, 1956. [7]C. Wells, A generalization of the concept of sketch. Theoretical Computer Science 70 (1990), 159-178. [8]C. Wells and Michael Barr, The formal description of data types using sketches. In M. Main, A. MElton, M. Mislove and D. Schmidt, editors, Mathematical Foundations of Programming Language Semantics, Springer Lecture Notes in Computer Science 298. Springer-Verlag, 1988. Atish Bagchi Department of Mathematics Case Western Reserve University University Circle Cleveland, OH 44106-7058, USA axb35@po.cwru.edu Charles Wells Department of Mathematics Case Western Reserve University University Circle Cleveland, OH 44106-7058, USA cfw2@po.cwru.edu ==============================================================================