Constructor-based Logics
Daniel Găină
(Japan Advanced Institute of Science and Technology, Nomi, Japandaniel@jaist.ac.jp)
Kokichi Futatsugi(Japan Advanced Institute of Science and Technology, Nomi, Japanfutatsugi@jaist.ac.jp)
Kazuhiro Ogata(Japan Advanced Institute of Science and Technology, Nomi, Japanogata@jaist.ac.jp)

Abstract: Many computer science applications concern properties that are true for a restrictedclass of models. In this paper, a couple of constructor-based institutions are presented. These
institutions are defined on top of some base institutions, roughly speaking, by enhancing thesyntax with constructor symbols and restricting the semantics to models with elements that arereachable by constructors. The proof rules for the constructor-based Horn logics, formalized as
institutions, are defined in this paper, and a proof of completeness is provided in the abstract
framework of institutions.
Key Words: institution, Horn logic, proof theory, completeness, induction, constructor.
Category: F.3, F.4

1

Introduction

Equational specification and programming constitute the basis of modern algebraic
specification languages like CASL [Astesiano et al., 2002], Maude [Clavel et al., 2007]
and CafeOBJ [Diaconescu and Futatsugi, 2002]. In 1935 Birkhoff provided the first
proof of completeness for equational logic, in the unsorted case. Goguen and Meseguer
extended this result to cover the many-sorted case, providing a full algebraisation offinitary many-sorted equational deduction. In [Codescu and Găină, 2008], the result iscast in the framework of institutions [Goguen and Burstall, 1992] capturing both thefinitary and the infinitary cases. In this paper, an institution-independent completenessresult for constructor-based Horn logics is presented. Preliminary results of this study
were published in [Găină et al., 2009]. However, the full treatment of the topic, including the proofs, can be found in this paper.
The theory of institutions of Goguen and Burstall is a category-based formalizationof the intuitive notion of logical system that has gained foundational status in algebraic specification theory. Horn institutions are obtained by restricting the sentencesof a given institution, for example the institution of first-order logic, to the so-calledV
Horn sentences of the form (∀X) H ⇒ C, where H is a set of atoms, and C is anatom. Constructor-based institutions [Bidoit et al., 2003] are obtained from a base institution, basically by enhancing the syntax with constructor symbols and restricting thesemantics to reachable models. The signatures of constructor-based institutions consistof a signature in the base institution and a distinguished family of sets of constructor
operators. The result sorts of the constructors are called constrained, and a sort thatis not constrained is called loose. The constructors determine the class of reachable
models, which are of interest from the user point of view. Intuitively, the carrier setsof such models consist of constructor-generated elements. In other words, the elements“can be reached” through constructors and constants of loose sorts. The sentences andthe satisfaction condition are preserved from the base institution. In order to obtain aconstructor-based institution, the signature morphisms of the base institution are restricted such that the reducts along the signature morphisms of the models that arereachable (in the target signature) are again reachable (in the source signature). In theexamples presented in this paper it is simply required that constructors are preserved bysignature morphisms, and no “new” constructors are introduced for “old” constrained
sorts (for sorts being in the image of some constrained sorts of the source signature).
The proof rules for the constructor-based Horn institutions are established in thisresearch. Also, a proof of completeness using institution-independent techniques is provided in two steps:
1. We give an institution-independent definition of reachable model, and we apply it toobtain a new institution by enhancing the syntax of a base institution with constructors and restricting the semantics to reachable models. We prove an abstract layered
completeness for reachable institutions, which are a particular case of constructorbased institutions, where all operators of constrained sorts are constructors.
2. We lift completeness from reachable institutions to constructor-based institutions
such that the new result depends on sufficient completeness. Intuitively, a specification (Σ, Ax), where Ax is a set of conditional equations over the vocabulary givenby the signature Σ, is sufficient complete when any term can be reduced to a term
formed with constructors and variables of loose sorts using the equations from Ax.
The present work constitutes the logical foundation of the so-called OTS/CafeOBJ
method. This is a method of modeling, specifying and verifying systems, which has
been developed and refined through some case studies (see [Ogata and Futatsugi, 2008]
and [Ogata and Futatsugi, 2003]). This paper fully justifies the practice of using constructors in connection with induction schemes and case analysis. One of the important
advantages of our approach is the institution-independent status of our concepts and results. In [Codescu and Găină, 2008] and [Găină and Petria, 2010] the completeness isobtained directly, whereas in this research, an intermediate result is obtained for reachable institutions, and then it is extended to constructor-based institutions via sufficientcompleteness.
Section 2 introduces the notions of institution and entailment system. These willconstitute the base for expressing the soundness and completeness properties for a logic,
i.e. that semantic deduction coincides with syntactic provability. Section 3 introduces
the abstract concept of universal institution and reachable universal entailment system,
which is proved sound and complete under conditions that are also investigated. Section
4 contains the main result. The completeness result of reachable institutions is extended
to constructor-based institutions via sufficient completeness. Section 5 concludes thepaper and discusses future work.
We assume that the reader is familiar with the basic notions of category theory. See[Mac Lane, 1998] for the standard definitions of category, functor, pushout, etc., whichhave been omitted here.

2

Institutions

Institutions were introduced in [Goguen and Burstall, 1992] with the original goal ofproviding an abstract framework for algebraic specification languages.
Definition 1. An institution I = (SigI , SenI , Mod I , |=I ) consists of
1. a category SigI , whose objects are called signatures,
2. a functor SenI : SigI → Set, providing for each signature Σ a set whose elements
are called (Σ-)sentences,
3. a functor Mod I : SigI → Cat op , providing for each signature Σ a category whose
objects are called (Σ-)models and whose arrows are called(Σ-)morphisms,
4. a relation |=IΣ ⊆ |Mod I (Σ)| × SenI (Σ) for each signature Σ, called (Σ-)satisfaction,such that for each signature morphism ϕ : Σ → Σ0 the following satisfaction condition holds:
M 0 |=IΣ0 SenI (ϕ)(e) iff Mod I (ϕ)(M 0 ) |=IΣ e
for all M 0 ∈ |Mod I (Σ0 )| and e ∈ SenI (Σ).
We denote the reduct functor Mod I (ϕ) by ϕ and the sentence translation SenI (ϕ)
by ϕ( ). When M = M 0ϕ we say that M is the ϕ-reduct of M 0 and M 0 is a ϕ-expansionof M. When there is no danger of confusion, we omit the superscript from the notationsof the institution components; for example SigI may be simply denoted by Sig.
Example 1 First-order logic (FOL) [Goguen and Burstall, 1992]. 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, and P = (Pw )w∈S∗ is the (S∗ -indexed) set of relation symbols.
If w = λ, an element of Fw→s is called a constant symbol, or a constant. By a slight noS
S
tational 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 (S0 , F 0 , P0 ) is a triplet ϕ = (ϕst , ϕop , ϕrl ),where ϕst : S → S0 , ϕop : F → F 0 , ϕrl : P → P0 such that ϕop (Fw→s ) ⊆ Fϕ0 st (w)→ϕst (s) andϕrl (Pw ) ⊆ Pϕ0 st (w) for all (w, s) ∈ S∗ × S. When there is no danger of confusion, we may
let ϕ denote each of ϕst , ϕrl and ϕop . Given a signature Σ = (S, F, P), a Σ-model M isa triplet M = ((Ms )s∈S , (Mw,s (σ))(w,s)∈S∗ ×S,σ∈Fw→s , (Mw (R))w∈S∗ ,R∈Pw ) interpreting eachsort s as a set Ms , each operation symbol σ ∈ Fw→s as a function Mw,s (σ) : Mw → Ms
(where Mw stands for Ms1 × . . . × Msn if w = s1 . . . sn ), and each relation symbol R ∈ Pw
as a relation Mw (R) ⊆ M w . When there is no danger of confusion we may let Mσ andMR denote Mw,s (σ) and Mw (R) respectively. Morphisms between models are the usual
Σ-morphisms, i.e., S-sorted functions that preserve the structure. The Σ-sentences are
obtained from– equality atoms t1 = t2 , where t1 ,t2 ∈ (T(S,F) )s and T(S,F) is the (S, F)-algebra ofground terms, or– relational atoms R(t1 , . . . ,tn ), where R ∈ Ps1 ...sn and ti ∈ (T(S,F) )si for all i ∈ {1, . . . , n},
by applying a finite number of times negation, conjunction, disjunction, and universal
or existential quantification over finite sets of constants (variables). Satisfaction is theusual first-order satisfaction and is defined using the natural interpretations of groundterms 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 theforgetful functor.
Example 2 Horn clause logic (HCL). A universal Horn sentence for a FOL signature
V(S, F, P) is a (universal) sentence of the form (∀X)( H) ⇒ C, where X is a finite set ofvariables, H is a finite set of (relational or equational) atoms, and C is a (relational or
equational) atom. 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.
Example 3 Constructor-based Horn clause logic (CHCL). Its signatures (S, F, F c , P)
consist of a first-order signature (S, F, P), and a distinguished subfamily F c ⊆ F ofsets of operation symbols called constructors. The constructors determine the set of
c . We call the sorts
constrained sorts Sc ⊆ S: s ∈ Sc iff there exists a constructor σ ∈ Fw→sin Sl = S − Sc loose. The (S, F, F c , P)-sentences are the universal Horn sentences of theVform (∀X)(∀Y ) H ⇒ C, where X is a finite set of variables of constrained sorts, Y isa finite set of variables of loose sorts, H is a finite set of atoms and C is an atom.
The (S, F, F c , P)-models are the usual first-order (S, F, P)-models M reachable by
the constructors in F c , i.e. there exists a set Y of variables of loose sorts, and a function
f : Y → M such that for every constrained sort s ∈ Sc the function fs# : (T(S,F c ) (Y ))s → Ms
is a surjection, where f # : T(S,F c ) (Y ) → M(S,F c ) is the unique extension of f to a (S, F c )morphism.

