Birkhoff Completeness in Institutions
Mihai Codescu and Daniel Găină
Abstract. We develop an abstract proof calculus for logics whose sentences are ’Hornsentences’ of the form: (∀X)H =⇒ c and prove an institutional generalization of
Birkhoff completeness theorem. This result is then applied to the particular cases ofHorn clauses logic, the ’Horn fragment’1 of preorder algebras, order-sorted algebras
and partial algebras and their infinitary variants.
Mathematics Subject Classification (2000). Primary 03B22; Secondary 03C95, 18A15,
03F03.
Keywords. Proof theory, institutional model theory, Horn sentences, Birkhoff completeness, abstract substitutions.

1. Introduction
In 1935 Birkhoff [3] first prove a completeness theorem for equational logic, in the unsorted case. Goguen and Meseguer [14], giving a sound and complete system of proof
rules for finitary many-sorted equational deduction, generalized the completeness theorem of Birkhoff to the completeness of finitary many-sorted equational logic and provided simultaneously a full algebraization of finitary many-sorted equational deduction.
The unsorted rules can be unsound for many sorted algebras that may have empty carriers(as noticed in [14]), suggesting the idea that generalizations to other variants of equational
logics may imply some difficulties.
The deduction rules introduced in [14] can be presented as in figure 1.
The concept of institution is a category-based model-oriented formalization of theconcept of logical system, including syntax, semantics and satisfaction between them.
Institution-independent model theory provides an abstract approach towards model theory, without a particular underlying logical system. This is important especially in the context of the recent proliferation of logics in computer science, mostly in the area of formal
specification, where it is now a tradition to have an institution underlying each language
or system. This perspective has the advantage of clarifying model theoretic phenomena
and causality relationships between them, allowing thus new fundamental insights andresults even in traditional areas of model theory.

2

Mihai Codescu and Daniel Găină

