Foundations of Logic Programming in Hybridised Logics

Abstract

The present paper sets the foundation of logic programming in hybridised logics. The basic logic programming semantic concepts such as query and solutions, and the fundamental results such as the existence of initial models and Herbrand’s theorem, are developed over a very general hybrid logical system. We employ the hybridisation process proposed by Diaconescu over an arbitrary logical system captured as an institution to define the logic programming framework.

1 Introduction

Hybrid logics [1] are a brand of modal logics that allows direct reference to the possible worlds/states in a simple and very natural way through the so-called nominals. This feature has several advantages from the point of view of logic and formal specification. For example, it becomes considerably simpler to define proof systems in hybrid logics [2], and one can prove results of a generality that is not available in non-hybrid modal logic. In specifications of dynamic systems the possibility of explicit reference to specific states of the model is an essential feature.

The hybridisation of a logic is the process of developing the features of hybrid logic on top of the base logic both at the syntactic level (i.e. modalities, nominals, etc.) and semantics (i.e. possible worlds). By a hybridised institution (or hybrid institution) we mean the result of this process when logics are treated abstractly as institutions [7]. The hybridisation development in [6, 13] abstracts away the details, both at the syntactic and semantic levels, that are independent of the very essence of the hybrid logic idea. One great advantage of this approach is the clarity of the theoretical developments that are not hindered by the irrelevant details of the concrete logics. Another practical benefit is the applicability of the results to a wide variety of concrete instances.

In this paper we investigate a series of model-theoretic properties of hybrid logics in an institution-independent setting such as basic set of sentences [3], substitution [4] and reachable model [10, 11]. While the definition of basic set of sentences is a straightforward extension from a base institution to its hybrid counterpart, the notion of substitution needs much consideration. Establishing an appropriate concept of substitution is the most difficult part of the whole enterprise of constructing an initial model of a given hybrid theory and proving a variant of Herbrand’s theorem. The notion of substitution is closely related to quantification. Our abstract results are applicable to hybrid logical systems where the variables may be interpreted differently across distinct worlds, which amounts to the world-line semantics of [14]. Our paper does not cover the rigid quantification of [2] when the possible worlds share the same domain and the variables are interpreted the same in all worlds.

Initial semantics [8] is closely related to good computational properties of logical systems and it plays a crucial role for the semantics of abstract data types. For example, initiality supports the execution of specification languages through rewriting, thus integrating efficiently formal verification of software systems into modelling. The initial semantics methodology has spread much beyond its original context, that of traditional equational specification, to a variety of modern and more sophisticated logical contexts. Moreover, initial semantics plays a foundational role in logic programming. For example, in [12], initial models are known as “least Herbrand models”. Our approach to initiality is layered and is intimately linked to the structure of sentences, in the style of [9]. The existence of initial models of sets of atomic sentences is assumed in abstract setting but is developed in concrete examples; then the initiality property is shown to be closed under certain sentence building operators.

The second main contribution of the paper is a variant of Herbrand’s theorem for hybrid institutions, which reduces the satisfiability of a query with respect to a hybrid theory to the search of a suitable substitution. The logic programming paradigm [12], in its classical form, can be described as follows: Given a program $(\varSigma ,\varGamma )$ (that consists of a signature $\varSigma$ and a set of Horn clauses $\varGamma$) and a query $(\exists Y)\rho$ (that consists of an existentially quantified conjunction of atoms) find a solution $\theta$, i.e. values for the variables Y such that the corresponding instance $\theta (\rho )$ of $\rho$ is satisfied by $(\varSigma ,\varGamma )$. The essence of this paradigm is however independent of any logical system of choice. The basic logic programming concepts, query, solutions, and the fundamental results, such as Herbrand’s theorem, are developed over an arbitrary institution (satisfying certain hypotheses) in [4] by employing institution-independent concepts of variables, substitution, quantifiers and atomic formulas. Our work sets foundation for a uniform development of logic programming over a large variety of hybrid logics as we employ the hybridisation process over an arbitrary institution [6, 13] to prove the desired results.

The institution-independent status of the present study makes the results applicable to a multitude of concrete hybrid logics including those obtained from hybridisation of non-conventional logics used in computer science.

The paper is organised as follows: in Sect. 2 we recall the definition of institution and the related notions such as substitution, reachable model and basic set of sentences. In Sect. 3 we recall the institution-indepedent process of hybridisation of a logical system and we lift the notions discussed in the previous section to the hybrid setting. Section 4 is dedicated to the development of the layered initiality result. In Sect. 5 we present an institution-independent version of Herbrand’s theorem and its applications to concrete hybrid logics. Section 6 concludes the paper and discusses the future work.

2 Institutions

The concept of institution formalises the intuitive notion of logical system, and has been defined by Goguen and Burstall in the seminal paper [7].

Definition 1

An institution $\mathtt {I}=({\mathbb Sig}^\mathtt {I},{\mathbb Sen}^\mathtt {I},{\mathbb Mod}^\mathtt {I},\models ^\mathtt {I})$ consists of

• (1) a category ${\mathbb Sig}^\mathtt {I}$, whose objects are called signatures,

• (2) a functor ${\mathbb Sen}^\mathtt {I}:{\mathbb Sig}^\mathtt {I}\rightarrow {\mathbb Set}$, providing for each signature $\varSigma$ a set whose elements are called ($\varSigma$-)sentences,

• (3) a functor ${\mathbb Mod}^\mathtt {I}: ({\mathbb Sig}^\mathtt {I})^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$, providing for each signature $\varSigma$ a category whose objects are called ($\varSigma$-)models and whose arrows are called ($\varSigma$-)morphisms,

• (4) a relation $\models ^\mathtt {I}_{\varSigma }\subseteq |{\mathbb Mod}^\mathtt {I}(\varSigma )|\times {\mathbb Sen}^\mathtt {I}(\varSigma )$ for each signature $\varSigma \in |{\mathbb Sig}^\mathtt {I}|$, called ($\varSigma$-)satisfaction, such that for each morphism $\varphi :\varSigma \rightarrow \varSigma '$ in ${\mathbb Sig}^\mathtt {I}$, the following satisfaction condition holds:

  $$M'\models ^\mathtt {I}_{\varSigma '} {\mathbb Sen}^\mathtt {I}(\varphi )(e) \text{ iff } {\mathbb Mod}^\mathtt {I}(\varphi )(M')\models ^\mathtt {I}_{\varSigma }e $$

  for all $M'\in |{\mathbb Mod}^\mathtt {I}(\varSigma ')|$ and $e\in {\mathbb Sen}^\mathtt {I}(\varSigma )$.

When there is no danger of confusion, we omit the superscript from the notations of the institution components; for example ${\mathbb Sig}^\mathtt {I}$ may be simply denoted by ${\mathbb Sig}$. We denote the reduct functor ${\mathbb Mod}(\varphi )$ by $\_\!\upharpoonright \!_{\varphi }$ and the sentence translation ${\mathbb Sen}(\varphi )$ by $\varphi (\_)$. When $M=M'\!\upharpoonright \!_{\varphi }$ we say that M is the $\varphi$-reduct of $M'$ and $M'$ is a $\varphi$-expansion of M. We say that $\varphi$ is conservative if each $\varSigma$-model has a $\varphi$-expansion. Given a signature $\varSigma$ and two sets of $\varSigma$-sentences $E_1$ and $E_2$, we write $E_1\mathrel {\models \!\!\!|}E_2$ whenever $E_1 \models E_2$ and $E_2\models E_1$.

The literature shows myriads of logical systems from computing or mathematical logic captured as institutions (see, for example, [5]).

Example 1

