Under consideration for publication in Formal Aspects of Computing

Birkhoff style calculi for hybrid logics
Daniel Găină
Institute of Mathematics for Industry, Kyushu University, Fukuoka, Japan

Abstract. We develop an abstract proof calculus for hybrid logics whose sentences are (hybrid) Horn clauses,
and we prove a Birkhoff completeness theorem for hybrid logics in the general setting provided by theinstitution theory. This result is then applied to particular cases of hybrid logics with user-defined sharing,where the first-order variables in quantified sentences are interpreted uniformly across worlds.
Keywords: Institution, Horn clause, Birkhoff calculus, Hybrid logic, Reconfigurable system

1. Introduction
In 1935, Birkhoff [Bir35] first proved a completeness theorem for equational logic, in the unsorted case.
Goguen and Meseguer [GM85], giving a sound and complete system of proof rules for many-sorted equational
deduction, generalised the completeness theorem of Birkhoff to the completeness of many-sorted equational
logic and provided simultaneously a full algebraisation of many-sorted equational deduction. Codescu andGăină [CG08] cast the result in the category-based setting of the institution theory [GB92], separating clearly
the details of concrete logics from the logical-independent aspects of the completeness property. Institution
theory is a category-based model theory that arose about three decades ago within formal methods as a
response to the explosion in the population of logics in use there; its original aim is to develop as muchcomputing science as possible in a general uniform way independently of particular logical systems. In thispaper, we define an abstract notion of Horn clause and we prove a Birkhoff completeness result for hybrid
logics in the general setting provided by the institution theory.
Hybrid logics [Bla00] are extensions of standard modal logics, involving symbols that name individualstates in models. Their history can be traced back to work of Arthur Prior in the fifties [Pri67]. The subject
was further developed in contributions such as [PT91, AB01, Bra11]. Recently, hybrid logics were developed
at an abstract institution theoretic level in works such as [MMDB11, Dia16b, DM16, G1̆5c, G1̆5b]. The ability
to refer to specific states has several advantages from the point of views of logic and formal specification. For
example, it has been argued [Bra11] that hybrid logics allow a more uniform proof theory than non-hybrid
modal logics. From a software engineering perspective, hybrid logics offer a generic framework to approach
the specification of reconfigurable systems, i.e. systems with reconfigurable features managing the dynamic
evolution of their configurations in response to external stimuli or internal performance indicators. See [SC11]
for an overview of the software reconfiguration paradigm.
The hybridization development presented in [MMDB11, Dia16b, DM16] defines a hybrid logical system
Correspondence and offprint requests to: Daniel Găină, e-mail: gaina.daniel@gmail.com

2

D. Găină

over an arbitrary institution. The parameters of this construction method are very general yielding to an
abstract framework that can be instantiated to many concrete hybrid logics. However, the definition of hybrid
institution given in [G1̆5b] provides a more general ‘top-down’ approach to the development of logical andcomputing science results in the spirit of ‘universal logic’ trend (in the sense envisaged by Jean-Yves Béziau[Béz06, Béz12]), and it captures examples of hybrid logics that are not instances of the hybridisation process.
Hybrid institutions are stratified institutions [AD07, Dia16a] with nominal and frame extraction. While thenotion of stratified institution describes modal logics, the definition of hybrid institution allows reference tothe states of the models and formalises the idea of hybrid logic.
As in [G1̆5b, G1̆5c], we are interested in extracting a significant fragment from a given hybrid logic withgood computational properties, in the sense that it can be used not only as a declarative language but
also as a executable/programming language. We define a notion of Horn clause for hybrid logics by notingthat classically, Horn clauses are constructed from atomic formulae by applying certain sentence building
operators in a specific order. The abstract Birkhoff entailment system is developed on top of an entailment
system for atomic sentences by adding proof rules for each sentence operator that occurs in Horn clauses.
The calculus proposed here will give a natural operational interpretation of the specifications written with(hybrid) Horn clauses. It is worth mentioning that this contribution targets the standard rigid quantification(e.g. [Bra11]) where the possible worlds share a common domain and the variables are interpreted identically
across the worlds. This approach is in contrast with the world-line semantics of [Sch11], where the quantified
variables may be interpreted differently across distinct worlds.
Concerning practical applications of this work, the general Birkhoff calculus developed in this paper
provides the foundations of a methodology for the formal specification and verification of reconfigurable
systems. Software systems with reconfigurable capabilities can be seen as transition structures, each nodecorresponding to a configuration. One may think as such nodes as local specifications of system configurations
while the global transition structure describes how the software evolves from one configuration to another. A
typical example of reconfigurable system is given by the cloud-based applications that flexibly react to clientdemands by allocating, for example, new server units to meet higher rates of service requests. The model
implemented over the cloud is pay-per-usage, which means that the users will pay only for using the services.
Therefore, the cloud service providers have to maintain a certain level of quality of service to keep up the
reputation. The operating systems of modern cars offer a second example: in each vehicle dozens of electronic
control units are connected together by a network and must operate in different modes, depending on thecurrent situation - such as driving on a highway or in town where different speed regulations are applied.
Switching between these modes is an example of dynamic reconfiguration. An error in the operating systemof a car could cause loss of human life. Reconfigurable systems are safety and security-critical systems withstrong qualitative requirements, and consequently, formal verification is needed. The cloud-based applications
and the operating systems of modern cars are mentioned as examples of reconfigurable systems in other works
such as [Mad13, MMBH15, NMMB16].
The paper is organised as follows. In Section 2 we recall the definition of institution that formalises theintuitive idea of logical system. In Section 3 we recall the definition of hybrid institution that constitutes theframework of the present work. Section 4 introduces the fundamental concepts that are necessary for our
general results. Section 5 is dedicated to the development of the abstract Birkhoff completeness. Section 6presents applications of the general theorems to concrete hybrid logics. Section 7 concludes the paper anddiscusses future work.

2. Institutions
The notion of logical system is formalised here as an institution.

2.1. Definition and examples
The concept of institution formalises the intuitive notion of logical system, and has been defined by Goguen
and Burstall in the seminal paper [GB92].
Definition 2.1 (Institution). An institution I = (SigI , SenI , ModI , |=I ) consists of(1) a category SigI , whose objects are called signatures,Birkhoff style calculi for hybrid logics

3(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
arrowsarecalled(Σ-)homomorphisms,(4) a family of relations |=I = {|=IΣ }Σ∈|SigI | , where |=IΣ ⊆ |ModI (Σ)| × SenI (Σ) is called (Σ-)satisfaction, suchthat the following satisfaction condition holds:
M 0 |=IΣ0 SenI (ϕ)(e) iff ModI (ϕ)(M 0 ) |=IΣ e
ϕfor all Σ → Σ0 ∈ SigI , M 0 ∈ |ModI (Σ0 )| and e ∈ SenI (Σ).
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  ϕ andthe 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 .
Example 2.1 (First-Order Logic (FOL) [GB92] ). The signatures are triplets of the form (S, F, P ),where S is the set of sorts, F = {Far→s }(ar,s)∈S ∗ ×S is the (S ∗ × S -indexed) set of operation symbols, andP = {Par }ar∈S ∗ is the (S ∗ -indexed) set of relation symbols. 1 If ar = ε then an element of
S Far→s is called aconstant symbol, or a constant. By a slight notational abuse, we let F and P also denote (ar,s)∈S ∗ ×S Far→sSand ar∈S ∗ Par , respectively. A signature morphism between (S, F, P ) and (S 0 , F 0 , P 0 ) is a triplet ϕ =
0
∗
rl
rl
(ϕst , ϕop , ϕrl ), where ϕst : S → S 0 , ϕop = {ϕopar→s : Far→s → Fϕst (ar)→ϕst (s) | ar ∈ S , s ∈ S}, ϕ = {ϕar :
0
∗
st
op
Par → Pϕst (ar) | ar ∈ S }. When there is no danger of confusion, we may let ϕ denote each of ϕ , ϕar→s ,ϕrl
ar . Given a signature Σ = (S, F, P ), a Σ-model is a triplet
M = ({Ms }s∈S , {Mσar,s }(ar,s)∈S ∗ ×S,σ∈Far→s , {Mπar }ar∈S ∗ ,π∈Par )interpreting each sort s as a set Ms , each operation symbol σ ∈ Far→s as a function Mσar,s : M ar → Ms
(where M ar stands for Ms1 × . . . × Msn if ar = s1 . . . sn ), and each relation symbol π ∈ Par as a relation
Mπar ⊆ M ar . When there is no danger of confusion we may let Mσ and Mπ denote Mσar,s and Mπar , respectively.
Morphisms between models are the usual Σ-morphisms, i.e., S-sorted functions that preserve the structure.
The Σ-algebra of terms is denoted by TΣ . The Σ-sentences are obtained from (a) equations t =s t0 , wheret ∈ (TΣ )s , t0 ∈ (TΣ )s , s ∈ S, and (b) relations π(t1 , . . . , tn ), where π ∈ Ps1 ...sn , ti ∈ (TΣ )si and si ∈ S, byapplying 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-ordersatisfaction and it is defined using the natural interpretations of ground terms t as elements Mt in models
M . The definitions of functors Sen and Mod on morphisms are the natural ones: for any signature morphism
ϕ : Σ → Σ0 , Sen(ϕ) : Sen(Σ) → Sen(Σ0 ) translates sentences symbol-wise, and Mod(ϕ) : Mod(Σ0 ) → Mod(Σ) is
the forgetful functor.
Example 2.2 (REL). The institution REL is the sub-institution of single-sorted first-order logic withsignatures having only constants and relational symbols.
Example 2.3 (Propositional Logic (PL)). The institution PL is the fragment of FOL determined by
the signatures with empty sets of sort symbols.
Example 2.4 (First-Order Logic with user-defined Sharing (FOLS)). This institution is used in Example 3.3 to define a hybrid logic and it is not intended for any other application. 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 SenFOLS ((S r , F r , P r ) ⊆(S, F, P )) consists of those sentences in SenFOL (S, F, P ) that contain only quantifiers over rigid variables.
The category of models ModFOLS ((S r , F r , P r ) ⊆ (S, F, P )) is ModFOL (S, F, P ). The satisfaction relation in
FOL
FOLS is induced from the satisfaction relation in FOL, i.e. |=FOLS(S r ,F r ,P r )⊆(S,F,P ) =|=(S,F,P ) .
1

If S is a set then S ∗ is the set of strings over symbols in S, including the empty string ε.

4

D. Găină

Example 2.5 (Preorder Algebra (POA) [DF02]). The POA signatures are just ordinary algebraic signatures, i.e. FOL signatures without relation symbols. The POA models are preordered algebras which areinterpretations 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 a preorder functor, whichmeans a preorder-preserving (i.e. monotonic) function. A preordered algebra morphism is just a 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 the terms are in the preorder relation of the carrier, i.e. Mt ≤ Mt0 . Full sentences areconstructed from equations and transitions by applying Boolean operators and first-order quantification.

2.2. Quantification category
Quantification comes with some subtle issues related to the translation of quantified sentences along signaturemorphisms that will be discussed in this subsection.
Definition 2.2 (Quantification category [Dia16b]). Given an institution I, a broad subcategory 2 Q ⊆χϕ
Sig is a quantification category for I when for each Σ → Σ0 ∈ Q and Σ → Σ1 ∈ Sig there is a designatedpushout

ΣO 0

ϕ[χ]

χ

/ Σ01
O

with χ(ϕ) ∈ Q and such that the horizontal composition of such designated

χ(ϕ)

Σ

ϕ

/ Σ1

pushouts is again a designated pushout: (a) χ(1Σ ) = χ, 1Σ [χ] = 1Σ0 , and (b) for the following pushouts
ΣO 0

ϕ[χ]

χ

/ Σ01 θ[χ(ϕ)]/ Σ02
O
O
χ(ϕ)

Σ

ϕ

/ Σ1

θ

we have ϕ[χ]; θ[χ(ϕ)] = (ϕ; θ)[χ] and χ(ϕ)(θ) = χ(ϕ; θ).

χ(ϕ)(θ)/ Σ2

In concrete examples of institutions the quantification category is fixed.
A first-order variable for a signature Σ = (S, F, P ) is a triple (x, s, Σ), where x is the name of thevariable and s ∈ S is the sort of the variable. Let χ : Σ ,→ Σ[X] be a signature extension with variables
fromX, where X = {Xs }s∈S is a S-sorted set of variables, Σ[X] = (S, F ∪ X, P ) and (F ∪ X)ar→s =
Far→sif ar ∈ (S ∗ − {ε})for all (ar, s) ∈ S ∗ × S. The quantification category QFOL for FOL
Far→s ∪ Xs if ar = εϕconsists of signature extensions with a finite set of variables. Given a signature morphism Σ → Σ1 , whereΣ1 = (S1 , F1 , P1 ), then(a) χ(ϕ) : Σ1 ,→ Σ1 [X ϕ ], where X ϕ = {(x, ϕ(s), Σ1 ) | (x, s, Σ) ∈ X}, and(b) ϕ[χ] is the extension of ϕ that maps each (x, s, Σ) to (x, ϕ(s), Σ1 ).
Remark 2.1. Let Σ be a FOL signature, (∀X)γ a Σ-sentence, and M a Σ-model.
(1) From the institution theory perspective, (∀X)γ is just an abbreviation for (∀χ)γ, where χ : Σ ,→ Σ[X]is the inclusion, and(2) M |=Σ (∀χ)γ iff for all χ-expansions M 0 we have M 0 |=Σ[X] γ.
When quantified sentences get translated along signature morphisms using this approach, one avoids clashingof variables with the constant symbols from the target signature.

2.3. Substitutions
We recall the notion of substitution in institutions.
2

A category C is a broad subcategory of C 0 if C is a subcategory of C 0 and C contains all objects of C 0 , i.e. |C| = |C 0 |.

Birkhoff style calculi for hybrid logics

5

χ1

Definition 2.3 (Substitution [Dia04]). Let I be an institution. For any signature morphisms Σ → Σ0 ∈
χ2
SigI and Σ → Σ00 ∈ SigI , a Σ-substitution θ : χ1 → χ2 consists of a pair (Sen(θ), Mod(θ)) , where Sen(θ) :Sen(Σ0 ) → Sen(Σ00 ) is a function and Mod(θ) : Mod(Σ00 ) → Mod(Σ0 ) is a functor, such that both of thempreserve Σ, i.e. the following diagrams commute:Sen(Σ0 )O
Sen(χ1 )Sen(θ)/ Sen(Σ00 )9

Sen(χ2 )Mod(Σ0 ) oMod(θ)

Mod(χ1 )Sen(Σ)

Mod(Σ00 )Mod(χ2 )% Mod(Σ)and such that the following satisfaction condition holds:
Mod(θ)(M2 ) |= γ1 iff M2 |= Sen(γ1 )for each Σ -model M2 and each Σ -sentence γ1 .
00

0Note that a substitution θ : χ1 → χ2 is uniquely identified by its domain χ1 , codomain χ2 and the pair(Sen(θ), Mod(θ)). When there is no danger of confusion, we let  θ denote the functor Mod(θ), and let θ
denote the sentence translation Sen(θ).
Example 2.6 (FOL substitutions [Dia04]). Consider two signature extensions with constants χ1 : Σ,→Σ[C1 ]and χ2 : Σ ,→ Σ[C2 ], where Σ = (S, F, P ) ∈ |SigFOL |, Ci is a set of constant symbols different from the theconstants in F . A function θ : C1 → TΣ (C2 ) represents a substitution between χ1 and χ2 :(1) On the syntactic side, θ : C1 → TΣ (C2 ) can be canonically extended to a function Sen(θ) : Sen(Σ[C1 ]) →Sen(Σ[C2 ]) which preserves Σ and substitutes Σ(C2 )-terms for constants in C1 .
(2) On the semantics side, θ determines a model functor Mod(θ) : Mod(Σ[C2 ]) → Mod(Σ[C1 ]) such that forall Σ[C2 ]-models M we have (a) Mod(θ)(M )x = Mx , for each sort x ∈ S, or operation symbol x ∈ F , orrelation symbol x ∈ P , and (b) Mod(θ)(M )c1 = Mθ(c1 ) for each c1 ∈ C1 .
Substitution functors. Let I be an institution. For any signature Σ ∈ |SigI |, Σ-substitutions form aχ
category SbI (Σ), where the objects are signature morphisms Σ → Σ0 ∈ Sig, and the arrows are substitutionsϕθ : χ1 → χ2 described in Definition 2.3. Given Σ0 → Σ ∈ SigI there exists a reduct functor SbI (ϕ) : SbI (Σ) →ISb (Σ0 ) that maps each Σ-substitution θ : χ1 → χ2 to the Σ0 -substitution Sb(ϕ)(θ) : ϕ; χ1 → ϕ; χ2 suchthat Sen(SbI (ϕ)(θ)) = Sen(θ) and Mod(SbI (ϕ)(θ)) = Mod(θ).
Fact 2.2. SbI : SigI → CATop is a functor.
In applications not all substitutions are of interest, and it is often assumed a substitution 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 of confusion we may drop the superscript I from the notations.
Example 2.7 (FOL substitution functor [G1̆5a]). Let DFOL ⊆ SigFOL be the broad subcategory ofsignature 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 byfunctions θ : C1 → TΣ (C2 ) as in Example 2.6.
Substitution systems. In theorem proving it is often useful to convert sentences into so-called normal
forms. An example of normal form in propositional logic is the conjunctive normal form. In order to reason
about such conversions, we formalise them as substitutions.
Definition 2.4. A substitution system ΘI = {ΘIΣ }Σ∈|SigI | for an institution I is a family of substitutions
ΘIΣ : 1Σ → 1Σ indexed by the signatures Σ ∈ |SigI | with the domain and codomain consisting of identity
signature morphisms 1Σ .
When there is no danger of confusion we may drop the superscript I and/or the subscript Σ from the notation
ΘIΣ . Examples of substitution systems may be found in Section 5.

6

D. Găină

3. Hybrid institutions
Given a base logic one can construct freely its hybridized version by applying the hybridisation process
defined in [MMDB11, DM16]. In this paper, we use the definition of hybrid logic given in [G1̆5b], which
provides a higher level of generality and a top-down approach to Kripke semantics in the spirit of universal
logic.

3.1. Definition and examples
Informally, hybrid institutions are institutions whose signatures are equipped with nominals and modalities
and whose models are Kripke structures. Hybrid institutions are refinements of stratified institutions thatwere introduced in [AD07] to enhance the concept of institution with ‘states’ for the models.
Definition 3.1 (Hybrid institution [G1̆5b]).
A hybrid institution HI = (SigHI , FHI , SenHI , ModHI , KHI , |=HI ) consists of(1) a category SigHI , whose objects are called signatures,(2) 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,HIHI(3) a sentence functor Sen : Sig → Set, providing for each signature ∆ a set whose elements are called(∆-)sentences,(4) a model functor ModHI : SigHI → CATop , providing for each signature ∆ a category whose objects arecalled (∆-)models and whose arrows are called (∆-)homomorphisms,(5) 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 ) consistingof a set of states/worlds |K∆ (M )| together with their accessibility relations K∆ (M )λ , where λ ∈ Λ∆n andn ∈ N,(6) a satisfaction relation |=HI = {M |=∆ }∆∈|SigHI |,M ∈|ModHI (∆)| , where M |=∆ ⊆ |K∆ (M )| × SenHI (∆) suchthat the following local satisfaction condition holds:
0