(Re f lexivity) ` (∀X)t = t(Symmetry) (∀X)t = t 0 ` (∀X)t 0 = t(Transitivity) {(∀X)t = t 0 , (∀X)t 0 = t 00 } ` (∀X)t = t 00
(Congruence) {(∀X)ti = ti0 } ` (∀X)σ(t1 , ...,tn ) = σ(t10 , ...,tn0 )for any σ ∈ Fs1 ...sn →s(Substitutivity) Γ ∪ {(∀X)θSen (c)} ` (∀X)θSen (t) = θSen (t 0 )for each set of conditional equations Γ, for each equation (∀Y )c =⇒ t = t 0 in Γ andfor each substitution θ : Y → TF (X)F IGURE 1. Complete rules for equational logic
We generalize the Birkhoff completeness result to arbitrary institutions obtaining
in a unitary fashion sound and complete systems of proof rules for an entire class oflogics used in computer science such as: Horn clause logic (HCL), the ’Horn fragment’ ofpreorder algebras (Horn(POA)), order sorted algebra (Horn(OSA)) and partial algebras(Horn(PA)).
There are several aspects that motivate and justify our study. One of them is the importance for model theory. Our study isolates the particular aspects of the logics from general ones in order to obtain an abstract completeness which covers many examples suchas the ones mentioned above and also their infinitary versions, HCL∞ , Horn(POA)∞ ,Horn(OSA)∞ and Horn(PA)∞ . This top-down approach is broader, in the sense that it
can also be applied in the case of logics that are not necessarily Horn, such as ”universal”
institutions.
The present paper is also meaningful for computer science. Modern algebraic specification languages (such as CafeOBJ [10], CASL [2], Maude) are rigorously based on
logic, in the sense that each feature and construct in a language can be expressed withina certain logic underlying it. Completeness results have great significance for an operational semantics of executable specification languages. In the context of proliferation ofa multitude of specification languages, these abstract results provide complete systems of
proof rules for the logical systems underlying them.
The paper is organized as follows: Section 2 presents the notions of institutionindependent model theory used in the paper, illustrating each concept in the familiar firstorder logic with equality (FOL). Section 3 introduces the abstract concepts of universaland Horn institution and a generic universal entailment system which is proved soundand complete, under conditions which are also investigated. Section 4 consists of therefinement of the universal entailment system to the particular case of Horn institutions,while Section 5 contains concrete instances of the Birkhoff completeness in several logics,
like HCL, PA, POA, OSA and their infinitary versions. Section 6 concludes the paper anddiscusses the future work.
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[17]. We use both the terms “morphism” and “arrow” to refer morphisms of a category.

Birkhoff Completeness in Institutions

3

Composition of morphisms and functors is denoted using the symbol “;” and is consideredin diagrammatic order.

2. Preliminaries
2.1. Institutions
Institutions were introduced in [13] with the original goal of providing an abstract framework for algebraic specifications of computer science systems. By isolating the essenceof a logical system in the abstract satisfaction relation, which states that truth is invariant
to change of notation or enlargement of context, and leaving open the details of signatures, sentences and models, these structure achieves an appropriate level of generality
for the development of abstract model theory - i.e. independent of the specific nature of
the underlying logic. Many logical notions and results can be developed in an institutionindependent way, to mention just a few: ultraproducts [5], Craig interpolation [7], Robinson consistency [12], saturated models [11], Beth definability [20]. A textbook dedicatedto this topic is under preparation [9].
Definition 1. An institution [13] consists of:
1. a category Sig, whose objects are called signatures.
2. a functor Sen : Sig → Set, providing for each signature a set whose elements arecalled (Σ-)sentences.
3. a functor Mod : Sigop −→ Cat, providing for each signature Σ a category whose objects are called (Σ-)models and whose arrows are called(Σ-)morphisms.
4. a relation |=Σ ⊆ |Mod(Σ)| × Sen(Σ) for each Σ ∈ |Sig|, called (Σ-)satisfaction, suchthat for each morphism ϕ : Σ −→ Σ0 in Sig, 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 ϕ wesay that M 0 is a ϕ-expansion of M, and that M is the ϕ-reduct of M 0 ; and similarly formodel morphisms. When E and E 0 are sets of sentences of the same signature Σ, we let
E |=Σ E 0 denote the fact that M |= E implies M |= E 0 for all Σ-models M. The relation|=Σ between sets of sentences is called (Σ-)semantic consequence relation (notice that it
is written just like the satisfaction relation).
Example 1. First order logic (FOL). The signatures are triplets (S, F, P), where S is theset 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 = λ, an element of Fw→sis called a constantsymbol, or a constant.
By a slight notational abuse, we let F and P
S
S
also denote (w,s)∈S∗ ×S Fw→s and w∈S∗ Pw respectively. A signature morphism between(S, F, P) and (S0 , F 0 , P0 ) is a triplet ϕ = (ϕsort , ϕop , ϕrel ), where ϕsort : S → S0 , ϕop : F → F 0 ,ϕrel : P → P0 such that ϕop (Fw→s ) ⊆ Fϕ0 sort (w)→ϕsort (s) and ϕrel (Pw ) ⊆ Pϕ0 sort (w) for all (w, s) ∈

4Mihai Codescu and Daniel Găină

S∗ × S. When there is no danger of confusion, we may let ϕ denote each of ϕsort , ϕrel andϕop . Given a signature Σ = (S, F, P), a Σ-model M is a triplet M = ({Ms }s∈S , {Mσw,s }(w,s)∈S∗
w×S,σ∈Fw,s , {Mπ }w∈S∗ ,π∈Pw ) interpreting each sort s as a set Ms , each operation symbolσ ∈ Fw→s as a function Mσw,s : Mw → Ms (where Mw stands for Ms1 × . . . × Msn if w =s1 . . . sn ), and each relation symbol π ∈ Pw as a relation Mπw ⊆ Mw . When there is nodanger of confusion we may let Mσ and Mπ denote Mσw,s and Mπw respectively. Morphisms
between models are the usual Σ-homomorphisms, i.e., S-sorted functions that preserve thestructure. The Σ-sentences are defined as the least set of sentences that contains all atoms,
i.e., equality atoms t1 = t2 , where t1 ,t2 ∈ (TF )s 1 or relational atoms π(t1 , . . . ,tn ), whereπ ∈ Ps1 ...sn and ti ∈ (TF )si for each i ∈ {1, . . . , n}, and is closed under:- 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 natural interpretations of ground terms t as elements Mt in models M. The definitions of functors
Sen and Mod on morphisms are the natural ones: for any signature morphism ϕ : Σ → Σ0 ,Sen(ϕ) : Sen(Σ) → Sen(Σ0 ) translates sentences symbol-wise, and Mod(ϕ) : Mod(Σ0 ) →Mod(Σ) is the forgetful functor.
Universal sentences in FOL (UNIV) A universal sentence for a FOL signature(S, F, P) is a (S, F, P)-sentence of the form (∀χ)ρ where ρ is a sentence formed without
quantifiers.
Example 2. Horn Clause logic (HCL). A universal Horn sentence for a FOL signature(S, F, P) is a (universal) sentence of the form (∀X)H ⇒ C, where H is a finite conjunctionof (relational or equational) atoms, C is a (relational or equational) atom, and H ⇒ C is
the implication of C by H. In the tradition of logic programming universal Horn sentences
are known as Horn Clauses. Thus HCL has the same signatures and models as FOL but
only universal Horn sentences as sentences.
By considering the case of empty sets of relational symbols, we obtain the conditional equational logic, CEQL.
Example 3. Preorder algebra (POA). The POA signatures are just the ordinary algebraic
signatures. The POA models are preordered algebras which are interpretations of the signatures into the category of preorders Pre rather than the category of sets Set. This meansthat each sort gets interpreted as a preorder, and each operation as a preorder functor,
which means a preorder-preserving (i.e. monotonic) function. A preordered algebra homomorphism is just a family of preorder functors (preorder-preserving functions) whichis also an algebra homomorphism.
The sentences have two kinds of atoms: equations and preorder atoms. A preorderatom t ≤ t 0 is satisfied by a preorder algebra M when the interpretations of the terms arein the preorder relation of the carrier, i.e. Mt ≤ Mt 0 . Full sentences are constructed fromequational and preorder atoms by using Boolean connectives and first order quantification.
Example 4. Order sorted algebra (OSA) An order sorted signature (S, ≤, F) consistsof an algebraic signature (S, F), with a partial ordering (S, ≤) such that the following
1 T is the ground term algebra over F.
FBirkhoff Completeness in Institutions

5

monotonicity condition is satisfied σ ∈ Fw1 →s1 ∩ Fw2 →s2 and w1 ≤ w2 imply s1 ≤ s2 . A
morphism of OSA signatures ϕ : (S, ≤, F) → (S0 , ≤0 , F 0 ) is just a morphism of algebraic
signatures (S, F) → (S0 , F 0 ) such that the ordering is preserved, i.e. ϕ(s1 ) ≤0 ϕ(s2 ) whenever s1 ≤ s2 .
An order sorted signature (S, ≤, F) is regular if and only if for each σ ∈ Fw1 →s1 andeach w0 ≤ w1 there is a unique least element in the set {(w, s) | σ ∈ Fw→s and w0 ≤ w}.
Fact 1. For regular signatures (S, ≤, F), any (S, ≤, F) has a least sort and the initial(S, ≤, F)-algebra in Mod(S, ≤, F) can be defined as a term algebra, cf. [16].
A partial ordering (S, ≤) is filtered if and only if for all s1 , s2 ∈ S, there is somes ∈ S such that s1 ≤ s and s2 ≤ s. A partial ordering is locally filtered if and only if every
connected component of it is filtered. An order sorted signature (S, ≤, F) is locally filteredif and only if (S, ≤) is locally filtered, and it is coherent signature if and only if it is both
locally filtered and regular. Hereafter we assume that all OSA signatures are coherent.
Given an order sorted signature (S, ≤, F), an order sorted (S, ≤, F)-algebra is a
(S, F)-algebra M such that- s1 ≤ s2 implies Ms1 ⊆ Ms2 , and- σ ∈ Fw1 →s1 ∪ Fw2 →s2 and w1 ≤ w2 imply Mσw1 ,s1 = Mσw2 ,s2 on Mw1 .
Given order sorted (S, ≤, F)-algebras M and N, an order sorted (S, ≤, F)-homomorphism h : M → N is a (S, F)-homomorphism such that s1 ≤ s2 implies hs1 = hs2 on
Ms1 .
Let (S, ≤, F) be a an order sorted signature. We say that the sorts s1 and s2 are in thesame connected component of S if and only if s1 ≡ s2 , where ≡ is the least equivalenceon S that contains ≤. The atoms of the signature (S, ≤, F) are equations of the form
t1 = t2 such that the least sort of the terms t1 and t2 are in the same connected component.
The sentences are formed from these equations by means of boolean connectives andquantification over (first order) variables. Order sorted algebras were extensively studiedin [15] and [16].
Example 5. Partial algebra (PA). A partial algebraic signature is a tuple (S, T F, PF)such that (S, T F ∪ PF) is an algebraic signature. Then T F is the set of total operations
and PF is the set of partial operations. A morphism of PA signatures ϕ : (S, T F, PF) →(S, T F 0 , PF 0 ) is just a morphism of algebraic signatures (S, T F ∪ PF) → (S, T F 0 ∪ PF 0 )such that ϕ(T F) ⊆ T F 0 and ϕ(PF) ⊆ PF 0 .
A partial algebra M for a PA signature (S, T F, PF) is just like an ordinary algebra but
interpreting the operations of PF as partial rather than total functions, which means thatMσ might be undefined for some arguments. A partial algebra homomorphism h : M → N
is a family of (total) functions {hs : Ms → Ns }s∈S indexed by the set of sorts S of thesignature such that hw (Mσ (a)) = Nσ (hs (a)) for each operation symbol σ : w → s and eachstring of arguments a ∈ Mw for which Mσ (a) is defined.
s
The sentences have three kinds of atoms: definedness def( ), strong equality = andeexistence equality =. The definedness de f (t) of a term t holds in a partial algebra Mswhen the interpretation Mt of t is defined. The strong equality t1 = t2 holds when bothterms are undefined or both of them are defined and are equal. The existence equality

6

Mihai Codescu and Daniel Găinăet1 = t2 holds when both terms are defined and are equal. The sentences are formed fromthese atoms by means of boolean connectives and quantification over total (first order)evariables. Notice that each definedness atom def(t) is semantically equivalent with t = tse
and any strong equality t1 = t2 is semantically equivalent with (def(t1 )∨def(t2 )) ⇒ t1 = t2 .
Partial algebras and their applications were extensively studied in [21] and [4].
Notation 1. Notice that in most of the standard cases, a logic comes with a notion of
atomic sentence, with the help of with the formulas of the logic are built. We can restrict
the sentences of some logic I, formalized as an institution, to the atomic ones, and denote
this sub-institution Atomic(I). We also denote by Horn(I) the sub-institution of I formedby restricting the sentences to universal Horn sentences built over the atomic formulae ofI.
Example 6. Infinitary Horn clause logic (HCL∞ ) This is the infinitary extension of HCL
obtained by allowing the hypothesis parts of a Horn clauses (∀X)H ⇒ C to consist of
infinitary conjunctions of atoms.
Similarly we may define Horn(POA)∞ , Horn(OSA)∞ , Horn(PA)∞ .
Example 7. Institution of presentations. A presentation is a pair (Σ, E) consisting of asignature Σ and a set E of Σ-sentences. A presentation morphism ϕ : (Σ, E) → (Σ0 , E 0 ) isa signature morphism ϕ : Σ → Σ0 which maps the axioms of the source presentation tological consequences of the target presentation: E 0 |= ϕ(E). Presentation morphisms forma category, denoted PresI . The model functor Mod of an institution can be extended fromthe category of its signatures Sig to a model functor from the category of its presentations
Pres, by mapping a presentation (Σ, E) to the full subcategory Mod pres (Σ, E) of Mod(Σ)
consisting of all Σ-models s atisfying E. The correctness of the definition of Mod pres isguaranteed by the satisfaction condition of the base institution; this is easy to check. This
leads to the institution of presentations I pres = (Sig pres , Sen pres , Mod pres , |= pres ) over thebase institution I where- Sig pres is the category PresI- Sen pres (Σ, E) = Sen(Σ), and- for each (Σ, E)-model M and any Σ-sentence e, M |= pres e iff M |= e.
Definition 2. A set of sentences E ⊆ Sen(Σ) is called basic if there exists a Σ-model
ME such that, for all Σ-models M, M |= E if and only if there exists a homomorphism
ME → M.
A set of sentences E is epic basic if it is basic and the morphism ME → M is unique.
Basic sentences were introduced in [24] under the name of “ground positive elementary sentences”. We prefered to use the terminology from [5].
The concept of epic basic sentence constitute the best institution-independent approximation of the actual atoms of the logic. One of the important consequences is that,
directly from the definition, we obtain that epic basic sets of sentences always admit initialmodels.
Lemma 1. Any set of atomic sentences in FOL, POA, OSA and PA is epic basic.

Birkhoff Completeness in Institutions

7

Proof. In any FOL the basic model ME for a set E of atomic (S, F, P)-sentences is theinitial model for E. This is constructed a follows: on the quotient (TF )=E of the term model
TF by the congruence generated by the equational atoms of E, we interpret each relation
symbol π ∈ P by (ME )π = {(t1 /=E , . . . ,tn /=E ) | π(t1 , . . . ,tn ) ∈ E}. A similar argument as
the preceding holds for POA and OSA.
In PA for a set E of atomic (S, T F, PF)-sentences we define SE to be the set if subterms appearing in E. We also define TT F (SE ) to be the partial algebra that is generated
by the set of terms SE . The basic model ME will be the quotient of this algebra by thepartial congruence induced by the equalities from E.
Internal logic. The following institutional notions dealing with logical connectives
and quantifiers were defined in [23].
Definition 3. Let Σ be a signature in an institution,- a Σ-sentence ¬e is a (semantic) negation of e when M |= ¬e if and only if M 2 e,
for each Σ-model M, and- a Σ-sentence e1 ∧ e2 is a (semantic) conjunction of e1 and e2 when M |= e1 ∧ e2 if
and only if M |= e1 and M |= e2 , for each Σ-model M.
- a Σ-sentence (∀χ)e0 is a (semantic) universal χ-quantification of e0 over χ when
M |= (∀χ)e0 if and only if M 0 |= e0 for all χ-expansion M 0 of M.
Very often quantification is considered only for a restricted class of signature morphisms. For example, quantification in FOL considers only the finitary signature extensions with constants. For a class D ⊆ Sig of signature morphisms, we say that the institution has universal D -quantification when for each χ : Σ → Σ0 in D , each Σ-sentence has auniversal χ-quantification.
Representable signature morphisms. The institutional notion of representable signature morphisms is meant to capture the phenomena of quantification over (sets of)first-order variables. The notion starts from the fact that semantics of quantification in
first-order-like logics can be given in terms of signature extensions: 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 definesomehow what ”injective signature morphism that only adds constant symbols” (such asι : (S, F, P) ,→ (S, F ∪ X, P)) means.
Definition 4. ([5]) A signature morphism χ : Σ → Σ0 is called:- representable, 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(Σ) → Mod(Σ) is the usual forgetful functor;

8

Mihai Codescu and Daniel Găină

- finitely representable, if it is representable and Mχ is a finitely presented object 2
in Mod(Σ);
Since 1Mχ is the initial object of the category Mχ /Mod(Σ), the Σ0 -model−1(iχ ) (1Mχ ) is the initial object of the category Mod(Σ0 ). We denote by OΣ0 the Σ0 -model(iϕ )−1 (1Mχ ). The notion of representability is built on the intuition that, in FOL, 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), where v : 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. Hence ι is represented by TΣ (X). And ι is finitely representable,i.e., TΣ (X) is finitely presented in Mod(Σ), if X is finite.
Remark 1. If χ : Σ → Σ0 is a representable signature morphism then for each Σ0 -model
M 0 , the canonical functor determined by the reduct functor Mod(χ) is an isomorphism ofcomma categories: M 0 /Mod(Σ0 ) ∼= (M 0 χ )/Mod(Σ). .
hThis means that each Σ-homomorphism M 0 χ → N admits an unique χ-expansion
h000
M 0 → N 0 = i−1
χ (h) where h : iϕ (M ) → (iϕ (M ); h) is regarded as a morphism in Mϕ /Mod(Σ).

M 0 ϕbhiϕ (M 0 )/N?
iϕ (M 0 );hMϕχLemma 2. Let Σ → Σ0 be a representable signature morphism. Then the following preχsentation morphism (Σ, E) → (Σ0 , E 0 ) is also representable (as a signature morphism in
I pres ) if the set of sentences E 0 is epic basic.
Proof. Since E 0 is epic basic the Σ0 -model ME 0 is the initial object in the
category Mod(Σ0 , E 0 ). Thus, Mod(Σ0 , E 0 ) ∼= ME 0 /Mod(Σ0 ) and by the above remark0
ME 0 /Mod(Σ0 ) ∼= ME 0 χ /Mod(Σ). We denote by iEχ the composition of isomorphisms
0Mod(Σ0 , E 0 ) ∼= ME 0 /Mod(Σ0 ) ∼= ME 0 χ /Mod(Σ) and we have iEχ ;U = Mod(χ).
The following Lemma is proven in [5].
Lemma 3. The reduct functor corresponding to representable signature morphisms preserves directed co-limits of models.
Substitutions. Given a FOL signature (S, F, P) and two sets of new constants, calledfirst order variables X and Y , a first order (S, F, P)-substitution from X to Y consists of a
mapping θ : X → TF (Y ) of the variables X with F-terms over Y .
2 An object A in a category C is called finitely presented ([1]) ifµ

g- for each directed diagram D : (J, ≤) → C with co-limit {Di →i B}i∈J , and for each morphism A −→ B,githere exists i ∈ J and A −→Di such that gi ; µ j = g,
- for any two arrows gi and g j as above, there exists i ≤ k, j ≤ k ∈ J such that gi ; D(i ≤ k) = g j ; D( j ≤k) = g.

Birkhoff Completeness in Institutions

9

On the semantics side, each (S, F, P)-substitution θ : X → TF (Y ) determines a functor Mod(θ) : Mod(S, F ∪Y, P) → Mod(S, F ∪ X, P) defined by- Mod(θ)(M)x = Mx for each sort s ∈ S, or operation symbol x ∈ F, or relation
symbol x ∈ P, and- Mod(θ)(M)x = Mθ(x) , i.e. the evaluation of the term θ(x) in M, for each x ∈ X.
On the syntax side, θ determines a sentence translation function Sen(θ) : Sen(S, F ∪X, P) → Sen(S, F ∪ Y, P) which in essence replaces all symbols from X with the corresponding (F ∪Y )-terms according to θ.
- Sen(θ)(t1 = t2 ) is defined as θ(t) = θ(t 0 ) for each (S, F ∪ X, P)-equation t1 = t2 ,where θ : TF (X) → TF (Y ) is the unique extension of θ to an F-morphism (θ is replacing
variables x ∈ X with θ(x) in each F ∪ X-term t).
- Sen(θ)(π(t1 , . . . ,tn )) is defined as π(θ(t1 ), . . . , θ(tn )) for each (S, F ∪X, P)-relational
atom π(t1 , . . . ,tn ).
- Sen(θ)(ρ1 ∧ρ2 ) is defined as Sen(θ)(ρ1 )∧Sen(θ)(ρ2 ) for each conjunction ρ1 ∧ρ2of (S, F ∪ X, P)-sentences, and similarly for the case of any other logical connectives.
- Sen(θ)((∀Z)ρ) is defined as (∀Z)Sen(θZ )(ρ) for each (S, F ∪ X ∪ Z, P)-sentence
ρ, where θZ is the trivial extension of θ to an (S, F ∪ Z, P)-substitution.
Note that we have extended the notations used for the models functor Mod and forthe sentence functor Sen from the signatures to the first order substitutions. This notational
extension is justified by the following satisfaction condition given by Proposition 1
Proposition 1. For each FOL-signature (S, F, P) and each (S, F, P)-substitution θ : X →TF (Y ),
Mod(θ)(M) |= ρ if and only if M |= Sen(θ)(ρ)
for each (S, F ∪Y, P)-model M and each (S, F ∪ X, P)-sentence ρ.
Proof. By noticing that Mod(θ)(M)t = Mθ(t) for each (F ∪ X)-term t, and by straightforward induction on the structure of the sentences.

The satisfaction condition property expressed above permits the definition of a general concept of substitution by abstracting• FOL signatures (S, F, P) to signatures Σ in arbitrary institutions, and• sets of first order variables X for (S, F, P) to signature morphisms Σ → Σ1 .
For any signature Σ of an institution, and any signature morphisms χ1 : Σ → Σ1 andχ2 : Σ → Σ2 , a Σ-substitution [6] θ : χ1 → χ2 consists of a pair (Sen(θ), Mod(θ)) , where- Sen(θ) : Sen(Σ1 ) → Sen(Σ2 ) is a function and- Mod(θ) : Mod(Σ2 ) → Mod(Σ1 ) is a functor.
such that both of them preserving Σ, i.e. the following diagrams commute:Sen(Σ1 )dSen(θ)Sen(χ1 )/ Sen(Σ2 ):Sen(χ2 )Sen(Σ)

Mod(Σ1 ) oMod(χ1 )Mod(θ)%yMod(Σ)

Mod(Σ2 )Mod(χ2 )10Mihai Codescu and Daniel Găină

and such that the following Satisfaction Condition holds:
Mod(θ)(M2 ) |= ρ1 if and only if M2 |= Sen(ρ1 )for each Σ2 -model M2 and each Σ1 -sentence ρ1 .
We sometimes let θ denote the functor Mod(θ) and let θ denote the sentencetranslation Sen(θ).
Looking at the example of substitution in FOL we observe that a homomorphism
between the term models TF (X) and TF (Y ) determines a first order substitution. Abstractly
we will want first order substitutions to be defined by morphisms between representantsMχ1 and Mχ2 of two representable signature morphisms χ1 : Σ → Σ2 and χ2 : Σ → Σ2 . One
should easily notice that given homomorphism h : Mχ1 → Mχ2 we can define the semantic
part of a substitution θh by Mod(θh ) = iχ2 ; (h/Mod(Σ)); i−1
χ . However, the syntactic partof the substitution must be defined as a characteristic of the institution.
Definition 5. For any class of morphisms D in an institution, a D-substitution is just a
substitution between signature morphisms in D .
An institution has representable D -substitutions, for a class D of representable signature morphisms, if for every χ1 : Σ → Σ1 and χ2 : Σ → Σ2 from D and every homomorphism h : Mχ1 → Mχ2 there exists a substitution θh : χ1 → χ2 , that has the semantic partdefined as Mod(θh ) = iχ2 ; (h/Mod(Σ)); i−1χ .
For sake of simplicity, we may refer to this notion just by saying that an institution
has D -substitution.
2.2. System of rules and entailment systems
Abstract systems of proof rules have been introduced in [8] which also developed thefree proof system defined in [18]. Entailment systems are just proof systems such that thecategory of proofs for a given signature is a preorder. The results in this subsection can befound in [8].
Definition 6. A system of (proof) rules (Sig, Sen, Rl) consists of- a category of ”signatures” Sig,
- a ”sentence functor” Sen : Sig → Set- a family of relations Rl = (RlΣ )Σ∈|Sig| between sets of sentences RlΣ ⊆ P (Sen(Σ))×
P (Sen(Σ)) for all signatures Σ ∈ |Sig|. such that the following property holds :An entailment system (Sig, Sen, `) is just a systems of rules such that the entailment
relation `Σ of each signatureanti-monotonicity: E1 `Σ E2 if E2 ⊆ E1 ,transitivity: E1 `Σ E3 if E1 `Σ E2 and E2 `Σ E3 ,unions: E1 `Σ E2 ∪ E3 if E1 `Σ E2 and E1 `Σ E3 , andtranslation: ϕ(E) `Σ0 ϕ(E 0 ) if E `Σ E 0 , for all ϕ : Σ −→ Σ0[
When we allow infinite unions, i.e. E ` Ei if E ` Ei for all i ∈ J, we call thei∈Jentailment system infinitary.

Birkhoff Completeness in Institutions

11

In any institution I = (Sig, Sen, Mod, |=), the semantic consequence relation |= between sets of sentences gives an example of an infinitary entailment system (Sig, Sen, |=), which is called the semantic entailment system of the institution. Infinitary entailment systems are used for infinitary logics like HCL∞ , Horn(POA)∞ , Horn(PA)∞ andHorn(OSA)∞ .
When is no danger of confusion we may omit the subscript Σ from `Σ and for every
signature morphism ϕ ∈ Sig, we sometimes let ϕ denote the sentence translation Sen(ϕ).
Fact 2. Note that every systems of rules (Sig, Sen, Rl) generates freely an entailment
system (Sig, Sen, `), where ` is the least entailment relation which contains Rl and it isclosed under anti-monotonicity, transitivity, unions and translation property.
The free infinitary entailment system is obtain by replacing unions with infinite
unions in the above definition.
A proof rule hh, ci is finitary when both sets h and c are finite. We say that an
entailment system (Sig, Sen, `) is compact whenever Γ ` E f for a finite set of sentences
E f ⊆ Sen(Σ), there exists Γ f ⊂ Γ finite such that Γ f ` E f . For each entailment system(Sig, Sen, `) one can easily construct the compact entailment sub-system (Sig, Sen, `c )by defining the entailment relation `c as follows:Γ `c E if and only if for each E f ⊆ E finite there exists Γ f ⊆ Γ finite such that Γ f ` E f
Proposition 2. (Sig, Sen, `c ) is an entailment system.
The result bellow is a corollary of Proposition 2.
Corollary 1. The entailment system freely generated by a system of finitary proof rules iscompact.
An entailment system (Sig, Sen, `) has universal D -quantification, for a sub-category
D ⊆ Sig of signature morphisms if the entailment system satisfies the following property(also called the meta-rule of ’Generalization’).
Γ `Σ (∀χ)e0 ⇔ χ(Γ) `Σ0 e0for each set of sentences Γ ⊆ Sen(Σ) and any sentence (∀χ)e0 ∈ Sen(Σ), where χ : Σ →Σ0 ∈ D .
The entailment system (Sig, Sen, `) of an institution (Sig, Sen, Mod, |=) is soundwhen E1 ` E2 implies E1 |= E2 . Likewise for the entailment system of an institution,
the system of rules (Sig, Sen, Rl) of an institution I = (Sig, Sen, Mod, |=) is sound whenfor each rule hh, ci ∈ RlΣ , we have that h |= c. Notice that all the definitions regarding
soundness may be extended to the infinitary case and actually all the results bellow holdfor both finitary and infinitary case.
The following lemma shows that the free construction of entailment systems fromsystems of rules preserve the soundness property and explains the actual practice of establishing soundness of the entailment systems which consists only of checking the soundness of the rules.
Lemma 4. The (infinitary) entailment system of an institution is sound whenever it isfreely generated by a sound system of rules.

12

Mihai Codescu and Daniel Găină

Note that the semantic entailment system of an institution which admits universal
quantifications over a sub-category D of signature morphisms satisfies the meta-rule ofGeneralization. The result below shows that by adding the meta-rule of Generalization toa system of rules the soundness property is preserved.
Lemma 5. The (infinitary) entailment system with D -universal quantifications of an institution is sound whenever it is freely generated by a sound system of rules.

3. Universal institutions
Let I = (Sig, Sen, Mod, |=) be an institution and• let Sen1 be a sub-functor of Sen (i.e. Sen1 : Sig → Set such that Sen1 (Σ) ⊆ Sen(Σ)
and ϕ(Sen1 (Σ)) ⊆ Sen1 (Σ0 ), for each signature morphism ϕ : Σ → Σ0 ), and• let D ⊆ Sig be a sub-category of signature morphisms.
We say that I is a D -universal institution over I1 , where I1 = (Sig, Sen1 , Mod, |=)when• I admits all sentences of form (∀χ)ρ, where χ : Σ → Σ0 is any signature morphismin D and ρ is any Sen1 (Σ0 ) sentence, and• any sentence of I is semantically equivalent to a sentence of form (∀χ)ρ as in theitem above.
For example, UNIV is a D -universal institution over the restriction of FOL to thequantifier-free sentences (i.e. sentences without quantifiers), where D is the class of all
signature extensions with a finite number of constants. Another example is HCL which
is a D -universal institution over the restriction of FOL to sentences of the form H ⇒ C
where H is a finite conjunction of atoms and C is an atom. Similarly, infinitary versions
UNIV∞ and HCL∞ are also examples of D -universal institutions, but in this case D isthe class of all signature extensions with constants (i.e. D might contain infinitary extensions).
Horn institutions. An institution I = (Sig, Sen, Mod, |=) is a (finitary) D -Horn institution over I0 = (Sig, Sen0 , Mod, |=) when I is a D -universal i nstitution over I1 =(Sig, Sen1 , Mod, |=) and Sen0 is a sub-functor of Sen1 such that• for each signature Σ, the institution I1 admits all sentences of the form H ⇒ C where
H is any (finite) set of Sen0 (Σ) sentences and C is any Sen0 (Σ) sentence, and• any sentence of I1 is semantically equivalent to a sentence of the form H ⇒ C as in
the item above.
For example, HCL is a finitary D -Horn institution over Atomic(FOL), where D isthe class of all signature extensions with a finite number of constants. Similarly, HCL∞ is
an infinitary D -Horn institution over Atomic(FOL), but in this case D is the class of all
signature extensions with constants (i.e. D might contain infinitary extensions).
The generic entailment system for Horn institutions developed in this section consists of three layers:
1. The ’atomic’ layer is that of the entailment system of I0 , which in the abstract setting
is assumed but which is to be developed in the concrete examples.

Birkhoff Completeness in Institutions

13

2. The layer of the entailment system for I1 which is obtained by adding the so-called’Modus-Ponens’ meta-rule in a restricted form involving the sentences of I0 .
3. The upmost layer is that of the entailment system for I, which is obtained by adding
the so-called ’Substitutivity’ rule and ’Generalization’ meta-rule to the entailment
system of I1 .
The soundness and the completeness at each layer is obtained relatively to thesoundness and completeness of the layer immediately below.
Such layered decomposition of the entailment system of I leads also to sound andcomplete entailment systems for universal institutions which are not necessarily Horninstitutions. For this it is enough to start with a sound and complete entailment system forI1 . For example, a sound and complete entailment system for quantifier-free sentences in
FOL determines automatically a sound and complete entailment system for UNIV.
3.1. The generic universal entailment system
Let us assume a D -universal institution I = (Sig, Sen, Mod, |=) over I1 with Sen1 the subfunctor of Sen. We also assume a sub-functor Sen0 of Sen1 , and denote the corresponding
institution by I0 , such that• for each (finite) set of sentences B ⊆ Sen0 (Σ) and any sentence e ∈ Sen1 (Σ) there
exists a sentence in Sen1 (Σ) which is semantically equivalent to B ⇒ e.
Remark 1. This condition is significantly more general than if we assumed that I is aHorn institution over I0 . Indeed, if I were a Horn institution over I0 for any I1 -sentencee = (H ⇒ C) and any (finite) set of I0 -sentences B we have that B ⇒ e is semanticallyequivalent to the I1 -sentence (H ∪ B) ⇒ C. However, the above condition holds also for
non-Horn settings such as when I = UNIV, the institution of the FOL universal sentences,Sen1 is a (sub-)functor of the quantifier-free sentences, and Sen0 is the (sub-)functor of
the atomic sentences.
Note also that the above condition comes in two variants: a finitary and an infinitary
one. The infinitary variant is applicable only to the infinitary variants of institutions, suchas HCL∞ or UNIV∞ .
We also assume another rather mild technical condition, namely that :pres• For each D -substitution θ : (ϕ : Σ → (Σ1 , E1 )) → (χ : Σ → (Σ2 , E2 )) in I0 , thepresinstitution of I0 -presentations, there exists a D -substitution ϕ → χ in I1 which’extends’θ. Since there is no danger of confusion we denote this latter substitution by θ too. This means that Sen0 (θ) extends to a function Sen1 (θ) : Sen1 (Σ1 ) →pres
Sen1 (Σ2 ) such that the pair (Sen1 (θ), Mod pres (θ)) constitute a substitution in I1 .
In all the examples mentioned above, this condition is fulfilled rather easily since
the I1 -sentences are Boolean expressions of I0 -sentences. For example, if I is a D -Horninstitution over I0 , then Sen0 (θ) extends canonically to Sen1 (θ) by defining Sen1 (θ)(H ⇒C) by Sen0 (H) ⇒ Sen0 (C).

14

Mihai Codescu and Daniel Găină

The rule of substitutivity. For all D -universal sentences (∀ϕ)ρ and all D -substitutions
χϕ/ → (Σ → (Σ2 , B)) in I0presθ : (Σ → (Σ1 , 0))/(Σ1 , 0)b

(Σ2 , B)
<
θ

−→

ϕ

χ

Σ
we consider the following rules of D -substitutivity(∀ϕ)ρ ` (∀χ)(B ⇒ θ(ρ))
where θ(ρ) denotes Sen1 (θ)(ρ).
Note that the rule of Substitutivity may also be considered in either a finitary and in
an infinitary variant. The above formulation corresponds to the infinitary variant since B
may be infinite. If in addition we only consider those I0 -presentations (Σ2 , B) for which B
is finite, we get the rule of finitary D -substitutivity.
Below we will see that under some technical conditions, which are often met in theapplications, the rule of Substitutivity may be rephrased to the familiar form(∀ϕ)ρ ` (∀χ)θ(ρ)
presfor D -substitutions θ in I0 rather than I0 . However, our formulation is more general andcan be applied in more actual situations.
Proposition 3. The rule of D -substitutivity is sound.
Proof. Let M be a Σ-model such that M |= (∀ϕ)ρ and let M2 be any χ-expansion of M suchthat M2 |= B. Because Mod(θ)(M2 ) is a ϕ-expansion of M (since Mod(θ)(M2 ) ϕ = M2 χ )which by hypothesis satisfies (∀ϕ)ρ, we have that Mod(θ)(M2 ) |= ρ. By the satisfaction
condition for substitutions, we obtain that M2 |= θ(ρ). Since M2 was an arbitrary expansion of M, we have thus proved that M |= (∀χ)(B ⇒ θ(ρ)).
Universal entailment systems. Given a compact entailment system (Sig, Sen1 , `1 )for I1 , the D -universal entailment system of I consists of the free entailment system• with universal D -quantification (i.e. the meta-rule of ’Generalization’)• over (Sig, Sen1 , `1 ) plus the rules of finitary D -Substitutivity.
This is the finitary version of the universal entailment system. Its infinitary variant
is obtained by considering the rules of (infinitary) D -Substitutivity, by dropping off thecompactness condition, and by considering the infinitary entailment system for I .
The soundness of D -substitutivity given by Proposition 3 has the following consequence.
Corollary 2. If the entailment system of I1 is sound then the corresponding universal
entailment system for I is sound too.
Proof. By Lemma 4 we lift the soundness from the entailment system of I1 to the entailment system which adds the rules of D -substitutivity. Then by Lemma 5 we lift soundness
further to the free entailment system with universal D -quantification.
Birkhoff Completeness in Institutions

15

3.2. Universal completenessCompleteness of the universal entailment systems is significantly more difficult than thesoundness property and therefore requires more conceptual infrastructure. The universal
completeness result below comes both in a finite and an infinite variant, the finite one
being obtained by assuming the finitary version for the entailment system of I1 and byadding (to the hypotheses of the infinite one) all the finiteness hypotheses marked inbrackets.
Theorem 1. (Universal completeness) The (finitary) universal entailment system for I
determined by the entailment system of I1 as defined above is complete if
1. the entailment system of I1 is complete,
2. every signature morphism in D is (finitely) representable,
3. every set of sentences in I0 is epic basic,pres
4. I0 has representable D -substitutions and5. for each set of sentences E ⊆ Sen1 (Σ) and each sentence e ∈ Sen1 (Σ), we have that
E |= e i f and only i f MB |= (∧E ⇒ e) f or each set o f sentences B ⊆ Sen0 (Σ)(where MB are the models defining B as basic sets of sentences).
Proof. Assume that Γ |= (∀χ)e0 for a set Γ ⊆ Sen(Σ) and e0 ∈ Sen1 (Σ0 ), where (χ : Σ →Σ0 ) ∈ D . We want to show that Γ ` (∀χ)e0 . Suppose towards a contradiction that Γ 6`(∀χ)e0 .
We define the set of Σ0 -sentencesΓ1 = {ρ0 ∈ Sen1 (Σ0 )|Γ ` (∀χ)ρ0 }χ

