Graph-based Logic and Sketches I: The General Framework

Atish Bagchi^{∗} and Charles Wells

October 12, 1994

1 Introduction

Sketches as a method of specification of mathematical structures are an alternative to the string-based specification employed in mathematical logic. Sketch theory has been criticized as being lacunary when contrasted with logic because it apparently has nothing corresponding to proof theory. This article describes an approach to associating a proof-theoretic structure with a sketch. It is written in an innovative style using some of the ideas for presenting mathematics outlined in [Bagchi and Wells, 1993b].

1.1 Prerequisites

This article requires familiarity with the basic notions of mathematical logic as in Chapters 2 through 5 of [Ebbinghaus et al., 1984], and with category theory and sketches as in Chapters 1 through 10 of [Barr and Wells, 1990]. We specifically presuppose that finite-limit sketches are known. Some notation for these ideas is established in Section 4.

∗The first author is grateful to the Mathematical Sciences Research Institute for providing the opportunity to work on this paper there. Research at MSRI is supported in part by NSF grant #DMS-9022140.

1.2 Rationale

Traditional treatments of formal logic provide:

1. A syntax for formulas. The formulas are typically defined recursively by a production system (grammar).

2. Inference relations between sets of formulas. This may be given by structural induction on the construction of the formulas.

3. Rules for assigning meaning to formulas (semantics) that are sound with respect to the inference relation. The semantics may also be given by structural induction on the construction 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 category-theoretic point of view frequently state and prove theorems using graphs and diagrams. The graphs, 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 by definition the structures given in the sketch. The analogy to the semantics of traditional model theory is close enough that sketches and their models fit the definition of “institution” ([Goguen and Burstall, 1986]), which is an abstract notion of a logical system having syntactic and semantic components. This is described in detail in [Barr and Wells, 1990], Section 10.3. Note that the soundness of functorial semantics appears trivial when contrasted with the inductive proofs of soundness that occur in string-based logic because the semantics functor is not defined recursively.

1.3 Overview

This paper exhibits a structure in sketch theory that corresponds to items 1 and 2 in the description of logic in Section 1.2. The data making up the structure we give do not correspond in any simple way to the data involved in items 1 and 2 of traditional logic; we will discuss the differences in situ.

The data in this structure are parametrized by the type of categorial theory being considered. Let E denote a finite-limit sketch that presents a type of category as essentially algebraic over the theory of categories. Let E denote the finite-limit theory generated by E. E-categories are then the models of E in the category of sets. (This is described in Section 5.) 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. Sketches for several specific instances of E are given in Appendix B.

An E-sketch S (defined in Section 5.3.1 below) is a sketch that allows the specification of any kind of construction that can be made in an Ecategory. As an example, let CCC be a finite-limit theory for Cartesian closed categories. It is possible to require that a certain object in a CCC-sketch be the function space A^{B} of two other objects A and B of the sketch. This generalization greatly enhances the expressive power of sketches as originally defined by Ehresmann (in which only limits and colimits can be specified).

Such an E-sketch is described in Section 5.3.1 as a formally adjoined global element of the limit vertex of a certain diagram in E. This diagram forces the value of the limit vertex in a model to contain the graph, diagrams and other structures in the sketch. The E-theory of this sketch, which corresponds roughly, but not precisely, to the deductive closure of a list of axioms in traditional logic, is the initial model of E[S], which is E with the global element adjoined.

An assertion in this setting is a potential factorization (PF) of an arrow of the E-theory of S through an arrow into its codomain (defined precisely in Section 6.1). The assertion is valid if the PF does indeed factorize in every model of E[S].

Instead of the set of rules of deduction of a traditional theory, we have a set of rules of construction. More precisely, we give in Appendix A a system of construction rules that produce the categorial theory of a finite-limits sketch. We say that the potential factorization is deducible if there is an actual factorization in the categorial theory of the sketch. Such an arrow must be constructible by the rules in Appendix A. Thus the usual system of inference is replaced by a system of construction of arrows in a finite-limit category (no matter what type of category is sketched by E). This system is sound and complete with respect to models (Section 6.2).

The fact that we have assumed finite-limit sketches as given prior to the general definition of E-sketch is basic to the strategy of the paper, which is to make finite-limit logic the basic logic for all E-sketches (Section 8). The variation in what can be proved, for example for finite-limit sketches (Esketches where E = FinLim ) as contrasted with cartesian closed sketches (in which case E is a finite-limit theory for cartesian closed categories such as CCC in Appendix B.6) is entirely expressed by the choice of E and has no effect on the rules of construction.

The system that we describe may not facilitate human manipulation. However, as we discuss in Remark A.1.2, the system should not be difficult for computer implementation. Our approach may seem unusual from the point of view of symbolic logic, but it is in keeping with practices in computer implementation of complex data structures (a proof is a complex data structure) in that much more detail about the relationships between different parts of the structure are necessarily made explicit than is customary for systems that are designed to be understood by human beings, who have sophisticated built-in pattern recognition abilities.

1.4 Acknowledgments

This article is better because of conversations we have had with Robin Cockett and Colin McLarty. The names “string-based logic” and “graph-based logic” were suggested by Peter Freyd. The diagrams were prepared using K. Rose’s xypic.

2 Notation

The notation established in this section is used throughout the article.

2.1 Lists

Given a set A, List[A] denotes the set of lists of elements of A, including the empty list. The kth entry in a list w of elements of A is denoted by w_{k} and the length of w is denoted by Length[w]. The range of w, denoted by Rng[w], is the set of elements of A occurring as entries in w. If f:A → B is a function, List[f] : List[A] → List[B] is by definition f “mapped over” List[A]: If w is a list of elements of A, then the kth entry of List[f](w) is by definition f(w_{k}). This makes List a functor from the category of sets to itself.

2.2 Graphs

For a graph G, the set of nodes of G is denoted by Nodes[G] and the set of arrows is Arrows[G]. The underlying graph of a category 𝒞 is denoted by UndGr[𝒞]. A subgraph H of a graph G is said to be full if every arrow f : h_{1} → h_{2} of G between nodes of H is an arrow of H.

2.3 Diagrams

We define an equivalence relation on the set of graph homomorphisms into a graph G as follows: If δ : I → G and δ′ : I′ → G are graph homomorphisms, then δ is equivalent to δ′ if and only if there is a graph isomorphism ϕ:I → I′ such that

[figure: \begin{aligned}I & & I_{′} \\ & G \end{aligned}; ϕ; δ; δ′]  (1)

commutes. A diagram in G is then by definition an equivalence class of graph homomorphisms δ : I → G. As is the practice when an object is defined to be an equivalence class, we will refer to a diagram by any member of the equivalence class.

If δ: I → G is a diagram, I is said to be a shape graph of the diagram, denoted by ShpGr(δ), and G is said to be the ambient space of the diagram, denoted by AmbSp(δ). Observe that the ambient space of the diagram is determined absolutely, but the shape graph is determined only up to an isomorphism that makes Diagram (1) commute.

If I is a graph, 𝒞 is a category, and δ : I → UndGr[𝒞] is a diagram, we will also write it as δ : I → 𝒞 (unless there is danger of confusion).

2.3.1 Convention on drawing diagrams

It is customary to draw a diagram without naming its shape graph. We adopt the following convention: If a diagram is represented by a drawing on the page, the shape graph of the diagram is the graph that has one node for each object shown and one arrow for each arrow shown, with source and target as shown. Two objects at different locations on the page correspond to two different nodes of the shape graph, even if they have the same label, and an analogous remark applies to arrows.

2.3.2 Example The diagram (2)

\xymatrix{ & f \ar[d] \\ g \ar[r] & \begin{matrix}A & A \\ B & B \end{matrix} & g \ar[l] \\  & Id[B] \ar[u]}  (2)

called δ, has shape graph

[figure: \begin{matrix}h & i \\ j & k \end{matrix}; u; t; v; x]  (3)

so that δ(h) = A, δ(i) = A, δ(v) = g, δ(x) = Id[B] and so on. Diagram (4) below also has shape graph (3) (or one isomorphic to it, of course):

[figure: \begin{matrix}A & B \\ C & D \end{matrix}; g; f; h; k]  (4)

On the other hand, Diagram (5) below

[figure: \begin{aligned}A & & A \\ & B \end{aligned}; g; f; g]  (5)

is not the same diagram as (2). It has shape graph

[figure: \begin{aligned}i & & j \\ & k \end{aligned}; v; u; w]  (6)

2.4 Cones For any graph G and diagram δ : I → G, a cone Θ : v [figure] (δ : I → G) (also written Θ : v [figure] δ if the context makes this clear) has vertex v denoted by Vertex[Θ] and base diagram δ denoted by BsDiag[Θ]. For each node i of ShpGr[δ], the formal projection of the cone Θ from Vertex[Θ] to δ(i) is denoted by Proj[Θ, i] : v → δ(i). For a category 𝒞, a cone Θ : v [figure] (δ: I → 𝒞) is commutative if, for every arrow f : i → j in I, the diagram

[figure: \begin{aligned}& Vertex[Θ] \\ δ(i) & & δ(j) \end{aligned}; Proj[Θ, i]; Proj[Θ, j]; δ(f)]  (7)

commutes. The limit cone for a diagram δ will be denoted by LimCone[δ] : Lim[δ] [figure] δ.

2.5 Fonts

In general, variable objects are given in slant or script notation and specific objects (given by proper names) are given in upright notation. In more detail, we have the following systematic notation.

1. Specific data constructors, such as List, and specific fieldnames for complex objects, such as Nodes[G], are given in sans serif and are capitalized as shown.

2. Specific objects and arrows of sketches are also given in sans serif.

3. Specific constructor spaces, such as FinLim and CCC, are given in bold sans serif. We use E to denote a variable constructor space because of the unavailability of bold slanted sans serif.

4. Specific categories other than constructor spaces, such as Set, are given in boldface.

5. Diagrams (specific and variable) are named by lowercase Greek letters.

6. Cones (specific and variable) are named by uppercase Greek letters.

7. Models (specific and variable) are given in uppercase fraktur, for example 𝔐, ℭ.

8. Variable sketches, and objects and arrows therein, are given in slanted sans serif.

9. Variable categories other than constructor spaces are given in script, for example 𝒜, ℬ, 𝒞.

10. Other variable objects are given in math italics, such as a, b, c or (especially arrows) in lowercase Greek letters.

3 Adjoining nodes to diagrams

We now state and prove some technical lemmas that are used many times herein.

3.1 Restrictions of diagrams

3.1.1 Definition Let δ : I → 𝒞 be a diagram and Incl[J ⊆ I] : J → I an inclusion of graphs. Let Θ : v [figure] δ be a cone. The base-restriction of Θ to J is defined to be the cone Θ|^{J} : v [figure] (δ^{∘} Incl[J ⊆ I]) with vertex v and projections defined by Proj[Θ|^{J}, j] := Proj[Θ, j] : v → δ(j) for all nodes j of J. In this case, we also say that Θ is a base-extension of Θ|^{J}.