0

HI
HI
0
w
M 0 |=w∆0 Sen (ϕ)(e) iff Mod (ϕ)(M ) |=∆ efor all models M 0 ∈ |ModHI (∆0 )|, states w0 ∈ K∆0 (M 0 ) and sentences e ∈ SenHI (∆).
Like for ordinary institutions, when appropriate we shall also use simplified notations without superscripts
or subscripts that are clear from the context. The consistency of the local satisfaction condition from Definition 3.1 (6) is given by the following lemma.
ϕLemma 3.1. For all signature morphisms ∆ → ∆0 , every ∆0 -model M 0 has exactly the same set of states
as its reduct M  ϕ .
ϕProof. Note that for all signature morphisms ∆ → ∆0 and ∆0 -models M 0 , by the definition of ModREL , wehave |K∆0 (M 0 )| = |K∆0 (M 0 )  F (ϕ) |, and since 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  ϕ )|.
Given a hybrid institution HI, we define the following global satisfaction relationw
M |=HI∆ e iff M |=∆ e for all states w ∈ |K∆ (M )|where ∆ ∈ |SigHI |, M ∈ |ModHI (∆)|, and e ∈ SenHI (∆). We overload the notation and let |=HI to denote
both families of relations {M |=∆ }∆∈|SigHI |,M ∈|ModHI | and { |=HI∆ }∆∈|SigHI | . Hybrid institutions determine
canonically institutions.
Fact 3.2. If HI is a hybrid institution then (SigHI , SenHI , ModHI , |=HI ) is an institution.
The following definition provides a pattern for describing the semantics of hybrid logics. More concretely,
it constructs a Kripke model functor from a base model functor such that the Kripke structures are pairsconsisting of a set of states and a mapping that associates to each state a base model. However, our approachBirkhoff style calculi for hybrid logics

7