Suppose Γ1 ` e0 . For the infinitary case we take Γ0 = Γ1 . For the finitary case, sinceχthe entailment system of I1 is compact, there exists a finite Γ0 ⊆ Γ1 such that Γ0 ` e0 .
Because the universal entailment system of I has D -universal quantification, we have thatχχ(Γ) ` ρ0 , for all ρ0 ∈ Γ1 , thus χ(Γ) ` Γ0 . Therefore χ(Γ) ` e0 and again by the universal
D -quantification property for the entailment system of I we obtain Γ ` (∀χ)e0 , whichχ
contradicts our assumption. Thus Γ1 6` e0 .
χχ
By the completeness of I1 , Γ1 6` e0 implies Γ1 6|= e0 . By the hypothesis there existsχ
an epic basic set of sentences B ⊆ Sen0 (Σ0 ) such that MB |= Γ1 but MB 6|= e0 . This implies0MB χ 6|= (∀χ)e . If we proved that MB χ |= Γ we reached a contradiction with Γ |= (∀χ)e0 .
We will therefore focus on proving that MB χ |= Γ.
Let (∀ϕ)e1 ∈ Γ, where (ϕ : Σ → Σ1 ) ∈ D and let N be any ϕ-expansion of MB χ . We
have to show that N |= e1 . For this we use the following Lemma (which we prove later):χχLemma 6. There exists a (finite) subset of sentences B0 ⊆ B and a homomorphism h :Mϕ → MB0 χ such that the diagram below commutes:

