数理解析研究所講究録
第 1555 巻 2007 年 75-92

75

A Generalization of Characterizations
for the Hybrid Definability
京都大学・文学研究科 佐野勝彦 (SANO Katsuhiko)
Graduate School of Letters, Kyoto University
katsuhiko.sano@gmail.com

1

Introduction

Invariance under (semantical) operations tells us the expressive power ofthe logic
under consideration Rom the semantical viewpoint, e.g., in Birkhoff Variety Theorem for universal algebra and in the seri es ofworks for captunng the expressivity

offirst-order logic, due to Kochen [9], Keisler [8] and Shelah [14] (or, [4, Corollary 6.1.16]), in first-order model theory. This invariance approach have been
applied also to the modal (propositional) languages [7]. Goldblatt-Thomason theorem [3, Theorem 3.19] states that: For any elementary class of frames, ismodally definable in the unimodal propositional language (roughly, expressible
by modal formulas) iff is closed under disjoint unions, generated subffames andbounded morphic images, and , the complement of , is closed under ultrafilter
$F$

$F$

$F$

$\overline{F}$$F$

extensions.
Goldblatt-Thomason theorem teaches us the limitations of modal expressivity of first-order propenies. For example, we camot express irreflexivity of theaccessibility relation by any modal fornulas. This is because ineflexivity is notpreserved under bounded morphic images [3, Example 3.15]. In order to overcome such a lack of expressivity, various extensions with additional modal operators have been proposed, e.g., the difference operator (e.g., [5]) and the global$D$

modality (e.g., [6]), etc.. The author and SATO Kentaro [12] have adopted
the modal-model-ffieorebc approach taken in [2] and proved the general version
of Goldblatt-Thomason theorem for almost all of the extended modal languages
with modal operators (see Table 1).
There are, however, other extended modal languages with a new kind ofpropositional variables, called nominals. Such extensions are called hybrid logics [1].
In his PhD thesis [15], ten Cate introduced the two notion of definability: hybrid
definability (roughly, expressivity by arbitrary formulas of a hybrid language) and
$E$

76

Table 1: Additional Modalities

pure defnability (roughly, expressivity by pure fomulas, i.e,, formulas that do notcontain the ordinary propositional variables but may contain nominals). He gave
Goldblatt-Thomason-style characterizations for these two definability ofthree hy-

brid languages: $H$ (modal logic extended with the nominals alone),
extended with the satisfaction operators ), $Pl(E)(Pi$ extended with the global
modality E). However, he did not consider the general extended languages as we
did for modal languages [12]. Thus, we adopt the approach taken in [12] and by
to generalize ten Cate’s characterization to the general extended hybrid languagewith any additional operators. In this paper, we will report current progress ofthis
project (see Table 2 in the final section).
Let us explain the contents briefly. Section 2 defines the basic notions of hybrid logics including the notion of ffames, models, modal satisfaction relation,and validity, and then introduces the relation between models called bisimulations. In Section 3, we briefly mention basic frame constructions preserving theand introduce some properties (the notion of absolute, trivialvalidity onize) for them. In Section 4, we define another frame construction called ul’afilter morphic images, which is a typical $\Re me$ construction of hybrid logics, andprove the Goldblatt-Thomason-style Characterizations for the hybrid definability$H(\copyright)(\# l$$\copyright_{i}$$\theta ames$of the general extended languages with and without the satisfaction operators .
Finally, Section 5 introduc es a new $\Re me$ consffuction called images of bisimulation system, which preserves the validity of pure formulas, and then gives thecharacterizations for pure definability similarly to Section 4.
$\copyright_{j}$2 PrelimInaries
2.1 Syntax and Semantical Notions
The hybrid language $H(Mod)$ (or, $Pi$ simply) consists of (i) Boolean connectives:(ii) an arbitrary set Mod of modal operators:
Mod, (iii) proposition$\wedge\neg$$\square \in$

77
letters: Prop $=\{p,q,r, \ldots\}$ , (iv) nominal variables: Nom $=\{i,j,k, \ldots\}$ . The
simply) consists of the vocabulary of
hybrid language $H(Mod, @)$ (or, are. The fomulas of, e.g.,
and the satisfaction operators
defined as:$\prime H$$H(\copyright)$$\copyright_{i}(i\in Nom)$$\varphi l(\copyright)$$\varphi::=p|i|\neg\varphi|\varphi\wedge\psi|\square \varphi|\copyright_{j}\varphi$.

, etc.. We, etc. and sets of formulas by
We denote formulas bydefine the Boolean $connectivesarrow,$ , etc. and the modal connective as usual. is called pure if it contains no proposition
abbreviations
letters.
(multimodal) frame
is a pair consisting of a nonempty
set and a amily ofbinary relation on $W(\square \in Mod)$ . (multimodal) model) is a pair consisting ofa ffame
and a valuation :$Prop\cup Nomarrow P(W)satisqing|V(i)|=1$ for any $i\in Nom$ . We denote the uniqueelement ofmeans the domain of a model SM (or, a ffameby .
, respectively). For any binary relation on $W,$ $R[w]$ denotes $\{x\in W|wRx\}$ .
, is defined inductively as:
Then, the satisfaction $relation\vdash$ , e.g., for$\varphi,$$\psi,$$\Gamma,$$\theta$$O$$\vee$$(e:g., O\varphi :=\neg\square \neg\varphi)$$A$$\Delta$$\varphi$$\mathfrak{F}=\langle W\{R_{O}I_{0\epsilon M}\alpha\rangle$

$W$

$A$

$R_{o}$$\mathfrak{M}=\langle \mathfrak{F},$

$V$

$V$

$\mathfrak{F}=\langle W,\{R_{D}I_{0\epsilon Mod}\rangle$$V(\iota)$$i^{V}$$|\mathfrak{M}|(or|\mathfrak{F}|)$$R$$\mathfrak{F}$$H(\copyright)$.

$\mathfrak{M},x|\vdash p\Leftrightarrow x\in V(\sim p)$$\mathfrak{M},x\vdash i\Leftrightarrow x=i^{\gamma}$.

$\mathfrak{M}_{X\vdash\approx}\neg\varphi \mathfrak{M},xr\varphi$.

$\mathfrak{M},x\vdash\varphi\wedge\psi\Leftrightarrow \mathfrak{M},x|\vdash\varphi$$\mathfrak{M},$

$x$

and

$\mathfrak{M},x\vdash\psi$.

ト $\square \varphi\Leftarrow\approx(\forall y\in W)[xR_{\theta}\supset \mathfrak{M}_{\mathcal{Y}^{1}}\vdash\varphi]$$(\approx R_{o}[x]\subset\{y\in W|\mathfrak{M},y\vdash\varphi\})$$\mathfrak{M},x\vdash\copyright_{i}\varphi\approx \mathfrak{M},$ $i^{V}\vdash\varphi$.

and $\Re,v$ are modally equivalent (written $\mathfrak{M},w*’\Re,v$) if
for any formula .
and $\Re,v$ are purely equivalent (written$\Re,v)$ if
and $\Re,v$ are modally equivalent with respect to the pure formulas.
Our main interest is in unimodaland models. We can deal with them$\thetaamework$in theof first-order languages. The first-order (unimodal) frame language is the first-order language that has the identity $symbol\approx togeher$ withthe binary predicate symbol R. We denoteas thefirst-order (unimodal) modelwith the unary predicateslanguage which is the expanded language of$C^{p}\in Prop)$ and the constant symbol $c_{i}(i\in Nom)$ . We wnite
toor
variables
denote a formula with at most one
variable or two distinct, respectively.
Note that a unimodal model
can be seen as the -structureanddefined as follows:Nom). A unimodal Rame can be seen as the 2 -structure defined similarly.
) is a n-tuple, means the usual satisfactionwhere$[\mathfrak{M},w\vdash\varphi\approx$$\mathfrak{M},w$$\Re,v|\vdash\varphi]$$\varphi$$\mathfrak{M},w$$\mathfrak{M},w\langle\sim_{P}$$\mathfrak{M}.w$$\theta ames$$\mathcal{L}^{f}$$\mathcal{L}^{m}$$\mathcal{L}^{f}$$P_{p}$$\alpha(x)$$\theta ee$$\alpha$$v_{1},$$x$$\beta(v_{1},v_{2})$$\theta ee$$v_{2}$$\mathfrak{M}=\langle W,R, V\rangle$$|\mathfrak{M}|=W,$$R^{\mathfrak{M}}=R,$$P_{p}^{\mathfrak{M}}=V(\sim p)(_{\sim}p\in Prop)$$f$$\mathfrak{F}$$\alpha[arrow a]$$a=\langle a_{1},$ $\ldots,a_{n}$$Rom|\mathfrak{M}|$$\mathcal{L}^{m}$$c_{i}^{\mathfrak{M}}=i^{\gamma}(i\in$$\mathfrak{M}F$78
relation (for details, see, e.g., [4, Ch. 1]). Notice
different ffom the modal
satisfaction relation symbol . In this paper, we use some notions Rom firstorder model theory, e.g., submodel, elementary embedding, -saturatedness. The
reader unfamiliar with ffiem ct refer to, e.g., [4].
$H(ffl])$ (or $H(ffi],$ \copyright ))family $\beta=\{\beta_{0}|0\in Mod\}$ of formulas ofFor
is the hybrid ltguage $H$ (or $Tl(@)$ , respectively) where the accessibility relationforis defined by the fomula . Thus, in $H(ffl])$ , we usually denote$o(\in Mod)$ by]. From now on, we will use the following notational convention:(or
simply)E.g., we denote by
by $[xRy\wedge\neg X\approx y]$ (orsimply) (see Table 1), etc.. Ais called $\bm{t}H(ffl])- ffame$ if, for$that\models is$$|\vdash$$\omega$$l^{f},$$\bm{t}y$$\square \in Mod$