3.1.2 Remark Observe that if Θ is commutative, then so is Θ|^{J}.

3.1.3 Definition Let δ : I → 𝒞 be a diagram and J a subgraph of I. Then the subdiagram δ|_{J} is said to dominate δ, or to be dominant in δ, if every commutative cone Θ:v → (δ|_{J}) has a base extension to a commutative cone Θ′ : v → δ with the same vertex.

3.1.4 Remark Tholen and Tozzi [1989] give a condition (“confinality”) on I and J such that any diagram based on I is dominated by its base restriction to J. One type of dominance that their condition does not cover is the case in which δ is obtained from δ|_{J} by adjoining a limit cone over a subdiagram of δ|_{J}. This occurs in Section 7.1.1.

3.2 Limits of subdiagrams

3.2.1 Lemma Let δ : I → 𝒞 be a diagram and let J be a subgraph of I with inclusion Incl[J ⊆ I]. Let γ = δ|_{J}. Then there is a unique arrow ϕ: Lim[δ] → Lim[γ] such that for all nodes j of J,

[figure: \begin{aligned}Lim[δ] & & Lim[γ] \\ & δ(j) \end{aligned}; ϕ; Proj[LimCone[δ], j]; Proj[LimCone[γ], j]]  (8)

commutes. Moreover, if γ is a dominant subdiagram of δ, then ϕ is an isomorphism.

Proof The base-restriction of LimCone[δ] to J is a commutative cone Θ with vertex Lim[δ]. We choose ϕ to be Fillin[Θ, γ], the arrow produced by Rule ∃FIA of Appendix A. It follows from Rule CFIA that for each node j of J, the diagram below

[figure: \begin{aligned}Lim[δ] & & Lim[γ] \\ & γ(j) \end{aligned}; Fillin[Θ, γ]; Proj[Θ, j]; Proj[LimCone[γ], j]]]  (9)

commutes. Because they do, rule !FIA implies that ϕ is the only arrow that makes them all commute, as required.

Assume that γ dominates δ. Then we may choose an extension Ψ : Lim[γ] → δ of LimCone[γ] to δ. Using ∃FIA, we define

ψ := Fillin[Ψ, δ] : Lim[γ] → Lim[δ]

It follows from !FIA that ψ is the only arrow from Lim[γ] to Lim[δ] that makes all diagrams of the form

[figure: \begin{aligned}Lim[γ] & & Lim[δ] \\ & γ(j) \end{aligned}; ψ; Proj[Ψ, j]; Proj[LimCone[δ], j]]]  (10)

commute for each node j of J. Since ϕ^{∘}ψ : Lim[γ] → Lim[γ] and Id[Lim[γ]] : Lim[γ] → Lim[γ] both commute with all the projections, it follows from !FIA that ϕ^{∘}ψ = Id[Lim[γ]], A similar argument shows that ψ^{∘}ϕ = Id[Lim[δ]], so that ϕ is an isomorphism.

3.3 Special cases of extending diagrams

Here we define some special cases of dominance that are easy to recognize.

3.3.1 Definition Let I and J be graphs that have the same nodes, and suppose that I has exactly one arrow a: j → k not in J. Let δ: I → 𝒞 be a diagram with the property that for all nodes j′ of J and all arrows f : j → j′ and g : j′ → k,

[figure: \begin{aligned}j & & k \\ & j′ \end{aligned}; a; f; g]  (11)

commutes. Then we say δ extends δ|_{J} by adjoining a composite.

3.3.2 Definition Let I and J be graphs with the following properties:

AC.1 I has exactly one node v not in J.

AC.2 Every arrow in I not in J has target v.

Suppose that δ : I → 𝒞 is a diagram with the property that if a : i → v, b: j → v and f : i → j are arrows of I, then

[figure: \begin{aligned}i & & v \\ & j \end{aligned}; a; f; b]  (12)

commutes. Then we say δ extends δ|J by adjoining a commutative cocone.

3.3.3 Definition Let I, J and J′ be graphs with J′ ⊆ J ⊆ I, such that J′ is full in J, I contains exactly one node v not in J, and for each node j of J′, I contains exactly one arrow p_{j}: v → j and no other arrows not in J. Let δ: J → 𝒞 be a diagram, and suppose δ′: I → 𝒞 is a diagram that extends δ in such a way that δ′(v) and the arrows δ′(p_{j}) constitute a limit cone to δ|_{J′}. Then we say that δ′ extends δ by adjoining a limit.

3.3.4 Lemma Suppose that δ′ : I → 𝒞 extends δ : J → 𝒞 by adjoining a composite, a commutative cocone, or a limit. Then

Fillin[LimCone[δ′]|_{J}, δ] : Lim[δ′] → Lim[δ]

is an isomorphism.

Proof It is easy to see that, in all three cases, J is dominant in I.

4 Finite limit sketches

We use a general concept of sketch described in Section 5 that is based on the concept of finite limit sketch, a particular case of projective sketch due to Ehresmann. In this section, we review briefly some aspects of finite limit sketches that are relevant later.

4.1 Categorial theories

The categorial theory generated by a finite-limit sketch S is denoted by CatTh[FinLim , S]. It is a category with finite limits together with a sketch morphism

UnivMod[FinLim , S] : S → CatTh[FinLim , S]

called the universal model of the sketch. It has the following property: For each model 𝔐 of S, there exists a functor F_{𝔐}: CatTh[FinLim , S] → Set, determined uniquely up to natural isomorphism, with the property that

U(F_{𝔐})^{∘} UnivMod[FinLim , S] = 𝔐

where U is the forgetful functor from the category of finite-limit categories and finite-limit-preserving functors to the category of finite-limit sketches and morphisms thereof. It follows from these properties that CatTh[FinLim , S] is determined up to equivalence of categories and UnivMod[FinLim , S] is determined up to natural isomorphism.

In this article, for a given sketch S, we assume given a particular instance of CatTh[FinLim , S]: that constructed in [Barr and Wells, 1993a]. It has the following properties (which are not preserved by equivalence of categories):

T.1 CatTh[FinLim , S] is a category with canonical finite limits. (The construction explicitly produces the canonical limits.)

T.2 Every object of CatTh[FinLim , S] is the canonical limit of a diagram of the form UnivMod[FinLim , S]^{∘}δ where δ is a diagram in the graph of S.

T.3 Every arrow of CatTh[FinLim , S] is a composite of projections from canonical limits and arrows of the form UnivMod[FinLim , S](f ) for arrows f of the graph of S.

CatTh[FinLim , S] is clearly closed under all the constructions of Appendix A. The properties listed in the preceding paragraph imply that the category CatTh[FinLim , S] is minimal with respect to the constructions of that Appendix, so that in fact those constructions can be taken as an recursive definition of CatTh[FinLim , S].

These observations are summed up in the following proposition.

4.1.1 Proposition For a given sketch S, every object and every arrow of CatTh[FinLim , S] is constructible by repeated applications of the constructions of Appendix A.

It is proved in [Barr and Wells, 1993a] that every object of CatTh[FinLim , S] is the limit of a diagram in the graph of the sketch S. Once this is known, the proof is a straightforward induction showing that the least fixed point of the constructions in Appendix A is indeed a category with finite limits.

4.2 Remark concerning models

Let Cat be some given finite-limit sketch for categories. We have to consider the following three mathematical entities.

1. A category 𝒞.

2. A model ℭ of the sketch Cat in the category of sets which “is” or “represents” 𝒞. ℭ is a morphism of finite-limit sketches from Cat to the underlying finite-limit sketch of Set. ℭ is determined uniquely by 𝒞 if one assumes that Set has canonical finite limits. It is determined up to natural isomorphism in any case.

3. The model CatTh[FinLim , ℭ] of CatTh[FinLim , Cat] induced by ℭ. This is a finite-limit-preserving functor from CatTh[FinLim , Cat] to Set.

For many category theorists, 𝒞, ℭ and CatTh[FinLim , ℭ] denote the “same thing”, or perhaps 𝒞 and CatTh[FinLim , ℭ] are the “same thing” and ℭ consists of presentation data for 𝒞. Other mathematicians would disagree, saying 𝒞 is a category (presumably for them “category” has some meaning other than “model for the sketch for categories”) and CatTh[FinLim , Cat] is a functor, so how could they be the same thing? In the sequel, we will distinguish these constructions typographically, but we do not take a stand on this difference of opinion. Note that in any case the following three categories are equivalent:

1. The category of small categories and functors.

2. Mod[Cat, Set], the category of models of the sketch Cat in the category Set with natural transformations as morphisms.

3. The category of finite-limit-preserving functors from CatTh[FinLim , Cat] to Set with natural transformations between them as morphisms.

5 Sketches in general

We provide here a definition of “sketch” based on [Wells, 1990] (some of the terminology has been changed.) This constitutes a generalization of the concept of sketch invented by Charles Ehresmann and described in [Bastiani and Ehresmann, 1972] or in [Barr and Wells, 1990]. This definition presupposes the concept of finite-limit sketch (see Sections 1.1 and 4).

5.1 Constructor spaces

5.1.1 Assumptions

We will assume given a fixed finite-limit sketch Cat whose category of models is the category of small categories and functors. A specific such sketch is given explicitly in Appendix B.2. The presentation that follows has Cat as an implicit parameter.

5.1.2 Notation For any finite-limit sketch S and morphism η : Cat → S of sketches, the induced functor between categorial theories will be denoted by

CatTh[FinLim , η] : CatTh[FinLim , Cat] → CatTh[FinLim , S] 5.1.3 Definition A finite-limit sketch E together with a morphism η : Cat → E of sketches is called a constructor space sketch provided that every object in CatTh[FinLim , E] is the limit of a finite diagram whose nodes are of the form CatTh[FinLim , η](n), where n is a node of Cat.

5.1.4 Remark In all the examples in this article, CatTh[FinLim , η] is injective on objects. We will often assume that it is an inclusion and write n for CatTh[FinLim , η](n).

5.1.5 Definition A category of the form CatTh[FinLim , E] for some constructor space sketch E is called a constructor space. We will normally denote the constructor space CatTh[FinLim , E] by E.

5.1.6 Definition A model of a constructor space E in Set is called an E-category, and a morphism of such models is called an E-functor.

5.1.7 Discussion

Definitions 5.1.3, 5.1.5 and 5.1.6 generalize those in [Wells, 1990]. They conform to the two-dimensional version given in [Power and Wells, 1992].

The value in a model 𝔐 of an object v in a constructor space is the set of all examples of a particular construction that is possible in the E-category 𝔐. Extended examples of this are discussed in Section 5.2 and Section 7. Thus each object of E represents a type of construction possible in E, hence the name “constructor space”.

Examples of constructor space sketches include the sketches for categories with finite products, categories with finite limits, cartesian closed categories, toposes, and so on. Several constructor space sketches are given in detail in Appendix B.

5.2 Notation for diagrams in a constructor space

The object of CatTh[FinLim , Cat] whose value in a model is the set of all not necessarily commutative diagrams of the form