16

Mihai Codescu and Daniel GăinăµB0 χ

MB0 a/ MB  χ = N  ϕ
9hiϕ (N)

Mϕ
where µB0 is the unique homomorphism MB0 → MB (because B0 is epic basic).
Because χ : Σ → Σ0 is representable and B0 is epic basic by Lemma 2 χ : Σ → (Σ0 , B0 )is representable as presentations morphism.
pres
Because I0 has representable D -substitutions, the homomorphism h : Mϕ → MB0 χgiven by the Lemma 6 determines a substitution θ : (ϕ : Σ → Σ1 ) → (χ : Σ → (Σ0 , B0 )) suchthat the following diagram commutes:0Mod(Σ0 , B0 )

iBχ

∼
=

/ MB0 χ /Mod(Σ)
h/Mod(Σ)

Mod(θ)

Mod(Σ1 )/ Mϕ /Mod(Σ)∼=
iϕWe have that
0

B
−1
−1
Mod(θ)(MB ) = i−1
ϕ (h; iχ (MB )) = iϕ (h; µB0 χ ) = iϕ (iϕ (N)) = N

By (finitary) D -substitutivity we obtain Γ ` (∀χ)(B0 ⇒ θ(e1 )). This implies B0 ⇒χχθ(e1 ) ∈ Γ1 . Since MB |= Γ1 , we obtain MB |= B0 ⇒ θ(e1 ). Because MB |= B0 we get MB |=θ(e1 ). By the satisfaction condition for substitutions we obtain that N |= e1 .
Proof of Lemma 6.
The infinitary case is rather simple: we take B0 = B and consequently h = iϕ (N). For
the finitary case, first note by using the fact that each subset of B is epic basic we havethat (µB f )B f ⊆B,B f finite is the directed colimit of (hB f ,B0f )B f ⊆B0 ⊆B finitefhB ,B0
f

MB f

f

/ MB0

f

µB f

!

MB

}

µB0

f

where µB f and hB f ,B0f are the unique model homomorphisms given by the fact that eachsubset of B is epic basic. Because the reduct functors corresponding to representablesignature morphisms preserve directed co-limits(cf. Lemma 3), we have that (µB f χ
)B f ⊆B, finite is also a directed co-limit. Because ϕ is finitary representable, Mϕ is finitely
presented. Hence there exists a finite set of sentences B0 ⊆ B and a model homomorphism
h : Mϕ → MB0 χ such that h; µB0 χ = iϕ (N).


Birkhoff Completeness in Institutions

17

Representable substitutions for presentations. The only condition of the completeness theorem which has a rather technical nature is the existence of representable
substitutions for presentations. However, in many situations this can be reduced to a simpler form.
Lemma 7. Let I0 be an institution with a sub-category D of representable signaturemorphisms such that every set of sentences is epic basic. Then the institution of presenpres
tations I0 has D -substitutions whenever for each signature morphism χ1 : Σ → Σ1 andχ2 : Σ → Σ2 in D and any set E of Σ2 -sentences every homomorphism h : Mχ1 → ME χ2pres/ → (χ2 : Σ → (Σ2 , E)) such that
determines a I0 -substitution θh : (χ1 : Σ → (Σ1 , 0))E−1Mod(θh ) = iχ2 ; h/Mod(Σ); iχ .
Proof. Note that because the institution has only epic basic sets of sentences, each presentation (Σ, E) has an initial model 0(Σ,E) which is precisely ME , the model defining E
as a basic set of sentences.
Let χ1 : Σ → Σ1 and χ2 : Σ → Σ2 and let h : ME1 χ1 → ME2 χ2 be a Σ-model homomorphism where Ei are sets of Σi sentences. We have to show that h determines apres
I0 -substitution θ : (χ1 : Σ → (Σ1 , E1 )) → (χ2 : Σ → (Σ2 , E2 )) such that the diagram below commutes
Let g = iχ1 (ME1 ); h. By hypothesis the Σ-homomorphism g generates a substitution/ → (Σ → (Σ2 , E2 )) such that Mod(θg ) = iEχ22 ; g/Mod(Σ); i−1
θg : (Σ → (Σ1 , 0))χ1 . We define
the substitution θh : (Σ → (Σ1 , E1 )) → (Σ → (Σ2 , E2 )) as follows- Sen(θh ) = Sen(θ)- Mod(θh ) = iEχ22 ; h/Mod(Σ); (i−1
χ1 ).
In order to show that θh is a substitution, i.e. the satisfaction condition holds, itsuffices to prove that for each (Σ2 , E2 )-model M2 , Mod(θh )(M2 ) = Mod(θg )(M2 ). We
have that Mod(θh )(M2 ) = (iEχ11 )−1 (h; (ME2 → M2 )) = i−1
χ1 (iχ1 (ME1 ); h; (ME2 → M2 )) =
i−1
(g;
(M
→
M
))
=
Mod(θ
)(M
).

E2
2
g
2
χ1
Proposition 4. In any institution I0 with a sub-category D of representable signaturemorphisms such that
1. every set of sentences is epic basic and,2. the representation Mϕ of any signature morphism ϕ ∈ D is projective with respect to
D -reducts of model homomorphisms of the form 0Σ → ME for all sets E of sentences,presthen the institution of presentations I0
has representable D -substitutions.

has representable D -substitutions whenever I0

Proof. By Lemma 7 it suffices to prove that for every signature morphisms χ1 : Σ →Σ1 and χ2 : Σ → Σ2 , each Σ-homomorphism h : Mχ1 → ME χ2 , where E is any set of/ → (Σ → (Σ2 , E)) such that
Σ2 -sentences, determines a substitution θh : (Σ → (Σ1 , 0))Mod(θh ) = iEχ2 ; h/Mod(Σ); i−1
χ1 .
Because Mχ1 is projective with respect to Mχ2 = 0Σ2 χ2 → ME χ2 , there exists a
homomorphism g such that the diagram below commutes

18

Mihai Codescu and Daniel GăinăMχ2Oiχ2 (ME )/ ME χ
2
;

g
h

Mχ1
Because I0 has representable D -substitutions there exists a D -substitution θg : χ1 →
χ2 in I0 such that Mod(θg ) = iχ2 ; g/Mod(Σ); i−1
χ1 . We define the substitution θh : (Σ →/ → (Σ → (Σ2 , E))(Σ1 , 0))- Sen(θh ) = Sen(θg ).
- Mod(θh ) = iEχ2 ; h/Mod(Σ); i−1
χ1 .
pres
In order to show that θh is a I0 -substitution, i.e. the satisfaction condition holds
it suffices to prove that Mod(θh )(M2 ) = Mod(θg )(M2 ) for each (Σ2 , E)-model M2 . We
−1have that Mod(θh )(M2 ) = i−1
χ1 (h; (ME → M2 ) χ2 ) = iχ1 (g; iχ2 (ME ); (ME → M2 ) χ2 ) =
−1
−1
i−1
χ1 (g; (OΣ2 → ME ) χ2 ; (ME → M2 ) χ2 ) = iχ1 (g; (OΣ2 → M2 ) χ2 ) = iχ1 (g; iχ2 (M2 )) =Mod(θg )(M2 ).

The first condition of the proposition is one of the conditions on I0 from Birkhoff
completeness Theorem 2. The second condition of Proposition 4 (closely related to theconcept of ’projectively representable’) is very easy to establish in institutions where themodel homomorphisms 0Σ → ME are surjective. One rather typical example is
Atomic(FOL) with D being the class of all signature extensions with constants.
Corollary 3. Atomic(FOL) pres has representable D -substitutions.
Proof. Each set E of atoms is epic basic and the model homomorphism 0Σ → ME issurjective. The reducts of surjective model homomorphisms are surjective too. For eachsignature extension with constants χ the model Mχ (which represents χ) is a free model(i.e. term model) hence it is projective with respect to any surjective homomorphism.
Atomic(FOL) has representable substitutions because each model homomorphism between free models h : TΣ (X) → TΣ (Y ) determines the Σ-substitution θ defined by θ(x) =h(x) for each x ∈ X. Thus all conditions of the Proposition 4 are fulfilled, hence
Atomic(FOL) pres has representable D -substitutions.
This type of argument can be replicated in many institutions such as the atomic subinstitutions of POA and OSA, one notable exception being the institution of existence
equations in partial algebra (PA). In this example, the model homomorphisms 0Σ → ME
are not necessarily surjective.
The substitutivity rule revisited. The conditions underlying Proposition 4 havealso another important consequence: they permit a significantly simpler formulation of
the Substitutivity rule which uses substitutions in the base institution rather than in theinstitution of the presentations. As usually, the finitary variant of the result below requires
the conditions in the brackets.

Birkhoff Completeness in Institutions

19

Proposition 5. Under the conditions of Proposition 4 and if the entailment system corresponding to the proof system of I1 has (finitary) Modus Ponens for Sen0 , meaning thatΓ ∪ B `Σ e if and only if Γ `Σ B ⇒ e
for any sets of sentences Γ ⊆ Sen1 (Σ) and (finite) B ⊆ Sen0 (Σ) and each sentence e ∈Sen1 (Σ), then we may use only Substitutivity rules of the form(∀ϕ)ρ ` (∀χ)θ(ρ)
where θ is any D -substitution in I0 .
Proof. Let us note that the Substitutivity rules of the form(∀ϕ)ρ ` (∀χ)θ(ρ)
for θ any D -substitution in I0 are just special cases of the full Substitutivity rules by/ Therefore we have only to show that for any D -substitution θ : (ϕ :considering B = 0.
/ → (χ : Σ → (Σ2 , B)) in I0pres we can have a proof
Σ → (Σ1 , 0))(∀ϕ)ρ ` (∀χ)(B ⇒ θ(ρ))
by using the Substitutivity rule in the simpler form proposed above.
The key to obtaining such proof lies in proof of Proposition 4 which shows thatχϕpres
/ → (Σ → (Σ2 , B)) determines a I0 -substitution
each I0 -substitution θ : (Σ → (Σ1 , 0))ϕχθ0 : (Σ → Σ1 ) → (Σ → Σ2 ) such Sthat Sen0 (θ) = Sen0 (θ0 ). By hypothesis we have that(∀ϕ)ρ ` (∀χ)θ(ρ). Because θ(ρ) B ` θ(ρ) and because I1 has Modus Ponens for Sen0 ,we have that θ(ρ) ` B ⇒ θ(ρ). Because (∀χ)θ(ρ) ` (∀χ)θ(ρ) and because the entailment
system of I has universal D -quantification we have that χ((∀χ)θ(ρ)) ` θ(ρ). This impliesχ((∀χ)θ(ρ)) ` B ⇒ θ(ρ) and again by the universal D -quantification property we obtain(∀χ)θ(ρ) ` (∀χ)B ⇒ θ(ρ) which leads to (∀ϕ)ρ ` (∀χ)B ⇒ θ(ρ).