$R_{o}$$\beta_{0}$$p_{0}$$\overline{D}$$[\neg X\approx y]$$\bm{t}d\blacksquare$$[\neq]$$[R\cap\neq]$$\theta ame\mathfrak{F}$$\in Mod,\beta_{0}defi.nesR_{o}.Amode1\mathfrak{M}=\langle \mathfrak{F},V\rangle isca11ed\bm{t}H(\emptyset])- modelif\mathfrak{F}is\bm{t}H(\oint^{\bm{t}yo}])-\theta ameObservethat\bm{t}H(ffl])- ffame\langle W,\{R_{o}\}_{0\epsilon Mod}\rangle(or- mode1)$

is detemined by the unimodal Rame$\langle WR\rangle$(or model, respectively). Therefore,

we ofien regardas. Multimodal fiames td
models are only for ffie technical puIposes, not of our original inter.est.
$\langle W,R\rangle$$H(ffl])-\theta ame\langle W, \{R_{O}\}_{0\epsilon Mod}\rangle$) if
Aformula is valid in amodet (written
for $\bm{t}yw$) if
in . is valid in apame (written
forvaluation: Prop $uNomarrow P(|\mathfrak{F}|)$ . is satisfiable in amodel (or afiame ) if(or
, respectively).
is valid in aclass offfames (written
if it is valid in every
F. For aset of fomulas, thesearedefined similarly. is satisfiable in if, somefor somesome. is finitely satisfiable in if, for, ffieconjunction of all elements of ) is satisfiable in F. Aset of fomulas definesaclass offfames if, for all
F. Aclass ofis -definable(or, purely) if there is some set of fomulas (or, pureformulas, respecbvely) of $l$ ffiat defines , where is ahybrid ltguage. For ry
class of ffames, we define Th(F)PTh(F).
Standard Translation S
is defined as:$\mathfrak{M}$$\mathfrak{M}\vdash\varphi$$\varphi$$\mathfrak{M}$$\mathfrak{F}\vdash\varphi$$\mathfrak{F}$$\varphi$$V$$\mathfrak{M},w\vdash\varphi$$\langle \mathfrak{F}, V\rangle\vdash\varphi$$\bm{r}y$$\mathfrak{M}$$\mathfrak{F}$$\varphi$$\mathfrak{M}r\neg\varphi$$\mathfrak{F}r\neg\varphi$$F$$\varphi$$Ft\vdash\varphi)$$no\dot{ti}ons$$\mathfrak{F}\in$$F$$\Gamma$$\bm{t}d$$\langle \mathfrak{F}, V\rangle,w\vdash\Gamma$$F$$\Gamma$$w\in|\mathfrak{F}|$$\bm{t}y\Gamma’\subset f\ln\Gamma\Gamma’(or\wedge\Gamma’$$\Gamma’$

$F$

$V$

$\mathfrak{F}\in F$$\Gamma$$\Re mes\mathfrak{F},$$F$$\mathfrak{F}|\vdash\Gamma\approx \mathfrak{F}\in$$\theta ames$$\mathcal{L}rightarrow definable$$\mathcal{L}$

$F$

$F$

$\mathcal{L}$$=\{\varphi|F|\vdash\varphi\}\bm{t}d$$=\{\varphi:pure|F|\vdash\varphi\}$$T_{x}:Pt(\copyright)arrow \mathcal{L}^{m}$$ST_{x}(\sim p):=P_{p}x$$ST_{x}(\iota):=x\approx c_{i}$$ST_{x}(\neg\varphi):=\neg ST_{x}(\varphi)$$ST_{x}(\varphi\wedge\psi):=ST_{x}(\varphi)\wedge ST_{x}(\psi)$S$T_{x}(\square \varphi)$$ST_{x}(\copyright_{i}\varphi)$For$\varphi l(ffl])$(or$:=\forall y(xRyarrow ST_{y}(\varphi))$$:=\exists\phi\approx c_{i}\ ST_{y}(\varphi)$$H(\emptyset].\copyright)$

can easily prove that

( : a fresh variable)
$y$

( ; a
$\gamma$$\theta esh$variable).

), we define $ST_{x}(o\varphi):=\forall y(\beta_{D}(x,y)arrow ST_{y}(\varphi))$ We$\mathfrak{M},w\vdash\varphi\approx \mathfrak{M}\models ST_{x}(\varphi)[w]$. If we extend $P$ to the.

second-order language, then, we have:Thus, is a pure formula, then defines the elementary property of ffames, i.e.,(. For example,
defines the irreflexivity of .
$\mathfrak{F}\vdash\varphi\approx \mathfrak{F}\triangleright(\forall P)(\forall \mathfrak{h}(\forall x)ST_{x}(\varphi)$$\varphi$$\forall \mathfrak{h}(\forall x)ST_{x}(\varphi)$$\varphi$$iarrow\neg\theta i$$R_{o}$

79

2.2 Bisimulations
Deflnition 1. A bisimulation between Ramesand or$Z\subset
W\crossW’$
is a binary lation
satisfying the following conditions (wnitten): For any,:$=\langle W^{j}, \{S_{O}I_{0\in Mod}\rangle$$\mathfrak{F}=\langle W, \{R_{o}I_{0\epsilon Mod}\rangle$

$re$

$Z$

$\square \in Mod$$\mathfrak{F}rightarrow-oe$(Zig) wZv and$wR_{o}\mathcal{N}\Rightarrow$(Zag) wZv andfor some$vS_{o}\sqrt{}\Rightarrow for$some$v^{j}\in W’$[$w^{j}Z\sqrt{}$and$vS_{O}\sqrt{}$].

$\sqrt{}\in W[\sqrt Z\sqrt \bm{t}dwR_{O}\sqrt{}]$.

An $H$-bisimulation between models
andulation between and satisfying the following conditions:$\Re=\langle \mathfrak{E}, V’\rangle$$\mathfrak{M}=\langle \mathfrak{F}, V\rangle$$Z$

is a bisim-$\mathfrak{E}$$\mathfrak{F}$(Atom) $IfwZv$, then $[w\in V(a)\approx v\in V’(a)]$ for all $a\in Prop\cup$ Nom.

-bisimulation is an $H$-bisimulation(Nom) for any $i\in Nom,$.

An$H(\copyright)$$Z$satisfying in addition:$i^{V}Zi^{V’}$Let be either $H$ or.
and
if there is an L-bisimulation between$\mathcal{L}$

Proposition 2. Let$\backslash$or$\mathfrak{M},w$$\mathcal{H}(\copyright)$]$H(\emptyset$$, \copyright$).

$\mathfrak{M}$,$\Re,$ $v$$\mathfrak{M}$sn be models and$\mathfrak{M},wrightarrow-\mathcal{L}\Re,v$

Pro of By Induction one.g., [3, Theorem 2.20].

$\varphi$

impliesare l-bisimilar (written

and

$\Re$

such that $wZv$ .
$v\in|\Re|$$w\in|\mathfrak{M}|,$$\mathfrak{M},w\sim\rangle$)$\mathfrak{M},wrightarrow\Re,v$$\mathfrak{N},v$.

. Let I be either $H(ffi])$[ $15$ , Theorem 4.1.2]. For the modal connectives, see,

QEDThe convers ofProposition 2 does not hold in general. The following fact [15,Theorem 4.1.2], however, holds.
$e$Fact 3. Let$H(ffl], \copyright)$$\Re,v$, then.

$\mathfrak{M}$, SVI be models and$If\mathfrak{M}$

and

$\Re$

$w\in|\mathfrak{M}|,$are -saturated as$\omega$.

$v\in|\Re|$$\mathcal{L}^{m}$. Let $l$ be either$r\{(\Phi])$-models (-structures) andor$\mathfrak{M},wrightarrow$$\mathfrak{M},wrightarrow-\mathcal{L}\mathfrak{N},v$

3 Basic Frame Constructions
is a generated subframe of\langle rv(wnitten) if $W’\subset W,$ $R_{o}’=R_{O}\cap(W’)^{2}$ , and $R_{0}[w]\subset W’$$(w\in W’)$ for any. Let be a ffame and. Th subffame generatedbyX (wnitten ) is the smallest generated subffame of whose domain contains, where is
X. A point generated subframe of by) is(written:called the root of the frame.
A model Wt
is a generated modelif (& is a generated
subframe ofNom, andfor any
for any $a\in$Prop Nom. Submodel generated byX and point generated submodel are definedsimilarly to the case of.
Definition 4. A ffime$\mathfrak{E}=\langle W’.\{R_{o}’\}_{0\in M\alpha}\rangle$$\{R_{O}\}_{0\in M\alpha}\rangle$$\mathfrak{F}=$$\mathfrak{E}\ovalbox{\tt\small REJECT}\approx\prime \mathfrak{F}$$\square \in Mod$$x\subset|\mathfrak{F}|$$\mathfrak{F}$$\mathfrak{F}_{X}$$\mathfrak{F}$$\mathfrak{F}$$=\langle \mathfrak{E}, V’\rangle$$\mathfrak{F},$$e$$i^{V}\in|\mathfrak{E}|$$\cup$$ffa\iota nes$$x\in|\mathfrak{F}|$$\mathfrak{F}_{X}$$of\mathfrak{M}=t\mathfrak{F},$$i\in$$\mathfrak{F}_{\{x\}}$$V\rangle$$V^{j}(a)=V(a)\cap|\mathfrak{E}|$

$x$

80
Deflnition 5. $\beta=\{\beta_{0}|0\in Mod\}$ is absolute for generated subframes if, for any$r\{(ffi])$ -Rameof ,, any generated subRame, the following holds:
and any$\mathfrak{F}’=\langle W’, \{R_{o}’I_{oeMod}\rangle$$\mathfrak{F}=\langle WR\rangle$$w^{arrow}\theta omW^{j}$$\mathfrak{F}$$\langle W,R\rangle F\beta_{0}[\vec{w}]\Leftrightarrow\langle W’,R’\rangle\vdash\beta_{0}[\vec{w}]$where $R’=R\cap(W’)^{2}$ .

, multimodally generated $sub\theta ames$ might differ fromFor anunimodally generated $subffa\iota nes$ since in the multimodal case the closure under
all associated relations is required.
For example, any combination of the modal operators Table 1 is absolute forgenerated subffames since they are all quantifier Ree. (As for the example thatis not absolute for generated $sub\theta ames$ , see [12]).
$\mathcal{H}(ffi])- ffame$$\beta$Proposition 6. Suppose that is absolute for generated subffames andfor any of $H(ffl])$ (or,for $H(oe])-\theta ames\mathfrak{F}$ and S. Then,$\beta$$\mathfrak{F}\mapsto \mathfrak{E}$$\mathfrak{E}\vdash\varphi\Rightarrow \mathfrak{F}\vdash\varphi$$\mathcal{H}(\Phi], \copyright))$$\varphi$.