is top-down meaning that the results will be developed at a more abstract level provided by Definition 3.1,
where the Kripke structures are implicitly assumed (not constructed).
Definition 3.2 (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(a) Kripke models of the form (W, M ), where W ∈ |ModREL (Nom, Λ)| and M : |W | → |ModI (Σ)| is amapping from the set of states/worlds |W | to the class of models |Mod(Σ)|, and(b) homomorphisms h : (W, M ) → (W 0 , M 0 ) of the form (hREL , hmod ), where
hREL : W → W 0 is a homomorphism in REL, andhmod : M ⇒ M 0 ◦ hREL is a natural transformation.
ϕ(2) for each signature morphism (Nom, Λ, Σ) → (Nom0 , Λ0 , Σ0 ) ∈ SigREL × SigI ,where ϕREL : (Nom, Λ) → (Nom0 , Λ0 ) ∈ SigREL and ϕI : Σ → Σ0 ∈ SigI ,the reduct functor ModIκ (ϕ) : ModIκ (Nom0 , Λ0 , Σ0 ) → ModIκ (Nom, Λ, Σ) is defined by(a) ModIκ (ϕ)(W 0 , M 0 ) = (W, M ) for all (W 0 , M 0 ) ∈ |ModIκ (Nom0 , Λ0 , Σ0 )|,where the model (W, M ) ∈ |ModIκ (Nom, Λ, Σ)| is defined by(i) W = W 0  ϕREL , i.e. |W | = |W 0 | and Wλ = Wϕ0 REL (λ) for all λ ∈ Λ, and(ii) Mw = Mw0  ϕI , for all states w ∈ |W |.
(b) ModIκ (ϕ)(h0 ) = h for all homorphisms h0 ∈ ModIκ (Nom0 , Λ0 , Σ0 ),where hREL = h0REL  ϕREL and hmod = {h0w  ϕI }w∈|W | .
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 ∆, the frame functor K∆ is the forgetful functor mapping each Kripke structure (W, M ) to W .
Assumption 1. Throughout this paper we assume that HI range hybrid institutions with a quantification
category QHI that satisfy the following exactness property: for every signature ∆ ∈ |SigHI | and each variable
j for (Nom∆ , Λ∆ ) there exists a designated signature morphism χ[j] : ∆ → ∆[j] ∈ QHI such that (a) F(χ[j]) =χ[j]REL , where χ[j]REL : (Nom∆ , Λ∆ ) ,→ (Nom∆ ∪ {j}, Λ∆ ), and (b) for any ∆-model M and any χ[j]REL expansion W 0 of K∆ (M ) there exists a unique χ[j]-expansion M 0 of M such that K∆[j] (M 0 ) = W 0 .
We use Definition 3.2 to justify Assumption 1. In applications, ∆ = (Nom, Λ, Σ), ∆[j] = (Nom ∪ {j}, Λ, Σ) andχ[j] : (Nom, Λ, Σ) ,→ (Nom ∪ {j}, Λ, Σ) is the inclusion. For any ∆-model (W, M ) and any χ[j]REL -expansion
W 0 of W , the model (W 0 , M ) is the unique χ[j]-expansion of (W, M ) such that K∆[j] (W 0 , M ) = W 0 .
Notation 3.3. Assume a hybrid institution HI and a ∆-model M , where ∆ is a signature of HI. If W is theframe of M , i.e. K∆ (M ) = W , then for every state w of M and each nominal variable j, we denote by(j,w)(1) W (j,w) the unique χREL
-expansion of W such that the denotation of j in W (j,w) is w, i.e. Wj
= w,
j
and
(2) M (j,w) the unique χj -expansion of M such that W (j,w) is the frame of M (j,w) , i.e. K∆[j] (M (j,w) ) = W (j,w) .
The semantics of each sentence operator is defined at the abstract level provided by Definition 3.1.
Definition 3.4 (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)(8) M |=w|=w
∆ (↓ j)e iff M∆[j] e.

8

D. Găinăχwhere ∆ → ∆0 is a signature morphism of HI, M is a ∆-model, W is the frame of 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 say that that k1 = k2 is a nominal equation and λ(k1 , . . . , kn ) is a nominal relation. The operator @ iscalled ‘retrieve’ because it changes the point of evaluation for a model. For any modality λ, the operator [λ]is called traditionally ‘necessity’. The operator ↓ is called ‘store’ because it allows us to give a name to thecurrent state that can be referred in sentences. The concepts of Boolean operators and quantifications inordinary institutions (e.g. from [Dia03, Dia08, Tar86a] etc.) arise as an instance of Definition 3.4 when theunderlying set of states |K∆ (M )| of each model M is a singleton set.
Example 3.1 (Hybrid first-order logic (HFOL)). This hybrid institution is a variation of first-orderhybrid logic of [BM02] where models may have different carrier sets across the states. The functor ModHFOL
is ModFOL: SigREL × SigFOL → CATop . Given a signature ∆ = (Nom, Λ, Σ) ∈ |SigHFOL |, the atomic
κsentences in SenHFOL (∆) are the atomic sentences in SenFOL (Σ). The sentences are constructed from atomic
sentences, nominal equations and nominal relations by applying Boolean operators, retrieve, store, necessityand quantification over nominal variables. The satisfaction of atomic sentences is defined by (W, M ) |=w
ρ iff Mw |=FOL ρ for all signatures ∆ ∈ |SigHFOL |, atomic sentences ρ ∈ SenHFOL (∆), models (W, M ) ∈|ModHFOL (∆)| and states w ∈ |W |.
Example 3.2 (Hybrid Propositional Logic (HPL) [AB01]). This institution is a particular case of
HFOL with empty set of sorts. The signatures (Nom, Λ, Prop) consist of a set of nominals Nom, a familyof sets of modalities Λ = {Λn }n∈N , and a set of propositional symbols Prop. Let ∆ = (Nom, Λ, Prop) be a
HPL signature. 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. The satisfaction relation for atomic sentences is defined by (W, M ) |=w p iff p ∈ Mw for all models(W, M ) ∈ |ModHPL (∆)|, states w ∈ |W | and propositional symbols p ∈ Prop.
Example 3.3 (Hybrid First-Order Logic with user-defined Sharing (HFOLS) [MMDB11]). The
model functor ModHFOLS : SigREL ×SigFOLS → CATop is a sub-functor of ModFOLS: SigREL ×SigFOLS →κCATop which restricts the models and the homomorphisms of ModFOLS
such
that
the
rigid symbols are inκ
terpreted uniformly across the states, i.e. for all ∆ ∈ |SigHFOLS |, we have (1) (W, M ) ∈ |ModHFOLS (∆)|
iff for all states w1 , w2 ∈ |W | and rigid symbols x in ∆ we have (Mw1 )x = (Mw2 )x , and (2) h : (W, M ) →mod(W 0 , M 0 ) ∈ ModHFOLS (∆) iff for all states w1 , w2 ∈ |W | and rigid sorts sr in ∆ we have (hmodw1 )sr = (hw2 )sr .
HFOLSGiven a signature ∆ = (Nom, Λ, Σ), the atomic sentences in Sen(∆) are the atomic sentences in
SenFOLS (Σ). The 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. The satisfaction of atomic sentences is defined as follows: (W, M ) |=w ρ iff Mw |=FOLS ρ, for all
signatures ∆, atomic sentences ρ ∈ SenHFOLS (∆), models (W, M ) ∈ |ModHFOLS (∆)| and states w ∈ |W |.
Example 3.4 (Hybrid First-Order Logic with user-defined Sharing and Annotation (HFOLSA)).
This institution was defined in [G1̆5b] and it has the same model functor as HFOLS, i.e. ModHFOLSA =ModHFOLS . Let ∆ = (Nom, Λ, Σ) be a HFOLSA signature, where Σ = (S r , F r , P r ) ⊆ (S, F, P ) is a FOLS
signature. For all nominals k ∈ N om, we define the S-sorted sets Tk∆ of hybrid terms:
τ1 ∈ (Tk∆ )sr1 , . . . , τn ∈ (Tk∆ )srnrfor all rigid symbols ς ∈ Fsr,
1 ...srn →srς(τ1 , . . . , τn ) ∈ (Tk∆ )sr
t1 ∈ (Tk∆ )s1 , . . . , tn ∈ (Tk∆ )sn(2)
for all non-rigid symbols σ ∈ (Fs1 ...sn →s − Fsr1 ...sn →s ),σk (t1 , . . . , tn ) ∈ (Tk∆ )sτ ∈ (Tk∆1 )sr, where sr ∈ S r .
(3)τ ∈ (Tk∆ )sr(1)

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 $(τ1 , . . . , τn ), where $ ∈ Psr, τi ∈ (Tk∆ )sri , sri ∈ S r and k ∈ Nom, and1 ...srn(c) non-rigid relations πk (t1 , . . . , tn ), where π ∈ (Ps1 ...sn − Psr1 ...sn ), ti ∈ (Tk∆ )si , si ∈ S and k ∈ Nom.

Birkhoff style calculi for hybrid logics

9

When there is no danger of confusion we omit the subscript s and/or the superscript k from the notationt =ks t0 . Full sentences are constructed from atomic sentences, nominal equations and relations by applying
Boolean operators, retrieve, store, necessity and quantification over nominal variables and rigid variables.
Given a model (W, M ) ∈ |ModHFOLSA (∆)|, the interpretation of a ∆-term into (W, M ) is defined inductively on the structure of the ∆-terms:(1) (W, M )ς(τ1 ,...,τn ) = (MWk )ς ((W, M )τ1 , . . . , (W, M )τn ),(2) (W, M )σk (t1 ,...,tn ) = (MWk )σ ((W, M )t1 , . . . , (W, M )tn ), and(3) assuming that (W, M )τ ∈ (MWk1 )sr is defined, then since (MWk1 )sr = (MWk )sr , the interpretation ofτ ∈ (Tk∆ )sr into (W, M ) is also (W, M )τ ∈ (MWk1 )sr .
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 ) |= $(τ1 , . . . τn ) iff ((W, M )τ1 , . . . , (W, M )τn ) ∈ (Mk )$ ;(c) (W, M ) |= πk (t1 , . . . , tn ) iff ((W, M )t1 , . . . , (W, M )tn ) ∈ (Mk )π .
Example 3.5 (SHARE). This institution is obtained from HFOLSA by restricting the signatures suchthat all sorts are rigid.
Example 3.6 (Hybrid Preorder Algebra with user-defined Sharing and Annotation (HPOASA)).
This institution was defined in [G1̆5b] and it is obtained by replicating the construction of HFOLSA in thecontext of preorder algebra. The Kripke structures of HPOASA upgrade the Kripke structures of HFOLSA
with preorder relations for the carrier sets of each sort. Given a HPOASA 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 ,where t ∈ (Tk∆ )s , t0 ∈ (Tk∆ )s , k ∈ Nom and s ∈ S. The 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. The satisfaction relation for atomic sentences is definedby (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 .

3.2. Hybrid quantification category
Let HI be a hybrid institution. Given a signature ∆, a nominal variable j for FHI (∆) is a pair (x, FHI (∆)),
where x is the name of the variable.
The quantification category QHFOLSA for HFOLSA consists of signature extensions with a finite numberof nominal variables and rigid variables of the form ∆ ,→ ∆[J, X], where ∆ = (Nom, Λ, Σ) ∈ |SigHFOLSA |,∆[J, X] = (Nom ∪ J, Λ, Σ[X]) ∈ |SigHFOLSA |, Σ = (S r , F r , P r ) ⊆ (S, F, P ) ∈ |SigFOLS |, J is a finite set ofvariables for (Nom, Λ), X is a finite set of rigid variables for Σ and Σ[X] = (S r , F r ∪ X, P r ) ⊆ (S, F ∪ X, P ).
The quantification category QHPL for HPL consists of signature extensions with a finite number of
nominal variables ∆ ,→ ∆[J], where ∆ = (Nom, Λ, Prop) ∈ |SigHPL |, ∆[J] = (Nom ∪ J, Λ, Prop) ∈ |SigHPL |and J is a finite set of variables for (Nom, Λ).

3.3. Standard approach vs. annotation
The hybrid logics with annotated syntax are recently introduced in [G1̆5b]. They have the advantage of
having good logical properties that brings them closer to the first-order logics, i.e. the existence of initialmodel of Horn clauses, completeness, compactness, etc. In what follows we show that hybrid logics withannotated syntax are more expressive than their classic versions using HFOLSA as a benchmark example.
Let ∆ = (Nom, Λ, Σ) a HFOLSA signature and j a variable for (Nom, Λ), where Σ = (S r , F r , P r ) ⊆∆[j](S, F, P ). Let atj : T(S,F,P ) → Tj
be the function from the set of first-order (S, F, P )-terms T(S,F,P ) to theσ(atj (t1 ), . . . , atj (tn ))if σ ∈ F r∆[j]
set of hybrid ∆-terms Tj
defined by atj (σ(t1 , . . . , tn )) =.
σj (atj (t1 ), . . . , atj (tn )) if σ ∈ F − F r
Let HFOLSa be the restriction of HFOLS to atomic sentences. The function α∆ : SenHFOLSa (∆) →SenHFOLSA (∆) is defined by extending atj to atomic sentences:

10(a) α∆ (t1 = t2 ) = (↓ j)(atj (t1 ) = atj (t2 )), and(↓ j)π(atj (t1 ), . . . , atj (tn ))(b) α∆ (π(t1 , . . . , tn )) =(↓ j)πj (atj (t1 ), . . . , atj (tn ))D. Găină

if π ∈ P r,
if π ∈ P − P r

where ti ∈ T(S,F,P ) .
Proposition 3.3. [G1̆5b] For any ∆-model (W, M ), state w ∈ |W | and sentence ρ ∈ SenHFOLSa (∆) wehave (W, M ) |=w ρ iff (W, M ) |=w α∆ (ρ).
This result says that the HFOLS-sentence ρ has the same expressive power as the HFOLSA-sentenceα∆ (ρ). Proposition 3.3 can be easily extended to all sentences of HFOLS, which implies that HFOLSA ismore expressive than HFOLS. Proposition 3.3 shows that the operator store is somehow integrated in theatomic sentences of HFOLS while in HFOLSA it is not the case. This is one of the main reasons HFOLSA
allows a more structured approach to model-theoretic properties. It is worth mentioning that HFOLSA is
not an instance of the hybridisation process described in [MMDB11, DM16, Dia16b].

3.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 3.5. Let HI be a hybrid institution. A hybrid substitution between the signature morphisms
χ1χ2θ∆ → ∆0 ∈ SigHI and ∆ → ∆00 ∈ SigHI is a substitution χ1 → χ2 such that the following local satisfaction
00
w
0
00
w
00
condition holds: M |= θ(ρ ) iff M  θ |= ρ, for all M ∈ |ModHI (∆00 )|, ρ ∈ SenHI (∆0 ) and w ∈ |K∆00 (M 00 )|.
Note that |K∆00 (M 00 )  θ | = |(K∆00 (M 00 )  θ )  χ1 | = |K∆00 (M 00 )  χ2 |, which makes the above definition consistent.
Example 3.7 (HFOLSA substitutions [G1̆5b]). Consider two signature extensions with nominals andrigid 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 con∆[C ,D ]stants different from the constants in F . A pair of functions θ = (θa : C1 → Nom ∪ C2 , θb : D1 → Tk 2 2 ),where k ∈ Nom, represents a substitution between χ1 and χ2 :(1) On the syntactic side, θ determines a sentence translation
SenHFOLSA (θ) : SenHFOLSA (∆[C1 , D1 ]) → SenHFOLSA (∆[C2 , D2 ]), which preserves ∆ and substitutes(a) nominals in Nom ∪ C2 for nominals in C1 corresponding to θa , and (b) ∆[C2 , D2 ]-terms for constantsin D1 according to θb .
(2) On the semantics side, θ determines a model functor
ModHFOLSA (θ) : ModHFOLSA (∆[C2 , D2 ]) → ModHFOLSA (∆[C1 , D1 ]) such that for all ∆[C2 , D2 ]-models(W 00 , M 00 ) the model (W 00 , M 00 )  θ interprets (a) each symbol x in ∆ as (W 00 , M 00 )x , (b) each nominalc1 ∈ C1 as (W 00 , M 00 )θa (c1 ) , and (c) any rigid symbol d1 ∈ D1 as (W 00 , M 00 )θb (d1 ) .
Hybrid substitution functors. Given a hybrid institution HI, for any signature ∆ ∈ |SigHI |, the hybrid∆-substitutions form a subcategory HSbHI (∆) of SbHI (∆).
Fact 3.4. HSbHI : SigHI → CATop is a sub-functor of SbHI .
In applications we work with a substitution sub-functor HStHI : DHI → CATop of HSbHI , where DHI ⊆ SigHI
is a broad subcategory of signature morphisms. When there is no danger of confusion we may drop thesuperscript HI from notations.
Example 3.8 (HFOLSA substitution functor). Given a signature ∆ = (Nom, Λ, (S r , F r , P r ) ⊆ (S, F, P )),∆[C ,D ]only substitutions represented by pairs of functions (θa : C1 → Nom ∪ C2 , θb : D1 → Tk 2 2 ) as describedin Example 3.7 are relevant for the present study. Let DHFOLSA ⊆ SigHFOLSA be the broad subcategory ofsignature extensions with nominals and rigid constants. Let HStHFOLSA : DHFOLSA → CATop denote thesubstitution functor which maps each signature ∆ to the category of hybrid substitutions represented by∆[C ,D ]pairs of functions (θa : C1 → Nom ∪ C2 , θb : D1 → Tk 2 2 ) as described in Example 3.7.

Birkhoff style calculi for hybrid logics

11

Example 3.9 (HPL substitution functor). Let DHPL be the broad subcategory of signature extensions
with nominals. Let HStHPL : DHPL → CATop denote the substitution functor which maps each signature∆ = (Nom, Λ, Prop) to the category of hybrid substitutions represented by functions θ : C1 → Nom∪C2 , where
Ci is a set of nominals different from the elements of Nom.
Hybrid substitution systems. We formalise sentence conversions in hybrid institutions as hybrid substitutions.
Definition 3.6. Given a hybrid institution HI, a hybrid substitution system is a substitution system thatconsists only of hybrid substitutions.
Examples of hybrid substitution systems may be found in Section 5.

4. Institution-independent concepts
We investigate some of the institution-independent notions and concepts that are necessary to prove ourabstract results.

4.1. Reachable models
In general, the signatures of institutions provide the vocabulary for defining sentences: one can constructterms from the syntactic elements that compose the signatures, and then build formulas using terms. Eachelement of a signature has a precise semantics, which implies that every term has a unique interpretation
into a model. Note that models consist of elements which may, or may not be, interpretations of terms. The
models with elements which are interpretations of terms are called reachable [Pet07, GP10, GFO12, G1̆5a,
cF15, G1̆5c, G1̆5b]. The following definition originates from [Pet07] and provides an institution-independent
characterisation of reachable models.
Definition 4.1. Let I be an institution, D ⊆ Sig a broad subcategory of signature morphisms, and St :D → CATop a substitution functor for I. Given a signature Σ ∈ |SigI |, a Σ-model M is St-reachable iffor every signature morphism χ : Σ → Σ0 ∈ D and each χ-expansion M 0 of M there exists a substitutionθ : χ → 1Σ ∈ St(Σ) such that M  θ = M 0 .
If the substitution functor St is fixed, St-reachable models may be called simply reachable. In the following
the notion of reachability is applied to concrete logical systems.
Proposition 4.1. [Pet07, GFO12] In FOL, a model is StFOL -reachable iff its elements consist of interpretations of terms.
Proposition 4.1 says that a first order (S, F, P )-model M is reachable iff the unique homomorphism T(S,F,P ) →M is surjective. In HFOLSA reachable models consist of interpretations of nominals and hybrid terms.
Proposition 4.2. [G1̆5b] In HFOLSA, a model is StHFOLSA -reachable iff (a) its set of states consists ofinterpretations of nominals and (b) its carrier sets for the rigid sorts consist of interpretations of terms.
The expansions of models that consist of interpretations of syntactic elements along signature extensions withrigid variables do not generate substitutions in HFOLS, in general. The abstract theorems of the following
sections are applicable to hybridized institutions with user-defined sharing in their standard versions only if
the quantification is restricted to the quantification over nominal variables.
Proposition 4.3. [G1̆5b] In HPL, a model is StHPL -reachable iff its states consists of interpretations of
nominals.

4.2. Basic sentences
In concrete examples of institutions, basic sentences are the simplest sentences, which are intimately linked
to the internal structure of models, in the sense that their satisfaction is preserved by homomorphisms. Basic

12

D. Găină

sentences [Dia03] tend to be the starting building blocks from which the complex sentences are constructed byusing Boolean operators, quantification, or other sentence operators. Basic sentences were initially introduced
in [Tar86b] under the name of positive elementary sentences.
Definition 4.2. Let I be an institution. A set of sentences B ⊆ Sen(Σ) is basic if there exists a Σ-modelM 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 the morphism M B → M is uniquethen the set B is called epi-basic.
We show that the sets of atomic sentences of the institutions presented above are epi-basic. In addition,
the basic model M B is reachable, since M B is obtained by factorising the term model by some congruence
relation generated by B.
Proposition 4.4. [Dia03] Any set of atomic sentences in FOL is epi-basic, and the basic models are StFOL reachable.
Proof. Let B be a set of atomic Σ-sentences in FOL. The basic model MB is the initial model of B and
it is constructed as follows: on the quotient TΣ /≡B of the term model TΣ by the congruence generated by
the equational atoms of B, we interpret each relation symbol π of Σ by (MB )π = {(t1 /≡B , . . . , tn /≡B ) |π(t1 , . . . , tn ) ∈ B}.
Proposition 4.5. [G1̆5b] Let HFOLSAb be the restriction of HFOLSA to sentences obtained by applying
the operator retrieve to atomic sentences, nominal equations and nominal relations. Any set of sentences in
HFOLSAb is epi-basic and the basic models are HStHFOLSA -reachable.
Proposition 4.6. [G1̆5b] Let HPLb be the restriction of HPL to sentences obtained by applying theoperator retrieve to nominal equations, nominal relations and sentences of the form @k p, where k is anominal and p is a propositional symbol. Any set of sentences in HPLb is epi-basic and the basic models
are HStHPL -reachable.
The following result shows that the semantic consequences of a basic set of sentences can be reduced tothe satisfaction by a base model.
Lemma 4.7. [G1̆5b] 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 |=Σ γ.

4.3. Entailment systems
Institutions with proof-theoretic structure provide a complete formal notion for the intuitive notion oflogic, including both the model and the proof-theoretic sides. To account for proofs and their construction, Meseguer [Mes89] introduced the notion of entailment system. The proof systems defined by Diaconescu [Dia06] provide a more refined framework by discriminating between different proofs and addressing
to their internal structure. Our approach is slightly more general than [Mes89] since we consider entailment
relations E1 ` E2 such that not only E1 but also E2 is a set of sentences rather than a single sentence.
Definition 4.3. An entailment system E = (Sig, Sen, `) consists of a category of signatures Sig, a sentencefunctor Sen : Sig → Set, and a family of entailment relations `= {`Σ }Σ∈|Sig| between sets of sentences withthe following properties:
E ⊆ E1E1 `Σ E2 , E2 `Σ E3(M onotonicity)(T ransitivity)
E1 `Σ EE1 `Σ E3E1 `Σ E2 , E1 `Σ E3
E1 `Σ E2
(T ranslation)
E1 `Σ E2 ∪ E3
ϕ(E1 ) `Σ0 ϕ(E2 )where Ei ⊆ Sen(Σ), E ⊆ Sen(Σ) and ϕ : Σ → Σ0 ∈ Sig.
(U nions)

When there is no danger of confusion we may omit the subscript Σ from `Σ . We call the entailment system
E = (Sig, Sen, `) compact whenever for every Γ ⊆ Sen(Σ) and each finite Ef ⊆ Sen(Σ) if Γ `Σ Ef then

Birkhoff style calculi for hybrid logics

13

there exists Γf ⊂ Γ finite such that Γf `Σ Ef . For each entailment system E = (Sig, Sen, `) one can easily
construct the compact entailment subsystem E c = (Sig, Sen, `c ) by defining the entailment relation `c asfollows: Γ `cΣ E iff for each finite set Ef ⊆ E there exists a finite set Γf ⊆ Γ such that Γf `Σ Ef .
Lemma 4.8 (Compact entailment subsystem [Dia06]). E c = (Sig, Sen, `c ) is an entailment system.
The semantic entailment system of an institution I consists of (SigI , SenI , |=I ). For every signature morphism ϕ ∈ SigI , we sometimes let ϕ denote the sentence translation SenI (ϕ). An entailment system
E I = (SigI , SenI , `I ) is sound (resp. complete) for an institution I if Γ `IΣ γ implies Γ |=IΣ γ (resp. Γ |=IΣ γ
implies Γ `IΣ γ) for every signature Σ, each set of Σ-sentences Γ and any Σ-sentence γ.
Proposition 4.9. Consider (a) an institution I, (b) a sub-functor SenI0 : SigI → Set of SenI , (c) an entailment system E I0 = (SigI , SenI0 , `I0 ) for the institution I0 = (SigI , SenI0 , ModI , |=I ), and (d) a substitution
system ΘI for I. We define E I = (SigI , SenI , `I ) as the least entailment system over E I0 closed to(SubstΘI )γ ` ΘIΣ (γ)

andΘIΣ (γ) ` γ