[figure: \begin{matrix}A & B \\ C & D \end{matrix}; f; h; k; x; g]  (13)

is the limit of the diagram

[figure: ar  ob  ar ob  ar  ob ar  ob  ar; source; target; source; target; source; target; source; target; source; target]  (14)

We now describe this in more detail and introduce some notation that makes the discussion of such diagrams easier to follow. We use the notation D(n) to refer to the diagram shown herein with label (n), and I(n) for its shape graph. For example, the limit of the diagram above is Lim[D(14)].

Every node of D(14) is either the object ob (the object that becomes the set of objects in a model) or the object ar (the object that becomes the set of arrows in a model) of CatTh[FinLim , Cat]. For a model ℭ of CatTh[FinLim , Cat] in Set, an element of ℭ(Lim[D(14)] is a diagram in ℭ, not necessarily commutative, of the form of Diagram (13).

In order to make the relation between Diagrams (13) and (14) clear, we give the shape graph of (14):

[figure: \begin{aligned}& f & C & g \\ A & & x & & D \\ & h & B & k \end{aligned}; s; t; s; t; s; t; s; t; s; t]  (15)

We have named the nodes of Diagram (15) by the objects and arrows that occur in Diagram (13) in such a way that the node named by an object or arrow of Diagram (13) will inhabit the value of that node in the model ℭ. For example, the object A of ℭ is at the upper left corner of Diagram (13) and the projection arrow from ℭ(Lim[D(14)]) to ℭ(ob) determined by the node labeled A of the shape graph (15) is a function from the set of diagrams in ℭ of the form of Diagram (13) to the set of objects of ℭ that takes a diagram to the object in its upper left corner.

We will combine diagrams such as Diagram (14) and their shape graphs into one graph by labeling the nodes of the diagram by superscripts naming the corresponding node of the shape graph. In the case of Diagram (14), doing this gives the following annotated diagram:

[figure: ar_{f}  ob_{C}  ar^{g} ob_{A}  ar^{x}  ob_{D} ar_{h}  ob_{B}  ar_{k}; source; target; source; target; source; target; source; target; source; target]  (16)

Here, the superscript A on the leftmost node indicates that the corresponding node of the shape graph is labeled A. Formally, the expression ob^{A} is used as the label for the node δ(A) and its use signifies that δ(A) = ob. That device helps the reader to see that Diagram (13) is indeed an element of ℭ(Lim[D(14)]).

For example, the particular arrow h of Diagram (13) is an element of ar, and the label ar^{h} in Diagram (16) helps one see that it is that node that projects to h in the model ℭ and that the source of h is A and that the target is B.

It is important to understand that an annotated diagram such as (16) denotes precisely the same diagram as (14). The fact that one node is labeled ob^{A} and another ob^{B} does not change the fact that both nodes are ob. The superscript merely gives information about the relation between Diagram (14) and Diagram (13).

Diagram (16) could also be drawn as the base of a limit cone Θ with limit Lim[D(16)] (which of course is the same as Lim[D(14)]) as follows.

[figure: Lim[δ(14)] ar^{g}  ar_{f}  ar^{x}  ar_{k}  ar_{h} ob_{C}  ob_{B} ob_{D}  ob_{A}; Proj[Θ, g]; Proj[Θ, f]; Proj[Θ, x]; Proj[Θ, k]; Proj[Θ, h]; source; target; source; target; source; target; source; target; source; target]  (17)

Because of the typographical complexity of doing this for diagrams more complicated than Diagram (16), we will usually give diagrams whose limits we discuss in the form of Diagram (16), without showing the cone, instead of in the form of Diagram (17).

Showing the cone explicitly as in Diagram (17) nevertheless has an advantage. It makes it clear that many of the projection arrows from Lim[D(16)] are induced by others; in the particular case of Diagram (17), all the arrows to nodes of the form ob are induced by composing arrows to some node of the form ar with source or target. Diagram (16) does not exhibit this property. A systematic method of translating from graphical expressions such as Diagram (17) to a string-based expression could presumably be based on this. In the case of Diagram (17), the string-based expression would be something like this:

{⟨g, f, x, k, h⟩ | source(g) = C, target(g) = D, source(f) = A, target(f) = C, source(x) = C, target(x) = B, source(k) = B,

target(k) = D, source(h) = A, target(h) = B}

or in more familiar terms,

{⟨g, f, x, k, h⟩ | g : C → D, f : A → C, x: C → B, k : B → D, h: A → B} 5.3 Sketches

5.3.1 Definition Let E be a constructor space. For any node v of E, we may freely adjoin a global element S :1 → v to obtain a finite-limit theory E[S]. S is called an E-sketch and E[S] is called the syntactic category of S; we will denote it SynCat[S]. It should be distinguished from the categorial theory CatTh[E, S], which is the initial model of E[S]. Details are in [Wells, 1990] or [Power and Wells, 1992].

5.3.2 Remark If E = FinLim , then a finite-limit sketch S in the traditional sense (a graph with diagrams and cones) corresponds to a FinLim - sketch in the sense of Definition 5.3.1 that we denote by Form[S] (but see Remark 5.3.4). The traditional sketch S is an element of the value in the initial model of a certain (not uniquely determined) node v of FinLim which is the limit of a generally large and complicated diagram (not uniquely determined) that specifies the graph, diagrams and cones of S. Example 5.3.3 illustrates this correspondence. These remarks apply to other types of Ehresmann sketches by replacing FinLim by the suitable constructor space.

5.3.3 Example As an example, consider the FinLim -sketch S with graph

[figure: A  B  C; v; u; f]  (18)

one diagram

[figure: \begin{matrix}B & A \\ B \end{matrix}; Id[B]; u; v]  (19)

and one cone

[figure: \begin{aligned}& B \\ A & & C \end{aligned}; u; f]  (20)

This is in fact a finite-product sketch, but any such sketch is also a FinLim - sketch. This is achieved, for instance, by setting S := Form[S] : 1 → v, where v is the limit of this diagram:

[figure: ob^{A} × ob^{C} ar^{u}  cone  ar_{f}  ob_{C} ob_{A}  _{ar_{2}}  ar  ob_{B} ar^{v}; prod; target; source; lproj; rproj; target; source; comp; lfac; rfac; unit; source; target]  (21)

This is however not the only way of viewing S as a FinLim -sketch as explained below.

5.3.4 Remark Note that the identification between traditional sketches and sketches in the new sense is many-to-one in both directions. A traditional finite-limit sketch can be described as an element of the limit of more than one diagram in FinLim . In the other direction, because every node v of FinLim is the limit of a diagram in a sketch for FinLim (for example, the one in Appendix B.5), any element of the value of v in an initial model can be described in terms of a graph, diagrams and cones, but in general not in only one way, and in any case such a description requires an arbitrary choice for the names of the nodes and arrows of the graph.

5.4 Models of sketches

Let S be an E-sketch as in Definition 5.3.1. The category of models (finitelimit-preserving functors) of E[S] has an underlying functor UndCat[E, S] to the category of E-categories induced by the embedding of E into E[S].

5.4.1 Definition Let S be an E-sketch and 𝒞 an E-category. An Efunctor from CatTh[E, S] to 𝒞 is called a model of S. A morphism of models in 𝒞 is a natural transformation. The category of models of S in 𝒞 is denoted by Mod[S, 𝒞].

5.4.2 Remark Each model of an E-sketch S is the unique functor induced (because CatTh[E, S] is an initial object) by a model 𝔐 of E[S] in Set (a finite-limit-preserving functor from E[S] to Set) that has 𝒞 as its underlying E-category. This passage from model of S to model of E[S] induces an equivalence of categories between the category of E-functors from CatTh[E, S] to 𝒞 and models (FinLim -functors) 𝔐 of E[S] in Set that have 𝒞 as underlying E-category.

5.4.3 Example In Example 5.3.3, a model of the traditional sketch S in a finite-limit category 𝒞 in the sense of Definition 5.4.1 is a finite-limit preserving functor from CatTh[FinLim , S] (which is the initial model of FinLim [S] that takes S to S) to 𝒞. The finite-limit functor from FinLim [S] to Set mentioned in Remark 5.4.2 is the extension of the model ℭ: FinLim → Set that “corresponds to” or “is” (see Remark 4.2) 𝒞 obtained by setting the value of the global element S to be the traditional sketch S.

6 Assertions in graph-based logic

6.1 Potential factorizations

In a constructor space E, a diagram of the form

\xymatrix{\begin{aligned}& C \\ A & B \end{aligned} & j \ar[l] \\ f \ar[u]}  (22)

is called a potential factorization or PF. B is called the workspace of the potential factorization, and j is called the claim of the potential factorization. In many examples, including all theories in this paper, j is monic and corresponds to a formal selection of a subset of those objects formally denoted by B.

6.1.1 Notation

We will use suggestive notation for a potential factorization, as exhibited in the diagram below.

[figure: claim hyp  wksp; claimcon; hypcon]  (23)

The names hypcon, claimcon and wksp respectively abbreviate “hypothesis construction”, “claim construction” and “workspace”. The reason for the names of the arrows and nodes is discussed in 7.3.

6.1.2 Actual factorizations

If an actual factorization arrow verif : hyp → claim exists in E that makes

[figure: claim hyp  wksp; claimcon; verif; hypcon]  (24)

commute, then we say that the potential factorization is deducible. If for some model 𝔐 of E there is an arrow ξ of Set that makes

[figure: 𝔐(claim) 𝔐(hyp)  𝔐(wksp); 𝔐(claimcon); ξ; 𝔐(hypcon)]  (25)

commute, then we say the model 𝔐 satisfies the potential factorization. If for every model 𝔐 there is such an arrow ξ then we say that the potential factorization is valid.

We give examples of potential factorizations in Section 7, and then discuss the general concept of potential factorization in Section 7.3.

6.2 Completeness

6.2.1 Theorem In any categorial theory CatTh[E, S], a potential factorization is deducible if and only if it is valid.

Proof That deducibility implies validity follows from the fact that functors preserve factorizations.

For the converse, let

[figure: claim hyp  wksp; claimcon; hypcon]  (26)

be a potential factorization in CatTh[E, S]. Suppose it is valid. Because the functor Hom(hyp, −) is a model, the hypothesis of the theorem implies that we may choose an arrow ξ of Set such that the diagram

[figure: Hom(hyp, claim) Hom(hyp, claim)  Hom(hyp, wksp); Hom(hyp, claimcon); ξ; Hom(hyp, hypcon)]  (27)

commutes. Define verif := ξ(id_{hyp}). Then claimcon^{∘} verif = hypcon, so that the potential factorization is deducible.

Any model 𝔐 is a functor that preserves finite limits, so that if claimcon is monic, so is 𝔐(claimcon). In that case, 𝔐(verif ) necessarily equals ξ.

Section B.7.2 gives an example of how completeness can be used.

6.2.2 Remark Traditional proofs of completeness contain an induction which is missing in the preceding argument. In the present system, a theorem can be identified with an arrow of CatTh[FinLim , S]. Proposition 4.1.1 describes the recursive construction of arrows and so is the analog of the inductive part of traditional proofs of completeness.

6.2.3 Proposition Let D : I → CatTh[E, S] be a diagram. Suppose for every model 𝔐 of CatTh[E, S], 𝔐^{∘}D commutes. Then D commutes.

Proof Suppose

[figure: \begin{aligned}A & B \\ & C \end{aligned}; f; h; g]  (28)

is a diagram in CatTh[E, S]. Then, because Hom(A, −) is a model,

Hom(A, A)  Hom(A, B)

Hom(A, C)

Hom(A, f) [figure]

Hom(A, h)

[figure]

Hom(A, g)

[figure]

commutes. By chasing Id[A] around the diagram both ways, we get g^{∘}f = h, so Diagram (28) commutes as well.

7 Examples of potential factorizations

We give two examples of potential factorizations in some detail. The example in 7.1 holds for any category and the example in 7.2 holds in any Cartesian closed category. We construct actual factorizations for these PF’s in Section 9.

7.1 A fact about diagrams in any category

The following proposition holds in any category.

7.1.1 Proposition In any category, given the following diagram

[figure: \begin{matrix}A & B \\ C & D \end{matrix}; f; h; k; x; g]  (29)

if the two triangles commute then so does the outside square.

Proof k^{∘}h = k^{∘}(x^{∘}f) = (k^{∘}x)^{∘}f = g^{∘}f.

We construct here the potential factorization in CatTh[FinLim , Cat] that corresponds to this theorem.

As we pointed out in Section 5.2, the value in a model of Lim[D(16)] is a diagram such as Diagram (29). However, Diagram (16) only carries the information as to the source and target of the arrows in Diagram (29). The structure we must actually work with includes the information as to which pairs are composable. There are four composable pairs in Diagram (29), and each one inhabits the value of ar_{2}, the node of formal composable pairs in a category (see Appendix B.2).

The following diagram thus contains the basic information about sources, targets and composability that are required for stating the theorem, and so its limit is suitable to be wksp.

[figure: ar_{2}^{⟨g,f⟩} ar_{f}  ob_{C}  ar^{g} ob_{A}  ar_{2}^{⟨x,f⟩}  ar^{x}  ar_{2}^{⟨k,x⟩}  ob_{D} ar_{h}  ob_{B}  ar_{k} ar_{2}^{⟨k,h⟩}; rfac; lfac; source; target; source; target; rfac; lfac; source; target; rfac; lfac; source; target; source; target; rfac; lfac]  (30)

The statement that the two triangles in Diagram (29) commute is: x^{∘}f = h and k^{∘}x = g. Using the composition arrow comp:ar_{2} → ar of CatTh[FinLim , Cat], this statement amounts to saying that Diagram (29) is a member of ℭ(Lim[D(31)]), which we take as hyp:

[figure: ar_{2}^{⟨g,f⟩} ar_{f}  ob_{C}  ar^{g} ob_{A}  ar_{2}^{⟨x,f⟩}  ar^{x}  ar_{2}^{⟨k,x⟩}  ob_{D} ar_{h}  ob_{B}  ar_{k} ar_{2}^{⟨k,h⟩}; rfac; lfac; source; target; source; target; rfac; lfac; comp; source; target; rfac; lfac; comp; source; target; source; target; rfac; lfac]  (31)

The statement that the outside of Diagram (29) commutes is that the diagram is a member of ℭ(Lim[δ(32)]), which we take as claim:

[figure: ar_{2}^{⟨g,f⟩} ar_{f}  ob_{C}  ar^{g} ob_{A}  ar_{2}^{⟨x,f⟩}  ar^{x}  ar_{2}^{⟨k,x⟩}  ob_{D}  ar_{k∘x∘f} ar_{h}  ob_{B}  ar_{k} ar_{2}^{⟨k,h⟩}; rfac; lfac; comp; source; target; source; target; rfac; lfac; source; target; rfac; lfac; source; target; source; target; rfac; lfac; comp]  (32)

Because Diagram (30) and Diagram (31) are restrictions of Diagram (32), we may, by Lemma 3.2.1 choose a function

claimcon: Lim[D(32)] → Lim[D(30)]

and similarly another function

hypcon: Lim[D(31)] → Lim[D(30)]

producing a potential factorization

[figure: Lim[D(32)] Lim[D(31)]  Lim[D(30)]; claimcon; hypcon]  (33)

This potential factorization expresses the content of Proposition 7.1.1 in diagrammatic form. It should be clear that the node Lim[D(30)] could have been replaced by Lim[D(16)].

7.2 A fact about Cartesian closed categories

Proposition 7.1.1 holds in any category. We now discuss a theorem of Cartesian closed categories, to show how the system presented in this paper handles structure that cannot be expressed using Ehresmann sketches. The latter are equivalent in expressive power to ordinary first order logic. (An excellent presentation of the details of this fact may be found in [Adámek and Rosičky, 1994].) Thus this example in a certain sense requires higher-order logic.

7.2.1 Proposition In any Cartesian closed category, if

[figure: \begin{aligned}A × B & C \\ & D \end{aligned}; g; h; f]

commutes, then so does

[figure: \begin{aligned}A & C_{B} \\ & D^{B} \end{aligned}; λg; λh; f^{B}]

See Appendix B.6 for notation. The arrow f^{B} is defined by

[figure: f^{B} := λ(C^{B} × B  C  D) : C^{B}  D_{B}; eval; f]  (34)

The proof follows from the fact that λ is invertible and the calculation

eval^{∘} ((f^{B}^{∘}λg) × Id[B]) = eval^{∘} ((f^{B} × Id[B])^{∘}(λg × Id[B]))
= (eval^{∘}(f^{B} × Id[B]))^{∘}(λg × Id[B])
= (f^{∘} eval)^{∘}(λg × Id[B])
= f^{∘}(eval^{∘}(λg × Id[B]))
= f^{∘}g = h = eval^{∘}(λh × Id[B])

The first equality is based on an assertion true in all categories that can be handled in our system in a manner similar to (but more complicated than) that of module (63) in Appendix B.4. The second and fourth equalities are associativity of composition and are proven using Figure (53) of Appendix B.2. The sixth equality is a hypothesis. The other three equalities are all based on Diagram (83) in Appendix B.6.

We present here the potential factorization corresponding to the third equality, which is the most complicated of those based on Diagram (83). In this presentation, unlike that of 7.1, we will use the modules developed in Appendix B to simplify the figures. The actual factorization corresponding to this potential factorization is given in 9.2.

The fact under discussion is that the diagram

[figure: \begin{aligned}A×B & C_{B}×B & D_{B}×B \\ & C & D \end{aligned}; λg× Id[B]; f^{B}× Id[B]; eval; eval; f]  (35)

commutes.

Thus wksp will be the limit of the following diagram, which describes the objects and arrows in Diagram (35) but has no requirements on its commutativity.

[figure: ar_{λg× Id[B]}  ob_{C^{B}× Id[B]}  ar_{f^{B}× Id[B]}  ob_{D^{B}× Id[B]} ob_{A×B}  ar_{eval}  ar_{eval} ob_{C}  ar_{f}  ob_{D}; target; source; source; target; source; target; source; target; source; target] (36)

We define hyp to be the limit of the following diagram, in which ϕ = (f^{∘} eval)^{∘}(λg× Id[B]).

[figure: ob_{D^{B}× Id[B]} ar_{f^{B}× Id[B]}  ar_{2}^{⟨eval,f^{B}× Id[B]⟩}  ar_{eval} ob_{C^{B}×B}  ar_{λg× Id[B]}  ob_{A×B}  ar_{ϕ} ar_{eval}  ar_{f ∘ eval}  ar_{2}^{⟨f ∘ eval,λg× Id[B]⟩} ob_{C}  ar_{2}^{⟨f,eval⟩}  ob_{D} ar_{f}; target; source; lfac; rfac; source; target; target; source; source; source; target; source; target; lfac; comp; rfac; rfac; comp; lfac; source; target] (37)

Then Diagram (36) is a subdiagram of Diagram (37) (the big rectangle in Diagram (36) is the perimeter of Diagram (37)) and we define hypcon to be the induced arrow from Lim[D(37)] to Lim[D(36)].

claim is the limit of a diagram we shall refer to as Diagram (37′), obtained from Diagram (37) by adjoining an arrow labeled comp from ar_{2}^{⟨eval,f^{B}×B⟩} to ar^{f ∘ eval}. Diagram (37′) includes Diagram (37) and hence Diagram (36), and we take the arrow claimcon to be the arrow from Diagram (37′) to Diagram (36) induced by this inclusion. The existence of both claimcon and hypcon follows from Lemma 3.2.1.

We now have a potential factorization

[figure: Lim[D(37′)] Lim[D(37)]  Lim[D(36)]; claimcon; hypcon]  (38)

The above potential factorization expresses the content of the third equality in the calculation in the proof of Proposition 7.2.1.

7.3 Discussion of the examples

7.3.1 General discussion

In a potential factorization

[figure: claim hyp  wksp; claimcon; hypcon]  (39)

each of hyp, claim and wksp represents a type of entity that can be constructed in an E-category. In this section, we discuss a way of thinking about these nodes that exhibits how they could represent a theorem about E-categories. This discussion is relevant to potential factorizations that are motivated by theorems stated in the traditional manner; it may not be relevant to an arbitrary potential factorization, which after all can be any pair of arrows with a common codomain.

1. The node wksp (for “workspace”) represents the data involved in both the hypothesis and the conclusion. For a given theorem, the choice of what is actually included in wksp may be somewhat arbitrary (see the discussion of Example 7.2 below).

2. The node hyp represents possible additional properties that are part of the assumptions in the theorem being represented.

3. The node claim represents the properties that the theorem asserts must hold given the assumptions.

4. The arrow hypcon represents the selection or construction necessary to see the hypothesis as part of the workspace. In both our examples, hypcon represents a simple forgetting of properties.

5. The arrow claimcon represents the selection or construction necessary to see the claim as part of the workspace.

6. The arrow verif in an actual factorization represents a specific way, uniform in any model, that any entity of type hyp can be transformed into, or recognized as, an entity of type claim.

7.3.2 Discussion of Example 7.1

In Example 7.1,

1. wksp represent squares of the form

[figure: \begin{matrix}A & B \\ C & D \end{matrix}; f; h; k; x; g]  (40)

with no commutativity conditions.

2. hyp represents diagrams of the form Diagram (40) in which the two triangles commute;

3. claim represents diagram of the form Diagram (40) in which the outside square commutes.

4. hypcon represents forgetting that the two triangles commute. Because it represents forgetting a property in this case, hypcon is monic, but in general it need not be.

5. claimcon represents forgetting that the outside square commutes.

7.3.3 Discussion of Example 7.2

In Example 7.2,

1. wksp represent diagrams of the form Diagram (35) with no commutativity conditions and no recognition that any sequence of arrows is composable. The phrase “The form of Diagram (35)” refers to the source and target commonalities of the arrows in the diagram. Obviously, some sequences compose but we have not represented that in wksp, although we could have.

2. hyp represents diagrams of the form of Diagram (35), recognizing the composite f^{∘} eval and the fact that

f^{∘} eval, λg × Id[B]

and eval, f^{B} × Id[B] are composable pairs.

3. claim represents diagram of the form Diagram (35) that commute.

4. hypcon represents forgetting the information concerning composition in hyp.

5. claimcon represents forgetting the information concerning composition in claim.

We discuss the meaning of the actual factorization arrows verif in 9.3.

7.3.4 Remark The representation of facts such as those of Example 7.1 and 7.2 as potential factorizations is variable free in the sense that in each statement, one does not refer to a particular diagram such as Diagram (29) or Diagram (35) which stands as a pattern for all such diagrams. Propositions 7.1.1 and 7.2.1 state the fact in question using those diagrams as patterns, and understanding their meaning calls on the reader’s ability to recognize patterns. Our description of the fact in the examples as a potential factorization is much more complicated because the diagrams involved in the potential factorization are essentially explicit descriptions of the relations between the nodes and arrows of Diagram (29) and Diagram (35) respectively, relations which a knowledgeable reader grasps from seeing the diagrams without having them indicated explicitly.

8 Construction and Deduction

8.1 The rules of graph-based logic

In first-order logic, rules are given for constructing terms and formulas, and further rules (rules of inference) are given for deriving formulas from formulas. These rules are intended to preserve truth.

In Appendix A we give rules for constructing all the objects and arrows of CatTh[FinLim , S] for an arbitrary finite-limit sketch S, and for constructing a basis for all the commutative diagrams in CatTh[FinLim , S]. These rules correspond to both the term and formula construction rules and the rules of inference of string-based logic. The tools of a typical string-based logic include constant symbols, variables, function symbols, logical operators and quantifiers. Here we have nodes, arrows and commutative diagrams. What corresponds to a sentence is a pair of arrows as in Diagram (39) (a potential factorization), and what corresponds to the satisfiability of the sentence in a model 𝔐 is the existence of an arrow ξ for which

[figure: 𝔐(hyp) 𝔐(claim)  𝔐(wksp); 𝔐(claimcon); ξ; 𝔐(hypcon)]  (41)

commutes. A demonstration of the deducibility of the sentence corresponds to the construction of an arrow verif : claim → hyp in CatTh[FinLim , S] such that

[figure: hyp claim  wksp; claimcon; verif; hypcon]  (42)

commutes. Thus the same rules suffice for constructing the sentence (the potential factorization) and for proving it (constructing the arrow that makes it an actual factorizaton). (See Section 7.3 for further discussion of these points.)

Each rule in Appendix A is actually a rule scheme, and each instance of the scheme is an assertion that, given certain arrows and commutative diagrams (see Remark 8.1.1 below) in CatTh[FinLim , S], other arrows or commutative diagrams exist in CatTh[FinLim , S]. For example, if δ is a diagram with shape graph

[figure: \begin{aligned}& i \\ j & k \end{aligned}; u; v]  (43)

then the following rule is an instance of ∃LIM:

[figure: \begin{aligned}& δ(i) \\ δ(j) & δ(k) \end{aligned}; δ(u); δ(u); \begin{matrix}Lim[δ] & δ(i) \\ δ(j) & δ(k) \end{matrix}; Proj[Lim[δ], j]; Proj[Lim[δ], k]; Proj[Lim[δ], i]]  (44)

8.1.1 Remark

Rules ∃FIA, !FIA and CFIA assume the existence of commutative cones, but a commutative cone is a collection of interrelated commutative diagrams, so the statement above that each scheme assumes the existence of certain arrows and commutative diagrams is correct. Thus given a cone Θ, an instance of ∃FIA is this rule:

[figure: \begin{matrix}Vertex[Θ] & δ(i) \\ δ(j) & δ(k) \end{matrix}; Proj[Θ, j]; Proj[Θ, k]; Proj[Θ, i]]

[figure: Vertex[Θ]  Lim[δ]; Fillin[Θ, δ]]

(45)

The point of this remark is that ∃FIA is a rule with a diagram as hypothesis and an arrow as conclusion. The hypothesis is the cone itself, not the string “Θ : v [figure] (δ : I → 𝒞)” or any other description of it.

9 Examples of theorems

9.1 Proof of Proposition 7.1.1

We continue Example 7.1 by constructing and thereby deducing the existence of an arrow verif : Lim[D(31)] → Lim[D(32)] making Diagram (33) commute.

We first construct Diagram (31′) (not shown) by adjoining ar_{3} to Diagram (31), along with arrows

lfac : ar_{3} → ar^{k}

mfac : ar_{3} → ar^{x}
rfac : ar_{3} → ar^{f}

We further construct Diagram (31′′) by adjoining

⟨lfac, mfac⟩: ar_{3} → ar_{2}^{⟨k,x⟩}
⟨mfac, rfac⟩: ar_{3} → ar_{2}^{⟨x,f⟩}
lass : ar_{3} → ar^{⟨g,f⟩}
rass : ar_{3} → ar^{⟨k,h⟩}

The first two are induced by the fact that ar_{3} is a limit and the other two are defined in Appendix B.2.

Diagram (30) is a base restriction of each of Diagram (31′) and Diagram (31′′), so, we may, using Lemma 3.2.1, choose arrows

ϕ_{1} : Lim[D(31′)] → Lim[D(30)]

and

ϕ_{2} : Lim[D(31′′)] → Lim[D(30)]

Diagram (31) is a dominant subdiagram of Diagram (31′) since the latter is obtained from the former by adjoining a limit of a subdiagram together with their projection arrows (lfac, mfac and rfac). Therefore, using Lemma 3.3.4, we may choose an isomorphism ψ_{1} making

[figure: Lim[D(31)]  Lim[D(31′)] Lim[D(30)]; ψ_{1}; hypcon; ϕ_{1}]  (46)

commute.

Similarly, Diagram (31′) is a dominant subdiagram of Diagram (31′′) since the latter is obtained from the former by adjoining four composites. Therefore by Lemma 3.3.4 we may choose an isomorphism ψ_{2} making

[figure: Lim[D(31′)]  Lim[D(31′′)] Lim[D(30)]; ψ_{2}; ϕ_{1}; ϕ_{2}]  (47)

commute. We then construct Diagram (31′′′) by adjoining arrows

comp : ar_{2}^{⟨g,f⟩} → ar^{k∘x∘f}

and

comp : ar_{2}^{⟨k,h⟩} → ar^{k∘x∘f}

where ar^{k∘x∘f} is a new node.

Because of associativity (the right diagram in Figure (53) of Appendix B.2), Diagram (31′′′) extends Diagram (31′′) by adjoining composites, so we may choose an isomorphism ψ_{3} : Lim[D(31′′)] → Lim[D(31′′′)] and an arrow ϕ_{3} : Lim[D(31′′′)] → Lim[D(30)] making

[figure: Lim[D(31′′)]  Lim[D(31′′′)] Lim[D(30)]; ψ_{3}; ϕ_{2}; ϕ_{3}]  (48)

commute.

Finally, by Lemma 3.2.1, we may choose arrow ψ_{4} : Lim[D(31′′′)] → Lim[D(32)] making

[figure: Lim[D(31′′′)]  Lim[D(32)] Lim[D(30)]; ψ_{4}; ϕ_{3}; claim]  (49)

commute.

We next set

verif := ψ_{4}^{∘}ψ_{3}^{∘}ψ_{2}^{∘}ψ_{1}  (50)

whence the theorem follows.

9.2 Proof of Theorem 7.2.1

In this section, we provide a factorization of the potential factorization described in Section 7.2.

Diagram (37) contains the following as a subdiagram, in which, using Diagram (34),

θ = ⟨eval, f^{B} × Id[B]⟩ = ⟨eval, λ(f^{∘} eval) × Id[B]⟩

[figure: ob_{C^{B}×B}  ar_{f^{B}×Id[B]}  ob_{D^{B}×B} ar_{2}^{θ} ar_{f ∘ eval}  ob_{D}  ar_{eval}; source; target; rfac; lfac; comp; target; source; target; source]  (51)

This diagram is an instance of Diagram (83), so it commutes. The arrow comp satisfies Definition 3.3.1, so Lemma 3.3.4 implies that there is an isomorphism verif : hyp → claim. Now the inclusion of Diagram (36) into Diagram (37) followed by the inclusion of Diagram (37) into Diagram (37′) is precisely the inclusion of Diagram (36) into Diagram (37′). It follows that hypcon^{∘} verif^{−1} = claimcon, so that claimcon^{∘} verif = hypcon as required.

9.3 Discussion of the proofs.

The factorization verif : Lim[D(31)] → Lim[D(32)] of Diagram (33) given in Equation (50) constitutes the recognition that if the two triangles commute, then so does the outside square. The fact that verif makes Diagram (33) commute is a codification of the fact that if the two triangles commute then so does the outside square of the same diagram. In general, the reason we require that actual factorizations be an arrow in a certain comma category instead of merely an arrow from one node to another is to allow us to assert hypotheses and conclusions that share data (in this case the data in Diagram (40)).

The factorization verif : hyp → claim constructed in 9.2 constitutes recognition that eval^{∘}(f^{B} ×Id[B]) = f^{∘} eval via the arrow comp:ar_{2}^{⟨eval,f^{B}×Id[B]⟩} → ar^{f ∘ eval} in Diagram (37′). Because of this, the node ar_{2}^{⟨f ∘ eval,λg×Id[B]⟩} could also be labeled ⟨eval^{∘}f^{B} × Id[B], λg × Id[B]⟩. Thus the factorization also exhibits the fact that

eval^{∘}(f^{B} × Id[B])^{∘}(λg × Id[B]) = f^{∘} eval^{∘}(λg × Id[B])

It is clear that there are many alternative formulations of Proposition 7.2.1. For example, instead of first constructing ar_{2}^{f ∘ eval} as in Diagram (37) (which is hyp in this case), we could have constructed a node ar_{2}^{eval ∘(f^{B}×Id[B])} and an arrow

comp : ar_{2}^{⟨eval,(f^{B}×Id[B]⟩)} → ar_{2}^{eval ∘(f^{B}×Id[B])}

Then the construction of an arrow

comp : ar_{2}^{⟨f,eval⟩} → ar^{eval ∘(f^{B}×Id[B])}

would have proved the theorem.

10 Future work

A second part of this work [Bagchi and Wells, 1993a] will discuss in detail the relationship between the graph-based logic for finite-product categories and the rules for equational deduction.

It is noteworthy that the rules of construction for constructor spaces given in Appendix A correspond to arrows of FinLim , although not in a one-to-one way (see Remark A.1.1). The rules are given here in a form that requires pattern recognition (recall the discussion in 7.3.4), but they clearly could be given at another level of abstraction as arrows or families of arrows of FinLim . We expect to make this explicit in a later work.

M. Makkai [1993a], [1993b] has produced an approach to explicating the logic of sketches that is quite different from that presented here. Both are attempts at codifying the process of diagram-manipulation used to prove results valid in particular structured categories. In both cases, structured categories or doctrines form the semantic universes with a pre-existing notion of validity. Both approaches are motivated by the desire to formulate a syntactic notion of deducibility. After that is said, the two approaches are very different and a detailed investigation of the relationship between them is desirable.

The following points are however worth mention.

• Both approaches require a generalization of Ehresmann sketches: Sketches as in Definition 5.3.1 here and sketch category over a category G in [Makkai, 1993b].

• In Makkai’s approach, the sketch axioms are different for different doctrines and serve both as axioms and as rules of inference. In contrast, here the rules of construction are the same for all doctrines, what distinguishes doctrines is their specification as CS-sketches. This feature is a departure from the usual practice in symbolic logic.

The rules of construction given herein take place in the doctrine of finite limits. Most of the syntax and rules of deduction of traditional logical theories are clearly expressible using context-sensitive grammars, which intuitively at least can be modeled using finite limits. (Context-free grammars can be modeled using only finite products [Wells and Barr, 1988].) However, one could imagine extensions of this doctrine; for example, the use of coproducts to allow the specification of conditional compilation or the use of doctrines involving epimorphic covering families that allow the deliberate description of ambiguous statements.

A Appendix: Rules of construction

These rules are given in two lists.

A.1 Rules that construct objects and arrows

This list gives all the rules that construct objects and arrows in the category CatTh[FinLim , S].

∃OB  \overline{c} for every object c of S.

∃ARR

[figure: a b; f]

for every arrow f : a → b of S.

∃COMP

[figure: a  b  c; f; g; a  c; g^{∘}f]

for every object b and pair of arrows f : a → b and g : b → c of CatTh[FinLim , S].

∃ID

\frac{c}{[figure: c; Id[c]]}

for every object c of CatTh[FinLim , S].

∃LIM

\frac{δ : I → CatTh[FinLim , S]}{LimCone[δ] : Lim[δ] [figure] δ}

for every diagram δ : I → CatTh[FinLim , S].

∃FIA

\frac{Θ : v [figure] δ}{Fillin[Θ, δ] : v → Lim[δ]}

for every diagram δ and every cone Θ : v [figure] δ in CatTh[FinLim , S].

A.1.1 Remark The first two rules are justified by the inclusion of the sketch S into CatTh[FinLim , S]. The rules ∃COMP corresponds to the arrow comp and ∃ID to unit of the sketch for categories B.2. ∃LIM and ∃FIA correspond to arrows in FinLim but not specifically to arrows of the sketch B.5, because an arbitrary finite limit is constructed from a combination of products and equalizers.

A.1.2 Remark

The rules just given construct specific objects and arrows in CatTh[FinLim , S]. Rule ∃LIM, for example, constructs a specific limit cone called LimCone[δ], thus providing canonical limits for CatTh[FinLim , S]. It is true that there are other limit cones in general for a given diagram δ, but LimCone[δ] is a specific one.

Of course, in many cases, the entity constructed is the unique entity satisfying some property. For example, the arrow g^{∘}f constructed by ∃COMP is (by definition of commutative diagram) the only one making the bottom diagram in COMPDIAG commute in CatTh[FinLim , S]. The arrow constructed by ∃ID is (by an easy theorem of category theory) the only one making the bottom diagrams in IDL and IDR commute. The arrow constructed by ∃FIA is (because of !FIA) the only one making the bottom diagram in CFIA commute. In connection with the point that each rule constructs a specific arrow, these observations are red herrings: in fact, each rule constructs a specific arrow with the name given, independently of any uniqueness properties arising from any other source.

This point of view is contrary to the spirit of category theory. We follow it here because we are constructing syntax with an eye toward implementing it in a computer language. It may be possible to design a computer language in which a construction such as ∃LIM produces a pointer to an isomorphism class of structures rather than to a specific one of them, but we know of no such language. On the other hand, implementing the specific constructions defined above should be relatively straightforward using a modern object-oriented language. Note that we are not asserting that it would be straightforward to find a confluent and normalizing form of these rules for automatic theorem proving, only that there are no obvious difficulties in implementing them so that they could be applied in an ad-hoc manner.

A.2 Rules that construct diagrams

The following rules produce the existence of diagrams that must commute.

REF

[figure: a  b; f; a  b; f; f]

for every arrow f : a → b of CatTh[FinLim , S]

TRANS

[figure: a  b  a  b; f; g; g; h; a  b; f; h]

for all objects a and b and all arrows f, g, h:a → b of CatTh[FinLim , S]

∃DIAG UnivMod[FinLim , S]^{∘}δ : I → CatTh[FinLim , S]

for every diagram δ in the set D_{S} of diagrams of S.

COMPDIAG

[figure: \begin{aligned}a & b \\ & c \end{aligned}; f; g; \begin{aligned}a & b \\ & c \end{aligned}; f; g^{∘}f; g]

for every pair of arrows f: a → b and g : b → c of CatTh[FinLim , S].

IDL

[figure: c; Id[c]; g : b → c; \begin{aligned}b & c \\ & c \end{aligned}; g; g; Id[c]]

for every object c and every arrow g : b → c of CatTh[FinLim , S].

IDR

[figure: c; Id[c]; f : c → d; \begin{aligned}c & c \\ & d \end{aligned}; Id[c]; f; f]

for every object c and every arrow f : c → d of CatTh[FinLim , S].

ASSOC

[figure: a  b  c  d; f; g; h; \begin{matrix}a & b \\ c & d \end{matrix}; f; g^{∘}f; h^{∘}g; g; h]

for all arrows f : a → b, g : b → c and h: c → d of CatTh[FinLim , S].

CFIA

\begin{matrix}i ∈ Nodes[I] \\ Θ : v [figure] δ \end{matrix}

[figure: \begin{aligned}v & & Lim[δ] \\ & δ(i) \end{aligned}; Fillin[Θ, δ]; Proj[Θ, i]; Proj[LimCone[δ], i]]]