Pvoof By Proposition 2. For details, see [15, Theorem 4.2.1].
For any binary relation

$R$

on

$W,$ $R^{*}$

is the reflexive and transitive closure ofDeflnition 7. $H$ trivializes generated subfiames if ($ffme\mathfrak{F}=\langle W\{R_{o}\}_{0\epsilon Mod}\rangle$

QED$\bigcup_{0\in m\alpha^{R_{0})’}}=W^{2}$.

Proposition 8. $H$ bivializes generated
every Rame or and .

$subRames\approx \mathfrak{F}\ovalbox{\tt\small REJECT}\approx \mathfrak{E}$implies$R$.

for every$\mathfrak{F}=\mathfrak{E}$for$\mathfrak{F}$Deflnition 9. A Rame is a hybrid amalgamation of a family 1, there exists $j\in J$ such that (up to isomorphism)
ffames if, for any$\mathfrak{E}$$\mathfrak{F}_{J}|j\in J$$x\in|\mathfrak{E}|$$\mathfrak{F}_{J}\bm{t}d|\mathfrak{E}_{x}|\neq|\mathfrak{F}_{j}|$Deflnition 10.
family.

trivializes hybrid amalgamations if, for any Rame
} of ffames, is not a hybrid amalgamation of 1$\mathcal{H}$$t\mathfrak{F}_{J}|j\in J$} of$\mathfrak{E}_{x^{\ovalbox{\tt\small REJECT}}}\approx\nu$$\mathfrak{E}$or and any$\mathfrak{F}_{j}|j\in J$}.

Proposition 11. (1) $H$ trivializes generated $sub\theta ames\Leftrightarrow(2)H$ bivializes hybrid amalgamations.
We prove the con 廿鴎 position. Assume thatis a hybrid
amalgamation of. Then, there exists $j\in J$ such that}. Take, which implies the negation of (1).
$[(2)\Rightarrow(1)]$ For the contraposition, assume that $H$ does not trivialize generated, for some and (&. SuPpose thatsubffames. Then,and.
holds, which implies. Thus, is a hybrid amalgamation.
QED

Proof.

$[(1)\Rightarrow(2)]$$\mathfrak{E}$$t\mathfrak{F}_{J}|j\in J$$x\in|\mathfrak{E}|$$\mathfrak{E}_{x}>\mathfrak{F}_{J}\bm{t}d|\mathfrak{E}_{x}|\neq|\mathfrak{F}_{J}|$$\mathfrak{F}\succ*\mathfrak{E}$$\mathfrak{F}\neq \mathfrak{E}$$|\mathfrak{F}_{x}|\neq|\mathfrak{E}|$$\mathfrak{F}_{x^{\ovalbox{\tt\small REJECT}}}\approx\nu \mathfrak{F}rightarrow \mathfrak{E}$$of\{\mathfrak{E}\}$Let$K_{al1}$be the class of all$\theta ames$.

$x\in|\mathfrak{F}|$$\mathfrak{F}$$\mathfrak{F}$81$\square m\in Mod$m\in \omega & a 1,
Proposition12. (1) {} is satisfiable indoes not trivialize hybrid amalgamations.
$0_{1}\cdots\square _{m}\neg i|$$K_{al1}$$\ldots,$$\Leftrightarrow(2)H$

Pmof.

$[(1)\Rightarrow(2)]$Suppose that (&,$\langle$. Then,$\square _{k}\in Mod(1\leq k\leq m)$$V\rangle,x$$i^{V}\not\in|\mathfrak{E}_{x}|$

トロ 1

for

$m^{\urcorner}$holds. Thus,and any. We conclude that$\bm{t}ym\in\omega$$|\mathfrak{E}_{x}|\subsetneq|\mathfrak{E}|$.
is a hybrid amalgamation of(%$[(2)\Rightarrow(1)]$ Assum.
}that is a hybrid amalgamation of. We prove thatand
. Take such that
Choose. For(, a $k\in Mod$ ) are simultaneously satisfiable atall, consider a valuation such that $i^{V}=*$ . Then,
Mod $(1 \leq k\leq m)$ ,. Thus, for any $m\in\omega$ and any
and$\{\mathfrak{E}\}$$\mathfrak{E}_{x}$$x\in|\mathfrak{E}|\neq\emptyset$$\square _{1}\cdots 0_{m}\neg i$$S_{x}\succ \mathfrak{F}_{J}$$\mathfrak{F}_{J}$$|\mathfrak{E}_{x}|\neq|\mathfrak{F}_{j}|$$m\in\omega$$x\in|\mathfrak{F}_{J}|$$V$$some*\in|\mathfrak{F}_{J}|\backslash |\mathfrak{E}_{x}|$$S_{x}\ovalbox{\tt\small REJECT}rightarrow \mathfrak{F}_{j}$$\square _{k}\in$$|\mathfrak{E}_{x}|\neq|\mathfrak{F}_{J}|$$t\mathfrak{F}_{J},$$V\rangle$$\subset K_{al1}$$t\mathfrak{F}_{J}|j\in J$$e$$,x$ トロ 1$0_{m}\neg i$.

QEDCorollary 13. The following are equivalent:(1) $H$ does not trivialize generated subRames,(2) $H$ does not trivialize hybrid amalgamations,$0_{m}\in Mod$ } is satisfiable in(3) {ロ 1$\square _{m}\neg i|m\in\omega\ \square _{1},$$K_{al1}$$\ldots,$.

Proposition 14. Assume that is absolute for generated subframes anddoes not trivialize generated subRames. Suppose that $\eta(ffi])$-frame is a hybrid
for any $j\in J$,
amalgamation of a family} of $H(ffl])- ffam$ es. Ifthen.
$ll(\emptyset])$$\beta$$\mathfrak{E}$$t\mathfrak{F}_{j}|j\in J$$\mathfrak{F}_{J}\vdash\varphi$$\mathfrak{E}\vdash\varphi$. Take the point-generated
Proof. Suppose for contraposition thatandsubframeof . By the assumption, there exists $j\in J$ such that
. Fix
. Define a valuation on as follows: $V’(p)=$$\langle \mathfrak{E}, V\rangle,vr\varphi$$\mathfrak{E}_{v}$$|\mathfrak{E}_{v}|\neq|\mathfrak{F}_{j}|$$\mathfrak{E}$$\mathfrak{E}_{v}rightarrow \mathfrak{F}_{j}$$V^{j}$$x\in|\mathfrak{F}_{j}|\backslash |\mathfrak{E}_{v}|$$V(p)\cap|\mathfrak{E}_{v}|(p\in Prop)$and$V^{j}(\iota)=V(\iota)$(if$\mathfrak{F}_{j}$$i^{V}\in|\mathfrak{E}_{v}|\neq\emptyset$) $;x$ (o.w.) $(i\in Nom)$a bisimulation between.

