An Institution-Independent Generalization of
Tarski’s Elementary Chain Theorem
Daniel Găină and Andrei Popescu
Şcoala Normală Superioară, Bucharest??
gaina daniel@yahoo.com, uuomul@yahoo.com

Abstract. We prove an institutional version of Tarski’s Elementary
Chain Theorem applicable to a whole plethora of “first-order-accessible”
logics, which are, roughly speaking, logics whose sentences can be constructed from atomic formulae by means of classical first-order connectives and quantifiers. These include the unconditional equational, positive, (Π ∪ Σ)0n , and full first-order logics, as well as less conventional
logics, used in computer science, such as hidden or rewriting logic.

Keywords: institution, elementary morphism, elementary chain property.

1Introduction

The notion of elementary embedding is an important one in classical first-ordermodel theory [4]. Elementary chains (i.e., chains of elementary embeddings) are
known to be a fundamental proof tool for results regarding preservation of satisfaction, axiomatizability, Robinson consistency, Craig interpolation [4], saturated
models, stability, categoricity in power [30], and many others. The extension ofelementary embeddings to infinitary logics [18, 21, 17] reveals the need in mathematical logic for accommodating this notion in other logical systems too. And
the monograph [18] actually shows that this is a natural and very fruitful thing
to do.
The present paper introduces and studies abstract notions of elementaryembedding and elementary chain, in the framework of institutions [14], andpoints out many particular cases. Two aspects motivate and justify our study:– the mentioned importance of elementary embeddings in model theory;– the logic-independent status of our concepts and results.
Besides its intrinsic abstract model-theoretic contribution, our study might be ofinterest for the theory of formal specifications, where a logic-independent view isdesirable for as long as possible in the specification process, and where structural??

Also: Department of Fundamentals of Computer Science, Faculty of Mathematics,
University of Bucharest.

properties usually approachable by means of elementary chains, such as Craig
interpolation or axiomatizability, are crucial.
Institutions are abstract logical frameworks which provide a category of signatures (languages) and signature morphisms (language translations), and, foreach signature, a set of sentences, a category of models, and a satisfaction relation. Sentences have translations, and models have reducts, along signaturemorphisms; the translations and reducts express the sentence- and model- modifications under change of notation from one language to another. Satisfaction
is required to be invariant under change of notation. More abstract than thegeneral logics of [1], institutions were introduced as frameworks for building
model theory for computer science, in a logic-independent way. Thus generalinstitutional results were applicable to the diversity of logical systems used incomputer science. Besides their great generality, another important feature of
institutions, not present, or poorly present, in other abstract frameworks, is theflexible support for language translations. This feature, particularly useful in formal specification and the semantics of programming languages, is also interestingfrom a logical point of view. As shown in [34, 35, 7, 10, 8, 6] and other places, signature morphisms (language translations) turn out to be a very insightful tool
for finding concrete structure in the core of abstract logic. For example, any
institution hides inside a “first-order logic”, which can be uncovered by meansof basic sentences, logical connectives, and quantifications over some signaturemorphisms (see Sections 2 and 3).1
Our institutional notion of elementary embedding (that we call “elementarymorphism”) also uses signature morphisms in an essential way, by defining elementarity as preservation of satisfaction in expansions along certain signaturemorphisms. Recall that, classically, an elementary embedding between two modhels A and B of the same language is a model-embedding A → B such that foreach formula e(x1 , . . . , xn ) and each sequence a1 , . . . , an ∈ A, A |= e(a1 , . . . , an )iff B |= e(h(a1 ), . . . , h(an )). Because of the existence of negations, the “iff” above
can be replaced by “implies”. In order to abstract away this concept, we follow
an idea originating in [34] which treats (non-closed) Σ-formulae as sentences insignature “extensions” ϕ : Σ → Σ 0 . And we use quasi-representable signaturemorphisms [6] to capture the requirement that the “extension” only adds “constants”. (ϕ is quasi-representable if, for each A0 ∈ |Mod(Σ 0 )|, the canonical functor A0 /Mod(ϕ) : A0 /Mod(Σ 0 ) → A0ϕ /Mod(Σ) is an isomorphism of categories;
hence giving a Σ 0 -morphism of source A0 is equivalent to giving a Σ-morphismof source A0 ϕ . This situation has the following intuitive explanation: all theh“extra items” of Σ 0 w.r.t. Σ being constant symbols, a Σ-morphism A → B canhave only one Σ 0 -expansion of given source A0 .) Quasi-representability of signature morphisms is a weakening of the concept of representability introducedin [7]. By fixing a class Q of quasi-representable signature morphisms, we call ahΣ-morphism A → B Q-elementary if for each signature morphism ϕ : Σ → Σ 0
1Compare this natural appearance of a first-order sublogic with the need to explicitly
postulate the existence of such a sublogic in the context of general logics of [1].

2h0

in Q, each ϕ-expansion A0 → B 0 of h, and each Σ-sentence e0 , A0 |= e0 implies
B 0 |= e0 . (See Section 4 for a detailed motivation of this definition.)
One can alternatively define elementary morphisms by elementary diagrams.
Classically, the elementary diagram [4] EDg(A) of a model A is the set of all
sentences in Σ(A) (the language Σ of A extended with all elements of A ashconstants), true in A. Then a model-inclusion A → B is elementary iff EDg(A) ⊆EDg(B). Thanks to a recent concept of institutional diagram [8], we can also
define institutionally elementary morphisms by diagrams (we abbreviate these as
d-elementary morphisms). The diagrams of [8] provide, for each signature Σ andΣ-model A, a parameterized signature extension ιΣ (A) : Σ → ΣA and a selfparameterized ιΣ (A)-expansion of A. In addition, the diagrams are “functorial”,
i.e., they have corresponding structure for signature- and model- morphisms;hin particular, any Σ-morphism A → B yields a signature morphism ιΣ (h) :ΣA → ΣB such that ιΣ (A); ιΣ (h) = ιΣ (B). We call h d-elementary if, for all
ΣA -sentences e0 , AA |= e0 implies BB |= ιΣ (h)(e0 ). d-elementarity is expressible
more compactly than Q-elementarity, but requires an amount of rather evolved
extra structure on institutions.
Here is the structure of this paper. Section 2 recalls some notions regarding
categories, institutions, and diagrams. Section 3 discusses and exemplifies theconcepts, central in this paper, of (finitely) representable and (finitely) quasirepresentable signature morphism. Section 4 introduces elementary (model-)morphisms w.r.t. a class of quasi-representable signature morphisms. Section
5 proves an institutional version of Tarski’s Elementary Chain Theorem, in thefollowing slightly stronger form: elementary morphisms are closed under directed
colimits. Section 6 introduces an alternative, diagrammatic version of elementarymorphism and shows its equivalence to the previous notion under certain mild
conditions (diagrams being in the considered class of quasi-representable morphisms and another condition that we call normality). Some concluding remarks
end the paper.

2

Preliminaries

Categories
We assume that the reader is familiar with basic categorical notions like functor, natural transformation, colimit, comma category, etc. A standard textbook
on the topic is [19]. We are going to use the terminology from there, with a few
exceptions that we point out below. We use both the terms “morphism” and “arrow” to refer morphisms of a category. Composition of morphisms and functors
is denoted using the symbol “;” and is considered in diagrammatic order.
Let C and C 0 be two categories. Given an object A ∈ |C|, the comma categoryof objects in C under A is denoted A/C. Recall that the objects of this categoryhare pairs (h, B), where B ∈ |C| and A −→ B is a morphism in C. Throughouththe paper, we might let either (A −→ B, B) or (h, B) indicate objects in A/C.
3

A morphism in A/C between two objects (h, B) and (g, D) is just a morphismfB −→ D in C such that h; f = g in C. There exists a canonical forgetful functor
between A/C and C, mapping each (h, B) to B and each f : (h, B) → (g, D)
to f : B → D. Also, if F : C 0 → C is a functor, A ∈ |C|, A0 ∈ |C 0 |, andu
A → F (A0 ) is in C, then there exists a canonical functor u/F : A0 /C 0 → A/Chmapping each (A0 → B, B) to (u; F (h), F (B)) and each f : (h, B) → (g, D)
to F (f ) : (u; F (h), F (B)) → (u; F (g), F (D)). If C = C 0 and F is the identity
functor 1C , we write u/C instead of u/F ; and if F (A0 ) = A and u = 1A , we write
A0 /F instead of u/F .
Let C and S be two categories such that S is small. A functor D : S → C isalso called a diagram. We usually identify a diagram D : S → C with its image
in C, D(S). A cocone of D is a natural transformation µ : D =⇒ V between thefunctor D and [the constant functor mapping all objects to V and all morphisms
to 1V ]; V is an object in C, the vertex of the colimit, and the components of µ
are the structural morphisms of the colimit. Any partially ordered set (I, ≤) canbe regarded as a category in the obvious way, with the arrows being pairs i ≤ j.
A non-empty partially ordered set (I, ≤) is said to be directed if for all i, j ∈ I,
there exists k ∈ I such that i ≤ k and j ≤ k, and is called a chain if the order ≤is total. A diagram defined on a directed set (on a chain) shall be called directed
diagram (chain diagram), and a colimit of such a diagram directed colimit (chain
colimit). A final subset of a directed partially ordered set (I, ≤) is a subset K of
I such that for all i ∈ I, there exists k ∈ K such that i ≤ k. For instance, giveni ∈ I, Ii = {j ∈ I | i ≤ j} is a final subset of (I, ≤). A sub-diagram of a directed
diagram D : (I, ≤) → C is the restriction of D to (K, ≤), where K is a subset of(I, ≤); the sub-diagram is said to be final if K is final. An object A in a category
C is called finitely presented if for each directed diagram D : (I, ≤) → C withµihcolimit {Di → B}i∈I , and for each morphism A → B, there exists j ∈ I andg
A → Dj such that g; µj = h.
Let C 0 be a subcategory of C. C 0 is called a broad subcategory if it contains all
the objects of C. C 0 is said to be closed under directed colimits (chain colimits)
if for any directed diagram (chain diagram) D : (I, ≤) → C such that [for eachµii ≤ j in I, D(i ≤ j) is in C 0 ], any colimit {Di → B}i∈I of D has all the structural
00morphisms µi in C . C is said to be closed under pushouts if for each pushout
h