A signature morphism ϕ : (S, F, F c , P) → (S0 , F 0 , F 0c , P0 ) in CHCL is a first-ordersignature morphism ϕ : (S, F, P) → (S0 , F 0 , P0 ) such that the constructors are preserved
along the signature morphisms (i.e. if σ ∈ F c then ϕ(σ) ∈ F 0c ) and no “new” constructors are introduced for “old” constrained sorts (i.e. if s ∈ Sc and σ0 ∈ (F 0c )w0 →ϕ(s) thencthere exists σ ∈ Fw→ssuch that ϕ(σ) = σ0 ).
Lemma 2. For every CHCL signature morphism ϕ : (S, F, F c , P) → (S0 , F 0 , F 0c , P0 ) andany (S0 , F 0 , F 0c , P0 )-model M 0 , we have M 0ϕ ∈ Mod(S, F, F c , P).
Proof. Let YM0 be a renaming of the loose elements of M such that YM0 is disjoint fromthe constants in F 0 . This means that there exists a S0 -sorted function conM0 : YM0 →/ and for all s0 ∈ S0l , (conM0 )s0 : (YM0 )s0 → Ms0 0 is
M 0 such that for all s0 ∈ S0c , YM0 = 0,bijective. Since M 0 ∈ Mod(S0 , F 0 , F 0c , P0 ), the unique extension con#M0 : T(S0 ,F 0c ) (YM0 ) →M 0(S0 ,F 0c ) of conM0 to a (S0 , F 0c )-morphism is surjective. We define M = M 0ϕ . Let YM
be a renaming of the loose elements of M such that YM is disjoint from the constantsin F. There exists a S-sorted function conM : YM → M such that for all s ∈ Sc , YM =/ and for all s ∈ Sl , (conM )s : (YM )s → Ms is bijective. We show that for all s ∈ S
0,and t 0 ∈ T(S0 ,F 0c ) (YM0 ) there exists t ∈ T(S,F c ) (YM ) such that con#M0 (t 0 ) = con#M (t), wherecon# : T(S,F c ) (YM ) → M(S,F c ) is the unique extension of conM to a (S, F c )-morphism.
We proceed by induction on the structure of the terms in T(S0 ,F 0c ) (YM0 ).
1. For the base case, let s ∈ S and t 0 ∈ (YM0 )ϕ(s) . It follows that ϕ(s) ∈ S0l , which
00implies s ∈ Sl . Take t = con−1
M (conM 0 (t )), and we have conM (t) = conM 0 (t ).
2. For the induction step, let s ∈ S, σ0 ∈ Fw0c0 →ϕ(s) and t 0 ∈ (T(S0 ,F 0c ) (YM0 ))w0 . Therecexists σ ∈ Fw→ssuch that ϕ(σ) = σ0 . By the induction hypothesis, there exists t ∈(T(S,F c ) (YM ))w such that con#M (t) = con#M0 (t 0 ). Hence, con#M (σ(t)) = Mσ (con#M (t)) =Mσ0 0 (con#M0 (t 0 )) = con#M0 (σ0 (t 0 )).
Since conM0 is surjective, conM is surjective too. Therefore, M ∈ Mod(S, F, F c , P).

tu

Variants of constructor-based first-order logic were studied in [Bidoit et al., 2003] and[Bidoit and Hennicker, 2006].
Example 4 Order-sorted algebra (OSA) [Goguen and Meseguer, 1992]. A OSA signature (S, ≤, F) consists of an algebraic signature (S, F), with a partial ordering (S, ≤)such that the following 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 amorphism of algebraic signatures (S, F) → (S0 , F 0 ) such that the ordering is preserved,
i.e. ϕ(s1 ) ≤0 ϕ(s2 ) whenever s1 ≤ s2 .
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 andw1 ≤ w2 implies Mσw1 ,s1 = Mσw2 ,s2 |Mw1 . Given order-sorted (S, ≤, F)-algebras M and N,
an order-sorted (S, ≤, F)-morphism h : M → N is a (S, F)-morphism such that s1 ≤ s2
implies hs1 = hs2 |Ms1 .

An OSA signature (S, ≤, F) is regular iff for each σ ∈ Fw1 →s1 and each w0 ≤ w1
there is a unique least element in the set {(w, s) | σ ∈ Fw→s and w0 ≤ w}. For regularsignatures (S, ≤, F), any (S, ≤, F)-term has a least sort and the initial (S, ≤, F)-algebra
can be defined as a term algebra, cf. [Goguen and Meseguer, 1992]. Let (S, ≤, F) be anorder-sorted signature. We say that the sorts s1 and s2 are in the same connected component of S iff s1 ≡ s2 , where ≡ is the least equivalence on S that contains ≤. A partial
ordering (S, ≤) is filtered iff for all s1 , s2 ∈ S, there is some s ∈ S such that s1 ≤ s ands2 ≤ s. A partial ordering is locally filtered iff every connected component of it is filtered. An order-sorted signature (S, ≤, F) is locally filtered iff (S, ≤) is locally filtered,and it is coherent iff it is both locally filtered and regular. Hereafter we assume that all
OSA signatures are coherent. The atoms of the signature (S, ≤, F) are equations of theform t1 = t2 such that the least sort of the terms t1 and t2 are in the same connectedcomponent. The sentences are closed formulas built by application of Boolean connectives and quantification to the equational atoms. Order-sorted algebras were extensively
studied in [Goguen and Diaconescu, 1994] and [Goguen and Meseguer, 1992]. HOSA
is obtained by restricting OSA to universal Horn sentences.
Example 5 Constructor-based Horn order-sorted algebra (CHOSA). This institution isdefined on top of HOSA similarly as CHCL is defined on top of HCL. The constructorbased order-sorted signatures (S, ≤, F, F c ) consist of an order-sorted signature (S, ≤, F),
and a distinguished subfamily F c ⊆ F of sets of operational symbols, called constructors, such that (S, ≤, F c ) is an order-sorted signature (the monotonicity and coherence
conditions are satisfied). The sort s ∈ S is constrained if there exists a constructorcσ ∈ Fw→s
with the result sort s. As in the first case, we let Sc to denote the set of
all constrained sorts. We call the sorts in Sl = S − Sc loose. The (S, ≤, F, F c )-sentencesV
are the universal Horn sentences of the form (∀X)(∀Y ) H ⇒ C, where X is a finite setof variables of constrained sorts, Y is a finite set of variables of loose sorts, H is a finite
set of equational atoms and C is an equational atom.
The (S, ≤, F, F c )-models are the usual order-sorted algebras with the carrier sets
for the constrained sorts consisting of interpretations of terms formed with constructors
and elements of loose sorts, i.e. there exists a set of loose variables Y , and a function
f : Y → M such that for every constrained sort s ∈ Sc the function fs# : (T(S,≤,F c ) (Y ))s →Ms is a surjection, where f # : T(S,≤,F c ) (Y ) → M(S,≤,F c ) is the unique extension of f toa (S, ≤, F c )-morphism.
A CHOSA signature morphism ϕ : (S, ≤, F, F c ) → (S0 , ≤0 , F 0 , F 0c ) is an order-sorted
signature morphism such that constructors are preserved along the signature morphisms(i.e. if σ ∈ F c then ϕ(σ) ∈ F 0c ), and no “new” constructors are introduced for “old”
cconstrained sorts (i.e. if s ∈ Sc and σ0 ∈ (F 0c )w0 →ϕ(s) then there exists σ ∈ Fw→s
such
0
0
0
c
0
0
that ϕ(σ) = σ , and if s0 ∈ S and s ∈ S such that s0 ≤ ϕ(s) then there exists s0 ∈ Ssuch that s0 ≤ s and ϕ(s0 ) = s00 ).
Example 6 Preorder algebra (POA) [Diaconescu and Futatsugi, 1998]. The POA signatures are just the ordinary algebraic signatures. The POA models are preordered al-gebras which are interpretations of the signatures into the category of preorders Pre
rather than the category of sets Set. This means that each sort gets interpreted as apreorder, and each operation as a preorder functor, which means a preorder-preserving(i.e. monotonic) function. A preordered algebra morphism is just a family of preorderfunctors (preorder-preserving functions) which is also an algebra morphism. POA constitutes an unlabeled form of Meseguer’s rewriting logic [Meseguer, 1992], but the later
is not an institution.
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
are in the preorder relation of the carrier, i.e. Mt ≤ Mt 0 . Full sentences are constructedfrom equational and preorder atoms by using Boolean connectives and first-order quantification.
As in the case of FOL we define Horn preorder algebra (HPOA) by restricting
the sentences to universal Horn sentences. The institution of constructor-based Hornpreorder algebra (CHPOA) is obtained in the same way as in the first-order case.
Example 7 Partial algebra (PA) [Reichel, 1984, Burmeister, 1986]. A partial algebraic
signature (S, F) consists of a set S of sorts and a set F of partial operations. We assume
that there is a distinguished constant on each sort ⊥s : s. Signature morphisms map thesorts and operations in a compatible way, preserving ⊥s .
A partial algebra is just like an ordinary algebra but interpreting the operations ofF as partial rather than total functions; ⊥s is always interpreted as undefined. A partialhalgebra (S, F)-morphism h : A → B is a family of (total) functions (As →s Bs )s∈S suchthat hs (Aσ (a)) = Bσ (hw (a)) for each operation σ : w → s and each string of argumentsa ∈ Aw for which Aσ (a) is defined.
Remark. For every inclusion Σ ,→ Σ(Z), where Σ = (S, F) and Σ(Z) = (S, F ∪ Z), theΣ(Z)-models can be represented as pairs (M, h) where M is a Σ-model and h : Z 0 → A
is a function such that Z 0 ⊆ Z is the set of constants which are defined in M.
e

We consider one kind of “base” sentences: existence equality t = t 0 . The existence equale
ity t = t 0 holds when both terms are defined and equal. The definedness predicate andesstrong equality can be introduced as notations: def (t) stands for t = t and t = t 0 standsVe 0
for (t = t ) ∨ (¬def (t) ¬def (t0 )). We consider the atomic sentences in Sen(S, F) tobe the atomic existential equalities. The sentences are formed from these “base” sentences by Boolean connectives and quantification over variables. The definition of PA
given here is slightly different from the one in [Mosses, 2004, Astesiano et al., 2002,
Mossakowski, 2002] since it does not consider total operation symbols.
Example 8 Constructor-based partial algebra (CHPA). The signatures of constructorbased partial algebra (S, F, F c ) consist of a signature (S, F) in the base institution, and a
distinguished subfamily F c ⊆ F of sets of constructors. The constructors determine thecset of constrained sorts Sc ⊆ S: s ∈ Sc iff there exists a constructor σ ∈ Fw→swith theresult sort s, and the set of loose sorts Sl = S − Sc .
The (S, F, F c )-sentences are the universal Horn sentences formed over existential
equations. The (S, F, F c )-models are the usual partial algebras M with the carrier sets forthe constrained sorts consisting of interpretations of terms formed with constructors andvariables of loose sorts, i.e. there exists a set Y of variables of loose sorts, and a function
f : Y → M such that for every constrained sort s ∈ Sc the function fs# : (T(M, f ) )s → Ms
is a surjection, where T(M, f ) ⊆ T(S,F c ∪Y ) is the maximal partial (S, F c ∪ Y )-algebra ofterms such that (M, f ) |= de f (t) for all t ∈ T(M, f ) , and f # : T(M, f ) → (M, f )(S,F c ∪Y ) is
the unique (S, F c ∪Y )-morphism extending f .
A constructor-based partial signature morphisms ϕ : (S, F, F c ) → (S1 , F1 , F1c ) is a PA
signature morphism ϕ : (S, F) → (S1 , F1 ) such that the constructors are preserved along
the signature morphisms (i.e. if σ ∈ F c then ϕ(σ) ∈ F1c ), and no “new” constructors are
introduced for “old” constrained sorts (i.e. if s ∈ Sc and σ1 ∈ (F1c )w1 →ϕ(s) then therecexists σ ∈ Fw→ssuch that ϕ(σ) = σ1 ).

Example 9 Reachable Horn clause logic (RHCL). RHCL is obtained from CHCL by
restricting the signatures such that all operation symbols of constrained sorts are conc
structors, i.e. for each (S, F, F c , P) we have F c = F S where
Fw→s : s ∈ Sc
Sc
Fw→s
=
0/ : s 6∈ Sc
In this case, we choose to denote each signature (S, F, F c , P) by (S, Sc , F, P) where Sc is
the set of constrained sorts.
Similarly, one may define RHOSA, RHPOA and RHPA.
2.1

