\begin{document}

\title{On Expressive Power and Class Invariance}
\author{Yanjing Wang\inst{1}\and Francien Dechesne\inst{2} \thanks{The authors are supported by 

NWO project VEMPS 612.000.528.}
}
\institute{CWI, Amsterdam, The Netherlands,

{\tt y.wang@cwi.nl}\\
\and Technische Universiteit Eindhoven, The Netherlands,

{\tt f.dechesne@tue.nl}
}
\maketitle

\begin{abstract}
In computer science, various logical languages are defined to analyze properties of systems. One way to pinpoint the essential differences between those logics is to compare their expressivity in terms of distinguishing power and expressive power. In this paper, we study those two concepts by regarding the latter notion as the former lifted to classes of models. We show some general results on lifting an invariance relation on models to one on classes of models, such that when the former corresponds to the distinguishing power of a logic, the latter corresponds to its expressive power, given certain compactness requirements. In particular, we introduce the notion of \textit{class bisimulation} to capture the expressive power of modal logics. We demonstrate the application of our results by revisiting   modal definability with our new insights.
\end{abstract}

\section{Introduction}

Logical languages are formal languages that can be used to express properties of mathematical structures: {\em models}. The standard notion for comparing how much logical languages can say about a certain class of models, are distinguishing power (can a language tell the difference between two models?), expressive power (which classes of models can be defined by a formula of the language?). 

The well-known hierarchy is as follows: distinguishing power is a coarser criterion for comparing languages than expressive power, e.g.~if two languages are equally distinguishing, they are not necessarily equally expressive, but if they are equally expressive, they are equally distinguishing. We can relate the two notions by observing that expressive power can be seen in terms of distinguishing power lifted to classes of models: a class of models is definable in a logic iff the logic can distinguish that class and its complement.

An important concept closely related to the distinguishing power in this context is \textit{structural equivalence} on models, e.g. isomorphism and bisimulation. Classic results showed that certain logics can only distinguish models up to certain structural equivalences, thus giving \textit{upper bounds} of the distinguishing power of the logics. In that case, the  structural equivalence is an \textit{invariance} relation for such logic. Under some restrictions, a structural equivalence may capture the distinguishing power of the logic precisely, such that two models can be distinguished by the logic iff they are equivalent according to the structural equivalence.

One goal of the paper is to sharpen the understanding of the difference between expressive and distinguishing power. 
We observe that expressive power can be seen as distinguishing power generalized to classes of models. This gives rise to the question whether a corresponding notion of invariance exists. In search of such notion, we generalize structural equivalence on models to structural relations on \textit{classes of models}, and use that for a notion of \textit{class invariance} for a logic that gives information about its expressive power. 