, i.e., $Z=$
Then, is a bisimulation between (& and . Furthermore,andis an H-bisimulation (i.e., $H(\Phi])-$ bisimulation) between
QED, we havewith $vZv$ . Since
by Proposition 2.

Consider the identity relation.

$|\mathfrak{E}_{v}|x|\mathfrak{E}_{v}|\subset|\mathfrak{E}|x|\mathfrak{F}_{J}|$$of|\mathfrak{E}_{v}|as$$Z$$\mathfrak{E}$and$\mathfrak{F}_{J}$$\mathfrak{F}_{j}$$Z$$\langle \mathfrak{E}, V\rangle$$\langle \mathfrak{E}, V\rangle,vr\varphi$$t\mathfrak{F}_{J},$$\mathfrak{F}_{J}r\varphi$}, where
Deflnition 15. The disjoint unionof a family \dag er(consisting), ofpairwise disjoint ffames is the pairof$\mathfrak{F}_{j}|j\in J$$\cup+_{j\in J}\mathfrak{F}_{J}$$\langle W_{j}, \{(R_{j})_{0}I_{0\epsilon M\infty}\rangle$

and$\{\bigcup_{j\in J}(R_{j})_{0}I_{0\in Mod}$.

$\beta$$t\mathfrak{F}_{J}|j\in J$$\square \in Mod$$\{(a, b\rangle|\langle W,R\rangle\succ\beta_{0}[a,b]\}=\bigcup_{j\in J}\{\langle a, b\rangle|\langle W_{j},R_{j}\rangle F\beta_{0}[a,b])$where$\mathfrak{F}_{J}=\langle W_{j},R_{j}\rangle,$$\mathfrak{F}_{J}=$$\bigcup_{j\epsilon J}W_{j}$is absolute for disjoint unions if, for any family$H(\emptyset])- fiames$,and for any
Deflnition 16.

$V’\rangle$$W= \bigcup_{j\epsilon J}W_{j}$and$R= \bigcup_{j\epsilon J}R_{j}$

.

,

I of

82
As a matter of convention, write $R_{\beta--}=(( \bigcup_{0\in Mod}R_{o})\cup=)$ for any $tl(ffl])-$. If
for any $q\{(ffl])- ffame\langle W,R\rangle$, then is absolute for disjoint unions. For example, $\{xRy,xRy\wedge\neg x\approx y\}$ (corresponding to$\{[R], [R\cap\neq]\})$ is absolute for disjoint unions but $\{xRy, \neg x\approx y\}$ (corresponding to$\{[R].[\neq]\})$ is not.

$\theta ame\mathfrak{F}=\langle W,R\rangle$$\beta$$(R_{\beta\overline{-}})^{*}\subset R^{*}$

Proposition 17. Suppose that is absolute for generated subffames and disjoint
unions, thendoes not trivialize generated subffames.
$\beta$$Pi(oe\backslash ])$Proof Assume that is absolute for disjoint unions. Take any$\beta$$\theta ame\mathfrak{F}$. Then,$\mathfrak{F}$is a hybrid amalgamation ofdoes not trivialize}. Thus,
QED
hybrid amalgamations. By Corollary 13, we get the conclusion.
$H(\emptyset])$$t\mathfrak{F}_{w}\cup*\mathfrak{F}_{w}|w\in|\mathfrak{F}|$By Propositions 14 and 17, we have the following:
Corollary 18. Assume that is absolute for generated $subffa\iota nes$ and disjoint
is a hybrid amalgamation of a family
unions. Suppose that an$Pi(\emptyset])- ffimes$. If
for any $j\in J$, thenof.
$\beta$$H(\emptyset])- ffame\mathfrak{E}$$t\mathfrak{F}_{j}|j\in J)$$\mathfrak{E}\vdash\varphi$$\mathfrak{F}_{j}\vdash\varphi$

4 Goldblatt-Thomason-style CharacteriZations for theHybrid Definability
4.1 Ultrafilter Morphic Images
Deflnition 19. A maPping(
to a{the following:$W,$$R_{o}I_{oeMod}\rangle$$f:|\mathfrak{F}|arrow|\mathfrak{E}|$$f(w)S_{o^{\mathcal{V}}}\Rightarrow for$

some

.

$w^{j}\in|\mathfrak{F}|,$

Note that $f$ is a bounded morphism
a bisimulation between and .
$\mathfrak{F}$on$\mathcal{P}(W):l_{R}(X)$[$wR_{o}w^{j}$ and $f(w’)=v$].

$\theta om\mathfrak{F}$to$\mathfrak{E}$iff$Z=\{\langle x,f(x)\rangle|x\in|\mathfrak{F}|\}$

is$\mathfrak{E}$Deflnition 20. Given a binary relation$l_{R}$$\mathfrak{F}=$$\theta me\mathfrak{E}=\langle W^{j}, \{S_{o}I_{0\in Mod}\rangle$(Forth) $wR_{o}W\Rightarrow f(w)S_{o}f(\mathcal{N})$(Back)

is a bounded morPhism ffom a ffime
if, for any $0\in M$ 屋何, $f$ safisfies$R$$:=\{w\in W|R[w]\subset X\}$

on a set , we define a unary operation.

$W$

The $ultr\phi lter$ extension ueis the ffame
whereis the set of (principal and $non- pr\dot{m}$cipal) ultrafilters over $W,$
for any $x\subset W,$
implies $X\in u’$ .
$\mathfrak{F}of\mathfrak{F}=\langle W\{R_{o}1_{0\in Mod}\rangle$$W^{ue}$$\langle W^{e}, \{R_{o}^{uc}I_{oeM\infty}\rangle$$uR_{o}^{uc}u’$if,$l_{R_{O}}(X)\in u$

Note that the ultrafilter extension of$H(ffi])- ffame$.

$H(\emptyset])- ffame\mathfrak{F}$is not necessarily an,83Definition 21. Let and be Rames. bi is an ultrafilter morphic image of ifor such that $|r^{1}[\{u\}]|=1$ forthere is a surjective bounded morphism $f$ :all principal ultrafilters.
$\mathfrak{E}$$\mathfrak{F}$$\mathfrak{F}$$\mathfrak{F}arrow ue$$u\in|ue\mathfrak{E}|$We can apply this notion to the $H(\Phi])-\theta ames$ . If and are
and or is an ultrafilter morphic image of , then, the notion of ultrafilter morphic
images links two-Rames and or via (multimodal) frame or.
$H(\mathfrak{F}])- ffames$$\mathfrak{E}$$\mathfrak{F}$$\mathfrak{F}$$H(\mathfrak{F}])$$\mathfrak{u}e$$\mathfrak{F}$Proposition 22. Let and be $H(ffi])-\theta ames$ . Suppose that is an ulffafilter
impliesmorphic image of . Then, for any of $H(ffl])$ (or, $H(ffl],$ \copyright )),bi.
$\mathfrak{F}$$\mathfrak{E}$$\mathfrak{E}$$\mathfrak{F}|\vdash\varphi$$\mathfrak{F}$$\varphi$$|\vdash\varphi$

Proof. Similar to [15, Proposition4.2.6].

QED

Proposition 23. Assume that is absolute for disjoint unions. Let$(i\in\{1,2\})$ be $H(\emptyset])- ffames$ . If
is an ultrafilter morphic image of$i\in\{1,2\}$ , then.
is an ultrafilter morphic image of$\beta$$\mathfrak{F}_{j}$$\mathfrak{F}_{i}$$\mathfrak{E}_{j}$andfor any$\mathfrak{E}_{i}$$\mathfrak{E}_{1}\cup*\mathfrak{E}_{2}$$\mathfrak{F}_{1}\cup*\mathfrak{F}_{2}$QED

Proof. Similar to [15, Lemma 4.2.13].

andProposition 24. Assume that is absolute for disjoint unions. Let$(i\in\{1,2\})$ be $H(ffl])- ffames$ . If
are elementarily equivalent for any
and$i\in\{1,2\}$ , thenare elementarily equivalent.
Si2 and$\beta$$\mathfrak{F}_{i}$$\mathfrak{F}_{1}\cup\star$$\mathfrak{E}_{i}$$\mathfrak{F}_{t}$$\mathfrak{E}_{i}$$\mathfrak{E}_{1}U\star \mathfrak{E}_{2}$Proof. Similar to $[15, Lemna4.2.14]$ .

QED

4.2 Characterizations for the Hybrid Definability
Theorem 25. Suppose that is absolute for generated subffames and disjoint
unions. Then, for any elementary family $FofH(\emptyset])-\theta ames,$ is $H(ffi])$ -definable
is closed under (i) ultrafilter morphic images, (ii) generated $sub\theta ames$, and(iii) hybrid amalgamations.
$\beta$$F$$\Leftrightarrow F$