where γ ∈ SenI (Σ). Then we have:(1) E I is sound if E I0 is sound,(2) E I is compact if E I0 is compact, and(3) E I is complete if (i) E I0 is complete and compact, and (ii) ΘIΣ (γ) ∈ SenI0 (Σ) for all signatures Σ ∈ |SigI |and sentences γ ∈ SenI (Σ).
Proof. For the sake of simplicity, we will drop the superscript I from the notations.
For soundness, it suffices to show that the proof rules (SubstΘ ) are sound, which follows directly fromthe satisfaction condition for substitutions.
For compactness, let E c = (Sig, Sen, `c ) be the compact entailment subsystem of E = (Sig, Sen, `). It iseasy to see that E c is closed to proof rules (SubstΘ ). Since E I0 is compact, E c includes all deductions from
E I0 . Hence, E = E c .
For completeness, suppose that Γ |=Σ γ, where Σ ∈ |Sig|, Γ ⊆ Sen(Σ) and γ ∈ Sen(Σ). By the satisfaction
condition for substitutions, Θ(Γ) |= Θ(γ). Since E I0 is complete, Θ(Γ) `I0 Θ(γ). By the compactness of E I0
there exists Γf ⊆ Γ finite such that Θ(Γf ) `I0 Θ(γ). Since Γf is finite and Γ ` Θ(e) for all e ∈ Γf , Γ ` Θ(Γf ).
It follows that Γ ` Θ(γ) and since Θ(γ) ` γ, we get Γ ` γ.
This result can be used to extend completeness to a logical system obtained from a given logic by adding
a new sentence operator that does not enrich the expressivity of the initial syntax, i.e. the new sentence
operator can be defined using the sentence operators of the given logic. Applications of Proposition 4.9 canbe found in Section 5.

5. CompletenessThe notion of Horn clause is generalised to the level of hybrid institutions, and an abstract Birkhoff calculus
is developed to reason formally about Horn clauses. The entailment system developed here consists of twolayers:(1) the base layer corresponding to atomic sentences, nominal equations and nominal relations which isassumed in the abstract setting but it is developed in concrete examples, and(2) the abstract layer corresponding to Horn clauses, which is developed on top of the base layer at thegeneral level provided by the institution theory by adding proof rules for each sentence operator.
Definition 5.1. Let HI be a hybrid institution and SenHIb : SigHI → Set a sub-functor of SenHI . HI is a Hornhybrid institution over HIb = (SigHI , FHI , SenHIb , ModHI , KHI , |=HI ) if all sentences of HI consist of Horn clauses
over HIb , i.e. sentences constructed from the sentences of HIb by applying at most one time the following
sentence building operators: implication, store, universal quantification, necessity over binary modalities andretrieve, respectively.
Given a Horn hybrid institution HI over HIb and a signature ∆ ∈ |SigHI |, the most complex ∆-sentence is

14

D. Găină

V
χ
0
HI
0
of the form @k [λ](∀χ)(↓ j) H ⇒ C, where k ∈ Nom∆ , λ ∈ Λ∆
2 , ∆ → ∆ ∈ Q , j is a variable for F (∆ ),
HIb
HIb
0
0
H ⊆ Sen (∆ [j]) and C ∈ Sen (∆ [j]).
An example of Horn hybrid institution is HFOLSAh , the restriction of HFOLSA to Horn clauses over
HFOLSAb . Another example of Horn hybrid institution is HPLh , the restriction of HPL to Horn clauses
over HPLb .
Assumption 2. Throughout this paper, we assume that HI range over hybrid institutions satisfying anothermild property: given a signature ∆ and a variable j for (Nom∆ , Λ∆ ), a signature morphism ψ REL : (Nom∆ ∪{j}, Λ∆ ) → (Nom∆ , Λ∆ ) ∈ SigREL which preserves (Nom∆ , Λ∆ ) defines a signature morphism ψ : ∆[j] → ∆ ∈SigHI such that F(ψ) = ψ REL and χ[j]; ψ = 1∆ .
Assumptions 1 and 2 lead to the following lemma which is useful to prove results about sentences constructedwith store and retrieve.
Lemma 5.1. Let M be a ∆-model, where ∆ is a signature of some hybrid institution HI. Consider a nominalk ∈ Nom∆ , a variable j for (Nom∆ , Λ∆ ), and a signature morphism ψ REL : (Nom∆ ∪ {j}, Λ∆ ) → (Nom∆ , Λ∆ )such that (Nom∆ , Λ∆ ) is preserved and ψ REL (j) = k. Then the unique expansion of M along χ[j] which
satisfies j = k is the reduct of M along ψ (i.e. M (j,w) = M  ψ , where K∆ (M )k = w).
Proof. Note that K∆[j] (M  ψ ) = K∆ (M )  ψREL = K∆ (M )(j,w) . Since χ[j]; ψ = 1∆ , the model (M  ψ ) is a
χ[j]-expansion of M . Since M (j,w) is the unique χ[j]-expansion of M such that K∆[j] (M (j,w) ) = K∆ (M )(j,w) ,we have M  ψ = M (j,w) .

5.1. Plain Horn clauses
Let HI be a Horn hybrid institution over HIb such that HIb is closed to retrieve (i.e. @k ρ ∈ SenHIb (∆) forall ∆ ∈ |SigHI |, k ∈ Nom∆ and ρ ∈ SenHIb (∆)). We say that a Horn clause is plain if it is constructed fromthe sentences of HIb without necessity and retrieve. Let HIp be the restriction of HI to plain Horn clauses.
We will prove that HI and HIp have the same expressivity power by defining a hybrid substitution system
for HI that maps every Horn clause to a plain Horn clause. Consider the hybrid substitution system ΘHI
defined in Table 1. For the sake of simplicity, the cases where the sentences do not contain implication orquantification are omitted as these cases can be seen as instances of more complex cases which have been
considered. This is due to the fact that sentences of the form ∅ ⇒ C and (∀1∆ )ρ are semantically equivalent
to C and ρ, respectively.
Proposition 5.2. ΘHI is a hybrid substitution system.
Proof. Given a Horn clause ρ, a model M , and a state w of M , one needs to show that M |=w ρ iff
M |=w ΘHI (ρ) by taking into account all six cases considered in Table 1. See Section A for full proof.
Fact 5.3. Notice that ΘHI∆ (ρ) is a plain Horn clause for all Horn clauses ρ.
Fact 5.3 and Proposition 5.2 show that HI and HIp have the same expressivity power. If we define anentailment system for HIp then we obtain an entailment system for HI by adding (SubstΘHI ) proof rules.
Moreover, soundness and completeness can be extended from HIp to HI using Proposition 4.9.

5.2. Birkhoff entailment systems
Consider a Horn hybrid institution HI over HIb such that HIb is closed to retrieve, and an entailment system
E HIb = (SigHI , SenHIb , `HIb ) for HIb .
Definition 5.2. E HIp = (SigHI , SenHIp , `HIp ) is the least entailment system over E HIb closed to the proof
rules defined in Table 2.
Soundness and compactness can be prove directly without any extra assumptions.
Theorem 5.4.
(1) E HIp is sound if E HIb is sound, andBirkhoff style calculi for hybrid logics

15

Table 1. Hybrid substitution system for Birkhoff institutions(1) ΘHI∆ (γ)=γ for all γ ∈ SenHIp (∆),

V(2) ΘHI∆ ([λ](∀χ)(↓ j)( H ⇒ C))=(∀χ)(∀χ[j])(↓ j1 )(λ(j1 , j) ∧^χ[j1 ](@j h) ⇒ χ[j1 ](@j C)),h∈H

where j1 is a new variable,
V 00(3) ΘHI∆ ([λ](∀χ)( H ⇒ C ))=^(∀χ)(∀χ[j])(↓ j1 )(λ(j1 , j) ∧(χ[j]; χ[j1 ])(@j h0 ) ⇒ (χ[j]; χ[j1 ])(@j C 0 )),h0 ∈H 0where j1 is a new variable,(4) ΘHI∆ (@k ((∀χ)(↓ j)(V

H ⇒ C)))=^@k0 ψ(h) ⇒ @k0 ψ(C)),
h∈Hwhere k0 = F(χ)(k),(∀χ)(ψ REL : F(∆0 )[j] → F(∆0 ) preserves F(∆0 ), andψ REL (j) = k0 ,(5) ΘHI∆ (@k ((∀χ)(

V

H 0 ⇒ C 0 )))

=

(∀χ)(

^

@k0 h0 ⇒ @k0 C 0 ),h0 ∈H 0where k0 = F(χ)(k),(6) ΘHI∆ (@k [λ]γ)

=

HI
ΘHI
∆ (@k Θ∆ ([λ]γ)).

(2) E HIp is compact if E HIb is compact.
Proof. For soundness, it suffices to prove that the proof rules in Table 2 are sound. For compactness, let
E c = (SigHI , SenHIp , `c ) be the compact entailment subsystem of E HIp . Since E HIb is compact, it suffices toprove that E c is closed to the proof rules defined in Tabel 2. See Section A for full proof.
For completeness, supplementary assumptions based on institution-independent concepts defined in Section 4 are needed.
Theorem 5.5. Assume a hybrid substitution functor HSt : D → CATop for HIb such that QHI ⊆ D. The
entailment system E HIp is complete if(1) each set of HIb sentences is basic and has a basic model that is reachable, and(2) E HIb is complete and compact.
Proof. We will focus on the most complex case as the remaining cases can be proved similarly. We assumeVχthat Γ |= (∀χ)(↓ j)( H ⇒ C), where ∆ → ∆0 ∈ QHI .
V
Suppose towards a contradiction that Γ 6`V(∀χ)(↓ j)( H ⇒ C). In what follows, we construct a model
M such that M |=HI Γ and MV6|=HI (∀χ)(↓ j)( H ⇒ C). This is a contradiction with the initial assumption,
which implies Γ ` (∀χ)(↓ j)( H ⇒ C).
S
Let Γb be the set of all HIb sentences entailed by (χ; χ[j])(Γ) and h∈H @j h, i.e. Γb = {ρ ∈ SenHIb (∆0 [j]) |S(χ; χ[j])(Γ) ∪ ( h∈H @j h) ` ρ}. Let M b be a basic model of Γb that is reachable. It is straightforward toshow that(1) Γb 6` @j C, andS(2) M b |=HI (χ; χ[j])(Γ) ∪ ( h∈H @j h).
b
HI
b
HI
By
Γb 6|= @j C,
j C. By (2), M |=V and by Lemma 4.7, M 6|= b @HI
S (1) and completeness of bHIb , we haveHI(∀χ)(↓ j)( H ⇒ C). By (2), we have M |= (χ; χ[j])(Γ), whichh∈H @j h, which implies M  (χ;χ[j]) 6|=
implies M b  (χ;χ[j]) |=HI Γ. See Section A for full proof.

The entailment system of the institution HI is obtained by adding the proof rules (SubstΘHI ) to thecalculus for HIp .

16

D. Găină

Table 2. Plain Birkhoff calculus^

χ[j](Γ) `∆0 [j](Generalisation)(@j h) ⇒ (@j C)h∈HVΓ `∆ (∀χ)(↓ j)( H ⇒ C)^Γ `∆ (∀χ)(↓ j)( H ⇒ C)^
χ[j](Γ) `∆0 [j](@j h) ⇒ (@j C)h∈H(Quantif ication)(Substitutivity)Vχ(Γ) `∆0 H 0 ⇒ C 0
VΓ `∆ (∀χ)( H 0 ⇒ C 0 )VΓ `∆ (∀χ)( H 0 ⇒ C 0 )V 0χ(Γ) `∆0 H ⇒ C 0^^(∀χ)(↓ j)( H ⇒ C) `∆θ(@j h) ⇒ θ(@j C)h∈H

where θ : (χ; χ[j]) → 1∆
VV
where θ0 : χ → 1∆(∀χ)( H 0 ⇒ C 0 ) `∆ θ0 (H 0 ) ⇒ θ0 (C 0 )^(@k e) ⇒ (@k ρ)Γ`e∈E(Implication)Γ∪([@k e) ` (@k ρ)

e∈E

Γ∪(

[

@k e) ` (@k ρ)

e∈E

Γ`

^

(@k e) ⇒ (@k ρ)e∈E(Retrieve)

V

E⇒ρ`

^

(@k e) ⇒ (@k ρ)e∈EDefinition 5.3. E HI = (SigHI , SenHI , `HI ) is the least entailment system over E HIb closed to the proof rules
defined in Table 2 and (SubstΘHI ), where ΘHI is defined in Table 1.
Soundness and compactness are direct consequences of Proposition 4.9 and Theorem 5.4.
Theorem 5.6 (Birkhoff soundness).
(1) E HI is sound if E HIb is sound, and(2) E HI is compact if E HIb is compact.
Completeness is a corollary of Proposition 4.9, Theorem 5.4 and Theorem 5.5.
Theorem 5.7 (Birkhoff Completeness). Consider a subcategory of signature morphisms D such that
QHI ⊆ D, and let HSt : D → CATop be a hybrid substitution functor for HIb such that (1) each set of sentencesof HIb is basic and has a basic model that is HSt-reachable, and (2) E HIb is complete and compact. Then E HI
is complete.
Proof. By Theorem 5.4, E HIp is compact, and By Theorem 5.5, E HIp is complete. For all ∆ ∈ |SigHI | andHIpρ ∈ SenHI (∆) we have ΘHI(∆). By Proposition 4.9, E HI is complete.
∆ (ρ) ∈ Sen

Birkhoff style calculi for hybrid logics

17

Table 3. Hybrid system for HPLb
HPLb

(ρ)

= ρ for all ρ ∈ SenHPL0 (∆),

HPLb(@k (k1 = k2 ))= (k1 = k2 ),HPLb(@k λ(k1 , . . . , kn ))= λ(k1 , . . . , kn ),HPLb(@k1 @k2 γ)= @k2 γ for all γ ∈ SenHPLb (∆).

Θ∆

Θ∆
Θ∆
Θ∆

Table 4. Proof rules for HPL0
(Ref lexivity)(T ransitivity)Γ ` k1 = k1
Γ ` k1 = k2 and Γ ` k2 = k3
Γ ` k1 = k3

(Symmetry)Γ ` k1 = k2
Γ ` k2 = k1

(Congruence)Γ ` λ(k1 , . . . , kn ) and Γ ` ki = ki0 for all i ∈ {1, . . . , n}0 )
Γ ` λ(k10 , . . . , kn

(Congruencep )Γ ` k1 = k2 and Γ ` @k1 p
Γ ` @k2 p