for every diagram δ:I → CatTh[FinLim , S], every node i of I, and every cone Θ with base diagram δ.

!FIA  \frac{δ : I → CatTh[FinLim , S] Θ : v [figure] δ h: v → Lim[δ] k : v → Lim[δ] and each of the following diagrams for each node i of I: [figure: \begin{aligned}v & & Lim[δ] \\ & δ(i) \end{aligned}; h; Proj[Θ, i]; Proj[LimCone[δ], i]]] [figure: \begin{aligned}v & & Lim[δ] \\ & δ(i) \end{aligned}; k; Proj[Θ, i]; Proj[LimCone[δ], i]]]}{[figure: v  Lim[δ]; h; k]}

for every diagram δ:I → CatTh[FinLim , S], every cone Θ in CatTh[FinLim , S] with base diagram δ, and every pair of arrows h, k : v → Lim[δ].

A.2.1 Remark Note that we do not need a rule of the form

SYM  [figure: a  b; f; g; a  b; g; f]

since the two diagrams exhibited are actually the same diagram (see 2.3).

B Appendix: Sketches for constructor spaces

Here we present constructor space sketches for certain types of categories. In each case the models are categories of the sort described and the morphisms of models are functors that preserve the structure on the nose. It is an old result that such categories can be sketched. See [Burroni, 1970a], [Burroni, 1970b], [McDonald and Stone, 1984], and [Coppey and Lair, 1988], for example.