and disjoint unions.
Propositions 6, 22 and Corollary 18. We
The lefl-to-right-direction is clear
will prove that the right-to-lefl-direction. It suffices to prove that, for any.
. Suppose thatframe , $Y 1- Th
We divide the proof into two cases: (Case 1) and (Case 2).
(Case 1) Let us assume that is point generated by . We can suppose that
, where
is
Prop
. Let
and Nom

Proof Suppose that is absolute for generated$\beta$$sub\theta ames$$\theta om$$H(\emptyset])-$$(F)\Rightarrow \mathfrak{F}\in F$$\mathfrak{F}$$\mathfrak{F}\vdash Th(F)$$w$$\mathfrak{F}$$=\{i_{x}|x\in|\mathfrak{F}|\}^{1}$$=\{p_{X}|X\subset|\mathfrak{F}|\}$

1

{ of
}
are alike except that the set ofpropositional and nominal variables$\mathfrak{F}\vdash$$Pi’(\emptyset)$$\mathfrak{M}=t\mathfrak{F},$Th(F)$[i_{x}|x\in|\mathfrak{F}|\}$.

$\approx \mathfrak{F}det\vdash$$H(\emptyset])|F\vdash\varphi$$\varphi$$\approx \mathfrak{F}\vdash[\varphi of\mathcal{H}’(\emptyset])|F\vdash\varphi$$V_{0}$$V_{0}\rangle$}, where$of\mathcal{H}’$is$H(\emptyset])$and$\{p_{X}|X\subset|\mathfrak{F}|\}\cup$84
the natural valuation with $V_{0}(p_{X})=X$ and $V_{0}(i_{x})=\{x\}$ . Let be the set consisting,of the following, for all $X,$
and$\Delta$$Y\subset W$$x\in|\mathfrak{F}|$(a $\in Mod$ ).

$p_{W\backslash X}rightarrow\neg p_{X};p_{X\cap Y}rightarrow p_{X}\wedge p_{Y};i_{x}rightarrow p_{\{x\}};p_{T_{R_{0}}(X)}rightarrow op_{X}$Let

be the following set:$\Delta_{\mathfrak{F}}$$\{i_{w}\}\cup${$\square _{1}\cdots 0_{m}\varphi|\varphi\in\Delta$

and$m\in\omega$and$0_{1},$$\ldots,$$0_{m}\in Mod$}.

It is easy to see thatis satisfiable on at under the natural valuation .
(for the proof, see, e.g., [15, p.59, Claim 1]):
Then, we can prove the.
is satisfiable in or for someBy this, we may infer that
Ag for some valuation and somein for some
F. It follows that all nominals in the set
denote points inthat are reachable Rom . Thus, we can think of as avaluation for the fiame . In this way, we can consider the point-generated sub, which implies
model \langle (&v’ofby (ii). Then, we can prove thatandfor all$w$$\mathfrak{F}$$\Delta_{\mathfrak{F}}$$\nabla_{0}$$f_{0^{\backslash }}11owing$$\mathfrak{E}\in F$$\Delta_{\mathfrak{F}}$

$2$

$V$

$\langle \mathfrak{E}, V\rangle,v\vdash$$\mathfrak{E}\in$$\mathfrak{E}$$v$$\{i_{x}|x\in|\mathfrak{F}|\}$$v^{3}$$\langle \mathfrak{E}, V\rangle$$V$$\mathfrak{E}_{v}$$V\rangle$$X\subset|\mathfrak{F}|wiffiw\in X(.\cdot\langle \mathfrak{E}_{v}, V\rangle,v|\vdash i_{w}$$\langle \mathfrak{E}_{v}, V\rangle,v|\vdash p_{X}$$\langle \mathfrak{E}_{v}, V\rangle\vdash\Delta$

and$S_{\nu}\in F$$\langle \mathfrak{E}, V\rangle$$i_{w}rightarrow p_{\{w\}},$ $p_{\iota w\}}rightarrow p_{X}\wedge p_{\{\iota\nu\}}\in\Delta$).

Let (%:,
be an -saturated elementary extension of, which implies. It follows thatandfor all
$w\in
X$
with
is the lement corresponding to , since the satisfaction
where$V^{*}\rangle$$\langle$$\langle \mathfrak{E}_{v}, V\rangle$$\omega$$\langle \mathfrak{E}_{v}^{*}, V^{*}\rangle|\vdash\Delta$$\mathfrak{E}_{v}^{*}\in F$$v^{*}$$e$$v$

relation is elementary.
CLAIM 1. is an ultrafilter morphic image of$\mathfrak{F}$CLAm) For any$X\subset|\mathfrak{F}_{w}|$$\langle \mathfrak{E}_{v}^{*}, V^{\cdot}\rangle,v|\vdash p_{X}$$\mathfrak{E}_{v}$.

is an ultrafilter.
This defines the mapping
to lue . We can prove that $f$ is a surjective
bounded morphism and satisfies the condition ofultrafilter morphic image (For thedetailed proof of these, see [15, Claim 2 in the proof of Theorem 4.3.4]).
(PROOF

$OP$

$s$

in

$\mathfrak{E}_{v},$$\{X\subset|\mathfrak{F}||\langle \mathfrak{E}_{v}, V^{\cdot}\rangle,s\vdash p_{X}\}$$fRom|\mathfrak{E}_{v}^{l}|$$\mathfrak{F}|$$r$

Thus, we can conclude thatRomby (i).
(Case 2) Assume that is not point generated. Here, we ne $ed$ the assumption$\mathfrak{F}\in F$$\mathfrak{E}_{v}\in F$$\mathfrak{F}$of absoluteness of disjoint unions and the clo sure condition (iii). Take any pointgeneratedof . In what follows, we will show that
. It
then follows by (iii) that.
As in (Cas $e1$ ), we also suppose that Prop
and Nom, where is a distinct nominal fiom.
2 . We prove that
Ag is finitely satisfiable in F. Let. SinceTh(F) andisin
By
satisfiable
F.
the
of
elementarinessisAsatisfiable in F. Note$sub\theta ame\mathfrak{F}_{w}$$\mathfrak{F}_{w}\cup*\mathfrak{F}_{w}\in F$$\mathfrak{F}$$\mathfrak{F}\in F$$=\{p_{X}|X\subset|\mathfrak{F}|\}$$\{i_{\emptyset}\}$$\{i_{x}|x\in|\mathfrak{F}|\}$$i_{\emptyset}$

$($

$)$

$\langle \mathfrak{F}, r_{0}\rangle,w\succ$$\Delta’\subset\hslash n\Delta_{\mathfrak{F}}$$\Delta’,$$=\{i_{x}|x\in|\mathfrak{F}|\}U$$\Delta’$$F,$that is closed under ultraproducts by elementaniness.
3 This is because
for any{$xRy$tion of. Note thatis equivalent to$\mathfrak{F}\vdash$$\Delta_{\mathfrak{F}}$$F$$0_{1}\cdots o_{m}(i_{l}arrow\theta i_{y})|$$i_{x}arrow Oi_{y}$$p_{Ix\}\cup(W\backslash l,_{0}(W\backslash |y|))}rightarrow p_{W\}l_{R_{0}}(W\backslash |y|)}\in\Delta$.

$m\in\omega$

and $0_{j}\in Mod$ } expresses the informa, which is equivalent to$i_{X}V\theta i_{y}rightarrow\theta i_{y}$

85
Let

is a natural valuation with $V_{0}(p_{X})=X,$. We define in th same way as in (Case 1). Let, where$\mathfrak{M}=\langle \mathfrak{F}_{w}, V_{0}\rangle$

andthe following set:$i_{0}^{V_{0}}=*\in|\mathfrak{F}|\backslash |\mathfrak{F}_{w}|$$\{i_{w}\}\cup$$\cup${{$V_{0}$$\Delta$$\square _{1}\cdots\square _{m}\varphi|\varphi\in\Delta$

$e$

and
and

$m\in\omega$$\square _{1}\cdots\square _{m}\neg i_{\emptyset}|m\in\omega$$\square _{1},$and$\ldots,$$0_{1},$$\ldots,$$\square _{m}\in Mod$$\square _{m}\in Mod$$i_{x}^{r_{0}}=x$$\Delta_{\mathfrak{F}_{\backslash \nu}}$

be

}

}.