6. Instances of Birkhoff entailment systems
In order to develop concrete sound and complete Birkhoff entailment systems we need to set the parametersof the completeness theorem for each example.

6.1. Birkhoff entailment system for HPL
We set the parameters of the completeness theorem for HPL as follows:• the institution HI is HPLh ,• the institution HIb is HPLb , and• the functor HSt : D → CATop is HStHPLb : DHPL → CATop , the restriction of HStHPL : DHPL → CATop(defined in Example 3.9) to HPLb .
Let HPL0 be the restriction of HPL to nominal equations, nominal relations and sentences of the form
@k p, where k is a nominal and p is a propositional symbol. We show that HPL0 has the same expressivity
power as HPLb by defining a hybrid substitution system for HPLb that maps each sentence of HPLb to asentence of HPL0 . The hybrid substitution system ΘHPLb for HPLb is defined in Table 3.
Proposition 6.1. ΘHPLb is a hybrid substitution system.
Proof. Straightforward.
We define an entailment system for HPL0 , and we prove its soundness, compactness and completeness.
Definition 6.1. E HPL0 = (SigHPL , SenHPL0 , `HPL0 ) is the least entailment system of HPL0 closed to theproof rules defined in Table 4.
Theorem 6.2. E HPL0 is sound, compact and complete.

18

D. Găină

Proof. The proof of soundness is straightforward as it is easy to show that the proof rules defined in Table 4
are sound.
For compactness, let E c = (SigHPL , SenHPL0 , `c ) be the compact entailment subsystem of E HPL0 . We
prove that E c is closed to the proof rules defined in Table 4, which implies E HPL0 = E c . For (Ref lexivity),Γ `c (k1 = k1 ) as for any finite Γf ⊆ Γ we have Γf `c (k1 = k1 ). For (Symmetry), assume that Γ `c (k1 =k2 ); there exists Γf ⊆ Γ such that Γf ` (k1 = k2 ), which implies Γf ` (k2 = k1 ), and we get Γ `c (k2 = k1 ).
The remaining cases can be proved similarly.
For completeness, we assume that Γ |=∆ ρ, where ∆ = (Nom, Λ, Prop). We construct a ∆-model (W Γ , M Γ )such that (a) (W Γ , M Γ ) |=HPL Γ and (b) (W Γ , M Γ ) |=HPL ρ iff Γ ` ρ. The ∆-model (W Γ , M Γ ) is defined
as follows:(1) |W Γ | = Nom/≡Γ , where ≡Γ = {(k1 , k2 ) | Γ ` k1 = k2 },b(2) WλΓ = {(kb1 , . . . , kcn ) | Γ ` λ(k1 , . . . , kn )} for all n ∈ Nat and λ ∈ Λn , where ki is the equivalence class ofki ,(3) the Prop-model MbkΓ interprets p ∈ Prop as true iff Γ ` @k p, where k ∈ Nom.
Since Γ |= ρ and (W Γ , M Γ ) |=HPL Γ, we have (W Γ , M Γ ) |=HPL ρ, which implies Γ ` ρ. See Section A for
full proof of completeness.
By adding the proof rules (SubstΘHPLb ) to the entailment system of HPL0 , we obtain an entailment system
for HPLb .
Definition 6.2. E HPLb = (SigHPL , SenHPLb , `HPLb ) is the least entailment system over E HPL0 closed tothe proof rules (SubstΘHPLb ), where ΘHPLb is defined in Table 3.
The following result is a corollary of Proposition 4.9 and Theorem 6.2.
Theorem 6.3. E HPLb is sound, complete and compact.
Proof. By noting that Θ∆ (γ) ∈ SenHPL0 (∆) for all ∆ ∈ |SigHPL | and γ ∈ SenHPLb (∆).
We can define now the Birkhoff entailment system for HPLh .
Definition 6.3. E HPLh = (SigHPL , SenHPLh , `HPLh ) is the least entailment system closed to the proof
rules defined in Table 2, (SubstΘHPLb ), where ΘHPLb is defined in Table 3, and (SubstΘHPLh ), where ΘHPLh
is defined in Table 1.
Theorem 6.4. E HPLh is sound, compact and complete.
Proof. By Theorem 6.3, E HPLb is sound and compact. By Theorem 5.6, E HPLh is sound and compact.
By Theorem 6.3, E HPLb is complete and compact. By Proposition 4.6, any set of sentences in HPLb is
epi-basic, and the basic models are HStHPL -reachable. In particular, the basic models are HStHPLb -reachable.
By Theorem 5.7, the entailment system E HPLh is complete.

6.2. Birkhoff entailment system for SHARE
Our abstract completeness result is not applicable to HFOLSA without any restriction, as our framework
does not allow equality of elements that originate from different states. For example, given a non-rigid
constant σ of non-rigid sort and two nominals k1 and k2 , if k1 = k2 is deducible then there is no way toinfer that σk1 is equal to σk2 as σk1 = σk2 is not an equation in our framework. We can either restrict thesignatures such that all sorts are rigid, or eliminate nominal equations. In this subsection we consider the
first case.
We set the parameters of the completeness theorem for SHARE as follows:• the institution HIb is SHAREb , where SHAREb is the restriction of SHARE to sentences obtained byapplying the operator retrieve to atomic sentences, nominal equations and nominal relations,• the institution HI is SHAREh , the restriction of SHARE to Horn clauses over SHAREb , and• the functor HSt : D → CATop is HStSHAREb : DSHAREb → CATop , the restriction of HStHFOLSA :DHFOLSA → CATop (defined in Example 3.8) to SHAREb .

Birkhoff style calculi for hybrid logics

19

Table 5. Hybrid substitution system for SHAREb
SHAREb(ρ)= ρ for all ρ ∈ SenSHARE0 (∆),

SHAREb(@k γ)= γ for all γ ∈ SenSHAREb (∆),

Θ∆
Θ∆

Table 6. Calculus for SHAREb(Ref lexivityn )(T ransitivityn )Γ ` k1 = k1
Γ ` k1 = k2 and Γ ` k2 = k3
Γ ` k1 = k3

(Symmetryn )Γ ` k1 = k2
Γ ` k2 = k1

(Congruencen )Γ ` λ(k1 , . . . , kn ) and Γ ` ki = ki0 for all i ∈ {1, . . . , n}0 )
Γ ` λ(k10 , . . . , kn

(Ref lexivity)(Symmetry)(T ransitivity)(Share)(Congruence)Γ ` t = t0
Γ ` t = t0
Γ ` t0 = t
Γ ` t = t0 and Γ ` t0 = t00
Γ ` t = t00
Γ ` τ =k τ 0Γ ` τ =k 0 τ 0Γ ` k = k0 and Γ ` ti = t0i for all i ∈ {1, . . . , n}
, where σ ∈ (F − F r )Γ ` σk (t1 , . . . , tn ) = σk0 (t01 , . . . , t0n )Γ ` τi = τi0 for all i ∈ {1, . . . , n}
, where ς ∈ F rΓ ` ς(τ1 , . . . , τn ) = ς(τ10 , . . . , τn0 )(Congruencep )Γ ` πk (t1 , . . . , tn ), Γ ` k = k0 and Γ ` ti = t0i for all i ∈ {1, . . . , n}
, where π ∈ (P − P r )Γ ` πk0 (t01 , . . . , t0n )Γ ` $(τ1 , . . . , τn ) and Γ ` τi = τi0 for all i ∈ {1, . . . , n}
, where $ ∈ P r
Γ ` $(τ10 , . . . , τn )λ is a modality, k, k0 and ki are nominals, t, ti , t0 , t0i and t00 are any terms, and τ , τi , τ 0 , τi0 are rigid terms.

Let SHARE0 be the restriction of SHARE to atomic sentences, nominal equations and nominal relations. We show that SHARE0 has the same expressivity power as SHAREb by defining a hybrid substitution system for SHAREb that maps each sentence of SHAREb to a sentence of SHARE0 . The hybrid
substitution system ΘSHAREb for SHAREb is defined in Table 5.
Proposition 6.5. ΘSHAREb is a hybrid substitution system.
Proof. Straightforward.
We define an entailment system for SHARE0 , and we prove its soundness, compactness and completeness.
Definition 6.4. E SHARE0 = (SigSHARE , SenSHARE0 , `SHARE0 ) is is the least entailment system of SHARE0
closed to the proof rules defined in Table 6.

20

D. Găină

Theorem 6.6. E SHARE0 is sound, complete and compact.
Proof. The proof of soundness is straightforward.
For compactness, let E c = (SigSHARE , SenSHARE0 , `c ) be the compact entailment subsystem of E SHARE0 .
We prove that E c is closed to the proof rules defined in Table 6, which implies E SHARE0 = E c . For(Ref lexivity), Γ `c t = t as for any finite Γf ⊆ Γ we have Γf `c t = t. For (Symmetry), assume thatΓ `c t = t0 ; there exists Γf ⊆ Γ such that Γf ` t = t0 , which implies Γf ` t0 = t, and we get Γ `c t0 = t. The
remaining cases can be proved similarly.
For completeness, we assume that Γ |=∆ ρ, where ∆ = (Nom, Λ, Σ) ∈ |SigSHARE | and Σ = (S, F r , P r ) ⊆(S, F, P ) ∈ |SigFOLS |. We construct a ∆-model (W Γ , M Γ ) such that (a) (W Γ , M Γ ) |=SHARE Γ and(b) (W Γ , M Γ ) |=SHARE ρ iff Γ ` ρ. Let ≡Nom = {(k1 , k2 ) | Γ ` k1 = k2 and ki ∈ Nom} be an equivalence on Nom. Let ≡k = {(t1 , t2 ) | Γ ` t1 = t2 and ti ∈ Tk∆ } be a congruence on the (S, F, P )-model Tk∆ ,where k ∈ Nom is a nominal. The ∆-model (W Γ , M Γ ) is defined as follows:b(1) |W Γ | = Nom/≡Nom and WλΓ = {(kb1 , . . . , kcn ) | Γ ` λ(k1 , . . . , kn )} for all n ∈ Nat and λ ∈ Λn , where ki isthe equivalence class of ki , and(2) for each k ∈ Nom, MbkΓ consists of the (S, F )-algebra Tk∆ /≡k , and interprets(a) each $ ∈ P r as (MbkΓ )$ = {(τb1 , . . . , τbn ) | Γ ` $(τ1 , . . . , τn )}, and(b) each π ∈ (P − P r ) as (MbkΓ )π = {(tb1 , . . . , tbn ) | Γ ` πk (t1 , . . . , tn )},where τbi and tbi are the equivalence classes of τi and ti , respectively.
Since Γ |= ρ and (W Γ , M Γ ) |=SHARE Γ, we have (W Γ , M Γ )SHARE |= ρ, which implies Γ ` ρ. See Section A
for full proof of completeness.
The following result is a corollary of Proposition 4.9 and Theorem 6.6.
Theorem 6.7. E SHAREb is sound, compact and complete.
b
Proof. By noting that for all ∆ ∈ |SigSHARE | and γ ∈ SenSHAREb (∆) we have ΘSHARE(γ) ∈ SenSHARE0 (∆).
∆

We can define now the Birkhoff entailment system for SHAREh .
Definition 6.5. E SHAREh = (SigSHARE , SenSHAREh , `SHAREh ) is the least entailment system of SHAREhclosed to the proof rules defined in Table 2 and Table 6, (SubstΘSHAREb ), where ΘSHAREb is defined in Table 5, and (SubstΘSHAREh ), where ΘSHAREh is defined in Table 1.
Theorem 6.8. E SHAREh is sound, compact and complete.
Proof. By Theorem 6.7, E SHAREb is sound and compact. By Theorem 5.6, E SHAREh is sound and compact.
By Theorem 6.7, E SHAREb is complete and compact. By Proposition 4.5, any set of sentences in HFOLSAb
is epi-basic and the basic models are HStHFOLSA -reachable. In particular, any set of sentences in SHAREb
is epi-basic and the basic models are HStSHAREb -reachable. By Theorem 5.7, E SHAREh is complete.