The embedding η of Section 5.1.3 will in each case be inclusion.

B.1 Notation

We denote the ith projection in a product diagram of the form

ob^{A} × ob^{B}
ob_{A}  ob_{B}

p_{1}

[figure]
p_{2}

[figure]

as p_{i}, or p_{i}^{A×B} if the source or target is not shown. We use a similar device for the product of three copies of ob.

B.2 The sketch Cat for categories

This version of the sketch for categories is based on [Barr and Wells, 1990]. Another version is given in [Coppey and Lair, 1988], page 64. The first versions were done by Ehresmann [1966], [1968a] and [1968b].

B.2.1 The graph of Cat The graph of the sketch for categories contains nodes as follows.

1. 1, the formal terminal object.

2. ob, the formal set of objects.

3. ar, the formal set of arrows.

4. ar_{2}, the formal set of composable pairs of arrows.

5. ar_{3}, the formal set of composable triples of arrows. The arrows for the sketch for categories are

1. unit : ob → ar that formally picks out the identity arrow of an object.

2. source, target : ar → ob that formally pick out the source and target of an arrow.

3. comp : ar_{2} → ar that picks out the composite of a composable pair.

4. lfac, rfac:ar_{2} → ar that pick out the left and right factors in a composable pair.

5. lfac, mfac, rfac : ar_{3} → ar that pick out the left, middle and right factors in a composable triple of arrows.