4. General Birkhoff entailment systems
Birkhoff entailment systems for Horn institutions refine the universal entailment systems
defined above by assuming a entailment system for I0 and defining a entailment system
for I1 rather than assuming an entailment system for I1 . Thus
• we assume an entailment system (Sig, Sen, `0 ) for I0 and• for I1 we consider the free entailment system (Sig, Sen1 , `) over (Sig, Sen0 , `0 ) with(finitary) Modus Ponens for Sen0 , i.e.
Γ ∪ B ` e if and only if Γ ` B ⇒ e
for any Γ ⊆ Sen1 (Σ), any (finite) B ⊆ Sen0 (Σ) and each e ∈ Sen1 (Σ).
The Birkhoff entailment system is finitary if and only if it is generated by using
the finitary version of Modus Ponens for Sen0 , and (Sig, Sen, `0 ) is generated by finitaryrules, otherwise it is infinitary.
Fact 3. The entailment system of I1 is sound if the entailment system of I0 is sound.

20

Mihai Codescu and Daniel Găină

In order to instantiate the general universal completeness Theorem 1 to the Birkhoff
entailment system we need to address the first and the last conditions of the theorem.
The following result addresses the first condition plus the compactness condition
from the definition of the finitary D -universal entailment systems. As usual, the result
comes in a finitary version (with the information contained within brackets included) andin an infinitary version.
Proposition 6. Let us assume that
1. each set of I0 -sentences is basic, and2. the entailment system of I0 is complete (and compact).
Then the entailment system of I1 is complete (and compact).
Proof. Because the entailment system of I1 has (finitary) Modus Ponens for Sen0 it isenough to prove thatΓ |= ρ implies Γ ` ρfor each Γ ⊆ Sen1 (Σ) and each ρ ∈ Sen0 (Σ). Let MΓ0 be the model defining the set ofsentences Γ0 = {e ∈ Sen0 (Γ)|Γ ` e} as basic. We use the following couple of lemmas.
Lemma 8. MΓ0 |= e if and only if Γ ` e for each sentence e ∈ Sen0 (Σ).
Lemma 9. MΓ0 |= Γ.
If Γ |= ρ then by Lemma 9 we have that MΓ0 |= ρ. Now by Lemma 8 we obtainΓ ` ρ.
For the compactness of the entailment system of I1 first let us recall that the sentences of I1 are of the form H ⇒ C where C is an I0 sentence and H is a finite set of
I0 sentences. We consider the sub-system of the compact entailments of I1 ; this is anentailment (sub-)system by Proposition 2. It contains the entailment system of I0 since
the latter is compact by the hypotheses. It also has the finitary Modus Ponens for Sen0
because for any finite B ⊆ Sen0 (Σ) the entailment Γ ∪ B ` e is compact if and only if theentailment Γ ` B ⇒ e is compact. Indeed, Γ ∪ B ` e compact means that there exists finiteΓ0 ⊆ Γ such that Γ0 ∪ B ` e which by the Modus Ponens for Sen0 property is equivalent toΓ0 ` B ⇒ e which means Γ ` B ⇒ e is compact. Now because the entailment system of I1
is the least one containing the entailment system of I0 and satisfying the finitary Modus
Ponens for Sen0 property we may conclude that this is exactly the compact sub-system of
the entailment system of I1 , which just means that the entailment system of I1 is compact.
Proof of Lemma 8. The implication from right to left holds by the definition of Γ0 .
For the other implication let us consider a sentence e such that MΓ0 |= e. For any model
M such that M |= Γ0 , because Γ0 is basic there exists a model homomorphism MΓ0 → M.
Since MΓ0 |= e and e is basic, there exists another model homomorphism Me → MΓ0 .
These give a model homomorphism Me → M which means M |= e. We have thus shownthat Γ0 |= e.
By the completeness of I0 we obtain that Γ0 ` e. For the infinitary case let us take
Γ00 = Γ0 . For the finitary case, since the entailment system of I0 is compact, there exists
Γ00 ⊆ Γ0 finite such that Γ00 ` e. By the definition of Γ0 we obtain that Γ ` Γ00 hence Γ ` e.