h

h0

h0

2
1
1
0 2
0
0
0
(A2←A
→A
1 , A2 →A ←A1 ) in C, h1 is in C whenever h1 is in C . Note that thenotion of “closed under” that we adopt is stronger for pushouts than for directedor chain colimits. The following lemma is proved in [19].

Lemma 1 Let (I, ≤) be a directed set, C a category, D : (I, ≤) → C a diagram,µiµi
and {Di → A}i∈I its colimit. If K is a final subset of (I, ≤), then {Di → A}i∈K
is a colimit of the corresponding final sub-diagram of D.
Institutions
Institutions were introduced in [14] with the original goal of providing an abstract, logic-independent framework for algebraic specifications of computer sci4

ence systems. By isolating the essence of a logical system in the abstract satisfaction relation, these structures achieve an appropriate level of generality forthe development of abstract model theory, as shown by a whole series of (oldand new) papers: [34–36, 31, 32, 7, 8, 10, 9, 13, 27]. See also [26] for an up-to-date
discussion on institutions as abstract logics.
An institution [14] consists of:
1. a category Sign, whose objects are called signatures.
2. a functor Sen : Sign → Set, providing for each signature a set whose elements are called (Σ-)sentences.
3. a functor Mod : Sign → Catop , providing for each signature Σ a category whose objects are called (Σ-)models and whose arrows are called(Σ-)morphisms.
4. a relation |=Σ ⊆ |Mod(Σ)|×Sen(Σ) for each Σ ∈ |Sign|, called (Σ-)satisfaction,such that for each morphism ϕ : Σ → Σ 0 in Sign, the satisfaction condition
M 0 |=Σ 0 Sen(ϕ)(e) iff Mod(ϕ)(M 0 ) |=Σ eholds for all M 0 ∈ |Mod(Σ 0 )| and e ∈ Sen(Σ). Following the usual notational
conventions, we sometimes let ϕ denote the reduct functor Mod(ϕ) and let
ϕ denote the sentence translation Sen(ϕ). When M = M 0ϕ we say that M 0
is a ϕ-expansion of M , and that M is the ϕ-reduct of M 0 ; and similarly formodel morphisms.
For all the following concepts related to institutions that we recall below, thereader is referred to [14] unless some other place is explicitly indicated.
Let Σ be a signature. Then,– for each E ⊆ Sen(Σ), let E ∗ = {M ∈ |Mod(Σ)| | M |=Σ e for all e ∈ E}.
– for each class M of Σ-models, let M ∗ = {e ∈ Sen(Σ) | M |=Σ e for all
M ∈ M}.
With no danger of confusion, we let • denote any of the two compositions ∗∗of the two operators ∗. Each of the two bullets is a closure operator. When E
and E 0 are sets of sentences of the same signature Σ, we let E |=Σ E 0 denotethe fact that E ∗ ⊆ E 0∗ . The relation |=Σ between sets of sentences is called the(Σ-)semantic consequence relation (notice that it is written just like the satisfaction relation). If E 0 = {e0 } , we might write E |=Σ e0 . In order to simplify
notation, we usually write |= instead of |=Σ , for both the satisfaction relationand the semantic consequence relation. Two sentences e and e0 are called equivalent, denoted e ≡ e0 , if {e}∗ = {e0 }∗ . Dually, two models M and M 0 are called
elementary equivalent, denoted M ≡ M 0 , if {M }∗ = {M 0 }∗ .
An institution is called semi-exact [22] if the model functor Mod : Sign →Catop preserves pushouts. Semi-exactness implies the following amalgamation
ϕ2

ϕ1

ϕ0

ϕ0

