Foundations of logic programming in hybrid logics withuser-defined sharing
Daniel Găină
Institute of Mathematics for Industry, Kyushu University

Abstract
The present contribution advances an abstract notion of hybrid logic by supplementing the definition of institution with an additional structure to extract
frames. The foundation of logic programming is set in the general framework
proposed by defining the basic concepts such as Horn clause, query and solution, and proving fundamental results such as the existence of initial model ofHorn clauses and Herbrand’s theorem. The abstract results are then applied tohybrid logics with user-defined sharing, where the possible worlds share a common domain and the variables used for quantification are interpreted uniformly
across the worlds.
Keywords: institution, logic programming, Herbrand’s theorem, initiality

1. Introduction
Hybrid logics [6] are a type of standard modal logics that have symbols
for naming individual states/worlds in models. Hybrid (propositinal) logic wasintroduced by Arthur Prior [40] in the fifties, and further developed in contributions such as [39, 2, 8]. Recently, hybrid logics have been studied in the abstract
framework provided by the institutional model theory [35, 17, 21, 27, 33, 38].
Nowadays, hybrid logics have been found useful to provide logical support fordeveloping reconfigurable systems, i.e. software systems with reconfigurable
features governing the evolution of their configurations in response to external stimuli or internal performance measures. See [43] for an overview of thereconfiguration paradigm and [34] for a specification method based on hybrid
logics. From a mathematical perspective, hybrid logics allow a more uniform
proof-theoretical approach than the ordinary modal logics [8].
The concept of institution [22] formalizes the intuitive notion of logical system in a category-based setting including syntax, semantics and the satisfaction
between them. This paper defines the notion of hybrid institution which supplements the definition of institution with an additional structure to extract frames

Email address: daniel@imi.kyushu-u.ac.jp (Daniel Găină)Preprint submitted to Theoretical Computer Science

April 17, 2017

from models. Hybrid institutions are stratified institutions [1, 16] with nominal and frame extraction. While the notion of stratified institution formalizes
modal logics, the definition of hybrid institution describes hybrid logics. The
hybridization method [35, 17, 21] is a construction technique of hybrid logicalsystems over an arbitrary institution. Its parameters are very general yielding
to an abstract framework that can be instantiated to many hybrid logics. However, the hybridization process consists of a ‘bottom-up’ technique, whereas thepresent approach provides a ‘top-down’ methodology to the developing of logicaland computing science results over classical and unconventional hybrid logics,
in the spirit of universal logic [4, 5].
This paper investigates a series of model-theoretic properties of hybrid logics
such as substitution [14, 28] (which is closely related to quantification), reachable model [31, 30, 28] and basic set of sentences [12]. This fundamental workis crucial for proving not only initiality and Herbrand’s theorem but also completeness, downward Lowenheim-Skolem property, interpolation, etc.
Initial semantics [26] is closely related to good computational propertiesof logical systems. For example, in logic programing, the initial models arecalled the least Herbrand models [32], and the initiality supports the executionof programs by resolution. In algebraic specification, initiality supports theexecution of specification languages by rewriting, thus increasing significantly
the automation of the formal verification process. Our approach to initiality inhybrid logics is layered, and it is intimately linked to the structure of sentences,in the style of [29]. The existence of initial models of sets of atomic sentences
is assumed in the abstract setting, but it is developed in concrete examples ofhybrid logical systems; then the initiality property is shown to be closed undercertain sentence building operators in the general framework provided by thedefinition of hybrid institution.
Another contribution of the paper is an abstract variant of Herbrand’s theorem applicable to hybrid logics, which reduces the satisfiability of a query bya theory at a given state to the search of a suitable substitution. The logic
programming paradigm [32], in its classical form, can be described as follows:
Given a program (Σ, Γ) (that consists of a signature Σ and a set of Horn clausesΓ) and a query (∃Y )ρ (that consists of an existentially quantified conjunctionof atoms) find a solution θ, i.e. values for the variables Y such that the corresponding instance θ(ρ) of ρ is satisfied by (Σ, Γ). The essence of this paradigm
is however independent of any logical system of choice. The basic logic programming concepts, query, solutions, and the the fundamental results, such as Herbrand’s theorem, are developed over an arbitrary institution (satisfying certain
hypotheses) in [14] by employing institution-independent concepts of variables,
substitution, quantifiers and atomic formulae. Our work sets the foundation oflogic programming over a large variety of hybrid logics by developing the resultsin the framework of hybrid institutions.
One major class of applications consists of hybrid logics with user-defined
sharing, where the possible worlds share a common domain and the variables
used for quantification are interpreted uniformly across worlds. In the literature,
this semantic approach is called rigid quantification [8]. We propose a new type2

of hybrid logics by upgrading the definition of some hybrid logics with userdefined sharing that can be found in the area of computer science. These new
hybrid logics increase the syntactic expressivity of their classical counterparts
and allow a more structured model-theoretic approach to proving the desired
properties.
Some preliminary results were reported in [27]. That study is performedin the framework provided by the hybridization method and it is applicableto hybrid logical systems where the quantified variables may be interpreted
differently across the worlds, which amounts to the world-line semantics of [42].
1.1. Contributions and structure of the paper
The paper is organized as follows:• Section 2 is devoted to the brief presentation of general institution theoretic notions that are needed by the present work.
• Section 3 proposes a notion of hybrid logic by upgrading the definition of
institution. This section lays the foundation in which the abstract results
are proved.
• Section 4 introduces hybrid logics with user-defined sharing and annotation, and it shows that the newly defined hybrid logics are more expressive
than their standard counterparts. The notion of substitution is generalized
to hybrid logics to cover the concept of solution for queries.
• Section 5 recalls the necessary fundamental concepts of institutional model
theory such as basic set of sentences and reachable model. One important
contribution, not only for the present study, but also for future research,is the investigation of the concepts of basic set of sentences and reachable
model in concrete hybrid logics.
• Section 6 is dedicated to the development of the general layered initiality
result on top of the foundational work completed in the previous section.
• Section 7 presents a version of Herbrand’s theorem in the context of hybrid
institutions, and its applications to concrete hybrid logics.
• Section 8 concludes the paper and discusses the future work.
2. Institutions
In this section we describe the abstract framework which is the basis fordeveloping the general results.

3