Easily, , is satisfiable onat under a natural valuation. Then, in thesame way as (Casse 1), we can prove thatfor some valuation(%and some in for some.
Letbe the subfiame of generated by . By the consWuction ofis a proper generated $sub\theta ame$ of or. Thus, by (ii) and (iii),
F. It) (except )follows
that all nominals in the set {denote points inthat are reachable. Thus, we can think of as avaluation for the ffame
by removing
our vocabulary. In this way, we
obtain the point-generated submodelof. Then we prove that
$w\in
X$.
\langle (&v’andfor allwith
In the same way as in (Case 1), we can take an -saturated elementary extensionof (&\mbox{\boldmath $\nu$}’and prove thatis an ultrafilter morphic image of$w$$\mathfrak{F}_{w}$$\Delta_{\mathfrak{F}_{\nu}}$$V$$\langle \mathfrak{E}, V\rangle,v|\vdash\Delta_{\mathfrak{F}_{w}}$$\mathfrak{E}\in F$$v$$\mathfrak{E}$$\mathfrak{E}_{\nu}$$v$$\Delta_{\mathfrak{F}_{w}},$$or_{\nu}$$\mathfrak{E}_{v}\cup*\mathfrak{E}_{\nu}\in$$\theta om\langle \mathfrak{E}, V\rangle,$ $v\vdash\Delta_{\mathfrak{F}_{w}}$$i_{x}|x\in|\mathfrak{F}|$$\theta omv$$\langle \mathfrak{E}, V\rangle$$\langle \mathfrak{E}.V\rangle$$\langle \mathfrak{E}_{v}, V\rangle$$\vdash\Delta$$V$$i_{0}\theta om$$\mathfrak{E}_{\nu}$$V\rangle$$i_{\emptyset}$$\langle \mathfrak{E}_{v}, V\rangle,v\vdash p_{X}$$\dot{C}\bm{t}$$X\subset|\mathfrak{F}|$$\omega$$\langle \mathfrak{E}_{\nu}^{*}, r\rangle$$\mathfrak{E}_{v}^{*}$$V\rangle$$\langle$$\mathfrak{F}_{w}$.

Thus, we can conclude thatis an ultrafilter morphic image of
by Proposition 23. By Proposition 24,
is elementarily equivalent to, which implies
QED. It follows thatby (i).
$\mathfrak{F}_{w}\cup*\mathfrak{F}_{w}$$\mathfrak{E}_{\nu}^{*}w\mathfrak{E}_{\nu}^{*}$$\mathfrak{E}_{\nu}U*$$\mathfrak{E}_{v}^{*}U*\mathfrak{E}_{\nu}^{*}$$\mathfrak{E}_{v}$$\mathfrak{F}_{w}\cup*\mathfrak{F}_{w}\in F$$\mathfrak{E}_{\nu}\cup*\mathfrak{E}_{v}\in F$

is absolute for generated subffames. Then, for any
elementary family
is-definable $\approx F$ is closed
under ultrafilter morphic images.
Theorem 26. Suppose that$F$$\beta$of $H(ffl])$-Rames,$F$$ti(\emptyset])$

Proof. We can prove this theorem similarly to the proof of Theorem 25. It suffice
to consider (Cas $e1$ ), i.e., the case where
right-to-lefi-direction.

For]$H(\emptyset$$, \copyright$$\mathfrak{F}$is point generated, in the proof of the
QED), we can prove the following characterization.

Theorem 27. Suppose that is absolute for generated $sub\theta ame$ and $H(\beta])$ does
not trivializes generated $sub\theta ames$ . Then, for any elementary family of $n(\Phi])-$Rames, is $H(ffi$] )-definable $=F$ is closed under (i) ultrafilter morphic
images and (ii) generated subBames.
$\beta$$F$$F$$, \copyright$

Proof Suppose that is absolute for generated subffimes.
$\beta$We will prove that the right-to-leR-direction. It suffices to prove that, for any. Suppose that
. We can supposethat Prop
and Nom, where. Let
is$H(oe])-\theta ame\mathfrak{F},$ $\mathfrak{F}\vdash Th(F)=\mathfrak{F}\in F$$=\{p_{X}|X\subset|\mathfrak{F}|\}$$=\{i_{x}|x\in|\mathfrak{F}|\}$$\mathfrak{F}|\vdash Th(F)$$\mathfrak{M}=\langle \mathfrak{F}, V_{0}\rangle$$V_{0}$

86
the natural valuation with $V_{0}(p_{X})=X$ andas in (Case 1) at the proof ofTheorem 25. Let{$\copyright_{i_{\nu}}\square _{1}\cdots\square _{m}\varphi|v\in|\mathfrak{F}|\bm{t}d\varphi\in\Delta$

and$\Delta_{\mathfrak{F}}$. We definein the same way
be the following set:$i_{x}^{V_{0}}=x$$m\in\omega$and$\square _{1},$$\Delta$$\ldots,$$\square _{m}\in Mod$).

is satisfiable on at under the natural valuation. Then
It is easy to see thatfor some valuation for some
we can prove that
. Since isclosed under generated subfiames, we may assume that or is generated by the set
ofpoints that ar\‘e named by nominals, i.e.,. Then, we can prove that$\mathfrak{F}$$\Delta_{\mathfrak{F}}$

$w$

$V$

$\langle \mathfrak{E}, V\rangle|\vdash\Delta_{\mathfrak{F}}$$\mathfrak{E}\in F$$F$$\{i_{x}^{V}|x\in|\mathfrak{F}|\}$$(\mathfrak{E},$$V\rangle$$|\vdash\Delta$.

be an w-saturated elementary extension of ((&, , which imLet \langle bi’,plies
F. It follows that
. We can prove the following claim in
the same way as in [15, Claim 2 in the proof of Theorem 4.3.4]: is an ultrafilter
morphic image of or‘. Thus, we can conclude that.
QED
$V^{\cdot}\rangle$$V\rangle$$\mathfrak{E}^{*}\in$$\langle \mathfrak{E}^{*}, V^{*}\rangle\vdash\Delta$$\mathfrak{F}$$\mathfrak{F}\in F$

In the case where is absolute for generated subffames anduivializes
generated subRames, we can prove, in the same way as Theorem 27, that for any)-definable $\approx F$ is closed]
elementary family of $H(\Phi])- ffames,$ is] ) andunder ultrafilter morphic images. Thus, in this case,have
the same expressive power with respect to any elementary family of ffames.
As corollaries of theorems in this section, we can obtain several semanticalcharacterizations of the extended hybrid languages whose chwacterizations werepreviously unknown. For example, by Theorem 25 (or 26, 27), we can get thecharacterization for the hybrid language whose operators are $\{[R], [R^{-1}\cap\neq]\}$ (or,$\{[R\cap\neq], [\neq]\},$ $\{[R\cap\neq], [R^{-1}\cap\neq], [\neq]\}$ , respectively).
$H(\emptyset])$$\beta$$F$$F$$H(\emptyset$$, \copyright$$H(\emptyset$$\mathcal{H}(ffl])$$, \copyright$

Remark 28. In this remark, let us restrict our interest to the set of qumtifier(QF-) fomulas of. Then, $n(ffl])$ is absolute for generated $sub\theta ames$ . We
can give the general chxacterization for extended modal languages (the modal
version of $Pi(ffi]))$ without assuming the absoluteness for disjoint unions [12]. In
our characterization (Theorems 25 and 26) of this paper, however, we need toclass the hybrid languages $H(ffi])$ under two cases: the case where we assume theabsoluteness for disjoint unions and the case where $H(ffl])$ trivializes generated
subffames (see Table 2 in the final section). Thus, the range where we apply ourcharacterizations (Theorems 25 and 26), is smaller than that of [12].
The satisfaction operators
can change the situation. For, we cangive the general characterization (Theorem 27) without assuming the absolutenessfor disjoint unions. Therefore, the range ofTheorem 27 is the same as that of [12].
It should be noted that SATO Kentaro [13] gives another Goldblatt-Thomasonstyle characterizations ofhybrid (not pure) definability for \copyright -\mbox{\boldmath $\theta$}e, without assuming the absoluteness for disjoint unions. In order to give characterizations, he introduces the notion ofKripke frame with designation and defines se$\beta$$\theta ee$$\mathcal{L}^{f}$$H(\emptyset])$$\copyright_{j}$$($$)^{\varphi}l(\Phi])$

87
mantical operations for it. Thus, together with his results, we have the comparable
characterizations for hybrid definability of $H(oe])$ and $H(ffi$] ) to [12].
$, \copyright$

5 GoldblaU-Thomason-style Characterizations for thePure Definabihty
5.1 Images of Bisimulation System
Definition 29. Given a bisimulation between ffames and or, and a subset $X$
respects $X$ ifthe following two conditions hold for all $x\in X$:$Z$$of|\mathfrak{E}|,$1.

$\mathfrak{F}$$Z$

such that $wZx$.

$(\exists!w)$

2. For all

and$w\in|\mathfrak{F}|$$v\in|\mathfrak{E}|$, if wZx and $wZv$, then $x=v$ .

In other words, respects
if
is a fimction on $Z^{-1}[X]$ .
$Z$$X\subset|\mathfrak{E}|$$Z^{-1}\subset|\mathfrak{E}|x|\mathfrak{F}|$is a tmction on

$X$

and

$Z\subset|\mathfrak{F}|\cross|\mathfrak{E}|$

Deflnition 30. Given a bisimulation$(\exists t\in|\mathfrak{E}|)$$=|\mathfrak{F}|$sZt andand ran$Z$$(\forall s\in|\mathfrak{E}|)(\exists t\in|\mathfrak{F}|)tZs$$Z=|\mathfrak{E}|$.

Deflnition 31. A bisimulation system$Z$:

is total if
and. In other words, is total if domZ