Birkhoff Completeness in Institutions

21

Proof of Lemma 9. Let us consider that we have an I1 -sentence H ⇒ C ∈ Γ and let
us assume that MΓ0 |= H. By Lemma 8 we have that Γ |= H and because H ⇒ C ∈ Γ andthe entailment system for I1 has (finitary) Modus Ponens for Sen0 we obtain that Γ ` C.
By Lemma 8 again we deduce MΓ0 |= C.
The following shows that the last condition of Theorem 1 is fulfilled.
Proposition 7. Under the conditions of the Proposition 6, for each set of sentences E ⊆Sen1 (Σ) and each sentence e ∈ Sen1 (Σ) we have that
E |= e if and only if MB |= (E ⇒ e) for each set of sentences B ⊆ Sen0 (Σ)(where MB are the models defining B as basic sets of sentences).
Proof. Let e = H ⇒ C with H ⊆ Sen0 (Σ) and C ∈ Sen0 (Σ). Consider the model M(E∪H)0
defining (E ∪ H)0 = {ρ ∈ Sen0 (Σ)|E ∪ H |= ρ}. By Lemma 9 we have that M(E∪H)0 |=E ∪ H. By the hypothesis this implies M(E∪H)0 |= H ⇒ C. Because M(E∪H)0 |= H too, it
follows that M(E∪H)0 |= C. Since C is basic there exists a homomorphism MC → M(E∪H)0 .
Now let M be any model such that M |= E ∪ H. By Lemma 8 we obtain that M |=(E ∪ H)0 . Because (E ∪ H)0 is basic, there exists a homomorphism M(E∪H)0 → M. We
obtain thus a homomorphism MC → M, which means M |= C.
The Propositions 6 and 7 lead to the following completeness result for Horn institutions obtained as an instance of the general universal completeness theorem.
Theorem 2. The (finitary) Birkhoff entailment system for a (finitary) D -Horn institution
is complete if
1. the entailment system of I0 is complete (and compact),
2. every signature morphism in D is (finitely) representable,
3. every set of sentences in I0 is epic basic andpres
4. I0 has representable D -substitutions.

5. Instances of Birkhoff completenessIn order to develop concrete sound and complete Birkhoff entailment systems we need to
set the parameters of the completeness theorem for each example.
5.1. The Birkhoff entailment system of HCL
We set the parameters of the completeness theorem for HCL as follows:• the institution I is HCL• the institution I0 is Atomic(FOL)• D is the class of all signature extensions with a finite number of constants• the system of proof rules for Atomic(FOL) is given by the following set of rules
for any FOL signature (S, F, P):– (R)0/ ` t = t for each term t– (S)t = t 0 ` t 0 = t for any terms t,t 0– (T ){t = t 0 ,t 0 = t 00 } ` t = t 00 for any terms t,t 0 ,t 00

22Mihai Codescu and Daniel Găină– (F){ti = ti0 |1 ≤ i ≤ n} ` σ(t1 , ...,tn ) = σ(t10 , ...,tn0 ) for any σ ∈ F– (P){ti = ti0 |1 ≤ i ≤ n} ∪ {π(t1 , ...,tn )} ` π(t10 , ...,tn0 ) for any π ∈ P

Proposition 8. Atomic(FOL) with the above system of proof rules is sound and complete.
Proof. Soundness follows by simple routine check. For proving the completeness, for any
set E of atoms for a signature (S, F, P) we define≡E = {(t,t 0 )|E ` t = t 0 }By (R), (S), (T ) and (F) this is a congruence on TF . Then we define a model ME as
follows:• the (S, F)-algebra part of ME is defined as the quotient of the initial algebra (termalgebra) TF by ≡E , and• for each relation symbol π ∈ P, we define (ME )π = {x/≡E |E ` π(x)}The definition of (ME )π is correct because of the rule (P). Now we note that foreach (S, F, P)-atom ρ we have E ` ρ if and only if ME |= ρ. Now if E |= ρ then ME |= ρwhich means E ` ρ.
We are now able to formulate the following corollary of the general Birkhoff completeness theorem.
Corollary 4. The finitary entailment system for HCL is sound and complete. Moreover,this entailment system is obtained as the free entailment system• with universal quantification and• with implication at the quantifier-free level i.e. for each quantifier-free Horn sentence H ⇒ C and all sets Γ of quantifier-free Horn sentencesΓ ∪ H ` C if and only if Γ ` H ⇒ C
generated by the following system of finitary rules for a signature (S, F, P)• (R)0/ ` t = t for each term t• (S)t = t 0 ` t 0 = t for any terms t,t 0• (T ){t = t 0 ,t 0 = t 00 } ` t = t 00 for any terms t,t 0 ,t 00• (F){ti = ti0 |1 ≤ i ≤ n} ` σ(t1 , ...,tn ) = σ(t10 , ...,tn0 ) for any σ ∈ F• (P){ti = ti0 |1 ≤ i ≤ n} ∪ {π(t1 , ...,tn )} ` π(t10 , ...,tn0 ) for any π ∈ P• (Subst)(∀Y )ρ ` (∀X)θ(ρ) for any (S, F, P)-sentence (∀Y )ρ and for any substitution
θ : Y → TF (X).
The following is the infinitary version of the above corollary.
Corollary 5. The infinitary Birkhoff entailment system HCL∞ is sound and complete forthe same rules as in the corollary above.
Remark 2. We can also consider the case when the set of relation is empty, obtaining
thus a completeness result for equational logic, CEQL.

Birkhoff Completeness in Institutions

23

5.2. The Birkhoff entailment system of Horn(POA)
We set the parameters of the completeness theorem for Horn(POA).
• the institution I is Horn(POA)• the institution I0 is Atomic(POA)• D is the class of all signature extensions with a finite number of constants• the system of proof rules for Atomic(POA) is given by the following set of rules
for any POA signature (S, F):– (R)0/ ` t = t for each term t– (S)t = t 0 ` t 0 = t for any terms t,t 0– (T ){t = t 0 ,t 0 = t 00 } ` t = t 00 for any terms t,t 0 ,t 00– (F){ti = ti0 |1 ≤ i ≤ n} ` σ(t1 , ...,tn ) = σ(t10 , ...,tn0 ) for any σ ∈ F– (R0 )0/ ` t ≤ t for each term t– (T 0 ){t ≤ t 0 ,t 0 ≤ t 00 } ` t ≤ t 00 for any terms t,t 0 ,t 00– (F 0 ){ti ≤ ti0 |1 ≤ i ≤ n} ` σ(t1 , ...,tn ) ≤ σ(t10 , ...,tn0 ) for any σ ∈ F– (ET ){t1 = t2 , t2 ≤ t3 , t3 = t4 } ` t1 ≤ t4 for any terms t1 ,t2 ,t3 ,t4
For the readers not familiar with preorder algebras we give the following definition:
Definition 7. A (preorder) congruence relation on a (S, F)-preorder algebra M is a pair(≡, v) where ≡ is a (S, F)-congruence relation and v is a preorder on M which- preserve the preorder structure of M, i.e. m ≤ m0 implies m v m0 for all elements
0m, m ∈ M,- is compatible with operations in F, i.e. m ≤ m0 implies Mσ (m) ≤ Mσ (m0 ) for all
operations σ ∈ Fw,s and all elements m, m0 ∈ Mw , and- is compatible with the congruence ≡, i.e. m1 ≡ m2 , m2 v m3 and m3 ≡ m4 implies
m1 v m4 for all elements m1 , m2 , m3 , m4 ∈ M.
Proposition 9. Atomic(POA) with the above system of proof rules is sound and complete.
Proof. Soundness follows by simple routine check. For proving the completeness, for any
set E of atoms for a signature (S, P) we define (≡E , vE )- ≡E = {(t,t 0 ) | E ` t = t 0 }- vE = {(t,t 0 ) | E ` t ≤ t 0 }By the above rules (≡E , vE ) is a preorder congruence on the term algebra TF . Then
we define the preorder algebra ME as the quotient of the term algebra by (≡E , vE ). We
note that for each equational or transitional (S, F)-atom ρE ` ρ if and only if ME |= ρNow if E |= ρ then ME |= ρ which means E ` ρ.

Corollary 6. The finitary entailment system for Horn(POA) is sound and complete.
Moreover, this entailment system is obtained as the free entailment system• with universal quantification and• with implication at the quantifier-free level i.e. for each quantifier-free Horn sentence H ⇒ C and all sets Γ of quantifier-free Horn sentences Γ ∪ H ` C if and only
if Γ ` H ⇒ C.

24

Mihai Codescu and Daniel Găină
generated by the following system of finitary rules for a signature (S, F)• (R)0/ ` t = t for each term t• (S)t = t 0 ` t 0 = t for any terms t,t 0• (T ){t = t 0 ,t 0 = t 00 } ` t = t 00 for any terms t,t 0 ,t 00• (F){ti = ti0 |1 ≤ i ≤ n} ` σ(t1 , ...,tn ) = σ(t10 , ...,tn0 ) for any σ ∈ F• (R0 )0/ ` t ≤ t for each term t• (T 0 ){t ≤ t 0 ,t 0 ≤ t 00 } ` t ≤ t 00 for any terms t,t 0 ,t 00• (F 0 ){ti ≤ ti0 |1 ≤ i ≤ n} ` σ(t1 , ...,tn ) ≤ σ(t10 , ...,tn0 ) for any σ ∈ F• (ET ){t1 = t2 , t2 ≤ t3 , t3 = t4 } ` t1 ≤ t4 for any terms t1 ,t2 ,t3 ,t4• (Subst)(∀Y )ρ ` (∀X)θ(ρ) for any (S, F, P)-sentence (∀Y )ρ and for any substitution
θ : Y → TF (X).

Corollary 7. The infinitary Birkhoff entailment system Horn(POA)∞ is sound and complete for the same rules as in the corollary above.
5.3. The Birkhoff entailment system of Horn(OSA)
We set the parameters of the completeness theorem for Horn(OSA) as follows:• the institution I is Horn(OSA),• the institution I0 is Atomic(OSA),• D is the class of all signature extensions with a finite number of constants, and• the system of proof rules for Atomic(OSA) is given by the following set of rules
for any OSA signature (S, ≤, F):– (R)0/ ` t = t for each term t– (S)t = t 0 ` t 0 = t for any terms t,t 0– (T ){t = t 0 ,t 0 = t 00 } ` t = t 00 for any terms t,t 0 ,t 00– (F){ti = ti0 |1 ≤ i ≤ n} ` σ(t1 , ...,tn ) = σ(t10 , ...,tn0 ) for any σ ∈ F
We give the definition of congruence relation on an order sorted model.
Definition 8. A congruence relation ≡ on a (S, ≤, F)-model M is a (S, F)-congruence
relation ≡= (≡s )s∈S such that if s ≤ s0 in (S, ≤) and a, a0 ∈ Ms then a ≡s a0 if and only ifa ≡s0 a0 .
Proposition 10. Atomic(OSA) with the above system of proof rules is sound and complete.
Proof. Soundness follows by simple routine check. For proving the completeness, for any
set E of equations for a signature (S, ≤, F) we define≡E = {(t,t 0 )|E ` t = t 0 }Since the signature (S, ≤, F) is regular the term algebra TF is the initial (S, ≤, F)algebra in Mod(S, ≤, F). By (R), (S), (T ) and (F) this is an F-congruence on TF . ≡E isalso an order sorted congruence on TF , because the definition of ≡E does not depend upona sort. Since the signature (S, ≤, F) is locally filtered we may define a model ME as thequotient of the initial algebra (term algebra) TF by order sorted congruence ≡E .
Notice that for each (S, ≤, F)-equation t = t 0 , E ` t = t 0 if and only if ME |= t = t 0 .
Now if E |= t = t 0 then ME |= t = t 0 which means E ` t = t 0 .
Birkhoff Completeness in Institutions