6. lass, rass : ar_{3} → ar_{2}: lass formally takes ⟨h, g, f⟩ to ⟨h^{∘}g, f⟩ and rass takes it to ⟨h, g^{∘}f⟩.

7. lunit, runit : ar → ar_{2}: lunit takes an arrow f : A → B to ⟨Id[B], f⟩ and runit takes it to ⟨f, Id[A]⟩.

8. Arrows id : x → x as needed. Observe that id, lfac and rfac, like p_{1} and p_{2}, are overloaded. We will observe the same care with these arrows as with p_{1} and p_{2} as mentioned in Section B.1.

B.2.2 Cones of Cat ar_{2} and ar_{3} are defined by these cones:

[figure: _{ar_{2}} ar  ar ob; lfac; rfac; source; target; _{ar_{3}} ar  ar  ar ob  ob; lfac; mfac; rfac; source; target; source; target]

B.2.3 Diagrams of Cat

[figure: _{ar_{2}}  _{ar_{3}} ar  _{ar_{2}}  ar; comp; ⟨lfac, mfac⟩; rfac; lass; lfac; rfac; _{ar_{3}}  _{ar_{2}} ar  _{ar_{2}}  ar; lfac; rass; ⟨mfac, rfac⟩; comp; lfac; rfac]

(52)

[figure: ob  ar ar  _{ar_{2}}  ar; unit; target; id; lunit; lfac; rfac; ar  ob ar  _{ar_{2}}  ar; id; runit; source; unit; lfac; rfac]

[figure: ar  _{ar_{2}}  ar ar; runit; id; comp; lunit; id; _{ar_{3}}  _{ar_{2}} _{ar_{2}}  ar; lass; rass; comp; comp]  (53)

B.3 The sketch for the constructor space FinProd To get the sketch for categories with finite products, we must add the following nodes and arrows to the sketch for categories:

Nodes:

1. ta, the formal set of terminal arrows.

2. cone, the formal set of cones of the form

[figure: \begin{aligned}& V \\ A & & B \end{aligned}; p_{2}; p_{1}]  (54)

3. fid, the formal set of fill-in diagrams (“sawhorses”) of the form

[figure: \begin{matrix}V & L \\ A & B \end{matrix}; h]  (55)

where h commutes with the cone projections. Arrows:

1. ter : 1 → ob, that formally picks out a particular terminal object.