(First-Order Logic (${\mathbf {FOL}}$) [7]). The signatures are triplets (S, F, P), where S is the set of sorts, $F=\{F_{{\underline{ar}}\rightarrow s})\}_{({\underline{ar}},s)\in S^*\times S}$ is the ($S^*\!\!\times \! S$ -indexed) set of operation symbols, and $P=\{P_{\underline{ar}}\}_{{\underline{ar}}\in S^*}$ is the ($S^*$-indexed) set of relation symbols. If ${\underline{ar}}=\epsilon$, where $\epsilon$ denotes the empty arity, an element of $F_{{\underline{ar}}\rightarrow s}$ is called a constant symbol, or a constant. By a slight notational abuse, we let F and P also denote $\bigcup _{({\underline{ar}},s)\in S^*\times S}F_{{\underline{ar}}\rightarrow s}$ and $\bigcup _{{\underline{ar}}\in S^*}P_{\underline{ar}}$, respectively. A signature morphism between (S, F, P) and $(S',F',P')$ is a triplet $\varphi =(\varphi ^{st},\varphi ^{op},\varphi ^{rl})$, where $\varphi ^{st}:S\rightarrow S'$, $\varphi ^{op}:F\rightarrow F'$, $\varphi ^{rl}:P\rightarrow P'$ such that for all $({\underline{ar}},s)\in S^*\times S$ we have $\varphi ^{op}(F_{{\underline{ar}}\rightarrow s})\subseteq F'_{\varphi ^{st}({\underline{ar}})\rightarrow \varphi ^{st}(s)}$, and for all ${\underline{ar}}\in S^*$ we have $\varphi ^{rl }(P_{\underline{ar}})\subseteq P'_{\varphi ^{st}({\underline{ar}})}$. When there is no danger of confusion, we may let $\varphi$ denote each of $\varphi ^{st}$, $\varphi ^{op}$, $\varphi ^{rl}$. Given a signature $\varSigma =(S,F,P)$, a $\varSigma$-model is a triplet $M=(\{s_M\}_{s\in S}, \{\sigma _M\}_{({\underline{ar}},s)\in S^*\times S,\sigma \in F_{{\underline{ar}}\rightarrow s}},\{\pi _M\}_{{\underline{ar}}\in S^*,\pi \in P_{\underline{ar}}})$ interpreting each sort s as a set $s_M$, each operation symbol $\sigma \in F_{{\underline{ar}}\rightarrow s}$ as a function $\sigma _M:{\underline{ar}}_M\rightarrow s_M$ (where ${\underline{ar}}_M$ stands for $(s_1)_M\times \ldots \times (s_n)_M$ if ${\underline{ar}}=s_1\ldots s_n$), and each relation symbol $\pi \in P_{\underline{ar}}$ as a relation $\pi _M\subseteq {\underline{ar}}_M$. Morphisms between models are the usual $\varSigma$-morphisms, i.e., S-sorted functions that preserve the structure. The $\varSigma$-algebra of terms is denoted by $T_\varSigma$. The $\varSigma$-sentences are obtained from (a) equality atoms (e.g. $t_1= t_2$, where $t_1,t_2\in s_{T_\varSigma }$, $s\in S$) or (b) relational atoms (e.g. $\pi (t_1,\ldots ,t_n)$, where $\pi \in P_{s_1\ldots s_n}$, $t_i\in (s_i)_{T_\varSigma }$, $s_i\in S$ and $i\in \{1,\ldots ,n\}$) by applying for a finite number of times Boolean connectives and quantification over finite sets of variables. Satisfaction is the usual first-order satisfaction and is defined using the natural interpretations of ground terms t as elements $t_M$ in models M. The definitions of functors ${\mathbb Sen}$ and ${\mathbb Mod}$ on morphisms are the natural ones: for any signature morphism $\varphi :\varSigma \rightarrow \varSigma '$, ${\mathbb Sen}(\varphi ):{\mathbb Sen}(\varSigma )\rightarrow {\mathbb Sen}(\varSigma ')$ translates sentences symbol-wise, and ${\mathbb Mod}(\varphi ):{\mathbb Mod}(\varSigma ')\rightarrow {\mathbb Mod}(\varSigma )$ is the forgetful functor.

Example 2

(${\mathbf {REL}}$). The institution ${\mathbf {REL}}$ is the sub-institution of single-sorted first-order logic with signatures having only constants and relational symbols.

Example 3

(Propositional Logic $({\mathbf {PL}})$. The institution ${\mathbf {PL}}$ is the fragment of ${\mathbf {FOL}}$ determined by signatures with empty sets of sort symbols.

Example 4

(Constrained Institutions). Let $\mathtt {I}=({\mathbb Sig}^\mathtt {I},{\mathbb Sen}^\mathtt {I},{\mathbb Mod}^\mathtt {I},\models ^\mathtt {I})$ be an institution. A constrained model functor ${\mathbb Mod}^{\mathtt {CI}}:({\mathbb Sig}^{\mathtt {CI}})^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ is a sub-functor of ${\mathbb Mod}^\mathtt {I}:({\mathbb Sig}^\mathtt {I})^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$, i.e. ${\mathbb Sig}^{\mathtt {CI}}\subseteq {\mathbb Sig}^\mathtt {I}$, for each $\varSigma \in |{\mathbb Sig}^{\mathtt {CI}}|$ we have ${\mathbb Mod}^{\mathtt {CI}}(\varSigma )\subseteq {\mathbb Mod}^\mathtt {I}(\varSigma )$, and for each $\varSigma \mathop {\rightarrow }\limits ^{\varphi }\varSigma \in {\mathbb Sig}^{\mathtt {CI}}$ the functor ${\mathbb Mod}^{\mathtt {CI}}(\varphi ):{\mathbb Mod}^{\mathtt {CI}}(\varSigma ')\rightarrow {\mathbb Mod}^{\mathtt {CI}}(\varSigma )$ is defined by ${\mathbb Mod}^{\mathtt {CI}}(\varphi )(h)={\mathbb Mod}^\mathtt {I}(\varphi )(h)$ for all $h\in {\mathbb Mod}^{\mathtt {CI}}(\varSigma ')$. We say that ${\mathtt {CI}}=({\mathbb Sig}^{\mathtt {CI}},{\mathbb Sen}^{\mathtt {CI}},{\mathbb Mod}^{\mathtt {CI}},\models ^{\mathtt {CI}})$ is a constrained institution, where (a) ${\mathbb Sen}^{\mathtt {CI}}:{\mathbb Sig}^{\mathtt {CI}}\rightarrow {\mathbb Set}$ is the restriction of ${\mathbb Sen}^\mathtt {I}:{\mathbb Sig}^\mathtt {I}\rightarrow {\mathbb Set}$ to ${\mathbb Sig}^{\mathtt {CI}}$, and (b) $\models ^{\mathtt {CI}}_\varSigma \subseteq |{\mathbb Mod}^{\mathtt {CI}}(\varSigma )|\times {\mathbb Sen}^\mathtt {I}(\varSigma )$ is the restriction of $\models ^\mathtt {I}_\varSigma \subseteq |{\mathbb Mod}^\mathtt {I}(\varSigma )|\times {\mathbb Sen}^\mathtt {I}(\varSigma )$ to $|{\mathbb Mod}^{\mathtt {CI}}(\varSigma )|$ for all $\varSigma \in |{\mathbb Sig}^{\mathtt {CI}}|$.

2.1 Quantification Subcategory

Let $\mathtt {I}=({\mathbb Sig},{\mathbb Sen},{\mathbb Mod},\models )$ be an institution. A broad subcategory¹ $\mathcal{Q}\subseteq {\mathbb Sig}$ is called quantification subcategory [6] when for each $\varSigma \mathop {\rightarrow }\limits ^{\chi }\varSigma '\in \mathcal{Q}$ and $\varSigma \mathop {\rightarrow }\limits ^{\varphi }\varSigma _1\in {\mathbb Sig}$ there is a designated pushout with $\chi (\varphi )\in \mathcal{Q}$ which is a weak amalgamation square² and such that the horizontal composition of such designated pushouts is again a designated pushout, i.e. $\chi (1_\varSigma )=\chi$, $1_\varSigma [\chi ]=1_{\varSigma '}$, and for the following pushouts we have $\varphi [\chi ];\theta [\chi (\varphi )]=(\varphi ;\theta )[\chi ]$ and $\chi (\varphi )(\theta )=\chi (\varphi ;\theta )$.

A variable for a ${\mathbf {FOL}}$ signature $\varSigma =(S,F,P)$ is a triple $(x,s,\varSigma )$, where x is the name of the variable and $s\in S$ is the sort of the variable. Let $\chi :\varSigma \hookrightarrow \varSigma [X]$ be a signature extension with variables from X, where $X=\{X_s\}_{s\in S}$ is a S-sorted set of variables, $\varSigma [X]=(S,F \cup X,P)$ and for all $({\underline{ar}},s)\in S^*\times S$ we have $(F \cup X)_{{\underline{ar}}\rightarrow s}= \left\{ \begin{array}{l l} F_{{\underline{ar}}\rightarrow s} &{} \text{ if } {\underline{ar}}\in S^+,\\ F_{{\underline{ar}}\rightarrow s} \cup X_s &{} \text{ if } {\underline{ar}}= \epsilon . \end{array}\right.$ The quantification subcategory $\mathcal{Q}^{\mathbf {FOL}}$ for ${\mathbf {FOL}}$ consists of signature extensions with a finite set of variables. Given a signature morphism $\varphi :\varSigma \rightarrow \varSigma _1$, where $\varSigma _1=(S_1,F_1,P_1)$, then

• $\chi (\varphi ):\varSigma _1\hookrightarrow \varSigma _1[X^\varphi ]$, where $X^\varphi =\{(x,\varphi (s),\varSigma _1)\mid (x,s,\varSigma )\in X\}$,

• $\varphi [\chi ]$ is the canonical extension of $\varphi$ that maps each $(x,s,\varSigma )$ to $(x,\varphi (s),\varSigma _1)$.

It is straightforward to check that $\mathcal{Q}^{\mathbf {FOL}}$ defined above is a quantification subcategory.

2.2 Substitutions

We recall the notion of substitution in institutions.

Definition 2

[4]. Let $\mathtt {I}=({\mathbb Sig},{\mathbb Sen},{\mathbb Mod},\models )$ be an institution and $\varSigma \in |{\mathbb Sig}|$. For any signature morphisms $\chi _1:\varSigma \rightarrow \varSigma _1$ and $\chi _2:\varSigma \rightarrow \varSigma _2$, a $\varSigma$-substitution $\theta :\chi _1\rightarrow \chi _2$ consists of a pair $({\mathbb Sen}(\theta ),{\mathbb Mod}(\theta ))$, where

• ${\mathbb Sen}(\theta ):{\mathbb Sen}(\varSigma _1)\rightarrow {\mathbb Sen}(\varSigma _2)$ is a function and

• ${\mathbb Mod}(\theta ):{\mathbb Mod}(\varSigma _2)\rightarrow {\mathbb Mod}(\varSigma _1)$ is a functor.

such that both of them preserve $\varSigma$, i.e. the following diagrams commute:

and such that the following satisfaction condition holds:

$${\mathbb Mod}(\theta )(M_2)\models \rho _1 \text{ iff } M_2\models {\mathbb Sen}(\theta )(\rho _1)$$

for each $\varSigma _2$-model $M_2$ and each $\varSigma _1$-sentence $\rho _1$.

Note that a substitution $\theta :\chi _1\rightarrow \chi _2$ is uniquely identified by its domain $\chi _1$, codomain $\chi _2$ and the pair $({\mathbb Sen}(\theta ),{\mathbb Mod}(\theta ))$. We sometimes let $\_ \!\upharpoonright \!_{\theta }$ denote the functor ${\mathbb Mod}(\theta )$, and let $\theta$ denote the sentence translation ${\mathbb Sen}(\theta )$.

Example 5

(${\mathbf {FOL}}$ substitutions [4]). Consider two signature extensions with constants $\chi _1:\varSigma {\hookrightarrow } \varSigma [C_1]$ and $\chi _2:\varSigma \hookrightarrow \varSigma [C_2]$, where $\varSigma =(S,F,P)\in |{\mathbb Sig}^{\mathbf {FOL}}|$, $C_i$ is a set of constant symbols different from the symbols in $\varSigma$. A function $\theta : C_1\rightarrow T_\varSigma (C_2)$ represents a substitution between $\chi _1$ and $\chi _2$. On the syntactic side, $\theta$ can be canonically extended to a function ${\mathbb Sen}(\theta ):{\mathbb Sen}(\varSigma [C_1])\rightarrow {\mathbb Sen}(\varSigma [C_2])$ as follows:

• ${\mathbb Sen}(\theta )(t_1=t_2)$ is defined as $\theta ^{term}(t)=\theta ^{term}(t')$ for each $\varSigma [C_1]$-equation $t_1=t_2$, where $\theta ^{term}:T_\varSigma (C_1)\rightarrow T_\varSigma (C_2)$ is the unique extension of $\theta$ to a $\varSigma$-morphism.

• ${\mathbb Sen}(\theta )(\pi (t_1,\ldots ,t_n))$ is defined as $\pi (\theta ^{term}(t_1),\ldots ,\theta ^{term}(t_n))$ for each $\varSigma [C_1]$-relational atom $\pi (t_1,\ldots ,t_n)$.

• ${\mathbb Sen}(\theta )(\bigwedge E)$ is defined as $\bigwedge {\mathbb Sen}(\theta )(E)$ for each conjuction $\bigwedge E$ of $\varSigma [C_1]$-sentences, and similarly for the case of any other Boolean connectives.

• ${\mathbb Sen}(\theta )((\forall X)\rho )$ is defined as $(\forall X^\theta ){\mathbb Sen}(\theta ')(\rho )$ for each $\varSigma [C_1]$-sentence $(\forall X)\rho$, where $X^\theta =\{(x,s,\varSigma [C_2])\mid (x,s,\varSigma [C_1])\in X\}$ and the substitution $\theta ':C_1\cup X \rightarrow T_\varSigma (C_2\cup X^\theta )$ extends $\theta$ by mapping each variable $(x,s,\varSigma [C_1])\in X$ to $(x,s,\varSigma [C_2])\in X^\theta$.

On the semantics side, $\theta$ determines a functor ${\mathbb Mod}(\theta )$ between ${\mathbb Mod}(\varSigma [C_2])$ and ${\mathbb Mod}(\varSigma [C_1])$ such that for all $\varSigma [C_2]$-models M we have

• ${\mathbb Mod}(\theta )(M)_x = M_x$, for each sort $x\in S$, or operation symbol $x\in F$, or relation symbol $x\in P$, and

• ${\mathbb Mod}(\theta )(M)_x = M_{\theta (x)}$ for each $x\in C_1$.

Category of Substitutions. Let $\mathtt {I}=({\mathbb Sig},{\mathbb Sen},{\mathbb Mod},\models )$ be an institution and $\varSigma \in |{\mathbb Sig}|$ a signature. $\varSigma$-substitutions form a category ${\mathbb Subst}^\mathtt {I}(\varSigma )$, where the objects are signature morphisms $\varSigma \mathop {\rightarrow }\limits ^{\chi }\varSigma '\in |\varSigma /{\mathbb Sig}|$, and the arrows are substitutions $\theta :\chi _1\rightarrow \chi _2$ as described in Definition 2. For any substitutions $\theta :\chi _1\rightarrow \chi _2$ and $\theta ':\chi _2\rightarrow \chi _3$ the composition $\theta ;\theta '$ consists of the pair $({\mathbb Sen}(\theta ;\theta '),{\mathbb Mod}(\theta ;\theta '))$, where ${\mathbb Sen}(\theta ;\theta ')={\mathbb Sen}(\theta );{\mathbb Sen}(\theta ')$ and ${\mathbb Mod}(\theta ;\theta ')={\mathbb Mod}(\theta ');{\mathbb Mod}(\theta )$.

Given a signature morphism $\varphi :\varSigma _0\rightarrow \varSigma$ there exists a reduct functor ${\mathbb Subst}^\mathtt {I}(\varphi ):{\mathbb Subst}^\mathtt {I}(\varSigma )\rightarrow {\mathbb Subst}^\mathtt {I}(\varSigma _0)$ that maps any $\varSigma$-substitution $\theta :\chi _1\rightarrow \chi _2$ to the $\varSigma _0$-substitution ${\mathbb Subst}(\varphi )(\theta ):\varphi ;\chi _1\rightarrow \varphi ;\chi _2$ such that ${\mathbb Sen}({\mathbb Subst}^\mathtt {I}(\varphi )(\theta ))={\mathbb Sen}(\theta )$ and ${\mathbb Mod}({\mathbb Subst}^\mathtt {I}(\varphi )(\theta ))={\mathbb Mod}(\theta )$. It follows that ${\mathbb Subst}^\mathtt {I}:{\mathbb Sig}^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ is a functor. In applications not all substitutions are of interest, and it is often assumed a substitution sub-functor ${\mathbb Sub}^\mathtt {I}:\mathcal{D}^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ of ${\mathbb Subst}^\mathtt {I}:{\mathbb Sig}^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ to work with, where $\mathcal{D}\subseteq {\mathbb Sig}$ is a subcategory of signature morphisms. When there is no danger of confusion we may drop the superscript $\mathtt {I}$ from the notations; for example ${\mathbb Sub}^\mathtt {I}$ may be simply denoted by ${\mathbb Sub}$.

Example 6

(${\mathbf {FOL}}$ substitution functor). Given a signature $\varSigma \in |{\mathbb Sig}^{\mathbf {FOL}}|$, only $\varSigma$-substitutions represented by functions $\theta :C_1\rightarrow T_\varSigma (C_2)$ are relevant for the present study, where $C_1$ and $C_2$ are finite sets of new constants for $\varSigma$. Let ${\mathbb Sub}^{\mathbf {FOL}}:(\mathcal{D}^{\mathbf {FOL}})^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ denote the substitution functor which maps each signature $\varSigma$ to the subcategory of $\varSigma$-substitutions represented by functions of the form $\theta :C_1\rightarrow T_\varSigma (C_2)$ as above.

Example 7

(${\mathbf {PL}}$ substitution functor) Let $\mathcal{D}^{\mathbf {PL}}$ be the subcategory of ${\mathbf {PL}}$ signature morphisms consisting of identities, and ${\mathbb Sub}^{\mathbf {PL}}:(\mathcal{D}^{\mathbf {PL}})^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ the trivial substitution functor consisting also of identities.

2.3 Reachable Models

This subsection is devoted to the institution-independent characterisation of the models that consist of interpretations of terms.

Definition 3

Let $\mathtt {I}=({\mathbb Sig},{\mathbb Sen},{\mathbb Mod},\models )$ be an institution, $\mathcal{D}\subseteq {\mathbb Sig}$ a broad subcategory of signature morphisms, and ${\mathbb Sub}:\mathcal{D}^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ a substitution functor. A model $M\in |{\mathbb Mod}(\varSigma )|$, where $\varSigma \in |{\mathbb Sig}|$, is ${\mathbb Sub}$-reachable if for every signature morphism $\varSigma \mathop {\rightarrow }\limits ^{\chi }\varSigma '\in \mathcal{D}$ and each $\chi$-expansion $M'$ of M there exists a substitution $\theta :\chi \rightarrow 1_\varSigma \in {\mathbb Sub}(\varSigma )$ such that $M\!\upharpoonright \!_\theta =M'$.

This notion of reachable model is the parametrisation of the one in [10] with substitutions.

Proposition 1

In ${\mathbf {FOL}}$, a model is ${\mathbb Sub}^{\mathbf {FOL}}$-reachable iff its elements consist of interpretations of terms.

The proof of Proposition 1 is a slight generalisation of the one in [10]. Note that in ${\mathbf {PL}}$, all models are ${\mathbb Sub}^{\mathbf {PL}}$-reachable.

2.4 Basic Sentences

A set of sentences $B\subseteq Sen(\varSigma )$ is basic [3] if there exists a $\varSigma$-model $M^B$ such that, for all $\varSigma$-models M, $M\models B$ iff there exists a morphism $M^B\rightarrow M$. We say that $M^B$ is a basic model of B. If in addition the morphism $M^B\rightarrow M$ is unique then the set B is called epi basic; in this case, $M^B$ is the initial model of B.

Lemma 1

Any set of atoms in ${\mathbf {FOL}}$ is epi basic and the corresponding basic models consist of interpretations of terms, i.e. are ${\mathbb Sub}^{\mathbf {FOL}}$-reachable.

Proof

Let B be a set of atomic (S, F, P)-sentences in ${\mathbf {FOL}}$. The basic model $M^B$ is the initial model of B and it is constructed as follows: on the quotient $T_{(S,F)}/_{\equiv _B}$ of the term model $T_{(S,F)}$ by the congruence generated by the equational atoms of B, we interpret each relation symbol $\pi \in P$ by $\pi _{M^B}=\{(\widehat{t_1},\ldots ,\widehat{t_n})\mid \pi (t_1,\ldots ,t_n)\in B\}$, where $\widehat{t}$ is the congruence class of t for all terms $t\in T_{(S,F)}$.    $\square$

The proof of Lemma 1 is well known, and it can be found, for example, in [3] or [5], but since it constitutes the foundation of the initiality property, we include it for the convenience of the reader. Since ${\mathbf {PL}}$ is obtained from ${\mathbf {FOL}}$ by restricting the category of signatures, every set of ${\mathbf {PL}}$ atoms is epi basic.

3 Hybrid Institutions

We recall the institution-independent process of hybridisation that has been introduced in [6, 13]. Consider an institution $\mathtt {I}=({\mathbb Sig},{\mathbb Sen},{\mathbb Mod},\models )$ with a quantification subcategory $\mathcal{Q}\subseteq {\mathbb Sig}$.

The Category of ${\mathtt {HI}}$ Signatures. The category of hybrid signatures of ${\mathbb Sig}$ is defined as the following cartesian product of categories: ${\mathbb Sig}^{\mathtt {HI}}={\mathbb Sig}^\mathtt {I}\times {\mathbb Sig}^{\mathbf {REL}}$. The ${\mathbf {REL}}$ signatures are denoted by $(Nom,\varLambda )$, where Nom is a set of constants called nominals and $\varLambda$ is a set of relational symbols called modalities; $\varLambda _n$ stands for the set of modalities of arity n. Hybrid signatures morphisms $\varphi =(\varphi _{\mathbb Sig},\varphi _{\mathbb Nom},\varphi _{\mathbb Rel}):(\varSigma ,Nom,\varLambda )\rightarrow (\varSigma ',Nom,\varLambda ')$ are triples such that $\varphi _{\mathbb Sig}:\varSigma \rightarrow \varSigma '\in {\mathbb Sig}^\mathtt {I}$ and $(\varphi _{\mathbb Nom},\varphi _{\mathbb Rel}):(Nom,\varLambda )\rightarrow (Nom',\varLambda ')\in {\mathbb Sig}^{\mathbf {REL}}$. When there is no danger of confusion we may drop the subscripts from notations and denote $\varphi _{\mathbb Sig}$, $\varphi _{\mathbb Nom}$ and $\varphi _{\mathbb Rel}$ simply by $\varphi$.

${\mathtt {HI}}$ Sentences. Let us denote by $\mathcal{Q}^{\mathtt {HI}}$ the subcategory $\mathcal{Q}^{\mathtt {HI}}\subseteq {\mathbb Sig}^{\mathtt {HI}}$ which consists of signature morphisms of the form $\chi :(\varSigma ,Nom,\varLambda )\rightarrow (\varSigma ',Nom,\varLambda )$ such that $\chi _{\mathbb Sig}\in \mathcal{Q}$, $\chi _{\mathbb Nom}=1_{Nom}$ and $\chi _{\mathbb Rel}=1_\varLambda$.

Theorem 1

[6, 13]. If $\mathcal{Q}$ is a quantification subcategory for $\mathtt {I}$ then $\mathcal{Q}^{\mathtt {HI}}$ is a quantification subcategory for ${\mathtt {HI}}$.

The satisfaction condition for hybridised institutions relies upon Theorem 1. A nominal variable for a hybrid signature $\varDelta =(\varSigma ,Nom,\varLambda )$ is a pair of the form $(x,\varDelta )$, where x is the name of the variable and $\varDelta$ is the qualification of the variable. Given a hybrid signature $\varDelta =(\varSigma ,Nom,\varLambda )$, the set of sentences ${\mathbb Sen}^{\mathtt {HI}}(\varDelta )$ is the least set such that

• $Nom\subseteq {\mathbb Sen}^{\mathtt {HI}}(\varDelta )$,

• $\lambda (k_1,\ldots ,k_n)\in {\mathbb Sen}^{\mathtt {HI}}(\varDelta )$ for any $\lambda \in \varLambda _{n+1}$, $k_i\in Nom$, $i\in \{1,\ldots ,n\}$;

• ${\mathbb Sen}^\mathtt {I}\subseteq {\mathbb Sen}(\varDelta )$;

• $\rho _1\star \rho _2\in {\mathbb Sen}^{\mathtt {HI}}(\varDelta )$ for any $\rho _1,\rho _2\in {\mathbb Sen}^{\mathtt {HI}}(\varDelta )$ and $\star \in \{\wedge ,\Rightarrow \}$;

• $\lnot \rho \in {\mathbb Sen}^{\mathtt {HI}}(\varDelta )$ for any $\rho \in {\mathbb Sen}^{\mathtt {HI}}(\varDelta )$;

• $@_k\rho \in {\mathbb Sen}^{\mathtt {HI}}(\varDelta )$ for any $\rho \in {\mathbb Sen}^{\mathtt {HI}}(\varDelta )$ and $k\in Nom$;

• $[\lambda ](\rho _1,\ldots ,\rho _n)$ for any $\lambda \in \varLambda _{n+1}$, $\rho _i\in {\mathbb Sen}^{\mathtt {HI}}(\varDelta )$ and $i\in \{1,\ldots ,n\}$;

• $(\forall \chi )\rho '\in {\mathbb Sen}^{\mathtt {HI}}(\varDelta )$ for any $\chi :(\varSigma ,Nom,\varLambda )\rightarrow (\varSigma ',Nom,\varLambda )\in \mathcal{Q}^{\mathtt {HI}}$ and $\rho '\in {\mathbb Sen}^{\mathtt {HI}}(\varSigma ',Nom,\varLambda )$;

• $(\forall J)\rho$ for any set J of nominal variables for $\varDelta$ and $\rho \in {\mathbb Sen}^{\mathtt {HI}}(\varSigma ,Nom\cup J,\varLambda )$;

• $(\downarrow j)\rho$ for any nominal variable j for $\varDelta$ and $\rho \in {\mathbb Sen}^{\mathtt {HI}}(\varSigma ,Nom\cup \{j\},\varLambda )$.

Translation of ${\mathtt {HI}}$ Sentences. Let $\varphi :(\varSigma ,Nom,\varLambda )\rightarrow (\varSigma ',Nom',\varLambda ')$ be a morphism of ${\mathtt {HI}}$ signatures. The translation ${\mathbb Sen}^{\mathtt {HI}}(\varphi )$ is defined as follows:

• ${\mathbb Sen}^{\mathtt {HI}}(\varphi )(k)=\varphi _{\mathbb Nom}(k)$;

• ${\mathbb Sen}^{\mathtt {HI}}(\varphi )(\lambda (k_1,\ldots ,k_n))=\varphi _{\mathbb Rel}(\lambda )(\varphi _{\mathbb Nom}(k_1),\ldots ,\varphi _{\mathbb Nom}(k_n))$ for $\lambda \in \varLambda _{n+1}$, $k_i\in Nom$, $i\in \{1,\ldots ,n\}$;

• ${\mathbb Sen}^{\mathtt {HI}}(\varphi )(\rho )={\mathbb Sen}^\mathtt {I}(\varphi _{\mathbb Sig})(\rho )$ for any $\rho \in {\mathbb Sen}^\mathtt {I}(\varSigma )$;

• ${\mathbb Sen}^{\mathtt {HI}}(\rho _1\star \rho _2)={\mathbb Sen}^{\mathtt {HI}}(\rho _1)\star {\mathbb Sen}^{\mathtt {HI}}(\rho _2)$, where $\star \in \{\wedge ,\Rightarrow \}$;

• ${\mathbb Sen}^{\mathtt {HI}}(\lnot \rho )=\lnot {\mathbb Sen}^{\mathtt {HI}}(\rho )$ ;

• ${\mathbb Sen}^{\mathtt {HI}}(@_k\rho )=@_{\varphi _{\mathbb Nom}(k)}{\mathbb Sen}^{\mathtt {HI}}(\rho )$;

• ${\mathbb Sen}^{\mathtt {HI}}([\lambda ](\rho _1,\ldots ,\rho _n))=[\varphi _{\mathbb Rel}(\lambda )]({\mathbb Sen}^{\mathtt {HI}}(\rho _1),\ldots ,{\mathbb Sen}^{\mathtt {HI}}(\rho _n))$;

• ${\mathbb Sen}^{\mathtt {HI}}((\forall \chi )\rho ')=(\forall \chi (\varphi )){\mathbb Sen}^{\mathtt {HI}}(\varphi [\chi ])(\rho ')$, where the signature morphisms $\chi :(\varSigma ,Nom,\varLambda )\rightarrow (\varSigma ',Nom,\varLambda )$ is in $\mathcal{Q}^{\mathtt {HI}}$, $\chi (\varphi )=(\chi _{\mathbb Sig}(\varphi _{\mathbb Sig}),1_{Nom'},1_{\varLambda '})$ and $\varphi [\chi ]=(\varphi _{\mathbb Sig}[\chi _{\mathbb Sig}],\varphi _{\mathbb Nom},\varphi _{\mathbb Rel})$;

• ${\mathbb Sen}^{\mathtt {HI}}((\forall J)\rho )=(\forall J^\varphi ){\mathbb Sen}^{\mathtt {HI}}(\varphi [J])(\rho )$, where $J^\varphi =\{(x,(\varSigma ',Nom',\varLambda '))\mid (x,(\varSigma ,Nom,\varLambda ))\in J\}$ and $\varphi [J]:(\varSigma ,Nom\cup J,\varLambda )\rightarrow (\varSigma ,Nom'\cup J^\varphi ,\varLambda ')$ is canonical extension of $\varphi$ that maps each variable $(x,(\varSigma ,Nom,\varLambda ))\in J$ to $(x,(\varSigma ',Nom',\varLambda '))$;

• ${\mathbb Sen}^{\mathtt {HI}}((\downarrow j)\rho )=(\downarrow j^\varphi ){\mathbb Sen}^{\mathtt {HI}}(\varphi [j])(\rho )$, where $j^\varphi =(x,(\varSigma ',Nom',\varLambda '))$ and $\varphi ^j:(\varSigma ,Nom\cup \{j\},\varLambda )\rightarrow (\varSigma ',Nom'\cup \{ j^\varphi \},\varLambda ')$ is the canonical extension of $\varphi$ mapping each j to $j^\varphi$.

${\mathtt {HI}}$ Models. The $(\varSigma ,Nom,\varLambda )$-models are paris $(\mathcal{M},R)$ where

• R is a $(Nom,\varLambda )$-model in ${\mathbf {REL}}$. The carrier set |R| forms the set of states of the model $(\mathcal{M},R)$. The relations $\{\lambda _R \mid \lambda \in \varLambda _n, n\in \mathbb {N}\}$ represent the interpretation of the modalities $\varLambda$.

• $\mathcal{M}$ is a function $|R|\rightarrow {\mathbb Mod}^\mathtt {I}(\varSigma )$. For each $s\in |R|$, we denote $\mathcal{M}(s)$ simply by $\mathcal{M}_s$.

A $(\varSigma ,Nom,\varLambda )$-homomorphism $h:(\mathcal{M},R)\rightarrow (\mathcal{M}',R')$ consists of

• a $(Nom,\varLambda )$-homomorphism in ${\mathbf {REL}}$, $h^{st}:R\rightarrow R'$, and

• a natural transformation $h^{mod}:\mathcal{M}\Rightarrow \mathcal{M}' \circ h^{st}$.³

When there is no danger of confusion we may drop the superscripts st and mod from the notations $h^{st}$ and $h^{mod}$, respectively. The composition of ${\mathtt {HI}}$ homomorphisms is defined canonically as $h_1;h_2=((h_1^{st};h_2^{st}), h_1^{mod};(h_2^{mod}\circ h_1^{st}))$.

Reducts of ${\mathtt {HI}}$ Models. Let $\varDelta =(\varSigma ,Nom,\varLambda )$ and $\varDelta '=(\varSigma ',Nom',\varLambda ')$ be two ${\mathtt {HI}}$ signatures, $\varDelta \mathop {\rightarrow }\limits ^{\varphi }\varDelta '$ a ${\mathtt {HI}}$ signature morphism, and $(\mathcal{M}',R')$ a $\varDelta '$-model. The reduct $(\mathcal{M},R)={\mathbb Mod}^{\mathtt {HI}}(\varphi )(\mathcal{M}',R')$ of $(\mathcal{M}',R')$ along $\varphi$ denoted by $(\mathcal{M}',R')\!\upharpoonright \!_\varphi$, is the $\varDelta$-model such that $|R|=|R'|$, $k_R=\varphi _{\mathbb Nom}(k)_{R'}$ for all $k\in Nom$, $\lambda _R=\varphi _{\mathbb Rel}(\lambda )_{R'}$ for all $\lambda \in \varLambda$, and $\mathcal{M}_s={\mathbb Mod}^\mathtt {I}(\varphi _{\mathbb Sig})(\mathcal{M}'_s)$ for all $s\in |R|$.

Satisfaction Relation. For any signaturel $\varDelta =(\varSigma ,Nom,\varLambda )$, model $(\mathcal{M},R)\in |{\mathbb Mod}^{\mathtt {HI}}(\varDelta )|$ and state $s\in |R|$ we define:

• $(\mathcal{M},R)\models ^s k$ iff $k_R=s$, for any $k\in Nom$;

• $(\mathcal{M},R)\models ^s\lambda (k_1,\ldots ,k_n)$ iff $(s,(k_1)_R,\ldots ,(k_n)_R)\in \lambda _R$, for any $\lambda \in \varLambda _{n+1}$, $k_i\in Nom$, $i\in \{1,\ldots ,n\}$;

• $(\mathcal{M},R)\models ^s \rho$ iff $\mathcal{M}_s\models ^\mathtt {I}\rho$ for any $\rho \in {\mathbb Sen}^\mathtt {I}(\varSigma )$;

• $(\mathcal{M},R)\models ^s\rho _1\wedge \rho _2$ iff $(\mathcal{M},R)\models ^s\rho _1$ and $(\mathcal{M},R)\models ^s\rho _2$;

• $(\mathcal{M},R)\models ^s\rho _1\Rightarrow \rho _2$ iff $(\mathcal{M},R)\models ^s\rho _1$ implies $(\mathcal{M},R)\models ^s\rho _2$;

• $(\mathcal{M},R)\models ^s\lnot \rho$ iff $(\mathcal{M},R)\not \models ^s\rho$;

• $(\mathcal{M},R)\models ^s @_k \rho$ iff $(\mathcal{M},R)\models ^{k_R} \rho$;

• $(\mathcal{M},R)\models ^s[\lambda ](\rho _1,\ldots ,\rho _n)$ iff for every $(s,s_1,\ldots ,s_n)\in \lambda _R$, $(\mathcal{M},R)\models ^{s_i}\rho _i$ for some $i\in \{1,\ldots ,n\}$;

• $(\mathcal{M},R)\models ^s (\forall \chi )\rho$ iff for every expansion $(\mathcal{M}',R)$ along $\chi :(\varSigma ,Nom,\varLambda )\rightarrow (\varSigma ',Nom,\varLambda )$ we have $(\mathcal{M}',R)\models ^s\rho$;

• $(\mathcal{M},R)\models ^s (\forall J)\rho$ iff for every expansion $(\mathcal{M},R')$ along $\iota _J:(\varSigma ,Nom,\varLambda )\hookrightarrow (\varSigma ,Nom\cup J,\varLambda )$ we have $(\mathcal{M},R')\models ^s\rho$;

• $(\mathcal{M},R)\models ^s(\downarrow j)\rho$ iff $(\mathcal{M},R')\models ^s \rho$, where $(M\,R')$ is the expansion of $(\mathcal{M},R)$ along $\iota _j:(\varSigma ,Nom,\varLambda )\rightarrow (\varSigma ,Nom\cup \{ j \},\varLambda )$ such that $j_R=s$.

$\lambda (k_1,\ldots ,k_n)$ is introduced in this paper but a semantically equivalent sentence can be obtained by combining the remaining sentence operators. However, in certain fragments of hybrid logics the sentence operators are restricted making the present approach more useful. The sentence building operator @ is called retrieve since it changes the point of evaluation in the model. The sentence building operator $\downarrow$ is called store since it gives a name to the current state and it allows a reference to it. The global satisfaction holds when the satisfaction holds locally in all states, i.e. $(\mathcal{M},R)\models ^{\mathtt {HI}}\rho$ iff $(\mathcal{M},R)\models ^s\rho$ for all $s\in |R|$. Given a signature $\varDelta \in |{\mathbb Sig}^{\mathtt {HI}}|$ and two sets of sentences $\varGamma ,E\in {\mathbb Sen}^{\mathtt {HI}}(\varDelta )$, we write $\varGamma \models ^{\mathtt {HI}}E$ iff for all models $(\mathcal{M},R)\in |{\mathbb Mod}^{\mathtt {HI}}(\varDelta )|$ such that $(\mathcal{M},R)\models ^{\mathtt {HI}}\varGamma$ we have $(\mathcal{M},R)\models ^{\mathtt {HI}}E$. Note that variables may be interpreted differently across distinct worlds, which amounts to the world-line semantics of [14].

Satisfaction Condition. The satisfaction condition for hybrid institutions is a direct consequence of the following local satisfaction condition.

Theorem 2

[6]. Let $\varDelta =(\varSigma ,Nom,\varLambda )$ and $\varDelta '=({\mathbb Sig}',Nom',\varLambda ')$ be two ${\mathtt {HI}}$ signatures and $\varphi :\varDelta \rightarrow \varDelta '$ a signature morphism. For any $\rho \in {\mathbb Sen}^{\mathtt {HI}}(\varDelta )$, $(\mathcal{M},R')\in {\mathbb Mod}^{\mathtt {HI}}(\varDelta ')$ and $s\in |R'|$ we have

$${\mathbb Mod}^{\mathtt {HI}}(\varphi )(\mathcal{M}',R')\models ^s \rho \text{ iff } (\mathcal{M}',R')\models ^s {\mathbb Sen}^{\mathtt {HI}}(\varphi )(\rho )$$

The result of the hybridisation process is an institution.

Corollary 1

[6]. ${\mathtt {HI}}=({\mathbb Sig}^{\mathtt {HI}},{\mathbb Sen}^{\mathtt {HI}},{\mathbb Mod}^{\mathtt {HI}},\models ^{\mathtt {HI}})$ is an institution.

A myriad of examples of hybrid institutions may be generated by applying the construction described above to various parameters: (1) the base institution $\mathtt {I}$ together with the quantification category $\mathcal{Q}$, and (2) by considering different constrained model functors $({\mathbb Mod}^{\mathtt {CHI}}:{\mathbb Sig}^{\mathtt {CHI}}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T})$ for ${\mathtt {HI}}$.

Example 8

(Hybrid first-order logic (${\mathbf {HFOL}}$)). This institution is obtained by applying the hybridisation process to ${\mathbf {FOL}}$ with the quantification subcategory consisting of signature extensions with a finite number of variables.

Example 9

(Hybrid Propositional Logic (${\mathbf {HPL}}$)). This institution is obtained by applying the hybridisation process to ${\mathbf {PL}}$ with the quantification category consisting only of identity signature morphisms. In applications, the category ${\mathbb Sig}^{\mathbf {HPL}}$ is restricted to the full subcategory⁴ ${\mathbb Sig}^{{\mathbf {HPL}}'}$ which consists of signatures $(P,Nom,\varLambda )$, where P is a set of propositional variables, Nom is a set of nominals and $\varLambda$ is the family of modalities such that $\varLambda _2=\{\lambda \}$ and $\varLambda _n=\emptyset$ for all $n\ne 2$. In this case we denote $[\varLambda ]$ simply by $\Box$. Let ${\mathbf {HPL}}'=({\mathbb Sig}^{{\mathbf {HPL}}'},{\mathbb Sen}^{\mathbf {HPL}},{\mathbb Mod}^{\mathbf {HPL}},\models ^{\mathbf {HPL}})$.

Example 10

(Constrained Hybridisation). Let $\mathtt {I}=({\mathbb Sig},{\mathbb Sen},{\mathbb Mod},\models )$ be a base institution, and ${\mathbb Mod}^{\mathtt {CHI}}:{\mathbb Sig}^{\mathtt {CHI}}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ a constrained model functor for ${\mathtt {HI}}$. The constrained hybridised institution ${\mathtt {CHI}}=({\mathbb Sig}^{\mathtt {CHI}},{\mathbb Sen}^{\mathtt {CHI}},{\mathbb Mod}^{\mathtt {CHI}},\models ^{\mathtt {CHI}})$ is obtained similarly to the case of base institutions:

• (a) ${\mathbb Sen}^{\mathtt {CHI}}:{\mathbb Sig}^{\mathtt {CHI}}\rightarrow {\mathbb Set}$ is the restriction of ${\mathbb Sen}^{\mathtt {HI}}:{\mathbb Sig}^{\mathtt {HI}}\rightarrow {\mathbb Set}$ to ${\mathbb Sig}^{\mathtt {CHI}}$,

• (b) for each signature $\varDelta \in |{\mathbb Sig}^{\mathtt {CHI}}|$ and model $(\mathcal{M},R)\in |{\mathbb Mod}^{\mathtt {CHI}}(\varDelta )|$,

  $$(\mathcal{M},R)\models ^{\mathtt {CHI}}\rho \text{ iff } (\mathcal{M},R)\models ^s\rho \text{ for } \text{ all } s\in |R|.$$

Note that $(\mathcal{M},R)\models ^{\mathtt {HI}}\rho \text{ iff } (\mathcal{M},R)\models ^{\mathtt {CHI}}\rho$. Given a signature $\varDelta \in |{\mathbb Sig}^{\mathtt {CHI}}|$ and two sets of sentences $\varGamma ,E\in {\mathbb Sen}^{\mathtt {CHI}}(\varDelta )$, we write $\varGamma \models ^{\mathtt {CHI}}E$ iff for each model $(\mathcal{M},R)\in |{\mathbb Mod}^{\mathtt {CHI}}(\varDelta )|$ such that $(\mathcal{M},R)\models ^{\mathtt {CHI}}\varGamma$ we have $(\mathcal{M},R)\models ^{\mathtt {CHI}}E$.

Remark 1

$\varGamma \models ^{\mathtt {HI}}E$ implies $\varGamma \models ^{\mathtt {CHI}}E$ but the converse implication may not hold.

Example 11

(Injective Hybridisation). Let $\mathtt {I}=({\mathbb Sig}^\mathtt {I},{\mathbb Sen}^\mathtt {I},{\mathbb Mod}^\mathtt {I},\models ^\mathtt {I})$ be a base institution. The injective hybridisation $\mathtt {IHI}=({\mathbb Sig}^\mathtt {IHI},{\mathbb Sen}^\mathtt {IHI},{\mathbb Mod}^\mathtt {IHI},\models ^\mathtt {IHI})$ of the base institution $\mathtt {I}$ is a constrained hybridised institution obtained from ${\mathtt {HI}}=({\mathbb Sig}^{\mathtt {HI}},{\mathbb Sen}^{\mathtt {HI}},{\mathbb Mod}^{\mathtt {HI}},\models ^{\mathtt {HI}})$ and its constrained model functor ${\mathbb Mod}^\mathtt {IHI}:{\mathbb Sig}^\mathtt {IHI}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ that do not allow confusion among nominals: (a) ${\mathbb Sig}^\mathtt {IHI}$ is the broad subcategory of ${\mathbb Sig}^{\mathtt {HI}}$ consisting of signature morphisms injective on nominals, i.e. $\varphi _{\mathbb Nom}$ is injective for all $\varphi \in {\mathbb Sig}^\mathtt {IHI}$, and (b) ${\mathbb Mod}^\mathtt {IHI}(\varSigma ,Nom,\varLambda )$ is the full subcategory of ${\mathbb Mod}^{\mathtt {HI}}(\varSigma ,Nom,\varLambda )$ consisting of models that do not allow confusion among nominals, i.e. $j_R=k_R$ implies $j=k$ for all $j,k\in Nom$.

Our results are not applicable directly to hybrid institutions but rather to their restriction to models that do not allow confusion among nominals. The following results can be instantiated, for example, to the injective hybridisation of ${\mathbf {FOL}}$. However, when the quantification subcategory $\mathcal{Q}$ consists of identities (take for example ${\mathbf {PL}}$) then the semantic restriction of the hybridised logic is no longer required. This means that the following results are applicable to ${\mathbf {HPL}}$.

Example 12

(Quantifier-free Injective Hybridisation). The quantifier-free injective hybridisation ${\mathtt {QIHI}}=({\mathbb Sig}^\mathtt {IHI},{\mathbb Sen}^{\mathtt {QIHI}},{\mathbb Mod}^\mathtt {IHI},\models ^\mathtt {IHI})$ of a base institution $\mathtt {I}=({\mathbb Sig}^\mathtt {I},{\mathbb Sen}^\mathtt {I},{\mathbb Mod}^\mathtt {I},\models ^\mathtt {I})$ is obtained from the injective hybridisation $\mathtt {IHI}=({\mathbb Sig}^\mathtt {IHI},{\mathbb Sen}^\mathtt {IHI},{\mathbb Mod}^\mathtt {IHI},\models ^\mathtt {IHI})$ by restricting the syntax to quantifier-free sentences, i.e. for each $(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^\mathtt {IHI}|$ the set ${\mathbb Sen}^{\mathtt {QIHI}}(\varSigma ,Nom,\varLambda )$ consists of sentences obtained from nominal sentences (e.g. $k\in Nom$), hybrid relational atoms (e.g. $\lambda (k_1,\ldots ,k_n)\in {\mathbb Sen}^\mathtt {IHI}(\varSigma ,Nom,\varLambda )$) and the sentences in ${\mathbb Sen}(\varSigma )$ by applying Boolean connectives and the operator @. This institution is useful for defining hybrid substitutions that do not involve any form of quantification (see Sect. 3.1).

3.1 Hybrid Substitutions

We extend the notion of substitution from a base institution to its hybridisation. In this subsection we assume a base institution $\mathtt {I}=({\mathbb Sig},{\mathbb Sen},{\mathbb Mod},\models )$, a broad subcategory of signature morphisms $\mathcal{D}\subseteq {\mathbb Sig}$, and a substitution functor ${\mathbb Sub}:\mathcal{D}^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ for the base institution $\mathtt {I}$. Let $\mathcal{D}^{\mathtt {HI}}\subseteq {\mathbb Sig}^{\mathtt {HI}}$ be the broad subcategory of hybrid signature morphisms of the form $\varphi :(\varSigma ,Nom,\varLambda )\rightarrow (\varSigma _1,Nom,\varLambda )$ such that $\varSigma \mathop {\rightarrow }\limits ^{\varphi _{\mathbb Sig}}\varSigma _1\in \mathcal{D}$, $\varphi _{\mathbb Nom}=1_{Nom}$ and $\varphi _{\mathbb Rel}=1_\varLambda$.

Inherited Substitutions. Hybrid substitutions can be obtained from combinations of substitutions in the base institution. Let $(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^\mathtt {IHI}|$ be a signature and $\varTheta =\{\theta _k:(\varSigma \mathop {\rightarrow }\limits ^{\varphi _1}\varSigma _1)\rightarrow (\varSigma \mathop {\rightarrow }\limits ^{\varphi _2}\varSigma _2)\}_{k\in Nom}$ a family of substitutions in ${\mathbb Sub}$. On the syntactic side, $\varTheta$ determines a function

$$\varTheta ^k:{\mathbb Sen}^{{\mathtt {QIHI}}}(\varSigma _1,Nom,\varLambda )\rightarrow {\mathbb Sen}^{{\mathtt {QIHI}}}(\varSigma _2,Nom,\varLambda )$$

for each nominal $k\in Nom$:

• $\varTheta ^k(j)=j$, for all $j\in Nom$;

• $\varTheta ^k(\lambda (k_1,\ldots ,k_n))=\lambda (k_1,\ldots ,k_n)$ for all $\lambda \in \varLambda _{n+1}$ and $k_i\in Nom$;

• $\varTheta ^k(\rho )=\theta _k(\rho )$ for any $\rho \in {\mathbb Sen}^\mathtt {I}(\varSigma )$;

• $\varTheta ^k(\rho \star \rho ')=\varTheta ^k(\rho )\star \varTheta ^k(\rho ')$, $\star \in \{\wedge ,\Rightarrow \}$;

• $\varTheta ^k(\lnot \rho )=\lnot \varTheta ^k(\rho )$;

• $\varTheta ^k(@_j\rho )=\varTheta ^j(\rho )$;

Since ${\mathbb Sen}^\mathtt {I}(\varphi _1);{\mathbb Sen}(\theta _k)={\mathbb Sen}^\mathtt {I}(\varphi _2)$ for all nominals $k\in Nom$, the following result holds.

Lemma 2

The diagram below is commutative

for all nominals $k\in Nom$.

On the semantic side, $\varTheta$ determines a functor

$${\mathbb Mod}^{\mathtt {IHI}}(\varTheta ^k):{\mathbb Mod}^{\mathtt {IHI}}(\varSigma _2,Nom,\varLambda )\rightarrow {\mathbb Mod}^{\mathtt {IHI}}(\varSigma _1,Nom,\varLambda )$$

often denoted by $\_\!\upharpoonright \!_{\varTheta ^k}$ for all nominals $k\in Nom$:

• for every $(\mathcal{M}^2,R)\in |{\mathbb Mod}^\mathtt {IHI}(\varSigma _2,Nom,\varLambda )|$, $(\mathcal{M}^2,R)\!\upharpoonright \!_{\varTheta ^k} = (\mathcal{M}^2\!\upharpoonright \!_{\varTheta ^k},R)$, where $\mathcal{M}^2\!\upharpoonright \!_{\varTheta ^k}$ is defined by

  • $(\mathcal{M}^2\!\upharpoonright \!_{\varTheta ^k})_{j_R}=\mathcal{M}^2_{j_R}\!\upharpoonright \!_{\theta _j}$ for all nominals $j\in Nom$, and

  • $(\mathcal{M}^2\!\upharpoonright \!_{\varTheta ^k})_s=\mathcal{M}^2_s\!\upharpoonright \!_{\theta _k}$ for all $s\in (|R|- {Nom}_R$).

• for every $h^2:(\mathcal{M}^2,R)\rightarrow (\mathcal{N}^2,P)\in {\mathbb Mod}^{\mathtt {IHI}}(\varSigma _2,Nom,\varLambda )$ we have

  • $(h^2\!\upharpoonright \!_{\varTheta ^k})_{j_R}=h^2_{j_R}\!\upharpoonright \!_{\theta _j}$ for all nominals $j\in Nom$, and

  • $(h^2\!\upharpoonright \!_{\varTheta ^k})_s=h^2_s\!\upharpoonright \!_{\theta _k}$ for all $s\in (|R|-{Nom}_R)$.

The definition of $\_\!\upharpoonright \!_{\varTheta ^k}$ is consistent because no confusion of nominals is allowed inside of the models $(\mathcal{M}^2,R)$. Since ${\mathbb Mod}(\theta _k);{\mathbb Mod}^\mathtt {I}(\varphi _1)={\mathbb Mod}^\mathtt {I}(\varphi _2)$ for all nominals $k\in Nom$, the following result holds.

Lemma 3

The diagram below is commutative

for all nominals $k\in Nom$.

Next result can be regarded as the satisfaction condition for the substitutions inherited from the base institution.

Proposition 2

(Satisfaction Condition). Given a signature $(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {HI}}|$, for every model $(\mathcal{M}^2,R)\in {\mathbb Mod}^\mathtt {IHI}(\varSigma _2,Nom,\varLambda )$ and each sentence $\rho \in {\mathbb Sen}^{\mathtt {QIHI}}(\varSigma ,Nom,\varLambda )$

$$(\mathcal{M}^2,R)\models ^{k_R} \varTheta ^k(\rho ) \text{ iff } (\mathcal{M}^2,R)\!\upharpoonright \!_{\varTheta ^j} \models ^{k_R} \rho $$

for all nominals $j,k\in Nom$.

Proposition 2 stands at the basis of proving initiality and Herbrand’s theorem in hybrid logics where the variables may be interpreted differently across distinct worlds. The following is a corollary of Proposition 2 which allows one to infer new sentences from initial axioms by applying substitutions inherited from the base institution.

Corollary 2

Assume a signature $\varDelta =(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {IHI}}|$ and a hybrid substitution $\varTheta =\{\theta _j:(\varSigma \mathop {\rightarrow }\limits ^{\varphi _1}\varSigma _1)\rightarrow (\varSigma \mathop {\rightarrow }\limits ^{\varphi _2}\varSigma _2)\}_{j\in Nom}$. For all sentences $\rho \in {\mathbb Sen}^{\mathtt {QIHI}}(\varDelta )$ $\rho$ we have

$$(\forall \varphi _1)\rho \models ^{\mathtt {IHI}} @_k(\forall \varphi _2)\varTheta ^k(\rho )$$

for all nominals $k\in Nom$.

Nominal Substitutions. Nominal substitutions are captured by the notion of signature morphisms in the hybridised institution. Let $\iota _j:(\varSigma ,Nom,\varLambda )\hookrightarrow (\varSigma ,Nom\cup \{j\},\varLambda )$ be a signature extension with the nominal variable j. A nominal substitution is represented by a function $\varphi _{\mathbb Nom}:\{j\}\rightarrow Nom$ which can be canonically extended to a signature morphism $\varphi :(\varSigma ,Nom\cup \{j\},\varLambda )\rightarrow (\varSigma ,Nom,\varLambda )$. The following result is a consequence of the satisfaction condition for the hybridised institution.

Lemma 4

Let $(\forall j)\rho \in {\mathbb Sen}^{\mathtt {HI}}(\varSigma ,Nom,\varLambda )$ and $k\in Nom$.

• (1) $(\forall j)\rho \models ^{\mathtt {HI}}\rho [j\leftarrow k]$; moreover, $(\mathcal{M},R)\models ^s (\forall j)\rho$ implies $(M,R)\models ^s \rho [j\leftarrow k]$ for all models $(\mathcal{M},R)\in |{\mathbb Mod}^{\mathtt {HI}}(\varSigma ,Nom,\varLambda )|$ and states $s\in |R|$;

• (2) $(\downarrow j)\rho \models ^{\mathtt {HI}}@_k \rho [j\leftarrow k]$.⁵

3.2 Reachable Hybrid Models

In this subsection we extend the notion of reachability to hybrid institutions. Let $\mathtt {I}=({\mathbb Sig},{\mathbb Sen},{\mathbb Mod},\models )$ be a base institution, $\mathcal{D}\subseteq {\mathbb Sig}$ a broad subcategory of signature morphisms, and ${\mathbb Sub}:\mathcal{D}^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ a substitution functor for $\mathtt {I}$.

Definition 4

A model $(\mathcal{M},R)\in |{\mathbb Mod}^{\mathtt {HI}}(\varSigma ,Nom,\varLambda )|$, where $(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {HI}}|$, is ${\mathbb Sub}$-reachable if (a) $|R|=Nom_R$, where $Nom_R=\{k_R\mid k\in Nom\}$, and (b) $\mathcal{M}_{k_R}$ is ${\mathbb Sub}$-reachable in $\mathtt {I}$ for all nominals $k\in Nom$.

In the injective hybridisation, the expansions of reachable models along signature morphisms in $\mathcal{D}^{\mathtt {HI}}$ generate hybrid substitutions.

Proposition 3

Given a signature $(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {HI}}|$ and a ${\mathbb Sub}$-reachable model $(\mathcal{M},R)\in |{\mathbb Mod}^\mathtt {IHI}(\varSigma ,Nom,\varLambda )|$ then for every signature morphism $\chi :(\varSigma ,Nom,\varLambda )\rightarrow (\varSigma ',Nom,\varLambda )$ with $\varSigma \mathop {\rightarrow }\limits ^{\chi }\varSigma '\in \mathcal{D}$ and each $\chi$-expansion $(\mathcal{M}',R)$ of $(\mathcal{M},R)$ there exists a hybrid substitution $\varTheta =\{\chi \mathop {\rightarrow }\limits ^{\theta _k}1_\varSigma \}_{k\in Nom}$ such that $(\mathcal{M},R)\!\upharpoonright \!_{\varTheta ^j}=(\mathcal{M}',R)$ for all nominals $j\in Nom$.

This definition of reachability is used in the context of injective hybridisations and their constrained sub-institutions.

4 Initiality

The following results on the existence of initial models depend on multiple parameters that can be instantiated in the same context in many ways producing different results. We will focus largely on parameter instantiation of the abstract theorems to concrete hybrid logical systems to obtain the desired applications. However, the interested reader may find other useful applications as well. In this section we assume a base institution $\mathtt {I}=({\mathbb Sig}^\mathtt {I},{\mathbb Sen}^\mathtt {I},{\mathbb Mod}^\mathtt {I},\models ^\mathtt {I})$, a broad subcategory $\mathcal{D}\subseteq {\mathbb Sig}$ of signature morphisms and a substitution functor ${\mathbb Sub}:\mathcal{D}^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ for the base institution $\mathtt {I}$.

4.1 Basic Hybrid Sentences

In addition to the assumptions made at the beginning of this section, let us consider a sub-functor $({\mathbb Sen}^\mathtt {I}_0:{\mathbb Sig}\rightarrow {\mathbb Set})$ of ${\mathbb Sen}^\mathtt {I}$. We define the sentence functor $({\mathbb Sen}^{\mathtt {HI}}_0:{\mathbb Sig}^{\mathtt {HI}}\rightarrow {\mathbb Set})$ of ${\mathbb Sen}^{\mathtt {HI}}$ for each signature $(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {HI}}|$,

• (1) $@_j k\in {\mathbb Sen}^{\mathtt {HI}}_0(\varSigma ,Nom,\varLambda )$ for all $j,k\in Nom$,

• (2) $@_j \lambda (k_1,\ldots ,k_n)\in {\mathbb Sen}^{\mathtt {HI}}_0(\varSigma ,Nom,\varLambda )$ for all $\lambda \in \varLambda _{n+1}$, $j\in Nom$ and $k_i\in Nom$,

• (3) $@_j\rho \in {\mathbb Sen}^{\mathtt {HI}}_0(\varSigma ,Nom,\varLambda )$ for all $j\in Nom$ and $\rho \in {\mathbb Sen}^\mathtt {I}_0(\varSigma )$.

In concrete examples of institutions, $\mathtt {I}_0=({\mathbb Sig}^\mathtt {I},{\mathbb Sen}^\mathtt {I}_0,{\mathbb Mod}^\mathtt {I},\models ^\mathtt {I})$ is the restriction of the base institution to atomic sentences, and the institution ${\mathtt {HI}}_0=({\mathbb Sig}^{\mathtt {HI}},{\mathbb Sen}^{\mathtt {HI}}_0,{\mathbb Mod}^{\mathtt {HI}},\models ^{\mathtt {HI}})$ gives the building bricks for constructing theories that have initial models in the hybridised institution.

Theorem 3

If every set of sentences of $\mathtt {I}_0$ is epi basic then every set of sentences of ${\mathtt {HI}}_0$ is epi basic. Moreover, if each set of sentences of $\mathtt {I}_0$ has a basic model that is ${\mathbb Sub}$-reachable then each set of sentences of ${\mathtt {HI}}_0$ has a basic model that is ${\mathbb Sub}$-reachable.

We apply Theorem 3 to ${\mathbf {HFOL}}$. Let ${\mathbb Sen}^{\mathbf {FOL}}_0:{\mathbb Sig}^{\mathbf {FOL}}\rightarrow {\mathbb Set}$ be the sub-functor of ${\mathbb Sen}^{\mathbf {FOL}}$ such that for any signature $\varSigma \in |{\mathbb Sig}^{\mathbf {FOL}}|$ the set ${\mathbb Sen}^{\mathbf {FOL}}_0(\varSigma )$ consists of atoms. We define ${\mathbf {FOL}}_0=({\mathbb Sig}^{\mathbf {FOL}},{\mathbb Sen}^{\mathbf {FOL}}_0,{\mathbb Mod}^{\mathbf {FOL}},\models ^{\mathbf {FOL}})$ and ${\mathbf {HFOL}}_0=({\mathbb Sig}^{\mathbf {HFOL}},{\mathbb Sen}^{\mathbf {HFOL}}_0,{\mathbb Mod}^{\mathbf {HFOL}},$ $\models ^{\mathbf {HFOL}})$ using the general pattern described above.

Corollary 3

All sets of ${\mathbf {HFOL}}_0$ sentences are epi basic and the corresponding basic models are ${\mathbb Sub}^{\mathbf {FOL}}$-reachable.

Proof

By Lemma 1, any set of ${\mathbf {FOL}}$ atoms is epi basic. By Proposition 1, the corresponding basic models are ${\mathbb Sub}^{\mathbf {FOL}}$-reachable. By Theorem 3, any set of ${\mathbf {HFOL}}_0$ sentences is epi basic and the corresponding basic models are ${\mathbb Sub}^{\mathbf {FOL}}$-reachable.    $\square$

We return to the general setting and we define the sub-functor $({\mathbb Sen}^\mathtt {IHI}_0:{\mathbb Sig}^\mathtt {IHI}\rightarrow {\mathbb Set})$ of ${\mathbb Sen}^\mathtt {IHI}$ for each signature $(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {HI}}|$,

• (1) $@_j \lambda (k_1,\ldots ,k_n)\in {\mathbb Sen}^\mathtt {IHI}_0(\varSigma ,Nom,\varLambda )$ for any $\lambda \in \varLambda _{n+1}$, $j\in Nom$ and $k_i\in Nom$,

• (2) $@_j\rho \in {\mathbb Sen}^\mathtt {IHI}_0(\varSigma ,Nom,\varLambda )$ for any $j\in Nom$ and $\rho \in {\mathbb Sen}^\mathtt {I}_0(\varSigma )$.

The institution $\mathtt {IHI}_0=({\mathbb Sig}^\mathtt {IHI},{\mathbb Sen}^\mathtt {IHI}_0,{\mathbb Mod}^\mathtt {IHI},\models ^\mathtt {IHI})$ gives the building bricks for constructing theories that have initial models in the injective hybridisation.

Theorem 4

If every set of sentences of $\mathtt {I}_0$ is epi basic then every set of sentences of $\mathtt {IHI}_0$ is epi basic. Moreover, if each set of sentences of $\mathtt {I}_0$ has a basic model that is ${\mathbb Sub}$-reachable then each set of sentences of $\mathtt {IHI}_0$ has a basic model that is ${\mathbb Sub}$-reachable.

We apply Theorem 4 to ${\mathbf {IHFOL}}$. Using the general pattern described above, let us define ${\mathbf {IHFOL}}_0=({\mathbb Sig}^{\mathbf {IHFOL}},{\mathbb Sen}^{\mathbf {IHFOL}}_0,{\mathbb Mod}^{\mathbf {IHFOL}},\models ^{\mathbf {IHFOL}})$ as the injective hybridisation of ${\mathbf {FOL}}$.

Corollary 4

All sets of ${\mathbf {IHFOL}}_0$ sentences are epi basic and the corresponding basic models are ${\mathbb Sub}^{\mathbf {FOL}}$-reachable.

Proof

By Lemma 1, any set of atoms in ${\mathbf {FOL}}$ is epi basic. By Proposition 1, the corresponding basic models are ${\mathbb Sub}^{\mathbf {FOL}}$-reachable. By Theorem 4, any set of sentences in ${\mathbf {HFOL}}_0$ is epi basic and the corresponding basic models are ${\mathbb Sub}^{\mathbf {FOL}}$-reachable.    $\square$

In the next subsections we prove that the initiality property is closed under the following sentence building operators: logical implication $\Rightarrow$, universal quantification $\forall$, store $\downarrow$, and box $\Box$.

4.2 Implication

In addition to the assumptions made at the beginning of this section, let us consider a constrained model functor ${\mathbb Mod}^{\mathtt {CHI}}:{\mathbb Sig}^{\mathtt {CHI}}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ for ${\mathtt {HI}}$, and three sub-functors $({\mathbb Sen}^{\mathtt {CHI}}_*:{\mathbb Sig}^{\mathtt {CHI}}\rightarrow {\mathbb Set})$, $({\mathbb Sen}^{\mathtt {CHI}}_\bullet :{\mathbb Sig}^{\mathtt {CHI}}\rightarrow {\mathbb Set})$ and $({\mathbb Sen}^{\mathtt {CHI}}_1:{\mathbb Sig}^{\mathtt {CHI}}\rightarrow {\mathbb Set})$ of ${\mathbb Sen}^{\mathtt {CHI}}$ such that any sentence of ${\mathbb Sen}^{\mathtt {CHI}}_1(\varDelta )$, where $\varDelta \in |{\mathbb Sig}^{\mathtt {CHI}}|$, is semantically equivalent in ${\mathtt {CHI}}$ to a sentence of the form $\bigwedge H\Rightarrow C$, where $H\subseteq {\mathbb Sen}^{\mathtt {CHI}}_*(\varDelta )$ and $C\in {\mathbb Sen}^{\mathtt {CHI}}_\bullet (\varDelta )$.

Theorem 5

If for each signature $\varDelta \in |{\mathbb Sig}^{\mathtt {CHI}}|$,

• (1) any set $B\subseteq {\mathbb Sen}^{\mathtt {CHI}}_*(\varDelta )$ is basic in ${\mathtt {HI}}$,⁶ and

• (2) any set $\varGamma \subseteq {\mathbb Sen}^{\mathtt {CHI}}_\bullet (\varDelta )$ has an initial ${\mathbb Sub}$-reachable model $(\mathcal{M}^\varGamma ,R^\varGamma )\in |{\mathbb Mod}^{\mathtt {CHI}}(\varDelta )|$,

then any set of sentences of the institution ${\mathtt {CHI}}_1=({\mathbb Sig}^{\mathtt {CHI}},{\mathbb Sen}^{\mathtt {CHI}}_1,{\mathbb Mod}^{\mathtt {CHI}},\models ^{\mathtt {CHI}})$ has an initial ${\mathbb Sub}$-reachable model.

We apply Theorem 5 to ${\mathbf {HFOL}}$. The constrained model functor ${\mathbb Mod}^{\mathtt {CHI}}$ is ${\mathbb Mod}^{\mathbf {HFOL}}:{\mathbb Sig}^{\mathbf {HFOL}}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$. The functors ${\mathbb Sen}^{\mathtt {CHI}}_*$ and ${\mathbb Sen}^{\mathtt {CHI}}_\bullet$ are both instantiated to ${\mathbb Sen}^{\mathbf {HFOL}}_0:{\mathbb Sig}^{\mathbf {HFOL}}\rightarrow {\mathbb Set}$. The institution ${\mathtt {CHI}}_1$ is ${\mathbf {HFOL}}_1$, the restriction of ${\mathbf {HFOL}}$ to sentences of the form $\bigwedge H\Rightarrow C$, where $H\cup \{C\}$ is a set of ${\mathbf {HFOL}}_0$ sentences.

Corollary 5

Any set of ${\mathbf {HFOL}}_1$ sentences has an initial ${\mathbb Sub}^{\mathbf {FOL}}$-reachable model.

We apply Theorem 5 to ${\mathbf {IHFOL}}$. The institution ${\mathtt {CHI}}$ is ${\mathbf {IHFOL}}$. The functor ${\mathbb Sen}^{\mathtt {CHI}}_*$ is the restriction of $({\mathbb Sen}^{\mathbf {HFOL}}_0:{\mathbb Sig}^{\mathbf {HFOL}}\rightarrow {\mathbb Set})$ to ${\mathbb Sig}^{\mathbf {IHFOL}}$. The functor ${\mathbb Sen}^{\mathtt {CHI}}_\bullet$ is $({\mathbb Sen}^{\mathbf {IHFOL}}_0:{\mathbb Sig}^{\mathbf {IHFOL}}\rightarrow {\mathbb Set})$. The sentence functor ${\mathbb Sen}^{\mathtt {CHI}}_1$ is $({\mathbb Sen}^{\mathbf {IHFOL}}_1:{\mathbb Sig}^{\mathbf {IHFOL}}\rightarrow {\mathbb Set})$ such that for all $\varDelta \in |{\mathbb Sig}^{\mathbf {IHFOL}}|$ the set ${\mathbb Sen}^{\mathbf {IHFOL}}_1(\varDelta )$ consists of sentences of the form $\bigwedge H\Rightarrow C$, where $H\subseteq {\mathbb Sen}^{\mathbf {HFOL}}_0(\varDelta )$ and $C\in {\mathbb Sen}^{\mathbf {IHFOL}}_0(\varDelta )$.

Corollary 6

Any set of ${\mathbf {IHFOL}}_1$ sentences has an initial ${\mathbb Sub}^{\mathbf {FOL}}$-reachable model, where ${\mathbf {IHFOL}}_1=({\mathbb Sig}^{\mathbf {IHFOL}},{\mathbb Sen}^{\mathbf {IHFOL}}_1,{\mathbb Mod}^{\mathbf {IHFOL}},\models ^{\mathbf {IHFOL}})$.

4.3 Nominal Quantification

In addition to the assumptions made at the beginning of this section, let us consider a constrained model functor ${\mathbb Mod}^{\mathtt {CHI}}:{\mathbb Sig}^{\mathtt {CHI}}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ for ${\mathtt {HI}}$, and two sub-functors $({\mathbb Sen}^{\mathtt {CHI}}_1:{\mathbb Sig}^{\mathtt {CHI}}\rightarrow {\mathbb Set})$ and $({\mathbb Sen}^{\mathtt {CHI}}_2:{\mathbb Sig}^{\mathtt {CHI}}\rightarrow {\mathbb Set})$ of ${\mathbb Sen}^{\mathtt {CHI}}$ such that all sentences of ${\mathtt {CHI}}_2=({\mathbb Sig}^{\mathtt {CHI}},{\mathbb Sen}^{\mathtt {CHI}}_2,{\mathbb Mod}^{\mathtt {CHI}},\models ^{\mathtt {CHI}})$ are semantically equivalent in ${\mathtt {CHI}}$ to a sentence of the form $(\forall j)\rho$, where j is a nominal variable and $\rho$ is a sentence of ${\mathtt {CHI}}_1=({\mathbb Sig}^{\mathtt {CHI}},{\mathbb Sen}^{\mathtt {CHI}}_1,{\mathbb Mod}^{\mathtt {CHI}},\models ^{\mathtt {CHI}})$.

Theorem 6

If every set of sentences of ${\mathtt {CHI}}_1$ has an initial ${\mathbb Sub}$-reachable model then each set of sentences of ${\mathtt {CHI}}_2$ has an initial ${\mathbb Sub}$-reachable model.

The following result is essential for applying Theorem 6 to concrete examples of institutions.

Lemma 5

In the institution ${\mathtt {CHI}}$, any sentence $\bigwedge H\Rightarrow C$ is semantically equivalent to $(\forall j) \bigwedge \{@_j h\mid h\in H\}\Rightarrow @_j C$, and any sentence $@_j@_k \rho$ is semantically equivalent to $@_k\rho$.

We apply Theorem 6 on top of ${\mathbf {HFOL}}_1$ defined in Subsect. 4.2. The institution ${\mathtt {CHI}}$ is ${\mathbf {HFOL}}$, and the institution ${\mathtt {CHI}}_1$ is ${\mathbf {HFOL}}_1$. The sentence functor ${\mathbb Sen}^{\mathtt {CHI}}_2$ is $({\mathbb Sen}^{\mathbf {HFOL}}_2:{\mathbb Sig}^{\mathbf {HFOL}}\rightarrow {\mathbb Set})$ which associates to each signature $\varDelta =(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathbf {HFOL}}|$ the set of sentences of the form $\bigwedge H\Rightarrow C$, where $H\cup \{C\}$ consists of sentences obtained from nominal sentences (e.g. $k\in Nom$), hybrid relational atoms (e.g. $\lambda (k_1,\ldots ,k_n)\in {\mathbb Sen}^{\mathbf {IHFOL}}(\varDelta )$) and ${\mathbf {FOL}}$ atoms (e.g. $t_1=t_2\in {\mathbb Sen}^{\mathbf {FOL}}_0(\varSigma )$ and $\pi (t_1,\ldots ,t_n)\in {\mathbb Sen}^{\mathbf {FOL}}_0(\varSigma )$) by applying the sentence building operator @.⁷

Corollary 7

Any set of sentences in ${\mathbf {HFOL}}_2$ has an initial ${\mathbb Sub}^{\mathbf {FOL}}$-reachable model.

Proof

By Lemma 5, any sentence in ${\mathbf {HFOL}}_2$ is semantically equivalent to a sentence of the form $(\forall j)\rho$, where j is a nominal variable and $\rho$ is a sentence of ${\mathbf {HFOL}}_1$. By Corollary 6, any set of sentences in ${\mathbf {HFOL}}_1$ has an initial ${\mathbb Sub}^{\mathbf {FOL}}$-reachable model. By Theorem 6, any set of sentences in ${\mathbf {HFOL}}_2$ has an initial ${\mathbb Sub}^{\mathbf {FOL}}$-reachable model.    $\square$

We apply Theorem 6 on top of ${\mathbf {HFOL}}_2$. Let ${\mathbf {HFOL}}_3$ be the institution obtained from ${\mathbf {HFOL}}$ by restricting the syntax to sentences of the form $(\forall J)\rho$, where J is a finite set of nominal variables and $\rho$ is a quantifier-free sentence of ${\mathbf {HFOL}}_2$.

Corollary 8

Any set of ${\mathbf {HFOL}}_3$ sentences has an initial ${\mathbb Sub}^{\mathbf {FOL}}$-reachable model.

We call the ${\mathbf {HFOL}}_3$ sentences hybrid Horn clauses of the institution ${\mathbf {HFOL}}$. Since ${\mathbf {PL}}$ is obtained from ${\mathbf {FOL}}$ by restricting the category of signatures, Corollary 8 holds also for ${\mathbf {HPL}}$. We apply Theorem 6 on top of ${\mathbf {IHFOL}}_1$ defined in Subsect. 4.2. The sentence functor ${\mathbb Sen}^{\mathtt {CHI}}_1$ is $({\mathbb Sen}^{\mathbf {IHFOL}}_1:{\mathbb Sig}^{\mathbf {IHFOL}}\rightarrow {\mathbb Set})$. The functor ${\mathbb Sen}^{\mathtt {CHI}}_2$ is $({\mathbb Sen}^{\mathbf {IHFOL}}_2:{\mathbb Sig}^{\mathbf {IHFOL}}\rightarrow {\mathbb Set})$ which associates to each signature the set of sentences of the form $\bigwedge H\Rightarrow C$, where

• (a) H consists of sentences obtained from nominal sentences, hybrid relational atoms, and ${\mathbf {FOL}}$ atoms by applying the sentence building operator @, and

• (b) C is a sentence obtained from hybrid relational atoms and ${\mathbf {FOL}}$ atoms by applying @.

Corollary 9

Any set of sentences in ${\mathbf {IHFOL}}_2$ has an initial ${\mathbb Sub}^{\mathbf {FOL}}$-reachable model.

Another application of Theorem 6 can be found in Subsect. 4.4.

4.4 Inherited Quantification

In addition to the assumptions made at the beginning of this section, let us consider a constrained model functor ${\mathbb Mod}^{\mathtt {CIHI}}:{\mathbb Sig}^{\mathtt {CIHI}}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ for the injective hybridisation $\mathtt {IHI}$, a quantification subcategory $\mathcal{Q}\subseteq \mathcal{D}$, and two sub-functors $({\mathbb Sen}^{\mathtt {CIHI}}_2:{\mathbb Sig}^{\mathtt {CIHI}}\rightarrow {\mathbb Set})$ and $({\mathbb Sen}^{\mathtt {CIHI}}_3:{\mathbb Sig}^{\mathtt {CIHI}}\rightarrow {\mathbb Set})$ of ${\mathbb Sen}^{\mathtt {CIHI}}$ such that

• (1) the sentences of ${\mathtt {CIHI}}_2=({\mathbb Sig}^{\mathtt {CIHI}},{\mathbb Sen}^{\mathtt {CIHI}}_2,{\mathbb Mod}^{\mathtt {CIHI}},\models ^{\mathtt {CIHI}})$ are semantically closed to @, i.e. for all $\varDelta \in |{\mathbb Sig}^{\mathtt {CIHI}}|$, $k\in Nom$ and $\rho \in {\mathbb Sen}^{\mathtt {CIHI}}_2(\varDelta )$ there exists $\varepsilon \in {\mathbb Sen}^{\mathtt {CIHI}}_2(\varDelta )$ such that $@_k\rho \mathrel {\models \!\!\!|}^{\mathtt {CIHI}}\varepsilon$,

• (2) In ${\mathtt {CIHI}}$, any sentence of ${\mathbb Sen}_3(\varSigma ,Nom,\varLambda )$, where $(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {CIHI}}|$, is semantically equivalent to a sentence of $(\forall \chi )\rho$, where $(\varSigma ,Nom,\varLambda )\mathop {\rightarrow }\limits ^{\chi }(\varSigma ',Nom,\varLambda )\in \mathcal{Q}^{\mathtt {HI}}$ and $\rho \in {\mathbb Sen}^{\mathtt {CIHI}}_2(\varSigma ',Nom,\varLambda )$,

• (3) for any $(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {CIHI}}|$ and $\varSigma \mathop {\rightarrow }\limits ^{\chi }\varSigma '\in \mathcal{D}$ we have $(\varSigma ',Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {CIHI}}|$, and

• (4) for any hybrid substitution $\varTheta =\{(\varSigma \mathop {\rightarrow }\limits ^{\chi _1}\varSigma _1)\mathop {\rightarrow }\limits ^{\theta _k}(\varSigma \mathop {\rightarrow }\limits ^{\chi _2}\varSigma _2)\}_{k\in Nom}$ and sentence $\rho \in {\mathbb Sen}^{\mathtt {CIHI}}_2(\varSigma _1,Nom,\varLambda )$ we have $\varTheta ^k(\rho )\in {\mathbb Sen}^{\mathtt {CIHI}}_2(\varSigma _2,Nom,\varLambda )$.

Theorem 7

If every set of sentences of ${\mathtt {CIHI}}_2$ has an initial ${\mathbb Sub}$-reachable model then each set of sentences of ${\mathtt {CIHI}}_3$ has an initial ${\mathbb Sub}$-reachable model.

We apply Theorem 7 on top of ${\mathbf {IHFOL}}_2$ defined in Subsect. 4.3. The institution ${\mathtt {CIHI}}$ is ${\mathbf {IHFOL}}$, and the institution ${\mathtt {CIHI}}_2$ is ${\mathbf {IHFOL}}_2$. Note that ${\mathbf {IHFOL}}_2$ is closed to @, which means that assumption (1) of this subsection holds. The institution ${\mathtt {CIHI}}_3$ is ${\mathbf {IHFOL}}_3$, the restriction of ${\mathbf {IHFOL}}$ to sentences of the form $(\forall X)\rho$, where X is a finite set of first-order variables and $\rho$ is a sentence in ${\mathbf {IHFOL}}_2$.⁸ This implies that assumption (2) of this subsection holds. Since $\mathcal{D}^{\mathtt {HI}}\subseteq {\mathbb Sig}^{\mathbf {IHFOL}}$, assumption (3) of this subsection holds. All sentences of ${\mathbf {IHFOL}}_2$ are quantifier-free and modal-free, and by applying a hybrid substitution to a ${\mathbf {IHFOL}}_2$ sentence, the result is also a ${\mathbf {IHFOL}}_2$ sentence. It follows that assumption (4) of this subsection holds.

Corollary 10

Any set of ${\mathbf {IHFOL}}_3$ sentences has an initial ${\mathbb Sub}^{\mathbf {FOL}}$-reachable model.

We apply Theorem 6 on top of the institution ${\mathbf {IHFOL}}_3$ defined above. Let ${\mathbf {IHFOL}}_4$ be the institution obtained from ${\mathbf {IHFOL}}$ by restricting the syntax to sentences of the form $(\forall J)\rho$, where J is a finite set of nominal variables and $\rho$ is a sentence of ${\mathbf {IHFOL}}_3$.

Corollary 11

Every set of ${\mathbf {IHFOL}}_4$ sentences has an initial ${\mathbb Sub}^{\mathbf {FOL}}$-reachable model.

We call the ${\mathbf {IHFOL}}_4$ sentences hybrid Horn clauses of the institution ${\mathbf {IHFOL}}$. Defining a paramodulation procedure for ${\mathbf {IHFOL}}_4$ is future research. However, the results obtained in this paper set the foundation for this direction of research.

Any sentence of the form $(\downarrow j)\rho$ is semantically equivalent to $(\forall j)j\Rightarrow \rho$. It follows that initiality is closed under store $\downarrow$. If $\lambda \in \varLambda _2$ then $[\lambda ](\rho )$ is semantically equivalent to $(\forall k)\lambda (k)\Rightarrow @_k\rho$. It follows that initiality is closed under box $\Box$ when $\varLambda _n=\emptyset$ for all $n\ne 2$.

5 Herbrand’s Theorem

We prove a version of Herbrand’s theorem in the framework of hybrid institutions.

Theorem 8

Let $\mathtt {I}=({\mathbb Sig},{\mathbb Sen},{\mathbb Mod},\models )$ be an institution, $\mathcal{D}\subseteq {\mathbb Sig}$ a broad subcategory of signature morphisms, ${\mathbb Sub}:\mathcal{D}^{op}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ a substitution functor for $\mathtt {I}$ and $\mathcal{Q}\subseteq \mathcal{D}$ a quantification subcategory. Consider a constrained model functor ${\mathbb Mod}^{\mathtt {CIHI}}:{\mathbb Sig}^{\mathtt {CIHI}}\rightarrow \mathbb {C}\mathbb {A}\mathbb {T}$ for the injective hybridisation $\mathtt {IHI}$ such that

• (1) for any $(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {CIHI}}|$ and $\varSigma \mathop {\rightarrow }\limits ^{\chi }\varSigma '\in \mathcal{D}$ we have $(\varSigma ',Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {CIHI}}|$.

Assume a sub-functor $({\mathbb Sen}_b^{\mathtt {CIHI}}:{\mathbb Sig}^{\mathtt {CIHI}}\rightarrow {\mathbb Set})$ of ${\mathbb Sen}^{\mathtt {CIHI}}$ such that

• (2) any $B\subseteq {\mathbb Sen}^{\mathtt {CIHI}}_b(\varSigma ,Nom,\varLambda )$ is basic in ${\mathtt {HI}}$, where $(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {CIHI}}|$.

Let $\varDelta =(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathtt {CIHI}}|$ be a signature, $k\in Nom$ a nominal, $\varGamma \subseteq {\mathbb Sen}^{\mathtt {CIHI}}(\varDelta )$ a set of sentences that has an initial ${\mathbb Sub}$-reachable model $(\mathcal{M}^\varGamma ,R^\varGamma )\in |{\mathbb Mod}^{\mathtt {CIHI}}(\varDelta )|$, and $(\exists J)(\exists \chi )\rho \in {\mathbb Sen}^{\mathtt {CIHI}}(\varDelta )$ a sentence such that (a) J is a set of nominal variables, (b) $\varDelta \mathop {\rightarrow }\limits ^{\chi }\varDelta '\in \mathcal{Q}^{\mathtt {HI}}$ with $\varDelta '=(\varSigma ',Nom,\varLambda )$, and (c) $\rho \in {\mathbb Sen}^{\mathtt {CIHI}}_b(\varDelta '[J])$ with $\varDelta '[J]=(\varSigma ',Nom\cup J,\varLambda )$. Then the following statements are equivalent:

• (i) $\varGamma \models ^{\mathtt {CIHI}}@_k(\exists J)(\exists \chi )\rho$,

• (ii) $(\mathcal{M}^\varGamma ,R^\varGamma )\models ^{{k_{(R^\varGamma )}}}(\exists J)(\exists \chi ) \rho$,

• (iii) there is a hybrid substitution $\varTheta =\{\theta _j:(\varSigma \mathop {\rightarrow }\limits ^{\chi }\varSigma ')\rightarrow (\varSigma \mathop {\rightarrow }\limits ^{\varphi }\varSigma '')\}_{j\in Nom}$ and a nominal substitution $\psi :J\rightarrow Nom$ such that $\varGamma \models ^{\mathtt {CIHI}}@_k(\forall \varphi )\varTheta ^k(\psi (\rho ))$ and $\varphi :(\varSigma ,Nom,\varLambda )\rightarrow (\varSigma '',Nom,\varLambda )$ is conservative in ${\mathtt {CIHI}}$.

The pair of substitutions $\langle \psi ,\varTheta \rangle$ from the statement (iii) of Theorem 8 are called solutions. The sentence $@_k(\exists J)(\exists \chi )\rho$ is a query. The implication $(i)~\Rightarrow ~(iii)$ reduces the satisfiability of a query by a program (represented here by a hybrid theory) to the search of a pair of substitutions, while the converse implication $(iii) \Rightarrow (i)$ shows that solutions are sound with respect to the given program. We apply Theorem 8 to ${\mathbf {IHFOL}}$. Since $\mathcal{D}^{\mathbf {HFOL}}\subseteq {\mathbb Sig}^{\mathbf {IHFOL}}$ the second hypothesis holds. The functor ${\mathbb Sen}^{\mathtt {CIHI}}_b$ is $({\mathbb Sen}^{\mathbf {IHFOL}}_b:{\mathbb Sig}^{\mathbf {IHFOL}}\rightarrow {\mathbb Set})$ such that for each $(\varSigma ,Nom,\varLambda )\in |{\mathbb Sig}^{\mathbf {IHFOL}}|$ the set ${\mathbb Sen}^{\mathbf {IHFOL}}_b(\varSigma ,Nom,\varLambda )$ consists of finite conjunctions of sentences in ${\mathbb Sen}^{\mathbf {HFOL}}_0(\varSigma ,Nom,\varLambda )$. By Corollary 3, any set of sentences in ${\mathbf {HFOL}}_0$ is epi basic in ${\mathbf {HFOL}}$, which implies that any conjunction of sentences in ${\mathbf {HFOL}}_0$ is also epi basic in ${\mathbf {HFOL}}$. It follows that condition (2) of Theorem 8 holds. By Corollary 11, any set of hybrid Horn clauses in ${\mathbf {IHFOL}}_4$ has an initial model. Note that for any nominal k, we have $(\exists J)(\exists X)\rho \mathrel {\models \!\!\!|}^{\mathbf {HFOL}}@_k (\exists J)(\exists X)\rho$, which implies $(\exists J)(\exists X)\rho \mathrel {\models \!\!\!|}^{\mathbf {IHFOL}}@_k (\exists J)(\exists X)\rho$. In ${\mathbf {IHFOL}}$, the queries are sentences of the form $(\exists J)(\exists X)\rho$, where $\rho$ is a finite conjunction of ${\mathbf {HFOL}}_0$ sentences.

Corollary 12

For any set of sentences $\varGamma \subseteq {\mathbb Sen}^{{\mathbf {IHFOL}}_4}((S,F,P),Nom,\varLambda )$, where $((S,F,P),Nom,\varLambda )\in |{\mathbb Sig}^{\mathbf {IHFOL}}|$, and any query $(\exists J)(\exists X)\rho$, where $\rho$ is a finite conjunction of sentences in ${\mathbb Sen}^{\mathbf {HFOL}}_0((S,F\cup X,P),Nom\cup J,\varLambda )$ the followings are equivalent:

• (i) $\varGamma \models ^{\mathbf {IHFOL}}(\exists J)(\exists X)\rho$,

• (ii) $(\mathcal{M}^\varGamma ,R^\varGamma )\models ^{\mathbf {IHFOL}}(\exists J)(\exists X)\rho$,

• (iii) there exists a hybrid substitution $\varTheta =\{\theta _j:X\rightarrow T_{(S,F,P)}(Y)\}_{j\in Nom}$ and a nominal substitution $\psi :J\rightarrow Nom$ such that $\varGamma \models ^{\mathbf {IHFOL}}(\forall Y)\varTheta ^k(\psi (\rho ))$ for some $k\in Nom$ and the sorts of variables in Y are inhabited, i.e. for any sort $s\in S$ and variable $y\in Y_s$ there exists a term $t\in T_{(S,F,P)}$.

The inhabitation requirement for the sorts of the variables in Y means that the inclusion $\iota _y:((S,F,P),Nom,\varLambda )\rightarrow ((S,F\cup Y,P),Nom,\varLambda )$ is conservative. The restriction to injective hybridisations required by Theorem 8 is not needed if the quantification subcategory consists of identities. For example, one can prove a version of Herbrand’s theorem for hybrid institutions that can be instantiated to ${\mathbf {HPL}}$.

6 Conclusions

In this paper we have proved the existence of initial models of hybrid Horn clauses. Our initiality results are not based on inclusion systems and quasi-varieties as in [6]. The proof follows the structure of the sentences in the style of [9]. We assume that the atomic sentences of the base institution are epi basic and then the initiality property is proved to be closed under certain sentence building operators. This approach requires less model theoretic infrastructure than [6] and it can be applied to theories for which the corresponding class of models does not form a quasi-variety. We have developed denotational foundations for logic programming in hybrid logics independently of the details of the underlying base institution by employing institutional concepts of quantification, substitution, reachable model and basic set of sentences. In this general setting we have proved Herbrand’s theorem. A future direction of research is developing a paramodulation procedure for hybrid logics. The results presented in this paper which do not involve inherited quantification can be applied to hybrid logics with model constraints [6], but much work is needed to cover the rigid quantification [2]. This constitutes another future direction of research.