From: cfw2@po.CWRU.Edu (Charles F. Wells)
Newsgroups: sci.math
Subject: Graph based logic and sketches (abstract)
Date: 9 Oct 1992 16:19:48 GMT
Organization: Case Western Reserve University, Cleveland, Ohio (USA)
NNTP-Posting-Host: slc12.ins.cwru.edu


             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

Newsgroups: sci.math,sci.math.num-analysis,sci.math.stat,sci.math.symbolic