25

We are now able to formulate the following corollary of the general Birkhoff completeness theorem.
Corollary 8. The finitary entailment system for Horn(OSA) is sound and complete.
Moreover, this entailment system is obtained as the free entailment system• with universal quantification and• with implication at the quantifier-free level i.e. for each quantifier-free Horn sentence H ⇒ C and all sets Γ of quantifier-free Horn sentences Γ ∪ H ` C if and only
if Γ ` H ⇒ C.
generated by the following system of finitary rules for a signature (S, ≤, F)• (R)0/ ` t = t for each term t• (S)t = t 0 ` t 0 = t for any terms t,t 0• (T ){t = t 0 ,t 0 = t 00 } ` t = t 00 for any terms t,t 0 ,t 00• (F){ti = ti0 |1 ≤ i ≤ n} ` σ(t1 , ...,tn ) = σ(t10 , ...,tn0 ) for any σ ∈ F• (Subst)(∀Y )ρ ` (∀X)θ(ρ) for any (S, F, P)-sentence (∀Y )ρ and for any substitution
θ : Y → TF (X).
Corollary 9. The infinitary Birkhoff entailment system Horn(OSA)∞ is sound and complete for the same rules as in the corollary above.
5.4. The Birkhoff entailment system of Horn(PA)We set the parameters of the completeness theorem for Horn(PA) as follows:• the institution I is Horn(PA),• the institution I0 is Atomic(PA) (the restriction of PA to the existence equations),• D is the class of all signature extensions with a finite number of total constants, and• the system of proof rules for Atomic(PA) is given by the following set of rules for
any PA signature (S, T F, PF):ee
– (S) t = t 0 ` t 0 = t for any terms t,t 0
e 0 0 e 00
e
– (T ) {t = t , t = t } ` t = t 00 for any terms t,t 0 ,t 00
e 0e– (C) {ti = ti , def(σ(t1 , . . . ,tn )), def(σ(t10 , . . . ,tn0 ))} ` σ(t1 , . . . ,tn ) = σ(t10 , . . . ,tn0 )for any σ ∈ T F ∪ PF
– (Totality) {def(ti ) | i = 1, n} ` def(σt (t1 , . . . ,tn )) for any σt ∈ T F– (Subterm) def(σ(t1 , . . . ,tn )) ` {def(ti ) | i ∈ 1, n} for any σ ∈ T F ∪ PF
We give the definition of partial congruence relation.
Definition 9. A congruence relation ≡ on a (S, T F, PF)-model M is a S-sorted equivalence relation ≡= (≡s )s∈S such that for every operation symbol σ ∈ T F ∪ PF and elements m, m0 ∈ M with m ≡ m0 if both Mσ (m) and Mσ (m0 ) are defined then Mσ (m) ≡Mσ (m0 ).
For each set E of existence (S, T F, PF)-equations we denote by SE the set of all subterms of the terms which occur in E and by def(E) the set of sentences {def(t) | t ∈ SE }.
We define a model Mdef(E) as follows- (Mdef(E) )s = (TT F (SE ))s for each sort s ∈ S, where TT F (SE ) is the free (S, T F)algebra of terms with elements from SE ,

26