Substitutions
χ1

χ2

In CHCL, consider Σ ,→ Σ(X1 ) and Σ ,→ Σ(X2 ) two inclusion signature morphisms,
where Σ = (S, F, F c , P) is a CHCL signature, Xi is a set of constant symbols disjoint
from the constants of F, and Σ(Xi ) = (S, F ∪ Xi , F c , P). Any substitution θ : X1 →T(S,F) (X2 ) can be extended to a function Sen(θ) : Sen(Σ(X1 )) → Sen(Σ(X2 )) that replaces all the symbols in X1 by the corresponding (S, F ∪ X2 )-terms, according to θ.
This can be formally defined as follows:(1) Sen(θ)(t = t 0 ) = (θtm (t) = θtm (t 0 )), for all equational Σ(X1 )-atoms t = t 0 , whereθtm : T(S,F) (X1 ) → T(S,F) (X2 ) is the unique extension of θ to a (S, F)-morphism.
(2) Sen(θ)(π(t1 , . . . ,tn )) = π(θtm (t1 ), . . . , θtm (tn )), for all Σ(X1 )-atoms π(t1 , . . . ,tn ).
(3) Sen(θ)( H ⇒ C) =V

V

Sen(θ)(H) ⇒ Sen(θ)(C), for all Σ(X1 )-sentencesV

H ⇒ C.

(4) Sen(θ)((∀Z1 )ρ) = (∀Z2 )Sen(θb )(ρ), for all Σ(X1 )-sentences (∀Z1 )ρ, where– Z2 is obtained by renaming the constants in Z1 , i.e. there is a bijection b : Z1 →
Z2 , such that Z2 is disjoint from the constants of Σ(X2 ), and– θb : Σ(X1 ∪ Z1 ) → Σ(X2 ∪ Z2 ) works like θ on Σ(X1 ) and maps every z1 ∈ Z1 tob(z1 ) ∈ Z2 .
On the semantics side, θ determines a functor Mod(θ) : Mod(Σ(X2 )) → Mod(Σ(X1 ))such that for all Σ(X2 )-models M we have(1) Mod(θ)(M)z = Mz , for each sort z ∈ S, or operation symbol z ∈ F, or relation
symbol z ∈ P, and(2) Mod(θ)(M)z = Mθ(z) for each z ∈ X1 .
Proposition 3. For every CHCL signature Σ and each substitution θ : X1 → Σ(X2 )Mod(θ)(M) |= ρ iff M |= Sen(θ)(ρ)
for all Σ(X2 )-models M and all Σ(X1 )-sentences ρ.
The proof is the same as the one for FOL, which can be found in [Diaconescu, 2004].
Assumption 2.1 Throughout this paper, for all institutions above, we assume that signature morphisms allow mappings of constants to terms.
The above assumption makes it possible to treat first-order substitutions in the comma
category 1 of signature morphisms.
χ1

χ2

Definition 4. Consider two signature morphisms Σ → Σ1 and Σ → Σ2 of an institution.
A signature morphisms θ : Σ1 → Σ2 such that χ1 ; θ = χ2 is called a Σ-substitution between χ1 and χ2 .
2.2

Entailment systems