1
0 2
←Σ1 ):
property for any pushout of signature morphisms (Σ2 ←Σ →Σ1 , Σ2 →Σ
for any M1 ∈ |Mod(Σ1 )|, M2 ∈ |Mod(Σ2 )| such that M1ϕ1 = M2ϕ2 , there exists
a unique model M 0 ∈ |Mod(Σ 0 )| such that M 0 ϕ02 = M1 and M 0 ϕ01 = M2 . An

5analogous property is implied about model morphisms. An institution is called
liberal on signature morphisms if the functor Mod(ϕ) has a left adjoint for eachsignature morphism ϕ.
A presentation is a pair (Σ, E), where E ⊆ Sen(Σ). A theory is a presentation(Σ, E) with E closed, i.e., with E • = E. One usually calls “presentation” or“theory” only the set E, and not the whole pair (Σ, E). A presentation morphism
ϕ : (Σ, E) → (Σ 0 , E 0 ) is a signature morphism ϕ : Σ → Σ 0 such that ϕ(E) ⊆ E 0• .
A presentation morphism between theories is called theory morphism. For apresentation (Σ, E), we let Mod(Σ, E) denote the category of all Σ-models A
such that A |= E.
A sentence ρ ∈ Sen(Σ) is called basic [7] if there exists a Σ-model Mρ suchthat, for all Σ-models M , M |= ρ iff there exists a morphism Mρ → M . If, inaddition, Mρ is a finitely presented object in Mod(Σ), ρ is called finitary basic [7].
Basic sentences tend to be the starting building blocks for sentences in concrete
institutions. For instance, in the institution of first-order predicate logic FOPL
(see below the examples of institutions), conjunctions of ground atoms are basic.
In this paper, we shall be interested in institutions whose sentences are accessible
from basic sentences by means of several first-order constructs; hence it suffices
to identify enough basic sentences, like the conjunctions of ground atoms above,in order to ensure accessibility. However, the concept of basic sentence turns out
to be quite comprehensive in concrete cases; for instance, existentially quantified
atoms are also basic in FOPL. The attribute “finitary” is usually equivalent, in
concrete cases, to the property that the sentence has only a finite number ofsymbols. All basic sentences in FOPL are also finitary basic, because FOPL isa “finitary” logic; this is not the case of the institution of infinitary first-order
predicate logic IFOPL, where basic sentences with an infinite number of symbols
can be constructed by means of infinite conjunctions of atoms.
The sentences of an institution I can be naturally extended with first-orderlike constructions [34]: if ϕ : Σ → Σ 0 , ρ, δ ∈ Sen(Σ),Vρ0 ∈ WSen(Σ 0 ), and E ⊆Sen(Σ), one can build the sentences ¬ρ, δ ∧ ρ, δ ∨ ρ, E, E, (∀ϕ)ρ0 , (∃ϕ)ρ0
by means of negation, conjunction, disjunction, arbitrary conjunction, arbitrary
disjunction, universal and existential quantification (over signature morphisms)
respectively, with the following semantics for each Σ-model M :– M |= ¬ρ iff M 6|= ρ;– M |= δ ∧ ρ iff M |= δ and M |= ρ;– M |= δV∨ ρ iff M |= δ or M |= ρ;– M |= W E iff M |= e for each e ∈ E;
– M |= E iff M |= e for some e ∈ E;
– M |= (∀ϕ)ρ0 iff M 0 |= ρ0 for each ϕ-expansion M 0 of M ;– M |= (∃ϕ)ρ0 iff M 0 |= ρ0 for some ϕ-expansion M 0 of M .
It might be the case that the newly constructed sentences are equivalent tosome existing sentences in I. The notion of a class of sentences closed undereither one of the above constructions (e.g., under conjunction, or under universal
quantification over a morphism ϕ) should be clear. An institution is said to admit
negation if the class of all its sentences is closed under negation.
6

Examples of institutions
1. FOPL - the institution of (many-sorted) first-order predicate logic (withequality). The signatures are triplets (S, F, P ), where S is the set of sorts,
F = {Fw,s }w∈S ∗ ,s∈S is the (S ∗ × S -indexed) set of operation symbols, andP = {Pw }w∈S ∗ is the (S ∗ -indexed) set of relation symbols. If w = λ, anelement of Fw,s is called a constant symbol,
S or a constant. By aS slight notational abuse, we let F and P also denote (w,s)∈S ∗ ×S Fw,s and w∈S ∗ Pw respectively. A signature morphism between (S, F, P ) and (S 0 , F 0 , P 0 ) is a triplet
ϕ = (ϕsort , ϕop , ϕrel ), where ϕsort : S → S 0 , ϕop : F → F 0 , ϕrel : P →P 0 such that ϕop (Fw,s ) ⊆ Fϕ0 sort (w),ϕsort (s) and ϕrel (Pw ) ⊆ Pϕ0 sort (w) for all(w, s) ∈ S ∗ × S. When there is no danger of confusion, we may let ϕ denoteeach of ϕsort , ϕrel and ϕop . Given a signature Σ = (S, F, P ), a Σ-model A isa triplet A = ({As }s∈S , {Aw,s (σ)}(w,s)∈S ∗ ×S,σ∈Fw,s , {Aw (R)}w∈S ∗ ,R∈Pw ) interpreting each sort s as a set As , each operation symbol σ ∈ Fw,s as a function
Aw,s (σ) : Aw → As (where Aw stands for As1 × . . . × Asn if w = s1 . . . sn ), andeach relation symbol R ∈ Pw as a relation Aw (R) ⊆ Aw . When there is no danger of confusion we may let Aσ and AR denote Aw,s (σ) and Aw (R) respectively.
Morphisms between models are the usual Σ-homomorphisms, i.e., S-sorted functions that preserve the structure. The Σ-sentences are obtained from atoms, i.e.,equality atoms t1 = t2 , where t1 , t2 ∈ (TF )s ,2 or relational atoms R(t1 , . . . , tn ),where R ∈ Ps1 ...sn and ti ∈ (TF )si for each i ∈ {1, . . . , n}, by applying for a
finite number of times:– negation, conjunction, disjunction;– universal or existential quantification over finite sets of constants (variables).
Satisfaction is the usual first-order satisfaction and is defined using the naturalinterpretations of ground terms t as elements At in models A. The definitionsof functors Sen and Mod on morphisms are the natural ones: for any signaturemorphism ϕ : Σ → Σ 0 , Sen(ϕ) : Sen(Σ) → Sen(Σ 0 ) translates sentences symbolwise, and Mod(ϕ) : Mod(Σ 0 ) → Mod(Σ) is the forgetful functor.
2. (Π ∪ Σ)0n - the fragment of FOPL containing only sentences that areequivalent to sentences in prenex normal form that have at most n alternatedblocks of quantifiers (universal and existential). Within a given signature, thementioned set of sentences actually puts together two well-known types of firstorder sentences: Πn0 and Σn0 [4].
3. PFOPL [6] - the institution of partial first-order predicate logic, an extension of FOPL whose signatures Σ = (S, F, F 0 , P ) contain, besides relation and(total) operation symbols (in F and P ), partial operation symbols too, in F 0 .
Models of course interpret the symbols in F 0 as partial operations of appropriate
ranks. Σ-model morphisms h : A → B are S-sorted functions which commute
with the total operations and relations in the usual way, and with the partial
operations σ ∈ Fs01 ...sn ,s in the following way: for each (a1 , . . . , an ) ∈ As1 ...sn , if
2

TF is the ground term algebra over F .

7Aσ (a1 , . . . , an ) is defined, then so is Bσ (hs1 (a1 ), . . . , hsn (an )), and in this case thelatter is equal to hs (Aσ (a1 , . . . , an )). A signature morphism between (S, F, F 0 , P )and (S0 , F0 , F00 , P0 ) is a FOPL-signature morphism ϕ : (S, F ∪F 0 , P 0 ) → (S0 , F0 ∪F00 , P00 ) such that, for each σ ∈ F , it holds that ϕop (σ) ∈ F0 . Thus signature morphisms are allowed to map partial operation symbols to total operation symbols,
but not vice versa. There exist two kinds of atoms: (existential) equality atomst = t0 and relational atoms R(t1 , . . . , tn ), having syntax just like at FOPL. An
equality atom t = t0 holds in a model A when both terms are defined and equal(At = At0 ). A relational atom R(t1 , . . . , tn ) holds when all terms ti are defined
and their interpretations Ati stay in relation AR . The sentences are obtained
from atoms just like in the case of FOPL (quantification over variables is allowedin the usual sense, which corresponds to considering the quantified variables as
new total constants). Note that other kinds of sentences usually considered inpartial algebraic frameworks can be expressed here: definedness, t ↓, as t = t;strong equality, t =s t0 (either both t and t0 are undefined, or both are definedand equal), as (¬ t ↓ ∧ ¬ t0 ↓) ∨ t = t0 ; weak equality, t =w t0 (if both t and t0 are
defined, then they are equal), as (¬ t ↓) ∨ (¬ t0 ↓) ∨ t = t0 . The functor Mod isdefined similarly to the case of FOPL.
4. PA - the institution of partial algebra, a fragment of PFOPL having signatures without relation symbols. Partial algebras and their applications wereextensively studied in [28] and [3].
5. IFOPL - the institution of infinitary first-order logic, an infinitary extension of FOPL, which allows conjunction on arbitrary sets of sentences. This
logical system is known under the name L∞,ω [21, 20] and plays an importantrole in categorical logic.
6. IFOPLα (where α is an infinite cardinal) - a fragment of IFOPL, admitting
only conjunction on sets of sentences with cardinal smaller than α. This logicalsystem is usually called Lα,ω [18]. Note that IFOPLω is FOPL.
7. PosFOPL - the institution of positive first order predicate logic, a fragmentof FOPL, with sentences constructed by means of ∧, ∨, ∀, ∃, but not negation ¬.
Here ∨ and ∃ are no longer reducible to ∧ and ∀ or vice versa. Positive sentences
are defined and studied for example in [4, 25].
8. EQL - the institution of equational logic [14], a fragment of FOPL, with norelation (only operation) symbols, and with sentences constructed from atoms
only by means of universal quantification (no logical connectives).
9. EQLN - a minimal extension of EQL with negation, allowing sentences
obtained from atoms and negations of atoms through only one round of quantification, either universal or existential, over a set of variables. More precisely,
all sentences have the form (Q X)t1 k t2 , where Q ∈ {∀, ∃} and k ∈ {=, 6=}. Notethat this institution admits negation.
10. RWL - the institution of (unconditional) rewriting logic. It has the same
signatures as EQL, but models have in addition a preorder relation on eachsort carrier, compatible with the operations, and model morphisms have to be
increasing w.r.t. these preorders. The sentences are usual equations as in EQL
and transitions (∀X)t → t0 , with → interpreted as the model preorder. This8

logic cannot be seen as a fragment of FOPL, due to the built-in nature of thepreorder on models. Rewriting logic was introduced in [23] with models having acategorical structure where arrows express different transitions between states; asimplified and more amenable version of this logic, which forces this categoricalstructure to be a preorder, is used in specification languages such as CafeObj[11] or Maude [5]; this simplified version was considered here.
11. OSL - the institution of order-sorted (equational) logic [29], an extensionof EQL where each signature has a partial order on the set of sorts. Thus asignature is a triplet (S, ≤, F ), where (S, ≤) is a partially ordered set and (S, F )is an EQL-signature. A (S, ≤, F )-model is an (S, F )-model in EQL subject totwo additional requirements:– for each s, s0 ∈ S with s ≤ s0 , it holds that As ⊆ As0 ;– for each (w, s), (w0 , s0 ) ∈ S ∗ × S such that w = s1 . . . sn , w0 = s01 . . . s0n , si ≤s0i , and s ≤ s0 , and each σ ∈ Fw,s ∩ Fw0 ,s0 , it holds that Aw,s (σ) : Aw → As
0
restricts and corestricts Aw0 ,s0 (σ) : Aw → As0 .
A (S, ≤, F )-morphism between A and B is a (S, F )-morphism in EQL, h : A →B, such that for all s, s0 ∈ S with s ≤ s0 , it holds that hs restricts and corestricts
hs0 . Given a signature Σ = (S, ≤, F ), one can construct the ground term Σalgebra TΣ similarly to the case of EQL, just that one needs to consider the
subsort relationship ≤ too. An (S, ≤, F )-sentence is an equation (∀X)t = t0 ,where X is an S-sorted set of variables and t, t0 ∈ T(S,≤,F ∪X) .3 Satisfaction of
a sentence by a model is defined in the obvious way. The functor Mod acts justlike in the case of EQL.
12. ML - the institution of (unconditional) membership equational logic, an
extension of EQL which calls the usual sorts ”kinds”, and allows on each kind aset of sorts that are to be interpreted, on models, as subsets of the kind carrier.
Thus a signature is a triplet (K, {Sk }k∈K , F ), where (K, F ) is an EQL-signatureand for each kind k ∈ K, Sk is the set of sorts for this kind. Besides equations,this logic also has membership assertions: (∀X)t : s, where t ∈ (TΣ (X))k ands ∈ Sk , meaning that ”t is of sort s”. This logic, introduced in [24], can beseen as a fragment of FOPL which only uses unary relation symbols and has
only universally quantified atoms as sentences. As shown in [24], ML naturally
embeds (a variation of) OSL.
13. EHL - the institution of extended hidden logic. The signatures are triplets(H, V, F ), where:– H is the set of hidden sorts;– V is the set of visible sorts, V ∩ H = ∅;– (H ∪ V, F ) is an EQL-signature (i.e., F is an (H ∪ V )∗ × (H ∪ V )-indexed
set of operation symbols).
The (H, V, F )-models are the usual (H ∪V, F )-models from EQL. For a model A,
one defines its behavioral equivalence ≡A to be the least congruence on A which
3

The variables in X are interpreted as new constants.

9

is an identity on visible sorts. The (H, V, F )-morphsism are the (H ∪ V, F )morphisms from EQL that preserve behavioral equivalence. There are two kinds
of atoms: (usual) equality atoms t = t0 and behavioral equality atoms t ≡ t0 .
Satisfaction of equality atoms is the usual first-order satisfaction. For a (H, V, F )model A, A |= t ≡ t0 iff Ac[x1 ←a1 ,...,xn ←an ,z←t] = Ac[x1 ←a1 ,...,xn ←an ,z←t0 ] for eachsort v ∈ V , each sequence x1 , . . . , xn of variables of various sorts, each context
c in TF ({x1 , . . . , xn , z}) of sort v, and each sequence a1 , . . . , an of elements in Aof appropriate sorts. (Here a context is a term with only one occurrence of thevariable z; z is assumed to have the same sort as t and t0 . Also, for instance c[x1 ←a1 , . . . , xn ← an , z ← t] is a ground (H ∪ V, F )-term parameterized by elementsin A, and Ac[x1 ←a1 ,...,xn ←an ,z←t] is its natural interpretation as an element in A.)
All sentences are constructed from atoms by means of first-order connectives andquantifiers just like in the case of FOPL (quantification is allowed over variablesof both hidden and visible sorts). A signature morphism between (H, V, F ) and(H 0 , V 0 , F 0 ) is an EQL-signature morphism ϕ : (H ∪ V, F ) → (H 0 ∪ V 0 , F 0 ) suchthat:
– ϕ(V ) ⊆ V 0 , ϕ(H) ⊆ H 0 ;– for each (w0 , s0 ) ∈ (H 0 ∪ V 0 )∗ × (H 0 ∪ V 0 ) such that w0 contains a sort inϕsort (H), and σ 0 ∈ Fw0 0 ,s0 , there exists σ ∈ F such that ϕop (σ) = σ 0 .
On signature morphisms, the functors Mod and Sen act as in the case of EQL.
The above description of EHL was adapted from [8]. See [15] for details about
hidden logic, and [2] for the description of (a variation of) full first-order hidden
logic.
14. HL - [16, 12] the institution of hidden logic, a fragment of EHL, withsentences constructed from atoms only by means of universal quantification (nological connectives).

3

Representable and quasi-representable signaturemorphisms

The institutional notions of representable and quasi-representable signature morphisms are abstract concepts meant to capture the phenomena of quantification
over (sets of) first-order variables. Both notions start from the fact that semantics of quantification in first-order-like logics can be given in terms of signatureextensions: M |=(S,F,P ) (∀X)e (M |=(S,F,P ) (∃X)e ) iff M 0 |=(S,F ∪X,P ) e for each(for some) (S, F ∪ X, P )-expansion M 0 of M . Thus, in order to reach first-order
quantification institutionally, one needs to define somehow what “injective signature morphism that only adds constant symbols” (such as ι : (S, F, P ) →(S, F ∪ X, P )) means.
Definition 2 A signature morphism ϕ : Σ →Σ 0 is called:– representable [7], if there exists a Σ-model Mϕ (called the representation ofϕ) and an isomorphism of categories Iϕ : Mod(Σ 0 ) → Mϕ /Mod(Σ) such that
Iϕ ; U = Mod(ϕ), where U : Mϕ /Mod(Σ) → M od(Σ) is the usual forgetful
functor;10

– finitely representable [7], if it is representable and Mϕ is a finitely presented
object in Mod(Σ);– quasi-representable [6], if for each A0 ∈ |Mod(Σ 0 )|, the canonical functor
A0 /Mod(ϕ) : A0 /Mod(Σ 0 ) → A0ϕ /Mod(Σ) is an isomorphism of categories;– finitely quasi-representable [6], if it is quasi-representable and for each colhi,jµi

imit (Ai → A)i∈I of a directed diagram of Σ-models (Ai → Aj )i,j∈I,i≤j andeach ϕ-expansion A0 of A, there exists an index i ∈ I and a ϕ-expansion µ0i
of µi .
The notion of representability is built on the intuition that, in FOPL, an
expansion of a Σ = (S, F, P )-model A over a signature inclusion ι : Σ → Σ 0 =(S, F ∪ X, P ) that only adds constants can be viewed as a pair (M, v), wherev : X → M is a function interpreting the new constants in X, and furthermore
as a pair (M, v), where v : TΣ (X) → M is a model-morphism.4 Hence ι isrepresented by TΣ (X). And ι is finitely representable, i.e., TΣ (X) is finitely
presented in Mod(Σ), if X is finite.
On the other hand, quasi-representability follows the intuition that the abovehsignature inclusion ι does not allow multiple expansions of Σ-morphisms A → B
00having a fixed source A (where A is a ι-expansion of A). This is because A0
already “indicates”, via h, how the constants in X should be interpreted in thetarget model B 0 of a presumptive ι-expansion h0 of h; and of course h0 has to be
identical, as a function, to h. Thus ι is also quasi-representable. And again, ι isfinitely quasi-represented if X is finite. Intuitively, if we regard directed colimitsof Σ-models as “unions”, all the interpretations in the “union model” A of thefinite number of constants in X will eventually be reached by one of the members
Ai of the union; hence the “inclusion” of Ai into A has a ι-expansion.
For most concrete institutions (at least for those admitting initial objects inthe categories of models, like our examples 1-14), the notions of representability
and quasi-representability coincide, as shown by the below lemma.
Lemma 3 [6] Let ϕ : Σ →Σ 0 be a signature morphism. Then [ϕ is (finitely) quasirepresentable and Mod(Σ) has an initial object] iff ϕ is (finitely) representable.
It is shown in [6] that quasi-representable signature morphisms create directed colimits. Throughout the paper, we are going to use intensively a similar
property:
Lemma 4 Let ϕ : Σ → Σ 0 be a quasi-representable signature morphism and let
fi,j

µi

(Ai → Aj )i,j∈I,i≤j be a directed diagram in Mod(Σ) with colimit (Ai → A)i∈I .
Also, let k ∈ I, Ik = {i ∈ I | k ≤ i}, and B a ϕ-expansion of Ak . Then0fi,jthere exists a directed diagram (A0i → A0j )i,j∈Ik ,i≤j in Mod(Σ 0 ), with colimitµ0(A0i →i A0 )i∈Ik , such that:
4TΣ (X) is the term algebra over variables X and operations in F , with all relationsin P empty.

11

– A0k = B;0
is a ϕ-expansion of fi,j ;– for each i, j ∈ Ik with i ≤ j, fi,j0
– for each i ∈ Ik , µi is a ϕ-expansion of µi .
Proof:
0For each i ∈ Ik , we define (fk,i: B → A0i , A0i ) to be (Ak /Mod(ϕ))−1 (fk,i :0
Ak → Ai , Ai ). In particular, for i = k, we have A0k = B and fk,k= 1B . Also,0
for each i, j ∈ Ik with k < i ≤ j, we define fi,j to be (Ak /Mod(ϕ))−1 (fi,j :0fi,j(fk,i , Ai ) → (fk,j , Aj )). Then Dg 0 = (A0i → A0j )i,j∈Ik ,i≤j is a directed diagramfi,jin Mod(Σ 0 ) and its ϕ-reduct is Dg = (Ai → Aj )i,j∈Ik ,i≤j . Now we define (µ0k :B → A0 , A0 ) to be (Ak /Mod(ϕ))−1 (µk : Ak → A, A) and, for each i ∈ Ik , µ0i toµ0be (Ak /Mod(ϕ))−1 (µi : (fk,i , Ai ) → (µk , A)). Then CC 0 = (A0i →i A0 )i∈Ik is a
µi
cocone of Dg 0 , and the ϕ-reduct of CC 0 is CC = (Ai → A)i∈Ik . The fact that
CC 0 is an actual colimit for Dg 0 follows at once by the quasi-representability of ϕ:ν0ν 0 ϕifor any cocone (A0i →i A00 )i∈Ik of Dg 0 , we get that its reduct (A0iϕ →A00ϕ )i∈Ik
is a cocone of Dg; thus if one takes u to be the universal arrow from CC to

ν 0ϕ

i
A00ϕ )i∈Ik (according to Lemma 1), then (Ak /Mod(ϕ))−1 (u : (µk , A) →(A0iϕ →ν0(νk0 ϕ , A00ϕ )) is the desired universal arrow from CC 0 to (A0i →i A00 )i∈Ik .
q.e.d.
The next lemma shows that (quasi-)representable signature morphisms behave well under composition and pushouts.
Lemma 5 [6]1. (Finitely) quasi-representable signature morphisms form a subcategory of
Sign.
2. (Finitely) representable signature morphisms form a subcategory of Sign.
3. If the institution is semi-exact, then the class of (finitely) quasi-representablesignature morphisms is closed under pushouts.
4. If the institution is semi-exact and liberal on signature morphisms, then theclass of (finitely) representable signature morphisms is closed under pushouts.
Of course, representability and quasi-representability are only abstract approximations for “injective morphisms that only add constants”. What will be
relevant for the results of this paper is that in all our examples 1-14 of institutions, (quasi-)representable signature morphism include the desired types ofmorphisms. Formally, let ϕ : Σ → Σ 0 be a signature morphism in any of theexamples 1-14 of institutions. We say that ϕ is an injective signature morphismthat only adds constants if the following conditions hold: ϕsort is bijective, ϕrelis bijective, ϕop is injective, and F 0 − ϕop (F ) contains only (total) operation
symbols. (Here, F and F 0 stand for the sets of all (partial and total) operation
symbols of Σ and Σ 0 respectively.) If in addition F 0 − ϕop (F ) is finite, we saythat ϕ is an injective signature morphism that only adds finitely many constants.
12

Proposition 6 In any of the examples 1-14 of institutions, all injective signature morphisms that only add (finitely many) constants are (finitely) representable, hence also (finitely) quasi-representable. Moreover, in each case, the(broad) subcategory of Sign of such morphisms is closed under pushouts.
Proof:
The fact that such morphisms are (finitely) representable can be shown usingarguments very similar to the ones for FOPL. The only slightly more exotic cases
are PFOPL, PA, OSL, RL, HL, and EHL; however, in each case the algebra freely
generated by a set of (total) variables exists in any signature. The cases of HL andEHL actually require a small separate discussion. Let (H, V, F ) be a signature ineither of the two institutions. Since each free algebra TF (X) has its behavioral
equivalence equal to the identity, every EQL-morphism with source TF (X) isalso an EHL- and HL- morphism, thus an EHL- or HL- signature morphismthat only adds (finitely many) constants X is indeed (finitely) represented by
TF (X).
As for closure under pushouts, this follows easily from the fact that, in the
category of sets and functions, the subcategory of injective functions is closed
under pushouts.
q.e.d.
Although not strictly needed in this paper, but helpful for getting an idea
on how close the above mentioned approximation is, we recall a concrete characterization of representable (and quasi-representable) signature morphisms in
FOPL.
Proposition 7 [33] Let ϕ : Σ = (S, F, P ) → Σ 0 = (S 0 , F 0 , P 0 ) be a signaturemorphism in FOPL. Then the following are equivalent:
1. ϕ is representable;
2. ϕ is quasi-representable;
3. ϕsort and ϕrel are bijective, and for all (w0 , s0 ) ∈ S 0∗ × S 0 with w0 6= λ, forall σ 0 ∈ Fw0 0 ,s0 , there exists a unique σ ∈ F such that ϕop (σ) = σ 0 (in otherwords, ϕ is bijective w.r.t. all items except constant symbols).
Moreover, the above three conditions stay equivalent if we add the word “finitely”
to the first two and add the requirement that F 0 − ϕop (F ) be finite to the third.

4

Elementary MorphismshIn classical first-order logic [4], an injective model morphism A → B is called anelementary embedding if one of the following equivalent conditions holds:
1. for each formula e(x1 , . . . , xn ) and each sequence a1 , . . . , an ∈ A, A |=e(a1 , . . . , an ) iff B |= e(h(a1 ), . . . , h(an ));2. for each formula e(x1 , . . . , xn ) and each sequence a1 , . . . , an ∈ A, A |=e(a1 , . . . , an ) implies B |= e(h(a1 ), . . . , h(an )).
13

The notion of elementary embedding has an immediate generalization to the
many-sorted case FOPL; and it was extended to cope with infinitary first-orderlogics too [18, 17]. Our next institutional generalization reads the concept of elementary embedding in the following way: the morphism h preserves sentences inany language extending with constants the original language, regardless of the actual interpretation of these constants. Notice that the two alternative definitionsof elementary embeddings listed above are equivalent thanks to the existence ofnegations in full first-order logic; however, this is not the case in less expressive
logics, such as PosFOPL or EQL. We prefer to consider the second variant and interpret elementarity as a sentence preservation property rather than a refinementof elementary equivalence. This subjective choice is motivated by our belief thattaking into consideration the direction of the arrow h in the definition is a more
fruitful approach. In an institution, the “languages extended with constants”
are captured by quasi-representable signature morphisms ϕ having as source thegiven language/signature, and satisfaction inside such an extended language iscaptured by usual satisfaction by ϕ-expansions. To keep the discussion generaland to avoid certain intricacies in the particular cases resulting from considering
all quasi-representable, or representable, signature morphisms, we parameterize
our definition by a class Q of quasi-representable signature morphisms. Thushlet A → B be a Σ-morphism. Formulae e(x1 , . . . , xn ) are expressed by usual
sentences e0 in signatures Σ 0 , where ϕ : Σ → Σ 0 is a signature morphism in Q.
Satisfaction of such sentences e0 ∈ Sen(Σ 0 ) makes sense in ϕ-expansions of A
and B, expansions which are to be seen as models together with some designatedconstants.5 However, asking that “A0 |= e0 implies B 0 |= e0 ” for all ϕ-expansions
A0 and B 0 of A and B and for all e0 ∈ Sen(Σ 0 ) is not appropriate, since thequoted implication should be required only about constants in A and B connected through h; the connection is realized by first considering ϕ-expansions h0
of h.
The injectivity assumption in the definition of elementary embedding forclassical first-order logic is superfluous. We did not consider it in the above discussion; this could be seen as yet another subjective choice, meant to emphasize
once more the idea of sentence preservation, this time to the prejudice of the algebraic property of model embedding. This choice has an important terminologicalconsequence: we define and study “elementary morphisms”, and not “elementaryembeddings”, although the elementary morphisms yield in particular the FOPLelementary embeddings.
For the whole section, we fix an institution I and a broad subcategory Q
of Sign (i.e., a class of signature morphisms containing all identity morphisms
and closed under composition), consisting of quasi-representable signature morphisms. In particular, by taking further mild assumptions on I such as semiexactness or liberality on signature morphisms, according to Lemma 5, possible
choices for Q are given by either of the following four types of signature mor5

Recall from Section 3 the connection between quasi-representable signature morphisms and first-order variables/constants.

14

phisms: quasi-representable, finitely quasi-representable, representable, finitely
representable.
hDefinition 8 Let Σ be a signature. A Σ-morphism A → B is called Q-elementaryh0

if for all signature morphisms ϕ : Σ → Σ 0 in Q, ϕ-expansions A0 → B 0 of h,and sentences e0 ∈ Sen(Σ 0 ), it holds that A0 |= e0 implies B 0 |= e0 .
Remark 9
1. Because each morphism in Q is quasi-representable, in Definition 8 the ϕexpansion h0 of h is uniquely determined by the ϕ-expansion A0 of A.
2. If the institution admits negations, then the condition in Definition 8 can beequivalently stated by replacing “A0 |= e0 implies B 0 |= e0 ” with “A0 |= e0 iff
B 0 |= e0 ”.
Let us see what our general concept of Q-elementary morphism becomes forour examples 1-14 of institutions. In what follows, for all these institutions, weshall simply call elementary morphisms the Q-elementary morphisms with Q being the category of injective signature morphisms that only add constants. (Notethat in logics with finite sentences, such as FOPL and all its fragments, elementarity w.r.t. arbitrary signature morphisms that only add constants is equivalent
to elementarity w.r.t. morphisms that only add finitely many constants; this isbecause just a finite set of the newly added constants are contained in a given
sentence.) Known and relatively well-studied cases are the following:– for FOPL, the elementary embeddings from (the many-sorted version of)classical model theory [4];– for PA, the elementary embeddings of partial algebras [3];– for IFOPL and IFOPLα , the L∞,w - and Lα,w - elementary embeddings frominfinitary model theory [18, 21, 17];
– for (Π ∪ Σ)01 , the existentially closed embeddings [17];– for (Π ∪ Σ)0n , the Σn0 -extensions [4].
Up to our knowledge, elementary embeddings for the other examples of institutions were not considered so far in the literature. However, such notions
are meaningful instances of the logic-independent concept of elementary morphism that we propose here. In each case, an elementary morphism is one that
preserves satisfaction of all sentences with elements of the source model as parameters. The next proposition gives some expected properties of Q-elementarymorphisms.
Proposition 10 Let χ : Σ → Σ 0 be a signature morphism. Then the following
hold:
1. The Q-elementary morphisms in Mod(Σ) form a subcategory of Mod(Σ).
2. Assume that the institution has pushouts of signatures and is semi-exact, andh0that Q is closed under pushouts. If A0 → B 0 is a Q-elementary morphism inMod(Σ 0 ), then h0χ is also Q-elementary;
15

h0

h

3. If χ is in Q, A → B is a Q-elementary morphism in Mod(Σ), and A0 → B 0
is a χ-expansion of h, then h0 is also Q-elementary.
Proof:
1: If A ∈ |Mod(Σ)|, then 1A is Q-elementary because any expansion of 1A along
a quasi-representable signature morphism is an identity model-morphism itself.
ghLet now A → B and B → C be two Q-elementary morphisms in Mod(Σ) and let
f = h; g. In order to show that f is Q-elementary, let ϕ : Σ → Σ0 be a signaturef0
morphism in Q and A0 → C0 a ϕ-expansion of f . Let h0 : A0 → B0 such that
(A0 , h0 ) = (A0 /Mod(ϕ))−1 (A, h). Let g0 = (A0 /Mod(ϕ))−1 (g : (A, h) → (A, f )).
Then h0 ; g0 = f0 . Since h and g are Q-elementary, it follows that {A0 }∗ ⊆{B0 }∗ ⊆ {C0 }∗ .
h

2: Let A → B denote the χ-reduct of h0 . In order to prove h elementary, leth
ϕ : Σ → Σ0 be a signature morphism in Q and A0 →0 B0 a ϕ-expansion
ϕ0

χ0

of h. Consider the pushout Σ 0 → Σ1 ← Σ0 of the signature morphism spanχϕ(Σ 0 ←Σ →Σ0 ). Then ϕ0 is also in Q. By semi-exactness, since h0 and h0 haveha common reduct (that is, h), they also have a common expansion A1 →1 B1 in
Mod(Σ1 ). Because h0 is elementary, {A1 }∗ ⊆ {B1 }∗ . Finally, using the satisfaction condition, we get {A0 }∗ ⊆ {B0 }∗ .
3: Immediate from the definition of Q-elementary morphisms and the fact that
Q is closed under composition.
q.e.d.

5

Elementary Chain Property

Throughout this section, we again fix an institution I and a broad subcategory
Q of Sign consisting of quasi-representable signature morphisms.
A Q-elementary chain is a chain diagram in Mod(Σ) for some signature Σ,
such that all its morphisms are Q-elementary. The elementary chain property(parameterized by Q and abbreviated Q-ECP) asks that, for each colimit ofeach Q-elementary chain, all the structural morphisms be Q-elementary. In otherwords, it asks that for each signature Σ, the subcategory of Mod(Σ) of Qelementary morphisms be closed under chain colimits. We are going to provethat, under appropriate accessibility assumptions on sentences, Q-ECP holds inan arbitrary institution. But first we need to consider some technical concepts
and results.
We say that a sentence e ∈ Sen(Σ) for some signature Σ is preserved (reflected) by directed colimits of Q-elementary morphisms, abbreviated Q-preservedfi,j(reflected), if for each directed diagram of Q-elementary Σ-morphisms (Ai →µi
Aj )i,j∈I,i≤j with colimit (Ai → A)i∈I and each k ∈ I, Ak |= e implies A |= e
(A |= e implies Ak |= e respectively).
Proposition 11 The class of sentences preserved by directed colimits of Qelementary morphisms
16

1. contains all basic sentences,
2. is closed under arbitrary conjunction and disjunction,
3. is closed under existential quantification over morphisms in Q,
4. is closed under universal quantification over finitely quasi-representable morphisms in Q.
Proof:
fi,jLet e ∈ Sen(Σ), (Ai → Aj )i,j∈I,i≤j a directed diagram of Q-elementaryµi
Σ-morphisms, with colimit (Ai → A)i∈I , and let k ∈ I. Assume that Ak |= e.
We need to prove that A |= e.
1: Assume e is a basic sentence. Since Ak |= e, there exists a Σ-morphism
Me → Ak , hence, by composition with µk , we find a morphism Me → A, implying A |= e.
V
2: Assume e is equivalent to E, where E ⊆ Sen(Σ) such that for all e0 ∈ E, e0
is Q-preserved. Since Ak |= e, it holds that Ak |= e0 for all e0 ∈ E, hence A |= e0
for all e0 ∈ E, hence A |= e. The proof for disjunction goes similarly.
3: Assume e is equivalent to (∃ϕ)e0 , where ϕ : Σ → Σ 0 is in Q and e0 is Qpreserved. Then there exists a ϕ-expansion A0k of Ak such that A0k |= e0 . By0fi,jLemma 4, there exists a directed diagram (A0i → A0j )i,j∈Ik ,i≤j in Mod(Σ 0 ), with
µ00colimit (A0i →i A0 )i∈Ik such that, for each i, j ∈ Ik with i ≤ j, fi,j
is a ϕ-expansion00of fi,j and µi is a ϕ-expansion of µi . In particular, A ϕ = A. According to Propo0
sition 10.(3), each fi,jis Q-elementary. Applying the fact that e0 is Q-preserved,00
we obtain that A |= e , hence A |= (∃ϕ)e0 , i.e., A |= e.
4: Assume e is equivalent to (∀ϕ)e0 , where ϕ : Σ → Σ 0 is a finitely quasirepresentable signature morphism in Q and e0 is Q-preserved. Let A0 be a ϕexpansion of A. We need to show that A0 |= e0 . Because ϕ is finitely quasirepresentable, there exists q ∈ I and a ϕ-expansion ξ 0 : A0q → A0 of µq .
Since (I, ≤) is directed, there exists p ∈ I such that q ≤ p and k ≤ p. Thus,f0

because fk,p is Q-elementary, we get Ap |= e. Define (A0q → A0p , A0p ) to be
fq,p(Aq /Mod(ϕ))−1 (Aq → Ap , Ap ) and ν 0 to be (Aq /Mod(ϕ))−1 (µp : (Aq , fq,p ) →(Aq , µq )). Note that ν 0 : A0p → A0 . By Lemma 4 applied to the index p,0fi,jthere exists a directed diagram (A0i → A0j )i,j∈Ip ,i≤j in Mod(Σ 0 ), with colimitµ00(A0i →i B 0 )i∈Ip , such that, for each i, j ∈ Ip with i ≤ j, fi,j
is a ϕ-expansion
0of fi,j and µi is a ϕ-expansion of µi . Again, Proposition 10.(3) assures us
0that each fi,jis Q-elementary. Since both (ν 0 , A0 ) and (µ0p , B 0 ) are equal to−1(Ap /Mod(ϕ)) (µp , A), it follows that A0 = B 0 and ν 0 = µ0p . Finally, since e0
is Q-preserved and A0p |= e0 (A0p being a ϕ-expansion of Ap ), we obtain that
A0 |= e0 .
q.e.d.

Proposition 12 Assume that the institution admits negation. Then the class ofsentences preserved and reflected by directed colimits of Q-elementary morphisms17

1. contains all finitary basic sentences,
2. is closed under arbitrary conjunction and disjunction, and under negation,
3. is closed under universal and existential quantification over finitely quasirepresentable morphisms in Q.
Proof:
fi,jLet e ∈ Sen(Σ), (Ai → Aj )i,j∈I,i≤j a directed diagram of Q-elementary Σµimorphisms, with colimit (Ai → A)i∈I , and let k ∈ I. We need to prove [Ak |= e
iff A |= e].
1: Assume e is a finitary basic sentence. That Ak |= e implies A |= e follows
from Proposition 11.(1). Therefore let us suppose A |= e, i.e., there exists a
Σ-morphism g : Me → A, and let us show that Ak |= e . Because Me is finitely
presentable, there exists j ∈ I and Σ-morphism h : Me → Aj such that h; µj = g.
Because (I, ≤) is directed, there exists i ∈ I such that k ≤ i and j ≤ i. Then,h;fj,iby the existence of the morphism Me → Ai , it follows that Ai |= e. Moreover,since fk,i : Ak → Ai is Q-elementary and the institution admits negation, we
obtain Ak |= e.
2: Similar to the proof of Proposition 11.(2) for conjunction and disjunction. For
negation, the property is obvious thanks to its symmetry.
3: Because the institution admits negation, universal and existential quantifications are mutually definable. Therefore let us focus on existential quantification. Assume e is equivalent to (∀ϕ)e0 , where ϕ : Σ → Σ 0 is a finitely quasirepresentable morphism in Q and e0 is a Σ 0 -sentence Q-[preserved and reflected].
That Ak |= e implies A |= e follows from Proposition 11.(3). Let us now suppose
A |= (∃ϕ)e0 and let us show that Ak |= (∃ϕ)e0 . We have that A |= ¬(∀ϕ)¬e0 ,which means A 6|= (∀ϕ)¬e0 . By point (2), ¬e0 is Q-[preserved and reflected]. Thus,
by Proposition 11.(4), (∀ϕ)¬e0 is Q-preserved, hence Ak |= (∀ϕ)¬e0 would imply
A |= (∀ϕ)¬e0 , which is a contradiction. Thus Ak |= ¬(∀ϕ)¬e0 , i.e., Ak |= (∃ϕ)e0 .
q.e.d.
Proposition 13 Assume that all sentences of the institution are preserved bydirected colimits of Q-elementary morphisms. Then for each signature Σ, thesubcategory of Mod(Σ) of Q-elementary morphisms is closed under directed colimits.
Proof:fi,jLet (Ai → Aj )i,j∈I,i≤j be a directed diagram in Mod(Σ) such that each
µifi,j is Q-elementary and let (Ai → A)i∈I be its colimit. Let k ∈ I. In order toprove that µk is Q-elementary, let ν 0 : A0k → A0 be a ϕ-expansion of µk and let
e0 ∈ Sen(Σ 0 ) such that A0k |= e0 . By Lemma 4, there exists a directed diagram
0
fi,j

µ0

(A0i → A0j )i,j∈Ik ,i≤j in Mod(Σ 0 ), with colimit (A0i →i B 0 )i∈Ik , such that, for0each i, j ∈ Ik with i ≤ j, fi,j
is a ϕ-expansion of fi,j and µ0i is a ϕ-expansion0of µi . Just like in the proof of Proposition 11.(4), one obtains that each fi,j
is
0
0
0
0
Q-elementary and that A = B and ν = µk . Thus, according to our hypothesis,
A0 |= e0 .
18

q.e.d.
Definition 14 An institution I is called Q-first-order-accessible if one of thetwo below properties holds:
1. All sentences of I are (equivalent to ones) obtained from basic sentences byapplying a finite number of times the following rules:– arbitrary conjunction;– arbitrary disjunction;– existential quantification over morphisms in Q;– universal quantification over finitely quasi-representable morphisms in Q.
2. I admits negation and all sentences of I are (equivalent to ones) obtained
from finitary basic sentences by applying a finite number of times the following rules:– arbitrary conjunction;– arbitrary disjunction;– negation;– existential quantification over finitely quasi-representable morphisms in Q;– universal quantification over finitely quasi-representable morphisms in Q.
Proposition 15 All the examples 1-14 of institutions are Q-first-order-accessible,
where Q is each time the category of injective signature morphisms that only add
constants.
Proof:Let us first see that IFOPL and all its fragments are Q-first-order accessible.
Indeed, for each signature Σ = (S, F, P ), an equality atom t = t0 is finitary basic
thanks to the model TΣ /t = t0 , that is, the (S, F )-algebra TF /t = t0 (a quotientof the ground term algebra over F ) with all the relations in P empty, while a relational atom R(t1 , . . . , tn ) is basic thanks to the model consisting of TF together
with all relations in P empty, except R, which is the singleton {(t1 , . . . , tn )}.
Moreover, quantification over finite or infinite sets of variables are particularcases of quantification over signature morphisms in Q. Thus PosFOPL, EQL,
and ML fall into case 1 of Definition 14, and FOPL, (Π ∪ Σ)0n , IFOPL, IFOPLα ,and EQLN into case 2.
A similar argument as above holds for PFOPL and PA too, since for instancegiven a PA-signature and a set of equality atoms, there exists the initial algebrain the category of algebras satisfying these atoms [3]. And similarly for RWL
and OSL.
As for EHL and HL, one has to notice mainly two things. First, all usual
equality atoms are basic; indeed, the algebra TF /t = t0 has the property that,for each (H, V, F )-model A satisfying the usual equality atom t = t0 , the unique
EQL-morphism between TF /t = t0 and A preserves behavioral equivalence, hence
it is also an EHL- and HL- morphism. Second, the behavioral equality atoms
are equivalent to (infinite) conjunctions of universallyV quantified usual equality atoms; indeed, it holds that A |= t ≡ t0 iff A |= {(∀{x1 , . . . , xn }) c[z ←t] = c[z ← t0 ] | v ∈ V, x1 , . . . , xn variables, c ∈ TF ({x1 , . . . , xn , z})v context}.
19

Thus HL falls into case 1 of Definition 14. Moreover, EHL falls into case 2,
since although behavioral equality atoms are not finitary, they are neverthelessobtainable from finitary basic sentences by means of the rules of universal quantification over finitely quasi-representable morphisms in Q (i.e., over finite sets
of variables) and arbitrary conjunction.
q.e.d.
Theorem 16. (Elementary Chain Theorem) Assume that the institution is Qfirst-order-accessible. Then for each signature Σ, the subcategory of Mod(Σ) of
Q-elementary morphisms is closed under directed colimits. In particular, theinstitution enjoys the Q-ECP .
Proof:
Follows immediately: for case 1 of Definition 14 from Propositions 11 and 13,
and for case 2 from Propositions 12 and 13.
q.e.d.
The separation on two cases in Definition 14 covers mainly the following
situations: the institution I either admits negation, or has no negation - intermediate cases are not covered. Some important examples of institutions to which
our Theorem 16 does not apply are all variations of Horn logic - in fact, for thoseinstitutions, we conjecture that the elementary chain property does not hold.
Corollary 17 All the examples 1-14 of institutions enjoy the Q-ECP.
Note that Theorem 16 is applicable to a whole variety of other logics resulted
from other different combinations of connectives and quantifiers. An interesting
example which takes full advantage of Proposition 11 is a version of positive
infinitary first-order logic admitting arbitrary conjunction and disjunction, existential quantification over arbitrary sets of variables, and universal quantification
over finite sets of variables. Moreover, the case of fragments of languages (overtransitive sets) in infinitary first-order logic [18] also seems to fall into our framework, provided that one takes the trouble of formalizing this as an institution.

6

Elementary morphisms by diagrams

An alternative definition of elementary embeddings in classical model theory isgiven in terms of elementary diagrams [4, 25]. There, the elementary diagram
EDg(A) of a model A is the set of all sentences in Σ(A) (the language Σ of A
extended with all elements of A as constants), true in A. Then an embeddinghA → B is elementary iff h(EDg(A)) ⊆ EDg(B), where h(EDg(A)) is the obvioustranslation through h of the sentences in EDg(A). The main difference to theoriginal definition (discussed at the beginning of Section 4) is that a language
which includes parameter symbols for the source model, Σ(A), is a priori given
and the desired property is stated locally, in that fixed language. By adapting an existing institutional concept of diagram, we can discuss this alternative
definition in a logic-independent framework.
20Institutional Diagrams
Diagrams are a basic concept in classical model theory [4]. They were first generalized to the institutional framework in [35, 36]; there, it is defined the conceptof abstract algebraic institution, which is an institution subject to some additional natural requirements (like finite-exactness, existence of direct products ofmodels etc.) and enriched with a system of diagrams. The reason for introducing
diagrams there was making all algebras accessible, for specification purposes. In
this paper, we need a more elaborated notion of institutional diagram, defined in[8], which takes into consideration not only models, but also model morphisms.
The concept was introduced under the name “elementary diagram”. For reasons that will be pointed out soon, here we prefer to use, like in [35], the name“positive diagram” instead.
An institution I = (Sign, Sen, Mod, |=) is said to have positive diagrams [8] if
1. for each signature Σ and Σ-model A there exists a signature morphismιΣ (A) : Σ → ΣA and a set EA of ΣA -sentences (called the positive diagram of A) such that Mod(ΣA , EA ) and A/Mod(Σ) are isomorphic by anisomorphism iΣ,A making the following diagram commutative:
iΣ,A/ A/Mod(Σ)
Mod(ΣA , EA )
NNN
q
NNN
qqq
q
NNN
q
q
ιΣ (A) NN
xqqq forgetful'Mod(Σ)

2. ι is “functorial”, i.e., for each signature morphism ϕ : Σ → Σ 0 , each A ∈|Mod(Σ)|, A0 ∈ |Mod(Σ 0 )| and h : A → A0 ϕ in Mod(Σ), there exists a0presentation morphism ιϕ (h) : (ΣA , EA ) → (ΣA
0 , EA0 ) making the following
diagram commutative:ιΣ (A)

Σ

/ ΣA

ϕ


Σ0



ιϕ (h)/ Σ0 0ιΣ 0 (A0 )A

3. i is natural, i.e., for each signature morphism ϕ : Σ → Σ 0 , each A ∈|Mod(Σ)|, A0 ∈ |Mod(Σ 0 )| and h : A → A0 ϕ in Mod(Σ), the following
diagram is commutative:
Mod(ΣA , EA )O

iΣ,A

/ A/Mod(Σ)
Oh/Mod(ϕ)

iΣ 0,A0/ A0 /Mod(Σ 0 )ιϕ (h)0Mod(ΣA
0 , E A0 )21

Here are some notational conventions that we hope will make the reader’s lifeeasier. Let ϕ : Σ → Σ 0 be a signature morphism, A0 ∈ |Mod(Σ 0 )|, and h : A → B
in Mod(Σ). We write ιΣ (h) instead of ι1Σ (h) and ιϕ (A0ϕ ) instead of ιϕ (1(A0ϕ ) ).
Let A be a fixed object in Mod(Σ) and let B, C ∈ |Mod(Σ)| and f : A → B,
g : A → C, u : B → C morphisms in Mod(Σ) such that f ; u = g. Then (f, B) and(g, C) are objects in A/Mod(Σ) and u is also a morphism in A/Mod(Σ) between(f, B) and (g, C). We establish the following notations: Bf = i−1
Σ,A (f, B) (and,u−1−1similarly, Cg = iΣ,A (g, C) ), uf,g = iΣ,A ((f, B) → (g, C)). Thus, for instance,
let f : A → B be a Σ-model morphism. Then f1A ,f is the image through i−1
Σ,Aof the morphism f : (1A , A) → (f, B) in A/Mod(Σ), and has source A(1A ) andtarget Bf . We shall write AA instead of A(1A ) and fA,f instead of f1A ,f .
In classical model theory, ΣA is the signature Σ enriched with all the elementsof A as constants, ιΣ (A) : Σ → ΣA is the inclusion of signatures, and EA is a setof parameterized sentences which hold in A, depending on the considered typeof morphism between models. If arbitrary model-homomorphisms are allowed
as morphisms, like in FOPL, one gets the “positive diagram”; if just modelembeddings are considered, one gets the “diagram”; and only if just elementaryembeddings are allowed, one gets what is classically called “elementary diagram”(see [4] for the pointed standard terminology in classical model theory). Thus theabove institutional definition of diagrams particularizes to elementary diagramsfor classical first-order logic only if a notion of elementary morphism is assumed
as previously defined. However, it is precisely the latter notion that we want tocapture using diagrams. Therefore, we prefer to use the term “positive diagram”,
in accordance to the particularization of the concept to the concrete institution
FOPL, widely accepted as the institution of first-order logic. Thus we view theset of sentences EA as the positive, rather than elementary, diagram of A, but ofcourse keeping for it the same understanding as in [8]: that EA axiomatizes theclass of Σ-morphisms with source A. And we use the term elementary diagram of
A for the set {AA }∗ , of all sentences satisfied by the self-parameterized extension
AA of A.
In [8], there are presented positive diagrams for FOPL, RWL, PA, and HL.
Most institutions that were built starting from “working” logical systems tend
to have elementary diagrams. We next recall the system of positive diagramsfor FOPL. Let Σ = (S, F, P ) be a FOPL-signature and A ∈ |Mod(Σ)|. DefineΣA = (S, FA , P ), where FA extends F by adding, for each s ∈ S, all elements of
As as constants of sort s. Further, we define:– AA ∈ |Mod(ΣA )|, as the ΣA -expansion of A which interprets each constanta ∈ A by a;– EA , as the set of all atoms in Sen(ΣA ) satisfied by AA ;– ιΣ (A), as the signature inclusion of Σ into ΣA ;– the functor iΣ,A : M od(ΣA , EA ) → A/Mod(Σ), as:h• iΣ,A (B 0 ) = (A → B, B), where B = B 0 ιΣ (A) and, for each s ∈ S anda ∈ As , hs (a) = Ba0 .
• iΣ,A (f ) = f .
22

Let ϕ : Σ = (S, F, P ) → Σ 0 = (S 0 , F 0 , P 0 ) be a signature morphism, A ∈|Mod(Σ)|, B ∈ |Mod(Σ 0 )|, and h : A → B ϕ in Mod(Σ). Then the natural0presentation morphism ιϕ (h) : (ΣA , EA ) → (ΣB, EB ) from the definition of
positive diagrams is the following: if e ∈ Sen(ΣA ), then ιϕ (h)(e) is obtained
from e by symbol-wise translation, mapping:– each σ ∈ F into ϕop (σ),– each R ∈ P into ϕrel (R),– for all s ∈ S, each a ∈ As into hs (a),– for all s ∈ S, each variable x : s of sort s into a variable x : ϕsort (s) of sort
ϕsort (s),– each other symbol u that appears in e (e.g., logical connectives and quantifiers) into u.
As a general rule easily seen to hold about positive diagrams, one has that:– if an institution I 0 extends an institution I and has the same category Sign
and functor M od (thus only adds new sentences), then positive diagrams are
inherited by I 0 from I;– if an institution I 0 restricts an institution I, has the same category Sign
and functor M od (thus only restricts the sets of sentences), but I 0 still has
all the sentences in the positive diagrams EA of I, then positive diagrams
are inherited by I 0 from I.
Thus the above described positive diagrams of FOPL are inherited by IFOPL,IF OLP Lα , PosFOPL, EQL, EQLN, ML. The positive diagrams for the othermentioned institutions can be constructed with a similar pattern as those of
FOPL; as remarked in [8], the sentences EA are always the basic sentences satisfied by the model A expanded to ΣA with constants in A pointing to themselves.
For what follows, we fix an institution with positive diagrams, I.
Definition 18 Let Σ be a signature.
1. Given a Σ-model A, the elementary diagram of A is the set {AA }∗ (of ΣA sentences satisfied by AA ).6h

2. A Σ-morphism A → B is called elementary by diagrams (d-elementary) if
one of the following two equivalent conditions holds:– A∗A ⊆ Bh∗ ;∗– ιΣ (h)(A∗A ) ⊆ BB.
That the two conditions in point (2) of the above definition are equivalentfollows from the satisfaction condition together with the fact that, by the naturality of i, BBιΣ (h) = Bh .
Thus we defined elementary morphisms by means of elementary diagrams. Wehcan spell out this definition as follows: A → B is d-elementary if the elementary
diagram of A is embedded, via h, into the elementary diagram of B.
6

Since AA |= EA , the positive diagram of A is included in the elementary diagram of A.

23

The relationship between Q-elementary and d-elementary
The notion of d-elementary morphism is more compact than that of Q-elementarymorphism, but the former needs a lot of further structure on top of the plain
institutional structure. We next provide conditions under which the two concepts are equivalent. For all this section, we fix a broad subcategory Q of Sign
consisting of representable signature morphisms.7
Definition 19 The positive diagrams of I are said to be Q-normal if for each
representable signature morphism ϕ : Σ → Σ 0 (represented by Mϕ ) there exists a
signature morphism χ : Σ 0 → ΣMϕ such that ϕ; χ = ιΣ (Mϕ ) and M od(χ); Iϕ =iΣ,Mϕ .8
In examples 1-14 of institutions, for the usual choice of Q, i.e., to consist of all
injective signature morphisms that only add constants, the signature morphismsιΣ (A) of the positive diagrams are all in Q. Moreover, in each case, the positive
diagrams are also Q-normal. Indeed, for example in FOPL, given an injective
signature morphism ϕ that only adds constants, which we can assume w.l.g. to
be an inclusion Σ = (S, F, P ) → Σ 0 = (S, F ∪X, P ), represented by the Σ-modelTΣ (X), the desired morphism χ such that ϕ; χ = ιΣ (TΣ (X)) is the signatureinclusion (S, F ∪ X, P ) → (S, F ∪ TΣ (X), P ) given by the set inclusion X →TΣ (X). In order to see that the corresponding condition on model categories
holds, let N be a ΣTΣ (X) -model that satisfies ETΣ (X) . Then iΣ,TΣ (X) (N ) = (h :TΣ (X) → N ιΣ (TΣ (X)) , N ιΣ (TΣ (X)) ), where h(t) = Nt for all t ∈ TΣ (X). On
the other hand, Iϕ (N χ ) = (g : TΣ (X) → N ϕ;χ , N ϕ;χ ) = (g : TΣ (X) →N ιΣ (TΣ (X)) , N ιΣ (TΣ (X)) ), where g is the unique Σ-morphism extending the
mapping v : X → N defined by v(x) = Nx for all x ∈ X. Thus, by the freenessof TΣ (X), g = h. Hence the functors M od(χ); Iϕ and iΣ,Mϕ coincide on objects.
That they coincide on morphisms too follows at once from ϕ; χ = ιΣ (TΣ (X)).
Normality of the positive diagrams for the other examples of institutions can beshown similarly to the case of FOPL.
Proposition 20 If the positive diagrams are normal and have each signaturemorphism ιΣ (A) in Q, then any model morphism is Q-elementary iff it is delementary.
Proof:hLet Σ be a signature and A → B a Σ-morphism.
hA
Assume first that h is Q-elementary. Then, since ιΣ (A) is in Q and AA →Bh∗∗
is a ιΣ (A)-expansion of h, we get {AA } ⊆ {Bh } . Thus h is d-elementary.
Conversely, assume that h is d-elementary. Let ϕ : Σ → Σ 0 be a signatureh0amorphism in Q and A0 → B 0 a ϕ-expansion of h. Let (Mϕ → A, A) = Iϕ (A0 ) and
7

Note that we require more than usual for the subcategory Q, namely representability
instead of quasi-representability.
8
Here, we made the slight notational abuse of letting M od(χ) denote the restrictionof M od(χ) : M od(ΣMϕ ) → M od(Σ 0 ) to M od(ΣMϕ , EM ϕ ).

24

b

(Mϕ → B, B) = Iϕ (B 0 ). By the naturality of i we have that hA,h ιΣ (a) = ha,b .9
Since {AA }∗ ⊆ {Bh }∗ , by the satisfaction condition, it follows that {Aa }∗ ⊆{Bb }∗ . Now, by the normality of diagrams, there exists χ : Σ 0 → ΣMϕ suchthat ϕ; χ = ιΣ (Mϕ ) and M od(χ); Iϕ = iΣ,M ϕ . Then M od(χ) = iΣ,M ϕ ; Iϕ−1 ,thus ha,b χ = Iϕ−1 (iΣ,Mϕ (ha,b )) = Iϕ−1 (h) = h0 . Hence Aa χ = A0 and Bb χ = B 0 .
Finally, by the satisfaction condition, we get {A0 }∗ ⊆ {B 0 }∗ .
q.e.d.
Corollary 21 In all the examples 1-14 of institutions (with their mentioned
diagrams), a model morphism is elementary iff it is d-elementary.

7

Concluding remarks

We outline the contributions of the present paper:– introduced an abstract notion of elementary morphism, parameterized by aclass of signature morphisms;– studied the connection between elementary morphisms and positive diagramsin an arbitrary institution, by giving an alternative diagrammatic definitionof elementarity;– showed how the general results particularize to many concrete cases of logical systems, yielding different known results in a unitary fashion, but also
some new results; in particular, the less conventional cases of partial algebra,
hidden logic and rewriting logic fall into our framework.
An open problem that we consider worthwhile is the institutional relationship between elementary morphisms and model-embeddings. Given the fact thatclassically elementary morphisms are also embeddings, a result stating that, under certain assumptions on the expressive power of sentences, all elementarymorphisms are embeddings (where “embeddings” can be defined either strictly
categorically, as subobjects, or by means of inclusion or factorization systems),
would be very desirable.
A more in depth study of elementary morphisms in some particular cases
might also prove to be interesting. Take for instance the equational framework.
In EQL and EQLN, the elementary morphisms do not seem very amenable. It
is not clear to us how they look like. Note that a surjective morphism is always
elementary in EQL, and an elementary morphism has to be injective in EQLN.
The case of HL is even more intricate, and the notion of “elementary behavioral
morphism”, complementing that of bisimulation, is potentially fruitful in thealgebraic study of systems and behavior.
9hA,h : AA → Bh is a morphism in ΣA and ha,b : Aa → Bb is a morphism in ΣMϕ recall the notational conventions about elementary diagrams.

25

8

AcknowledgmentsRăzvan Diaconescu taught us institution-independent model theory, during some
lectures that he held at Şcoala Normală Superioară, Romania. He also readseveral preliminary versions of this paper, and his comments improved the paper
substantially. Our colleagues, especially Traian Şerbănuţă, Marius Petria, andCristian Cucu, pointed out lots of bugs in our proofs and minds w.r.t. elementary
chains, that we hope we managed to correct. Last but not least, our two referees
criticized the paper constructively.

References
1. J. Barwise and J. Feferman. Model-Theoretic Logics. Springer, 1985.
2. M. Bidoit and R. Hennicker. Proving behavioural theorems with standard firstorder logic. In Algebraic and Logic Programming (ALP’94), volume 850 of LNCS,
pages 41–58, 1994.
3. P. Burmeister. A Model Theoretic Oriented Appraoch to Partial Algebras.
Akademie-Verlag Berlin, 1986.
4. C. C. Chang and H. J. Keisler. Model Theory. North Holland, Amsterdam, 1973.
5. M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In
J. Meseguer, editor, Proceedings of the First International Workshop on Rewriting
Logic, volume 4 of Electronic Notes in Theoretical Computer Science, pages 65–89.
Elsevier, 1996.
6. R. Diaconescu. Institution-independent Model Theory. Book draft. (Ask author
for current version at Razvan.Diaconescu@imar.ro).
7. R. Diaconescu. Institution-independent ultraproducts. Fundamenta Informaticae,
55(3-4):321–348, 2003.
8. R. Diaconescu. Elementary diagrams in institutions. Journal of Logic and Computation, 14(5):651–674, 2004.
9. R. Diaconescu. Herbrand theorems in arbitrary institutions. Inf. Process. Lett.,
90:29–37, 2004.
10. R. Diaconescu. An institution-independent proof of Craig interpolation theorem.
Studia Logica, 77(1):59–79, 2004.
11. R. Diaconescu and K. Futatsugi. CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. World Scientific, 1998. AMAST Series in Computing, volume 6.
12. R. Diaconescu and K. Futatsugi. Behavioural coherence in object-oriented algebraic specification. Universal Computer Science, 6:74–96, 2000.
13. D. Găină and A. Popescu. An institution-independent proof of Robinson consistency theorem. Studia Logica. To appear.
14. J. Goguen and R. Burstall. Institutions: Abstract model theory for specificationand programming. Journal of the Association for Computing Machinery, 39(1):95–
146, January 1992.
15. J. Goguen and G. Malcolm. A hidden agenda. Theoretical Computer Science,
245(1):55–101, August 2000.
16. J. Goguen and G. Roşu. Hiding more of hidden algebra. In Formal Methods 1999
(FM’99), volume 1709 of Lecture Notes in Computer Sciences, pages 1704–1719.
Springer-Verlag, 1999.

26

17. J. Hirschfeld and W. Wheeler. Forcing, arithmetic, division rings. Lecture Notes
in Mathematics, (454), 1975.
18. H. J. Keisler. Model Theory for Infinitary Logic. North-Holland, 1971.
19. S. Mac Lane. Categories for the Working Mathematician. Springer, 1971.
20. M. Makkai and R. Paré. Accessible Categories: The Foundations of Categorical
Model Theory. Providence, 1989.
21. M. Makkai and G. Reyes. First order categorical logic. Lecture Notes in Mathematics, (611), 1977.
22. J. Meseguer. General logics. In H.-D. Ebbinghaus et al., editors, Proceedings, Logic
Colloquium 1987, pages 275–329. North-Holland, 1989.
23. J. Meseguer. Conditional Rewriting Logic as a Unified Model of Concurrency.
Theoretical Computer Science, pages 73–155, 1992.
24. J. Meseguer. Membership algebra as a logical framework for equational specification. In Proceedings, WADT’97, volume 1376 of LNCS, pages 18–61. Springer,
1998.
25. J. D. Monk. Mathematical Logic. Springer-Verlag, 1976.
26. T. Mossakowski, J. Goguen, R. Diaconescu, and A. Tarlecki. What is a logic? In
J.-Y. Beziau, editor, Logica Universalis, pages 113–133. Birkhauser, 2005.
27. M. Petria and R. Diaconescu. Abstract Beth definability institutionally. Submitted.
(Ask authors for current version at Razvan.Diaconescu@imar.ro).
28. H. Reichel. Structural Induction on Partial Algebras. Akademie-Verlag Berlin,
1984.
29. G. Roşu. The institution of order-sorted equational logic. Bulletin of EATCS,
53:250–255, 1994.
30. G. E. Sacks. Saturated Model Theory. W. A. Bejamin, Inc., Reading, 1972.
31. A. Salibra and G. Scollo. A soft stairway to institutions. In M. Bidoit and
C. Choppy, editors, Recent Trends in Data Type Specification, volume 655 of Lecture Notes in Computer Science, pages 310–329. Springer-Verlag, 1992.
32. A. Salibra and G. Scollo. Interpolation and compactness in categories of preinstitutions. Math. Struct. in Comp. Science, 6:261–286, 1996.
33. T. Şerbănuţă. Institutional concepts in first-order logic, parameterized specifications, and logic programming. Master Disertation. University of Bucharest, 2004.
34. A. Tarlecki. Bits and pieces of the theory of institutions. In D. Pitt, S. Abramsky,
A. Poigné, and D. Rydeheard, editors, Proceedings, Summer Workshop on Category
Theory and Computer Programming, Lecture Notes in Computer Science, volume240, pages 334–360. Springer, 1986.
35. A. Tarlecki. On the existence of free models in abstract algebraic institutions.
Theoretical Computer Science, 37:269–304, 1986.
36. A. Tarlecki. Quasi-varieties in abstract algebraic institutions. Journal of Computerand System Sciences, 33(3):333–360, 1986.

27