2.1. Definition
The concept of institution formalises the intuitive notion of logical system,and has been defined by Goguen and Burstall in the seminal paper [22].
Definition 1. An institution I = (SigI , SenI , ModI , |=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 ModI : SigI → CATop , providing for each signature Σ a category whose objects are called (Σ-)models and whose arrows are called(Σ-)homomorphisms,(4) a relation |=IΣ ⊆ |ModI (Σ)| × SenI (Σ) for each signature Σ ∈ |SigI |, called(Σ-)satisfaction, such that for each morphism ϕ : Σ → Σ0 in SigI , thefollowing satisfaction condition holds:
M 0 |=IΣ0 SenI (ϕ)(e) iff ModI (ϕ)(M 0 ) |=IΣ e
for all M 0 ∈ |ModI (Σ0 )| and e ∈ SenI (Σ).
We let I range over institutions of the form (SigI , SenI , ModI , |=I ). When
there is no danger of confusion, we omit the superscript from the notations of
the institution components; for example SigI may be simply denoted by Sig.
We denote the reduct functor Mod(ϕ) by  ϕ and the sentence translation Sen(ϕ)
by ϕ( ). When M = M 0  ϕ we say that M is the ϕ-reduct of M 0 and M 0 isa ϕ-expansion of M . A signature morphism ϕ : Σ → Σ0 is conservative if all
Σ-models have a ϕ-expansion. Given a signature Σ and two sets of Σ-sentences
E1 and E2 , we write (a) E1 |= E2 whenever E2 is a semantic consequence of E2 ,i.e. M |= E1 implies M |= E2 for all Σ-models M , and (b) E1 |=| E2 wheneverE1 and E2 are semantically equivalent, i.e. E1 |= E2 and E2 |= E1 .
The following institutional notions dealing with the semantics of Boolean
operators and quantifiers were defined in [45].
Definition 2 (Internal logic). Given an institution I then(1) M |= ρ1 ∧ ρ2 iff M |= ρ1 and M |= ρ2 ;(2) M |= ¬ρ iff M 6|= ρ;(3) M |= (∀χ)γ iff M 0 |= γ for all χ-expansions M 0 of M .
χwhere Σ → Σ0 ∈ SigI , M ∈ |ModI (Σ)|, ρ ∈ SenI (Σ), ρi ∈ SenI (Σ) and γ ∈SenI (Σ0 ).
Based on these constructors for sentences we can also define ∨ , false, (∃χ)
using the classical definitions. For example, f alse = ∨∅.

4

2.2. Examples
We give a few examples of institutions which are often in met in algebraic
specification literature.
Example 3 (Propositional Logic (PL)). The category of signatures SigPL isSet. For any set P , the set of sentences SenPL (P ) is generated by the grammar
S ::= P | S ∧ S | ¬S. The category of models ModPL (P ) is (2P , ⊆). For any
mapping ϕ : P → P 0 , the function SenPL (ϕ) replaces each element p ∈ P that0
occur in a sentence of SenPL (P ) by ϕ(p). For each model M 0 ∈ 2P , we have
ModPL (ϕ)(M 0 ) = ϕ; M 0 . The satisfaction relation is defined by induction on the
structure of the sentences:• M |= e0 iff e0 ∈ M ,• M |= e1 ∧ e2 iff M |= e1 and M |= e2 ,• M |= ¬e3 iff M 6|= e3 .
where M ∈ 2P , e0 ∈ P , and ei ∈ SenPL (P ) for all i ∈ {1, 2, 3}.
Example 4 (First-Order Logic (FOL) [22] ). The signatures are triplets of theform (S, F, P ), where S is the set of sorts, F = {Fa→s }(a,s)∈S ∗ ×S is the (S ∗ × S-indexed) set of operation symbols, and P = {Pa }a∈S ∗ is the (S ∗ -indexed) setof relation symbols. 1 If a = ε then an element of Fa→s is called a constantsymbol, or a constant. A signature morphism between (S, F, P ) and (S 0 , F 0 , P 0 )is a triplet ϕ = (ϕst , ϕop , ϕrl ), where ϕst : S → S 0 , ϕop = {ϕopa→s : Fa→s →0∗
Fϕ0 st (a)→ϕst (s) | a ∈ S ∗ , s ∈ S}, ϕrl = {ϕrla : Pa → Pϕst (a) | a ∈ S }. Whenst
op
there is no danger of confusion, we may let ϕ denote each of ϕ , ϕa→s , ϕrla.
Given a signature Σ = (S, F, P ), a Σ-model is a triplet
M = ({Ms }s∈S , {Mσ }(a,s)∈S ∗ ×S,σ∈Fa→s , {Mπ }a∈S ∗ ,π∈Pa )interpreting each sort s as a set Ms , each operation symbol σ ∈ Fa→s as a function Mσ : Ma → Ms (where Ma stands for Ms1 × . . . × Msn if a = s1 . . . sn ),and each relation symbol π ∈ Pa as a relation Mπ ⊆ Ma . The model morphisms are the usual Σ-homomorphisms, i.e., S-sorted functions that preserve
the structure. The initial Σ-model of terms is denoted by TΣ .
The Σ-sentences are obtained from (a) equations t =s t0 , where t ∈ (TΣ )s ,0t ∈ (TΣ )s , s ∈ S, and (b) relations π(t), where π ∈ Pa , t ∈ (TΣ )a and a ∈ S ∗ ,by applying for a finite number of times Boolean operators and quantification
over finite sets of variables. When there is no danger of confusion we may omit
the subscript s from t =s t0 .
Satisfaction is the usual first-order satisfaction and it is defined using thenatural interpretations of ground terms t as elements Mt in models M . The
definitions of functors SenFOL and ModFOL on signature morphisms are the
1 If S is a set then S ∗ is the set of strings over symbols in S, including the empty string ε.

5natural ones: for any arrow ϕ : Σ → Σ0 ∈ SigFOL , the function SenFOL (ϕ) :SenFOL (Σ) → SenFOL (Σ0 ) translates sentences symbol-wise, and ModFOL (ϕ) :ModFOL (Σ0 ) → ModFOL (Σ) is the forgetful functor.
Notice that PL is a fragment of FOL determined by the signatures withempty sets of sort symbols.
Example 5 (REL). The institution REL is the sub-institution of single-sorted
first-order logic with signatures having only constants and relational symbols.
Example 6 (First-Order Logic with Rigid symbols (FOLR)). This institution
is used in Example 24 to define a hybrid logic and it is not intended for any otherapplication. The signatures (S r , F r , P r ) ⊆ (S, F, P ) consist of FOL signatures(S, F, P ) enhanced with a sub-signature (S r , F r , P r ) of ‘rigid’ symbols. Signature morphisms ϕ : (S r , F r , P r ) ⊆ (S, F, P ) → (S 0r , F 0r , P 0r ) ⊆ (S 0 , F 0 , P 0 )are FOL signature morphisms (S, F, P ) → (S 0 , F 0 , P 0 ) that map rigid symbols to rigid symbols. The set SenFOLR ((S r , F r , P r ) ⊆ (S, F, P )) consists of
those sentences in SenFOL (S, F, P ) that contain only quantifiers over variablesof rigid sorts. The category of models ModFOLR ((S r , F r , P r ) ⊆ (S, F, P )) is
ModFOL (S, F, P ). The satisfaction relation in FOLR is induced from the satisFOL
faction relation in FOL, i.e. |=FOLR(S r ,F r ,P r )⊆(S,F,P ) =|=(S,F,P ) .
Example 7 (Preorder Algebra (POA) [19, 20]). The POA signatures are justordinary algebraic signatures, i.e. FOL signatures without relation symbols.
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 means that each sort gets interpreted as a preorder, and each operation as apreorder functor, which means a preorder-preserving (i.e. monotonic) function.
The preorder relation is denoted by ≤. A preordered algebra morphism is justa family of preorder functors (preorder-preserving functions) which is also an
algebra morphism.
The sentences have two kinds of atoms: equations and transitions. A transition t ⇒ t0 is satisfied by a preorder algebra M when the interpretations of theterms are in the preorder relation of the carrier, i.e. Mt ≤ Mt0 . Full sentences
are constructed from equations and transitions by applying Boolean operatorsand first-order quantification.
Example 8 (Partial algebra (PA) [41, 9]). 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
the sorts and operations in a compatible way, preserving ⊥s .
A partial algebra is just like an ordinary algebra but interpreting the operations of F as partial rather than total functions; ⊥s is always interpreted as
undefined. A partial algebra (S, F )-morphism h : M → N is a family of (total)hfunctions {Ms →s Ns }s∈S such that hs (Mσ (m)) = Nσ (ha (m)) for each operation
σ : a → s and each string of arguments m ∈ Ma for which Mσ (m) is defined.
e
We consider one kind of atomic sentences: existence equality t = t0 . The
e 0existence equality t = t holds when both terms are defined and equal. The definedness predicate and strong equality can be introduced as notations: def (t)
6

V
e
s
e
stands for t = t and t = t0 stands for (t = t0 ) ∨ (¬def (t) ¬def (t 0 )). We consider the atomic sentences in SenPA (S, F ) to be the atomic existentence equalities. The sentences are formed from existence equalities by applying Boolean
operators and quantification over variables (interpreted as partial constants).
The definition of PA given here is slightly different from the one in [37, 3, 36]
since it does not consider total operation symbols.
2.3. Substitutions
We recall the notion of substitution in institutions.
Definition 9. [14] For any signature morphisms χ1 : Σ → Σ1 and χ2 :
Σ → Σ2 of an institution, a Σ-substitution θ : χ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 Σ is preserved, i.e. the following
diagrams commute,Sen(Σ1 )O
Sen(χ1 )Sen(θ)

Mod(Σ1 ) o/ Sen(Σ2 )9Sen(χ2 )Mod(θ)

Mod(χ1 )Sen(Σ)

Mod(Σ2 )Mod(χ2 )% Mod(Σ)and the following satisfaction condition holds:
Mod(θ)(M2 ) |= ρ1 iff M2 |= Sen(ρ1 )for each Σ2 -model M2 and each Σ1 -sentence ρ1 .
Note that a substitution θ : χ1 → χ2 is uniquely identified by its domain χ1 ,codomain χ2 and the pair (Sen(θ), Mod(θ)). We sometimes let  θ denote thefunctor Mod(θ), and let θ denote the sentence translation Sen(θ).
Example 10 (FOL substitutions [14]). Consider two signature extensions withconstants χ1 : Σ,→Σ[C1 ] and χ2 : Σ ,→ Σ[C2 ], where Σ = (S, F, P ) ∈ |SigFOL |,Ci is a set of constant symbols different from the the constants in F and Σ[Ci ] =(S, F ∪ Ci , P ). A function θ : C1 → TΣ (C2 ) represents a substitution between
χ1 and χ2 .
On the syntactic side, θ can be canonically extended to a function Sen(θ) :Sen(Σ[C1 ]) → Sen(Σ[C2 ]) that substitutes terms in TΣ (C2 ) for constants in C1
according to θ.
On the semantics side, θ determines a functor Mod(θ) : Mod(Σ[C2 ]) →Mod(Σ[C1 ]) such that for all Σ[C2 ]-models M we have
• Mod(θ)(M )x = Mx , for each sort x ∈ S, or operation symbol x ∈ F , orrelation symbol x ∈ P , and• Mod(θ)(M )c1 = Mθ(c1 ) for each c1 ∈ C1 .

7

Example 11 (PA substitutions [30]). Consider two signature extensions withpartial constants χ1 : Σ,→Σ[C1 ] and χ2 : Σ ,→ Σ[C2 ], where Σ = (S, F ) ∈|SigPA |, Ci is a set of partial constant symbols different from the the constantsin F . A function θ : C1 → TΣ (C2 ) represents a substitution between χ1 and χ2 .
Substitution functors.
Let I be an institution. For any signature Σ ∈ |SigI |, Σ-substitutions form aχ
category SbI (Σ), where the objects are signature morphisms Σ → Σ0 ∈ SigI , andϕthe arrows are substitutions θ : χ1 → χ2 described in Definition 9. Given Σ0 →
Σ ∈ SigI there exists a reduct functor SbI (ϕ) : SbI (Σ) → SbI (Σ0 ) that maps
each Σ-substitution θ : χ1 → χ2 to the Σ0 -substitution SbI (ϕ)(θ) : ϕ; χ1 →ϕ; χ2 such that SenI (SbI (ϕ)(θ)) = SenI (θ) and ModI (SbI (ϕ)(θ)) = ModI (θ).
Fact 12. [28] SbI : SigI → CATop is a functor.
In applications not all substitutions are of interest, and it is often assumed asubstitution sub-functor StI : DI → CATop of SbI to work with, where DI ⊆ SigI
is a broad subcategory of signature morphisms. When there is no danger ofconfusion we may drop the superscript I from notations.
Example 13 (FOL substitution functor [28]). Let DFOL ⊆ SigFOL be the broad
subcategory of signature extensions with constants. The first-order substitutions
are represented by functions θ : C1 → TΣ (C2 ), where Σ ∈ |SigFOL | and Ci
are finite sets of new constants for Σ. Let StFOL : DFOL → CATop denotethe substitution functor which maps each signature Σ to the subcategory of Σsubstitutions represented by functions θ : C1 → TΣ (C2 ) as in Example 10.
Example 14 (PA substitution functor). Let DPA ⊆ SigPA be the broad subcategory of signature extensions with partial constants. The partial substitutions
are represented by functions θ : C1 → TΣ (C2 ), where Σ ∈ |SigPA | and Ci are
finite sets of new partial constants for Σ. Let StPA : DPA → CATop denotethe substitution functor which maps each signature Σ to the subcategory of Σsubstitutions represented by functions θ : C1 → TΣ (C2 ) as in Example 11.
3. Hybrid institutions
Given a base logic one can construct freely its hybridised version by applying the hybridisation process defined in [35, 17, 21]. In this paper, we give adefinition of hybrid institution which provides a higher level of generality and a
top-down approach to Kripke semantics in the spirit of universal logic.
3.1. Definition
Informally, hybrid institutions are institutions whose signatures are equippedwith nominals and modalities and whose models are Kripke structures. Hybrid
institutions are refinements of stratified institutions that were introduced in [1]to enhance the concept of institution with ‘states’ for the models.

8

Definition 15 (Hybrid institution).
A hybrid institution HI = (SigHI , FHI , SenHI , ModHI , KHI , |=HI ) is an institution(SigHI , SenHI , ModHI , |=HI ) equipped with
(1) a functor F : SigHI → SigREL , which extracts from each signature ∆ its
relational part F(∆) = (Nom∆ , Λ∆ ), where Nom∆ is a set of nominals andΛ∆ = {Λ∆n }n∈N is a family of sets of modalities,(2) a natural transformation K : ModHI ⇒ (F; ModREL ), providing for each signature ∆ a frame functor K∆ : ModHI (∆) → ModREL (Nom∆ , Λ∆ ), which extracts
from each ∆-model M its frame K∆ (M ) consisting of a set of states/worlds|K∆ (M )| together with their accessibility relations K∆ (M )λ , where λ ∈ Λ∆n
and n ∈ N,(3) a local satisfaction relation {M |=∆ }∆∈|SigHI |,M ∈|ModHI (∆)| ,where M |=∆ ⊆ |K∆ (M )| × SenHI (∆) is a binary relation such that(a) the (global) satisfaction holds iff the local satisfaction holds for allstates, i.e. given a signature ∆, for each ∆-model M and any ∆w
sentence ρ we have: M |=HI
∆ ρ iff M |=∆ ρ for all states w of M .
(b) the local satisfaction condition holds, i.e. given a signature morphism
ϕ : ∆ → ∆0 , for every ∆0 -model M 0 , each state w0 of M 0 and any00w0∆-sentence ρ we have: M 0 |=w∆0 ϕ(ρ) iff M  ϕ |=∆ ρ.
The notation is overloaded such that |=HI denote both families of relations{M |=∆ }∆∈|SigHI |,M ∈|ModHI | and { |=HI∆ }∆∈|SigHI | . Notice that the (global)
satisfaction relation is determined by the local satisfaction relation. The consistency of the local satisfaction condition is ensured by the following result.
Lemma 16. Given a signature morphism ϕ : ∆ → ∆0 of a hybrid institution,any ∆0 -model M 0 has exactly the same set of states as its reduct M  ϕ .
Proof. By the definition of ModREL , we have |K∆0 (M 0 )| = |K∆0 (M 0 )  F (ϕ) |, andsince K is a natural transformation, we obtain |K∆0 (M 0 )  F (ϕ) | = |K∆ (M 0  ϕ )|.
It follows that |K∆0 (M 0 )| = |K∆ (M 0  ϕ )|.
In general, the semantics of hybrid institutions is constructed on top of
the semantics of some base institution. This construction is presented in thefollowing definition.
Definition 17 (Kripke structures). Let ModI : SigI → CATop be a base model
functor. The Kripke model functor ModIκ : SigREL × SigI → CATop over ModI
is defined as follows:(1) for each signature (Nom, Λ, Σ) ∈ |SigREL ×SigI |, where (Nom, Λ) ∈ |SigREL |and Σ ∈ |SigI |, ModIκ (Nom, Λ, Σ) is the category that consists of

9

(a) Kripke models of the form (W, M ), where W ∈ |ModREL (Nom, Λ)| andM : |W | → |ModI (Σ)| is a mapping from the set of states |W | to theclass of Σ-models |Mod(Σ)|, and
00REL(b) homomorphisms, hmod ), REL h : (W, 0M ) → (W , M ) of the form (hh: W → W is a homomorphism in REL,
where
hmod : M ⇒ M 0 ◦ hREL is a natural transformation.
ϕ(2) for each signature morphism (Nom, Λ, Σ) → (Nom0 , Λ0 , Σ0 ) ∈ SigREL × SigI ,
ϕREL

ϕI

where ϕ = (ϕREL , ϕI ), (Nom, Λ) → (Nom0 , Λ0 ) ∈ SigREL and Σ → Σ0 ∈SigI , the reduct functor ModIκ (ϕ) : ModIκ (Nom0 , Λ0 , Σ0 ) → ModIκ (Nom, Λ, Σ) is
defined by(a) ModIκ (ϕ)(W 0 , M 0 ) = (W, M ) such that
• W = W 0  ϕREL and Mw = Mw0  ϕI for all states w ∈ |W |,where (W 0 , M 0 ) is a (Nom0 , Λ0 , Σ0 )-model.
(b) ModIκ (ϕ)(h0 ) = h such that• hREL = h0REL  ϕREL and hmod = {h0w  ϕI }w∈|W | ,where h0 is a (Nom0 , Λ0 , Σ0 )-homomorphism.
In our examples of hybrid institutions, the model functor is a sub-functor
of some Kripke functor ModIκ : SigREL × SigI → CATop , the functor FHI :SigREL × SigI → SigREL is the first projection, and for all signatures ∆, theframe functor K∆ is the forgetful functor mapping each Kripke structure (W, M )to W . Definition 17 provides a pattern for describing the semantics of hybrid
institutions but the results of this paper will be developed at a more abstractlevel provided by Definition 15, where the Kripke structures are implicitly assumed, not constructed. This approach corresponds to the universal logic ideas
such that the results are developed at the most general level and hypothesis are
introduced only by-need basis.
Assumption 18. Throughout this paper we assume that HI range over hybrid institutions satisfying the following property: for each signature ∆ and any
nominal variable j there exists a designated signature morphism χj : ∆ → ∆[j],where ∆[j] is the notation of its target signature, such that
(1) F(χj ) = χREL
, where χREL
: (Nom∆ , Λ∆ ) ,→ (Nom∆ ∪ {j}, Λ∆ ), andjj(2) for each ∆-model M and any χREL
-expansion W 0 of K∆ (M ) there exists aj0unique χj -expansion M of M such that K∆[j] (M 0 ) = W 0 .
The above assumption is easily justified by Definition 17: the signatures ofhybrid institutions are of the form ∆ = (Nom, Λ, Σ), ∆[j] = (Nom ∪ {j}, Λ, Σ)and χj : (Nom, Λ, Σ) ,→ (Nom ∪ {j}, Λ, Σ) is the inclusion. For any ∆-model(W, M ) and any χREL
-expansion W 0 of W , the model (W 0 , M ) is the uniquejχj -expansion of (W, M ) such that K∆[j] (W 0 , M ) = W 0 .
10Notation 19. Assume a hybrid institution HI and a ∆-model M , where ∆ isa signature of HI. If W is the frame of M , in symbols K∆ (M ) = W , then forevery state w of M and each nominal variable j, we denote by(1) W (j,w) the unique χREL
-expansion of W such that the denotation of j inj(j,w)

W (j,w) is w, in symbols Wj= w, and(2) M (j,w) the unique χj -expansion of M such that W (j,w) is the frame ofM (j,w) , in symbols K∆[j] (M (j,w) ) = W (j,w) .
The semantics of each sentence operator is defined at the abstract levelprovided by Definition 15.
Definition 20 (Internal logic). Given a hybrid institution HI then(1) M |=w k1 = k2 iff Wk1 = Wk2 ;(2) M |=w λ(k1 , . . . , kn ) iff (Wk1 , . . . , Wkn ) ∈ Wλ ;(3) M |=w @k ρ iff M |=Wk ρ;(4) M |=w ρ1 ∧ ρ2 iff M |=w ρ1 and M |=w ρ2 ;(5) M |=w ¬ρ iff M 6|=w ρ;(6) M |=w [λ](ρ1 , . . . , ρn−1 ) iff for all (w, w1 , . . . , wn−1 ) ∈ Wλ we have M |=wi
ρi for some i ∈ {1, . . . , n − 1};(7) M |=w (∀χ)γ iff M 0 |=w γ for all χ-expansions M 0 of M ;
(j,w)
|=w
(8) M |=w
∆ (↓ j)e iff M∆[j] e.
χ

where ∆ → ∆0 is a signature morphism of HI, M is a ∆-model, W is the frameof M , w is a state of M , k ∈ Nom∆ , ki ∈ Nom∆ , n ∈ N∗ , λ ∈ Λn , ρ is a ∆sentence, ρi is a ∆-sentence, γ is a ∆0 -sentence, j is a nominal variable, and e
is a ∆[j]-sentence.
We call k1 = k2 nominal equations, and λ(k1 , . . . , kn ) nominal relations.
The operator @ is called retrieve because it changes the point of evaluation fora model. For any modality λ, the operator [λ] is called traditionally necessity.
The operator ↓ is called store because it allows us to give a name to the current
state that can be referred later on in sentences.
Lemma 21. Every (ordinary) institution I generates a hybrid institution H(I) =(SigI , FI , SenI , ModI , KI , |=I ) where(1) FI : SigI → SigREL is defined by FI (Σ) = (∅, ∅) for all Σ ∈ |SigI |,(2) for any Σ ∈ |SigI |, the functor KIΣ : ModI (Σ) → ModREL (∅, ∅) is defined by11

(a) KIΣ (N ) = (WN , MN ) for all Σ-models N ,where |WN | = {?} and MN (?) = N .
(b) KIΣ (h : N → P ) = (hREL , hmod ) : (WN , MN ) → (WP , MP ) for all Σhomomorphisms h : N → P , where hREL (?) = ? and hmod= h.
?
(3) (WN , MN ) |=? ρ iff N |=I ρ for all Σ ∈ |SigI |, N ∈ |ModI (Σ)| and ρ ∈SenI (Σ).
Proof. It is easy to prove that FI : SigI → SigREL is a functor and KI : ModI ⇒FI ; ModREL defined by KI = {KIΣ : ModI (Σ) → ModREL (∅, ∅)}Σ∈|Sig| is a naturaltransformation. Given a signature Σ, for all Σ-models N and Σ-sentences ρ wehave N |=H(I) ρ iff N |=? ρ iff N |=I ρ. It follows that the local satisfaction
condition for H(I) is a consequence of the satisfaction condition for I.
Lemma 21 shows that ordinary institutions can be regarded as particularcases of hybrid institutions such that the set of states for each model is a singleton. For this reason, the semantics of sentence operators is strictly moregeneral for hybrid institutions than for ordinary ones.
For example, given anVinstitution I, we have (a) ¬¬ρ |=I ρ, and (b) Γ |=I H ⇒ C iff Γ ∪H |=I C, forall Σ ∈ |SigI |, ρ ∈ SenI (Σ), Γ ⊆ SenI (Σ) and H ∪ {C} ⊆ SenI (Σ). The above
properties do not hold in hybrid institutions. It follows that the abstract results
developed at the level of institutions are not applicable to hybrid institutions, ingeneral. On the other hand, Lemma 21 provides a solution to apply the resultsfor hybrid institutions to ordinary institutions. See Section 7.
3.2. Examples
We give a few examples of hybrid institutions which can be found in otherworks as well.
Example 22 (Hybrid Propositional Logic (HPL) [2]). The signatures of thisinstitution ∆ = (Nom, Λ, Prop) consist of a set of nominals Nom, a family ofsets of modalities Λ = {Λn }n∈N , and a set of propositional symbols Prop. The∆-models are Kripke structures of the form (W, M ), where W is a (Nom, Λ)model in REL and M : |W | → |ModPL (Prop)| is a mapping. The atomic∆-sentences consist of propositional symbols p ∈ Prop. ‘Full’ sentences areconstructed from atomic sentences, nominal equations and nominal relations
by applying Boolean operators, retrieve, store, necessity and quantification overnominal variables. The satisfaction relation for atomic sentences is definedby (W, M ) |=w p iff p ∈ Mw for all ∆-models (W, M ), states w ∈ |W | andpropositional symbols p ∈ Prop.
Example 23 (Hybrid first-order logic (HFOL)). This hybrid institution isa variation of first-order hybrid logic of [7] where models may have different carrier sets across the states. The functor ModHFOL is the Kripke model
functor ModFOL: SigREL × SigFOL → CATop . Given a HFOL signatureκ∆ = (Nom, Λ, Σ), the atomic sentences in SenHFOL (∆) are the atomic sentencesin SenFOL (Σ). The sentences are constructed from atomic sentences, nominal
12equations and nominal relations by applying Boolean operators, retrieve, store,
necessity and quantification over nominal variables. The satisfaction of atomic
sentences is defined by (W, M ) |=w ρ iff Mw |=FOL ρ for all signatures ∆,atomic ∆-sentences ρ, ∆-models (W, M ) and states w ∈ |W |.
Example 24 (Hybrid First-Order Logic with user-defined Sharing (HFOLS)[35, 17]). The functor ModHFOLS : SigREL × SigFOLR → CATop is a subfunctor of ModFOLR: SigREL × SigFOLR → CATop which restricts the models
κand the homomorphisms of ModFOLR
such that the rigid symbols are interpretedκ
uniformly across the states, i.e. for all ∆ ∈ |SigHFOLS |, we have (a) (W, M ) ∈|ModHFOLS (∆)| iff for all states w1 , w2 ∈ |W | and rigid symbols x in ∆ we have
(Mw1 )x = (Mw2 )x , and (b) h : (W, M ) → (W 0 , M 0 ) ∈ ModHFOLS (∆) iff for all
modstates w1 , w2 ∈ |W | and rigid sorts sr in ∆ we have (hmodw1 )sr = (hw2 )sr .
Given a signature ∆ = (Nom, Λ, Σ), the atomic sentences in SenHFOLS (∆)
are the atomic sentences in SenFOLR (Σ). The sentences are constructed fromatomic sentences, nominal equations and nominal relations by applying Boolean
operators, retrieve, store, necessity and quantification over nominal variables
and rigid variables. The satisfaction of atomic sentences is defined as follows:(W, M ) |=w ρ iff Mw |=FOLR ρ, for all signatures ∆, atomic ∆-sentences ρ,∆-models (W, M ) and states w ∈ |W |.
4. Hybrid institutions with annotated syntax
We propose a variation of hybrid institutions, where the atomic sentences
are constructed from the terms of the initial model. This approach has the advantage of (a) increasing the expressivity of the logical syntax, and (b) allowing
a more structured model theory, which leads to the proof of the desired results.
Given a hybrid institution, we let ∆ and ∆0 range over signatures of the form
(Nom, Λ, Σ) and (Nom0 , Λ0 , Σ0 ), respectively. If the hybrid institution is HFOLS
then we let Σ and Σ0 range over FOLR signatures of the form (S r , F r , P r ) ⊆(S, F, P ) and (S 0r , F 0r , P 0r ) ⊆ (S 0 , F 0 , P 0 ), respectively.
4.1. Initial term model
We proceed by studying the existence of initial models in HFOLS.
Definition 25 (Hybrid term). Let ∆ be a HFOLS signature. For all nominalsk ∈ N om, we define (simultaneously) the S-sorted sets Tk∆ of hybrid ∆-terms:
(1)

(2)

τ ∈ (Tk∆ )arfor all rigid symbols ς ∈ F r ,ς(τ ) ∈ (Tk∆ )sr
where ar is the arity of ς and sr is the sort of ς;t ∈ (Tk∆ )afor all non-rigid symbols σ ∈ (F − F r ),σk (t) ∈ (Tk∆ )swhere a is the arity of σ and s is the sort of σ;

13

(3)

τ ∈ (Tk∆1 )sr
for all nominals k1 ∈ Nom and rigid sorts sr ∈ S r .
τ ∈ (Tk∆ )sr

By the first statement of Definition 25, the rigid symbols do not receive
annotation as they are interpreted uniformly across the states. By the second
statement of Definition 25, the non-rigid symbols receive annotation as they are
not shared between states. By the third statement of Definition 25, we have(Tk∆1 )sr = (Tk∆2 )sr for all nominals k1 , k2 ∈ Nom and rigid sorts sr ∈ S r .
Definition 26. The interpretation of a hybrid term into Kripke structure isdefined inductively on the structure of the hybrid terms. Given a HFOLS signature ∆, for any ∆-model (W, M ), we have:(1) (W, M )ς(τ ) = (MWk )ς ((W, M )τ ),r
where ς ∈ Far→sr, τ ∈ (Tk∆ )ar , k ∈ Nom, ar ∈ (S r )∗ and sr ∈ S r ;(2) (W, M )σk (t) = (MWk )σ ((W, M )t ),rwhere σ ∈ (Fa→s − Fa→s), k ∈ Nom, t ∈ (Tk∆ )a , a ∈ S ∗ and s ∈ S;

(3) Let τ ∈ (Tk∆1 )sr be a rigid term, where k1 ∈ Nom and sr ∈ S r .
For any nominal k ∈ Nom, assuming that (W, M )τ ∈ (MWk1 )sr is definedthen the interpretation of τ ∈ (Tk∆ )sr into (W, M ) is (W, M )τ ∈ (MWk1 )sr .
The third statement of Definition 26 is consistent as (MWk1 )sr = (MWk )sr .
Definition 27. Let ∆ be a HFOLS signature and k ∈ Nom a nominal.
(1) We define the first-order Σ-model Mk∆ as follows:(a) the carrier set of Mk∆ is Tk∆ ;(b) the function (Tk∆ )ς : (Tk∆ )ar → (Tk∆ )sr is defined by (Mk∆ )ς (τ ) = ς(τ )for all rigid function symbols ς ∈ F r and hybrid terms τ ∈ (Tk∆ )ar ,where ar is the arity of ς and sr is the sort of ς;(c) the function (Tk∆ )σ : (Tk∆ )a → (Tk∆ )s is defined by (Mk∆ )σ (t) = σk (t)for all non-rigid function symbols σ ∈ (F − F r ) and hybrid termst ∈ (Tk∆ )a , where a is the arity of σ and s is the sort of σ;(d) (Mk∆ )π = ∅ for all π ∈ P .
(2) We define the ∆-model (W ∆ , M ∆ ) as follows:(a) W ∆ is (Nom, Λ)-model such that |W ∆ | = Nom and Wλ∆ = ∅ for all
λ ∈ Λ, and(b) M ∆ maps each nominal k ∈ Nom to Mk∆ .
Since the rigid function and relation symbols do not receive annotations andthe terms of rigid sorts are shared between states, the definition of term model
above is consistent.
14

Lemma 28. The term model (W ∆ , M ∆ ) defined in Definition 27 is initial.
Proof. Let (W, M ) ∈ |ModHFOLS (∆)|. One can straightforwardly prove that
there exists a homomorphism h : (W ∆ , M ∆ ) → (W, M ) defined by hmod(t) =k(W, M )t for all k ∈ Nom and t ∈ Tk∆ .
For the uniqueness part, assume another homomorphism g : (W ∆ , M ∆ ) →(W, M ) and prove gkmod = hmod
for all nominals k ∈ Nom by induction on thekstructure of the ∆-terms:(1) Let ς ∈ F r , k ∈ Nom, τ ∈ (Tk∆ )ar , where ar is the arity of ς, and assume
gkmod (τ ) = hmod(τ ).
k
We have hmod
(ς(τ )) = (Mk )ς (hmod(τ )) = (Mk )ς (gkmod (τ )) = gkmod (ς(τ )).
kk(2) Let σ ∈ (F − F r ), k ∈ Nom, t ∈ (Tk∆ )a , where a is the arity of σ, and assume(t).
gkmod (t) = hmodk
We have hmod(σk (t)) = (Mk )σ (hmod(t)) = (Mk )σ (gkmod (t)) = gkmod (σk (t)).
kkmod(3) Let sr ∈ S r , k1 ∈ Nom, τ ∈ (Tk∆1 )sr , and assume hmod
k1 (τ ) = gk1 (τ ). We
modmodshow that hk (τ ) = gk (τ ) for a given nominal k ∈ Nom. By the definition(τ ). By induction hypothesis, gkmod(τ ) = hmodof g, gkmod (τ ) = gkmod
k1 (τ ). By
1
1
mod
mod
mod
mod
the definition of h, hk1 (τ ) = hk (τ ). Hence, gk (τ ) = hk (τ ).

One can replicate Definitions 25, 26 and 27 for hybrid preorder algebras
with user-defined sharing (HPOAS) and define the hybrid terms, their interpretations into the models, and the hybrid term models. Note that in HPOAS
the preorder relation on the hybrid term models is empty. It follows that theinitiality result of Lemma 28 can be straightforwardly replicated to HPOAS.
4.2. Examples
We present two examples of hybridised logics where the atomic sentences areconstructed with terms of the initial model.
Example 29 (Hybrid First-Order Logic with user-defined Sharing and Annotation (HFOLSA) [27]). This institution has the same model functor as HFOLS,
i.e. ModHFOLSA = ModHFOLS .
The set of atomic ∆-sentences consist of(a) hybrid equations t =ks t0 , where t ∈ (Tk∆ )s , t0 ∈ (Tk∆ )s , k ∈ Nom and s ∈ S;r(b) rigid relations $(τ ), where $ ∈ Par, τ ∈ (Tk∆ )ar , ar ∈ (S r )∗ and k ∈ Nom;(c) non-rigid relations πk (t), where π ∈ (Pa − Par ), t ∈ (Tk∆ )a , a ∈ S ∗ andk ∈ Nom.

15

When there is no danger of confusion we omit the subscript s and/or the superscript k from the notation t =ks t0 . Full sentences are constructed from atomic
sentences, nominal equations and nominal relations by applying Boolean operators, retrieve, store, necessity and quantification over nominal variables andϕrigid variables. Given a signature morphism ∆ → ∆0 , the atomic sentences get
translated symbol-wise.
The satisfaction relation for atomic sentences is defined as follows:(a) (W, M ) |= t = t0 iff (W, M )t = (W, M )t0 ;(b) (W, M ) |= $(τ ) iff (W, M )τ ∈ (Mk )$ ;(c) (W, M ) |= πk (t) iff (W, M )t ∈ (Mk )π .
ϕLemma 30. We have (W 0 , M 0 )ϕ(t) = ((W 0 , M 0 )  ϕ )t , for all ∆ → ∆0 ∈SigHFOLSA , (W 0 , M 0 ) ∈ |ModHFOLSA (∆0 )|, k ∈ Nom and t ∈ Tk∆ .
The local satisfaction condition is a corollary of Lemma 30.
Corollary 31. HFOLSA is an institution.
Similarly one can replicate the construction of HFOLSA in the context ofpreorder algebra.
Example 32 (Hybrid Preorder Algebra with user-defined Sharing and Annotation (HPOASA)). The Kripke structures of HPOASA upgrade the Kripke
structures of HFOLSA with preorder relations for the carrier sets of each sort.
Given a signature ∆ = (Nom, Λ, Σ), where Σ = (S r , F r ) ⊆ (S, F ), the atomic∆-sentences consist of (a) equations t =ks t0 and (b) transitions t ⇒ks t0 , wheret ∈ (Tk∆ )s , t0 ∈ (Tk∆ )s , k ∈ Nom and s ∈ S. The sentences are constructed fromatomic sentences, nominal equations and nominal relations by applying Boolean
operators, retrieve, store, necessity and quantification over nominal variables
and rigid variables. The satisfaction relation for atomic sentences is defined by(a) (W, M ) |= (t = t0 ) iff (W, M )t = (W, M )t0 and (b) (W, M ) |= (t ⇒ t0 ) iff(W, M )t ≤ (W, M )t0 .
4.3. Standard approach vs. annotation
We investigate the connection between HFOLS and HFOLSA pointing outthat HFOLSA is superior in terms of expressivity. We denote by FOLR0 and
HFOLSA0 the restrictions of FOLR and HFOLSA, respectively, to atomic
sentences.
Remark 33. We have (W, M ) |=w1 ρ iff (W, M ) |=w2 ρ for all HFOLSA
signatures ∆, models (W, M ) ∈ |ModHFOLSA (∆)|, states w1 , w2 ∈ |W |, andatomic sentences ρ ∈ SenHFOLSA0 (∆).
The above remark says that the satisfaction of HFOLSA atoms is invariant
across the states. Consider a HFOLS signature ∆ = (Nom, Λ, Σ) and recall thatin HFOLS we let Σ range over signatures of the form (S r , F r , P r ) ⊆ (S, F, P ).
Let j be a nominal variable and define the functions:
16

∆[j]

(1) atj : T(S,F,P ) → Tj
by induction on the structure of terms:σ(atj (t))
if σ ∈ F r
atj (σ(t)) =σj (atj (t)) if σ ∈ F − F rwhere t ∈ (T(S,F,P ) )a and a is the arity of σ.
(2) α∆ : SenHFOLS0 (∆) → SenHFOLSA (∆) by extending atj to atomic sentences:(a) α∆ (t1 = t2 ) = (↓ j)(atj (t1 ) = atj (t2 )), where t1 , t2 ∈ T(S,F,P ) ;(↓ j)π(atj (t))
if π ∈ P r(b) α∆ (π(t)) =(↓ j)πj (atj (t)) if π ∈ P − P r
where t ∈ (T(S,F,P ) )a , and a is the arity of π.
We overload the notation and let α∆ denote the canonical extension of thefunction α∆ : SenHFOLS0 (∆) → SenHFOLSA (∆) to all HFOLS sentences.
Proposition 34. We have (W, M ) |=w ρ iff (W, M ) |=w α∆ (ρ) for all HFOLS
signatures ∆, models (W, M ) ∈ |ModHFOLS (∆)|, states w ∈ |W | and sentencesρ ∈ SenHFOLS (∆).
Proof. Firstly, we show that (Mw )t = (W (j,w) , M )atj (t) for all signatures ∆,models (W, M ) ∈ |ModHFOLS (∆)|, states w ∈ |W | and terms t ∈ T(S,F,P ) . Weproceed by induction on the structure of terms. Let σ(t) ∈ T(S,F,P ) such that(a) σ ∈ F r : (Mw )σ(t) = (Mw )σ ((Mw )t ) = (Mw )σ ((W (j,w) , M )atj (t) ) =(W (j,w) , M )σ(atj (t)) = (W (j,w) , M )atj (σ(t)) .
(b) σ ∈ (F − F r ): (Mw )σ(t) = (Mw )σ ((Mw )t ) = (Mw )σ ((W (j,w) , M )atj (t) ) =(W (j,w) , M )σj (atj (t)) = (W (j,w) , M )atj (σ(t)) .
Secondly, we prove the statement of the proposition for the atoms of HFOLS.
(1) For any t1 , t2 ∈ T(S,F,P ) we have (W, M ) |=w t1 = t2 iff (Mw )t1 = (Mw )t2
iff (W (j,w) , M )atj (t1 ) = (W (j,w) , M )atj (t2 ) iff (W (j,w) , M ) |=w atj (t1 ) =atj (t2 ) iff (W, M ) |=w (↓ j)atj (t1 ) = atj (t2 ) iff (W, M ) |=w α∆ (t1 = t2 ).
(2) There are two sub-cases for hybrid relations.
(a) For $ ∈ P r and τ ∈ (T(S,F,P ) )ar where ar is the arity of $:(W, M ) |=w $(τ ) iff (Mw )τ ∈ (Mw )$ iff (W (j,w) , M )atj (τ ) ∈ (Mw )$iff (W (j,w) , M ) |=w $(atj (τ )) iff (W, M ) |=w (↓ j)$(atj (τ ))iff (W, M ) |=w α∆ ($(τ )).
(b) For any π ∈ (P − P r ) and t ∈ (T(S,F,P ) )a , where a is the arity of π:(W, M ) |=w π(t) iff (Mw )t ∈ (Mw )π iff (W (j,w) , M )atj (t) ∈ (Mw )π iff(W (j,w) , M ) |=w πj (atj (t)) iff (W, M ) |=w (↓ j)πj (atj (t)) iff (W, M ) |=wα∆ (πj (t)).
17Thirdly, the proof of the statement for all HFOLS sentences is a straightforward extension of the case for atomic sentences.
By Proposition 34, for any sentence in HFOLS there exists a semanticallyequivalent formula in HFOLSA. The sentence operator store is somehow integrated in the atomic sentences of HFOLS while the construction of HFOLSA
avoids this situation, e.g. each HFOLS equation t1 = t2 is satisfied by the samemodels as the HFOLSA sentence (↓ j)atj (t1 ) = atj (t2 ) and the top sentence
operator of the latter sentence is store. It follows that HFOLSA allows a morestructured approach to model-theoretic properties.
Notice that α : SenHFOLS ⇒ SenHFOLSA defined by α = {α∆ }∆∈|SigHFOLS |is a natural transformation. Using Proposition 34 one can easily define a comorphism [25] from HFOLS to HFOLSA which means that HFOLSA is at leastas expressive as HFOLS. Annotated atomic sentences of the form σk1 = σk2 ,which say that the non-rigid constant symbol σ is interpreted uniformly in theworlds denoted by the nominals k1 and k2 , cannot be expressed in HFOLS.
Therefore, we conclude that HFOLSA is more expressive than HFOLS.
4.4. Hybrid substitutions
In this subsection we define an abstract notion of hybrid substitution, which
upgrades the notion of substitution defined in Section 2.3 to hybrid institutions.
Definition 35. Let HI be a hybrid institution. A hybrid substitution between
χ1χ2
the signature morphisms ∆ → ∆0 ∈ SigHI and ∆ → ∆00 ∈ SigHI is a substitutionθχ1 → χ2 such that the following local satisfaction condition holds: M 00 |=w
θ(ρ0 ) iff M 00  θ |=w ρ, for all M 00 ∈ |ModHI (∆00 )|, ρ ∈ SenHI (∆0 ) and w ∈|K∆00 (M 00 )|.
The following result shows that the local satisfaction condition for substitutions is consistent.
Lemma 36. M 00 and M 00  θ from Definition 35 share the same set of states.
Proof. By Lemma 16, |K∆00 (M 00  θ )| = |K∆00 (M 00  θ  χ1 )|. It follows that|K∆00 (M 00  θ )| = |K∆00 (M 00  χ2 )|. By Lemma 16, |K∆00 (M 00  χ2 )| = |K∆00 (M 00 )|.
Hence, |K∆00 (M 00  θ )| = |K∆00 (M 00 )|.
Example 37 (HFOLSA substitutions). Consider two signature extensions
with nominals and rigid constant symbols χ1 : ∆ ,→ ∆[C1 , D1 ] and χ2 : ∆ ,→∆[C2 , D2 ], where ∆ = (Nom, Λ, Σ), Σ = (S r , F r , P r ) ⊆ (S, F, P ), Ci is a set of
nominals different from the elements of Nom, and Di is a set of rigid constantsdifferent from the constants in F . A pair of functions θ = (θa : C1 → Nom ∪∆[C ,D ]C2 , θb : D1 → Tk 2 2 ), where k ∈ Nom, represents a substitution between χ1and χ2 :18

(1) On the syntactic side, θ determines a sentence translation
SenHFOLSA (θ) : SenHFOLSA (∆[C1 , D1 ]) → SenHFOLSA (∆[C2 , D2 ]), which
preserves ∆ and substitutes(i) nominals in Nom ∪ C2 for nominals in C1 according to θa , and(ii) ∆[C2 , D2 ]-terms for constants in D1 according to θb .
(2) On the semantics side, θ determines a model functor
ModHFOLSA (θ) : ModHFOLSA (∆[C2 , D2 ]) → ModHFOLSA (∆[C1 , D1 ]) suchthat for all (W 00 , M 00 ) ∈ |ModHFOLSA (∆[C2 , D2 ])| the model (W 00 , M 00 )  θ
interprets(i) every symbol in ∆ as (W 00 , M 00 ),(ii) each nominal c1 ∈ C1 as (W 00 , M 00 )θa (c1 ) , and(iii) any rigid symbol d1 ∈ D1 as (W 00 , M 00 )θb (d1 ) .
Lemma 38. We have ((W 00 , M 00 )  θ )t = (W 00 , M 00 )θ(t) for all ∆[C2 , D2 ]-models∆[C1 ,D1 ](W 00 , M 00 ) and terms t ∈ Tk.
∆[C1 ,D1 ]Proof. Straightforward, by induction on the structure of the terms in Tk.

The local satisfaction condition for substitutions is a direct consequence ofLemma 38.
Corollary 39. We have (W 00 , M 00 )  θ |=w ρ iff (W 00 , M 00 ) |=w θ(ρ) for all∆[C2 , D2 ]-models (W 00 , M 00 ), states w ∈ |W 00 |, and ∆[C1 , D1 ]-sentences ρ.
Hybrid substitution functors.
Given a hybrid institution HI, for any signature ∆ ∈ |SigHI |, the hybrid∆-substitutions form a subcategory HSbHI (∆) of SbHI (∆).
Fact 40. HSbHI : SigHI → CATop is a sub-functor of SbHI .
In applications we work with a substitution sub-functor HStHI : DHI → CATopof HSbHI , where DHI ⊆ SigHI is a broad subcategory of signature morphisms.
When there is no danger of confusion we may drop the superscript HI fromnotations.
Example 41 (HPL substitution functor). Let DHPL be the broad subcategoryof signature extensions with nominals. Let HStHPL : DHPL → CATop denotethe sub-functor of HSbHPL : SigHPL → CATop which maps each signature∆ = (Nom, Λ, Prop) to the subcategory of hybrid ∆-substitutions represented byfunctions θ : C1 → Nom ∪ C2 , where Ci is a set of nominals different fromthe elements of Nom. Notice that the substitutions given by HStHPL determine
signature morphisms. It follows that the local satisfaction condition is satisfied.

19

Example 42 (HFOLSA substitution functor). Given a HFOLSA signature∆ = (Nom, Λ, (S r , F r , P r ) ⊆ (S, F, P )), only substitutions represented by pairs of∆[C ,D ]functions (θa : C1 → N om∪C2 , θb : D1 → Tk 2 2 ) as described in Example 37
are relevant for the present study. Assume that DHFOLSA ⊆ SigHFOLSA is thebroad subcategory of signature extensions with nominals and rigid constants.
Let HStHFOLSA : DHFOLSA → CATop denote the substitution functor whichmaps each signature ∆ to the subcategory of hybrid ∆-substitutions represented∆[C ,D ]by pairs of functions (θa : C1 → N om ∪ C2 , θb : D1 → Tk 2 2 ) as describedin Example 37.
Proposition 43 (Hybridised substitutions). Given an institution I, any substitution functor StI : DI → CATop for I generates a hybrid substitution functor
HStH(I) : DI → CATop for H(I):χ1χ2

Proof. For any substitution θ : (Σ → Σ1 ) → (Σ → Σ2 ) ∈ StI (Σ) the following
are equivalent M |=H(I) θ(ρ) iff M |=? θ(ρ) iff M |=I θ(ρ) iff M  θ |=I ρ iff
M  θ |=? ρ iff M  θ |=H(I) ρ, where M is a Σ2 -model and ρ is a Σ1 -sentence.
Hence, any substitution for I is also a substitution for H(I).
5. Institution-independent concepts
In this section, we investigate some of the institution-independent notions
which are necessary to prove our abstract results.
5.1. Reachable models
We give an institution-independent characterisation of the models which
consist of interpretations of syntactic elements.
Definition 44. [30] Let I be an institution and StI : DI → CATop a substitutionfunctor for I. Given a signature Σ ∈ |Sig|, a Σ-model M is StI -reachable ifχfor each signature morphism Σ → Σ0 ∈ DI and any χ-expansion M 0 of M there
exists a substitution θ : χ → 1Σ ∈ StI (Σ) such that M  θ = M 0 .
If the substitution functor StI is fixed, StI -reachable models may be called
simply reachable.
Fact 45. Given a substitution functor StI : DI → CATop for an institution I,
a model is StI -reachable iff it is HStH(I) -reachable.
In what follows, we study the notion of reachability in concrete logical systems.
Proposition 46. [30, 28] In FOL, a model is StFOL -reachable iff its elements
consist of denotations of terms.
Proposition 47. [30] In PA, a model is StPA -reachable iff its elements consistof denotations of terms.

20

In HPL, the reachability notion is connected to the states of models.
Proposition 48. In HPL, a model is HStHPL -reachable iff its states consistof denotations of nominals.
Proof. For the direct implication, assume a reachable ∆-model (W, M ), where∆ = (Nom, Λ, Prop) is a HPL signature. Let w ∈ |W | be an arbitrary state. We
prove that there exists a nominal k ∈ Nom such that Wk = w. Let χ : ∆ → ∆[j]be a signature extension with the nominal variable j. Since (W, M ) is reachable,
there exists a substitution θ : {j} → Nom such that (W, M )  θ = (W (j,w) , M ).
(j,w)
It follows that Wθ(j) = Wj
= w. We define k = θ(j).
For the converse implication, assume a ∆-model (W, M ) such that its statesconsists of interpretations of nominals, where ∆ = (Nom, Λ, Prop) is a HPL
signature. Let χ : ∆ ,→ ∆[C] be a signature extension with nominals from C,
and (W 0 , M ) a χ-expansion of (W, M ). We define the functions (a) f : Nom →|W | by f (k) = Wk for all k ∈ Nom, and (b) g : C → |W 0 | by g(c) = Wc0 for allc ∈ C. Note that f is surjective and |W | = |W 0 |. It follows that there exists
θ : C → Nom such that θ; f = g.
/ |W | = |W 0 |
:

f

Nom`

g

θ

C
Notice that (W  θ )c = Wθ(c) = f (θ(c)) = g(c) = Wc0 for all c ∈ C. Hence,(W, M )  θ = (W 0 , M ).
In HFOLSA, the elements of reachable models denote nominals and hybrid
terms.
Proposition 49. In HFOLSA, a model is HStHFOLSA -reachable iff (a) its
set of states consists of denotations of nominals and (b) its carrier sets for the
rigid sorts consist of denotations of hybrid terms.
Proof. For the direct implication, let (W, M ) be a reachable ∆-model.
(a) Let w ∈ |W |: We prove there exists k ∈ Nom such that Wk = w. Consider
a signature extension ι : ∆ ,→ ∆[j] with the nominal variable j. Since(W, M ) is reachable there exists a substitution θ : {j} → Nom such that
(W, M )  θ = (W (j,w) , M ). It follows that (W, M )θ(j) = ((W, M )  θ )j =(j,w)

(W (j,w) , M )j = Wj

= w. Hence, k = θ(j).

(b) Let k ∈ Nom, s ∈ S r and m ∈ (MWk )s : We prove that there exists t ∈ (Tk∆ )ssuch that m = (W, M )t . Consider the signature extension χ : ∆ ,→ ∆[x]with the rigid constant x and let (W, M 0 ) be the χ-expansion of (W, M ) suchthat (W, M 0 )x = m. Since (W, M ) is reachable, there exists a substitutionθ : {x} → Tk∆ such that (W, M )  θ = (W, M 0 ). It follows that (W, M )θ(x) =((W, M )  θ )x = (W, M 0 )x = m. Hence, t = θ(x).
21For the converse implication, consider a signature extension χ : ∆ ,→ ∆[C, D]
with nominals from C and rigid constants from D, a ∆-model (W, M ) such thatthe conditions (a) and (b) are satisfied, and a χ-expansion (W 0 , M 0 ) of (W, M ).
θ

We prove that there exists a substitution χ → 1∆ ∈ HStHFOLSA (∆) such that
(W, M )  θ = (W 0 , M 0 ). Let k ∈ Nom be an arbitrary fixed nominal. We define
the following functions:(1) fa : C → |W | by fa (c) = Wc0 for all c ∈ C and(2) fb : D → MWk by fb (d) = (W 0 , M 0 )d for all d ∈ D.
Let h : (W ∆ , M ∆ ) → (W, M ) be the homomorphism given by the initiality of(W ∆ , M ∆ ). Since the set of states |W | consists of interpretations of nominals,
hrel : Nom → |W | is surjective. It follows that there exists θa : C → Nom suchthat θa ; hrel = fa .
/ |W |
>

hrel

Nom`
θa

fa

C
Since the carrier sets of (W, M ) for the rigid sorts consist of interpretationsof terms, hmod
: Tk∆ → MWk is surjective on S r . It follows that there existsk∆θb : D → Tk such that θb ; hmod
= fb .
k
Tk∆

hmod
k

`
θb

/ MW
k
=
fb

D
Let θ = (θa , θb ) : χ → 1∆ , where θa and θb are defined as above. It follows that
(1) ((W, M )  θ )c = (W, M )θa (c) = hrel (θa (c)) = fa (c) = Wc0 for all c ∈ C, and(2) ((W, M )  θ )d (W, M )θb (d) = hmod
(θb (d)) = fb (d) = (W 0 , M 0 )d for all d ∈ D.
kHence, (W, M )  θ = (W 0 , M 0 ).
The expansion of models that consist of interpretations of syntactic elements
along signature morphisms used for quantification does not generate substitutions in HFOLS. The abstract theorems of the following sections are not applicable to hybrid institutions with user-defined sharing in their standard versions.
We make another mild assumption about the hybrid substitution functors,
which is satisfied in all examples of hybrid institutions given in this paper andwill allows us to prove that the set of states of reachable models consists ofinterpretations of nominals.

22

Assumption 50. Let HI be a hybrid institution. We assume that HStHI range
over substitution functors satisfying the following property: given a signature ∆and a nominal variable j, we haveχj• ∆ → ∆[j] ∈ DHI , andθ• each substitution χj → 1∆ ∈ HSt(∆) is represented by a signature morθphism ∆[j] → ∆ ∈ SigHI such that χj ; θ = 1∆ .
In concrete examples of hybrid institutions, θ from Assumption 50 range
over substitutions θ : {j} → Nom that map j to a nominal.
Proposition 51. Let HI be a hybrid institution with a hybrid substitution functor HStHI : DHI → CATop . The set of states of reachable models consists ofdenotations of nominals.
Proof. Let ∆ be a signature. Assume a reachable ∆-model M and a state
w of M . We show that there exists k ∈ Nom∆ such that Wk = w, where
W = K∆ (M ). Let j be a nominal variable. Since M is reachable, there exists aθ

substitution χj → 1∆ ∈ HSt(∆) such that M  θ = M (j,w) . By Assumption 50,
θ is represented by a signature morphism θ : ∆[j] → ∆ such that χj ; θ = 1∆ .
We have WθREL (j) = (W  θREL )j = (W (j,w) )j = w. We define k = θREL (j).
5.2. Basic sets of sentences
In concrete examples of institutions, basic sentences are the simplest sentences, which are intimately linked to the internal structure of models, inthe sense that their satisfaction is preserved by homomorphisms. Basic sentences [12] tend to be the starting building blocks from which the complex
sentences are constructed by using Boolean operators, quantification, or othersentence operators.
Definition 52. Given an institution I, a set of sentences B ⊆ SenI (Σ) is basic
if there exists a Σ-model M B such that
M |= B iff there exists a homomorphism M B → M
for all Σ-models M . We say that M B is a basic model of B. If in addition thehomomorphism M B → M is unique then the set B is called epi-basic.
Note that any set of epi-basic set of sentences has an initial model which isthe basic model. We show that the sets of atomic sentences of the institutions
presented above are epi-basic.
Lemma 53. Any set of sentences in FOLb is epi-basic and the basic model is
StFOL -reachable, where FOLb is the restriction of FOL to atomic sentences.

23

Proof. Let B be a set of atomic (S, F, P )-sentences in FOL. The basic model
M B is constructed as follows: on the quotient algebra T(S,F ) /≡B obtained bypartitioning the elements of T(S,F ) into equivalence classes given by the congruence generated by the equational atoms of B, we interpret each relation symbolπ ∈ P by MπB = {(t1 /≡B , . . . , tn /≡B ) | π(t1 , . . . , tn ) ∈ B}. Since M B consistsof interpretations of terms, by Proposition 46, M B is reachable.
The proof of Lemma 53 is well known, and it can be found, for example, in[12] or [15], but since we want to make use of the construction of the basic model,
we include it for the convenience of the reader. By defining an appropriate notionof congruence for POA models compatible with the preorder (see [18] or [10])one may obtain the same result for POA.
Lemma 54. [30] Let PAb be the restriction of PA to existence equations. Any
set of sentences in PAb is epi-basic and the basic model is StPA -reachable.
Proof. For a set of existence equations E we define S E as the set of sub-terms
appearing in E. Note that S E is a partial algebra. The basic model M E willbe the quotient of S E by the partial congruence induced by E.
Theorem 55. Any set of sentences in HPLb is epi-basic and the basic models
are HStHPL -reachable, where HPLb is the restriction of HPL to (a) nominal
equations, (b) nominal relations and (c) sentences of the form @k p such that k
is a nominal and p is a propositional symbol.
Proof. Let B ⊆ SenHPLb (∆), where ∆ = (Nom, Λ, Prop) ∈ |SigHPL |. We define
the following equivalence relation on nominals ≡B = {(k1 , k2 ) | B |=HPL k1 =k2 }. We define the basic model (W B , M B ) as follows:(1) Let W B be the REL model such that(a) |W B | = Ndom, where Nd
om is the factorisation of Nom to ≡B , and(b) WλB = {bk | B |=HPL λ(k)} for all λ ∈ Λ.
(2) Given a nominal k ∈ Nom, let MbkB be the PL model which consists of{p ∈ Prop | B |=HPL @k p}. Let M B : Ndom → |ModPL (Prop)| be theB bBmapping defined by M (k) = M for all k ∈ Nom.
bk

We prove that
(W, M ) |= B iff there exists a unique arrow (W B , M B ) → (W, M )for all ∆-models (W, M ).
“⇒” Let f REL : W ∆ → W and g REL : W ∆ → W B be the unique homomorphisms such that W ∆ is the initial model of ModREL (Nom, Λ). Since24(W, M ) |=HPL B, we have ≡B ⊆ Ker(f REL ). It follows that there exists
a unique arrow hREL : W B → W such that g REL ; hREL = f REL .
W Bb

hREL

g REL

/W
=
f REL

W

∆

Let k ∈ Nom be an arbitrary nominal. Since (W, M ) |=HPL B, for allp ∈ Prop we have B |=HPL @k p implies MWk |=PL p. It follows that
there exists a unique PL homomorphism hbmod: MbkB → MWk . Hencekh = (hREL , hmod ) : (W B , M B ) → (W, M ) is unique.
“⇐” Straightforward.
Since W B is constructed from factorisation of W ∆ , by Proposition 48, (W B , M B )is reachable.
Theorem 56. Any set of sentences in HFOLSAb is epi-basic and the basic models are StHFOLSA -reachable, where HFOLSAb is the restriction of
HFOLSA to (a) atomic sentences, (b) nominal equations and (c) nominal
relations.
Proof. Firstly we prove that any set of atomic sentences and nominal relations
is epi-basic. Let Γ ⊆ SenHFOLSAb (∆) be such a set, where ∆ = (Nom, Λ, Σ) isa HFOLSA signature and Σ = (S r , F r , P r ) ⊆ (S, F, P ) is a FOLR signature.
We define the congruences ≡k = {(t1 , t2 ) | t1 , t2 ∈ Tk∆ , Γ |=HFOLSA t1 = t2 } onthe Σ-models Mk∆ for all k ∈ Nom (see Definition 27 for the construction of Mk∆ ).
We show that ≡k is indeed a congruence. There are two cases to consider:(1) Let ς ∈ F r and τ1 , τ2 ∈ (Tk∆ )ar such that τ1 ≡k τ2 , where ar is the arityof ς. By the definition of ≡k , we have Γ |=HFOLSA τ1 = τ2 , which implies
Γ |=HFOLSA ς(τ1 ) = ς(τ2 ). By the definition of ≡k , ς(τ1 ) ≡k ς(τ2 ).
(2) Let σ ∈ (F − F r ) and t1 , t2 ∈ (Tk∆ )a such that t1 ≡k t2 , where a is thearity of σ. By the definition of ≡k , Γ |=HFOLSA t1 = t2 , which implies
Γ |=HFOLSA σk (t1 ) = σk (t2 ). By the definition of ≡k , σk (t1 ) ≡k σk (t2 ).
We denote by MkΓ the Σ-model obtained by(a) factorising Mk∆ by the congruence ≡k , and(b) interpreting each relation π ∈ P by (MkΓ )π = {t/≡ | π(t) ∈ Γ or πk (t) ∈ Γ}.
Let W Γ be the (Nom, Λ)-model such that |W Γ | = Nom and WλΓ = {k | λ(k) ∈ Γ}
for all λ ∈ Λ. Let M Γ : Nom → |Mod(Σ)| be the mapping defined by M Γ (k) = MkΓ
for all k ∈ Nom. The definition of (W Γ , M Γ ) is correct as for any rigid sortsr ∈ S r and nominals k1 , k2 ∈ Nom we have ≡ksr1 =≡ksr2 . We prove that
(W, M ) |= Γ iff there exists a unique arrow (W Γ , M Γ ) → (W, M )for all ∆-models (W, M ).
25

“⇒” Since for all λ(k) ∈ Γ we have Wk ∈ Wλ , there exists a unique (Nom, Λ)homomorphism hrel : W Γ → W defined by hrel (k) = Wk for all k ∈ Nom.
Let f : (W ∆ , M ∆ ) → (W, M ) and g : (W ∆ , M ∆ ) → (W Γ , M Γ ) be
the unique homomorphisms given by the initiality of (W ∆ , M ∆ ). Since(W, M ) |= Γ, if t1 ≡k t2 then fkmod (t1 ) = fkmod (t2 ) for all t1 , t2 ∈ Tk∆ .
We obtain Ker(fkmod ) ⊆≡Γk . It follos that there exists a unique homomorphism hmod
: MkΓ → MWk such that the following diagram is commutative.
k
MkΓ

hmod
k

a

mod
gk

/ MW
k
<
fkmod

Mk∆
Thus, we have defined a unique homomorphism h : (W Γ , M Γ ) → (W, M )such that g; h = f .
”⇐” Straightforward.
Secondly, we prove that any set of atomic sentences, nominal equations andnominal relations B ⊆ SenHFOLSAb (∆) is epi-basic. We define(a) the equivalence relation ≡= {(k1 , k2 ) | Γ |=HFOLSA k1 = k2 } on Nom, andb where ∆b = (Nd(b) the signature morphism ϕ : ∆ → ∆,om, Λ, Σ), which maps
each nominal k to its equivalence class b
k w.r.t. ≡ and it is the identity on
the rest of the symbols.
We show that
(W, M ) |= B iff there exists a unique arrow (W ϕ(B) , M ϕ(B) )  ϕ → (W, M )where (W ϕ(B) , M ϕ(B) ) is the basic model of ϕ(B) defined above.
“⇒” If (W, M ) |= B then there exists a unique ϕ-expansion (W 0 , M ) of (W, M )such that |W 0 | = |W |, W 0 interprets each b
k as Wk , and Wλ0 = Wλ forall λ ∈ Λ. By the satisfaction condition, (W 0 , M ) |= ϕ(B). Since ϕ(B)is epi-basic, there exists a unique arrow h0 : (W ϕ(B) , M ϕ(B) ) → (W 0 , M ).
By the uniqueness of the ϕ-expansion (W 0 , M ) and the homomorphism
h0 , it follows that h0  ϕ : (W ϕ(B) , M ϕ(B) )  ϕ → (W, M ) is also unique.
“⇐” Assume a homomorphism h : (W ϕ(B) , M ϕ(B) )  ϕ → (W, M ). Since
W ϕ(B) = Ndom, the model (W, M ) satisfies all nominal equations in B.
There exists a unique ϕ-expansion h0 : (W ϕ(B) , M ϕ(B) ) → (W 0 , M ) of h.
Since ϕ(B) is epi-basic, (W 0 , M ) |=HFOLSA ϕ(B), and by the satisfaction
condition, (W, M ) |=HFOLSA B.

26

Finally, notice that (W ϕ(B) , M ϕ(B) ) is constructed by factorisations of some setsof signature symbols. By Proposition 49, (Mϕ(B) , Rϕ(B) ) is reachable, and since
ϕ is surjective, the reduct of (W ϕ(B) , M ϕ(B) ) along ϕ is also reachable.
The following result shows that the semantic consequences of a basic set ofsentences can be reduced to the satisfaction by a base model.
Lemma 57. Let I be an institution. Consider a signature Σ ∈ |SigI |, a basic
set B of Σ-sentences and a basic model M B for B. Then for all basic sentencesγ ∈ Sen(Σ) we have B |=Σ γ iff M B |=Σ γ.
Proof. The direct implication is trivial. For the converse implication assume
that M B |= γ and let M ∈ |Mod(Σ)| such that M |=Σ B. We show that
M |=Σ γ. Since M B |= γ, there exists an arrow M γ → M B , where M γ is abasic model for γ. Since M |=Σ B, there exists an arrow M B → M . It follows
that there exists an arrow M γ → M . Hence, M |=Σ γ.
6. Initiality
We have proved in concrete logical settings that certain sets of sentences
are epi-basic. It follows that those sets of sentences have initial models. In
this section, we prove in the general framework of hybrid institutions that theinitiality property is closed to implication, store, quantification and necessity.
The framework in which the results of this section will be proved is given
by a hybrid institution HI (such that Assumption 18 holds) equipped with asubstitution functor HStHI : DHI → CATop (such that Assumption 50 holds).
An example of such institution is HPL, where the substitution functor HStHI is
HStHPL defined in Example 41. Another example of institution HI is HFOLSA,
where the substitution functor HStHI is HStHFOLSA defined in Example 42.
6.1. Implication
Consider two sub-functors SenHIi ⊆ SenHI and SenHIb ⊆ SenHIi such that
(1) all sentences of HIi = (SigHI , FHI , SenHIi , ModHI , KHI , |=HI ) are constructedfrom the sentences of HIb = (SigHI , FHI , SenHIb , ModHI , KHI , |=HI ) by applying
logical implication,i.e. all sentences of HIi (a) belong to HIb or (b) are ofV
the form H ⇒ C, where H ∪ {C} belongs to HIb , and(2) HIb is semantically closed to retrieve, i.e. if ρ is a sentence of HIb then forany nominal k there exists a sentence in HIb that is semantically equivalent
to @k ρ.
Theorem 58. Every set of sentences in HI has a initial reachable model if every
set of sentences in HIb is basic and the basic models are reachable.

27

Proof. Let Γ be a set of ∆-sentences in HIi , where ∆ is a signature. We defineΓb = {ρ ∈ SenHIb | Γ |=HI ρ}. Let M Γb be the basic model of Γb . Notice thatfor all ∆-models M such that M |=HI Γ there exists a unique arrow M Γb → M
since M |=HI Γb and M Γb is the initial model of Γb . If we prove that M Γb |=HI Γ
then M ΓVb is the initial model of Γ.
Let H ⇒ C ∈ Γ and w ∈ |K∆ (M Γb )|, and assume that M Γb |=w H.
By Proposition 51, there exists k ∈ Nom such that w = K∆ (M Γb )k . We haveM Γb |=HI {@k h | h ∈ H}. Since HIb is semantically closed to @, the set{@k h | h ∈ H} is basic. By Lemma 57, Γb |=HI
V {@k h | h ∈ H}, which implies
Γ |=HI {@k h | h ∈ H}. Notice that Γ |=HI h∈H @k h ⇒ @k C, and we getΓ |=HI @k C. Because HIb is semantically closed to @, there exists a sentence ρ
in HIb that is semantically equivalent to @k C. We have ρ ∈ Γb , which implies
Γb |=HI ρ. By Lemma 57, M Γb |=HI ρ, which is equivalent to M Γb |=HI @k C.
Hence, M Γb |=w C.
The following two results are corollaries of Theorem 58.
Corollary 59. Any set of sentences in HPLi has a initial reachable model,
where HPLi is the restriction of HPL to sentences constructed from HPLb
formulae by applying logical implication.
Proof. By Theorem 55, any set of sentences in HPLb is epi-basic and the basicmodels are reachable. HPLb is semantically closed to @ as for all nominals
k and sentences ρ of HPLb , we have ρ |=| @k ρ. By Theorem 58, any set ofsentences in HPLi has a initial model that is reachable.
Corollary 60. Any set of sentences in HFOLSAi has a initial reachable model,
where HFOLSAi is the restriction of HFOLSA to sentences constructed fromHFOLSAb formulae by applying logical implication.
Proof. By Theorem 56, any set of sentences in HFOLSAb is epi-basic and thebasic models are reachable. HFOLSAb is semantically closed to @ as for all
nominals k and sentences ρ of HFOLSAb , we have ρ |=| @k ρ. By Theorem 58,
any set of sentences in HFOLSAi has a initial model that is reachable.
6.2. Store
Assume two sub-functors SenHIs ⊆ SenHI and SenHI∗ ⊆ SenHI such that all
sentences of HIs = (SigHI , FHI , SenHIs , ModHI , KHI , |=HI ) are constructed from thesentences of HI∗ = (SigHI , FHI , SenHI∗ , ModHI , KHI , |=HI ) by applying store.
In order to prove that initiality is closed to store we need the following
assumption, which is easily satisfied in all examples of hybrid institutions that
we are aware of.
Assumption 61. HI range over hybrid institutions satisfying another mild
property: given a signature ∆ ∈ |SigHI | and a nominal variable j,
REL
the REL signature morphism θj←k
: (Nom∆ ∪ {j}, Λ∆ ) → (Nom∆ , Λ∆ )which preserves (Nom∆ , Λ∆ ) and maps j to k28

defines a signature morphism θj←k : ∆[j] → ∆ in HI
REL
such that F(θj←k ) = θj←kand χj ; θj←k = 1∆ .

Lemma 62. We have(1) M  θj←k = M (j,w) , where w = K∆ (M )k ,(2) @k (↓ j)ρ |=| @k θj←k (ρ), andVV(3) @k ( H ⇒ C) |=| h∈H @k h ⇒ @k C
where
∆ ∈ |SigHI |, k ∈ Nom∆ , j is a nominal variable, ρ ∈ SenHI (∆[j]), andV
H ⇒ C ∈ SenHI (∆).
Proof.
(j,w)
REL = K∆ (M )(1) We have K∆[j] (M  θj←k ) = K∆ (M )  θj←k.

Since χj ; θj←k = 1∆ , the model (M  θj←k ) is a χj -expansion of M .
Recall that M (j,w) is the unique χj -expansion of M such that K∆[j] (M (j,w) ) =K∆ (M )(j,w) . It follows that M  θj←k = M (j,w) .
(2) Assume that M |=HI @k (↓ j)ρ, where M is a ∆-model. It follows thatM |=w (↓ j)ρ, where w = K∆ (M )k . We have M (j,w) |=w ρ. By the local
satisfaction condition, M |=w θj←k (ρ). Hence, M |=HI @k θj←k (ρ).
Assume that M |=HI @k θj←k (ρ), where M is a ∆-model. It follows thatM |=w θj←k (ρ), where w = K∆ (M )k . By the local satisfaction condition,M  θj←k = M (j,w) |=w ρ. We have M |=w (↓ j)ρ. Hence, M |=HI @k (↓ j)ρ.
(3) Straightforward.

The following result provide conditions for proving that initiality is closed
to store.
Theorem 63. Any set of sentences in HIs has a initial reachable model if any
set of sentences in HI∗ has a initial reachable model and HI∗ is semanticallyclosed to retrieve.
Proof. Let Γ be a set of ∆-sentences in HIs , where ∆ is a signature. We define
the set of sentences Γ∗ = {ρ ∈ SenHI∗ (∆) | Γ |=HI ρ}. Let M Γ∗ be the initialmodel of Γ∗ . Notice that for all ∆-models M such that M |=HI Γ there exists
a unique arrow M Γ∗ → M as M |=HI Γ∗ and M Γ∗ is the initial model of Γ∗ . If
we prove that M Γ∗ |= Γ then M Γ∗ is the initial model of Γ.
Let (↓ j)γ ∈ Γ and w ∈ |K∆ (M Γ∗ )|. We show that M Γ∗ |=w (↓ j)γ. Since M ∗is reachable, by Proposition 51, there exists k ∈ Nom such that K∆ (M Γ∗ )k = w.
We have (↓ j)γ |=HI @k (↓ j)γ. By Lemma 62(2), (↓ j)γ |=HI @k θj←k (γ). SinceHI∗ is semantically closed to retrieve, there exists ρ ∈ SenHI∗ (∆) such that wehave ρ |=| @k θj←k (γ). It follows that Γ |=HI ρ, which implies ρ ∈ Γ∗ . We
have M Γ∗ |=HI ρ, which implies M Γ∗ |=HI @k θj←k (γ). By the local satisfaction
condition, M Γ∗  θj←k = (M Γ∗ )(j,w) |=w γ. Hence, M Γ∗ |=w (↓ j)γ.
29

The following results are corollaries of Theorem 63.
Corollary 64. Any set of sentences in HPLs has a initial reachable model,
where HPLs is the restriction of HPL to sentences constructed from HPLi
formulae by applying store.
Proof. By Corollary 59, any set of sentences in HPLi has a initial reachable
model. Since HPLb is semantically closed to retrieve, by Lemma 62(3), HPLi
is semantically closed to retrieve. By Theorem 63, any set of sentences in HPLs
has a initial reachable model.
Corollary 65. Any set of sentences in HFOLSAs has a initial reachable
model, where HFOLSAs is the restriction of HFOLSA to sentences constructed from HFOLSAi formulae by applying store.
Proof. By Corollary 60, any set of sentences in HFOLSAi has a initial reachable
model. Since HFOLSAb is semantically closed to retrieve, by Lemma 62(3),HFOLSAi is semantically closed to retrieve. By Theorem 63, any set of sentences in HFOLSAs has a initial reachable model.
6.3. Quantification
Consider two sub-functors SenHIq ⊆ SenHI and SenHI∗ ⊆ SenHIg and a broad
subcategory QHI ⊆ DHI of signature morphisms such that all sentences of HIq =(SigHI , FHI , SenHIq , ModHI , KHI , |=HI ) are constructed from the formulae of HI∗ =(SigHI , FHI , SenHI∗ , ModHI , KHI , |=HI ) by applying universal quantification over thesignature morphisms in QHI .
Theorem 66. All sets of sentences in HIq have a initial reachable model if all
sentences in HI∗ have a initial reachable model.
Proof. Let Γ be a set of ∆-sentences in HIq , where ∆ is a signature. We defineΓ∗ = {ρ ∈ SenHI∗ | Γ |=HI ρ}. Let M Γ∗ be the initial model of Γ∗ . Notice thatfor all ∆-models M such that M |=HI Γ there exists a unique arrow M Γ∗ → M
as M |=HI Γ∗ and M Γ∗ is the initial model of Γ∗ . In what follows we prove thatM Γ∗ |=HI Γ.
χConsider a sentence (∀)ρ ∈ Γ, where ∆ → ∆0 ∈ QHI and ρ ∈ SenHI∗ (∆0 ). Let
w be a state of M Γ∗ and M 0 be a χ-expansion of M Γ∗ . We prove that M 0 |=w ρ.
θSince M Γ∗ is reachable, there exists a hybrid substitution χ → 1∆ ∈ HStHI (∆)
such that M Γ∗  θ = M 0 . Note that (∀χ)ρ |=HI θ(ρ), which implies θ(ρ) ∈ Γ∗ . It
follows that M Γ∗ |=w θ(ρ). By the local satisfaction condition, M 0 |=w ρ.
The following results are corollaries of Theorem 66.
Corollary 67. Any set of sentences in HPLq has a initial reachable model,
where HPLq is the restriction of HPL to sentences constructed from HPLs
formulae by applying universal quantification over nominal variables.

30

Proof. By Corollary 64, any set of sentences in HPLs has a initial reachable
model. By Theorem 66, any set of sentences in HPLq has a initial reachable
model.
Corollary 68. Any set of sentences in HFOLSAq has a initial reachable
model, where HFOLSAq is the restriction of HFOLSA to sentences constructed from HFOLSAs formulae by applying universal quantification overnominal and rigid variables.
Proof. By Corollary 65, any set of sentences in HFOLSAs has a initial reachable model. By Theorem 66, any set of sentences in HFOLSAq has a initialreachable model.
6.4. Necessity
Consider two sub-functors SenHIn ⊆ SenHI and SenHI∗ ⊆ SenHIn such that all
sentences of HIn = (SigHI , FHI , SenHIn , ModHI , KHI , |=HI ) are constructed from thesentences of HI∗ by applying (a) necessity over binary modalities, and (b) retrieve.
The following result show that initiality is closed to necessity restricted tobinary modalities.
Theorem 69. Any set of sentences in HIn has a initial reachable if any setof sentences in HI∗ has a initial reachable and HI∗ is semantically closed toretrieve.
Proof. Let Γ be a set of ∆-sentences in HIn , where ∆ is a signature. We defineΓ∗ = {ρ ∈ SenHI∗ (∆) | Γ |=HI ρ}. Let M Γ∗ be a initial reachable model of Γ∗ .
Since for all models M that satisfies Γ there exists a unique arrow M Γ∗ → M ,we only need to prove that M Γ∗ |=HI Γ.
Consider a sentence [λ]γ ∈ Γ and let w, w0 ∈ |K∆ (M Γ∗ )| such that (w, w0 ) ∈0K∆ (M Γ∗ )λ . We show that M Γ∗ |=w γ. Since M Γ∗ is reachable, by Proposition 51, there exists k, k 0 ∈ Nom such that K∆ (M Γ∗ )k = w and K∆ (M Γ∗ )k0 = w0 .
Note that Γ |=HI @k0 γ:
Indeed for any ∆-model M that satisfies Γ, we have M |=HI Γ∗ .
Since M Γ∗ is initial, there exists an arrow K∆ (M Γ∗ ) → K∆ (M ) in REL.
It follows that (s, s0 ) ∈ K∆ (M )λ , where s = K∆ (M )k and s0 = K∆ (M )k0 .
0Since M |=HI [λ]γ, we have M |=s γ. Therefore, M |=HI @k0 γ.
Since HI∗ is semantically closed to retrieve, there exists ρ ∈ SenHI∗ (∆) suchthat ρ |=| @k0 γ. We have Γ |=HI ρ, where ρ ∈ SenHI∗ (∆), which implies ρ ∈ Γ∗ .
It follows that M Γ∗ |=HI ρ, which is equivalent to M Γ∗ |=HI @k0 γ. Hence,0
M Γ∗ |=w γ.
The case @k [λ]γ ∈ Γ is similar.
The following result is useful to show that the instances of HI∗ in this subsection are semantically closed to retrieve.
31

Lemma 70. We have @k (∀χ)ρ |=| (∀χ)@F(χ)(k) ρ for all sentences of the formχ(∀χ)ρ, where ∆ → ∆0 ∈ SigHI and ρ ∈ SenHI (∆0 ).
Proof. For any ∆0 -model M 0 we have K∆0 (M 0 )F (χ)(k) = (K∆0 (M 0 )  F (χ) )k =K∆ (M 0  χ )k . The following are equivalent:
M |=w @k (∀χ)ρ iff M |=K∆ (M )k (∀χ)ρ iff
M 0 |=K∆ (M )k ρ for all χ-expansions M 0 of M iff0
M 0 |=K∆0 (M )F (χ)(k) ρ for all χ-expansions M 0 of M iff
M 0 |=w @F (χ)(k) ρ for all χ-expansions M 0 of M iff M |=w (∀χ)@F (χ)(k) ρ.
Hence, @k (∀χ)ρ |=| (∀χ)@F (χ)(k) ρThe following results are corollaries of Theorem 69.
Corollary 71. Any set of sentences in HPLn has a initial reachable model,
where HPLn is the restriction of HPL to sentences constructed from HPLq
formulae by applying (a) necessity over binary modalities, and (b) retrieve.
Proof. By Corollary 67, any set of sentences in HPLq has a initial reachable model. By Lemma 62(2), HPLi is semantically closed to retrieve. By
Lemma 62(3), HPLs is semantically closed to retrieve. By Lemma 70, HPLq issemantically closed to retrieve. By Theorem 69, any set of sentences in HPLn
has a initial reachable model.
Corollary 72. Any set of sentences of HFOLSAn has a initial reachable
model, where HFOLSAn is the restriction of HFOLSA to sentences constructed from HFOLSAq formulae by applying (a) necessity over binary modalities, and (b) retrieve.
Proof. By Corollary 68, any set of sentences in HFOLSAq has a initial reachable model. By Lemma 62(2), HFOLSAi is semantically closed to retrieve.
By Lemma 62(3), HFOLSAs is semantically closed to retrieve. By Lemma 70,
HFOLSAq is semantically closed to retrieve. By Theorem 69, any set of sentences in HFOLSAn has a initial reachable model.
We have shown that in hybrid institutions such as HPL and HFOLSA thesentences constructed from some basic sentences by applying logical implication,
store, universal quantification, necessity over binary modalities and retrieve,
have an initial model. The sentence operators store, quantification, necessity,and retrieve may be applied in a different order by a finite number of times andinitiality is still preserved. Moreover, the results may be applied in different
contexts such as preorder algebras.
The initiality property can be borrowed from hybrid institutions with annotated syntax to their classical versions.
Proposition 73. Any set of sentences in HFOLSn has a initial reachable
model, where32

(a) HFOLSn is the restriction of HFOLS to sentences constructed from theformulae of HFOLSb by applying logical implication, store, quantification
over nominal and rigid variables, necessity over binary modalities and retrieve, and(b) HFOLSb is the restriction of HFOLS to nominal equations, nominal relations and sentences of the form @k ρ, where k is a nominal and ρ is anatomic sentence.
Proof. Recall that HFOLS and HFOLSA share the same signatures and models. Given a signature ∆, for each atomic sentence ρ ∈ SenHFOLS0 (∆) and any
nominal k for ∆, the sentences @k ρ and α∆ (ρ)[j ← k] are satisfied by the samemodels:By Proposition 34, ρ and α∆ (ρ) are satisfied by the same models, which
implies that @k ρ and @k α∆ (ρ) are satisfied by the same models. By
Lemma 62(2), @k α∆ (ρ) is semantically equivalent to @k α∆ (ρ)[j ← k].
Since α∆ (ρ)[j ← k] is an atomic sentence, by Remark 33, α∆ (ρ)[j ← k] issemantically equivalent to @k α∆ (ρ)[j ← k]. Hence, @k ρ and α∆ (ρ)[j ← k]
are satisfied by the same models.
For any sentence in HFOLSb there is a semantically equivalent formula in
HFOLSAb . It follows that for any sentence in HFOLSn there is a semantically equivalent formula in HFOLSAn By Corollary 72, any set of sentencesin HFOLSAn has a initial model, which implies that any set of sentences in
HFOLSn has a initial model.
7. Herbrand’s theorem
We prove a version of Herbrand’s theorem at the abstract level of hybrid
institutions.
Theorem 74. Let HI be a hybrid institutions equipped with a hybrid substitutionfunctor HStHI : DHI → CATop and a sub-functor SenHIb ⊆ SenHI . ConsiderVχ• a sentence (∃χ) E such that ∆ → ∆0 ∈ DHI and E ⊆ SenHIb (∆0 ),• a set Γ ⊆ SenHI (∆) that has a initial HStHI -reachable model M Γ , and• a nominal k of ∆.
If HIb is semantically closed to retrieve and all sets of sentences in HIb are basic
then the following are equivalent:V(1) Γ |=HI @k (∃χ) E,
V(2) M Γ |=HI @k (∃χ) E, andVθ(3) Γ |=HI @k (∀ϕ) θ(E) for some substitution χ → ϕ ∈ HStHI (∆) such that ϕ
is conservative.
33

Proof.
(1) ⇒ (2) Obvious since M Γ |=HIVΓ.
(2) ⇒ (3) Since M Γ |=HI @k (∃χ) E, there exists a χ-expansion M 0 of M Γsuch that M 0 |=w E, where w = K∆ (M Γ )k . By the reachability of M Γ , there
exists a substitutionθ : χ → 1∆ in HStHI (∆) such that M Γ  θ = M 0 . We show
V
HI
that Γ |= @k θ(E).
Let M be a ∆-model such that M |=HI Γ. By the initiality of M Γ , there
exists a unique homomorphism
h : M Γ → M . Since HIb is semantically closed
S
to retrieve, B = e∈E @k e is basic. Since M 0 |=w E, we have M 0 |=HI B. Thereexists an arrow g : M B → M 0 , where M B is the basic model of B. It follows that
there exists an arrow g; (h  θ ) : M B → M  θ , which implies M  θ |= B. Notethat for all e ∈ E, we have M  θ |=w e, and by the local satisfaction
condition,V
M |=w θ(e). We obtain M |=w θ(E), which implies M |=HI @k θ(E).
(3) ⇒ (1) Let M be a ∆-model such that M |=HI Γ. We denote K∆ (M )kby w. Thereexists a ϕ-expansion M 00 of M as ϕ is conservative. Since Γ |=HIV@k (∀ϕ) θ(E), we have M 00 |=w θ(E). By the local satisfaction condition,
M 00  θ |=w VE. Note that (M 00  θ ) is Va χ-expansion of M . It follows thatM |=w (∃χ) E. Hence, M |=HI @k (∃χ) E.
The substitution θ from the third statementVof Theorem 74 is called a solution. The existentially quantified formula (∃χ) E is a query. The implication(1) ⇒ (3) reduces the satisfiability of a query by a program (represented here by
a theory) at the state denoted by k to the search of a substitution. The converse
implication (3) ⇒ (1) shows that the solutions are sound with respect to thegiven program. Implication (1) ⇒ (3) is called completeness, while implication(3) ⇒ (1) is called soundness.
We apply Theorem 74 to HPL. In this case, the quantification is restricted
to signature extensions with a finite set of nominal variables. We call HornVclauses the sentences of HPLn . A query is any sentence of the form (∃J) E,
where J is a finite set of nominal variables and E is a finite set of HPLb
sentences.
V
Corollary 75. In HPL, for every set of Horn clauses Γ, each query (∃J) E
and any nominal k for a given signature ∆ = (Nom, Λ, Prop), the following are
equivalent:V(1) Γ |=HPL @k (∃J) E,
V(2) (W Γ , M Γ ) |=HPL @k (∃J) E, where (W Γ , M Γ ) is the initial model of Γ,V(3) Γ |=HPL @k (∀J 0 ) θ(E) for some hybrid substitution θ : J → Nom ∪ J 0 ,where J 0 is a finite set of nominal variables.
Proof. Since Nom is not empty (as k ∈ Nom), the inclusion χ0 : ∆ ,→ ∆[J 0 ] is conservative. By Corollary 71, any set of Horn clauses has a initial reachable model.
By Theorem 55, any set of sentences in HPLb is epi-basic. By Theorem 74, thethree statements of Corollary 75 are equivalent.

34

The institution HFOLSA falls into the framework of Theorem 74. We
call Horn clauses the sentences of the institution HFOLSAn . A query isVany
existentially quantified conjunction of basic sentences of the form (∃X) E,
where X is a finite set of nominal and rigid variables and E is a finite set ofsentences in HFOLSAb .
Corollary
76. In HFOLSA, for every set of Horn clauses Γ, each query
V(∃X) E and any nominal k for the signature ∆ = (Nom, Λ, Σ), the following
are equivalent:V(1) Γ |=HFOLSA @k (∃X) E,
V(2) (W Γ , M Γ ) |=HFOLSA @k (∃X) E,
where (W Γ , M Γ ) is the initial model of Γ,V(3) Γ |=HI @k (∀X 0 ) θ(E)∆[Xa0 ,Xb0 ]for some hybrid substitution θ = (θa : Xa → Nom∪Xa0 , θb : Xb → Tk),

where Xa is the set of nominal variables of X, Xb is the set of rigid variablesof X, Xa0 is a finite set of nominal variables, Xb0 is a finite set of rigid
variables such that the sorts of the variables in Xb0 are inhabited 2 andX 0 = Xa0 ∪ Xb0 .
Proof. Since k ∈ Nom and the sorts of the variables in X 0 are inhabited, theinclusion χ0 : ∆ ,→ ∆[X 0 ] is conservative. By Corollary 72, any set of Hornclauses has a initial reachable model. By Theorem 56, any set of sentences in
HFOLSAb is epi-basic. By Theorem 74, the three statements of Corollary 76
are equivalent.
Theorem 74 can be instantiated in a similar preorder algebra context. In
what follows, we apply Theorem 74 to ordinary institution such as FOL. We
call Horn clauses the sentences of FOLq , the restriction of FOL to sentences
constructed from atomic sentences by applying logical implication and universal
quantification over finite sets of first-order variables. A query V
is any existentiallyquantified conjunction of atomic sentences of the form (∃X) E, where X is a
finite set of first-order variables and E is a finite set of atomic sentences.
V
Corollary 77. In FOL, for any set of Horn clauses Γ and any query (∃X) E
for the signature Σ, the following are equivalent:V(1) Γ |=FOL (∃X) E,
V(2) M Γ |=FOL (∃X) E, where M Γ is the initial model of Γ,
2 For each rigid sort s of ∆ and any variable x ∈ X 0 of sort s there exists a hybrid ∆-termbt of sort s.

35

(3) Γ |=FOL (∀X 0 )Vθ(E) for some substitution θ : X → TΣ (X 0 ),where X 0 is a finite set of first-order variables for Σ such that the sorts ofthe variables in X 0 are inhabited.
Proof. The substitution functor StFOL (see Proposition 43) generates a hybrid
substitution functor HStH(FOL) for H(FOL). By Fact 45, a model is StFOL reachable model iff it is HStH(FOL) -reachable. It follows that H(FOL) falls into
the frameworkof Theorem 74. For any set of Horn clauses Γ and any query
V(∃X) E the following are equivalent:VΓ |=FOL (∃X) E iff
VVΓ |=H(FOL) @∗ (∃X) E iff M Γ |=H(FOL) @∗ (∃X) E iffV
M Γ |=FOL (∃X) E iff
VΓ |=H(FOL) @∗ (∀X 0 ) θ(E) for some substitution θ : X → TΣ (X 0 ) suchthat all sorts of the variables in X 0 are inhabited iff
VΓ |=FOL (∀X 0 ) θ(E) for some substitution θ : X → TΣ (X 0 ) such thatall sorts of the variables in X 0 are inhabited.

The above result can be found also in [14], where Herbrand’s theorem isproved at the level of an arbitrary institution satisfying certain conditions. The
result in [14] is based on a notion of representable signature morphisms which is
replaced here by more permissive hypotheses for concrete logical systems suchas reachable models. For example, PA is an instance of Theorem 74 but it does
not fall into the abstract framework of [14] as the signature extensions with“partial” variables (used for quantification) are not representable.
8. Conclusions
The existence of initial models of Horn clauses and Herbrand’s theorem isproved for hybrid logics. The study on initiality is performed in two steps:(1) We commence by showing that the set of atomic sentences of hybrid logics given as examples here are epi-basic and the basic models are reachable.
(2) Then we investigate the closure of the initiality property under certain sentence operators used for constructing Horn clauses in the general setting provided by hybrid institutions. Similar results on initiality have been formulated
in the context of ordinary institutions in [29]. The present work is not based on
quasi-variety concepts, and the results are not obtained within the framework offactorization systems [44, 46] or inclusion systems [13]. The hybrid logics withuser-defined sharing and annotation are not instances of the hybridization process, since the definition of the atomic sentences involves nominals; therefore,
the quasi-variety theorem in [17] does not cover these examples of hybrid logics. Finding an inclusion system for the models of the base institution to meetthe preservation conditions of the quasi-variety theorem is the most difficult
36

technical part of [17]. The aforementioned paper does not provide a good hint
for the application of the abstract quasi-variety theorem to hybrid logics withuser-defined sharing. Our approach requires less model-theoretic infrastructure
and it is applicable to theories for which the corresponding class of models may
not form a quasi-variety.
Herbrand’s theorem has been proved for various logical systems [32, 23, 24].
The first institution-independent version is due to [14]. The result has beenrefined in [11] in the context of abstract substitution systems. We propose aversion of Herbrand’s theorem for hybrid institutions where the queries areformulated for certain states of the program represented here by nominals.
Our abstract results are not applicable to hybrid institutions with userdefined sharing in their standard versions as the expansions of models thatconsist of interpretations of syntactic elements along signature morphisms used
for quantification does not generate substitutions, in general. While initiality can be borrowed from hybrid institutions with annotated syntax to theirstandard variants, the solutions of queries cannot be transported in the samemanner. This fact is related to the reacher syntactic expressivity provided byannotation, which is an important contribution of the present work.
References[1] M. Aiguier and R. Diaconescu. Stratified institutions and elementary homomorphisms. Information Processing Letters, 103(1):5–13, 2007.
[2] C. Areces and P. Blackburn. Bringing them all Together. Journal of Logic
and Computation, 11(5):657–669, 2001.
[3] E. Astesiano, M. Bidoit, H. Kirchner, B. Krieg-Brückner, P. D. Mosses,
D. Sannella, and A. Tarlecki. CASL: the Common Algebraic Specification
Language. Theoretical Computer Science, 286(2):153–196, 2002.
[4] J.-Y. Béziau. 13 questions about universal logic. Bulletin of the Section of
Logic, 35(2/3):133–150, 2006.
[5] J.-Y. Béziau. Universal Logic: An Anthology: from Paul Hertz to Dov
Gabbay. Birkhäuser, 2012.
[6] P. Blackburn. Representation, reasoning, and relational structures: a hybrid logic manifesto. Logic Journal of the IGPL, 8(3):339–365, 2000.
[7] P. Blackburn and M. Marx. Tableaux for Quantified Hybrid Logic. In
U. Egly and C. G. Fermüller, editors, Automated Reasoning with Analytic
Tableaux and Related Methods, International Conference, TABLEAUX
2002, Copenhagen, Denmark, July 30 - August 1, 2002, Proceedings, volume 2381 of Lecture Notes in Computer Science, pages 38–52. Springer,
2002.

37

[8] T. Braüner. Hybrid logic and its proof-theory, volume 37 of Applied logic
series. Springer, Dordrecht, 2011. 22503921.
[9] P. Burmeister. A Model Theoretic Oriented Appraoch to Partial Algebras.
Akademie-Verlag Berlin, 1986.
[10] M. Codescu and D. Găină. Birkhoff Completeness in Institutions. Logica
Universalis, 2(2):277–309, September 2008.
[11] I. Ţuţu and J. L. Fiadeiro. From conventional to institution-independent
logic programming. Journal of Logic and Computation, FirstView:1–38,
June 2015. DOI: 10.1093/logcom/exv021.
[12] R. Diaconescu. Institution-independent Ultraproducts. Fundamenta Informaticæ, 55(3-4):321–348, 2003.
[13] R. Diaconescu. Elementary diagrams in institutions. J. Log. Comput.,
14(5):651–674, 2004.
[14] R. Diaconescu. Herbrand theorems in arbitrary institutions. Information
Processing Letters, 90(1):29–37, 2004.
[15] R. Diaconescu. Institution-independent Model Theory. Studies in Universal
Logic. Birkhäuser, 2008.
[16] R. Diaconescu.
Implicit Kripke Semantics and Ultraproductsin Stratified Institutions.
Journal of Logic and Computation,
DOI:10.1093/logcom/exw018, 2016.
[17] R. Diaconescu. Quasi-varieties and initial semantics for hybridized institutions. Journal of Logic and Computation, 26(3):855–891, 2016.
[18] R. Diaconescu and K. Futatsugi. CafeOBJ Report: The Language, Proof
Techniques, and Methodologies for Object-Oriented Algebraic Specification,
volume 6 of AMAST Series in Computing. World Scientific, 1998.
[19] R. Diaconescu and K. Futatsugi. Logical foundations of CafeOBJ. Theoretical Computer Science, 285(2):289–318, 2002.
[20] R. Diaconescu, K. Futatsugi, and K. Ogata. CafeOBJ: Logical Foundations
and Methodologies. Computers and Artificial Intelligence, 22(3-4):257–283,
2003.
[21] R. Diaconescu and A. Madeira. Encoding hybridized institutions into firstorder logic. Mathematical Structures in Computer Science, 26(5):745–788,
2016.
[22] J. A. Goguen and R. M. Burstall. Institutions: Abstract Model Theory forSpecification and Programming. Journal of the Association for Computing
Machinery, 39(1):95–146, 1992.

38

[23] J. A. Goguen, G. Malcolm, and T. Kemp. A hidden Herbrand theorem: combining the object and logic paradigms. J. Log. Algebr. Program.,
51(1):1–41, 2002.
[24] J. A. Goguen and J. Meseguer. Equality, types, modules, and (why not ?)generics for logic programming. J. Log. Program., 1(2):179–210, 1984.
[25] J. A. Goguen and G. Roşu. Institution Morphisms. Formal Asp. Comput.,
13(3-5):274–307, 2002.
[26] J. A. Goguen and J. W. Thatcher. Initial Algebra Semantics. In SWAT
(FOCS), pages 63–77. IEEE Computer Society, 1974.
[27] D. Găină. Logical Foundations for Logic Programming in Hybridised Logics. In R. Diaconescu, M. Codescu, and I. Ţuţu, editors, Recent Trends in
Algebraic Development Techniques - 20th International Workshop, WADT
2014, Sinaia, Romania, September 4-7, 2014, Revised Selected Papers, volume 9463 of Lecture Notes in Computer Science, pages 69–89. Springer,
2014.
[28] D. Găină. Downward Löwenheim-Skolem Theorem and interpolation inlogics with constructors. Journal of Logic and Computation, FirstView:1–
36, May 2015. DOI:10.1093/logcom/exv018.
[29] D. Găină and K. Futatsugi. Initial semantics in logics with constructors.
J. Log. Comput., 25(1):95–116, 2015.
[30] D. Găină, K. Futatsugi, and K. Ogata. Constructor-based logics. J. UCS,
18(16):2204–2233, 2012.
[31] D. Găină and M. Petria. Completeness by Forcing. J. Log. Comput.,20(6):1165–1186, 2010.
[32] J. W. Lloyd. Foundations of Logic Programming, 2nd Edition. Springer,
1987.
[33] A. Madeira, M. A. Martins, L. S. Barbosa, and R. Hennicker. Refinement
in hybridised institutions. Formal Asp. Comput., 27(2):375–395, 2015.
[34] A. Madeira, R. Neves, L. S. Barbosa, and M. A. Martins. A method for
rigorous design of reconfigurable systems. Sci. Comput. Program., 132:50–
76, 2016.
[35] M. A. Martins, A. Madeira, R. Diaconescu, and L. S. Barbosa. Hybridization of institutions. In A. Corradini, B. Klin, and C. Cı̂rstea, editors, Algebra and Coalgebra in Computer Science - 4th International Conference,
CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Proceedings, volume 6859 of Lecture Notes in Computer Science, pages 283–297.
Springer, 2011.

39

[36] T. Mossakowski. Relating CASL with other specification languages: theinstitution level. Theor. Comput. Sci., 286(2):367–475, 2002.
[37] P. D. Mosses. CASL Reference Manual, The Complete Documentationof the Common Algebraic Specification Language, volume 2960 of Lecture
Notes in Computer Science. Springer, 2004.
[38] R. Neves, A. Madeira, M. A. Martins, and L. S. Barbosa. Proof theory forhybrid(ised) logics. Sci. Comput. Program., 126:73–93, 2016.
[39] S. Passay and T. Tinchev. An Essay in Combinatory Dynamic Logic.
Information and Computation, 93(2):263–332, 1991.
[40] A. Prior. Past, Present and Future. Oxford books. OUP Oxford, 1967.
[41] H. Reichel. Structural Induction on Partial Algebras. Akademie-Verlag
Berlin, 1984.
[42] G. Schurz. Combinations and completeness transfer for quantified modal
logics. Logic Journal of the IGPL, 19(4):598–616, 2011.
[43] R. Szepesia and H. Ciocârlie. An overview on software reconfiguration.
Theory Appl. Math. Comput. Sci., 1(1):74–79, 2011.
[44] A. Tarlecki. On the Existence of Free Models in Abstract Algebraic Institutuons. Theor. Comput. Sci., 37:269–304, 1985.
[45] 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, volume 240, pages 334–360. Springer, 1986.
[46] A. Tarlecki. Quasi-varieties in Abstract Algebraic Institutions. J. Comput.
Syst. Sci., 33(3):333–360, 1986.

Appendix A. Exiled proofs
Proof of Lemma 30. We proceed by induction on the structure of the ∆-terms:(1) Let ς ∈ F r , k ∈ Nom and τ ∈ (Tk∆ )ar , where ar is the arity of ς, and assume(W 0 , M 0 )ϕ(τ ) = ((W 0 , M 0 )  ϕ )τ .
We have (W 0 , M 0 )ϕ(ς(τ )) = (Mw0 0 )ϕ(ς) ((W 0 , M 0 )ϕ(τ ) ), where w0 = Wϕ0 REL (k) .
It follows that (Mw0 0 )ϕ(ς) ((W 0 , M 0 )ϕ(τ ) ) = (Mw0 0  ϕ )ς (((W 0 , M 0 )  ϕ )τ ) =((W 0 , M 0 )  ϕ )ς(τ ) .

40

(2) Let σ ∈ (F − F r ), k ∈ Nom and t ∈ (Tk∆ )a , where a is the arity of σ, andassume (W 0 , M 0 )ϕ(t) = ((W 0 , M 0 )  ϕ )t .
We have (W 0 , M 0 )ϕ(σk (t)) = (Mw0 0 )ϕ(σ) ((W 0 , M 0 )ϕ(t) ), where w0 = Wϕ0 REL (k) .
It follows that (Mw0 0 )ϕ(σ) ((W 0 , M 0 )ϕ(t) ) = (Mw0 0  ϕ )σ (((W 0 , M 0 )  ϕ )t ) =((W 0 , M 0 )  ϕ )σk (t) .
(3) Let k1 ∈ Nom, sr ∈ S r , t ∈ (Tk∆1 )sr and assume that (W 0 , M 0 )ϕ(t) =((W 0 , M 0 )  ϕ )t . We can conclude that for t ∈ (Tk∆ )s we have (W 0 , M 0 )ϕ(t) =((W 0 , M 0 )  ϕ )t .

Proof of Corollary 31. In order to show that HFOLSA is an institution, we
need to show the local satisfaction condition holds. We prove that the local
satisfaction condition holds for atomic sentences.
(a) We have (W 0 , M 0 )  ϕ |= (t = t0 ) iff ((W 0 , M 0 )  ϕ )t = ((W 0 , M 0 )  ϕ )t0 for
all t, t0 ∈ (Tk∆ ); by Lemma 30, we have ((W 0 , M 0 )  ϕ )t = ((W 0 , M 0 )  ϕ )t0 iff(W 0 , M 0 )ϕ(t) = (W 0 , M 0 )ϕ(t0 ) , and we get (W 0 , M 0 )ϕ(t) = (W 0 , M 0 )ϕ(t0 ) iff(W 0 , M 0 ) |= ϕ(t = t0 ).
(b) Let $ ∈ P r , k ∈ Nom and τ ∈ (Tk∆ )ar , where ar is the arity of $: wehave that (W 0 , M 0 )  ϕ |= $(τ ) iff ((W 0 , M 0 )  ϕ )τ ∈ (Mw0 0  ϕ )$ , where0
w0 = Wϕ(k), iff (W 0 , M 0 )ϕ(τ ) ∈ (Mw0 0 )ϕ($) iff (W 0 , M 0 ) |= ϕ($(τ )).
(c) Let π ∈ (P − P r ), k ∈ Nom and t ∈ (Tk∆ )a , where a is the arity of σ: we have0
(W 0 , M 0 )  ϕ |= πk (t) iff ((W 0 , M 0 )  ϕ )t ∈ (Mw0 0  ϕ )π , where w0 = Wϕ(k)
, iff
0
0
0
0
0
(W , M )ϕ(t) ∈ (Mw0 )ϕ(π) iff (W , M ) |= ϕ(πk (t)).
The remaining proof is straightforward and it is similar to the proof of the local
satisfaction condition for hybridized institutions (see Theorem 3.2 of [17]).

41