2. ! : ob → ta, that picks out the arrow from an object to the terminal object.

3. inc : ta → ar, the formal inclusion of the set of terminal arrows into the set of arrows.

4. prod : ob × ob → cone, that picks out the product cone over a pair of objects.

5. soco : fid → cone, that picks out the source cone of a fill-in arrow.

6. taco : fid → cone, that picks out the target cone of a fill-in arrow.

7. ufid : cone → fid, that takes a cone to the unique fill-in diagram that has the cone as source cone.

8. fia:fid → ar that formally picks out the fill-in arrow in a fill-in diagram.

B.3.1 Cones for FinProd

FinProd has four cones in addition to those of the sketch for categories. One is the cone with vertex 1 over the empty diagram. The one below says that ta is the formal set of arrows to the terminal object:

[figure: ta ar  ob 1; inc; target; ter]  (56)

Note that in giving this cone, we are not only saying that ta is the limit of the diagram

[figure: ar  ob 1; target; ter]  (57)

but also that inc is one of the projection arrows. (Indeed, this is the only projection arrow that matters, since the other two are induced.)

The following cone makes cone the formal object of cones to a discrete diagrams consisting of a pair of objects.

[figure: cone ar  ob  ar; lproj; rproj; source; source]  (58)

Finally, there must be a cone with vertex fid over Diagram 59 below, which is annotated to refer to Diagram (55), in which Γ is the cone with vertex V, Λ is the cone with vertex L and is a limit cone, and h is the fill-in arrow. In this case, the projection arrows of the cone are not shown.

[figure: _{ar_{2}}  ob_{V} ar  cone_{Γ}  ar ob_{A}  ob^{A}×ob^{B}  ob_{B}  _{ar_{2}}  ar_{h} ar  cone_{Λ}  ar ob_{L}; comp; lfac; rfac; target; source; lproj; rproj; target; source; p_{1}; p_{2}; prod; comp; lfac; rfac; source; target; target; source; lproj; rproj; target; source]  (59)

In addition, we require:

1) The projection to cone^{Γ} must be soco.

2) The projection to cone^{Λ} must be taco.

3) The projection to ar^{h} must be fia.

B.3.2 Diagrams for FinProd

The following two diagrams make the arrow to the terminal object have the correct source and target.

[figure: ob  ta  ar ob; !; id; inc; source; ta  ar  ob ta; inc; id; source; !]  (60)

The diagram below makes the fill-in arrow to a product unique.

[figure: cone  fid; ufid; soco]  (61)

The diagram below forces the product cone projections to have the correct targets.

[figure: ob × ob ob  ar  cone  ar  ob; p_{1}; p_{2}; prod; target; lproj; rproj; target]  (62)

B.4 Modules

As we proceed to sketch more complicated constructions, we will need to use some device to communicate the nature of the necessary diagrams, which become too large to comprehend easily. Here we introduce the first of several modules: diagrams that occur frequently as subdiagrams because they are needed to force the value of a node in a model to contain certain types of constructions.

B.4.1 The module for the product of objects

Every occurrence of ob that is annotated M ×N must be part of a subdiagram of the following form:

[figure: ob_{M}  ar_{p_{1}^{M×N}} ob^{M} × ob^{N}  cone  ob_{M×N} ob_{N}  ar_{p_{2}^{M×N}}; target; source; prod; p_{1}; p_{2}; lproj; rproj; target; source]  (63)

Henceforth, an occurrence of ob annotated A×B (for example) will be taken to imply the existence of a subdiagram of the form of Diagram (63) with M replaced with A and N replaced with B. The subdiagram will not necessarily be shown. If this is part of a diagram δ, the diagram can be reconstructed by taking the union of the shape graph of the module (63) and the shape graph of the part of δ that is shown on the page, and defining the diagram based on the resulting graph as the pushout of the diagram shown and the module. This is illustrated in Diagrams (65) and (66) in the next section.

B.4.2 The module for the product of arrows

In the commutative diagram

[figure: \begin{aligned}K & K × N \\ & & N \\ M & M × N \end{aligned}; u; p_{1}; p_{2}; p_{2}; p_{2}]  (64)

the unlabeled arrow is necessarily u×Id[N]:K×N → M ×N. Such a diagram must be an element in a model of the value of Diagram (65) below, which is therefore a module for the product of an arrow and an identity arrow. In this diagram, ϕ := ⟨p_{2}^{M×N}, u × Id[N]⟩.

[figure: ob^{K}×ob^{N} cone ob_{K}  ar_{p_{1}^{K×N}}  ob_{K×N}  ar_{p_{2}^{K×N}} ar^{u}  ar_{2}^{⟨u,p_{1}⟩}  ar  ar_{2}^{⟨u× Id[N],p_{2}⟩} ar_{u× Id[N]}  ar_{2}^{ϕ}  ob_{N} ob_{M}  ar_{p_{1}^{M×N}}  ob_{M×N}  ar_{p_{2}^{M×N}} cone ob^{M}×ob^{N}; p_{1}; prod; p_{2}; lproj; rproj; target; source; source; target; source; target; lfac; rfac; comp; comp; rfac; lfac; target; source; rfac; comp; lfac; target; source; source; target; lproj; rproj; p_{1}; prod; p_{2}] (65)

More precisely, let x be an element of 𝔐(Lim[D(65)]), for some category 𝔐 with finite limits. Then if Proj[Lim[D(65)], h](x) = h, then

Proj[Lim[D(65)], h× Id[A]](x) = h× Id[A]

as suggested by the notation. This will be used in Section B.6 below.

Diagram (65) contains two copies of Diagram (63), the module for the product of two objects. The copy at the bottom is precisely Diagram (63), and the copy at the top is Diagram (63) with M replaced with K. In the sequel, a diagram such as Diagram (65) will be drawn without the modules, as shown below.

ob_{K}  ar_{p_{1}^{K×N}}  ob_{K×N}  ar_{p_{2}^{K×N}}

ar^{u}  ar_{2}^{⟨u,p_{1}^{K×N} ⟩}  ar  ar_{2}^{⟨u× Id[N],p_{2}⟩}  ar_{u× Id[N]}  ar_{2}^{ϕ}  ob_{N}

ob_{M}  ar_{p_{1}^{M×N}}  ob_{M×N}  ar_{p_{2}^{M×N}}

target

[figure]

source

[figure]

source

[figure]

target

[figure]

source

[figure]

target

[figure]

lfac

[figure]

rfac

[figure] [figure]

comp

[figure]

comp

[figure]

rfac

[figure]

lfac

[figure] [figure]

target

[figure]

source

[figure]

rfac

[figure]

comp

[figure]

lfac

[figure]

target

[figure]

source

[figure]

source

[figure]

target

[figure] [figure]

(66)

Diagram (65) may be mechanically reconstructed from Diagram (66) and the annotations that include the symbols M × N and K × N (three of each). The shape diagram of Diagram (65) is the pushout of the shape diagram of Diagram (66) and the shape diagrams of the modules Diagram (63) and Diagram (63) with M ← K. Each of the latter two have four annotated nodes and six annotated arrows in common with Diagram (66), and the values of any two of the three smaller diagrams at a given common node or arrow is of course the same, so that Diagram (65) is the union of Diagram (66) and the two modules.

B.5 The sketch for the constructor space FinLim

We sketch the constructor space FinLim by adding data to the sketch for FinProd that ensure that a FinLim -category has equalizers of pairs of arrows. The sketch has the following nodes:

1. ppair is the formal set of parallel pairs of the form

[figure: A  B; f; g]  (67)

2. econe is the formal set of diagrams

[figure: E  A  B; u; f; g]  (68)

in which f^{∘}u = g^{∘}u. Of course, a cone to Diagram (67) also has a projection to B, but that is forced and need not be included in the data for the cone.

3. efid is the set of fill-in diagrams

[figure: \begin{aligned}& X \\ E & A & B \end{aligned}; v; u; e; f; g]  (69)

in which f^{∘}e = g^{∘}e and u = e^{∘}v. The arrows of the sketch include:

1. equ : ppair → econe, that formally picks out the equalizer of the parallel pair.

2. top, bot : ppair → ar, that pick out f and g in Diagram (67).

3. etop, ebot : econe → ar, that pick out f and g in Diagram (68).

4. esoco, etaco : efid → econe that pick out the source and target cones of the fill-in arrow.

5. eufid : econe → efid that takes a diagram of the form of Diagram (68) to the unique fill-in diagram that has this diagram as source cone.

6. efia : efid → ar that picks out the fill-in arrow in a fill-in diagram.

B.5.1 Cones for FinLim

ppair is the limit of the diagram

[figure: ar_{f}  ob_{B} ob_{A}  ar^{g}; target; source; source; target]  (70)

The following projections from ppair have names: soob : ppair → ob^{A}, top : ppair → ar^{f}, and bot : ppair → ar^{g}.

econe is the limit of

[figure: _{ar_{2}}  ar_{f} ar  ar^{e}  ob_{A}  ob_{B} _{ar_{2}}  ar^{g}; rfac; lfac; comp; source; target; target; comp; lfac; rfac; source; target]  (71)

Two projections have names: etop : econe → ar^{f} and ebot : econe → ar^{g}.

efid is the limit of the pushout of Diagram (71) and the following diagram. Note that the common part of the two diagrams is

[figure: ar^{e}  ob_{A}; t]

We could have presented Diagram (59) as a pushout in much the same way (the common part would describe the arrow h:V → L). We have deliberately varied the way we present the data in this article because we are not sure ourselves which approach communicates best.

[figure: ar^{v}  ob_{X}  ar^{u} _{ar_{2}} ob_{E}  ar^{e}  ob_{A}; target; source; source; target; rfac; comp; lfac; source; target]  (72)

The named projections are esoco:efid → ar^{u}, etaco:efid → ar^{e} and efia:efid → ar^{v}.

B.5.2 Diagrams for FinLim

The following diagram makes the fill-in arrow unique.

[figure: econe  efid; eufid; esoco]  (73)

These two diagrams ensure that the equalizer cone be a cone to the correct diagram.

[figure: ppair  econe ar; equ; top; etop; ppair  econe ar; equ; bot; ebot]  (74)

B.6 The sketch for the constructor space CCC

B.6.1 Definition A Cartesian closed category is a category 𝒞 with the following structure:

CCC.1 𝒞 has binary products.

CCC.2 For each pair of objects A and B of 𝒞, there is an object B^{A} and an arrow eval :B^{A} × A → B.

CCC.3 For each triple of objects A, B and C of 𝒞, there is a map

λ: Hom(B × A, C) → Hom(B, C^{A})  (75)

such that for every arrow f : B × A → C,

[figure: \begin{aligned}B×A & C_{A}×A \\ & C \end{aligned}; λf× Id[A]; f; eval]  (76)

commutes.

CCC.4 For any arrow g : B → C^{A}, λ(eval^{∘}(g× Id[A])) = g.

Using this definition, the sketch for the constructor space for Cartesian closed categories may be built on the sketch for FinProd by adding the following nodes and arrows.