between$\theta om$$\{X|\dot{X}\subset n_{n}|\mathfrak{E}|\}arrow${$Z$$\mathfrak{E},$$\mathfrak{F}$$Z$$(\forall s\in|\mathfrak{F}|)$$Z$

a ffame to a Rame (% is a fimction$\mathfrak{F}$:$\mathfrak{F}-rightarrow \mathfrak{E}|Z$

is total}satisfying that $Z(X)$ respects $X$. If there exists a bisimulation system $Z$ Rom affame to a ffame , then, is an image of bisimulation system Rom .
$\mathfrak{E}$$\mathfrak{F}$$\mathfrak{E}$$\mathfrak{F}$We can also apply this notion to the-frames. Compared with the notionof ultrafilter morphic images, notice that there is no need to consider multimodal
ffames in order to link two-Bames.
$H(\mathfrak{F}])$$H(\mathfrak{F}])$

Recall that is pure if contains no proposition letters.
$\varphi$$\varphi$

Proposition 32. Let and or be. Suppose that (& is an imageof bisimulation system. Then, for any pure formula of $H(oe])$ (or,$\mathcal{H}(ffl])-\theta ames$$\mathfrak{F}$$\theta om\mathfrak{F}$$H(\emptyset], \copyright))$,$\mathfrak{F}\vdash\varphi$

implies or$|\vdash\varphi$$\varphi$.

Pmof. See $[15, Theorem4.2.10]$ .

QEDA

Proposition 33. Assume that is absolute for disjoint unions. Let
and$H(\Phi])-\thetaa\bm{P}es$$(i\in\{1,2\})$ be. If is an image of bisimulation system
for any $i\in\{1,2\}$ , thenis an image ofbisimulation system$\mathfrak{F}_{l}$$\mathfrak{F}_{i}$$\mathfrak{F}_{1}u*\mathfrak{F}_{2}$Proof. See [15, Lemma4.2.15].

$\mathfrak{E}_{i}$$\theta om\mathfrak{E}_{i}$$\theta om\mathfrak{E}_{1}\mathfrak{G}\mathfrak{E}_{2}$

.

QED

88

5.2 Characterizations for the Pure Definability
Recall that pure formulas define elementary properti es of frames by standardtranslation.

Theorem 34. Suppose that is absolute for generated subfram es and disjoint
unions. Then, for any family of $H(ffl])- ffames,$ is purely $H(oe])$ -definable
is elementary and is closed under (i) images ofbisimulation system, (ii)generated $sub\theta ames$ , and (iii) hybrid amalgamations.
$\beta$

$F$

$F$

$F$

$\Leftrightarrow F$

Proof. Suppose that is absolute for generated subframes and disjoint unions.
$\beta$We prove the-direction. It suffices to show that, for all ffames ,.
. Suppose that(Case1) and (Case 2).
We divide the proof into two cases:(Case 1) Assume that is point generated by . We can suppose that Nom). Let, where is the natural valuation with.
{Let
is satisfiable on under .
}. Clearly,{ : pure
Then, we can prove that Ag is satisfiabl in , similarly to Theorem 25. Let
F. Letfor some
be the subffame of or generated by ,\langle bi,,
by (ii). It follows
which implies
that all nominals inthe set. Thus, wedenote points inthat are reachableor,.
can think of as a valuation for the ffame
In this way, we can consider the.
point-generated submodelofWe can prove the following [15, Claim 2 in the proof of Theorem 4.4.4].
$\dot{n}ght- to- lefl$$\mathfrak{F}$$\mathfrak{F}|\vdash PTh(F)$$\mathfrak{F}|\vdash PTh(F)\Rightarrow \mathfrak{F}\in F$$i_{x}|x\in|\mathfrak{F}|$$V$$\mathfrak{M}=\langle \mathfrak{F}V\rangle$$\Delta_{\mathfrak{F}}=$$|\langle \mathfrak{F},$$\varphi$$i_{x}^{V}=x$$V\rangle,w\vdash\varphi$$\mathfrak{E}\in$$V$$\mathfrak{F}$$\Delta_{\mathfrak{F}}$

$F$

$e$

$\langle \mathfrak{E}, U\rangle,v|\vdash\Delta_{\mathfrak{F}}$

$=$

$w$

$\mathfrak{F}$$v$$\mathfrak{E}_{v}$$\theta om$$S_{v}\in F$$\{i_{x}|x\in|\mathfrak{F}|\}$$U\rangle$$v\vdash\Delta_{\mathfrak{F}}$$\theta omv$$\langle \mathfrak{E}, U\rangle$$U$$\langle \mathfrak{E}, U\rangle$$\langle \mathfrak{E}_{v}, U\rangle$

CLAIM 2. For all pure$H(\emptyset])$-formulas$\varphi,$$\langle \mathfrak{F}, V\rangle|\vdash\varphi\approx\langle \mathfrak{E}_{v}, U\rangle|\vdash\varphi$

.

Let
and
be -saturated elementary extensions. By elementaniness,.
In what follows, we will construct a bisimulation system Romto .
, and introduce new nominals
Fix. We will(or simply) for the expansion of
write
in which $j_{k}^{V}=w_{k}(1\leq k\leq n)$ . We can prove the following analogous to [15,Claim 3 in the proof of Theorem 4.4.1].
$\langle \mathfrak{F}^{*}, V^{\cdot}\rangle$$\langle \mathfrak{E}_{v}^{r}, U^{*}\rangle$$\omega$$\mathfrak{E}_{v}^{*}\in F$$\mathfrak{F}\cdot$$\mathfrak{E}_{v}$$J^{\gamma}=(- j_{1}, \ldots,j_{n})$$w_{1},$ $\ldots,w_{n}\in|\mathfrak{F}^{*}|$$t\mathfrak{F}^{*},$$V^{*},w_{1},$ $\ldots,w_{n}\rangle$

CLAIM 3. There exists$t\mathfrak{F}^{*},$$V^{*},w^{arrow}\rangle$$t\mathfrak{F}\cdot,$$\theta\in|\mathfrak{E}_{\nu}|$$V^{*},\tilde{w}\rangle$$t\mathfrak{F}^{*},$$r\rangle$

such that, for any pure $Pi(ffl])[\prime 1$ -fomula ,$\varphi$$|\vdash\varphi\approx\langle \mathfrak{E}_{v}^{*}, U^{\cdot},\theta\rangle|\vdash\varphi$.

Define the binary relation,such thatin $Pi(ffl])[;1$ . Then, we can prove that is a total bisimulation(see, e.g., [15, Claim 4 in the proo ofbetweenand respecting
Theorem 4.4.1]). We have constructed a bisimulation system
to . By(i),and then, by elementariness,.
$sZt\approx d\epsilon ft\mathfrak{F}\cdot,$$Zbetween|\mathfrak{E}_{\nu}^{*}|\bm{t}d|\mathfrak{F}\cdot|$$\langle*\nu_{p}\langle \mathfrak{E}", U^{*},\theta\rangle,$$\mathfrak{E}_{\nu}$

$Z$

$t$

$\mathfrak{F}^{*}$$\{w_{1}, \ldots,w_{n}\}$$f$$\theta om\mathfrak{E}_{\nu}$$\mathfrak{F}\cdot\in F$$r,warrow\rangle$$\mathfrak{F}\in F$$\mathfrak{F}^{*}$

$s$

89
Assume that is not point-generated. Take any point-generated subof In what follows, we will show that
. It then follows(Case 2)$\mathfrak{F}$$\theta ame\mathfrak{F}_{w}$$\mathfrak{F}_{w}u*\mathfrak{F}_{w}\in F$$\mathfrak{F}$by (iii) that$\mathfrak{F}\in F$.

We can suppose that Nom

ffom

where is a distinct nominal, where is a natural valuation with
and
. Let
. Let
is satisfiable{ : pure}. Clearly,. Then, we can prove thatis satisfiable in , similarly to$\{i_{x}|x\in|\mathfrak{F}|\}$$\Delta_{\mathfrak{F}_{W}}=$$|\langle \mathfrak{F},$$\varphi$$i_{\emptyset}$$V$$\mathfrak{M}=\langle \mathfrak{F}, V\rangle$$i_{\emptyset}^{V}=*\in|\mathfrak{F}|\backslash |\mathfrak{F}_{w}|$on$=\{i_{x}|x\in|\mathfrak{F}|\}\cup\{i_{\emptyset}\}$$i_{x}^{V}=x$$V\rangle,w\vdash\varphi$$\Delta_{\mathfrak{F}_{\mathcal{V}}}$

under
Theorem 25.
. Let be th subRame of (& generatedLet
for someby . By the construction,
is a proper generated subffame of . Hence, by (ii)and (iii),.
It follows Romthat all nominals in the set(except ) denote points in (&,. Hence we can ffiin
that are reachable(
as a valuation for the Rameby removing ffom our vocabulary. In thisway, we can consider the point-generated submodelof. We canprove the following as in (Case 1): For all pure-fornulas$V$$\mathfrak{F}_{w}$$\langle \mathfrak{E}, U\rangle,$$F$$\Delta_{\mathfrak{F}_{w}}$$\mathfrak{E}\in F$$v|\vdash\Delta_{\mathfrak{F}_{w}}$

$v$

$e$

$or_{\nu}$$\mathfrak{E}$$\mathfrak{E}_{v}$$\mathfrak{E}_{v}\cup*\mathfrak{E}_{v}\in F$$\{i_{x}|x\in|\mathfrak{F}_{w}|\}$$\langle \mathfrak{E}, U\rangle,v\vdash\Delta_{\mathfrak{F}_{w}}$$i_{\emptyset}$$\theta omv$

$U\rangle$$\langle$$U$$S_{v}$$k$$i_{\emptyset}$$\langle \mathfrak{E}_{\nu}, U\rangle$$\langle \mathfrak{E}, U\rangle$$H(\emptyset])$$\Leftrightarrow\langle \mathfrak{E}, U\rangle|\vdash\varphi$$\varphi,$.

$\langle \mathfrak{F}_{w}, \nabla\rangle|\vdash\varphi$

andbe -saturated elementary extensions. By elemenF. In the ame way as (Case 1), we can construct a bisimulationto. Thus, we can conclude thatis a image of bisimsystem fromulation system Rom
isby Proposition 33. By Proposition 24,, which implies
elementarily equivalent to (&vF. It follows that
QED
by (i).

Let
tariness,$\langle \mathfrak{F}_{w}, V’\rangle$$\langle \mathfrak{E}_{\nu}, U^{\cdot}\rangle$$\omega$$s$$\mathfrak{E}_{\nu}^{*}\in$$\mathfrak{E}_{\nu}^{*}$$\mathfrak{F}_{w}u*\mathfrak{F}_{w}$$\mathfrak{F}_{w}^{*}$$\mathfrak{E}_{v}^{*}\cup*\mathfrak{E}_{\nu}^{*}$$\mathfrak{E}_{\nu}^{l}\mathfrak{G}\mathfrak{E}_{v}^{*}$$u*\mathfrak{E}_{\nu}$$\mathfrak{E}_{v}^{*}\mathfrak{G}\mathfrak{E}_{v}^{*}\in$$\mathfrak{F}_{w}\cup*\mathfrak{F}_{w}\in F$

Theorem 35. Suppose that is absolute for generated subffames andializes generated subframes. Then, for any family of $\mathcal{H}(ffi])- fiames,$$F$$\mathcal{H}(ffl])$-definable$\Leftrightarrow F$tion system.

trivis purely$H(\emptyset])$$\beta$is lementary and
$e$

$F$

$F$

is closed under images of bisimula-

Proof We can prove this theorem similarly to the proof ofTheorem 34. It suffice
to consider (Case 1), i.e., the case where
rigt-to-lefl-direction.

$\mathfrak{F}$is point generated, in the proof of the
QED.
$Then,for\bm{t}yfami1yFfH(\beta$)]$Theorem_{O}36.Suposeffiat\beta isabsoluteforgeneratedsub\theta ames$$,\copyright$$- definable\approx$