Mihai Codescu and Daniel Găină- (Mdef(E) )σt (t1 , . . . ,tn ) = σt (t1 , . . . ,tn ) for each total operation symbol σt ∈ T F andany terms t1 , . . . ,tn ∈ TT F (SE ), and- (Mdef(E) )σ (t1 , . . . ,tn ) = σ(t1 , . . . ,tn ) if σ(t1 , . . . ,tn ) ∈ SE for each partial operation
symbol σ ∈ PF.
Proposition 11. Atomic(PA) with the above system of proof rules is sound and complete.
Proof. Soundness follows by simple routine check. For proving the completeness, for any
set E of atoms for a signature (S, T F, PF) we definee≡E = {(t,t 0 )|E ` t = t 0 }We use the following Lemma (which we prove later).
Lemma 10. For every set of existence equations E ⊆ Sen(S, T F, PF) we have that E `def(t) if and only if t ∈ Mdef(E) .
Firstly we prove that ≡E is a congruence relation on Mdef(E) . The reflexivity of ≡E
is given by the above Lemma. The first two rules ensure the symmetry and the transitivityof ≡E . By the rule (C) we have that ≡E is a congruence relation on Mdef(E) .
ee

For each existence equation t = t 0 we have E ` t = t 0 ⇔ t ≡E t 0 ⇔ Mdef(E) /≡E |=
e

e

e

e

t = t 0 . If E |= t = t 0 then Mdef(E) /≡E |= t = t 0 which implies E ` t = t 0 .
Proof of Lemma 10.
”the only if part” one can easily prove by induction in the definition of ` that E `e
t = t 0 implies t,t 0 ∈ Mdef(E) .
”the if part” We prove this by induction on the structure of the term t. Let σ(t1 , . . . ,tn )be a term such that ti ∈ Mdef(E) , for all i ∈ {1, . . . , n}. By the hypothesis induction we haveE ` def(ti ), for all i ∈ {1, . . . , n}.
- if σ ∈ T F then by Totality rule we obtain E ` def(σ(t1 , . . . ,tn ))- if σ ∈ PF then by the definition of Mdef(E) we have σ(t1 , . . . ,tn ) ∈ SE . By theee . Without
definition of SE there exists an existence equation t1 = t2 ∈ E such that t ∈ St =t

e

1

2

e

loss of generality we assume that t ∈ Sdef(t1 ) . We have E ` t1 = t2 and E ` t2 = t1 which
implies E ` def(t1 ). By Subterm rule, def(t1 ) ` def(t). So E ` def(t).
The case of Horn(PA) requires more technical constructions. We address the conditions of Theorem 2.
First order substitutions in PA. Given a PA signature (S, T F, PF) and two sets of
new total constants X and Y , a first order (S, T F, PF)-substitution from X to Y consistsof a mapping θ : X → TT F∪PF (Y ) of the variables X with (T F ∪ PF)-terms over Y . Letdef(θ) to denote the set {def(θ(x)) | x ∈ X} of (S, T F ∪Y, PF)-sentences.
On the semantics side, each (S, T F, PF)-substitution θ : X → TT F∪PF (Y ) determines
a functor Mod(θ) : Mod((S, T F ∪Y, PF), def(θ)) → Mod(S, F ∪ X, P) defined by- Mod(θ)(M)x = Mx for each sort x ∈ S, or operation symbol x ∈ T F ∪ PF, andBirkhoff Completeness in Institutions

27- Mod(θ)(M)x = Mθ(x) , i.e. the evaluation of the term θ(x) in M, for each x ∈ X.
Notice that since M |= def(θ) the term θ(x) which may contain partial operation symbols
is evaluated in the model M.
On the syntax side, θ determines a sentence translation function Sen(θ) : Sen(S, T F ∪X, PF) → Sen(S, T F ∪Y, PF) which in essence replaces all symbols from X with the corresponding (T F ∪Y ∪ PF)-terms according to θ.
ee- Sen(θ)(t1 = t2 ) is defined as θ(t) = θ(t 0 ) for each (S, T F ∪ X, PF)-existence equation t1 = t2 , where θ : TT F∪PF (X) → TT F∪PF (Y ) is the unique extension of θ to an (T F ∪PF)-homomorphism (θ is replacing variables x ∈ X with θ(x) in each (T F ∪X ∪PF)-termt).
- Sen(θ)(ρ1 ∧ρ2 ) is defined as Sen(θ)(ρ1 )∧Sen(θ)(ρ2 ) for each conjunction ρ1 ∧ρ2of (S, T F ∪ X, PF)-sentences, and similarly for the case of any other logical connectives.
- Sen(θ)((∀Z)ρ) is defined as (∀Z)Sen(θZ )(ρ) for each (S, T F ∪X ∪Z, PF)-sentence
ρ, where θZ is the trivial extension of θ to an (S, T F ∪ Z, PF)-substitution.
The satisfaction condition is given by the proposition bellow.
Proposition 12. For each PA-signature and each (S, T F, PF)-substitution
θ : X → TT F∪PF (Y )eeMod(θ)(M) |= t1 = t2 if and only if M |= Sen(θ)(t1 = t2 )for each (S, T F ∪ Y, PF)-model M which satisfies def(θ) and each existence (S, T F ∪e
X, PF)-equation t1 = t2 .
Proof. By noticing that Mod(θ)(M)t = Mθ(t) for each (T F ∪ X ∪ PF)-term t.



We denote by χ and ϕ the inclusion signature morphisms (S, T F, PF) ,→ (S, T F ∪X, PF) and (S, T F, PF) ,→ (S, T F ∪Y, PF). Notice that there exists an unique homomorphism g : TT F (X) → (Mdef(θ) ) ϕ such that g(x) = θ(x) for all x ∈ X.
TT F (X)
O
?
X

g

/ (M
def(θ) ) ϕ
8θ

def(θ)
Proposition 13. Mod(θ) = iϕ
; g/Mod(S, T F, PF); i−1χ .
Proof. For any (S, T F ∪Y, PF)-model M which satisfies def(θ) we havedef(θ)- (iϕ; g/Mod(S, T F, PF); i−1χ )(M)x = Mx = Mod(θ)(M)x for each sort x ∈ S, or
operation symbol x ∈ T F ∪ PF
def(θ)−1; g/Mod(S, T F, PF); i−1- (iϕχ )(M)x = iχ (g; (Mdef(θ) → M) ϕ )x= (g; (Mdef(θ) → M) ϕ )(x) = (Mdef(θ) → M) ϕ (g(x)) = (Mdef(θ) → M)(g(x)) =(Mdef(θ) → M)(θ(x)) = Mθ(x) = Mod(θ)(M)x for each x ∈ X.

Proposition 14. Atomic(PA) pres has representable D -substitutions.

28

Mihai Codescu and Daniel Găină

Proof. Let χ : (S, T F, PF) ,→ (S, T F ∪ X, PF) and ϕ : (S, T F, PF) ,→ (S, T F ∪Y, PF) be
two extensions with total constants of the signature (S, T F, PF) and let h : TT F (X) →ME ϕ be a (S, T F, PF)-homomorphism where E is a set of existence (S, T F ∪ Y, PF)equations. By Lemma 7 it suffices to show that there exists a substitution
θ : X → TT F∪PF (Y ) such that/(iEϕ ; h/Mod(S, T F, PF); i−1χ ) : Mod((S, T F ∪Y, PF), E) → Mod((S, T F ∪ X, PF), 0)
is a sub-functor of/Mod(θ) : Mod((S, T F ∪Y, PF), def(θ)) → Mod((S, T F ∪ X, PF), 0)
The reducts of surjective model homomorphisms are surjective too and since thealgebra of terms TT F (X) is projective with respect to all surjections there exists a model
homomorphism h0 : TT F (X) → Mdef(E) ϕ such the following diagram commutes.
(Mdef(E)O
h0b/ ME ) ϕ:h

TT F (X)
We define the substitution θ : X → TT F∪PF (Y ) as the restriction of h0 to the setof variables X, i.e. θ(x) = h0 (x), for each x ∈ X. There exists an unique (S, T F, PF)homomorphism g : TT F (X) → (Mdef(θ) ) ϕ such that g(x) = θ(x), for each x ∈ X. Because
g(x) = θ(x) = h0 (x), for each x ∈ X, we have that
- θ(X) ⊆ SE which implies Mdef(θ) ⊆ Mdef(E) , and- the following diagram commutes(Mdef(θ)
Ob/ ME ) ϕ:gh

TT F (X)−1
For each (S, T F ∪ Y, PF)-model (iEϕ ; h/Mod(S, T F, PF); i−1χ )(M) = iχ (h; (ME →def(θ)M) ϕ ) = i−1; g/Mod(S, T F, PF); i−1χ (g; (Mdef(θ) → M) ϕ ) = (iϕχ )(M) = Mod(θ)(M).
The Substitutivity rules for Horn(PA).
Proposition 15. In Horn(PA) we may use substitutivity rules of the form(∀Y )ρ ` (∀X)def(θ) ⇒ θ(ρ)
Proof. Notice that the Substitutivity rules of the form(∀Y )ρ ` (∀X)def(θ) ⇒ θ(ρ)

Birkhoff Completeness in Institutions

29

where θ : Y → TT F∪PF (X) is a any (S, T F, PF)-substitution are just special cases of Substitutivity rules by considering B = def(θ). Therefore we have only to show that for any
substitution θ : Y → TT F∪PF (X) we can have a proof(∀Y )ρ ` (∀X)B ⇒ θ(ρ)
by using the Substitutivity rule in the simpler form proposed above. Since Mod(θ) :Mod((S, T F ∪ X, PF), def(θ)) → Mod(S, T F ∪ Y, PF), B |= def(θ) which implies (byProposition 11) B ` def(θ). Because the institution I1 has implications we have def(θ) ∪(def(θ) ⇒ θ(ρ)) ` θ(ρ). We obtain B ∪ (def(θ) ⇒ θ(ρ)) ` θ(ρ) and using again the factthat I1 has implications def(θ) ⇒ θ(ρ) ` B ⇒ θ(ρ).
Because (∀χ)def(θ) ⇒ θ(ρ) ` (∀χ)def(θ) ⇒ θ(ρ) and because the entailment system of I has universal D -quantification we have that χ((∀χ)def(θ) ⇒ θ(ρ)) ` def(θ) ⇒θ(ρ). This implies χ((∀χ)def(θ) ⇒ θ(ρ)) ` B ⇒ θ(ρ) and again by the universal D quantification property we obtain (∀χ)def(θ) ⇒ θ(ρ) ` (∀χ)B ⇒ θ(ρ) which leads to(∀ϕ)ρ ` (∀χ)B ⇒ θ(ρ).
We are now able to formulate the following corollary of the general Birkhoff completeness theorem.
Corollary 10. The finitary entailment system for Horn(PA) is sound and complete. Moreover, this entailment system is obtained as the free entailment system• with universal quantification and• with implication at the quantifier-free level i.e. for each quantifier-free Horn sentence H ⇒ C and all sets Γ of quantifier-free Horn sentences Γ ∪ H ` C if and only
if Γ ` H ⇒ C.
generated by the following system of finitary rules for a signature (S, T F, PF)ee• (S) t = t 0 ` t 0 = t for any terms t,t 0eee• (T ) {t = t 0 , t 0 = t 00 } ` t = t 00 for any terms t,t 0 ,t 00
ee• (C) {ti = ti0 , def(σ(t1 , . . . ,tn )), def(σ(t10 , . . . ,tn0 ))} ` σ(t1 , . . . ,tn ) = σ(t10 , . . . ,tn0 ) for
any σ ∈ T F ∪ PF
• (Totality) {def(ti ) | i = 1, n} ` def(σt (t1 , . . . ,tn )) for any σt ∈ T F• (Subterm) def(σ(t1 , . . . ,tn )) ` {def(ti ) | i ∈ 1, n} for any σ ∈ T F ∪ PF
• (Subst) (∀Y )ρ ` (∀X)def(θ) ⇒ θ(ρ) for any (S, T F, PF)-sentence (∀Y )ρ and forany substitution θ : Y → TT F∪PF (X).
The following is the infinitary version of the above corollary.
Corollary 11. The infinitary Birkhoff entailment system Horn(PA)∞ is sound and complete for the same rules as in the corollary above.

6. Conclusions and future work
The present result is the first generalization of Birkhoff Completeness to the institutionalcase. We developed a common framework that allows one to formulate and prove complete deduction for variants and generalizations of equational logic. The paper captures

30

Mihai Codescu and Daniel Găină

uniformly both finitary and infinitary case and it shows the connection between the structure of the sentences and the proof of completeness. The approach distinguishes clearly
the specific aspects of an institution from the general ones yielding to the decompositionof the completeness on three layers. Such an approach leads to unexpected results.
• Theorem 1 is applicable also to universal institutions which are not necessarily Horninstitutions, such as UNIV.
• the conditions of Proposition 6 do not require that the sentences of I0 to be epic
basic. In this case we may start with an institution I0 which has sentences of theform (∃X)e where e is a an atom or a conjunction of atoms.
The practical aspect of the present paper is that it provides complete calculus for the
logics underlying the modern algebraic specification languages.
An interesting direction of future work is to extend the result to modal logics. Another direction of further research is to provide sound and complete systems of proof rules
for first order institutions like FOL, POA and PA. An institutional version of Godel’s
completeness theorem by redoing Henkin’s proof may be found in [19] but this is applicable only to the finitary case. We suggest a different approach by forcing techniques
which covers also the infinitary case in classical first order logic.
Concerning related work, another abstract calculus for equational logics is developed in [22], in a categorial framework, based on satisfaction as injectivity.
Acknowledgement.
We are very grateful to Răzvan Diaconescu for introducing us to the topics of algebraic specifications and abstract model theory, at the courses held at the Şcoala NormalăSuperioară, Romania. This paper is a direct result of our work there. Moreover, prof. Diaconescu helped us improve presentation with many suggestions and comments. We would
also like to thank our colleagues, Andrei Popescu, Marius Petria, Denisa Diaconescu andAndrei Plăiaşu, for being opened for discussions and for encouragement.
Mihai Codescu has been supported by a PhD scholarship of DFKI Laboratory, Bremen. Daniel Găină has been supported by a PhD scholarship of Japan Advanced Instituteof Science and Technology.

References[1] J. Adámek and J. Rosický. Locally Presentable and Accessible Categories. Number
189 in London Mathematical Society Lecture Notes. Cambridge University Press,
1994.
[2] E. Astesiano, M. Bidoit, H. Kirchner, B. Krieg-Brückner, P. D. Mosses, D. Sannella,and A. Tarlecki. CASL: the common algebraic specification language. Theor. Comput. Sci., 286(2):153–196, 2002.
[3] G. Birkhoff. On the structure of abstract algebras. (31):433–454, 1935.
[4] P. Burmeister. A Model Theoretic Oriented Appraoch to Partial Algebras.
Akademie-Verlag Berlin, 1986.
[5] R. Diaconescu. Institution-independent ultraproducts. Fundamenta Informaticae,
55(3-4):321–348, 2003.

REFERENCES

31[6] R. Diaconescu. Herbrand theorems in arbitrary institutions. Inf. Process. Lett.,
90:29–37, 2004.
[7] R. Diaconescu. An institution-independent proof of Craig interpolation theorem.
Studia Logica, 77(1):59–79, 2004.
[8] R. Diaconescu. Proof systems for institutional logic. Journal of Logic and Computation, 16(3):339–357, 2006.
[9] R. Diaconescu. Institution-independent Model Theory. 2008. To appear in Studies
in Universal Logic, Birkhäuser.
[10] R. Diaconescu and K. Futatsugi. Logical foundations of CafeOBJ. Theor. Comput.
Sci., 285(2):289–318, 2002.
[11] R. Diaconescu and M. Petria. Saturated models in institutions. In preparation.
[12] D. Găină and A. Popescu. An institution-independent proof of Robinson consistency
theorem. Studia Logica, 85(1):41–73, 2007.
[13] J. Goguen and R. Burstall. Institutions: Abstract model theory for specification andprogramming. Journal of the Association for Computing Machinery, 39(1):95–146,
January 1992.
[14] J. Goguen and J. Meseguer. Completeness of many-sorted equational logic. Houston
Journal of Mathematics, 11(3):307–334, 1985.
[15] J. A. Goguen and R. Diaconescu. An Oxford survey of order sorted algebra. Mathematical Structures in Computer Science, 4(3):363–392, 1994.
[16] J. A. Goguen and J. Meseguer. Order-sorted algebra I: Equational deduction for
multiple inheritance, overloading, exceptions and partial operations. TheoreticalComputer Science, 105(2):217–273, 1992.
[17] S. Mac Lane. Categories for the Working Mathematician. Springer, 1971.
[18] 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.
[19] M. Petria. An institutional version of Gödel’s completeness theorem. In
T. Mossakowski, U. Montanari, and M. Haveraaen, editors, CALCO, volume 4624
of Lecture Notes in Computer Science, pages 409–424. Springer, 2007.
[20] M. Petria and R. Diaconescu. Abstract Beth definability in institutions. J. Symbolic
Logic, 71(3):1002–1028, 2006.
[21] H. Reichel. Structural Induction on Partial Algebras. Akademie-Verlag Berlin,
1984.
[22] G. Roşu. Complete categorical deduction for satisfaction as injectivity. In K. Futatsugi, J.-P. Jouannaud, and J. Meseguer, editors, Essays Dedicated to Joseph
A. Goguen, volume 4060 of Lecture Notes in Computer Science, pages 157–172.
Springer, 2006.
[23] 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.
[24] A. Tarlecki. Quasi-varieties in abstract algebraic institutions. J. Comput. Syst. Sci.,
33(3):333–360, 1986.

32

REFERENCES

Mihai Codescu
Şcoala Normală Superioară Bucureşti and DFKI Laboratory, Bremene-mail: mcodescu@dfki.de
Daniel Găină
Şcoala Normală Superioară Bucureşti and Japan Advanced Institute of Science and Technology
e-mail: daniel@jaist.ac.jp