The nodes are:

1. twovf, the formal set of “functions of two variables”, that is, arrows of the form B × A → C.

2. curry, the formal set of “curried functions” B → C^{A}.

The sketch for CCC has arrows

1. fs : ob^{B} × ob^{A} → ob^{B^{A}} that picks out the function space B^{A} of two objects B and A.

2. ev : ob^{B} × ob^{A} → ar that picks out the arrow eval :B^{A} × A → B.

3. lam : ar → ar, the formal version of the mapping λ of Diagram (75).

4. tsource : twovf → ob^{B×A}, that picks out the source of a function f : A × B → C.

5. ttarget:twovf → ob^{C}, that picks out the target of a function f:A×B → C.

6. arrow : twovf → ar^{f}, that picks out the arrow f itself.

7. csource : curry → ob^{B}, that picks out the source of a curried function g : B → C^{A}.

8. ctarget : curry → ob^{C^{A}}, that picks out the target of a curried function f : B → C^{A}.

9. arrow : curry → ar^{g}, that picks out the arrow g itself.

B.6.2 Cones for CCC

CCC must have two cones

[figure: twovf ob_{B×A}  ar_{f}  ob_{C}; tsource; arrow; ttarget; source; source]  (77)

[figure: curry ob^{C}×ob^{A}  ob_{c^{A}}  ar^{g}  ob_{B}; ctarget; arrow; csource; fs; target; source]  (78)

B.7 The module for function spaces Henceforth, we will assume the module

[figure: ob_{M}  ob^{M}×ob^{N}  ob_{M^{N}} ob_{N}; p_{1}; fs; p_{2}]  (79)

is attached whenever an occurrence of ob is annotated by M^{N}. Note that this occurred in Diagram (78).

B.7.1 Diagrams for CCC Diagram (80) below forces eval to have the correct domain and codomain.

[figure: ob_{B^{A}×A}  ar_{eval}  ob_{B}; source; target]  (80)

Expanding this diagram using the required modules is a two stage process, giving

[figure: ob_{A}  ob^{B^{A}}×ob^{A}  ob_{B^{A}} ar  cone  ar  ob^{B}×ob^{A}  ob_{A} ob_{B^{A}×A}  ar_{eval}  ob_{B}; p_{2}; p_{1}; prod; rproj; source; lproj; rproj; lproj; source; fs; p_{1}; p_{2}; source; target]  (81)

Diagram (82) below forces λf to have the correct domain and codomain.

[figure: ob_{C}  ob_{C^{A}} ob_{B×A}  twovf_{f}  curry^{λf} ob_{B}; tsource; lam; ttarget; csource; ctarget]  (82)

Diagram (83) below forces Diagram (76) to commute.

[figure: ob_{B×A} ar_{λf× Id[A]} ob_{C^{A}×A} _{ar_{2}} ar_{f} ob_{C} ar_{eval}; source; target; rfac; comp; lfac; target; source; target; source] (83)

Diagram (84) below ensures that requirement CCC–4 holds.

ob_{C^{A}×A}  ar_{eval}  ob_{C}  ob_{B}
ar_{g× Id[A]}  ar_{2}^{⟨eval,g× Id[A]⟩}  ar^{g}  ob_{C^{A}}
ob_{B×A}  ar_{eval ∘(g× Id[A])}  curry

twovf source

[figure]

target

[figure]

target

[figure]

source

[figure]

lfac

[figure]

rfac

[figure]

comp

[figure]

source

[figure]

target

[figure]

source

[figure]

target

[figure]

arrow

[figure]

tsource

[figure] [figure]

ttarget

[figure]

arrow

[figure] [figure]

lam

[figure]

(84)

B.7.2 Invertibility of λ

It follows from CCC-4 that if 𝒞 is any Cartesian closed category corresponding to a model ℭ, then ℭ(λ) is a bijection. The Completeness Theorems 6.2.1 and 6.2.3 then imply that there is an arrow λ^{−1} in CCC that, as its name suggests, is a formal inverse to λ.

References

At the end of each entry, the pages on which that entry is cited are listed in parentheses.

[Adámek and Rosičky, 1994] Jiří Adámek and Jiří Rosičky. Locally Presentable and Accessible Categories. Cambridge University Press, 1994. (26)

[Bagchi and Wells, 1993a] Atish Bagchi and Charles Wells. Graph-based logic and sketches II: Finite product categories and equational logic. Avail-

able by gopher from gopher.cwru.edu, path=/class/mans/math/pub/

wells/, 1993. (37)

[Bagchi and Wells, 1993b] Atish Bagchi and Charles Wells. The varieties of mathematical prose. Available by gopher from gopher.cwru.edu,

path=/class/mans/math/pub/wells/, 1993. (1)

[Barr and Wells, 1985] Michael Barr and Charles Wells. Toposes, Triples and Theories, volume 278 of Grundlehren der mathematischen Wissenschaften. Springer-Verlag, New York, 1985. A list of corrections and additions is maintained in [Barr and Wells, 1993c]. (59)

[Barr and Wells, 1990] Michael Barr and Charles Wells. Category Theory for Computing Science. Prentice-Hall International Series in Computer Science. Prentice-Hall International, New York, 1990. The document [Barr and Wells, 1993b] contains corrections and additions to the book. (1, 2, 13, 43, 59)

[Barr and Wells, 1992] Michael Barr and Charles Wells. On the limitations of sketches. Canadian Mathematical Bulletin, 35:287–294, 1992.

[Barr and Wells, 1993a] Michael Barr and Charles Wells. The category of diagrams, 1993. To appear. (11, 12)

[Barr and Wells, 1993b] Michael Barr and Charles Wells. Category Theory for Computing Science: Update. Available by anonymous FTP

from triples.math.mcgill.ca in directory pub/barr. The file is called

ctcsupdate.dvi, 1993. Corrections and additions to [Barr and Wells, 1990]. (58)

[Barr and Wells, 1993c] Michael Barr and Charles Wells. Corrections to Toposes, Triples and Theories. Available by anonymous FTP from triples.math.mcgill.ca in directory pub/barr, 1993. Corrections and additions to [Barr and Wells, 1985]. (58)

[Bastiani and Ehresmann, 1972] Andrée Bastiani and Charles Ehresmann. Categories of sketched structures. Cahiers de Topologie et Géométrie Différentielle, 13:104–213, 1972. (13)

[Burroni, 1970a] Albert Burroni. Esquisses des catégories à limites et des quasi-topologies. Esquisses Mathématiques, 5, 1970. (43)

[Burroni, 1970b] E. Burroni. Catégories discretement structurées. Esquisses Mathématiques, 5, 1970. (43)

[Coppey and Lair, 1988] L. Coppey and C. Lair. Leçons de théorie des esquisses, partie II. Diagrammes, 19, 1988. (43)

[Ebbinghaus et al., 1984] H.-D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical Logic. Springer-Verlag, 1984. (1)

[Ehresmann, 1966] Charles Ehresmann. Introduction to the theory of structured categories. Technical Report 10, University of Kansas, 1966. (43)

[Ehresmann, 1968a] Charles Ehresmann. Catégories structurées généralisés. Cahiers de Topologie et Géométrie Différentielle, X:139–168, 1968. (43)

[Ehresmann, 1968b] Charles Ehresmann. Esquisses et types des structures algébriques. Bul. Inst. Polit. Iaşi, XIV, 1968. (43)

[Fourman and Vickers, 1986] Michael Fourman and S. Vickers. Theories as categories. In Category Theory and Computer Programming, D. Pitt et al., editors, volume 240 of Lecture Notes in Computer Science, pages 434–448. Springer-Verlag, 1986.

[Goguen and Burstall, 1986] Joseph A. Goguen and R. M. Burstall. A study in the foundations of programming methodology: Specifications, institutions, charters and parchments. In Category Theory and Computer Programming, D. Pitt et al., editors, volume 240 of Lecture Notes in Computer Science, pages 313–333. Springer-Verlag, 1986. (2)

[Goguen and Meseguer, 1982] Joseph A. Goguen and José 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.

[Guitart and Lair, 1980] René Guitart and Christian Lair. Calcul syntaxique des modèles et calcul des formules internes. Diagrammes, 4, 1980.

[Guitart and Lair, 1982] René Guitart and Christian Lair. Limites et colimites pour representer les formules. Diagrammes, 7, 1982.

[Lambek and Scott, 1984] Joachim Lambek and P. Scott. Aspects of higher order categorical logic. In Mathematical Applications of Category Theory, J.W. Gray, editor, volume 30 of Contemporary Mathematics, pages 145–174. American Mathematical Society, 1984.

[Lambek and Scott, 1986] Joachim Lambek and P. Scott. Introduction to Higher Order Categorical Logic, volume 7 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1986.

[Makkai and Paré, 1990] Michael Makkai and R. Paré. Accessible Categories: the Foundations of Categorical Model Theory, volume 104 of Contemporary Mathematics. American Mathematical Society, 1990.

[Makkai and Reyes, 1977] Michael Makkai and Gonzalo Reyes. First Order Categorical Logic, volume 611 of Lecture Notes in Mathematics. Springer-Verlag, 1977.

[Makkai, 1993a] Michael Makkai. Generalized sketches as a framework for completeness theorems, 1993. Preprint, McGill University. (37)

[Makkai, 1993b] Michael Makkai. The syntax of categorical logic, 1993. Preprint, McGill University. (37)

[McDonald and Stone, 1984] John L. McDonald and Arthur Stone. Topoi over graphs. Cahiers de Topologie et Géométrie Différentielle, XXV, 1984. (43)

[Meseguer, 1989] José Meseguer. General logics. Technical Report CSL-89-5, SRI International Computer Science Laboratory, 333 Ravenswood Ave., Menlo Park, CA 94025, USA, 1989.

[Power and Wells, 1992] A.J. Power and Charles Wells. A formalism for the specification of essentially algebraic structures in 2-categories. Mathematical Structures in Computer Science, 2:1–28, 1992. (14, 18)

[Sanella and Tarlecki, 1988] D. Sanella and A. Tarlecki. Building specifications in an arbitrary institution. Information and Control, 76:165–210, 1988.

[Tholen and Tozzi, 1989] Walter Tholen and Anna Tozzi. Completions of categories and initial completions. Cahiers de Topologie et Géométrie Différentielle Catégorique, pages 127–156, 1989. (8)

[Wells and Barr, 1988] Charles Wells and M. Barr. The formal description of data types using sketches. In Mathematical Foundations of Programming Language Semantics, Michael Main et al., editors, volume 298 of Lecture Notes in Computer Science. Springer-Verlag, 1988. (38)

[Wells, 1990] Charles Wells. A generalization of the concept of sketch. Theoretical Computer Science, 70:159–178, 1990. (13, 14, 18)

Atish Bagchi 226 West Rittenhouse Square #702 Philadelphia, PA 19103 atish@math.upenn.edu Charles Wells Department of Mathematics Case Western Reserve University University Circle Cleveland, OH 44106-7058, USA cfw2@po.cwru.edu