is closed under (i) images of bisimulation system and (ii) generated subffames.

and

$F$

Proof Suppose that is absolute for generated subRames. It suffices to show$\beta$that for all frames
can suppose that Nom
valuation with.
$\mathfrak{F},$$i_{x}^{V}=x$

F. Suppose that
, where. Let$\mathfrak{F}|\vdash PTh(F)\Rightarrow \mathfrak{F}\in$$=\{i_{x}|x\in|\mathfrak{F}|\}$$\mathfrak{M}=\langle \mathfrak{F}, V\rangle$$\mathfrak{F}|\vdash$PTh(F). We$\nabla$is the natural

90: pure, and,Let{
is satisfiable on}. Clearly,
under . Then, we can prove that Ag is satisfiable in , similarly to Theorem 25.
Let
for some. Since is closed under generated $sub\theta ames$ ,we may assume that or is generated by $\{i_{x}^{U}|x\in|\mathfrak{F}|\}(=Nom)$ . We can prove thefollowing [15, Claim 2 in the proo of Theorem 4.4.1]:$\Delta_{\mathfrak{F}}=$$\copyright_{i_{x}}\varphi|\varphi$$\langle \mathfrak{F},$$V\rangle,x|\vdash\varphi$$\mathfrak{F}$$\Delta_{\mathfrak{F}}$

$V$

$F$

$F$

$\mathfrak{E}\in F$$\langle \mathfrak{E}, U\rangle\vdash\Delta_{\mathfrak{F}}$$f$

CLAIM 4. For all pure]$H(\vec{\psi}$$, \copyright$)-fornulas$\langle \mathfrak{F}, \nabla\rangle$$\varphi,$te.

$\varphi\Leftrightarrow\langle \mathfrak{E}, U\rangle|\vdash\varphi$

and \langle &’,be -saturated elementary extensions. By elementarine $ss,$
F. In the same way in (Case 1) of the proof of Theorem 34, we
can construct a bisimulation system
to . By (i),and hence, by

Let

$($

$\langle \mathfrak{F}^{*}, V^{*}\rangle$$U^{*})$$\omega$$\mathfrak{E}\cdot\in$$\theta om\mathfrak{E}^{*}$

elementariness,$\mathfrak{F}\in F$$\mathfrak{F}^{*}\in F$$\mathfrak{F}^{r}$.

QED

In the case where is absolute for generated $sub\theta ames$ and $H(ffl])$ trivializes
generated subffames, we can prove, in the same way as Theorem 36, that for any
family of $H(\emptyset])- ffames,$ is purely $H(ffl$] )-definable $\approx F$ is closed underimages ofbisimulation system. Thus, in this case,]) andhave thesame expressive power with respect to an elementary family of ffames.
As in the same way in Section 4, we can obtain several semantical characterizations of the extended hybrid languages whose characterizations (for puredefinability) were previously unknown.
$\beta$$F$$F$$, \copyright$$H(\emptyset$$, \copyright$$H(\emptyset])$6 Conclusion
We can summarize our results as in Table 2. In the table, [Ags] (or [Adu]) means

Table 2: Summary of this paper

that
ofthe generalized hybrid language
is absolute forgenerated subffames (or disjoint unions, respectively). [Tgs] means thattrivializes generated subRames. (gs) (or, (ha), (um), (bs)) denotes the closure condition under generated subffames (or, hybrid amalgamations, ultrafilter morphic
images, images of bisimulation systems, respectively). (ele) means that a given$\beta=\{\beta_{0}|\square \in Mod\}$$H(\emptyset])$$H(\emptyset])$91class of ffames is elementary. Theorems 27 and 36 cover almost all extensionsofwith modal operators that have been already introduc $ed$, e.g., any nonempty subsets of$H(\copyright)$$\{[R], [R^{-1}], [W\backslash R], [W\backslash R^{-1}], [(R\cap=)], [(R\cap\neq)], [W^{2}], [\neq]\}$.

Acknowledgement
The author would like to thank SATO Kentaro for his invaluable comments.

References[1] C. Areces and B. ten Cate. Hybrid logics. In P. Blackbum, F. Wolter, andJ. van Benthem, editors, Handbook of Modal Logics. Elsevier, 2006. (In$prep\pi ation)$.

[2] J. van Benthem. Modal ffame classes revisited. Fundamenta Informaticae,

Vol. 18, pp. 303-17, 1993.

[3] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge Tracts

in Theoretical Computer Science. Cambridge University Press, Cambridge,

2001.

[4] C. C. Chang and H. J. Keisler. Model Theo’y. North-Holland Publishing
Company, Amsterdam, 3 edition, 1990.
[5] M. de Rijke. The modal logic of inequality. Journal of Symbolic Logic,

Vol. 57, pp. 56-84, 1992.

[6] G. Gargov and V. Goranko. Modal logic with names. Journal ofPhilosoph-

ical Logic, Vol. 22, pp. 607-36, 1993.

[7] R. I. Goldblatt and S. K. Thomason. Axiomatic classes in propositional

modal logic. In J. N. Crossley, editor, Algebra and Logic, pp. 163-73.
Springer-Verlag, 1975.

[8] H. J. Keisler. Limit ultrapowers. Transaction of American Mathematical$Socie\varphi$, Vol. 107, pp. 382-408, 1963.

[9] S. Kochen. Ultraproducts in the theory of models. Annals of Mathematics,

Vol. 74, pp. 221-61, 1961.

[10] A.N. Prior. Papers on fime and Tense. Oxford University Press, new edition,

2003.

92
Bimodal logics with the irreflexive modality.
Journal of the Japan Association for Philosophy of Science (in Japanese),
No. 106. (To appear).

[11] K. Sano and Y. Nakayama.

[12] K. Sano and K. Sato. Semantical characterization for irreflexive and gener-

alized modal languages. To app ar in Notre Dame Journal ofFormal Logic.
$e$[13] K. Sato. Fundamental theorem of extended modal model theory. Unpub-

lished.
[14] S. Shelah. Every two elementarily equivalent models have isomorphic ultra-

powers. Israel Journal ofMathematics, Vol. 10, pp. 224-33, 1972.

[15] B. ten Cate. Model theory for atended modal languages. PhD thesis, Uni-

versity ofAmsterdam, Institute for Logic, Language and Computation, 2005.