In Section~\ref{DandE} we study the expressive power as generalized distinguishing power in detail. We give some general invariance results in Section~\ref{secGen} on lifting structural equivalence on models to a relation on classes of models. We show that the two natural notions of class invariance correspond precisely to the class-equivalence and class-indistinguishability relations respectively, when restricted to \textit{compact classes}. This result is closely related to the use of compactness in existing Lindstr{\"o}m-type characterization theorems. 
In Section~\ref{secbis} we study class-bisimulation in the light of existing results on bisimulation.

We characterize modal definability by our notion of class-bisimilarity.

\paragraph{Related work.}
Comparing expressive power of different logics has always been a central issue in the study of logics. In the context of computer science, the work on comparing LTL and CTL is a notable example (a.o.~\cite{EmersonH83,BrowneClarkeGr87,ExCTLLTL,NainV07}), besides fundamental characterization theorems that capture the expressive power of modal logic and modal mu-calculus~\cite{Benthem,MuEx}. More recent results in terms of Lindstr{\"o}m-type characterization theorems also helped us sharpen our understanding on various fragments of FOL which are useful in computer science~\cite{BenthemMLLind07,LindTCate,LindTfragment}. More comprehensive discussions on the expressivity of modal logics can be found in~\cite{ModelModalHML}.

\section{Preliminaries} \langlebel{DandE}
In this section, we study the gap between distinguishing power and expressive power. 
When comparing two logics $L_1$ and $L_2$, we assume a given class of models $\mc{M}$ on which $L_1$ and $L_2$ are interpreted; we use `classes of models' usually for `subclasses of $\mc{M}$'. All logics in this paper are assumed to be 2-valued.

\subsection{Expressive Power as a Generalized Distinguishing Power}

As we mentioned in the introduction, the distinguishing power of a logic is its power to tell two models apart. We call a formula $\varphi$ in a language $L$ a \textit{separating formula} for models $M_1$ and $M_2$ ($\sepf{M_1}{\varphi}{M_2}$), if either $M_1\vDash\varphi$ and $M_2\not\vDash\varphi$, or vice versa. We write $\sepL{M_1}{L}{M_2}$ if there exists $\varphi\in L$ with $\sepf{M_1}{\varphi}{M_2}$.

We say $L_2$ is at least as \textit{distinguishing} as $L_1$ ($L_1\ensuremath{\alpha}adi[] L_2$)
iff
\[\forall M_1, M_2\in\mc{M}: \sepL{M_1}{L_1}{M_2} \textit{ implies }
\sepL{M_1}{L_2}{M_2}.\]

For expressive power, we say $L_2$ is at least as \textit{expressive} (in defining properties i.e. classes of models)
as logic $L_1$ on \ensuremath{\mc{M}}\ ($L_1{\ensuremath{\alpha}aex[]} L_2$)
iff
\[\forall\varphi_1\in L_1\exists\varphi_2\in L_2\forall M\in\mc{M}: M\vDash \varphi_1 \textit{ iff } M\vDash \varphi_2,\]

It is not hard to prove that $L_1\ensuremath{\alpha}aex[] L_2$ implies $L_1\ensuremath{\alpha}adi[] L_2$, but the converse may fail, as the following table, comparing several modal logics, shows.  

\begin{figure}
\caption{Some modal logics compared with respect to expressive and distinguishing power. The symbols $\saladi[],\eqdi[]$ and $\incdi[]$ stand for strictly less distinguishing, equally distinguishing and incomparable in distinguishing power respectively; $\salaex[],\eqex[]$ and $\incex[]$ are the respective counterparts for expressive power. In the table, $\ensuremath{\textit{ML}
\end{figure}

We now have a closer look at the notions of expressive and distinguishing power. The key observation is to view expressive power as distinguishing power on classes of models, with standard distinguishing power the special case for the restriction to singleton classes.

Like in the case for distinguishing power, we call a formula $\varphi$ in a language a \textit{separating formula} for classes of models $\mc{C}_1,\mc{C}_1i\subseteq\mc{M}$ ($\sepf{\mc{C}_1}{\varphi}{\mc{C}_1i}$), if either $$\mc{C}_1\subseteq\{M\in\mathcal{M}\mid M\vDash \varphi\} \textrm{ and } \mc{C}_1i\subseteq\{M\in\mathcal{M}\mid M\not\vDash \varphi\}\textrm{ or vice versa. }$$  We write $\sepL{\mc{C}_1}{L}{\mc{C}_1i}$ if there exists $\varphi\in L$ with $\sepf{\mc{C}_1}{\varphi}{\mc{C}_1i}$.  Note that $\sepf{\{M_1\}}{\varphi}{\{ M_2\}}\Leftrightarrow\sepf{M_1}{\varphi}{M_2}$ and that the existence of a separating formula for two classes of models implies that they are disjoint.

We can gradually fill up the gap between distinguishing power and expressive power, with a hierarchy of notions capturing the ability of languages to distinguish pairs of {\em classes of} models, where those classes have cardinality up to $\kappa$: $L_2$ is at least as {\em $\kappa$-distinguishing} as $L_1$($L_1\ensuremath{\alpha}adikk L_2$) iff $L_2$ can distinguish the same classes of size up to $\kappa$ as $L_1$. Formally, $L_1\ensuremath{\alpha}adikk L_2 \Leftrightarrow$\\
$$\forall \mc{C}_1, \mc{C}_1i\subseteq\mc{M} \textrm{ {\em of cardinality less than or equal to} } \kappa:
\sepL{\mc{C}_1}{L_1}{\mc{C}_1i} \Rightarrow \sepL{\mc{C}_1}{L_2}{\mc{C}_1i}.$$ We say $L_2$ is at least as {\em class-distinguishing} as $L_1$($L_1\ensuremath{\alpha}adicc L_2$) if $L_2$ can distinguish the same classes up to arbitrary size as $L_1$.

Now it is straightforward to see that $\kappa$-distinguishability coincides with standard distinguishability for $\kappa=1$. Standard expressivity coincides with class-distinguishability or $|\ensuremath{\mc{M}}|$-distinguishability if $\ensuremath{\mc{M}}$ is not a proper class as Theorem~\ref{Expr=ClassDist} shows:

 \begin{thm}\langlebel{Expr=ClassDist}
For logical languages $L_1,L_2$ that are interpretable on a class of models \ensuremath{\mc{M}}, the following are equivalent:
\begin{enumerate}
\item $L_2$ is at least as class-distinguishing as $L_1$ ($L_1\ensuremath{\alpha}adicc L_2$).
\item $L_2$ is at least as expressive as $L_1$ ($L_1\ensuremath{\alpha}aex L_2$).
\end{enumerate}
\end{thm}

The essence of the proof of Theorem~\ref{Expr=ClassDist} consists of the fact that
 a subclass $\mc{C}$ of $\mc{M}$ is definable by $L$ iff there exists a separating formula in $L$ for $\mc{C}$ and $\overline{\mc{C}}=\mc{M}\setminus\mc{C}$. 
(Cf.~Appendix~\ref{app-Expr=ClassDist}.)

Since $\ensuremath{\alpha}adi$ is $\ensuremath{\alpha}adikk$ for $\kappa=1$, we have:

\begin{cor}
$L_1\ensuremath{\alpha}aex L_2$ implies $L_1\ensuremath{\alpha}adi L_2$.
\end{cor}

From the above results we know that expressive power can be approximated by distinguishing power for increasing sizes of classes of models.
However, the hierarchy may collapse due to the presence in the logical languages of certain connectives (which correspond to set-theoretic operations), as the following result shows:

\begin{thm}[Collapsing theorem]
If $L_2$ contains negation and $\kappa$-ary disjunction and conjunction, then  $L_1\ensuremath{\alpha}adi L_2$ iff $L_1{\ensuremath{\alpha}adikk}L_2$.
\end{thm}

\begin{proof}
Right to left is obvious, we prove from left to right.
Assume $L_1\ensuremath{\alpha}adi L_2$, and suppose $\mc{C}_1,\mc{C}_1i\subseteq{\mc{M}}$ are of cardinality $\leq\kappa$, and $\sepL{\mc{C}_1}{L_1}{\mc{C}_1i}$. Then, in particular, for each $M_1\in \mc{C}_1$ and $M_2\in\mc{C}_1i$:
$\sepL{M_1}{L_1}{M_2}$. But because $L_1\ensuremath{\alpha}adi L_2$, then also $\sepL{M_1}{L_2}{M_2}$. For each pair $M_1\in \mc{C}_1$ and $M_2\in\mc{C}_1i$, pick a formula $\psi({M_1,M_2})\in L_2$
such that $\sepL{M_1}{\psi({M_1,M_2})}{M_2}$. Without loss of generality, because $L_2$ contains negation, we can take the $\psi({M_1,M_2})$ such that they are true on the $M_1 (\in \mc{C}_1)$, and false on the $M_2 (\in\mc{C}_1i)$.
But then for each $M_1\in \mc{C}_1$: $\bigwedge_{M_2\in\mc{C}_1i}\psi(M_1,M_2)\in L_2$ separates $\{M_1\}$ and ${\mc{C}_1i}$,
and hence: $\bigvee_{M_1\in\mc{C}_1}\bigwedge_{M_2\in\mc{C}_1i}\psi(M_1,M_2)\in L_2$ separates $\mc{C}_1$ and ${\mc{C}_1i}$.
So: $\sepL{\mc{C}_1}{L_2}{\mc{C}_1i}$.

Hence: $L_1\ensuremath{\alpha}adi L_2$ implies $L_1{\ensuremath{\alpha}adikk}L_2$.
\qed\end{proof}
From the above theorem, it is straightforward to see that distinguishing power and expressive power coincide if we restrict to finite model classes and a logic with the usual connectives:
\begin{cor}\langlebel{1=n}
If $L_2$ contains $\lor,\langlend$ and $\neg$, then for each $\kappa<\ensuremath{\alpha}eph_0$, $L_1\ensuremath{\alpha}adi L_2\Leftrightarrow L_1{\ensuremath{\alpha}adikk} L_2$ .
\end{cor}

\subsection{Induced Equivalence Relation}
In the previous subsection, we viewed distinguishing power and expressive power in terms of the abilities of the languages to separate model classes. Now we take a dual perspective, namely the equivalence induced by the limit of distinguishing power over classes, since this will lead us to the notion of invariance.

Let $\equiv_L$ be the \textit{induced equivalence relation} of language $L$ such that for all $M_1,M_2\in\ensuremath{\mc{M}}$:
$M_1\equiv_L M_2$ iff $M_1$ and $M_2$ satisfy exactly the same set of $L$-formulas. Note that $\sepL{M_1}{L}{M_2}$ iff $M_1\not\equiv_L M_2$, so we can easily prove:
\begin{thm}\langlebel{IndEquiv=Indist}
 $L_1\ensuremath{\alpha}adi L_2$ iff~~$\equiv_{L_2}\subseteq \equiv_{L_1} $ .
\end{thm}

The theorem states: logical languages that induce a finer equivalence relation, have stronger distinguishing power and vice versa. We thus can compare distinguishing power of two logics by comparing their induced equivalence relations. As we mentioned in the introduction, given a logic, we would like to find a {\em structural} characterizations of its induced equivalence, as a structural measure of its distinguishing power. We call an equivalence relation $\sim$ on a class of models $\mc{M}$ an \textit{invariance} for $L$ on $\mc{M}$ if for all $M_1,M_2\in\mc{M}$:
 $$M_1\sim M_2 \Rightarrow M_1\equiv_L M_2.$$

Various structural invariance relations for logics are known, like bisimulation for modal logic and isomorphism for first-order logic. Sometimes we have a precise structural characterization of the induced equivalence, e.g. two pointed Kripke models are bisimilar iff they satisfy the same set of infinitary modal formulas \cite{mlbook}. So bisimulation coincides with the induced equivalence relation for $\ensuremath{\textit{ML}}inf$. However, for many temporal logics including $\mu$-calculus $\ensuremath{L_{\mu}}$, bisimulation is an invariance relation but not the induced equivalence relation: it is possible to find two non-bisimilar models that can not be told apart by \ensuremath{L_{\mu}}~\cite{MucalcHML}. It follows that \ensuremath{\textit{ML}}inf\ is strictly more distinguishing than $\ensuremath{L_{\mu}}$. On the other hand, $\ensuremath{L_{\mu}}$ and $\ensuremath{\textit{ML}}inf$ are not comparable in terms of expressive power since $\ensuremath{L_{\mu}}$ can define well-foundedness while $\ensuremath{\textit{ML}}inf$ can not, cf.~\cite{MucalcHML}.

We now investigate whether we can define a relation on models that similarly corresponds to expressive power. A promising candidate is class equivalence:  
\begin{defi} Define the equivalence $\equivC{L}$ induced by $L$ on classes of models by
$\mc{C}_1\equivC{L} \mc{C}_1i\Leftrightarrow(\forall{\varphi\in L}, \mc{C}_1\vDash\varphi \text{ iff\ } \mc{C}_1i\vDash\varphi)$,
where $\mc{C}_1,\mc{C}_1i\subseteq\mc{M}$ and $\mc{C}\vDash\varphi$ iff $\forall M\in \mc{C},M\vDash\varphi$.
\end{defi}

However, this natural notion of equivalence notion does not match class-indis\-tinguishability, as the following Proposition shows:
\begin{prop}
For all classes of models $\mc{C}_1,\mc{C}_1i\subseteq\mc{M}$:
$\sepL{\mc{C}_1}{L}{\mc{C}_1i}\Rightarrow \mc{C}_1\not\equivC{L}\mc{C}_1i $,
but the converse does not hold in general.
\end{prop}
\begin{proof}
$\Rightarrow$ is trivial.

To see that the converse does not hold, we may take some formula $\psi\in L$ that is contingent on $\mc{M}$ (i.e. $\psi$ can be satisfiable but not valid on $\ensuremath{\mc{M}}$). Now let $\mc{C}_1$ be the class of models defined by $\psi$, and let $\mc{C}_1i$ be $\mc{M}$. Then $\mc{C}_1\subset\mc{C}_1i$, so they are not distinguishable (distinguishability implies disjointness). But obviously $\mc{C}_1\not\equivC{L}\mc{C}_1i$, because $\mc{C}_1\vDash\psi$ but {\em not} $\mc{C}_1i\vDash\psi$. So, the right-to-left-implication does not hold.
\qed\end{proof}

The relation that corresponds to class-indistinguishability is the following:
\begin{defi} For classes of models $\mc{C}_1,\mc{C}_1i\subseteq\mc{M}$, we define the symmetric relation $\asymp_L$ of $L$ by:
\[\mc{C}_1\asymp_L\mc{C}_1i\Leftrightarrow\forall{\varphi\in L}:
(\mc{C}_1\vDash\varphi \Rightarrow \mc{C}_1i\nvDash\neg \varphi)\langlend (\mc{C}_1i\vDash\varphi \Rightarrow \mc{C}_1\nvDash\neg \varphi)\]

\end{defi}

It is easy to see that $\mc{C}_1\not\asymp_L\mc{C}_1i\Leftrightarrow \sepL{\mc{C}_1}{L}{\mc{C}_1i}$ (but note that $\asymp_L$ is not an equivalence relation, as it does not satisfy transitivity in general).

Thus we have:
\begin{thm}
$L_1\ensuremath{\alpha}aex L_2 \Leftrightarrow \asymp_{L_2}\subseteq\asymp_{L_1}.$ 
\end{thm}

\section{Class Invariance}\langlebel{secGen}
In this section, we propose two ways to lift the structural equivalence to class similarity relations which can be used as candidates for the structural characterization of $\equivC{L}$ and $\asymp_L$. We show in Theorem~\ref{DimpE} that they are indeed class invariance relations if they are based on model invariance relations for the same language $L$.
\begin{defi}\langlebel{classlift}
Given an equivalence relation $\sim$ on models, we can lift $\sim$ to a relation on classes of models in the following two ways:
\begin{itemize}
\item $\mc{C}_1\ulcornertA{\sim}\mc{C}_1i$ iff:
\begin{itemize}
\item for each $M_1\in \mc{C}_1$ there is $M_2\in \mc{C}_1i$ such that $M_1\sim M_2$.
\item for each $M_2\in \mc{C}_1i$ there is $M_1\in \mc{C}_1$ such that $M_1\sim M_2$.
\end{itemize}
\item $\mc{C}_1\ulcornertE{\sim}\mc{C}_1i$ iff there are two models $M_1\in \mc{C}_1$ and $M_2\in \mc{C}_1i$ such that $M_1\sim M_2$.
\end{itemize}
\end{defi}
It is easy to see that $\ulcornertE{\sim}$ and $\ulcornertA{\sim}$ are indeed generalizations of $\sim$: $M\sim N\Leftrightarrow \{M\}\ulcornertE{\sim}\{N\}\Leftrightarrow \{M\}\ulcornertA{\sim}\{N\}.$
\begin{rema}
The above definitions give rise to some intuitive class comparison games that naturally lift the model comparison game for $\sim$. For example, considering $\ulcornertE{\sim}$, define $G_E^{\sim}(\mc{C}_1,\mc{C}_1i)$ for classes $\mc{C}_1,\mc{C}_1i$ of models as follows: Verifier chooses two models $M,N$ from $\mc{C}_1$ and $\mc{C}_1i$ respectively. Then he plays the model comparison game $\mathit{MC}^{\sim}(M,N)$ with Spoiler, if $\mathit{MC}^{\sim}(M,N)$ is defined. Verifier wins iff he wins in $\mathit{MC}^{\sim}(M,N)$. 
Depending on the type of $\mathit{MC}^{\sim}(M,N)$ (e.g. n-round, unbounded, infinitary) and the the results on $\mathit{MC}^{\sim}(M,N)$ with respect to certain language $L$, we may characterize $\asymp_{L'}$ with $L'$ being a fragment of $L$, by the Verifier's winning strategies of the game $G_E^{\sim}(\mc{C}_1,\mc{C}_1i)$. 
(Space limitations prevent us from elaborating further on the game perspective in this paper.)
\end{rema}

We can show that if $\sim$ is an invariance for $L$ then the lifted relations $\ulcornertA{\sim}$ and $\ulcornertE{\sim}$ are invariance relations for the class equivalence or class indistinguishability respectively.
\begin{thm}\langlebel{DimpE}
$\forall M,N: M\sim N\Rightarrow M\equiv_L N$ implies:
\begin{enumerate}
\item $\forall \mc{C}_1,\mc{C}_1i:\mc{C}_1\ulcornertA{\sim} \mc{C}_1i \Rightarrow \mc{C}_1\equivC{L}\mc{C}_1i$
\item  $\forall \mc{C}_1,\mc{C}_1i:\mc{C}_1\ulcornertE{\sim} \mc{C}_1i \Rightarrow \mc{C}_1\asymp_{{L}}\mc{C}_1i$
\end{enumerate}
\end{thm}
\begin{proof}
(1) is obvious, we only prove (2). If $\mc{C}_1\ulcornertE{\sim}\mc{C}_1i$, then there are $M\in \mc{C}_1, N\in \mc{C}_1i$ such that $M\sim N$. For any formula $\phi$ such that $\mc{C}_1\vDash\phi$, we know $M\vDash\phi.$ Since $M\sim N$ implies $M\equiv_L N$, we have $N\vDash\phi$. Therefore $\mc{C}_1i\not\subseteq \{M\mid M\nvDash\phi\}$.
\qed\end{proof}

As we have seen in the examples, $\forall M,N: M\sim N\Leftrightarrow M\equiv_L N$ does not imply $\forall \mc{C}_1,\mc{C}_1i:\mc{C}_1\ulcornertE{\sim} \mc{C}_1i \Leftrightarrow \mc{C}_1\equivC{L}\mc{C}_1i$ in general, otherwise there would be no difference between distinguishing power and expressive power. Now let ${\ensuremath{\mathcal{L}^{\infty}_{\infty}}}$ be a logical language with arbitrarily large (up to class-size) conjunctions and disjunctions. We then have the following straightforward results:
\begin{thm}\langlebel{Linf}
$\forall M,N: M\sim N\Leftrightarrow M\equiv_{\ensuremath{\mathcal{L}^{\infty}_{\infty}}} N$ implies:
\begin{enumerate}
\item $\forall \mc{C}_1,\mc{C}_1i:\mc{C}_1\ulcornertA{\sim} \mc{C}_1i \Leftrightarrow \mc{C}_1\equivC{\ensuremath{\mathcal{L}^{\infty}_{\infty}}}\mc{C}_1i$
\item  $\forall \mc{C}_1,\mc{C}_1i:\mc{C}_1\ulcornertE{\sim} \mc{C}_1i \Leftrightarrow \mc{C}_1\asymp_{{\ensuremath{\mathcal{L}^{\infty}_{\infty}}}}\mc{C}_1i$
\end{enumerate}
\end{thm}
\begin{proof} We again only show (2), and due to Theorem~\ref{DimpE} we only need to show $\Rightarrow$.
Suppose $\mc{C}_1\asymp_{\ensuremath{\mathcal{L}^{\infty}_{\infty}}}\mc{C}_1i$. Towards contradiction, suppose there are no models $M\in \mc{C}_1$, $N\in\mc{C}_1i$ such that $M\sim N$. Then since $\forall M,N: M\sim N\Leftrightarrow M\equiv_L N$, we can find a differential formula $\varphi_{M,N}$ in $\ensuremath{\mathcal{L}^{\infty}_{\infty}}$ for each $M\in \mc{C}_1$ and $N\in \mc{C}_1i$ such that $M\vDash \varphi_{M,N}$ but $N\nvDash\varphi_{M,N}$. Let $\psi$ be $\bigvee_M\bigwedge_{N}\varphi_{M,N}$ then $\mc{C}_1\vDash \psi$ but $\mc{C}_1i\vDash \neg \psi$, contradiction.
\qed\end{proof}

We call a class of models $\mc{C}$ \textit{$L$-compact}, if for any set of $L$-formulas $\Sigma$: every finite subset of $\Sigma$ is satisfiable in $\mc{C}$ implies that $\Sigma$ itself is satisfiable in $\mc{C}$. For example, any class of finitely many mutually $L$-nonequivalent models is $L$-compact.\footnote{If not, there is an infinite set $\Sigma$ of $L$-formulas such that each finite subset of $\Sigma$ is satisfiable, but $\Sigma$ is not satisfiable as a whole. Then, for each equivalence class $[M]$ of $\equiv_L$ in $\mc{C}$, pick a $\phi_{[M]}\in\Sigma$ that does not hold on the models in $[M]$. Let $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta=\{\varphi_{[M]}|M\in\mc{C}\}\subseteq\Sigma$, then $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ is finite but not satisfiable on $\mc{C}$. Contradiction.} In the following we always assume that $L$ contains binary conjunction $\langlend$ with its normal semantics. We show that if we restrict to $L$-compact classes then $\ulcornertA{\sim}$ and $\ulcornertE{\sim}$ match $\equivC{L}$ and $\asymp_{L} $ exactly, given that $\sim$ matches $\equiv_L$ exactly.  To obtain this result, we use the following lemma: 

\begin{lem}\langlebel{lem-compactC}
If $\forall M,N\in\mc{M}: M\sim N\Leftrightarrow M\equiv_L N$ then for any $L$-compact $\mc{C}\subseteq\ensuremath{\mc{M}}$ and $N\in\ensuremath{\mc{M}}$, (1) implies (2):
\begin{enumerate}
\item for all $\varphi\in L: \mc{C}\vDash\varphi\Rightarrow N\vDash\varphi$.
\item there is a model $M\in \mc{C}$ such that $M\sim N$.
\end{enumerate}
\end{lem}
\begin{proof}
Suppose (1), and towards contradiction suppose there is no model in $\mc{C}$ such that $M\sim N$. Let $\Sigma=\{\varphi\mid N\vDash \varphi\}.$ Since $\forall M,N\in\mc{M}: M\sim N\Leftrightarrow M\equiv_L N$, $\Sigma$ is not satisfiable in $\mc{C}$, otherwise there is a model $M\in\mc{C}$ such that $M\sim N$. Since $\mc{C}$ is $L$-compact, there is a finite subset $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ of $\Sigma$ such that $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ is not satisfiable in $\mc{C}$. Clearly, $\mc{C}\subseteq\{M\in\ensuremath{\mc{M}}|M\nvDash\bigwedge\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta\}$. From (1) we know $N\nvDash\bigwedge\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ contradictory to $N\vDash\Sigma$.
\qed\end{proof}
\begin{thm}\langlebel{thm-compactC}
Suppose $\forall M,N\in\mc{M}: M\sim N\Leftrightarrow M\equiv_L N$. For $L$-compact classes $\mc{C}_1$ and $\mc{C}_1i$ of $\ensuremath{\mc{M}}$ the following hold: 
\begin{enumerate}
\item  $ \mc{C}_1\ulcornertA{\sim}\mc{C}_1i\Leftrightarrow \mc{C}_1\equivC{L}\mc{C}_1i$
\item $ \mc{C}_1\ulcornertE{\sim}\mc{C}_1i\Leftrightarrow \mc{C}_1\asymp_L \mc{C}_1i$
\end{enumerate}
\end{thm}

\begin{proof}
We only show the direction $\mathcal{L}eftarrow$ in (2). The proof of (1) is similar but simpler.

Suppose $\mc{C}_1$ and $\mc{C}_1i$ are $L$-compact and $\mc{C}_1\asymp_L \mc{C}_1i$. Now suppose towards contradiction that $\mc{C}_1\ulcornertE{\not\sim}\mc{C}_1i$. Then there are no models $M\in\mc{C}_1$ and $N\in\mc{C}_1i$ such that $M\sim N.$ We claim the following:
$$\textrm{ for each } N\in\mc{C}_1i \textrm{ there is some }\varphi_N\in L \textrm{ such that }\mc{C}_1\vDash\varphi_N \textrm{ and }N\nvDash \varphi_N $$
Suppose not, then there would be a model $N\in\mc{C}_1i$ such that for all $\varphi:\mc{C}_1\vDash\varphi_N \Rightarrow N\vDash \varphi_N$. From Lemma~\ref{lem-compactC} there is $M\in \mc{C}_1$ such that $M\sim N$, contradictory to the assumption.

Let $\Sigma$ be the collection of such formulas: $\{\varphi_N\mid N\in\mc{C}_1i\}$.
Clearly, $\Sigma$ is not satisfiable in $\mc{C}_1i$, but $\mc{C}_1\vDash\Sigma$. Since $\mc{C}_1i$ is $L$-compact, there is a finite subset $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ of $\Sigma$ which is not satisfiable in $\mc{C}_1i$.  It is easy to see that $\mc{C}_1i\subseteq \{M\mid M\nvDash\bigwedge\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta\}$. However, $\mc{C}_1\vDash\bigwedge\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$. Therefore $\mc{C}_1\not\asymp_L \mc{C}_1i$, contradiction.
\qed\end{proof}
From the definition of $L$-compact classes, it is straightforward to see that:
\begin{prop}\langlebel{prop-CC2CL}
Suppose $L$ contains negation. If for every class $\mc{C}\subseteq\ensuremath{\mc{M}}$ there is an $L$-compact class $\mc{C}'$ such that $\mc{C}\equivC{L}\mc{C}'$, then $L$ is compact. 
\end{prop}
\begin{proof}
Given an arbitrary set of $L$-formulas $\Sigma$, if every finite subset of $\Sigma$ is satisfiable in $\mc{C}$ then every finite subset of $\Sigma$ is satisfiable in the compact $\mc{C}'$ (otherwise there would be a finite $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta\subseteq\Sigma$ such that $\mc{C}\nvDash\neg\bigwedge\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ but $\mc{C}'\vDash\neg\bigwedge\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$, which is a contradiction). Since $\mc{C}'$ is compact, there is a model $M\in \mc{C}'$ such that $M\vDash\Sigma$. Thus $L$ is compact.
\qed\end{proof}

\begin{prop}\langlebel{prop-CdefC}
 If $L$ is compact, then $L$ only defines $L$-compact classes. 
\end{prop}
\begin{proof}
 Suppose $L$ is compact and defines the non-compact class $\mc{C}\subseteq{\mc{M}}$ by $\varphi\in L$. Let $\Sigma$ be a witness to the non-$L$-compactness of $\mc{C}$, i.e.\ every finite subset of $\Sigma$ is satisfiable on $\mc{C}$, but not $\Sigma$ itself. Note that every finite subset of $\Sigma'=\Sigma\cup\{\varphi\}$ is then satisfiable on $\mc{C}$, and therefore on $\mc{M}$. By compactness of $L$, $\Sigma'$ is then satisfied by some $M\in\mc{M}$. But then $M\vDash\Sigma$ and $M\in\mc{C}$ by $M\vDash\varphi$. Contradiction.
\qed\end{proof}

\begin{thm}\langlebel{thm-main}
 If $L_2$ is a language extension of $L_1$  ($L_1\subseteq L_2$), then:
\begin{enumerate}
\item An $L_2$-compact class is also $L_1$-compact. 

\item If $L_1$ and $L_2$ are compact and contain $\neg$ then they have the same distinguishing power iff they have the same expressive power.
\item If $L_1$ and $L_2$ have the same distinguishing power and contain $\neg$ then: $L_1\salaex L_2\Leftrightarrow L_2$ defines some non-$L_2$-compact class which can not be defined by $L_1$. 
\end{enumerate}
\end{thm}
\begin{proof}
For (1): trivially by $L_1\subseteq L_2$. 

For (2), $\mathcal{L}eftarrow$ is obvious; we need to show $\Rightarrow.$  Suppose $L_1$ and $L_2$ have the same distinguishing power. Then $\equiv_{L_1}=\equiv_{L_2}$. Since $L_2$ extends $L_1$, we only need to show $L_2\ensuremath{\alpha}aex L_1$. From Proposition~\ref{prop-CdefC} and the fact that $L_1$ and $L_2$ are compact, we know that $L_1$ and $L_2$ can only define $L_1$- and $L_2$-compact classes respectively. We only need to show that if $L_2$ can define an $L_2$-compact class $\mc{C}$, then $L_1$ can also define it,i.e.\ for any $L_2$-compact class $\mc{C}: \mc{C}\not\asymp_{L_2}\overline{\mc{C}}\Rightarrow \mc{C}\not\asymp_{L_1}\overline{\mc{C}}$. Now suppose for an $L_2$-compact class $\mc{C}:$ $\mc{C}\not\asymp_{L_2}\overline{\mc{C}}$. Since $L_2$ contains negation, from Proposition~\ref{prop-CdefC} it is easy to see that $\overline{\mc{C}}$ is also $L_2$-compact. From statement (1), $\mc{C}$ and $\overline{\mc{C}}$ are also $L_1$-compact.  From Theorem~\ref{thm-compactC}, we know that it is \textit{not} the case that $\mc{C}\ulcornertE{(\equiv_{L_2})}\overline{\mc{C}}$.\footnote{cf.~Def.\ref{classlift}, replace $\sim$ by $\equiv_{L_2}$.} Since $\equiv_{L_1}=\equiv_{L_2}$, it is \textit{not} the case that $\mc{C}{\ulcornertE{(\equiv_{L_1})}}\overline{\mc{C}}$. Again from Theorem~\ref{thm-compactC}, $\mc{C}{\not\asymp_{L_1}}\overline{\mc{C}}$.

For (3), $\mathcal{L}eftarrow$ is trivial. For $\Rightarrow,$ suppose towards contradiction that $L_1\salaex L_2$, but that for all classes $\mc{C}$ that are {\em not} $L_2$-compact: if $L_2$ can define $\mc{C}$, then so can $L_1$. Because $L_1\salaex L_2$, then there must be an $L_2$-compact class $\mc{C}$ which is definable by $L_2$ but not definable by $L_1$. From Proposition~\ref{prop-CdefC}, $\mc{C}$ and $\overline{\mc{C}}$ are both $L_1$- and $L_2$-compact. However, according to Theorem~\ref{thm-compactC}, with similar technique used in the proof of (2) we can show that $\mc{C}$ is then definable by $L_1$, contradiction. 
\qed\end{proof}

\paragraph{Discussion} Statements (2) and (3) of Theorem~\ref{thm-main} are closely related to some well-known results. Recent results on Lindstr\"{o}m-type theorems for fragments $L$ of first-order logic are often formalized in the following form~\cite{BenthemMLLind07,LindTCate,LindTfragment}:
\begin{center}
\textit{A logic $L'$ that extends $L$ has equal expressive power as $L$ iff:\\
 (a) $L'$ is compact and (b) $L'$-formulas are invariant for some $\sim$. }
\end{center}
It follows from statement (2) that for compact logics, in order to obtain such theorem from right to left, we only need to show that the extended logic $L'$ has the same {\em distinguishing power} as $L$, which in principle is weaker. 
This gives an alternative perspective on the classical model theoretic arguments in~\cite{ModelModalHML,MCSF}, that use compactness for proving characterization results. Condition (b) helps to limit the distinguishing power with the presence of (a) but with some hurdles to overcome, cf.\ the discussions in~\cite{LindTfragment}.

Statement (3) gives us a hint on how to show that two equally distinguishing logics have different expressive power. This task is often considered hard. However, due to statement (3), we only need to concentrate on non-$L$-compact classes. This could explain the complicated constructions in many works on expressivity of temporal logic. For example, in~\cite{BrowneClarkeGr87}, it is shown that if a $\ensuremath{\mathit{CTL}}star$ formula does not correspond to a $\ensuremath{\mathit{CTL}}$ formula then it must have an infinite number of mutually nonequivalent finite models. Now this is just a straightforward consequence of our general result.

\section{Application: Class Bisimulation and Modal Logic}\langlebel{secbis}
In this section, we focus on \textit{class bisimulation} $\ulcornertE{\bis}$, the lifted notion of bisimulation $\bis$. We will demonstrate that such particular structural relations on classes can be studied in a similar way as the equivalence relations on models. As we will see in the following, most of the definitions and results about bisimulation and modal logic can be adapted to the corresponding ones for class bisimulation. As an example, we show a class bisimulation characterization of modal definability similar to the previous result in \cite{UUpuremodal}.

\subsection{Standard Bisimulation}
We first recall some standard results of bisimulation and modal logic, which we will use intensively in the next subsection.
Let $M$ and $N$ be two Kripke models with set of states $S$ and $T$. A binary (symmetric) relation $R \subseteq S\times T$ is a \textit{bisimulation} relation if $sRt$ implies:
\begin{enumerate}
\item $V(s)=V(t)$
\item if $s\to s'$ in $M$ then there is a $t'$ such that $t\to t'$ in $N$ and $s'Rt'$;
\item if $t\to t'$ in $M$ then there is a $s'$ such that $s\to s'$ in $N$ and $t'Rs'$.
\end{enumerate}
For two pointed models $M,s$ and $N,t$, we say $M,s$ is bisimilar to $N,t$ ($M,s\bis N,t$) if there is a bisimulation $R$ between $M$ and $N$ and $(s,t)\in R$. Note that in this section we will only talk about \textit{pointed Kripke models}. We may also call them \textit{pointed models} or simply \textit{models} for short.

We call a pointed Kripke model $M,s$ \textit{modally-saturated} or simply \textit{m-saturated} if for any state $w\in M$ and any set of $\ensuremath{\textit{ML}}$ formula $\Sigma$: if every finite subset of $\Sigma$ is satisfiable at the successors of $w$ then $\Sigma$ is satisfiable at some successor of $w$. We say a class of models $\mc{M}$ for a logic $L$ has the \textit{Hennessy-Milner property} for $\ensuremath{\textit{ML}}$ if for all models $M,s,N,t\in\mc{M}$:$$M,s\equiv_\ensuremath{\textit{ML}} N,t \Rightarrow M,s\bis N,t.$$

Here we list some standard results cf.~\cite{mlbook}. First, bisimulation is an invariance for \ensuremath{\textit{ML}}:
\begin{thm}\langlebel{bisinv}
If pointed Kripke models $M,s\bis N,t$ then $M,s\equiv_{\ensuremath{\textit{ML}}} N,t.$
\end{thm}
Let $\mathfrak{ue}(M),\pi_s$ be the \textit{pointed} \textit{ultrafilter extension}\footnote{An ultrafilter extension of a Kripke model $M=\langle W,R,V\rangle$ is again a Kripke model where the set of worlds is the set of ultrafilters over $W$; two ultrafilters $u$ and $v$ are linked by a relation iff $X\in v$ implies the set of points which \textit{sees} $X$ through a relation in $M$ is in $u$. The valuation of proposition letter $p$ at $u$ is true iff $V(p)\in u$. For the formal definition of ultrafilter extension cf.~\cite{mlbook}.} of a model $M,s$, with the principal ultrafilter $\pi_s$ generated by $s$ as its designated point. We know that:
\begin{thm}\langlebel{ueequiv}
For any pointed model $M,s:$ $M,s\equiv_{\ensuremath{\textit{ML}}}\mathfrak{ue}(M),\pi_s$ and $\mathfrak{ue}(M),\pi_s$ is m-saturated.
\langlebel{uethem}
\end{thm}
The above Theorem implies the following \textit{bisimulation-somewhere-else} result:
\begin{thm}\langlebel{bissomewhereelse}
For pointed models: $M,s\equiv_{\ensuremath{\textit{ML}}} N,t \Leftrightarrow \mathfrak{ue}(M),\pi_s\bis \mathfrak{ue}(N),\pi_t$.
\end{thm}
Let $\mc{C}^m$ be the class of m-saturated pointed Kripke models. Bisimulation coincides with the induced equivalence relation of \ensuremath{\textit{ML}}\ on $\mc{C}^m$:
\begin{thm}\langlebel{biscoi}
$\mc{C}^m$ enjoys Hennessy-Milner property for \ensuremath{\textit{ML}}. Thus for any $M,s$, $N,t\in \mc{C}^m: M,s\bis N,t \Leftrightarrow M,s\equiv_{\ensuremath{\textit{ML}}} N,t$.
\end{thm}
The last standard result we want to mention here is that bisimulation coincides with induced equivalence relation of \ensuremath{\textit{ML}}inf\ (\ensuremath{\textit{ML}}\ with conjunction over any set):
\begin{thm}\langlebel{MLinf}
$M,s\bis N,t \Leftrightarrow M,s\equiv_{\ensuremath{\textit{ML}}inf} N,t$
\end{thm}
Moreover, we can actually show that the class of $m$-saturated models is the biggest class which contains $\mc{C}^m$ and satisfies Hennessy-Milner property for \ensuremath{\textit{ML}}.
\begin{thm}\langlebel{biggesthmclass}
For any class of pointed models (generated by the designated points) $\mc{C}\supset\mc{C}^m$, there exist models $M,s,N,t\in \mc{C}$ such that $M,s\equiv_\ensuremath{\textit{ML}} N,t$ but $M,s\not \bis N,t$.
\end{thm}
\begin{proof}
The proof makes use of the next lemma, Lemma~\ref{m-bis}. See Appendix~\ref{app-biggesthmclass}.
\qed\end{proof}
\begin{lem}\langlebel{m-bis}
If $M,s\bis N,t$ and $N,t$ is m-saturated, then $M,s$ is m-saturated too.
\end{lem}
\begin{proof}
See Appendix~\ref{app-m-bis}.
\qed\end{proof}
\subsection{Class Bisimulation}\langlebel{Cbis}
In this section, we prove the analogies of the results in the previous section w.r.t class bisimulation $\ulcornertE{\bis}$. Corresponding results w.r.t $\ulcornertA{\bis}$ can be also proved with little adaptation.

From Theorem~\ref{DimpE} and Theorem~\ref{bisinv}, we know that $\ulcornertE{\bis}$ is the class invariance for \ensuremath{\textit{ML}}, namely for any classes of models $\mc{C}_1$ and $\mc{C}_1i$: $$\mc{C}_1\ulcornertE{\bis} \mc{C}_1i\Rightarrow \mc{C}_1\asymp_{\ensuremath{\textit{ML}}} \mc{C}_1i.$$ However the converse is not true even when we restrict to m-saturated models. According to Theorem~\ref{thm-compactC}, such counterexample must involve non-compact classes. For example, let $\mc{C}_1=\{M_1, M_2,\dots\}$ be the set of all the finite walks while $\mc{C}_1i=\{M_0\}$ where $M_0$ is a single point with self-loop.
\begin{exm}\langlebel{ex2}
$\mc{C}_1\ulcornertE{\not\bis} \mc{C}_1i$ but $\mc{C}_1\asymp_\ensuremath{\textit{ML}} \mc{C}_1i.$\\ 

\centerline{
$\xymatrix@R-5pt@C-5pt@M-4pt{\bullet\ar[d] & \bullet\ar[d] &\bullet\ar[d]  &\dots & & & \bullet\ar@(ul,ur) \\

\bullet & \bullet\ar[d] &\bullet\ar[d]  & \dots &  & & \\
& \bullet &\bullet\ar[d]  &\dots &  & & \\
&         &\bullet  & \dots&  & &\\

& &\mc{C}_1 & & & & \mc{C}_1i }$
}
\end{exm}

Note that $M_0$ is not bisimilar to any of the models in $\mc{C}_1$. However we can show that $\mc{C}_1\asymp_L \mc{C}_1i$. Suppose not, then there is a formula $\varphi\in L$ such that $\mc{C}_1\vDash \neg \varphi $ and $\mc{C}_1i\vDash \varphi$. Since $\varphi$ is satisfiable at the tree unraveling of $M_0$, it must be satisfiable at a finite submodel of it due to the finite depth property of \ensuremath{\textit{ML}}. However, any finite submodel of the unraveling of $M_0$ is just a finite walk. Thus there is a $k$ such that $M_k\vDash \varphi$. Therefore $\mc{C}_1\nvDash \neg \varphi$. Contradiction.

Like in the case of standard bisimulation, we want to identify the collections of model classes where class bisimulation coincides with the class equivalence relation of modal logic. Thus we need to lift the notion of m-saturated models.
\begin{defi}[Modally-saturated class]
A class $\mc{C}$ of pointed Kripke models is \textit{m-saturated} if each model in $\mc{C}$ is m-saturated and $\mc{C}$ is $\ensuremath{\textit{ML}}$-compact.
\end{defi}
The following is a corollary of Theorem~\ref{biscoi} and Theorem~\ref{thm-compactC}:
\begin{thm}\langlebel{cbiscoin}
If $\mc{C}_1$ and $\mc{C}_1i$ are m-saturated then $ \mc{C}_1\ulcornertE{\bis}\mc{C}_1i\Leftrightarrow \mc{C}_1\asymp_L \mc{C}_1i$..
\end{thm}

The \textit{class-bisimulation-somewhere-else} result corresponding to Theorem~\ref{bissomewhereelse} requires the following generalization of ultrafilter extensions which aims to make a class m-saturated.
\begin{defi}[Ultrafilter extension of classes]
Given a class $\mc{C}$ of pointed models, let $S_{\mc{C}}$ be the set of designated points of the models in $\mc{C}$. We define the  \textit{ultrafilter extension} of a class $\mc{C} $(written $\mathfrak{ue}(\mc{C}))$ as a new class of models as follows:  $$\mathfrak{ue}(\mc{C})=\{\mathfrak{ue}(\biguplus\mc{C}),u\mid u\in U_\mc{C}\}$$ 
where $U_{\mc{C}}=\{u\mid u\in\mathfrak{ue}(\biguplus\mc{C})$ and $\forall X\in u: X\cap S_{\mc{C}}\not=\emptyset \}$, and $\biguplus\mc{C}$ the disjoint union of models in $\mc{C}$ (as unpointed models). Then $\mathfrak{ue}(\{M,s\})=\{\mathfrak{ue}(M),\pi_s\}$.
\end{defi}
Note that our purpose is to make a class m-saturated by a operation on class of models, like ultrafilter extension does on single model. This means we need to include many auxiliary models to make the class \ensuremath{\textit{ML}}-compact. It is not hard to see that the pointed models in $\mathfrak{ue}(\mc{C})$ are defined differently than the \textit{Ultraunions} in \cite{UUpuremodal}, where $\mathfrak{ue}(\biguplus\mc{C}),u$ is called an \textit{ultraunion} of $\mc{C}$ iff $u\in U_{\mc{C}}'=\{u\mid  u\in \mathfrak{ue}(\biguplus\mc{C}) \textrm{ and $u$ contains all the cofinite subsets of $S_\mc{C}$}\}$. First of all, $U_{\mc{C}}'$ does not contain principal ultrafilters generated by $s\in S_{\mc{C}}$. Moreover, when we restrict ourselves to non-principal ultrafilters of $\biguplus\mc{C}$, $U_{\mc{C}}'$ is still a subset of $U_{\mc{C}}$. To see this we can prove:
\begin{prop}\langlebel{prop-diff}
If $S_{\mc{C}}$ is infinite, $U_{\mc{C}}'\subseteq U_{\mc{C}}|_{np}$ where $$U_{\mc{C}}|_{np}=\{u\mid u\in U_\mc{C} \textrm{ and $u\not=\pi_s$ for any  $s\in S_\mc{C}$} \}.$$
Moreover if $\biguplus\mc{C}\backslash S_{\mc{C}}$ is infinite, then $U_{\mc{C}}'\subset U_{\mc{C}}|_{np}.$
\end{prop}
\begin{proof}
See Appendix~\ref{app-prop-diff}.
\qed\end{proof}
Now we want to show an analogy of Theorem~\ref{bissomewhereelse}:
\begin{thm}[Class Bisimulation somewhere else]\langlebel{cbissomewhereelse} For all classes of pointed Kripke models  $\mc{C}_1$ and $\mc{C}_1i$:
$\mc{C}_1\asymp_{\ensuremath{\textit{ML}}}\mc{C}_1i\Leftrightarrow \mathfrak{ue}(\mc{C}_1)\ulcornertE{\bis} \mathfrak{ue}(\mc{C}_1i).$

\end{thm}
To prove this theorem, we need Theorem~\ref{cbiscoin} and the following two lemmas.

\begin{lem}\langlebel{cueequiv}
For any class of pointed Kripke models $\mc{C}$, any $\varphi\in\ensuremath{\textit{ML}}:$
$$\mc{C}\vDash\varphi\Leftrightarrow \mathfrak{ue}(\mc{C})\vDash \varphi$$
\end{lem}
\begin{proof}
$\mathcal{L}eftarrow:$ Note that for all $s\in S_{\mc{C}}$: $\mathfrak{ue}(\biguplus\mc{C}),\pi_s\in \mathfrak{ue}(\mc{C})$ where $\pi_s$ is the principal ultrafilter generated by $s$. Assume $\mathfrak{ue}(\mc{C})\vDash \varphi$ then for all $s\in S_{\mc{C}}$: $\mathfrak{ue}(\biguplus\mc{C}),\pi_s\vDash\varphi.$ Thus from Theorem~\ref{ueequiv} and the preservation result for disjoint union, $\mc{C}\vDash\varphi$.

$\Rightarrow:$ Suppose $\mc{C}\vDash\varphi$, then $S_\mc{C}\subseteq V_{\biguplus\mc{C}}(\varphi)$ where $V_{\biguplus\mc{C}}(\varphi)=\{w\mid  \biguplus\mc{C},w\vDash \varphi\}$. Now we need to show that for all $u\in U_{\mc{C}}$: $\mathfrak{ue}(\biguplus\mc{C}),u\vDash \varphi.$ Since $\mathfrak{ue}(\biguplus\mc{C})$ is the ultrafilter extension of $\biguplus\mc{C}$, it amounts to prove for every $u\in U_{\mc{C}}$: $$ V_{\biguplus\mc{C}}(\varphi)\in u $$ Suppose not, then $\overline{V_{\biguplus\mc{C}}(\varphi)}\in u$, due to the fact that $u$ is an ultrafilter. Since $S_\mc{C}\subseteq V_{\biguplus\mc{C}}(\varphi)$, $\overline{V_{\biguplus\mc{C}}(\varphi)}\cap S_{\mc{C}}=\emptyset$, in contradiction to the assumption that $u\in U_{\mc{C}}.$
\qed\end{proof}

\begin{lem}\langlebel{cuems}
For any class $\mc{C}$ of pointed Kripke models, $\mathfrak{ue}(\mc{C})$ is m-saturated.
\end{lem}
\begin{proof} Since all the models in $\mathfrak{ue}(\mc{C})$ are ultrafilter extensions thus m-saturated, we only need to show that $\mathfrak{ue}(\mc{C})$ is \ensuremath{\textit{ML}}-compact.  
Given a class $\mc{C}$ of pointed Kripke models, suppose every finite subset of $\Sigma$ is satisfiable in $\mathfrak{ue}(\mc{C})$. We claim that:
$$ \textrm{every finite subset of $\Sigma$ is satisfiable in $\{\biguplus\mc{C},s\mid s\in S_{\mc{C}}\}$ }$$
Suppose not, then there is a finite $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta\subseteq \Sigma$ such that $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ is not satisfiable in $\{\biguplus\mc{C},s\mid s\in S_{\mc{C}}\}$. Thus for any $s\in S_{\mc{C}}: \biguplus\mc{C},s\vDash\neg\bigwedge\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$. Therefore from the preservation property of the disjoint union, for any pointed model $M,s\in \mc{C}:M,s\vDash\neg\bigwedge\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ and then $\mc{C}\vDash\neg \bigwedge\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta.$ From Lemma~\ref{cueequiv}, $\mathfrak{ue}(\mc{C})\vDash\neg\bigwedge\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ contradictory to the assumption that every finite subset of $\Sigma$ is satisfiable in $\mathfrak{ue}(\mc{C})$.

Now let $$F_{\mc{C}}(\Sigma)=\{V'_{\biguplus\mc{C}}(\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta)\mid \ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta \textrm{ is a finite subset of }\Sigma\}$$ where $V'_{\biguplus\mc{C}}=\{s\mid s\in S_{\mc{C}}\textrm{ and } \biguplus\mc{C},s\vDash\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta\}.$ It is not hard to see that $F_{\mc{C}}(\Sigma)$ has the finite intersection property since:
\begin{enumerate}
\item for any finite subsets $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ and $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta'$ of $\Sigma:$
$V'_{\biguplus\mc{C}}(\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta)\cap V'_{\biguplus\mc{C}}(\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta')=V'_{\biguplus\mc{C}}(\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta\cup\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta')$
\item $ V'_{\biguplus\mc{C}}(\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta\cup\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta')\not=\emptyset \textrm{ according to the above claim}.$
\end{enumerate}
From Ultrafilter Theorem cf.~\cite{mlbook}, $F_{\mc{C}}(\Sigma)$ can be extended to an ultrafilter $u^*$. Now for any $\varphi\in\Sigma$, clearly $V_{\biguplus\mc{C}}(\varphi)\in u^*$ since $V'_{\biguplus\mc{C}}(\varphi)\subseteq V_{\biguplus\mc{C}}(\varphi)$ and $V'_{\biguplus\mc{C}}(\varphi)\in u^*$. Thus from the construction of ultrafilter extension, $\mathfrak{ue}(\biguplus\mc{C}),u^*\vDash\varphi.$ Therefore $\mathfrak{ue}(\biguplus\mc{C}),u^*\vDash\Sigma.$

We now only need to prove that $u^*\in U_{\mc{C}}$, namely for all $X\in u^*: X\cap S_{\mc{C}}\not=\emptyset.$ Suppose not, then there is an $X$ such that $X\cap S_{\mc{C}}=\emptyset$. However, since $F_{\mc{C}}(\Sigma)\subseteq S_{\mc{C}}$, there is an $Y\in u^*:X\cap Y=\emptyset$. Then $u^*$ is not an ultrafilter, contradiction.
\qed\end{proof}

The previous two lemmas complete the proof for Theorem~\ref{cbissomewhereelse}. 

As a corollary of Theorem~\ref{cbissomewhereelse} we can give a class-bisimulation characterization of the modally-definable classes:
\begin{cor}\langlebel{cordef}
A class of pointed model $\mc{C}$ is \textbf{not} definable in $\ensuremath{\textit{ML}}$ iff $\mathfrak{ue}(\mc{C})\ulcornertE{\bis}\mathfrak{ue}(\overline{\mc{C}}).$
\end{cor}
\begin{proof}
Follows from Theorem~\ref{cbissomewhereelse}.
Note that $\mc{C}$ is not definable by a single \ensuremath{\textit{ML}}\ formula iff $\mc{C}\asymp_{\ensuremath{\textit{ML}}}\overline{\mc{C}}$. 
\qed\end{proof}
It follows that:
\begin{cor}
A class of pointed Kripke model $\mc{C}$ is definable in $\ensuremath{\textit{ML}}$ iff $\mc{C}$ and $\overline{\mc{C}}$ are closed under bisimulation and $\mathfrak{ue}$(namely $\mathfrak{ue}(\mc{C})\subseteq \mc{C}$).
\end{cor}
\begin{proof}
$\Rightarrow$ is straightforward. We now prove $\mathcal{L}eftarrow$. Note that from Corollary~\ref{cordef}, we only need to show
$$\textrm{ $\mc{C}$ and $\overline{\mc{C}}$ are closed under bisimulation and $\mathfrak{ue}$ implies $\mathfrak{ue}(\mc{C})\ulcornertE{\not\bis}\mathfrak{ue}(\overline{\mc{C}})$}$$
Suppose $\mathfrak{ue}(\mc{C})\ulcornertE{\bis}\mathfrak{ue}(\overline{\mc{C}})$, namely there are $M,s\in\mathfrak{ue}(\mc{C})$ and $N,t\in\mathfrak{ue}(\overline{\mc{C}})$ such that $M,s\bis N,t$. Now suppose $\mc{C}$ and $\overline{\mc{C}}$ are closed under $\mathfrak{ue}$, then $M,s\in\mc{C}$ and $N,t\in\overline{\mc{C}}$. Since $M,s\bis N,t$ then $\mc{C}$ is not closed under bisimulation.
\qed\end{proof}

We have to be careful if we want to obtain the analogy of Theorem~\ref{MLinf}. A natural question to ask is whether we can get rid of class-size conjunction and disjunctions in Theorem~\ref{Linf}, but only use \ensuremath{\textit{ML}}inf\ that is the modal logic with conjunctions over arbitrarily large sets. Unfortunately, we observe that the following is not true:
$$\mc{C}_1\asymp_{\ensuremath{\textit{ML}}inf}\mc{C}_1i\Leftrightarrow \mc{C}_1\bis^{E}_{\mc{C}} \mc{C}_1i \quad (\divideontimes)$$

Consider an example from \cite{ModelModalHML} (where it is used to show that \ensuremath{\textit{ML}}inf\ can not define well-foundedness). For each ordinal $\ensuremath{\alpha}pha$, let $M_\ensuremath{\alpha}pha=\{\{\beta \mid \beta\leq \ensuremath{\alpha}pha\},R\}$ be its reverse, i.e.\ $R=\{(\beta,\beta')\mid \beta'<\beta\leq\ensuremath{\alpha}pha\}$. Let $M_\ensuremath{\alpha}pha'$ be the modification of $M_\ensuremath{\alpha}pha$ with $R$ replaced by $R'=R\cup\{(\ensuremath{\alpha}pha,\ensuremath{\alpha}pha)\}.$ Now let $C_1$ be the class of reserved ordinals $M_\ensuremath{\alpha}pha$ and $C_2$ be the class of modified reversed ordinals $M_\ensuremath{\alpha}pha'$. It is not hard to see that none of the two models in these two classes are bisimilar to each other.  However, from \cite{ModelModalHML} we know that there is no \ensuremath{\textit{ML}}inf\ formula to separate $\mc{C}_1$ from $\mc{C}_1i$, namely $\mc{C}_1\asymp_{\ensuremath{\textit{ML}}inf} \mc{C}_1i$. Thus $\divideontimes$ does not hold.

As an analogy of Theorem~\ref{biggesthmclass} about Hennessy-Milner property, we can actually show that m-saturated classes constitute the core of the maximal collection $\mc{K}$ of model classes which has the following property: $$\forall \mc{C}_1,\mc{C}_1i\in \mc{K}: \mc{C}_1\bis^E_\mc{C}\mc{C}_1i\Leftrightarrow \mc{C}_1\asymp_\ensuremath{\textit{ML}} \mc{C}_1i \quad(\circledast)$$
Let $\mc{K}^m$ be the collection of model classes which extend some m-saturated classes by possibly adding modally-equivalent m-saturated models. Given a model class $\mc{C}$, let $\mc{C}|_m$ be the class of m-saturated models in $\mc{C}$. Formally, $$\mc{K}^m=\{ \mc{C}\mid \mc{C}|_m \textrm{ is m-saturated and }\forall M\in\mc{C}\exists M'\in\mc{C}|_m:M\equiv_\ensuremath{\textit{ML}} M' \}$$
We now prove the following theorem:
\begin{thm}\langlebel{largestcollclassthm}
$\mc{K}^m$ is the largest collection of model classes that contains $\mc{K}^m$ and satisfies $(\circledast)$.
\end{thm}
\begin{proof}
See Appendix~\ref{app-largestcollclassthm}.
\qed\end{proof}

\section{Conclusion and Future Work}
In this paper, we studied the expressive power as class-distinguishing power in depth. We lifted the notion of invariance to classes of models aiming to capture the expressive power of logics. On compact classes, the lifted notions of class invariance captures the expressive power precisely. In particular, we focused on the notion of \textit{class bisimulation} and demonstrated the application of our results by revisiting modal-definability with our new insights which may shorten the proof. It makes clear that compactness of classes of models plays an important role in obtaining precise structural characterizations of expressive power. If two logics satisfy the compactness property, their comparison in terms of distinguishing power conincides with their comparison in terms of expressive power. This helps to obtain characterization of compact logics in terms of Lindstr\"{o}m-type theorems. However, compactness fails on non-elementary extension of FOL (e.g.\ modal $\mu$-calculus) or fragments of FOL restricted on finite models. We may look for different classes of models with different lifting method for such case to characterize the expressive power.  

{\scriptsize
 

 

}

\appendix
\noindent{\bf\mathcal{L}arge Appendix}

\section{Proof of Theorem~\ref{Expr=ClassDist}}
\langlebel{app-Expr=ClassDist}
\begin{proof}
\begin{description}
 \item[($1\Rightarrow 2$)] Suppose $L_2$ is at least as class-distinguishing as $L_1$, and let
$\mc{C}$ be a class of models definable by $\varphi_1\in L_1$. Then $\mc{C}=\{M\in\mathcal{M}\mid M\vDash\varphi_1\}$ and its complement $\overline{\mc{C}}=\{M\in\mathcal{M}\mid M\not\vDash\varphi_1\}$. Since $\varphi_1$ separates $\mc{C}$ and its complement, it follows from the assumption that there exists a separating formula $\varphi_2\in L_2$ for $\mc{C}$ and its complement. But then either $\mc{C}=\{M\in\mathcal{M}\mid M\vDash\varphi_2\}$ and $\overline{\mc{C}}=\{M\in\mathcal{M}\mid M\nvDash\varphi_2\}$ or vice versa. In any case $\mc{C}$ is definable in $L_2$.

 \item[($2\Rightarrow 1$)] Suppose $L_2$ is at least as expressive as $L_1$, and let $\mc{C}_1$, $\mc{C}_1i$ be classes of models in $\mathcal{M}$. Suppose there exists a separating formula $\varphi_1\in L_1$ for $\mc{C}_1$ and $\mc{C}_1i$ such that $\mc{C}_1\subseteq \{M\mid M\vDash\varphi_1\}$ and $\mc{C}_1i\subseteq \{M\mid M\nvDash\varphi_1\}$. Since $L_2$ is at least as expressive, there is a formula $\varphi_2$ in $L_2$ such that $$\{M\in\mathcal{M}\mid M\vDash\varphi_1\}=\{M\in\mathcal{M}\mid M\vDash\varphi_2\}.$$ But then obviously $\varphi_2$ is a separating formula for $\mc{C}_1$ and $\mc{C}_1i$ in $L_2$.
 \end{description}
\qed\end{proof}
\section{Proof of Proposition~\ref{prop-diff}}
\langlebel{app-prop-diff}
\begin{proof}
First note that for any $u\in U_\mc{C}$, if $u$ is not a principal ultrafilter generated by some $s\in S_{\mc{C}}$ then it is not a principal ultrafilter. Suppose not, then $u$ is generated by a $s'\not\in S_\mc{C}$. Since $\{s'\}\cap S_{\mc{C}}=\emptyset$, $u\not\in U_\mc{C},$ contradiction. Now we know that $U_{\mc{C}}|_{np}$ only contains non-principal ultrafilters. Since $S_\mc{C}$ is infinite, for any co-finite subset $X$ of $\biguplus\mc{C}$: $X\cap S_\mc{C}\not=\emptyset$. Thus we have: $$U_{\mc{C}}|_{np}=\{u\mid  \textrm{ $u$ contains all co-finite subsets of $\biguplus\mc{C}$ and $\forall X\in u: X\cap S_\mc{C}\not=\emptyset$ }\}$$
Suppose $u\in U'_\mc{C}.$ According to the definition, $u$ contains all cofinite subsets of $S_\mc{C}$. Now we show $u\in U_\mc{C}$ by checking whether all co-finite subsets of $\biguplus\mc{C}$ are in $u.$ Take a co-finite subset $X$ of $\biguplus\mc{C}$. It is not hard to see that $X\cap S_\mc{C}$ is co-finite in $S_\mc{C}.$ Thus $X\cap S_\mc{C}\in u$, then by closure property of ultrafilter $u$, $X\in u.$

If $\biguplus\mc{C}\backslash S_{\mc{C}}$ is infinite, then it is easy to see that $u^*\in U_\mc{C}$ where $$u^*=\{X\mid X \textrm{ is a co-finite subset of $\biguplus\mc{C}$}\}$$ however, $u^*\not\in U'_\mc{C}$ since it does not contain any co-finite subset of $S_\mc{C}.$
\qed 
\end{proof}

\section{Proof of Theorem~\ref{biggesthmclass}}
\langlebel{app-biggesthmclass}
\begin{proof}
Suppose towards contradiction that there is a class of pointed Kripke models $\mc{C}\supset\mc{C}^m$ such that $\mc{C}$ enjoys Hennessy-Milner property. Then there is a pointed model ($M,s$ generated by $s$) in $\mc{C}$ such that $M,s$ is not m-saturated. Now we consider the ultrafilter extension of pointed model $M$: $\mathfrak{ue}(M)$ (call the generated model $N,t$). From Theorem~\ref{uethem}, $M,s\equiv_{\ensuremath{\textit{ML}}}N,t$ and $N,t$ is m-saturated, thus $N,t\in\mc{C}$. Since $\mc{C}$ has Hennessy-Milner property, $M,s\bis N,t$. From Lemma~\ref{m-bis}, $M,s$ is m-saturated, contradiction.
\qed\end{proof}
\section{Proof of Lemma~\ref{m-bis}}
\langlebel{app-m-bis}
\begin{proof}
Suppose $M,s\bis N,t$ and $N,t$ is m-saturated. Towards contradiction suppose that pointed model $M,s$ is not m-saturated. Then there is a point $s'$ such that there is a set of \ensuremath{\textit{ML}}\ formulas $\Sigma$ for which each finite subset is satisfiable at successors of $s'$, but $\Sigma$ itself is not satisfiable at any successor of $s'$. Let $t'$ be the bisimilar point of $s'$ in $N$. We claim $$\textrm{every finite subset of $\Sigma$ is satisfiable at the successors of $N,t'$}.$$
To prove the claim, observe that for any finite subset $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ of $\Sigma$, $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}iamond\bigwedge\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ is satisfiable at $s'$. Since $M,s'\bis N,t'$ thus $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}iamond\bigwedge\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$ is satisfiable at $t'$, meaning that there is a successor of $t'$ such that $t'$ satisfies $\ensuremath{\mathcal{L}_{DEL^*}(\textit{Prop})}elta$. Therefore, every finite subset of $\Sigma$ is satisfiable at the successors of $t'$.

Now based on the claim, and the fact that $N,t$ is m-saturated, we have that $\Sigma$ is satisfiable at some successor $r$ of $t'$. However, there can not be a bisimilar successor of $s'$ in $M$ to $r$ in $N$, otherwise $\Sigma$ is satisfiable in a successor of $s'$. Thus $M,s'\not \bis N,t'$, contradiction.\qed
\end{proof}
\section{Proof of Theorem~\ref{largestcollclassthm}}
\langlebel{app-largestcollclassthm}
\begin{proof}
Suppose towards contradiction that there is a class $\mc{K}'\supseteq \mc{K}^m$ such that $(\circledast)$ holds for \ensuremath{\textit{ML}}. Then according to the definition of $\mc{K}^m$, there is a class $\mc{C}\in \mc{K}'$ such that either $\mc{C}|_m$ is not m-saturated or there is a model $M,s\in\mc{C}$ that is not equivalent to any m-saturated model in $\mc{C}$.

For the first case, there is a set of formulas $\Sigma$ such that it is not satisfiable in $\mc{C}|_m$ but each finite subset of $\Sigma$ is. Now consider the $\mathfrak{ue}(\mc{C})$. It is easy to see that $\Sigma$ is satisfiable  in $\mathfrak{ue}(\mc{C})$. Thus there is a m-saturated model $M,s$ in $\mathfrak{ue}(\mc{C})$ such that $M,s\vDash\Sigma$. We now take the class $\mc{C}'=\{M,s\}$, it is clear that $\mc{C}'\in \mc{K}'$ since it is m-saturated. Then for any $\phi\in\Sigma$, $\mc{C}\nvDash\neg\phi$ since $\phi$ must be satisfiable somewhere in $\mc{C}$. Thus it is not hard to verify that $\mc{C}\asymp_\ensuremath{\textit{ML}} \mc{C}'$. Now according to our assumption that $\mc{K}'$ has property $(\circledast)$ for \ensuremath{\textit{ML}}, we know that there is a model $N,t$ in $\mc{C}$ which is bisimilar to $M,s$. However, then $N,t\vDash\Sigma$, contradiction.

For the latter case, since $M,s$ is not m-saturated and we know there is no modally equivalent m-saturated model of $M,s$ in $\mc{C}$, thus $\mathfrak{ue}(M),\pi_s\not\in\mc{C}$. Now we consider $\mc{C}$ and $\mc{C}'=\{\mathfrak{ue}(M),\pi_s\}$. It is easy to see that $\mc{C}\asymp_\ensuremath{\textit{ML}}\mc{C}'$. However, there is no model $N,t$ in $\mc{C}$ such that $N,t\bis\mathfrak{ue}(M),\pi_s$, since otherwise according to Lemma~\ref{m-bis} and Theorem~\ref{ueequiv}, $N,t$ is m-saturated too and $N,t\equiv_\ensuremath{\textit{ML}} M,s.$
\qed\end{proof}

\end{document}