6.3. Birkhoff entailment system for HFOLSA
We set the parameters of the completeness theorem for HFOLSA as follows:• the institution HIb is HFOLSA0b , where HFOLSA0b is the restriction of HFOLSA to sentences obtainedby applying the operator retrieve to atomic sentences and nominal relations,• the institution HI is HFOLSA0h , the restriction of HFOLSA to Horn clauses over HFOLSA0b , and0• the functor HSt : D → CATop is HStHFOLSAb : DHFOLSA → CATop , the restriction of HStHFOLSA :DHFOLSA → CATop (defined in Example 3.8) to HFOLSA0b .
Let HFOLSA00 be the restriction of HFOLSA to atomic sentences and nominal relations. We show that
HFOLSA00 has the same expressivity power as HFOLSA0b by defining a hybrid substitution system for
HFOLSA0b that maps each sentence of HFOLSA0b to a sentence of HFOLSA00 . The hybrid substitution
0
system ΘHFOLSAb for HFOLSA0b is defined in Table 7.

Birkhoff style calculi for hybrid logics

21

Table 7. Hybrid substitution system for HFOLSA0b
HFOLSA0b

Θ∆

HFOLSA0b

Θ∆

0

(ρ)

= ρ for all ρ ∈ SenHFOLSA0 (∆),(@k γ)= γ for all γ ∈ SenHFOLSAb (∆),

0

Table 8. Calculus for HFOLSA0b(Ref lexivity)(Symmetry)(T ransitivity)(Share)(Congruence)Γ ` t = t0
Γ ` t =k t0
Γ ` t0 = t
Γ ` t = t0 and Γ ` t0 = t00
Γ ` t = t00
Γ ` τ =ksr τ 0, where sr is a rigid sortΓ ` τ =ksr0 τ 0Γ ` ti = t0i for all i ∈ {1, . . . , n}
, where σ ∈ (F − F r )Γ ` σk (t1 , . . . , tn ) = σk (t01 , . . . , t0n )Γ ` τi = τi0 for all i ∈ {1, . . . , n}
, where ς ∈ F rΓ ` ς(τ1 , . . . , τn ) = ς(τ10 , . . . , τn0 )(Congruencep )Γ ` πk (t1 , . . . , tn ) and Γ ` ti = t0i for all i ∈ {1, . . . , n}
, where π ∈ (P − P r )Γ ` πk (t01 , . . . , t0n )Γ ` $(τ1 , . . . , τn ) and Γ ` τi = τi0 for all i ∈ {1, . . . , n}
, where $ ∈ P r
Γ ` $(τ10 , . . . , τn )k and k0 are nominals, t, ti , t0 , t0i and t00 are terms, and τ , τi , τ 0 and τi0 are rigid terms.
0

Proposition 6.9. ΘHFOLSAb is a hybrid substitution system.
Proof. Straightforward.
We define an entailment system for HFOLSA00 , and we prove its soundness, compactness and completeness.
00

0Definition 6.6. E HFOLSA0 = (SigHFOLSA , SenHFOLSA0 , `HFOLSA0 ) is is the least entailment system of
HFOLSA00 closed to the proof rules in Table 8.
0

Theorem 6.10. E HFOLSA0 is sound, complete and compact.
Proof. The proof is similar to the proof of Theorem 6.6.
0

0

0

Definition 6.7. E HFOLSAb = (SigHFOLSA , SenHFOLSAb , `HFOLSAb ) is the least entailment system over0
0
E HFOLSA0 closed to (SubstΘHFOLSA0b ), where ΘHFOLSAb is defined in Table 7.
The following result is a corollary of Proposition 4.9 and Theorem 6.10.
0Theorem 6.11. E HFOLSAb is sound, complete and compact.
HFOLSA0b

Proof. By noting that Θ∆00(γ) ∈ SenHFOLSA0 (∆) for all ∆ ∈ |SigHFOLSA | and γ ∈ SenHFOLSAb (∆).

22

D. Găină

We can define now the Birkhoff entailment system for HFOLSA0h .
000

