There seems to be two competing(?) formalisms for specifying theories: [sketches](http://ncatlab.org/nlab/show/sketch) (as developped by Ehresmann and students, and expanded upon by Barr and Wells in, for example, [Toposes, Triples and Theories](http://www.tac.mta.ca/tac/reprints/articles/12/tr12.pdf)), and the setting of [institutions](http://cseweb.ucsd.edu/~goguen/pps/nel05.pdf). 


But I sometimes get a glimpse that sketches are really a very nice way to specifiy a good category of *signatures*, while institutions are much more model-theoretic. But in works on institutions, the category of signatures is usually highly under-specified (which is quite ironic, really).


So my question really is: what is the relation between Sketches and Institutions? 


A subsidiary question is, why do I find a lot of work relying on institutions, but comparatively less on sketches? [I am talking volume here, not quality.] Did sketches somehow not prove to be effective?



On Sketches and Institutions
So, saying that sketches compete with institutions is not correct because the former is an instance of the latter. The actual content of the question is probably this.


There are two types/styles/paradigms of predicate logic: elementwise (eg, ordinary FOL) and sortwise, or categorical, logic. In the latter, predicates are just sorts, whose intended internal structure (set of tuples) is given by a family of projection arrows pi: P-->Ai (i=1,2..n for n-ary predicate P \subset A1x..xAn) declared to be jointly monic to exclude duplication of tuples. Importantly, a theory interpretation t: T1-->T2 can map sorts Ai in T1 to predicates Qj in T2. Such "mixing" theory interpretations are not considered in the elementwise logic. Thus, the competition is between two styles of predicate logic: sortwise vs. elementwise. Below I'll comment on this, but first let's clarify the institution part of the question. 


There are many elementwise logics (Horn, FOL, etc), each one forms an institution. There are many sortwise logics (formed by sketches of different types), each one also forms an institution (models are sketch morphisms m:T-->U from a theory sketch T to some "semantic" sketch U, usually extracted from a "semantic" category like Set). The actual Jacques' question is (Q1): why a typical work on institution theory is normally motivated by elementwise logic examples, and never by sketches? The dual of this question is (Q2): why institutions are so rarely mentioned/used in the categorical logic literature? 


(Q1). Institutions were invented by Goguen and Burstall to unify the diversity of elementwise logics; I think that they never considered sortwise logics in their papers. The institution theory has been heavily used by the algebraic specification community, whose main motivating example is algebras considered elementwise (like in universal algebra rather than in categorical algebra). Sortwise logics simply did not appear in their contexts. 


(Q2). For a categorical logician, the institution framework may seem unnecessarily too abstract. I mean that abstract institution's functors, sen: Sig-->Set and mod:Sig^op-->Cat, have quite concrete origin for a sketch logic. Since both sentences (diagrams) and models are arrows, functors sen and mod are given by, respectively, post- and pre-composition of these arrows with signature moprhisms. On the other hand, the institution theory does not take into account the concreteness of models (they have underlying sets), which is crucial for "real" model theory (and algebraic logic a la Henkin-Monk-Tarski). 


Now about "competition" sortwise vs. elementwise logic. Different contexts may need one or the other, or both. For example, in my application area -- model-driven software engineering --- sortwise setting is very convenient and actually widely sped in practice (of course, implicitly :). However, only considering universal predicates (limits, colimits,...) would be too heavy and very inconvenient. What is needed is the possibility to consider arbitrarily sortwise predicates in syntax, but specify their semantics elementwisely (with FOL or the like) rather than by universal properties. This idea leads to a version of Makkai's generalized sketches described in [1]. The paper discusses advantages of generalized sketches over Ehresnmann's sketches in software engineering applications, and shows that generalized sketches form an institution.


[1] Diskin and Wolter, A Diagrammatic Logic for Object-Oriented Visual Modeling. ENTCS, Volume 203 Issue 6, November, 2008 