A sentence system (Sig, Sen) consists of a category of signatures Sig and a sentencefunctor Sen : Sig → Set. An entailment system [Meseguer, 1989] E = (Sig, Sen, `) consists of a sentence system (Sig, Sen) and a family of entailment relations `= (`Σ )Σ∈|Sig|between sets of sentences with the following properties:(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 , andϕ(Translation) ϕ(E1 ) `Σ0 ϕ(E2 ) if E1 `Σ E2 , for all Σ → Σ0 ∈ Sig.
f
1 Given a category C and an object A ∈ |C |, the comma category A/C has arrows A →B∈C
as objects, and h ∈ C (B, B0 ) with f ; h = f 0 as arrows.

The semantic entailment system of an institution I = (Sig, Sen, Mod, |=) consists of(Sig, Sen, |=). When there is no danger of confusion we may omit the subscript Σ from`Σ . For every signature morphism ϕ ∈ Sig, we sometimes let ϕ denote the sentencetranslation Sen(ϕ). An entailment system (Sig, Sen, `) is sound (resp. complete) for an
institution (Sig, Sen, Mod, |=) if Γ `Σ ρ implies Γ |=Σ ρ (resp. Γ |=Σ ρ implies Γ `Σ ρ)
for every signature Σ, each set of Σ-sentences Γ and any Σ-sentence ρ. We call theentailment system E = (Sig, Sen, `) compact whenever for every Γ ⊆ Sen(Σ) and eachfinite E f ⊆ Sen(Σ) if Γ `Σ E f then there exists Γ f ⊂ Γ finite such that Γ f `Σ E f . For eachentailment system E = (Sig, Sen, `) one can easily construct the compact entailment
subsystem [Diaconescu, 2006] E c = (Sig, Sen, `c ) by defining the entailment relation`c as follows: Γ `cΣ E iff for each finite set E f ⊆ E there exists a finite set Γ f ⊆ Γ suchthat Γ f `Σ E f .
Lemma 5 (Compact entailment subsystems) [Diaconescu, 2006]. (Sig, Sen, `c ) is anentailment system.
2.3

Basic sentences

A set of sentences B ⊆ Sen(Σ) is called basic [Diaconescu, 2003] if there exists a Σmodel MB such that, for all Σ-models M, M |= B iff there exists a morphism MB → M.
We say that MB is a basic model of B. If in addition the morphisms MB → M is uniquethen the set B is called epi basic. It is well-known that any set of atoms in FOL and
POA is epi basic (see for example [Diaconescu, 2003] or [Diaconescu, 2008]).
Lemma 6. Any set of atomic sentences in FOL, OSA, POA and PA is epi basic.
Proof. In FOL, for a set E of atomic (S, F, P)-sentences there exists a basic model
ME . Actually it is the initial model for E. This is constructed as follows: on the quotient (T(S,F) )=E of the term model T(S,F) 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 OSA and POA too.
In PA for a set of atomic sentences E we define SE as the set of sub-terms appearing
in E. Note that SE is a partial algebra. The basic model ME will be the quotient of SE
by the partial congruence induced by the equalities in E.
tu
2.4

Internal logic

The following institutional notions dealing with logical connectives and quantifiers
were defined in [Tarlecki, 1986].
Let Σ be a signature of an institution, a Σ-sentence– ¬e is a (semantic) negation of the Σ-sentence e when for every Σ-model M we have
M |=Σ ¬e iff M 2Σ e,

– e1 ∧ e2 is a (semantic) conjunction of the Σ-sentences e1 and e2 when for every
Σ-model M we have M |=Σ e1 ∧ e2 iff M |=Σ e1 and M |=Σ e2 ,– e1 ⇒ e2 is a (semantic) implication of the Σ-sentences e1 and e2 when for every
Σ-model M we have M |=Σ e1 ⇒ e2 iff M |=Σ e1 implies M |=Σ e2 , andχ– (∀χ)e0 , where Σ → Σ0 ∈ Sig and e0 ∈ Sen(Σ0 ), is a (semantic) universal χ-quantification of e0 when for every Σ-model M we have M |=Σ (∀χ)e0 iff M 0 |=Σ0 e0 for allχ-expansions 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 -quantifications when for each Σ → Σ0 ∈ D , each Σ0 -sentence
has a universal χ-quantification.
2.5

Reachable models

In this subsection we give an abstract characterizations of reachable models.
Definition 7. Let D be a broad subcategory 2 of signature morphisms of an institution
I = (Sig, Sen, Mod, |=). We say that a Σ-model M is D -reachable if for each span of
χ1χsignature morphisms Σ1 ← Σ0 → Σ in D , each χ1 -expansion M1 of Mχ determines a
substitution θ : χ1 → χ such that Mθ = M1 .
In concrete examples of institutions, D -reachable models correspond to models
with elements reachable by ground terms.
Proposition 8. In FOL, OSA, POA and PA, assume that D is the class of signatureextensions with constants. A model M is D -reachable iff its elements are the interpretations of terms.
Proof. In FOL, let Σ = (S, F, P) be a signature, X and Y two disjoint sets of constants
with elements that are different from the constants in F, and (M, h) a Σ(Y )-model withelements that are interpretation of terms, i.e. the unique extension h# : TΣ (Y ) → M of h
to a Σ-morphism is surjective. Then for every Σ(X)-model (M, g) there exists a function
θ : X → TΣ (Y ) such that θ; h# = g. Note that for any x ∈ X we have ((M, h)θ )x =h# (θ(x)) = g(x) = (M, g)x . Therefore, (M, h)θ = (M, g).
For the converse implication, let Σ = (S, F, P) be a signature and assume a Σ-model
M that is D -reachable. We prove that TΣ → M is surjective, i.e. for every m ∈ M there
exists t ∈ TΣ such that Mt = m. Let m ∈ Ms be an arbitrary element of M. Consider avariable x of sort s and let N be an expansion of M along Σ ,→ Σ(x) (where Σ(x) =2 C 0 is a broad subcategory of C if |C 0 | = |C |.

(S, F ∪ {x}, P)) which interprets the constant symbol x as m. Since M is D -reachable
there exists a substitution θ : {x} → TΣ such that Mθ = N. Take t = θ(x) and we have
Mt = Mθ(x) = (Mθ )x = Nx = m.
One can replicate the arguments above for OSA and POA too.
In PA, let Σ = (S, F) be a signature, X and Y two sets of constants with elementsthat are different from the constants in F, and M a Σ(Y )-model, with elements that areinterpretations of terms, i.e. the unique Σ(Y )-morphism h : TM → M is surjective, whereTM ⊆ TF∪Y is the maximal algebra of terms such that M |= de f (t) for all t ∈ TM . Let M 0
be a Σ(X)-expansion of MΣ , where M 0 = (MΣ , g), g = (gs : Xs0 → Ms )s∈S and X 0 ⊆ X are
all constants of X defined in M 0 . Since h is surjective, there exists a function θ0 : X 0 → TMsuch that θ0 ; h = g. We straightforwardly extend θ0 to a substitution θ : X → TΣ (Y ) suchthat θ is equal to θ0 on X 0 , and θ(x) = ⊥ for all x ∈ (X\X 0 ). Note that for every– x ∈ X 0 we have: (Mθ )x = Mθ(x) = Mθ0 (x) = h(θ0 (x)) = g(x) = Mx0 ;0 = M0 .
– x ∈ (X\X 0 ) we have: (Mθ )x = Mθ(x) = M⊥ = M⊥xHence Mθ = M 0 .
For the converse implication, consider a partial (S, F)-algebra M that is D -reachable. We prove that for all m ∈ M there exists a term t ∈ TΣ such that Mt = m. Letm ∈ Ms be an arbitrary element of M. Consider a variable x of sort s and let N be an
expansion of M along Σ ,→ Σ(x) which interprets the constant symbol x as m. Since M is
D -reachable, there exists a substitution θ : {x} → TΣ such that Mθ = N. Take t = θ(x),and we have Mt = Mθ(x) = (Mθ )x = Nx = m.
tuRemark. Note that for each set E of atomic sentences in FOL, OSA, POA and PA
the basic model ME is D -reachable, where D is the class of signature extensions withconstants.
Definition 9. We say that a signature morphism ϕ : Σ → Σ0 is finitary if it is finitely
presented 3 in the comma category Σ/Sig.
In typical institutions the extensions of signatures with a finite number of symbols are
finitary.
Definition 10. Assume two broad subcategories of signature morphisms D and D l . A
ϕΣ-model M is (D , D l )-reachable if there exists a signature morphism Σ → Σ0 ∈ D anda D -reachable Σ0 -model M 0 such that
3 An object A in a category C is finitely presented ([Adámek and Rosický, 1994]) ifµi– for each directed diagram D : (J, ≤) → C with co-limit {Di → B}i∈J , and for each morphismggi
A → B, there exists i ∈ |J| and A → Di such that gi ; µi = g,
– for any two arrows gi and g j as above, there exists k ∈ |J| such that i ≤ k, j ≤ k and gi ; D(i ≤k) = g j ; D( j ≤ k).

1. M 0ϕ = M, and
ui, j

u

2. ϕ is the vertex of a co-limit (ϕi →i ϕ)i∈J of a directed diagram (ϕi → ϕ j )(i≤ j)∈(J,≤)
in Σ/Sig, with ϕi ∈ D l for all i ∈ J.
Throughout this paper we implicitly assume that D represents the subcategory of signature morphisms that consists of signature extensions with constants, and D l represents
the subcategory of signature morphisms that consists of signature extensions with a finite number of constants of loose sorts. In institutions such as HCL, HOSA, HPOA
and HPA, for each signature we consider the set of constrained sorts empty; therefore
all sorts are regarded as loose, and D consists of signature extensions with constants ofany sort, and D l consists of signature extensions with a finite number of constants ofany sort.
Proposition 11. In CHCL, all models are (D , D l )-reachable.
Proof. Let M be a Σ-model, where Σ = (S, F, F c , P). There exists an assignment f :Y → M, where Y is a set of loose variables that are different from the constants in F,
such that the unique extension f # : T(S,F c ) (Y ) → M(S,F c ) of f to a (S, F c )-morphismϕis surjective. The inclusion Σ ,→ Σ(Y ), where Σ = (S, F ∪Y, F c , P), is the vertex of the
ϕi

ui

ϕ

ϕi

directed co-limit ((Σ ,→ Σ(Yi )) ,→ (Σ ,→ Σ(Y )))Yi ⊆Y f inite of the directed diagram ((Σ ,→
ui, j

ϕj

Σ(Yi )) ,→ (Σ ,→ Σ(Y j )))Yi ⊆Y j ⊆Y f inite . Since for all s ∈ S the function fs# : (T(S,F c ) (Y ))s →Ms is surjective, the elements of (M, f ) consist only of interpretations of terms. By
Proposition 8, (M, f ) is D -reachable, and by Definition 10, M is (D , D l )-reachable.
tu
In the following we prove an important property of (D , D l )-reachable models.
Proposition 12. Assume a (D , D l )-reachable Σ-model M as in Definition 10, and aχ
finitary signature morphism Σ → Σ1 ∈ D . Then every χ-expansion M1 of M generates
ψa substitution θ : χ → ψ, and a ψ-expansion M2 of M such that Σ → Σ2 ∈ D l andM2θ = M1 .
Proof. Let M be a (D , D l )-reachable model as in Definition 10 and let M1 be a χχ
expansion of M, where Σ → Σ1 ∈ D is finitary. Since M 0 is D -reachable there exists a
substitution v : χ → ϕ such that M 0v = M1 . Because χ is finitary there exists a substitution vi : χ → ϕi such that vi ; ui = v. Then take ψ = ϕi , θ = vi and M2 = M 0ui .
tu
Since the subcategories D and D l of signature morphisms are fixed in concrete
institutions, we will refer to D -reachable model(s) as ground reachable model(s), andto (D , D l )-reachable model(s) as reachable model(s).

3Universal Institutions

The reachable universal entailment system (RUES) developed in this section consistsof four layers:
1. the “atomic” layer of the atomic entailment system (AES), which in abstract settings
is assumed but is developed in concrete examples,
2. the layer of the entailment system with implications (IES) obtained by adding to the
AES the rules of implication,
3. the layer of the generic universal entailment system (GUES) obtained by adding to
the IES the rules for the quantification over variables of loose sorts, and4. the upmost layer of the RUES of I is obtained by adding to the GUES the rules forthe quantification over variables of constrained sorts.
Soundness and completeness at each layer are obtained relatively to the soundness andcompleteness of the layer immediately below.
Definition 13. Consider an institution I = (Sig, Sen, Mod, |=), and let D • , Sign ⊆ Sig
be two broad subcategories of signature morphisms, and Senn : Sign → Set a sub-functorof Sen 4 . We denote by In the institution (Sign , Senn , Modn , |=n ), where– Modn : Sign → Cat op is the restriction of Mod : Sig → Cat op to Sign , and– for all Σ ∈ |Sig|, (|=n )Σ is the restriction of |=Σ to |Mod(Σ)| × Senn (Σ).
We say that I is a D • -universal institution over In whenχ

1. (∀χ)ρ ∈ Sen(Σ) for all Σ → Σ0 ∈ D • and ρ ∈ Senn (Σ0 ), and2. any sentence of I is of the form (∀χ)ρ as above.
Fact 3.1 If I = (Sig, Sen, Mod, |=) is a D • -universal institution over the institution
In = (Sign , Senn , Modn , |=n ) then for all Σ ∈ |Sig| = |Sign |, Γ ⊆ Senn (Σ) and ρ ∈Senn (Σ) we have Γ |=n ρ iff Γ |= ρ.
For example CHCL is a D c -universal institution over its restriction CHCL2 to(a) signature morphisms that do not add constructors on “old” sorts, and(b) sentences quantified over finite sets of variables of loose sorts,

4 For each signature Σ ∈ |Sig | we have Sen (Σ) ⊆ Sen(Σ) and for any signature morphismnnΣ → Σ0 ∈ Sign we have ϕ(Senn (Σ)) ⊆ Senn (Σ0 )).
ϕwhere D c consists of signature extensions with a finite number of constants of constrained sorts. If SigCHCL2 = SigCHCL then the translation of a sentence quantified overa variable of loose sort may be a sentence quantified over a variable of constrained sort,which implies that CHCL2 is not an institution.
Example 10. Consider the following example of CHCL signature morphism:
sort Trivϕ
Triv7→Nat

sort Nat/ op 0 : → Nat{constr}
op s : Nat → Nat {constr}

Note that (∀x : Triv)x = x is a sentence quantified over the variable (x : Triv), which isloose, but ϕ((∀x : Triv)x = x) is equal to (∀x : Nat)x = x, a sentence quantified over thevariable (x : Nat) which is constrained.
3.1

Reachable universal entailment systems

Our approach is top-down, and we start by defining the proof rules for the sentences
quantified over constrained variables.
Assumption 3.1 Throughout this subsection, we assume a D c -universal institution I =(Sig, Sen, Mod, |=) over I2 = (Sig2 , Sen2 , Mod2 , |=2 ), and two broad subcategories ofsignature morphisms D l ⊆ D ⊆ Sig such that D c ⊆ D , and I2 has D l -quantifications.
CHCL is a D c -universal institution over CHCL2 , where D c consists of signature extensions with a finite number of constants of constrained sorts. Assume that D and D l
are as in subsection 2.5. It follows that CHCL is an example of I = (Sig, Sen, Mod, |=).
We define the following proof rules, for the RUES of I :{Γ `Σ (∀ϕ)θ(ρ) | ϕ ∈ D l , θ : χ → ϕ is a substitution}(C-Abstraction)Γ `Σ (∀χ)ρ
where Γ ⊆ Sen(Σ) and (∀χ)ρ ∈ Sen(Σ) with χ ∈ D c .
(Substitutivity)(∀χ)ρ `Σ (∀ϕ)θ(ρ)
where (∀χ)ρ ∈ Sen(Σ) and θ : χ → ϕ is a substitution.
In CHCL, consider a set Γ of Σ-sentences and a Σ-sentence (∀x)ρ such that x is a constrained variable. In this case C-Abstraction says that if for any term t of the same sort asx formed with loose variables and operation symbols from Σ, we have Γ ` (∀Y )ρ(x ← t)
5 , where Y are all (loose) variables that occur in t, then we have proved Γ ` (∀x)ρ. In
most of the cases the set of terms t is infinite, which implies that the premises of CAbstraction are infinite, and thus, the corresponding entailment system is not compact.
Given a compact entailment system E2 = (Sig2 , Sen2 , `2 ) for I2 , the RUES of I
consists of the least entailment system over E2 closed under C-Abstraction and Substitutivity. Note that the resulting entailment system is not compact (even if E2 is compact)
5 ρ(x ← t) is the formula obtained from ρ by substituting t for x.

since the premises of C-Abstraction may be infinite. The abstract RUES above can beinstantiated to CHCL, CHOSA, CHPOA and CHPA.
Proposition 14 (R-soundness). The RUES of I is sound if the entailment system of I2
is sound, the signature morphisms in D c are finitary, and all models of I are (D , D l )reachable.
Proof. Firstly, we show that
1. C-Abstraction is sound, i.e. for a set Γ ⊆ Sen(Σ) of sentences and any sentence(∀χ)ρ ∈ Sen(Σ) with χ ∈ D c we have Γ |=Σ (∀χ)ρ whenever Γ |=Σ (∀ϕ)θ(ρ) forall substitutions θ : χ → ϕ with ϕ ∈ D l . Fix Γ and (∀χ)ρ as above, and assume
M |= Γ. Let M 0 be an χ-expansion of M. By Proposition 12, there exists a signatureϕmorphism Σ → Σ00 ∈ D l , a substitution θ : χ → ϕ, and a ϕ-expansion M 00 of M suchthat M 00θ = M 0 . We have M |= (∀ϕ)θ(ρ) which implies M 00 |= θ(ρ), and by thesatisfaction condition, M 0 |= ρ. Since M 0 is an arbitrary expansion of M, we havethus proved M |= (∀χ)ρ.
2. Substitutivity is sound, i.e. (∀χ)ρ |=Σ (∀ϕ)θ(ρ) for all sentences (∀χ)ρ ∈ Sen(Σ)
and substitutions θ : χ → ϕ. Let M be a Σ-model such that M |= (∀χ)ρ. Assume asubstitution θ : χ → ϕ, and let M2 be any ϕ-expansion of M. We have M2θ |= ρ andby the satisfaction condition, M2 |= θ(ρ). Since M2 is an arbitrary expansion of M,
we have thus proved M |= (∀ϕ)θ(ρ).
Secondly, since E2 , C-Abstraction and Substitutivity are sound then the least entailment
system closed to C-Abstraction and Substitutivity is sound too.
tu
CHCL with the RUES defined above is not complete. If we restrict the signaturesin such a way that all operations of constrained sorts are constructors then we can prove
completeness. Concretely, we will prove that the RUES of RHCL is complete.
Assumption 3.2 In addition to Assumption 3.1, we also consider a full subcategory 6
of signature morphisms Sigr ⊆ Sig.
Let Sigr2 ⊆ Sig2 be the full subcategory such that |Sigr2 | = |Sigr |. Note that the definition of Sigr2 is correct because Sigr ⊆ Sig and |Sig| = |Sig2 |. We define
1. Senr : Sigr → Set and Mod r : Sigr → Cat op as the restrictions of Sen : Sig → Set
and Mod : Sig → Cat op , respectively, to Sigr .
2. Senr2 : Sigr2 → Set and Mod2r : Sigr2 → Cat op as the restrictions of Sen2 : Sig2 → Set
and Mod : Sig2 → Cat op , respectively, to Sigr2 .
de f

de f

3. |=r = (|=Σ )Σ∈|Sigr | and |=r2 = ((|=2 )Σ )Σ∈|Sigr | .
6 C 0 is a full subcategory of C if for all objects A, B ∈ |C 0 | we have C (A, B) = C 0 (A, B).

Fact 3.2 I r = (Sigr , Senr , Mod r , |=r ) and I2r = (Sigr2 , Senr2 , Mod2r , |=r2 ) are institutions.
In concrete examples,
1. I is CHCL, I r is RHCL,
2. I2 is CHCL2 and I2r is RHCL2 , the restriction of RHCL to(a) signature morphisms that do not add constructors on “old” sorts, and(b) sentences quantified over variables of loose sorts.
Theorem 15 (R-completeness). Assume that every signature morphism in D c is finitary, and each model of I is (D , D l )-reachable. Then the RUES E r = (Sigr , Senr , `r ) ofI r = (Sigr , Senr , Mod r , |=r ) is complete if the entailment system E2r = (Sigr2 , Senr2 , `r2 )of I2r = (Sigr2 , Senr2 , Mod2r , |=r2 ) is complete and compact.
Proof. Let Σ ∈ |Sigr | be a signature of I r , Γ ⊆ Senr (Σ) a set of sentences and (∀χ)e0 ∈χSenr (Σ) any sentence, where Σ → Σ0 ∈ D c , such that Γ |=r (∀χ)e0 . Suppose towards aϕcontradiction that Γ 0r (∀χ)e0 . Then there exists a signature morphism Σ → Σ00 ∈ D l
and a substitution θ : χ → ϕ in I such that Γ 0r (∀ϕ)θ(e0 ).
We define the set of Σ-sentences Γ2 = {ρ ∈ Senr2 (Σ) | Γ `r ρ}. We show that Γ2 0r2(∀ϕ)θ(e0 ). Assume that Γ2 `r2 (∀ϕ)θ(e0 ). Since the entailment system of I2r is compact,
there exists Γ f ⊆ Γ2 finite such that Γ f `r2 (∀ϕ)θ(e0 ). It follows that Γ f `r (∀ϕ)θ(e0 )and, since Γ `r ρ for all ρ ∈ Γ f , by Unions we obtain Γ `r Γ f . Therefore, Γ `r (∀ϕ)θ(e0 )which is a contradiction with our assumption.
We have Γ2 0r2 (∀ϕ)θ(e0 ), and because E2r is complete, there exists a Σ-model Msuch that M |=r2 Γ2 and M 6|=r2 (∀ϕ)θ(e0 ). It follows that M |=r Γ2 and M 6|=r (∀ϕ)θ(e0 ).
Note that M 6|=r (∀ϕ)θ(e0 ) implies M 6|=r (∀χ)e0 . If we prove that M |=r Γ then we reacha contradiction with Γ |=r (∀χ)e0 and therefore we can conclude Γ `r (∀χ)e0 .
χ1
Let (∀χ1 )e1 ∈ Γ, where Σ → Σ1 ∈ D c , and N be any χ1 -expansion of M. Since M is
ϕ1
(D , D l )-reachable, by Proposition 12, there exists a signature morphism Σ → Σ01 ∈ D l ,a substitution ψ : χ1 → ϕ1 in I , and a ϕ1 -expansion N 0 of M such that N 0θ = N. By Substitutivity, we have (∀ϕ1 )ψ(e1 ) ∈ Γ2 , and since M |=r Γ2 , we obtain M |=r (∀ϕ1 )ψ(e1 ).
Since N 0 is a ϕ1 -expansion of M, N 0 |=r ψ(e1 ) and by satisfaction condition, N |=r e1 .
tu
One may wonder what is the role played by I in the abstract setting. The answer issimple: I provides the subcategory D c of signature morphisms and the satisfaction relation for the sentences quantified over the signature morphisms in D c . If I is CHCL andI r is RHCL then it is easy to notice that a signature extension with constants of constrained sorts is not a signature morphism in RHCL. Therefore, in concrete examples,
we have D c 6⊆ Sigr .

3.2

Generic universal entailment systems

We define the proof rules for the sentences quantified over loose variables.
Assumption 3.3 Throughout this subsection, we assume a D l -universal institution I =(Sig, Sen, Mod, |=) over I1 = (Sig1 , Sen1 , Mod1 , |=1 ).
HCL is a D l -universal institution over its restriction HCL1 to quantifier-free sentences,where D l consists of signature extensions with a finite number of constants. Also,
RHCL2 is a D l -universal institution over its restriction RHCL1 to quantifier-free sentences, where D l consists of signature extensions with a finite number of constants ofloose sorts.
We define the proof rules for the GUES of I .
Γ `Σ (∀ϕ)e0
ϕ(Γ) `Σ0 e0(Generalization)andϕ(Γ) `Σ0 e0Γ `Σ (∀ϕ)e0
ϕ

where Γ ⊆ Sen(Σ), (∀ϕ)e0 ∈ Sen(Σ) and Σ → Σ0 ∈ D l .
Given a compact entailment system E1 = (Sig1 , Sen1 , `1 ) for I1 , the GUES of I consistsof the least entailment system over E1 closed under Substitutivity and Generalization.
Proposition 16 (G-soundness). The GUES of I is sound whenever the entailment system of I1 is sound.
Proof. Note that Generalization is sound, i.e. for every set Γ of Σ-sentences and eachΣ-sentence (∀ϕ)e0 we have Γ |= (∀ϕ)e0 iff ϕ(Γ) |= e0 . Since Substitutivity and E1 arealso sound, the least entailment system over E1 closed under Substitutivity and Generalization is sound too.
tu
Theorem 17 (G-completeness). Assume that
1. the entailment system of I1 is complete and compact, and
2. for every set of sentences E ⊆ Sen1 (Σ) and each sentence e ∈ Sen1 (Σ),
E |=1 e iff for all D l -reachable models M, we have M |=1 E implies M |=1 e
Then the GUES E = (Sig, Sen, `) of I is complete and compact.
ϕ

Proof. Let Σ ∈ |Sig|, Γ ⊆ Sen(Σ) and (∀ϕ)e0 ∈ Sen(Σ), where Σ → Σ0 ∈ D l and e0 ∈Sen1 (Σ0 ), such that Γ |=Σ (∀ϕ)e0 . We show that Γ `Σ (∀ϕ)e0 . Suppose towards a contradiction that Γ 6`Σ (∀ϕ)e0 .
ϕ
We define the set of Σ0 -sentences Γ1 = {ρ0 ∈ Sen1 (Σ0 )|ϕ(Γ) ` ρ0 }. Suppose thatϕϕ
Γ1 `1 e0 . Since the entailment system of I1 is compact, there exists a finite Γ f ⊆ Γ1 suchthat Γ f `1 e0 , which implies Γ f ` e0 . We have ϕ(Γ) ` ρ f for all ρ f ∈ Γ f , which implies
ϕ(Γ) ` Γ f . By Transitivity property, ϕ(Γ) ` e0 , and by Generalization, Γ ` (∀ϕ)e0 , whichϕcontradicts our assumption. Hence, Γ1 6`1 e0 .

By completeness of I1 , Γ1 6|=1 e0 . There exists a D l -reachable model M such thatϕϕ
M |=1 Γ1 but M 6|=1 e0 . It follows that M |= Γ1 and M 6|= e0 . This implies Mϕ 6|= (∀ϕ)e0 .
If we prove Mϕ |= Γ then we reach a contradiction with Γ |= (∀ϕ)e0 . We will focus onproving Mϕ |= Γ.
ϕϕ1Consider (∀ϕ1 )e1 ∈ Γ, where Σ → Σ1 ∈ D l , and let N be any ϕ1 -expansion of Mϕ .
We prove that N |= e1 . Since M is D l -reachable there exists a substitution θ : ϕ1 → ϕsuch that Mθ = N. By Substitutivity, Γ ` (∀ϕ)θ(e1 ), and by Generalization, ϕ(Γ) `ϕϕ
θ(e1 ), which implies θ(e1 ) ∈ Γ1 . Since M |= Γ1 , we have M |= θ(ρ) and by the satisfaction condition Mθ = N |= e1 .
For the compactness of the GUES of I , we consider the compact entailment subsystem E c = (Sig, Sen, `c ) of E = (Sig, Sen, `). It contains E1 because E1 is compact.
It is straightforward to check that E c satisfies Substitutivity. If we prove that E c satisfies Generalization then because E is the least entailment system over E1 satisfying therules of Substitutivity and Generalization we obtain E c = E .
If Γ `c (∀ϕ)e0 then there exists a finite subset Γ f ⊆ Γ such that Γ f ` (∀ϕ)e0 . By
Generalization, ϕ(Γ f ) ` e0 which means ϕ(Γ) `c e0 . Now if ϕ(Γ) `c e0 then there is a
finite subset Γ f ⊆ Γ such that ϕ(Γ f ) ` e0 . By Generalization, Γ f ` (∀ϕ)e0 which impliesΓ `c (∀ϕ)e0 .
t
u
3.3

Entailment systems with implications

All the results in this subsection can be found in [Codescu and Găină, 2008].
Assumption 3.4 Throughout this subsection, we assume an institution I = (Sig, Sen,
Mod, |=), and a sub-functor Sen0 : Sig → Set of Sen such that
– ( H ⇒ C) ∈ Sen(Σ) for all finite sets H ⊆ Sen0 (Σ) and any C ∈ Sen0 (Σ),
V– any sentence of I is of the formV

H ⇒ C as above.

An example of institution I = (Sig, Sen, Mod, |=) is the restriction of HCL to quantifierfree sentences, where I0 = (Sig, Sen0 , Mod, |=) is the restriction of HCL to atoms. Another example is the restriction of RHCL1 to quantifier-free sentences, where I0 is its
restriction to atoms.
We define the following
V proof rules for the IES of I :Γ `Σ ( H ⇒ C)
Γ ∪ H `Σ C
V
(Implications)and,Γ ∪ HV`Σ C
Γ `Σ ( H ⇒ C)
where Γ ⊆ Sen(Σ) and H ⇒ C ∈ Sen(Σ).
Given a compact entailment system E0 = (Sig, Sen0 , `0 ) for I0 , the IES of I consists of
the least entailment system over E0 closed to Implications.
Proposition 18 (I-soundness). The IES of I is sound when the entailment system of I
is sound.

Theorem 19 (I-completeness). Let D ⊆ Sig be a broad subcategory of signature morphisms such that the entailment system of I0 is complete and compact, every set ofsentences of I0 is basic, and for all sets B ⊆ Sen0 (Σ) there exists a D -reachable model
MB defining B as basic set of sentences. Then
1. the IES of I is complete and compact,
2. for every set Γ ⊆ Sen(Σ) and each sentence ρ ∈ Sen(Σ) we have
Γ |=Σ ρ iff for all D -reachable Σ-models M, we have M |=Σ Γ implies M |= ρ
3.4

Atomic entailment systems

In order to develop concrete universal entailment systems we need to define the entailment systems for the “atomic” layers of institutions.
Proposition 20 [Petria, 2007]. Let FOL0 be the restriction of FOL to the atomic sentences. The entailment system of FOL0 generated by the rules below is sound, complete
and compact.
(Reflexivity) 0/ ` t = t, where t is a term.
(Symmetry) t = t 0 ` t 0 = t , where t,t 0 are terms.
Transitivity {t = t 0 ,t 0 = t 00 } ` t = t 00 , where t,t 0 ,t 00 are terms.
(Congruence) {ti = ti0 |1 ≤ i ≤ n} ` σ(t1 , ...,tn ) = σ(t10 , ...,tn0 ), where ti ,ti0 are terms andσ is an operation symbol.
(P-Congruence) {ti = ti0 |1 ≤ i ≤ n} ∪ {π(t1 , ...,tn )} ` π(t10 , ...,tn0 ), where ti ,ti0 are terms
and π is a predicate symbol.

Proposition 21 [Codescu and Găină, 2008]. Let OSA0 be the restriction of OSA to
the atomic sentences. The entailment system of OSA0 generated by the rules below issound, complete and compact.
(Reflexivity) 0/ ` t = t, where t is a term.
(Symmetry) t = t 0 ` t 0 = t , where t,t 0 are terms.
Transitivity {t = t 0 ,t 0 = t 00 } ` t = t 00 , where t,t 0 ,t 00 are terms.
(Congruence) {ti = ti0 |1 ≤ i ≤ n} ` σ(t1 , ...,tn ) = σ(t10 , ...,tn0 ), where ti ,ti0 are terms andσ is an operation symbol.

Proposition 22 [Codescu and Găină, 2008]. Let POA0 be the restriction of POA to
the atomic sentences. The entailment system of POA0 generated by the rules below issound, complete and compact.
(Reflexivity) 0/ ` t = t for each term t(Symmetry) t = t 0 ` t 0 = t for any terms t,t 0
Transitivity {t = t 0 ,t 0 = t 00 } ` t = t 00 for any terms t,t 0 ,t 00

(Congruence) {ti = ti0 |1 ≤ i ≤ n} ` σ(t1 , ...,tn ) = σ(t10 , ...,tn0 ), where ti ,ti0 are terms andσ is an operation symbol.
(Reflexivity’) 0/ ` t ≤ t for each term t(Transitivity’) {t ≤ t 0 ,t 0 ≤ t 00 } ` t ≤ t 00 for any terms t,t 0 ,t 00(Congruence’) {ti ≤ ti0 |1 ≤ i ≤ n} ` σ(t1 , ...,tn ) ≤ σ(t10 , ...,tn0 ), where ti ,ti0 are terms andσ is an operation symbol.
(ET) {t1 = t2 , t2 ≤ t3 , t3 = t4 } ` t1 ≤ t4 for any terms t1 ,t2 ,t3 ,t4
Proposition 23 [Petria, 2007]. Let PA0 be the restriction of PA to the atomic sentences. The entailment system of PA0 generated by the rules below is sound, complete
and compact.
ee(Symmetry) t = t 0 ` t 0 = t for any terms t,t 0
e 0 0 e 00
eTransitivity {t = t , t = t } ` t = t 00 for any terms t,t 0 ,t 00
e 0(Congruence) {ti = ti , de f (σ(t1 , . . . ,tn )), de f (σ(t10 , . . . ,tn0 ))} `e
σ(t1 , . . . ,tn ) = σ(t10 , . . . ,tn0 ), where ti ,ti0 are terms and σ is an operation symbol.
(Subterm) de f (σ(t1 , . . . ,tn )) ` {de f (ti ) | i ∈ 1, n}, where ti are terms and σ is an operation symbol.
The proof rules defined above are sound and complete for the “atomic” layers of“reachable” institutions, and sound but not complete for the “atomic” layers of theconstructor-based variants. For example, the proof rules of Proposition 20 are
1. sound and complete for RHCL0 , the restriction of RHCL to(a) signature morphisms that do not add constructors on “old” sorts and(b) atomic sentences, and2. sound but not complete for CHCL0 , the restriction of CHCL to(a) signature morphisms that do not add constructors on “old” sorts and(b) atomic sentences.
The following is a corollary of Theorems 17, 19 and Proposition 20.
Corollary 24. [Completeness of HCL] The GUES of HCL generated by the rules of
Substitutivity, Generalization, Implications, Reflexivity, Symmetry, Transitivity, Congruence and P-Congruence is complete and compact.
Similar corollaries as above can be formulated for HOSA, HPOA, and HPA. The following is a corollary of Theorems 15, 17, 19 and Proposition 20.
Corollary 25. [Completeness of RHCL] The RUES of RHCL generated by the rulesof C-Abstraction, Substitutivity, Generalization, Implications, Reflexivity, Symmetry,
Transitivity, Congruence and P-Congruence is complete.
Similar corollaries as above can be formulated for RHOSA, RHPOA, and RHPA.

4

Sufficient CompletenessIf we instantiate C-Abstraction to CHCL then we obtain the following proof rule:{Γ ` (∀Y )θ(ρ) | θ : X → T(S,F) (Y ), Y -finite set of loose vars}(C-Abstraction)Γ ` (∀X)ρ
where Γ is a set of (S, F, F c , P)-sentences, and (∀X)ρ is a (S, F, F c , P)-sentence suchthat X is a finite set variables of constrained sorts. Below is a refined version of theabove rule:{Γ ` (∀Y )θ(ρ) | θ : X → T(S,F c ) (Y ), Y -finite set of loose vars}(C-Abstraction’)Γ ` (∀X)ρ
where Γ is a set of (S, F, F c , P)-sentences, and (∀X)ρ is a (S, F, F c , P)-sentence suchthat X is a finite set variables of constrained sorts.
Let (SigCHCL , SenCHCL , `CHCL ) be the entailment system of CHCL generated with
C-Abstraction, and (SigCHCL , SenCHCL , `0 ) be the entailment system of CHCL generated with C-Abstraction’. When there is no danger of confusion we may drop thesuperscript CHCL from notations.
Proposition 26. We have `CHCL ⊆`0 ⊆|=CHCL .
Proof. We prove that `CHCL ⊆`0 and `0 ⊆|=CHCL .
`⊆`0 . It suffices to show that (SigCHCL , SenCHCL , `0 ) satisfies C-Abstraction. Consider a CHCL signature (S, F, F c , P), and let Γ be a set of (S, F, F c , P)-sentences and(∀X)ρ a (S, F, F c , P)-sentence such that the sorts of the variables in X are constrained.
Assume Γ `0(S,F,F c ,P) (∀Y )θ(ρ) for all θ : X → T(S,F) (Y ) such that Y consists only ofloose variables. In particular, Γ `0(S,F,F c ,P) (∀Y )θ(ρ) for all θ : X → T(S,F c ) (Y ) such that
Y consists only of loose variables. By C-Abstraction’, we obtain Γ `0(S,F,F c ,P) (∀X)ρ.
`0 ⊆|=. By soundness of C-Abstraction’.
tu
The entailment system generated with C-Abstraction’ is more expressive. Hereafter, we replace the definition of C-Abstraction by the definition of C-Abstraction’.
Let (SigRHCL , SenRHCL , `RHCL ) be the entailment system of RHCL. Recall that forFw→s : s ∈ Sccc
S
any CHCL signature (S, F, F , P), Fw→s =.
0/ : s 6∈ Sc
CHCL
Proposition 27. For any CHCL signature (S, F, F c , P) we have `RHCL(S,Sc ,F,P) ⊆`(S,F,F c ,P) .

Proof. By induction in the definition of `RHCL . All cases are trivial except Translation
and C-Abstraction.
Translation. Let (S, F, F c , P) be a CHCL signature, ϕ : (S0 , S0c , F0 , P0 ) → (S, Sc , F, P)
a RHCL signature morphism, and E1 , E2 ⊆ Sen(S0 , S0c , F0 , P0 ) two sets of sentencescc∗such that E1 `RHCL(S ,Sc ,F ,P ) E2 . We define F0 = ((F0 )w0 →s0 )(w0 ,s0 )∈S0 ×S0 : for all (w0 , s0 ) ∈
0

0

0

0

c
S0∗ × S0 , (F0c )w0 →s0 = ϕ−1 (Fϕ(w). Since ϕ : (S0 , S0c , F0 , P0 ) → (S, Sc , F, P) is a
0 )→ϕ(s0 )RHCL signature morphism, ϕ : (S0 , F0 , F0c , P0 ) → (S, F, F c , P) is a CHCL signature

CHCL
morphism. By the induction hypothesis, E1 `RHCL(S ,Sc ,F ,P ) E2 implies E1 `(S ,F ,F c ,P ) E2 ,
0

0

0

0

0

0

0

0

and by Translation we obtain ϕ(E1 ) `CHCL(S,F,F c ,P) ϕ(E2 ).
C-Abstraction. Let (S, F, F c , P) be a CHCL signature, Γ ⊆ Sen(S, F, F c , P) a setof sentences, and (∀X)ρ ∈ Sen(S, F, F c , P) a sentence such that X consists only of
constrained variables. Assume that Γ `RHCL(S,Sc ,F,P) (∀Y )θ(ρ) for all substitutions θ : X →T(S,F Sc ) (Y ) such that Y consists of loose variables. By induction hypothesis, Γ `CHCL(S,F,F c ,P)(∀Y )θ(ρ) for all substitutions θ : X → T(S,F Sc ) (Y ) such that Y consists of loose variables.
c
In particular, Γ `CHCL(S,F,F c ,P) (∀Y )θ(ρ) for all substitutions θ : X → T(S,F ) (Y ) such that Y
consists of loose variables. By C-Abstraction, Γ `CHCL(S,F,F c ,P) (∀X)ρ.

tu

Definition 28. A CHCL presentation ((S, F, F c , P), E) is sufficient complete, where(S, F, F c , P) is a CHCL signature and E is a set of (S, F, F c , P)-sentences, if for allcmodels M ∈ Mod(S, F, F S , P) that satisfies E we have M ∈ Mod(S, F, F c , P).
Theorem 29. The entailment system of CHCL generated by C-Abstraction, Substitutivity, Generalization, Implications, Reflexivity, Symmetry,Transitivity, Congruenceand P-Congruence is complete with respect to the sufficient complete presentations, i.e.
for all sufficient complete presentations ((S, F, F c , P), Γ) and (S, F, F c , P)-sentences ρ,
CHCL
Γ |=CHCL(S,F,F c ,P) ρ implies Γ `(S,F,F c ,P) ρ.
Proof. Let ((S, F, F c , P), Γ) be a sufficient complete presentation and ρ a (S, F, F c , P)csentence . If Γ |=CHCL(S,F,F c ,P) ρ then since ((S, F, F , P), Γ) is sufficient complete, we have
RHCL
CHCL
Γ |=RHCL(S,Sc ,F,P) ρ. By Corollary 25, Γ `(S,Sc ,F,P) ρ, and by Proposition 27, Γ `(S,F,F c ,P) ρ.
tu

Similar results as Theorem 29 can be formulated for CHOSA, CHPOA and CHPA.
Below there is an example of sufficient complete specification.
Example 11. Consider the following signature
sort Nat
op 0 : → Nat{constr}
Σ = op s : Nat → Nat {constr}
op + : Nat Nat → Nat
If ρ1 = (∀x)x + 0 = x and ρ2 = (∀{x, x0 })x + (s x0 ) = s(x + x0 ) then (Σ, {ρ1 , ρ2 }) issufficient complete. Intuitively, if (Σ, Γ) specifies that non-constructor operators are
inductively defined with respect to the constructors then (Σ, Γ) is sufficient complete.
In general, the proof rules for the constructor-based institutions are not complete, as
one can see in the following example.
Example 12. Consider the following signatures
sort ssort sΣ = op a : → sand Σr = op a : → s {constr}
op b : → s {constr}
op b : → s {constr}It is easy to notice that 0/ |=Σ a = b but there is no way to prove 0/ `Σ a = b because/ is not sufficient complete. Indeed, if 0/ `Σ a = b then since there are no sentences(Σ, 0)
quantified over constrained variables, we have 0/ `Σr a = b, and we get 0/ |=Σr a = b,which is not true.
4.1

An induction scheme

One big problem raised by C-Abstraction is its premises which are infinite, in general. One needs to perform infinitely many proofs for checking the premises of CAbstraction, one for each substitution θ. In order to make proofs it is mandatory to havea finitary procedure to deal with the infinite conditions of C-Abstraction. The standard
one is the so-called method of Structural Induction.
For a better understanding of the following proposition, we will give some explanations in advance. Assume that we need to prove a property (∀X)ρ for a CHCL
presentation (Σ, Γ), where Σ = (S, F, F c , P) and X consists of constrained variables.
Let CON be a sort-preserving mapping X → F c (i.e. for all x ∈ X, CON(x) has thesame sort as x). For each x ∈ X, let Zx,CON = z1x,CON . . . znx,CON be a string of arguments
for the constructor CON(x). We define the set ZCON = ∪x∈X Zx,CON 7 and the substitution
VAR#CON : X → T(S,F c ) (ZCON ) by VAR#CON (x) = CON(x)(Zx,CON ). We let VARCON range over all
sort-preserving substitutions X → T(S,F c ) (ZCON ) with the following properties:– for all x ∈ X we have VARCON (x) ∈ Zx,CON or VARCON (x) = CON(x)(Zx,CON ), and– there exists x ∈ X such that VARCON (x) ∈ Zx,CON .
The function CON will give all the induction cases, while the function VARCON is used todefine the induction hypothesis for each case.
Proposition 30 (Structural Induction). The entailment system of CHCL is closed to
Structural Induction:– (Induction Step) Γ ∪ {VARCON (ρ) | VARCON : X → T(S,F c ) (ZCON )} `Σ(ZCON ) VAR#CON (ρ)
for all CON : X → F c , implies– (Induction Conclusion) Γ `Σ (∀X)ρ.
Proof. If we prove that Γ `Σ θ(ρ) for all substitutions θ : X → T(S,F c ) (Y ) such that Y
consists of loose variables then by C-Abstraction we obtain Γ `Σ (∀X)ρ.
We proceed by induction on the sum of depth of the terms in {θ(x) | x ∈ X} which
exists as a consequence of X being finite. Let CON : X → F c be the sort-preserving
mapping such that for all x ∈ X, CON(x) is the topmost constructor of θ(x). Let Tx =7 By a slightly abuse of notation, we let Z

its corresponding set {z1x,CON , . . . , znx,CON }.

1nx,CON to represent both the string zx,CON . . . zx,CON andtx1 . . .txn be the string of the immediate sub-terms of θ(x), and Y =[Yx , where Yx arex∈X

all variables of the terms in Tx . We define the substitution SUB : ZCON → T(S,F c ) (Y ) by
SUB(zix,CON ) = txi .
CON(x)

z1x,CON

CON(x)

znx,CON

...
SUB

6 tx1

...

6 txn

SUB

Note that SUB(Γ ∪ {VARCON (ρ) | VARCON : X → T(S,F c ) (ZCON )}) = Γ ∪ {(VARCON ; SUB)(ρ) |VARCON : X → T(S,F c ) (ZCON )} and SUB(VAR#CON (ρ)) = θ(ρ). By our assumptions,Γ ∪ {VARCON (ρ) | VARCON : X → T(S,F c ) (ZCON )} `Σ(ZCON ) VAR#CON (ρ)(1)

By Translation applied to (1),Γ ∪ {(VARCON ; SUB)(ρ) | VARCON : X → T(S,F c ) (ZCON )} `Σ(Y ) θ(ρ)(2)

The sum of depth of the terms in {(VARCON ; SUB)(x) | x ∈ X} is strictly less than thesum of depth of the terms in {θ(x) | x ∈ X}. By the induction hypothesis, we have thatΓ `Σ (∀Y )(VARCON ; SUB)(ρ) for all VARCON : X → T(S,F c ) (ZCON ). By Generalization, we
obtain Γ `Σ(Y ) (VARCON ; SUB)(ρ) for all VARCON : X → T(S,F c ) (ZCON ). By Union, we getΓ `Σ(Y ) {(VARCON ; SUB)(ρ) | VARCON : X → T(S,F c ) (ZCON )}. It follows thatΓ `Σ(Y ) Γ ∪ {(VARCON ; SUB)(ρ) | VARCON : X → T(S,F c ) (ZCON )}(3)

By Transitivity applied (3) and (2), Γ `Σ(Y ) θ(ρ). By Generalization, Γ `Σ (∀Y )θ(ρ).
tu
The above induction scheme was inspired from [Diaconescu, 2011].
4.2

An example of inductive proof

Consider the signature Σ defined in Example 11. We prove by structural induction that{ρ1 , ρ2 } `Σ (∀n)0 + n = n. The function CON range over all mappings {n} → {0, s }.
We have only two possibilities for the mapping CON : {n} → {0, s }:1. CON(n) = 0. By Proposition 30, we need Γ `Σ 0 + 0 = 0.
(a) {ρ1 , ρ2 } `Σ ρ1 by Monotonicity of the entailment relation.
(b) ρ1 `Σ 0 + 0 = 0 by Substitutivity for x substituted by 0.
(c) {ρ1 , ρ2 } `Σ 0 + 0 = 0 from (1a) and (1b) by Transitivity of `Σ .

2. CON(n) = s . By Proposition 30, we need {ρ1 , ρ2 , 0 + z = z} `Σ(z) 0 + s z = z.
(a) {ρ1 , ρ2 , 0 + z = z} `Σ(z) {ρ1 , ρ2 } by Monotonicity of the entailment relation.
(b) {ρ1 , ρ2 } `Σ(z) 0 + s z = s(0 + z) by Substitutivity for x and x0 substituted by 0
and z, respectively.
(c) {ρ1 , ρ2 , 0 + z = z} `Σ(z) 0 + s z = s(0 + z) from (2a) and (2b) by Transitivity ofthe entailment relation.
(d) {ρ1 , ρ2 , 0 + z = z} `Σ(z) 0 + z = z by Monotonicity of the entailment relation.
(e) 0 + z = z `Σ(z) s(0 + z) = s z by Congruence.
(f) {ρ1 , ρ2 , 0 + z = z} `Σ(z) 0 + s z = s z from (2c) and (2e) by Transitivity of theentailment relation.
By soundness, {ρ1 , ρ2 } |=Σ (∀n)0 + n = n. Notice that
– N, the standard model of the natural numbers with the carrier set for the sort Nat
consisting of elements {0, 1, 2, . . .} and interpreting the function symbol 0 as theelement 0, s as the successor function and + as addition, and– Zn , the model of integers modulo n with the carrier set for the sort Nat consisting
of {b
0, b
1, . . . , n[− 1} and interpreting the function symbol 0 as the element b
0, s asthe successor function and + as addition,satisfy {ρ1 , ρ2 }. Hence, we have proved formally that N and Zn satisfy (∀n)0 + n = n.
Similarly, one can prove that N and Zn satisfy (∀{m, n})s m + n = s(m + n), and thecommutativity of the addition, i.e. (∀{m, n})m + n = n + m.
4.3

Case Analysis

One of the advantages of this approach is that we can reason about “inductive” properties of a given specification even if it is not sufficient complete. As we have seen in
Example 12, the proof rules for CHCL are not complete, in general. Consider a set Γ ofΣ-sentences, where Σ = (S, F c , F, P), a non-constructor operation symbol σ ∈ Fs1 ...sn →ssuch that s is a constrained sort, and a string of arguments for σ, T = t1 . . .tn , such thatthe terms ti are formed with constructors and variables of loose sorts from Y . We define
the following proof rule:{Γ ∪ {σ(T ) = t} `Σ(Z) ρ | t ∈ T(S,F c ) (Z), Z ⊇ Y finite set of loose vars.}(Case Analysis)Γ `Σ ρ
The rule above says that if σ(T ) cannot be “reduced” to a term formed with constructors and variables of loose sorts by the equations in Γ then we need to make acase analysis on the possible value of σ(T ). The set of terms t above may be infinite
and therefore the premises of Case Analysis may be infinite too. In many examples, thecase analysis is conducted on the possible value of a term of sort Bool (the sort of σ(T )above can be Bool) that has two constructors: true and f alse. In this case, the premisesof Case Analysis are finite.
Proposition 31. The entailment system of CHCL generated by the rules of Case Analysis, C-Abstraction, Substitutivity, Generalization, Implications, Reflexivity, Symmetry, Transitivity, Congruence and P-Congruence is sound.
Proof. Firstly we prove that Case Analysis is sound. Let Γ be a set of Σ-sentences, ρ a
Σ-sentence, where Σ = (S, F, F c , P), σ ∈ Fs1 ...sn →s a non-constructor operation symbol
such that s is constrained, and T = t1 . . .tn a string of terms formed with constructors andloose variables. We prove that Γ |=Σ ρ whenever Γ ∪ {σ(T ) = t} |=Σ(Y ) ρ for all terms t
formed with constructors and loose variables, where Y is a finite set of loose variables
such that ti ∈ T(S,F c ) (Y ) and t ∈ T(S,F c ) (Y ). Assume a Σ-model M such that M |=Σ Γ. Let
Y 0 be all variables in T , f : Y 0 → M be a valuation of Y 0 into M and m = f (σ(T )), wherecf : T(S,F Sc ) (Y 0 ) → M is the unique extension of f to a (S, F S )-morphism. Since M ∈Mod(S, F, F c , P) there exists a finite set of loose variables Y 00 , a valuation g : Y 00 → M
and a term t ∈ T(S,F c ) (Y 00 ) such that g# (t) = m, where g# : T(S,F c ) (Y 00 ) → M is the uniqueextension of g to a (S, F c )-morphism. Let Y = Y 0 ∪Y 00 and h : Y → M such that h|Y 0 = f
and h|Y 00 = g. Note that (M, h) |=Σ(Y ) Γ ∪ {σ(T ) = t}, and since Γ ∪ {σ(T ) = t} |=Σ(Y ) ρ,
we obtain (M, h) |=Σ(Y ) ρ. By the satisfaction condition, M |=Σ ρ.
Since all the proof rules enumerated in the hypothesis are sound, the least entailment
system closed to these rules is sound too.
tuConsider the signature Σ defined in Example 12. The sort s has one constructor, andsince a = b `Σ a = b, by Case Analysis, we obtain 0/ `Σ a = b.
Case Analysis is often used in applications (see for example [Futatsugi et al., 2005]
and [Futatsugi, 2006]) and it splits the initial goal Γ `Σ ρ into subgoals Γ ∪ {σ(T ) =t} `Σ(Z) ρ, where the presentations (Σ, Γ ∪ {σ(T ) = t}) are expected to be sufficientcomplete. So, we can state that we provided all rules for proving the constructor-based
properties. In some cases we need to iterate the process of splitting the goals with Case
Analysis several times. Therefore, it is difficult to formulate a completeness result that
does not depend on sufficient completeness.

5

Conclusions

Consider a CHCL signature (S, F, F c ) with no predicate symbols such that all opera/ The
tors are constructors (i.e. F = F c ) and the set of loose sorts is empty (i.e. Sl = 0).
ccarrier sets of every (S, F, F )-algebra consist of interpretations of terms formed withconstructors. Let Γ be a set of conditional (S, F)-equations. Since F = F c , it follows that((S, F, F c ), Γ) is sufficient complete, and Γ has an initial model OΓ . Since all algebras
consist of interpretations of terms, every morphism OΓ → M is surjective. Further, sincesurjective morphisms preserve satisfaction of equations, for every (S, F, F c )-morphismOΓ → M and each (S, F)-equation (∀X)t = t 0 we have OΓ |= (∀X)t = t 0 implies M |=(∀X)t = t 0 . Therefore, Γ |= (∀X)t = t 0 iff OΓ |= (∀X)t = t 0 for all (∀X)t = t 0 ∈ Sen(S, F).
Because the entailment system of CHCL is complete, the proof rules generate a complete entailment relation to reason about the properties of the initial model OΓ . We
have defined Structural induction to deal with the infinitary premises of C-Abstraction.
However, the infinitary rules cannot be replaced with the finitary ones in order to obtaina complete and compact entailment system; we would obtain complete and compact
entailment relations to reason about the properties of the initial models of the specifications. Gödel incompleteness theorem shows that this is not possible even for the initialmodel of the specification of natural numbers.
The area of applications provided by the general framework of the present work ismuch wider. For example, we may consider variations of the institutions presented here,
such as order-sorted algebra with transitions. The abstract results of this research can beapplied also to constructor-based Horn variants of higher-order logic with intensional
Henkin semantics, and membership algebra [Meseguer, 1997]. Higher order logic with
Henkin semantics has been introduced and studied in [Church, 1940, Henkin, 1950]
and intensionality is discussed in [Moggi, 1985] and [Astesiano and Cerioli, 1995]. The
generic universal entailment system developed in this paper can be seen as a refinedversion of the one in [Codescu and Găină, 2008]. However, HPA cannot be capturedby the abstract framework of [Codescu and Găină, 2008] due to the quantification overpartial constant symbols (the signature extensions with a finite number of partial constant symbols are not representable). On the other hand, the Horn part of the partial
algebra with both partial and total operation symbols is an instance of the framework of[Codescu and Găină, 2008] but it cannot be captured by the present framework.
Due to the abstract definition of reachable model, one can easily define a constructorbased institution on top of some base institution by enhancing the syntax with a subsignature of constructors and restricting the semantics to reachable models. This construction may be useful when lifting the interpolation and amalgamation properties fromthe base institution. The institution-independent rule of C-Abstraction allows somehow
a uniform treatment of induction schemes in different institutions. Future work includes
the development of the OTS/CafeOBJ method based on the theoretical framework defined in this paper.

References[Adámek and Rosický, 1994] Adámek, J. and Rosický, J. (1994). Locally Presentable and Accessible Categories. Number 189 in London Mathematical Society Lecture Notes. Cambridge
University Press.
[Astesiano et al., 2002] Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses,
P. D., Sannella, D., and Tarlecki, A. (2002). CASL: the Common Algebraic Specification
Language. Theor. Comput. Sci., 286(2):153–196.
[Astesiano and Cerioli, 1995] Astesiano, E. and Cerioli, M. (1995). Free objects and equational
deduction for partial conditional specifications. Theor. Comput. Sci., 152(1):91–138.

[Bidoit and Hennicker, 2006] Bidoit, M. and Hennicker, R. (2006). Constructor-based observational logic. J. Log. Algebr. Program., 67(1-2):3–51.
[Bidoit et al., 2003] Bidoit, M., Hennicker, R., and Kurz, A. (2003). Observational logic,
constructor-based logic, and their duality. Theor. Comput. Sci., 3(298):471–510.
[Burmeister, 1986] Burmeister, P. (1986). A Model Theoretic Oriented Appraoch to Partial Algebras. Akademie-Verlag Berlin.
[Church, 1940] Church, A. (1940). A formulation of the simple theory of types. J. Symb. Log.,
5(2):56–68.
[Clavel et al., 2007] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martı́-Oliet, N., Meseguer, J.,
and Talcott, C. L., editors (2007). All About Maude - A High-Performance Logical Framework,
How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes
in Computer Science. Springer.
[Codescu and Găină, 2008] Codescu, M. and Găină, D. (2008). Birkhoff Completeness in Institutions. Logica Universalis, 2(2):277–309.
[Diaconescu, 2003] Diaconescu, R. (2003). Institution-independent Ultraproducts. Fundamenta Informaticae, 55(3-4):321–348.
[Diaconescu, 2004] Diaconescu, R. (2004). Herbrand theorems in arbitrary institutions. Inf.
Process. Lett., 90(1):29–37.
[Diaconescu, 2006] Diaconescu, R. (2006). Proof systems for institutional logic. Journal of
Logic and Computation, 16(3):339–357.
[Diaconescu, 2008] Diaconescu, R. (2008). Institution-independent Model Theory. Birkhäuser
Basel, 1st edition.
[Diaconescu, 2011] Diaconescu, R. (2011). Structural induction in institutions. Inf. Comput.,
209(9):1197–1222.
[Diaconescu and Futatsugi, 1998] Diaconescu, R. and Futatsugi, K. (1998). CafeOBJ Report:
The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, volume 6 of AMAST Series in Computing. World Scientific.
[Diaconescu and Futatsugi, 2002] Diaconescu, R. and Futatsugi, K. (2002). Logical foundationsof CafeOBJ. Theor. Comput. Sci., 285(2):289–318.
[Futatsugi, 2006] Futatsugi, K. (2006). Verifying specifications with proof scores in CafeObj.
In ASE, pages 3–10. IEEE Computer Society.
[Futatsugi et al., 2005] Futatsugi, K., Goguen, J. A., and Ogata, K. (2005). Verifying design
with proof scores. In Meyer, B. and Woodcock, J., editors, VSTTE, volume 4171 of Lecture
Notes in Computer Science, pages 277–290. Springer.
[Goguen and Burstall, 1992] Goguen, J. A. and Burstall, R. (1992). Institutions: Abstract Model
Theory for Specification and Programming. Journal of the Association for Computing Machinery, 39(1):95–146.
[Goguen and Diaconescu, 1994] Goguen, J. A. and Diaconescu, R. (1994). An Oxford surveyof Order Sorted Algebra. Mathematical Structures in Computer Science, 4(3):363–392.
[Goguen and Meseguer, 1992] Goguen, J. A. and Meseguer, J. (1992). Order-sorted algebra I:
Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theoretical Computer Science, 105(2):217–273.
[Găină et al., 2009] Găină, D., Futatsugi, K., and Ogata, K. (2009). Constructor-based institutions. In Kurz, A., Lenisa, M., and Tarlecki, A., editors, CALCO, volume 5728 of Lecture Notes
in Computer Science, pages 398–412. Springer.
[Găină and Petria, 2010] Găină, D. D. and Petria, M. (2010). Completeness by Forcing. J. Log.
Comput., 20(6):1165–1186.
[Henkin, 1950] Henkin, L. (1950). Completeness in the Theory of Types. J. Symb. Log.,
15(2):81–91.
[Mac Lane, 1998] Mac Lane, S. (1998). Categories for the Working Mathematician. Springer,
second edition.
[Meseguer, 1989] Meseguer, J. (1989). General logics. In Logic Colloquium 87, pages 275–329.
North Holland.
[Meseguer, 1992] Meseguer, J. (1992). Conditional Rewriting Logic as a Unified Model of Concurrency. Theoretical Computer Science, pages 73–155.

[Meseguer, 1997] Meseguer, J. (1997). Membership algebra as a logical framework for equational specification. In WADT, pages 18–61.
[Moggi, 1985] Moggi, E. (1985). Categories of partial morphisms and the lambdap - calculus.
In Pitt, D. H., Abramsky, S., Poigné, A., and Rydeheard, D. E., editors, CTCS, pages 242–251.
[Mossakowski, 2002] Mossakowski, T. (2002). Relating CASL with other specification languages: the institution level. Theor. Comput. Sci., 286(2):367–475.
[Mosses, 2004] Mosses, P. D. (2004). CASL Reference Manual, The Complete Documentationof the Common Algebraic Specification Language, volume 2960 of Lecture Notes in Computer
Science. Springer.
[Ogata and Futatsugi, 2003] Ogata, K. and Futatsugi, K. (2003). Flaw and modification of theiKP electronic payment protocols. Inf. Process. Lett., 86(2):57–62.
[Ogata and Futatsugi, 2008] Ogata, K. and Futatsugi, K. (2008). Simulation-based Verification for Invariant Properties in the OTS/CafeOBJ Method. Electr. Notes Theor. Comput. Sci.,
201:127–154.
[Petria, 2007] Petria, M. (2007). An institutional Version of Gödel’s Completeness Theorem. In
Mossakowski, T., Montanari, U., and Haveraaen, M., editors, CALCO, volume 4624 of Lecture
Notes in Computer Science, pages 409–424. Springer.
[Reichel, 1984] Reichel, H. (1984). Structural Induction on Partial Algebras. Akademie-Verlag
Berlin.
[Tarlecki, 1986] Tarlecki, A. (1986). Bits and pieces of the theory of institutions. In Pitt, D.,
Abramsky, S., Poigné, A., and Rydeheard, D., editors, Proceedings, Summer Workshop on Category Theory and Computer Programming, Lecture Notes in Computer Science, volume 240,
pages 334–360. Springer.