Definition 6.8. E HFOLSAh = (SigHFOLSA , SenHFOLSAh , `HFOLSAh ) is the least entailment system of0
HFOLSA0h closed to the proof rules defined in Table 2 and Table 8, (SubstΘHFOLSA0b ), where ΘHFOLSAb is0defined in Table 7, and (SubstΘHFOLSA0h ), where ΘHFOLSAh is defined in Table 1.
0

Theorem 6.12. E HFOLSAh is sound, compact and complete.
00

Proof. By Theorem 6.11, E HFOLSAb is sound and compact. By Theorem 5.6, E HFOLSAh is sound andcompact.
0
By Theorem 6.11, E HFOLSAb is complete and compact. By Proposition 4.5, any set of sentences in0
HFOLSAb is epi-basic and the basic models are HStHFOLSA -reachable. In particular, the basic models are
0
0
HStHFOLSAb -reachable. By Theorem 5.7, E HFOLSAh is complete.

7. Conclusions
We have proved a Birkhoff completeness theorem for hybrid logics in the general setting of the institution
theory. We have instantiated the result to hybrid propositional logic (HPL) and hybrid first-order logic withuser-defined sharing and annotation (HFOLSA). The former result comes in two variants. For the first case,the signatures are restricted such that all sorts are rigid, which implies that models share the same carrier
sets across the states. The second case excludes nominal equations from the syntax. The abstract result
is applicable also to hybrid first-order logic (HFOL), similarly to the case of HPL, and hybrid preorderalgebra with user-defined sharing and annotation (HPOASA), similarly to the case of HFOLSA. Manyother instances are expected to the hybridization of unconventional logics used in computer science such asorder-sorted algebra [GM92], partial algebra [ABK+ 02] or higher-order logic [Hen50] with intensional Henkin
semantics.
The definition of hybrid institution provides a more general framework than the hybridization process[MMDB11, Dia16b, DM16], since the hybrid framework is assumed and not constructed. As a result, hybrid
institutions with annotation syntax, such as HFOLSA, are not instances of the hybridization but they fall
into our framework. hybridization is a method of hierarchical logic combination but it is different from fibring [CCG+ 08] (which is the major general theory of logic combination in the mathematical logic literature);a discussion comparing them is outside the scope of our paper.
The temporalization method of Finger and Gabbay [FG92] is a simplified version of hybridization performed with different sentence operators, where signature morphisms and homomorphisms are not considered.
The work reported in [FG92] proves that soundness and completeness are preserved from the base logic to thetemporalized version. A similar result is obtained for the abstract framework provided by the hybridization
process [NMMB16]. Both papers, [FG92] and [NMMB16], do not consider quantified formulas for the logic
construction method and are not concerned with extracting a fragment with good computational properties.
The operator retrieve is essential for proving our completeness property, which shows that our results may
not be applicable to pure modal logics. By defining an abstract notion of Horn clause, the present work shows
how to extract a fragment with good computational properties from a hybrid logic. The Birkhoff entailment
system opens the possibility to perform theorem proving based on term rewriting [Gog94] in hybrid logics.
In the future we are planning to develop o methodology for proving properties of reconfigurable softwaresystems that are described with hybrid logics. An interesting research topic is borrowing interpolation fromfirst-order logics to hybrid logics in the style of [Dia12] or [G1̆3].

References[AB01][ABK+ 02]
[AD07]

Carlos Areces and Patrick Blackburn. Bringing them all Together. Journal of Logic and Computation, 11(5):657–
669, 2001.
Egidio Astesiano, Michel Bidoit, Hélène Kirchner, Bernd Krieg-Brückner, Peter D. Mosses, Donald Sannella,and Andrzej Tarlecki. CASL: the Common Algebraic Specification Language. Theoretical Computer Science,
286(2):153–196, 2002.
Marc Aiguier and Razvan Diaconescu. Stratified institutions and elementary homomorphisms. Information Processing Letters, 103(1):5–13, 2007.

Birkhoff style calculi for hybrid logics[Béz06][Béz12][Bir35]23

Jean-Yves Béziau. 13 questions about universal logic. Bulletin of the Section of Logic, 35(2/3):133–150, 2006.
Jean-Yves Béziau. Universal Logic: An Anthology: from Paul Hertz to Dov Gabbay. Birkhäuser, 2012.
Garrett Birkhoff. On the structure of abstract algebras. Mathematical Proceedings of the Cambridge PhilosophicalSociety, 31:433–454, October 1935.
[Bla00]Patrick Blackburn. Representation, reasoning, and relational structures: a hybrid logic manifesto. Logic Journalof the IGPL, 8(3):339–365, 2000.
[BM02]
Patrick Blackburn and Maarten Marx. Tableaux for Quantified Hybrid Logic. In Uwe Egly and Christian 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.
[Bra11]
Torben Braüner. Hybrid logic and its Proof-Theory, volume 37 of Applied Logic Series. Springer, 2011.
[CCG+ 08] Walter Carnielli, Marcelo Coniglio, Dov M. Gabbay, Paula Gouveia, and Cristina Sernadas. Analysis and Synthesis
of Logics - How To Cut And Paste Reasoning Systems. Applied Logic Series. Springer, 2008.
[cF15]
Ionut Ţuţu and José Luiz Fiadeiro. Revisiting the Institutional Approach to Herbrand’s Theorem. In Lawrence S.
Moss and Pawel Sobocinski, editors, 6th Conference on Algebra and Coalgebra in Computer Science, CALCO
2015, June 24-26, 2015, Nijmegen, The Netherlands, volume 35 of LIPIcs, pages 304–319. Schloss Dagstuhl Leibniz-Zentrum fuer Informatik, 2015.
[CG08]
Mihai Codescu and Daniel Găină. Birkhoff completeness in institutions. Logica Universalis, 2(2):277–309, 2008.
[DF02]
Razvan Diaconescu and Kokichi Futatsugi. Logical foundations of CafeOBJ. Theoretical Computer Science,
285(2):289–318, 2002.
[Dia03]Răzvan Diaconescu. Institution-independent Ultraproducts. Fundamenta Informaticæ, 55(3-4):321–348, 2003.
[Dia04]
Razvan Diaconescu. Herbrand theorems in arbitrary institutions. Information Processing Letters, 90(1):29–37,
2004.
[Dia06]Răzvan Diaconescu. Proof systems for institutional logic. Journal of Logic and Computation, 16(3):339–357, 2006.
[Dia08]Răzvan Diaconescu. Institution-independent Model Theory. Studies in Universal Logic. Birkhäuser Basel, 1 edition,
2008.
[Dia12]
Razvan Diaconescu. Borrowing interpolation. Journal of Logic and Computation, 22(3):561–586, 2012.
[Dia16a]Răzvan Diaconescu. Implicit Kripke Semantics and Ultraproducts in Stratified Institutions. Journal of Logic andComputation, DOI:10.1093/logcom/exw018, 2016.
[Dia16b]Răzvan Diaconescu. Quasi-varieties and initial semantics for hybridized institutions. Journal of Logic and Computation, 26(3):855–891, 2016.
[DM16]Răzvan Diaconescu and Alexandre Madeira. Encoding hybridized institutions into first-order logic. Mathematical
Structures in Computer Science, 26(5):745–788, 2016.
[FG92]
Marcelo Finger and Dov M. Gabbay. Adding a temporal dimension to a logic system. Journal of Logic, Language
and Information, 1(3):203–233, 1992.
[GB92]
Joseph Goguen and Rod Burstall. Institutions: Abstract model theory for specification and programming. Journalof the Association for Computing Machinery, 39(1):95–146, 1992.
[GFO12]
Daniel Găină, Kokichi Futatsugi, and Kazuhiro Ogata. Constructor-based Logics. J. UCS, 18(16):2204–2233, 2012.
[GM85]
Joseph Goguen and Jose Meseguer. Completeness of many-sorted equational logic. Houston Journal of Mathematics, 11(3):307–334, 1985.
[GM92]
Joseph A. Goguen and José Meseguer. Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance,
Overloading, Exceptions and Partial Operations. Theoretical Computer Science, 105(2):217–273, 1992.
[Gog94]
Joseph Goguen. Theorem Proving and Algebra. https://cseweb.ucsd.edu/ goguen/pubs/tp.html, 1994.
[GP10]
Daniel Găină and Marius Petria. Completeness by forcing. Journal of Logic and Computation, 20(6):1165–1186,
2010.
[G1̆3]
Daniel Găină. Interpolation in logics with constructors. Theoretical Computer Science, 474:46–59, 2013.
[G1̆5a]Daniel Găină. Downward Löwenheim-Skolem Theorem and interpolation in logics with constructors. Journal of
Logic and Computation, DOI:10.1093/logcom/exv018, May 2015.
[G1̆5b]Daniel Găină. Foundations of Logic Programming in Hybrid Logics with user-defined Sharing, 2015. submitted.
[G1̆5c]Daniel Găină. Foundations of Logic Programming in Hybridised Logics. In Mihai Codescu, Răzvan Diaconescu,
and Ionuţ Ţuţu, editors, Recent Trends in Algebraic Development Techniques - 22nd International Workshop,
WADT 2014, Sinaia, Romania, September 4-7, 2014. Proceedings, volume 9463 of Lecture Notes in Computer
Science, pages 69–89. Springer, 2015.
[Hen50]
Leon Henkin. Completeness in the Theory of Types. Journal of Symbolic Logic, 15(2):81–91, 1950.
[Mad13]Alexandre Madeira. Foundations and techniques for software reconfigurability. PhD thesis, Universidades do
Minho, Aveiro and Porto, 2013. Joint MAP-i Doctoral Programme.
[Mes89]Joseph Meseguer. General logics. In H.-D. Ebbinghaus, J. Fernandez-Prida, M. Garrido, D. Lascar, and M. Rodriguez Artalejo, editors, Logic Colloquium ’87, volume 129 of Studies in Logic and the Foundations of Mathematics, pages 275–329. North Holland, 1989.
[MMBH15] Alexandre Madeira, Manuel A. Martins, Luı́s Soares Barbosa, and Rolf Hennicker. Refinement in hybridised
institutions. Formal Aspects of Computing, 27(2):375–395, 2015.
[MMDB11] Manuel A. Martins, Alexandre Madeira, Razvan Diaconescu, and Luı́s Soares Barbosa. Hybridization of institutions.
In Andrea Corradini, Bartek Klin, and Corina Cı̂rstea, editors, Algebra and Coalgebra in Computer Science - 4thInternational Conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Proceedings, volume6859 of Lecture Notes in Computer Science, pages 283–297. Springer, 2011.
[NMMB16] Renato Neves, Alexandre Madeira, Manuel A. Martins, and Luı́s Soares Barbosa. Proof theory for hybrid(ised)
logics. Science of Computer Programming, 126:73–93, 2016.

24[Pet07][Pri67][PT91][SC11][Sch11][Tar86a][Tar86b]

D. Găină

Marius Petria. An Institutional Version of Gödel’s Completeness Theorem. In Till Mossakowski, Ugo Montanari,and Magne Haveraaen, editors, Algebra and Coalgebra in Computer Science, Second International Conference,
CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings, volume 4624 of Lecture Notes in Computer
Science, pages 409–424. Springer, 2007.
Arthur Prior. Past, Present and Future. Oxford books. OUP Oxford, 1967.
Solomon Passay and Tinko Tinchev. An essay in combinatory dynamic logic. Information and Computation,
93(2):263–332, 1991.
Robert Szepesia and Horia Ciocârlie. An overview on software reconfiguration. Theory Appl. Math. Comput. Sci.,
1(1):74–79, 2011.
Gerhard Schurz. Combinations and completeness transfer for quantified modal logics. Logic Journal of the IGPL,
19(4):598–616, 2011.
Andrzej Tarlecki. Bits and Pieces of the Theory of Institutions. In David Pitt, Samson Abramsky, Axel Poigné,and David Rydeheard, editors, Proceedings, Summer Workshop on Category Theory and Computer Programming,
Lecture Notes in Computer Science, volume 240, pages 334–360. Springer, 1986.
Andrzej Tarlecki. Quasi-varieties in abstract algebraic institutions. Journal of Computer and System Sciences,33(3):333–360, 1986.

A. Exiled proofs
Proof of Proposition 5.2 We have six cases to consider. The first case γ ∈ SenHIp (∆) is trivial. The thirdcase and the fifth case are instances of the second case and the forth case, respectively. We will focus on the
non-trivial cases:V(2) Let M ∈ |Mod(∆)|, w1 ∈ |K∆ (M )|, and
W = K∆ (M ). Assuming M |=w1 [λ](∀χ)(↓ j)( H ⇒ C) we proveV
M |=w1 (∀χ)(∀χ[j])(↓ j1 )(λ(j1 , j) ∧ ( h∈H χ[j1 ](@j h)) ⇒ χ[j1 ](@j C)).
S
Let M 1 be a (χ; χ[j]; χ[j1 ])-expansion of M such that M 1 |=w1 λ(j1 , j), M 1 |=w1 h∈H χ[j1 ](@j h) and
Wj11 = w1 , where W 1 = K∆0 [j][j1 ] (M 1 ). Let M 0 = M 1  χ[j1 ] , W 0 = W 1  F(χ[j1 ]) = K∆0 [j] (M 0 ) and w =Wj1 = Wj0 . Since M 1 |=w1 λ(j1 , j), weVhave (Wj11 , Wj1 ) ∈ Wλ1 , i.e. (w1 , w) ∈ Wλ1 . Since Wλ1 = W
Vλ , we have
(w1 , w) ∈ Wλ . M |=w1 [λ](∀χ)(↓ j)( H ⇒ C)Sand (w1 , w) ∈ Wλ implies M |=w (∀χ)(↓ j)(
S H ⇒ C).
By the local satisfaction condition, M 1 |=w1 h∈H χ[j1 ](@j h) is equivalent to M 0 |=w1 h∈H @j h; it0follows that M 0 |=Wj H, i.e. M 0 |=w H. Since M 0 is a (χ; χ[j])-expansion of M such that Wj0 = w and0
M 0 |=w H, we have M 0 |=w C, i.e. M 0 |=Wj C; it follows that M 0 |=w1 @j C, and by the local satisfaction1
w1
condition, we get M |= χ[j1 ](@j C).
V
Assuming M V|=w1 (∀χ)(∀χ[j])(↓ j1 )(λ(j1 , j) ∧ ( h∈H χ[j1 ](@j h) ⇒ χ[j1 ](@j C)) we prove M |=w1[λ](∀χ)(↓ j)( H ⇒ C). Let w ∈ |W | such that (w1 , w) ∈ Wλ and consider a (χ; χ[j])-expansion
M 0 of M such that M 0 |=w H and Wj0 = w, where W 0 = K∆0 [j] (M 0 ). It follows that M 0 |=w1
SS
condition, we have M 0(j1 ,w1 ) |=w1 h∈H χ[j1 ](@j h). Sinceh∈H @j h, and by the local satisfactionV
M |=w1 (∀χ)(∀χ[j])(↓ j1 )(λ(j1 , j) ∧ h∈H χ[j1 ](@j h) ⇒ χ[j1 ](@j C)) and M 0(j1 ,w1 ) is a (χ; χ[j]; χ[j1 ])S
0(j ,w )expansion of M such that M 0(j1 ,w1 ) |=w1 λ(j1 , j), M 0(j1 ,w1 ) |=w1 h∈H χ[j1 ](@j h) and Wj1 1 1 = w1 ,we have M 0(j1 ,w1 ) |=w1 χ[j1 ](@j C). By the local satisfaction condition, we obtain M 0 |=w1 @j C, which0implies M 0 |=Wj C, i.e. M 0 |=w C.
(4) For all ∆-models M Vand states w ∈ |W |, where W =V
K∆ (M ), we have:
M |=w @k (∀χ)(↓ j)( H ⇒ C) iff M |=Wk (∀χ)(↓ j)( V H ⇒ C) iff
for all χ-expansions M 0 of M we have M 0 |=Wk (↓ j) H ⇒ C iff
V0
for all χ-expansions M 0 of M , M 0 |=Wk0 (↓ j) H ⇒ C, where W 0 = K∆0 (M 0 ) and k 0 = F(χ)(k) iff
00 V
for all χ-expansions M 0 of M , M 0(j,Wk0 ) |=Wk0 H ⇒ C, where W 0 = K∆0 (M 0 ) and k 0 = F(χ)(k).
By Lemma 5.1, the last statement is equivalent V
to the followings:
0
for all χ-expansions M 0 of M , M 0  ψ |=Wk0
H ⇒ C, where W 0 = K∆0 (M 0 ), k 0 = F(χ)(k) and
REL
0
0
0
REL
ψ
: F(∆ )[j] → F(∆ ) preserves F(∆ ) and ψ(j) = k 0 iff
V
Wk0 0
0
0
for all χ-expansions M of M , M |=ψ(H) ⇒ ψ(C), where W 0 = K∆0 (M 0 ), k 0 = F(χ)(k) and
REL
0
0
0
0
ψ
: F(∆ )[j] → F(∆ ) preserves F(∆ ) and ψ REL
V (j) = k iff
for all χ-expansions M 0 of M we have M 0 |=w h∈H @k0 ψ(h) ⇒ @k0 ψ(C), where k 0 = F(χ)(k) andψ REL : F(∆0 )[j] → F(∆0 ) preserves F(∆0 ) and ψ REL (j) = k 0 iff

Birkhoff style calculi for hybrid logics

25V
M |=w (∀χ) h∈H @k0 ψ(h) ⇒ @k0 ψ(C), where k 0 = F(χ)(k) and ψ REL : F(∆0 )[j] → F(∆0 ) preserves
F(∆0 ) and ψ REL (j) = k 0 .
(6) For all ∆-models M and states w ∈ |K∆ (M )| we have:
M |=w @k [λ]ρ iff M |=w @k Θ([λ]ρ) iff M |=w Θ(@k Θ([λ]ρ)).
Proof of Theorem 5.4(1) We show that the proof rules in Table 2 are
V sound.
V(Generalisation) : Assuming χ[j](Γ) |= h∈H (@j h) ⇒ (@j C) we prove Γ |= (∀χ)(↓ j)( H ⇒ C).
Let M be a ∆-model such that M |=HI Γ, and let w ∈ |W | be an arbitrary state, where W = K∆ (M ).
Consider a (χ; χ[j])-expansion M 0 of M such that Wj0 = w, where W 0 = K∆0 (M 0 ). By the satisfaction
V
condition, M 0 |=HI (χ; χ[j])(Γ). It follows that M 0 |=HI h∈H (@j h) ⇒ (@j C), which is equivalent toV0 V
M 0 |=Wj H ⇒ C. Hence,VM 0 |=w H ⇒ C.
V
Assuming Γ |= (∀χ)(↓ j)( H ⇒ C) we prove χ[j](Γ) |= h∈H (@j h) ⇒ (@j C). Let M 0 be a ∆0 [j]model such that M 0 |=HI χ[j](Γ). By the satisfaction condition, M 0  (χ;χ[j]) |=HI Γ, which implies M 0 VV0HI(∀χ)(↓ j)( H ⇒ C). We have M 0  (χ;χ[j]) |=Wj (∀χ)(↓ j)( H ⇒ C), where W 0 = K∆0 (M 0 ).
(χ;χ[j]) |=V
0 V
It follows that M 0 |=Wj H ⇒ C, which is equivalent to M 0 |=HI h∈H (@j h) ⇒ (@j C).
(Quantif ication) : This case is similar to
V the one above.
V(Substitutivity) : We proveV(∀χ)(↓ j)( H ⇒ C) |= h∈H θ(@j h) ⇒ θ(@j C). Let M be a ∆-modelsuch that M |=HI (∀χ)(↓ j)( H ⇒ C). Let w ∈ |W | be a state such that M |=w θ(@j h) for all h ∈ H,
where W = K∆ (M ). We show that M |=w θ(@j C). We denote M  θ and K∆0 [j] (M 0  θ ) by M 0 and W 0 ,0 V
respectively. Since M 0 is a (χ; χ[j])-expansion of M , we have M 0 |=Wj
H ⇒ C. By the satisfaction
0
condition for hybrid substitutions, M 0 |=w @j h for all h ∈ H, which is equivalent to M 0 |=Wj H. It follows
0that M 0 |=Wj C, which is equivalent to M 0 |=w @j C. By the satisfaction condition, M |=w θ(@j C).
The other subcase can be provedVsimilarly.
S(Implication) : Assuming Γ |=S e∈E (@k e) ⇒ (@k ρ) we prove Γ ∪ ( e∈EV@k e) |= @k ρ. Let M be a∆-model such that M |=HI Γ ∪ ( e∈E @k e). Since M |=HI Γ, we have M |=HI e∈E (@k e) ⇒ (@k ρ), whichSV
is equivalent to M |=Wk E ⇒ ρ, where W = K∆ (M ). Since M |=HI e∈E @k e, we get M |=Wk E. It
follows that M S|=Wk ρ. Hence, M |=HI @k ρ.
VAssuming Γ ∪ ( e∈E @k e) |= @k ρ we proveΓ |= e∈E (@k e) ⇒ (@k ρ). Let M be a ∆-modelSsuch thatSw
HI
M |=HI Γ. Let w ∈ |W | suche∈E @k e, where W = K∆ (M ). It follows that M |=e∈E @k e,
S that M |=HI
HIw
and we have M |= Γ ∪ ( e∈E @k e). We obtain (W, M ) |= @k ρ. Hence, M |= @k ρ.
(Retrieve) : Straightforward.
(2) Let E c = (SigHI , SenHIp , `c ) be the compact entailment subsystem of E HIp . We prove that E c is closed tothe proof rules defined in Tabel 2.
V(Generalisation) : Assume that χ[j](Γ)`c h∈H (@j h) ⇒ (@j C); by the definition of E c , thereVexistsVΓf ⊆ Γ finite such that χ[j](Γf ) `V h∈H (@j h) ⇒ (@j C); by (Generalisation),Γf ` (∀χ)(↓ j)( H ⇒VC), which implies Γ `c (∀χ)(↓ j)( H ⇒ C). Now, if Γ `cV(∀χ)(↓ j)( H ⇒ C) then by the definitioncof(∀χ)(↓ j)( H ⇒ C); by (Generalisation), χ[j](Γf ) `V E , there exists Γf ⊆ Γ finite such that Γf c` Vh∈H (@j h) ⇒ (@j C), which implies χ[j](Γ) `h∈H (@j h) ⇒ (@j C).
(Quantif ication): Can be proved similarly as above.
^^(Substitutivity) : By the definition of E c , we have (∀χ)(↓ j)( H ⇒ C) `cθ(@j h) ⇒ θ(@j C).
h∈HVc(Implication) : Assumeof E c , there exists Γf ⊆ Γe∈E (@k e) ⇒ (@k ρ); by the definition
V that Γ `SfiniteSsuch that Γf ` e∈E (@k e) ⇒S(@k ρ); by (Implication), Γf ∪ ( e∈E @k e) ` @k ρ, which impliesΓ ∪ ( e∈E @k e) `c @k ρ.SNow if, Γ ∪ ( e∈E @k e) `c @k ρ then by theVdefinition of E c , there exists Γf ⊆ Γ
finiteVsuch that Γf ∪ ( e∈E @k e) ` @k ρ; by (Implication), Γf ` e∈E (@k e) ⇒ (@k ρ), which impliesΓ `c e∈E (@k e) ⇒ (@k ρ).
(Retrive) : Straightforward.

26

D. Găină

Vχ
Proof of Theorem 5.5 We assume that Γ |= (∀χ)(↓ j)( H ⇒ C), where ∆ → ∆0 ∈ QHI , j is a nominal
HIb
HIb
HIp
0
0
variable, H ⊆VSen (∆ [j]), C ∈ Sen (∆ [j]) and Γ ⊆ Sen (∆). Suppose towards a contradiction that
Γ 6` (∀χ)(↓ j)( H ⇒ C).
S
We define Γb = {ρ ∈ SenHIb (∆0 [j]) | (χ; χ[j])(Γ) ∪ ( h∈H @j h) ` ρ}. We show that Γb 6`HIb @j C. IfHIbΓb `HIb @j C thenis compact, there exists Γf ⊆ Γb finite such that Γf S`HIb @j C; we have
S since E(χ; χ[j])(Γ) ∪ ( h∈H @j h) `S ρ for all ρ ∈ Γf , and since Γf is finite, (χ; χ[j])(Γ)
V ∪ ( h∈H @j h) ` Γf ; itfollows that (χ; χ[j])(Γ) ∪ ( h∈HV@j h) ` @j C; by (Implication), (χ; χ[j])(Γ) ` h∈H (@j h) ⇒ (@j C); by(Generalisation), Γ ` (∀χ)(↓ j)( H ⇒ C), which is a contradiction with our assumption.
Let M b be a basic model of Γb that is reachable. We denote K∆0 [j] (M b ) by W b . Since Γb 6`HIb @j C,
by completeness of E HIbS, we have Γb 6|= @j C, and by Lemma 4.7, we obtain M b 6|=HI @j C. We prove thatM b |=HI (χ; χ[j])(Γ) ∪ ( h∈H @j h):(a) For each h ∈ H, we have @j h ∈ Γb , which implies Γb |= @j h, and by Lemma 4.7, we get M b |=HI @j h.
Vχ1(b) Let (∀χ1 )(↓ j1 )( H1 ⇒ C1 ) ∈ (χ; χ[j])(Γ), where ∆0 [j] → ∆00 ∈ QHI , j1 is a variable for F(∆00 ), H1 ⊆
HIb
HIb
00
00
Sen (∆ [j1 ]) and C1 ∈ Sen (∆ [j1 ]). Let M be a (χ1 ; χ[j1 ])-expansion of M b such that M |=Wj1 H1 ,where W = K∆00 [j1 ] (M ). We show that M |=Wj1 C1 . Since M b is reachable, there exists a substitutionθ(χ1 ; χ[j1 ]) → 1∆0 [j] ∈ HSt(∆0 [j]) such that M b  θ = M .
/ Sen(∆00 )χ1Sen(∆0 [j]) lχ[j1 ]/ Sen(∆00 [j1 ])θ/ |Mod(∆00 [j1 ])| 3 Mθ

M b ∈ |Mod(∆0 [j])|lχ1 ;χ[j1 ]Since M |=Wj1 H1 , we have M |=HI @j1 h1 for all h1 ∈ H1 . By the satisfaction condition for substitutions,
M b |=HI θ(@j1 h1 ) for all h1 ∈ H1 , and by Lemma 4.7, Γb |= θ(@j1 h1 ) for all h1 ∈ H1 . It follows thatΓb |= @j θ(@j1 h1 ) forSall h1 ∈ H1 . By completeness of E HIb , Γb `HIb @j θ(@j1 h1 ) for all h1 ∈ H1 . Since
H1 is finite, Γb `HIb h1 ∈H1 @j θ(@j1 h1 ). By compactness of E HIb , there exists a finite set Γf ⊆ Γb such
S
S
that Γf `HIb S
h1 ∈H1 @j θ(@j1 h1 ). We have (χ; χ[j])(Γ) ∪ ( h∈H
S @j h) ` ρ for
S all ρ ∈ Γf , which implies(χ; χ[j])(Γ) ∪ ( h∈H @j h) ` Γf . It follows that (χ; χ[j])(Γ) ∪ ( h∈H @j h) ` h1 ∈H1 @j θ(@j1 h1 ), and weget(χ; χ[j])(Γ) ∪ ([[@j h) ` (χ; χ[j])(Γ) ∪ (h∈H[@j h) `@j θ(@j1 h1 ))(1)^

θ(@j1 h1 ) ⇒ θ(@j1 C1 ).

h1 ∈H1h∈H^[
h1 ∈H1h∈H

By (Substitutivity), (χ; χ[j])(Γ) ∪ (By (Retrieve),@j h) ∪ (^θ(@j1 h1 ) ⇒ θ(@j1 C1 ) `h1 ∈H1@j θ(@j1 h1 ) ⇒ @j θ(@j1 C1 ),h1 ∈H1

which implies (χ; χ[j])(Γ) ∪ ([@j h) `h∈H^@j θ(@j1 h1 ) ⇒ @j θ(@j1 C1 ).

h1 ∈H1By (Implication), we get(χ; χ[j])(Γ) ∪ ([h∈H@j h) ∪ ([@j θ(@j1 h1 )) ` @j θ(@j1 C1 )(2)

h1 ∈H1

By statements (1) and (2), (χ; χ[j])(Γ) ∪ (Sh∈H @j h) ` @j θ(@j1 C1 ), meaning that @j θ(@j1 C1 ) ∈ Γb .
b

We have Γb |= @j θ(@j1 C1 ), and by Lemma 4.7, M b |=HI @j θ(@j1 C1 ). It follows that M b |=Wj θ(@j1 C1 ),b
and by the local satisfaction condition, M |=Wj @j1 C1 . Hence, M |=Wj1 C1 .
V
We have M b  (χ;χ[j]) 6|=HI (∀χ)(↓ j)( H ⇒ C) as M b |=HI @j h for all h ∈ H and M b 6|=HI @j C. SinceBirkhoff style calculi for hybrid logics

27VM b  (χ;χ[j]) |=HI Γ, there isVa contradiction with the statement Γ |= (∀χ)(↓Vj)( H ⇒ C). It follows that theassumption Γ 6` (∀χ)(↓ j)( H ⇒ C) is not correct. Hence, Γ ` (∀χ)(↓ j)( H ⇒ C).
Proof of Theorem 6.2 We assume that Γ |=∆ ρ and we prove Γ `∆ ρ, where ∆ = (Nom, Λ, Prop). Let(W Γ , M Γ ) be the ∆-model such that(1) |W Γ | = Nom/≡Γ , where ≡Γ = {(k1 , k2 ) | Γ ` k1 = k2 },b(2) WλΓ = {(kb1 , . . . , kcn ) | Γ ` λ(k1 , . . . , kn )} for all n ∈ Nat and λ ∈ Λn , where ki is the equivalence class ofki ,(3) the Prop-model MbkΓ interprets p ∈ Prop as true iff Γ ` @k p, where k ∈ Nom.
By (Ref lexivity), (Symmetry) and (T ransitivity), the relation ≡Γ is an equivalence on Nom. By (Congruence),
the definition of WλΓ is consistent for all modalities λ ∈ Λ. It follows that W Γ is a REL model. By(Congruencep ), the definition of MbkΓ is consistent for each nominal k ∈ Nom. It follows that MbkΓ is a PL
model, and (W Γ , M Γ ) is a HPL model. We show that (W Γ , M Γ ) |= Γ:(a) for any (k1 = k2 ) ∈ Γ, we have Γ ` k1 = k2 , which implies kb1 = kb2 ; by the definition of (W Γ , M Γ ), we
have WkΓ1 = kb1 = kb2 = WkΓ2 , which implies (W Γ , M Γ ) |= k1 = k2 .
(b) for any λ(k1 , . . . , kn ) ∈ Γ we have Γ ` λ(k1 , . . . , kn ), and by the definition of (W Γ , M Γ ), we getΓΓΓ(kb1 , . . . , kcn ) ∈ Wλ , which implies (W , M ) |= λ(k1 , . . . , kn );(c) for any @k p ∈ Γ we have Γ ` @k p and by the definition of (W Γ , M Γ ), p is true in MbkΓ , which implies(W Γ , M Γ ) |= @k p.
Since Γ |= ρ and (W Γ , M Γ ) |= Γ, we have (W Γ , M Γ ) |= ρ. In order to prove completeness, three cases need
to be considered:(a) if ρ is a nominal equation of the form k1 = k2 then WkΓ1 = WkΓ2 , which means kb1 = kb2 , and we getΓ ` k1 = k2 ;(b) if ρ is a nominal relation of the form λ(k1 , . . . , kn ) then (WkΓ1 , . . . , WkΓ1 ) ∈ WλΓ , which means that weΓΓΓhave (kb1 , . . . , kcn ) ∈ Wλ , and by the definition of (W , M ), we obtain Γ ` λ(k1 , . . . , kn );(c) if ρ is of the form @k p, where k is a nominal and p a propositional symbol, then MbkΓ interprets p as true,and by the definition of (W Γ , M Γ ), we obtain Γ ` @k p.
Proof of Theorem 6.6 We assume that Γ |=∆ ρ and prove that Γ `∆ ρ, where ∆ = (Nom, Λ, Σ). We define
the equivalence ≡Nom = {(k1 , k2 ) | Γ ` k1 = k2 and ki ∈ Nom} on Nom. By (Ref lexivityn ), (Symmetryn )and (T ransitivityn ), the relation ≡Nom is indeed an equivalence. For each k ∈ Nom we define the congruence≡k = {(t1 , t2 ) | Γ ` t1 = t2 and ti ∈ Tk∆ } on the (S, F, P )-model Tk∆ . By (Ref lexivity), (Symmetry),(T ransitivity) and (Congruence), the relation ≡k is indeed a congruence on Tk∆ . We define the ∆-model(W Γ , M Γ ) as follows:b(1) |W Γ | = Nom/≡Nom and WλΓ = {(kb1 , . . . , kcn ) | Γ ` λ(k1 , . . . , kn )} for all n ∈ Nat and λ ∈ Λn , where ki isthe equivalence class of ki , and(2) for each k ∈ Nom, MbkΓ consists of the (S, F )-algebra Tk∆ /≡k and interprets(a) each $ ∈ P r as (MbkΓ )$ = {(τb1 , . . . , τbn ) | Γ ` $(τ1 , . . . , τn )}, and(b) each π ∈ (P − P r ) as (MbkΓ )π = {(tb1 , . . . , tbn ) | Γ ` πk (t1 , . . . , tn )},where τbi and tbi are the equivalence classes of τi and ti , respectively.
By (Congruencen ), W Γ is a (Nom, Λ)-model. By (Congruencep ), (MbkΓ ) is a (S, F, P )-model. By (Share), forall k1 , k2 ∈ Nom we have Γ ` t1 =k1 t2 iff Γ ` t1 =k2 t2 , which implies ≡k1 =≡k2 , meaning that Tk∆1 /≡k1
and Tk∆2 /≡k2 have the same carrier sets. Hence, the definition of (W Γ , M Γ ) is consistent. We show that
(W Γ , M Γ ) |= Γ:28

D. Găină(a) For any nominal equation (k1 = k2 ) ∈ Γ we have Γ ` k1 = k2 , and by the definition of (W Γ , M Γ ), we
have WkΓ1 = kb1 = kb2 = WkΓ2 , which means that (W Γ , M Γ ) |= k1 = k2 .
(b) For any nominal relation λ(k1 , . . . , kn ) ∈ Γ, we have Γ ` λ(k1 , . . . , kn ), and by the definition of (W Γ , M Γ ),
Γ
Γ
Γ
Γ
Γ
Γ
we have (kb1 , . . . , kcn ) ∈ Wλ , which is equivalent to (Wk1 , . . . , Wkn ) ∈ Wλ , and we get (W , M ) |=λ(k1 , . . . , kn ).
(c) For any hybrid equation (t = t0 ) ∈ Γ we have Γ ` t = t0 , and by the definition of (W Γ , M Γ ), we have(W Γ , M Γ )t = b
t = tb0 = (W Γ , M Γ )t0 , which means that (W Γ , M Γ ) |= t = t0 .
(d) For any rigid relation $(τ1 , . . . , τn ) ∈ Γ, where $ ∈ P r , we have Γ ` $(τ1 , . . . , τn ). By the definition of(W Γ , M Γ ), (τb1 , . . . , τbn ) ∈ (MbkΓ )$ for all k ∈ Nom. This means ((W Γ , M Γ )τ1 , . . . , (W Γ , M Γ )τn ) ∈ (MbkΓ )$for all k ∈ Nom. Hence, (W Γ , M Γ ) |= $(τ1 , . . . , τn ).
For any non-rigid relation πk (t1 , . . . , tn ) ∈ Γ, where π ∈ (P − P r ), we have Γ ` πk (t1 , . . . , tn ). By thedefinition of (W Γ , M Γ ), we have (tb1 , . . . , tbn ) ∈ (MbkΓ )π . This means ((W Γ , M Γ )t1 , . . . , (W Γ , M Γ )tn ) ∈(MbkΓ )π . Hence, (W Γ , M Γ ) |= πk (t1 , . . . , tn ).
Since Γ |= ρ and (W Γ , M Γ ) |= Γ, we get (W Γ , M Γ ) |= ρ. In order to prove completeness, four cases are
considered:(a) If ρ is a nominal equation k1 = k2 then WkΓ1 = WkΓ2 , and by the definition of (W Γ , M Γ ), we have kb1 = kb2 ,which is equivalent to Γ ` k1 = k2 .
(b) If ρ is a nominal relation λ(k1 , . . . , kn ) then (WkΓ1 , . . . WkΓn ) ∈ WλΓ , and by the definition of (W Γ , M Γ ),Γ
we have (kb1 , . . . , kcn ) ∈ Wλ , which is equivalent to Γ ` λ(k1 , . . . , kn ).
(c) If ρ is a hybrid equation (t = t0 ) then (W Γ , M Γ )t = (W Γ , M Γ )t0 , and by the definition of (W Γ , M Γ ), we
have bt = (W Γ , M Γ )t = (W Γ , M Γ )t0 = tb0 , which is equivalent to Γ ` t = t0 .
(d) If ρ is a rigid relation of the form $(τ1 , . . . , τn ), where $ ∈ P r , then ((W Γ , M Γ )τ1 , . . . , (W Γ , M Γ )τn ) ∈(MkΓ )$ for all k ∈ Nom. By the definition of (W Γ , M Γ ), we have (τb1 , . . . , τbn ) ∈ (MbkΓ )$ for all k ∈ Nom.
Hence, Γ ` $(τ1 , . . . , τn ).
Similarly, if ρ is a non-rigid relation of the form πk (t1 , . . . , tn ), where π ∈ (P − P r ), then we have((W Γ , M Γ )t1 , . . . , (W Γ , M Γ )tn ) ∈ (MbkΓ )π . By the definition of (W Γ , M Γ ), we have (tb1 , . . . , tbn ) ∈ (MbkΓ )π .
Hence, Γ ` πk (t1 , . . . , tn ).