# Taming “McKinsey-like” formula: An Extended Correspondence and Completeness
Theory for Hybrid Logic H(@)

Zhiguang Zhao

###### Abstract

In the present article, we extend the fragment of inductive formulas for the
hybrid language $\mathcal{L}(@)$ in [8] including a McKinsey-like formula, and
show that every formula in the extended class has a first-order correspondent,
by modifying the algorithm $\mathsf{hybrid}$-$\mathsf{ALBA}$ in [8]. We also
identify a subclass of this extended inductive fragment, namely the extended
skeletal formulas, which extend the class of skeletal formulas in [8], each
formula in which axiomatize a complete hybrid logic. Our proof method here is
proof-theoretic, following [10, 19] and [3, Chapter 14], in contrast to the
algebraic proof in [8].

_Keywords_ : Hilbert system, hybrid logic, completeness theory, algorithmic
correspondence theory

##  1 Introduction

#### Hybrid logic

Hybrid logics [3, Chapter 14] refer to the class of logics which has higher
expressive power than modal logic where a special class of propositional
symbols called _nominals_ are used to refer to single states. A nominal is
true at exactly one world. Different logical connectives are used increase the
expressive power, e.g. the _satisfaction operator_ $@_{\mathbf{i}}\varphi$
which means $\varphi$ is true at the state denoted by $\mathbf{i}$. We use
$\mathcal{L}(@)$ to denote the hybrid language with nominals and satisfaction
operators, and $\mathbf{K}_{\mathcal{H}(@)}$ to denote the basic Hilbert
system.

#### Correspondence and completeness theory for hybrid logic

In modal logic, a modal formula corresponds to a first-order formula if they
are valid on the same class of frames. Sahlqvist [14] and van Benthem [18]
identified a class of modal formulas (later called _Sahlqvist formulas_) which
have first-order correspondents and axiomatize strongly complete normal modal
logics with respect to the class of frames defined by them.

There are extensitve research on the correspondence and completeness theory
for hybrid logic, see [1, 4, 5, 8, 9, 10, 11, 12, 15, 17, 19, 21, 22]. Gargov
and Goranko [9] proved that any extension of $\mathbf{K}_{\mathcal{H}}$ with
pure axioms (formulas that contain no ordinary propositional variables but
possibly contain nominals) is strongly complete. ten Cate and Blackburn [2]
proved that any pure extensions of $\mathbf{K}_{\mathcal{H}(@)}$ and
$\mathbf{K}_{\mathcal{H}(@,\downarrow)}$ are strongly complete. ten Cate, Marx
and Viana [17] proved that any extensions of $\mathbf{K}_{\mathcal{H}(@)}$
with modal Sahlqvist formulas (with no nominals but possibly with
propositional variables) are strongly complete, and that these two kinds of
results cannot be combined in general, since there is a pure formula and a
modal Sahlqvist formula which together axiomatize a Kripke-incomplete logic
when added to $\mathbf{K}_{\mathcal{H}(@)}$. Conradie and Robinson [8] studied
to what extent can these two results be combined in $\mathcal{L}(@)$, using
algorithmic and algebraic method. Zhao [21, 22] studies the correspondence and
completeness theory for $\mathcal{L}(@,\downarrow)$ following the algorithmic
methodology of [8].

#### Our contribution

In the present article, we extend the fragment of inductive formulas in [8] to
_extended inductive formulas_ for $\mathcal{L}(@)$, which contains a Mckinsey-
like formula, and show that every extended inductive formula has a first-order
correspondent, by modifying the Ackermann Lemma Based Algorithm
$\mathsf{hybrid}$-$\mathsf{ALBA}$ in [8] into another algorithm called
$\mathsf{ALBA}^{@}$. We also identify a subclass of this extended inductive
fragment, namely the _extended skeletal formulas_ , which extend the class of
skeletal formulas in [8], each formula in which axiomatize a complete hybrid
logic. Our proof method here is proof-theoretic, following [10, 19, 22] and
[3, Section 3.1 in Chapter 14], in contrast to the algebraic proof in [8]. We
define the class of extended skeletal formulas for $\mathcal{L}(@)$, show that
for every such formula $\varphi$ and its hybrid pure correspondence $\pi$,
$\mathbf{K}_{\mathcal{H}(@)}+\varphi$ proves $\pi$, therefore
$\mathbf{K}_{\mathcal{H}(@)}+\varphi$ is complete with respect to the class of
frames defined by $\pi$, using a restricted version
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ of the $\mathsf{ALBA}^{@}$.

#### Structure of the article

The structure of the article is as follows: Section 2 gives preliminaries on
hybrid logic $\mathcal{L}(@)$, including its syntax, semantics and basic
Hilbert system $\mathbf{K}_{\mathcal{H}(@)}$. Section 3 lists ingredients on
the algorithm and the completeness proof, and defines the expanded hybrid
modal language $\mathcal{L}(@)^{+}$, the first-order correspondence language
and the standard translation. Section 4 defines extended inductive formulas
and extended skeletal formulas. Section 5 gives the algorithm
$\mathsf{ALBA}^{@}$ and $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ for
$\mathcal{L}(@)$. Section 6 shows the soundness of the algorithm
$\mathsf{ALBA}^{@}$. Section 7 sketches the proof that $\mathsf{ALBA}^{@}$
succeeds on extended inductive formulas and
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ succeeds on extended skeletal
formulas. Section 8 proves that $\mathbf{K}_{\mathcal{H}(@)}$ extended with
extended skeletal formulas are strongly complete.

##  2 Preliminaries on hybrid logic $\mathcal{L}(@)$

In this section, we give preliminaries on the hybrid logic $\mathcal{L}(@)$ in
the style of [21]. For more details of hybrid logic, see [3, Chapter 14] and
[16].

###  2.1 Language and syntax

######  Definition 2.1.

Given a countably infinite set $\mathsf{Prop}$ of propositional variables and
a countably infinite set $\mathsf{Nom}$ of nominals which are disjoint, the
hybrid language $\mathcal{L}(@)$ is defined as follows:

$\varphi::=p\mid\mathbf{i}\mid\bot\mid\top\mid\neg\varphi\mid\varphi\lor\varphi\mid\varphi\land\varphi\mid\varphi\to\varphi\mid\Diamond\varphi\mid\Box\varphi\mid@_{\mathbf{i}}\varphi,$

where $p\in\mathsf{Prop}$, $\mathbf{i}\in\mathsf{Nom}$. We define
$\varphi\leftrightarrow\psi:=(\varphi\to\psi)\land(\psi\to\varphi)$. We say
that a formula is _pure_ if it contains no propositional variables. We use
$\sigma$ to denote a _sorted substitution_ that uniformly replaces
propositional variables by formulas and nominals by nominals.

We will use _inequalities_ of the form $\varphi\leq\psi$, where $\varphi$ and
$\psi$ are formulas, and _quasi-inequalities_ of the form
$\varphi_{1}\leq\psi_{1}\ \&\ \ldots\ \&\ \varphi_{n}\leq\psi_{n}\
\Rightarrow\ \varphi\leq\psi$. We will find it easy to work with inequalities
$\varphi\leq\psi$ in place of implicative formulas $\varphi\to\psi$ in Section
4.

###  2.2 Semantics

######  Definition 2.2.

A _frame_ is a pair $\mathbb{F}=(W,R)$ where $W\neq\varnothing$ is the
_domain_ of $\mathbb{F}$, $R\subseteq W\times W$ is the _accessibility
relation_. A _model_ is a pair $\mathbb{M}=(\mathbb{F},V)$ where
$V:\mathsf{Prop}\cup\mathsf{Nom}\to P(W)$ is a _valuation_ on $\mathbb{F}$
such that $V(\mathbf{i})\subseteq W$ is a singleton for all nominals
$\mathbf{i}\in\mathsf{Nom}$.

The satisfaction relation is given as follows: for any model
$\mathbb{M}=(W,R,V)$, any $w\in W$,

$\mathbb{M},w\Vdash p$ | iff |  $w\in V(p)$;
---|---|---
$\mathbb{M},w\Vdash\mathbf{i}$ | iff |  $\\{w\\}=V(\mathbf{i})$;
$\mathbb{M},w\Vdash\bot$ | : | never;
$\mathbb{M},w\Vdash\top$ | : | always;
$\mathbb{M},w\Vdash\neg\varphi$ | iff |  $\mathbb{M},w\nVdash\varphi$;
$\mathbb{M},w\Vdash\varphi\lor\psi$ | iff |  $\mathbb{M},w\Vdash\varphi$ or $\mathbb{M},w\Vdash\psi$;
$\mathbb{M},w\Vdash\varphi\land\psi$ | iff |  $\mathbb{M},w\Vdash\varphi$ and $\mathbb{M},w\Vdash\psi$;
$\mathbb{M},w\Vdash\varphi\to\psi$ | iff |  $\mathbb{M},w\nVdash\varphi$ or $\mathbb{M},w\Vdash\psi$;
$\mathbb{M},w\Vdash\Diamond\varphi$ | iff |  $\exists v(Rwv\ \mbox{ and }\ \mathbb{M},v\Vdash\varphi)$;
$\mathbb{M},w\Vdash\Box\varphi$ | iff |  $\forall v(Rwv\ \Rightarrow\ \mathbb{M},v\Vdash\varphi)$;
$\mathbb{M},w\Vdash@_{\mathbf{i}}\varphi$ | iff |  $\mathbb{M},V(\mathbf{i})\Vdash\varphi$.

For any formula $\varphi$,

  * •

$V(\varphi):=\\{w\in W\mid\mathbb{M},w\Vdash\varphi\\}$ denotes the _truth
set_ of $\varphi$ in $\mathbb{M}$.

  * •

$\varphi$ is _globally true_ on $\mathbb{M}$ (notation:
$\mathbb{M}\Vdash\varphi$) if $\mathbb{M},w\Vdash\varphi$ for every $w\in W$.

  * •

$\varphi$ is _valid_ on a frame $\mathbb{F}$ (notation:
$\mathbb{F}\Vdash\varphi$) if $\varphi$ is globally true on $(\mathbb{F},V)$
for each valuation $V$.

The semantics of inequalities and quasi-inequalities are given as follows:

  * •

$\mathbb{M}\Vdash\varphi\leq\psi\mbox{ iff }(\mbox{for all }w\in W,\mbox{ if
}\mathbb{M},w\Vdash\varphi,\mbox{ then }\mathbb{M},w\Vdash\psi).$

  * •

$\mathbb{M}\Vdash\varphi_{1}\leq\psi_{1}\ \&\ \ldots\ \&\
\varphi_{n}\leq\psi_{n}\ \Rightarrow\ \varphi\leq\psi\mbox{ iff }$

$(\mathbb{M}\Vdash\varphi_{i}\leq\psi_{i}\mbox{ for all }1\leq i\leq n)\mbox{
implies }(\mathbb{M}\Vdash\varphi\leq\psi).$

Validities for inequalities and quasi-inequalities are defined similar to
formulas. It is obvious that $\mathbb{M}\Vdash\varphi\leq\psi$ iff
$\mathbb{M}\Vdash\varphi\to\psi$.

###  2.3 Hilbert system

The Hilbert system $\mathbf{K}_{\mathcal{H}(@)}$ of $\mathcal{L}(@)$ is given
as follows (see [16]):

  * (CT)

$\vdash\varphi$ for all classical tautologies $\varphi$

  * (Dual)

$\vdash\Diamond p\leftrightarrow\neg\Box\neg p$

  * (K)

$\vdash\Box(p\to q)\to(\Box p\to\Box q)$

  * (K@)

$\vdash@_{\mathbf{i}}(p\to q)\to(@_{\mathbf{i}}p\to@_{\mathbf{i}}q)$

  * (Selfdual)

$\vdash\neg@_{\mathbf{i}}p\leftrightarrow@_{\mathbf{i}}\neg p$

  * (Ref)

$\vdash@_{\mathbf{i}}\mathbf{i}$

  * (Intro)

$\vdash\mathbf{i}\land p\to@_{\mathbf{i}}p$

  * (Back)

$\vdash\Diamond@_{\mathbf{i}}p\rightarrow@_{\mathbf{i}}p$

  * (Agree)

$\vdash@_{\mathbf{i}}@_{\mathbf{j}}p\to@_{\mathbf{j}}p$

  * (MP)

If $\vdash\varphi\to\psi$ and $\vdash\varphi$ then $\vdash\psi$

  * (SB)

If $\vdash\varphi$ then $\vdash\sigma(\varphi)$

  * (Nec)

If $\vdash\varphi$ then $\vdash\Box\varphi$

  * (Nec@)

If $\vdash\varphi$ then $\vdash@_{\mathbf{i}}\varphi$

  * (Name@)

If $\vdash@_{\mathbf{i}}\varphi$ then $\vdash\varphi$, for $\mathbf{i}$ not
occurring in $\varphi$

  * (BG@)

If $\vdash@_{\mathbf{i}}\Diamond\mathbf{j}\land@_{\mathbf{j}}\varphi\to\psi$,
then $\vdash@_{\mathbf{i}}\Diamond\varphi\to\psi$, for
$\mathbf{j}\neq\mathbf{i}$ and $\mathbf{j}$ not occurring in $\varphi$ and
$\psi$

We use $\mathbf{K}_{\mathcal{H}(@)}+\Sigma$ to denote the system containing
all axioms of $\mathbf{K}_{\mathcal{H}(@)}$ and $\Sigma$ and is closed under
the rules of $\mathbf{K}_{\mathcal{H}(@)}$. $\vdash_{\Sigma}\varphi$ means
$\varphi$ is a theorem of $\mathbf{K}_{\mathcal{H}(@)}+\Sigma$. When $\Sigma$
is empty, we use $\vdash\varphi$ instead of $\vdash_{\varnothing}\varphi$ .

$\Gamma\vdash_{\Sigma}\varphi$ means that there are
$\gamma_{1},\ldots,\gamma_{n}\in\Gamma$ such that
$\vdash_{\Sigma}\gamma_{1}\land\ldots\land\gamma_{n}\to\varphi$. Given a frame
class $\mathcal{F}$, we use $\Gamma\Vdash_{\mathcal{F}}\varphi$ to mean that
for any frame $\mathbb{F}=(W,R)\in\mathcal{F}$, any valuation $V$ on
$\mathbb{F}$, any point $w\in W$, if $\mathbb{F},V,w\Vdash\gamma$ for all
$\gamma\in\Gamma$, then $\mathbb{F},V,w\Vdash\varphi$.

The following is a theorem for any $\mathbf{K}_{\mathcal{H}(@)}+\Sigma$ where
$@_{\mathbf{j}}\alpha$ has a single positive occurrence in $\theta$. This will
be useful in Section 8:

$\vdash_{\Sigma}@_{\mathbf{i}}\theta(@_{\mathbf{j}}\alpha)\leftrightarrow@_{\mathbf{i}}\theta(\bot)\lor(@_{\mathbf{i}}\theta(\top)\land@_{\mathbf{j}}\alpha).$

######  Definition 2.3 (Soundness and Strong Completeness).

  * •

$\mathbf{K}_{\mathcal{H}(@)}+\Sigma$ is said to be _sound_ with respect to
$\mathcal{F}$, if $\Gamma\vdash_{\Sigma}\varphi$ implies that
$\Gamma\Vdash_{\mathcal{F}}\varphi$.

  * •

$\mathbf{K}_{\mathcal{H}(@)}+\Sigma$ is said to be _strongly complete_ with
respect to $\mathcal{F}$, if $\Gamma\Vdash_{\mathcal{F}}\varphi$ implies that
$\Gamma\vdash_{\Sigma}\varphi$.

######  Theorem 2.4 (Corollary in [16]).

If $\Sigma$ is a set of pure $\mathcal{L}(@)$-formulas, then
$\mathbf{K}_{\mathcal{H}(@)}+\Sigma$ is sound and strongly complete with
respect to the class of frames defined by $\Sigma$.

##  3 Ingredients of algorithmic correspondence

In this article, we give a modified version $\mathsf{ALBA}^{@}$ of the
correspondence algorithm $\mathsf{hybrid}$-$\mathsf{ALBA}$ defined in [8] for
$\mathcal{L}(@)$. The algorithm $\mathsf{ALBA}^{@}$ transforms the input
extended inductive hybrid formula $\varphi\to\psi$ into an equivalent set of
pure quasi-inequalities without propositional variables. This section follows
the style of [20].

The ingredients of algorithmic correspondence can be listed as follows:

  * •

An expanded hybrid modal language $\mathcal{L}(@)^{+}$, its semantics and its
standard translation into first-order correspondence language;

  * •

An algorithm $\mathsf{ALBA}^{@}$ which transforms a given extended inductive
hybrid formula $\varphi\to\psi$ into equivalent pure quasi-inequalities
$\mathsf{Pure}(\varphi\to\psi)$ as well as the first-order correspondent
$\mathsf{FO}(\varphi\to\psi)$;

  * •

The class of _extended inductive formulas_ , which is strictly larger than
inductive formulas defined in [8], on which $\mathsf{ALBA}^{@}$ is successful;

  * •

A soundness proof of the algorithm.

The ingredients of the completeness proof can be listed as follows:

  * •

A translation of the inequalities and quasi-inequalities involved in a
restricted version $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ of the algorithm
$\mathsf{ALBA}^{@}$ into $\mathcal{L}(@)$-formulas;

  * •

A proof that for any extended skeletal formula $\varphi\to\psi$, for each step
of the execution of $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$, the
translations of the resulting quasi-inequalities are provable in
$\mathbf{K}_{\mathcal{H}(@)}+(\varphi\to\psi)$, therefore $\pi$ is provable in
$\mathbf{K}_{\mathcal{H}(@)}+(\varphi\to\psi)$.

In the algorithmic correspondence part, we define an expanded hybrid modal
language $\mathcal{L}(@)^{+}$ which the $\mathsf{ALBA}^{@}$ will manipulate
(Section 3.1), the first-order correspondence language and the standard
translation (Section 3.2). We define the extended inductive/skeletal formulas
(Section 4), define the algorithms $\mathsf{ALBA}^{@}$ and
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ (Section 5), show their soundness
(Section 6) and success on extended inductive/skeletal formulas (Section 7).

In the completeness proof part, we give a translation of the inequalities and
quasi-inequalities involved in $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ into
$\mathcal{L}(@)$ and prove that for any extended skeletal formula
$\varphi\to\psi$, for each step of the execution of
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$, the translations of the resulting
quasi-inequalities are provable in
$\mathbf{K}_{\mathcal{H}(@)}+(\varphi\to\psi)$ (Section 8).

###  3.1 The expanded hybrid modal language $\mathcal{L}(@)^{+}$

We define the expanded hybrid modal language $\mathcal{L}(@)^{+}$ used in
$\mathsf{ALBA}^{@}$:

$\varphi::=p\mid\mathbf{i}\mid\bot\mid\top\mid\neg\varphi\mid\varphi\land\varphi\mid\varphi\lor\varphi\mid\varphi\to\varphi\mid\Box\varphi\mid\Diamond\varphi\mid@_{\mathbf{i}}\varphi\mid\blacksquare\varphi\mid\vardiamond\varphi$

For $\blacksquare$ and , they are interpreted as the box and diamond modality
on the inverse relation $R^{-1}$. For the semantics, the additional
connectives are interpreted as follows:

$\mathbb{M},w\Vdash\blacksquare\varphi$ | iff | $\forall v(Rvw\ \Rightarrow\ \mathbb{M},v\Vdash\varphi)$
---|---|---
$\mathbb{M},w\Vdash\vardiamond\varphi$ | iff |  $\exists v(Rvw\ \mbox{ and }\ \mathbb{M},v\Vdash\varphi)$.

###  3.2 The first-order correspondence language and the standard translation

In the first-order correspondence language, we have a binary predicate symbol
$R$ corresponding to the accessibility relation, unary predicate symbols $P$
corresponding to each propositional variable $p$, constant symbols $i$
corresponding to each nominal $\mathbf{i}$.

######  Definition 3.1.

The standard translation of $\mathcal{L}(@)^{+}$ is as follows:

  * •

$ST_{x}(p):=Px$;

  * •

$ST_{x}(\mathbf{i}):=x=i$;

  * •

$ST_{x}(\bot):=x\neq x$;

  * •

$ST_{x}(\top):=x=x$;

  * •

$ST_{x}(\neg\varphi):=\neg ST_{x}(\varphi)$;

  * •

$ST_{x}(\varphi\land\psi):=ST_{x}(\varphi)\land ST_{x}(\psi)$;

  * •

$ST_{x}(\varphi\lor\psi):=ST_{x}(\varphi)\lor ST_{x}(\psi)$;

  * •

$ST_{x}(\varphi\to\psi):=ST_{x}(\varphi)\to ST_{x}(\psi)$;

  * •

$ST_{x}(\Box\varphi):=\forall y(Rxy\to ST_{y}(\varphi))$;

  * •

$ST_{x}(\Diamond\varphi):=\exists y(Rxy\land ST_{y}(\varphi))$;

  * •

$ST_{x}(@_{\mathbf{i}}\varphi):=ST_{i}(\varphi)$;

  * •

$ST_{x}(\blacksquare\varphi):=\forall y(Ryx\to ST_{y}(\varphi))$;

  * •

$ST_{x}(\vardiamond\varphi):=\exists y(Ryx\land ST_{y}(\varphi))$.

It is obvious that the translation is correct:

######  Proposition 3.2.

For any model $\mathbb{M}$, any $w\in W$ and any $\mathcal{L}(@)^{+}$-formula
$\varphi$,

$\mathbb{M},w\Vdash\varphi\mbox{ iff }\mathbb{M}\vDash ST_{x}(\varphi)[w].$

For inequalities and quasi-inequalities, the standard translations are given
in a global way:

######  Definition 3.3.

  * •

$ST(\varphi\leq\psi):=\forall x(ST_{x}(\varphi)\to ST_{x}(\psi))$;

  * •

$ST(\varphi_{1}\leq\psi_{1}\ \&\ \ldots\ \&\ \varphi_{n}\leq\psi_{n}\
\Rightarrow\ \varphi\leq\psi):=ST(\varphi_{1}\leq\psi_{1})\land\ldots\land
ST(\varphi_{n}\leq\psi_{n})\to ST(\varphi\leq\psi)$.

######  Proposition 3.4.

For any model $\mathbb{M}$, any inequality $\mathsf{Ineq}$, any quasi-
inequality $\mathsf{Quasi}$,

$\mathbb{M}\Vdash\mathsf{Ineq}\mbox{ iff }\mathbb{M}\vDash ST(\mathsf{Ineq});$
$\mathbb{M}\Vdash\mathsf{Quasi}\mbox{ iff }\mathbb{M}\vDash
ST(\mathsf{Quasi}).$

##  4 Extended inductive/skeletal formulas

In the present section, we use the unified correspondence style definition
(cf. [6, 7, 13, 20]) to define extended inductive/skeletal formulas. We will
find it convenient to use inequalities $\varphi\leq\psi$ instead of
implicative formulas $\varphi\to\psi$. For formulas $\theta$ not of the form
$\varphi\to\psi$, we treat it as $\top\to\theta$.

######  Definition 4.1 (Order-type).

(cf. [6, page 346]) For any $n$-tuple $(p_{1},\ldots,p_{n})$ of propositional
variables, an _order-type_ $\varepsilon$ of this $n$-tuple is an element in
$\\{1,\partial\\}^{n}$. With respect to an order-type $\varepsilon$, we say
that $p_{i}$ has order-type 1 (resp. $\partial$) if $\varepsilon_{i}=1$ (resp.
$\varepsilon_{i}=\partial$), and write $\varepsilon(p_{i})=1$ (resp.
$\varepsilon(p_{i})=\partial$). We use $\varepsilon^{\partial}$ to denote the
opposite order-type of $\varepsilon$ where $\varepsilon^{\partial}(p_{i})=1$
if $\varepsilon(p_{i})=\partial$ and $\varepsilon^{\partial}(p_{i})=\partial$
if $\varepsilon(p_{i})=1$.

######  Definition 4.2 (Signed generation tree).

(cf. [7, Definition 4]) The _positive_ /_negative generation tree_ of an
$\mathcal{L}(@)^{+}$-formula $\varphi$ is defined as follows: we first label
the root of the syntactic generation tree of $\varphi$ with $+$ (resp. $-$),
then label the children nodes as below:

  * •

Label the same sign to the children nodes of a mother node labelled with
$\lor,\land,\Box$, $\Diamond$, $\blacksquare$, ;

  * •

Label the opposite sign to the child node of a mother node labelled with
$\neg$;

  * •

Label the opposite sign to the first child node and the same sign to the
second child node of a mother node labelled with $\to$;

  * •

Label the same sign to the second child node of a mother node labelled with
$@$ (notice that we do not label the first child node, i.e. the nominal node).

A node in a signed generation tree is called _positive_ (resp.  _negative_) if
it is signed $+$ (resp. $-$).

######  Example 4.3.

The positive generation tree of $+\Box(p\lor\neg\Diamond q)\to\Box q$ is given
in Figure 1.

$+\to$$-\Box$$-\lor$$-p$$-\neg$$+\Diamond$$+q$$+\Box$$+q$ Figure 1: Positive
generation tree for $\Box(p\lor\neg\Diamond q)\to\Box q$

We use $+\varphi$ and $-\psi$ in $\varphi\leq\psi$ when defining extended
inductive/skeletal inequalities. For any $\ast\in\\{+,-\\}$, $\ast\varphi$ is
_uniform_ in $p_{i}$ if all occurrences of $p_{i}$ in $\ast\varphi$ have the
same sign, and $\ast\varphi$ is $\varepsilon$-_uniform_ in an array $\vec{p}$
(notation: $\varepsilon(\ast\varphi)$) if $\ast\varphi$ is uniform in each
$p_{i}$ in $\vec{p}$, where $p_{i}$ always has the sign $+$ (resp. $-$) if
$\varepsilon(p_{i})=1$ (resp. $\partial$).

For any $\varepsilon$ over $(p_{1},\ldots p_{n})$, any $\varphi$, any
$i=1,\ldots,n$, any $\ast\in\\{+,-\\}$, an _$\varepsilon$ -critical node_ in
$\ast\varphi$ is a leaf node $+p_{i}$ when $\varepsilon(p_{i})=1$ or $-p_{i}$
when $\varepsilon(p_{i})=\partial$. An $\varepsilon$-critical branch in
$\ast\varphi$ is a branch from the root to an $\varepsilon$-critical node. The
$\varepsilon$-critical branches are those which $\mathsf{ALBA}^{@}$ and
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ will solve for.

We use $+\psi\prec\ast\varphi$ (resp. $-\psi\prec\ast\varphi$) to indicate
that an occurrence of a subformula $\psi$ inherits the positive (resp.
negative) sign from $\ast\varphi$. We use
$\varepsilon(\gamma)\prec\ast\varphi$ (resp.
$\varepsilon^{\partial}(\gamma)\prec\ast\varphi$) to denote that the signed
generation subtree $\gamma$, with the sign inherited from $\ast\varphi$, is
$\varepsilon$-uniform (resp. $\varepsilon^{\partial}$-uniform). $p$ is
_positive_ (resp.  _negative_) in $\varphi$ if $+p\prec+\varphi$ (resp.
$-p\prec+\varphi$) for all occurrences of $p$ in $\varphi$.

######  Definition 4.4.

(cf. [7, Definition 5]) Nodes in signed generation trees are called _outer
nodes_ and _inner nodes_ , according to Table 1. For the names of outer nodes
and inner nodes in the classification, see Remark 4.8. For the name SRA and
SRR, they stands for “syntactic right adjoint” and “syntactic right residual”,
respectively. This is based on the algebraic properties of the interpretations
of the connectives. For more details, see [13, Remark 3.24].

For any $\ast\in\\{+,-\\}$, a branch in a $\ast\varphi$ is called a _extended
good branch_ if it is the concatenation of three paths $P_{1},P_{2},P_{3}$,
one of which might be of length $0$, such that $P_{1}$ is a path from the leaf
consisting (apart from variable nodes) of inner nodes only, and $P_{2}$
consists (apart from variable nodes) of outer nodes only, and in $P_{3}$, the
node (apart from variable nodes) farthest to the root is $@$. A branch is
called a _extended skeletal branch_ if it is an extended good branch and the
path $P_{1}$ is of length 0. A branch is called a _good branch_ if it is an
extended good branch and the path $P_{3}$ is of length 0. A branch is called a
_skeletal branch_ if it is an extended good branch and the path $P_{1},P_{3}$
are of length 0.

Outer | Inner
---|---
| SRA
|  | $+$ | $\wedge$ | $\Box$ | $\neg$ | $@$
---|---|---|---|---
$-$ | $\vee$ | $\Diamond$ | $\neg$ | $@$
| SRR
| $+$ | $\vee$ | $\wedge$ | $\Diamond$ | $\neg$ | $@$ |
---|---|---|---|---|---|---
$-$ | $\wedge$ | $\vee$ | $\Box$ | $\neg$ | $@$ | $\to$
| $+$ | $\vee$ | $\to$
---|---|---
$-$ | $\wedge$ |
Table 1: Outer and Inner nodes.

######  Definition 4.5 (Extended Inductive/Extended
Skeletal/Inductive/Skeletal Inequalities).

(cf. [7, Definition 6]) For any order-type $\varepsilon$ and any strict
partial order $<_{\Omega}$ on $p_{1},\ldots p_{n}$ (the _dependence order_),
the signed generation tree $*\varphi$ $(*\in\\{-,+\\})$ of a formula
$\varphi(p_{1},\ldots p_{n})$ is _$(\Omega,\varepsilon)$ -extended
inductive/extended skeletal/inductive/skeletal_ if

  1. 1.

for any $i=1,\ldots,n$, every $\varepsilon$-critical branch with leaf $p_{i}$
is extended good/extended skeletal/good/skeletal;

  2. 2.

every SRR-node in an $\varepsilon$-critical branch is either
$\bigstar(\gamma,\beta)$ or $\bigstar(\beta,\gamma)$, where $\bigstar$ is a
binary connective, the $\varepsilon$-critical branch goes through $\beta$, and

    1. (a)

$\varepsilon^{\partial}(\gamma)\prec\ast\varphi$;

    2. (b)

$p_{k}<_{\Omega}p_{i}$ for every $p_{k}$ occurring in $\gamma$.

An inequality $\varphi\leq\psi$ is _$(\Omega,\varepsilon)$ -extended
inductive/extended skeletal/inductive/skeletal_ if the signed generation trees
$+\varphi$ and $-\psi$ are so. An inequality $\varphi\leq\psi$ is _extended
inductive/extended skeletal/inductive/skeletal_ if it is so for some
($\Omega$, $\varepsilon$). A formula $\varphi\to\psi$ (resp. a formula
$\theta$ which is not implicative) is _extended inductive/extended
skeletal/inductive/skeletal_ if $\varphi\leq\psi$ (resp. $\top\leq\theta$) is
so.

From the definition, it is easy to see that the classes of extended
inductive/skeletal formulas are respectively strictly larger than the classes
of inductive/skeletal formulas. For the examples distinguish the extended
classes and the non-extended classes, we give the following examples:

######  Example 4.6.

For the formula $\Box@_{\mathbf{i}}\Diamond\Box p\to\Diamond\Box p$, it is
$(\Omega,\varepsilon)$-extended inductive where $\varepsilon(p)=1$ and
$<_{\Omega}$ is empty. Here The critical branch is
$+\Box@_{\mathbf{i}}\Diamond\Box p$, where the $P_{3}$-part is
$+\Box,+@_{\mathbf{i}}$, the $P_{2}$-part is $+\Diamond$, the $P_{1}$-part is
$+\Box$. It is obvious that it is not an inductive formula.

######  Example 4.7.

For the McKinsey-like formula $\Box@_{\mathbf{i}}\Diamond p\to\Diamond\Box p$
, it is $(\Omega,\varepsilon)$-extended inductive where $\varepsilon(p)=1$ and
$<_{\Omega}$ is empty. Here The critical branch is
$+\Box@_{\mathbf{i}}\Diamond p$, where the $P_{3}$-part is
$+\Box,+@_{\mathbf{i}}$, the $P_{2}$-part is $+\Diamond$, the $P_{1}$-part is
empty. It is obvious that it is not a skeletal formula.

######  Remark 4.8.

The classification of outer nodes and inner nodes is based on how different
connectives behave in the algorithm. When the input formula is an extended
inductive formula, the algorithm first decompose the $P_{3}$-part, then the
outer part of the formula, and then the inner part of the formula, as we will
see in the algorithm.

The $P_{3}$-part is the special point of the definition of extended inductive
formulas. The basic idea is that when computing the minimal valuation, the
$@$-operator can “reset” the minimal valuation, so no matter what connectives
occur in the $P_{3}$-part, the last connective $@$ can make the minimal
valuation a nominal again, so the “outer-inner structure” is not necessary in
the $P_{3}$-part. From the example of the algorithm, this will be more clear.

##  5 The algorithm $\mathsf{ALBA}^{@}$ and
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$

In this section, we define the modified version of the correspondence
algorithms $\mathsf{ALBA}^{@}$ and $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$
for $\mathcal{L}(@)$, following the style of [8]. The major difference between
the two algorithms is that the latter algorithm does not treat the
$P_{1}$-part of extended good branches, therefore it could only treat extended
skeletal branches and extended skeletal formulas. We define
$\mathsf{ALBA}^{@}$, and $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ is the
algorithm without the Stage 2.3.

The input of $\mathsf{ALBA}^{@}$ is a formula $\varphi\to\psi$ (when the input
formula $\theta$ is not implicative, we first rewrite it into
$\top\to\theta$). $\mathsf{ALBA}^{@}$ transforms it into an inequality
$\varphi\leq\psi$. Then $\mathsf{ALBA}^{@}$ goes in three steps.

  1. 1.

First approximation: We apply the following _first approximation rule_ to
$\varphi\leq\psi$:

$\mathbf{i}_{0}\leq\varphi\ \&\ \psi\leq\neg\mathbf{i}_{1}\
\Rightarrow\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}\varphi\leq\psi$

We call the quasi-inequality $\mathbf{i}_{0}\leq\varphi\ \&\
\psi\leq\neg\mathbf{i}_{1}\ \Rightarrow\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$ a
_system_.

  2. 2.

The reduction stage: In this stage, for each system $\mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$ obtained during this stage, we apply the
following rules to prepare for eliminating all the proposition variables in
$\mathsf{S}$:

     * •

Stage 2.1: Decomposing the $P_{3}$-part

       1. (a)

Suppose that we have an inquality
$\mathbf{i}\leq\theta(@_{\mathbf{j}}\alpha)$, where
$+@_{\mathbf{j}}\alpha\prec+\theta$ is a farthest $@$ node in the
$P_{3}$-part, then we have the following decomposition rule:

$(\mathbf{i}\leq\theta(\bot)\ \&\ \mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\ (\mathbf{i}\leq\theta(\top)\ \&\
\mathbf{j}\leq\alpha\ \&\ \mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\mathbf{i}\leq\theta(@_{\mathbf{j}}\alpha)\
\&\ \mathsf{S}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$

       2. (b)

Suppose that we have an inquality
$\mathbf{i}\leq\theta(@_{\mathbf{j}}\alpha)$, where
$-@_{\mathbf{j}}\alpha\prec+\theta$ is a farthest $@$ node in the
$P_{3}$-part, then we have the following decomposition rule:

$(\mathbf{i}\leq\theta(\top)\ \&\ \mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\ (\mathbf{i}\leq\theta(\bot)\ \&\
\alpha\leq\neg\mathbf{j}\ \&\ \mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\mathbf{i}\leq\theta(@_{\mathbf{j}}\alpha)\
\&\ \mathsf{S}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$

       3. (c)

Suppose that we have an inquality
$\theta(@_{\mathbf{j}}\alpha)\leq\neg\mathbf{i}$, where
$-@_{\mathbf{j}}\alpha\prec-\theta$ is a farthest $@$ node in the
$P_{3}$-part, then we have the following decomposition rule:

$(\theta(\bot)\leq\neg\mathbf{i}\ \&\ \mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\ (\theta(\top)\leq\neg\mathbf{i}\ \&\
\mathbf{j}\leq\alpha\ \&\ \mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\theta(@_{\mathbf{j}}\alpha)\leq\neg\mathbf{i}\
\&\ \mathsf{S}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$

       4. (d)

Suppose that we have an inquality
$\theta(@_{\mathbf{j}}\alpha)\leq\neg\mathbf{i}$, where
$+@_{\mathbf{j}}\alpha\prec-\theta$ is a farthest $@$ node in the
$P_{3}$-part, then we have the following decomposition rule:

$(\theta(\top)\leq\neg\mathbf{i}\ \&\ \mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\ (\theta(\bot)\leq\neg\mathbf{i}\ \&\
\alpha\leq\neg\mathbf{j}\ \&\ \mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\theta(@_{\mathbf{j}}\alpha)\leq\neg\mathbf{i}\
\&\ \mathsf{S}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$

     * •

Stage 2.2: Decomposing the $P_{2}$-part

In the current stage, the following rules are applied to decompose the
$P_{2}$-part of critical branches. Except for two splitting rules for $\lor$
and $\land$, the other rules execute on a single inequality in the antecedent
part of the quasi-inequalities and rewrite it into one or two inequalities:

       1. (a)

Splitting rules:

$(\mathbf{i}\leq\beta\ \&\ \mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\ (\mathbf{i}\leq\gamma\ \&\ \mathsf{S}\
\Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\mathbf{i}\leq\beta\lor\gamma\ \&\
\mathsf{S}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$
$(\beta\leq\neg\mathbf{i}\ \&\ \mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\ (\gamma\leq\neg\mathbf{i}\ \&\
\mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\beta\land\gamma\leq\neg\mathbf{i}\ \&\
\mathsf{S}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$
$\mathbf{i}\leq\beta\ \ \
\mathbf{i}\leq\gamma\mathbf{i}\leq\beta\land\gamma\qquad\alpha\leq\neg\mathbf{i}\
\ \ \beta\leq\neg\mathbf{i}\alpha\lor\beta\leq\neg\mathbf{i}$

       2. (b)

Approximation rules:

$\mathbf{j}\leq\alpha\ \ \
\mathbf{i}\leq\Diamond\mathbf{j}\mathbf{i}\leq\Diamond\alpha\qquad\alpha\leq\neg\mathbf{j}\
\ \ \Box\neg\mathbf{j}\leq\neg\mathbf{i}\Box\alpha\leq\neg\mathbf{i}$
$\mathbf{j}\leq\alpha\mathbf{i}\leq@_{\mathbf{j}}\alpha\qquad\alpha\leq\neg\mathbf{j}@_{\mathbf{j}}\alpha\leq\neg\mathbf{i}$
$\mathbf{j}\leq\alpha\ \ \ \ \ \ \ \beta\leq\neg\mathbf{k}\ \ \ \ \ \ \
\mathbf{j}\rightarrow\neg\mathbf{k}\leq\neg\mathbf{i}\alpha\rightarrow\beta\leq\neg\mathbf{i}$

The nominals introduced by the approximation rules must not occur in the
system before applying the rule.

       3. (c)

Residuation rules:

$\alpha\leq\neg\mathbf{i}\mathbf{i}\leq\neg\alpha\qquad\mathbf{i}\leq\alpha\neg\alpha\leq\neg\mathbf{i}$

     * •

Stage 2.3: Decomposing the $P_{1}$-part

In the current stage, the following rules are applied to decompose the
$P_{1}$-part of the critical branch. Except for two residuation rules for $@$,
the other rules execute on a single inequality in the antecedent part of the
quasi-inequalities and rewrite it into one or two inequalities.

       1. (a)

Splitting rules:

$\alpha\leq\beta\ \ \
\alpha\leq\gamma\alpha\leq\beta\land\gamma\qquad\alpha\leq\gamma\ \ \
\beta\leq\gamma\alpha\lor\beta\leq\gamma$

       2. (b)

Residuation rules:

$\beta\leq\neg\alpha\alpha\leq\neg\beta\qquad\neg\beta\leq\alpha\neg\alpha\leq\beta\qquad\alpha\leq\blacksquare\beta\Diamond\alpha\leq\beta\qquad\vardiamond\alpha\leq\beta\alpha\leq\Box\beta$
$\alpha\leq\beta\to\gamma\alpha\land\beta\leq\gamma\qquad\alpha\land\neg\beta\leq\gamma\alpha\leq\beta\lor\gamma\qquad\alpha\land\beta\leq\gamma\alpha\leq\beta\to\gamma$
$\beta\leq\alpha\to\gamma\alpha\land\beta\leq\gamma\qquad\alpha\land\neg\gamma\leq\beta\alpha\leq\beta\lor\gamma\qquad\beta\leq\alpha\to\gamma\alpha\leq\beta\to\gamma$
$(\alpha\leq\bot\ \&\ \mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\ (\mathbf{j}\leq\beta\ \&\ \mathsf{S}\
\Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\alpha\leq@_{\mathbf{j}}\beta\ \&\
\mathsf{S}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$
$(\top\leq\beta\ \&\ \mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})\ (\alpha\leq\neg\mathbf{j}\ \&\
\mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})@_{\mathbf{j}}\alpha\leq\beta\ \&\
\mathsf{S}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$

     * •

Stage 2.4: The Ackermann stage

In the current stage, we compute the minimal/maximal valuations for
propositional variables and use the Ackermann rules to eliminate all the
propositional variables.

       1. (a)

The right-handed Ackermann rule:

$\mathop{\mbox{\Large\&}}_{j=1}^{m}\eta_{j}(\theta/p)\leq\iota_{j}(\theta/p)\
\Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}\mathop{\mbox{\Large\&}}_{i=1}^{n}\theta_{i}\leq
p\ \&\ \mathop{\mbox{\Large\&}}_{j=1}^{m}\eta_{j}\leq\iota_{j}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$

where:

         1. i.

$p$ does not occur in $\theta_{1},\ldots,\theta_{n}$;

         2. ii.

Each $\eta_{i}$ is positive, and each $\iota_{i}$ negative in $p$, for $1\leq
j\leq m$;

         3. iii.

$\theta:=\theta_{1}\lor\ldots\lor\theta_{n}$. When $n=0$, we define
$\theta:=\bot$.

       2. (b)

The left-handed Ackermann rule:

$\mathop{\mbox{\Large\&}}_{j=1}^{m}\eta_{j}(\theta/p)\leq\iota_{j}(\theta/p)\
\Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}\mathop{\mbox{\Large\&}}_{i=1}^{n}p\leq\theta_{i}\
\&\ \mathop{\mbox{\Large\&}}_{j=1}^{m}\eta_{j}\leq\iota_{j}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$

where:

         1. i.

$p$ does not occur in $\theta_{1},\ldots,\theta_{n}$;

         2. ii.

Each $\eta_{i}$ is negative, and each $\iota_{i}$ positive in $p$, for $1\leq
j\leq m$;

         3. iii.

$\theta:=\theta_{1}\land\ldots\land\theta_{n}$. When $n=0$, we define
$\theta:=\top$.

  3. 3.

Output: If in the previous stage, for some system, the algorithm gets stuck,
i.e. some propositional variables cannot be eliminated by the reduction rules
in Stage 2, then the algorithm stops and output “failure”. Otherwise, the
system after the first-approximation has been reduced to a set of pure quasi-
inequalties. Then the output is this set of pure quasi-inequalities and the
conjunction of universally quantified (over the individual symbols
corresponding to nominals) first-order sentences of their standard
translations.

######  Remark 5.1.

  * •

There are no preprocessing rules in Stage 1 in $\mathsf{ALBA}^{@}$ and
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ compared with
$\mathsf{hybrid}$-$\mathsf{ALBA}$ in [8], i.e. there are no distribution
rules, splitting rules, and monotone/antitone variable elimination rules in
Stage 1. This is because we incorporate these rules in the splitting rules for
$\land,\lor$ in Stage 2.2 and the Ackermann rules (where we allow empty
minimal valuations) in Stage 2.4.

  * •

A special feature of $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ compared with
$\mathsf{ALBA}^{@}$ is that there is no expanded hybrid language needed in
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$, and there is no tense operators
needed. Another feature of $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ is that
during Stage 2, for each inequality involved, they are of the form
$\mathbf{i}\leq\gamma$ or $\gamma\leq\neg\mathbf{i}$, which means that they
can be equivalently translated into hybrid formulas of the form
$@_{\mathbf{i}}\gamma$ or $\neg@_{\mathbf{i}}\gamma$, as we can see in Section
7 and 8.

######  Example 5.2.

Consider the formula $\Box\Diamond@_{\mathbf{i}}\Diamond p\to\Diamond\Box p$
as given in Example 4.7. We first rewrite it into

$\mathbf{i}_{0}\leq\Box\Diamond@_{\mathbf{i}}\Diamond p\ \&\ \Diamond\Box
p\leq\neg\mathbf{i}_{1}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}.$

Now we know that for $\Diamond\Box p\leq\neg\mathbf{i}_{1}$, we cannot use it
to compute the minimal valuation, as in the McKinsey formula $\Box\Diamond
p\to\Diamond\Box p$ in modal logic.

For the $\mathbf{i}_{0}\leq\Box\Diamond@_{\mathbf{i}}\Diamond p$ part, in
standard ways to compute the minimal valuation, we will get
$\vardiamond\mathbf{i}_{0}\leq\Diamond@_{\mathbf{i}}\Diamond p$ and we get
stuck.

However, if we use the decomposition rules for $P_{3}$-part, then we can “jump
over” the outer $\Box\Diamond$ part, and get two systems

$\mathbf{i}_{0}\leq\Box\Diamond\top\ \&\ \mathbf{i}\leq\Diamond p\ \&\
\Diamond\Box p\leq\neg\mathbf{i}_{1}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$

and

$\mathbf{i}_{0}\leq\Box\Diamond\bot\ \Diamond\Box p\leq\neg\mathbf{i}_{1}\
\Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}.$

For the first system, we have the following execution:

$\mathbf{i}_{0}\leq\Box\Diamond\top\ \&\ \mathbf{i}\leq\Diamond p\ \&\
\Diamond\Box p\leq\neg\mathbf{i}_{1}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$
$\mathbf{i}_{0}\leq\Box\Diamond\top\ \&\ \mathbf{i}\leq\Diamond\mathbf{j}\ \&\
\mathbf{j}\leq p\ \&\ \Diamond\Box p\leq\neg\mathbf{i}_{1}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$
$\mathbf{i}_{0}\leq\Box\Diamond\top\ \&\ \mathbf{i}\leq\Diamond\mathbf{j}\ \&\
\Diamond\Box\mathbf{j}\leq\neg\mathbf{i}_{1}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$.

For the second system, we have the following execution:

$\mathbf{i}_{0}\leq\Box\Diamond\bot\ \Diamond\Box p\leq\neg\mathbf{i}_{1}\
\Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$
$\mathbf{i}_{0}\leq\Box\Diamond\bot\ \Diamond\Box\bot\leq\neg\mathbf{i}_{1}\
\Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$.

We skip the standard translation step.

As we can see, the execution above is also an execution of
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$.

##  6 Soundness

In this section, we prove the soundness of the algorithms in the style of [6,
20]. Since most of the rules in the algorithm is the same as in
$\mathsf{hybrid}$-$\mathsf{ALBA}$ in [8], therefore by dualizing their
soundness proof, we get the soundness of the rules already in [8]. Therefore,
we only treat the new rules in $\mathsf{ALBA}^{@}$.

######  Theorem 6.1 (Soundness of the algorithm).

If $\mathsf{ALBA}^{@}$ runs successfully on $\varphi\to\psi$ and outputs a
first-order formula $\mathsf{FO}(\varphi\leq\psi)$, then for any frame
$\mathbb{F}=(W,R)$,

$\mathbb{F}\Vdash\varphi\to\psi\mbox{ iff
}\mathbb{F}\models\mathsf{FO}(\varphi\to\psi).$

###### Proof.

The proof is similar to [6, Theorem 8.1]. Let $\varphi\to\psi$ denote the
input formula, $\mathbf{i}_{0}\leq\varphi\ \&\ \psi\leq\neg\mathbf{i}_{1}\
\Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$ denote the system after the
first-approximation rule, let $\textsf{Pure}(\varphi\to\psi)$ denote the set
of pure quasi-inequalities after Stage 2, let $\mathsf{FO(\varphi\to\psi)}$
denote resulting first-order formula in Stage 3, then it suffices to show the
equivalence from (1) to (4) given below:

$\displaystyle\mathbb{F}\Vdash\varphi\to\psi$ (1)
$\displaystyle\mathbb{F}\Vdash\mathbf{i}_{0}\leq\varphi\ \&\
\psi\leq\neg\mathbf{i}_{1}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$
(2) $\displaystyle\mathbb{F}\Vdash\textsf{Pure}(\varphi\to\psi)$ (3)
$\displaystyle\mathbb{F}\vDash\mathsf{FO(\varphi\to\psi)}$ (4)

The equivalence between (1) and (2) follows from the soundness of the first-
approximation rule;

The equivalence between (2) and (3) follows from the soundness of the rules in
Stage 2;

The equivalence between (3) and (4) follows from Proposition 3.4. ∎

In the remainder of the section, we prove the soundness of the rules in Stage
2.1, the splitting rules creating two systems in Stage 2.2, the approximation
rule for $\to$ in Stage 2.2 and the residuation rules for $@$ in Stage 2.3.

For the soundness of a rule we mean that for any frame $\mathbb{F}$, the
system before the application of a rule is valid in $\mathbb{F}$ iff the
systems after the application of the rule is valid in $\mathbb{F}$.

######  Proposition 6.2.

The rules in Stage 2.1 are sound.

###### Proof.

For the soundness of the rules in Stage 2.1, we only prove for (a), the other
three rules are similar.

By the validity of the equivalence

$(\alpha_{1}\land\beta\to\gamma)\land(\alpha_{2}\land\beta\to\gamma)\leftrightarrow((\alpha_{1}\lor\alpha_{2})\land\beta\to\gamma),$

it suffices to show that for any model $(\mathbb{F},V)$,

$\mathbb{F},V\Vdash\mathbf{i}\leq\theta(@_{\mathbf{j}}\alpha)\mbox{ iff
}(\mathbb{F},V\Vdash\mathbf{i}\leq\theta(\bot))\mbox{ or
}(\mathbb{F},V\Vdash\mathbf{i}\leq\theta(\top)\mbox{ and
}\mathbb{F},V\Vdash\mathbf{j}\leq\alpha).$

Since $\mathbb{F},V\Vdash\mathbf{i}\leq\gamma$ iff
$\mathbb{F},V,V(\mathbf{i})\Vdash\gamma$, it suffices to show that

$\mathbb{F},V,V(\mathbf{i})\Vdash\theta(@_{\mathbf{j}}\alpha)\mbox{ iff
}(\mathbb{F},V,V(\mathbf{i})\Vdash\theta(\bot))\mbox{ or
}(\mathbb{F},V,V(\mathbf{i})\Vdash\theta(\top)\mbox{ and
}\mathbb{F},V,V(\mathbf{j})\Vdash\alpha).$

$\Rightarrow:$ Assmue that
$\mathbb{F},V,V(\mathbf{i})\Vdash\theta(@_{\mathbf{j}}\alpha)$. Since
$@_{\mathbf{j}}\alpha$ is either globally true or globally false, we have that
there are two cases:
$\mathbb{F},V\Vdash@_{\mathbf{j}}\alpha\leftrightarrow\bot$ or
$\mathbb{F},V\Vdash@_{\mathbf{j}}\alpha\leftrightarrow\top$. In the first case
we have $\mathbb{F},V,V(\mathbf{i})\Vdash\theta(\bot)$, in the second case we
have $\mathbb{F},V,V(\mathbf{i})\Vdash\theta(\top)$ and
$\mathbb{F},V\Vdash@_{\mathbf{j}}\alpha$, i.e.
$\mathbb{F},V,V(\mathbf{j})\Vdash\alpha$.

$\Leftarrow:$ Assume that

$(\mathbb{F},V,V(\mathbf{i})\Vdash\theta(\bot))\mbox{ or
}(\mathbb{F},V,V(\mathbf{i})\Vdash\theta(\top)\mbox{ and
}\mathbb{F},V,V(\mathbf{j})\Vdash\alpha).$

If $\mathbb{F},V,V(\mathbf{i})\Vdash\theta(\bot)$ then by
$+@_{\mathbf{j}}(\alpha)\prec+\theta$ we have that $\theta$ is monotone in the
position of $@_{\mathbf{j}}\alpha$, so
$\mathbb{F},V,V(\mathbf{i})\Vdash\theta(@_{\mathbf{j}}\alpha)$.

If $\mathbb{F},V,V(\mathbf{i})\Vdash\theta(\top)\mbox{ and
}\mathbb{F},V,V(\mathbf{j})\Vdash\alpha$, then
$\mathbb{F},V\Vdash@_{\mathbf{j}}\alpha$, therefore
$\mathbb{F},V\Vdash@_{\mathbf{j}}\alpha\leftrightarrow\top$, so
$\mathbb{F},V,V(\mathbf{i})\Vdash\theta(@_{\mathbf{j}}\alpha)$. ∎

######  Proposition 6.3.

The splitting rules creating two systems in Stage 2.2 are sound.

###### Proof.

We only prove it for the splitting rule for $\lor$, the splitting rule for
$\land$ is similar. By the validity of the equivalence

$(\alpha_{1}\land\beta\to\gamma)\land(\alpha_{2}\land\beta\to\gamma)\leftrightarrow((\alpha_{1}\lor\alpha_{2})\land\beta\to\gamma),$

it suffices to show that for any frame $\mathbb{F}$ and any valuation $V$ on
$\mathbb{F}$,

$\mathbb{F},V\Vdash\mathbf{i}\leq\beta\lor\gamma\mbox{ iff
}(\mathbb{F},V\Vdash\mathbf{i}\leq\beta\mbox{ or
}\mathbb{F},V\Vdash\mathbf{i}\leq\gamma),$

which is equivalent to

$\mathbb{F},V,V(\mathbf{i})\Vdash\beta\lor\gamma\mbox{ iff
}(\mathbb{F},V,V(\mathbf{i})\Vdash\beta\mbox{ or
}\mathbb{F},V,V(\mathbf{i})\Vdash\gamma),$

which follows from the semantics. ∎

For the soundness of the approximation rule for $\to$ in Stage 2.2, see [21].

######  Proposition 6.4.

The residuation rules for $@$ in Stage 2.3 are sound.

###### Proof.

We only prove it for the residuation rule for $@$ where $@_{\mathbf{j}}\alpha$
is on the right-hand side, the other rule is similar.

By the validity of the equivalence

$(\alpha_{1}\land\beta\to\gamma)\land(\alpha_{2}\land\beta\to\gamma)\leftrightarrow((\alpha_{1}\lor\alpha_{2})\land\beta\to\gamma),$

it suffices to show that for any frame $\mathbb{F}$ and any valuation $V$ on
$\mathbb{F}$,

$\mathbb{F},V\Vdash\alpha\leq@_{\mathbf{j}}\beta\mbox{ iff
}(\mathbb{F},V\Vdash\alpha\leq\bot\mbox{ or
}\mathbb{F},V\Vdash\mathbf{j}\leq\beta),$

which follows from the soundness of the ($@$-R-Res) rule in [8]. ∎

Since the algorithm $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ is a restricted
version of $\mathsf{ALBA}^{@}$, its soundness follows from the soundness of
$\mathsf{ALBA}^{@}$.

##  7 Success of $\mathsf{ALBA}^{@}$ and
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$

In this section, we show that $\mathsf{ALBA}^{@}$ succeeds on all extended
inductive formulas and that $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ succeeds
on all extended skeletal formulas. The proof is similar to [21, Section 7],
but we will stress on the special shape of the inequalities involved in the
execution of $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$.

######  Theorem 7.1.

$\mathsf{ALBA}^{@}$ succeeds on all extended inductive formulas and
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ succeeds on all extended skeletal
formulas.

######  Lemma 7.2.

Given a system $\mathbf{i}_{0}\leq\varphi\ \&\ \psi\leq\neg\mathbf{i}_{1}\
\Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$ obtained from Stage 1 where
$+\varphi$ and $-\psi$ are $(\Omega,\varepsilon)$-extended inductive, by
applying the rules in Stage 2.1 exhaustively, for each quasi-inequality
$\mathsf{S}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$ obtained, the
inequalities in $\mathsf{S}$ are in one of the following forms:

  * •

$\mathbf{k}\leq\beta$, where $+\beta$ is $(\Omega,\varepsilon)$-inductive;

  * •

$\beta\leq\neg\mathbf{k}$, where $-\beta$ is $(\Omega,\varepsilon)$-inductive.

###### Proof.

Suppose we have an inequality $\mathbf{i}\leq\theta(@_{\mathbf{j}}\alpha)$
where $+@_{\mathbf{j}}\alpha\prec+\theta$, $+\theta$ is
$(\Omega,\varepsilon)$-extended inductive and $@_{\mathbf{j}}$ is the farthest
node in the $P_{3}$-part of a $\varepsilon$-critical branch. Then by applying
the decomposition rule in Stage 2.1, we get inequalities of the form
$\mathbf{i}\leq\theta(\top)$, $\mathbf{i}\leq\theta(\bot)$ and
$\mathbf{j}\leq\alpha$. For $\mathbf{i}\leq\theta(\top)$ and
$\mathbf{i}\leq\theta(\bot)$, $+\theta(\top)$ and $+\theta(\bot)$ are still
$(\Omega,\varepsilon)$-extended inductive, but have one less
$\varepsilon$-critical branch with $P_{3}$-part, and in
$\mathbf{j}\leq\alpha$, $+\alpha$ is $(\Omega,\varepsilon)$-inductive, since
it has no $P_{3}$-part in $\varepsilon$-critical branches.

For the other three cases where a decomposition rule can be applied, we get
inequalities with either the $\theta(\top)$ and $\theta(\bot)$ part having one
less $\varepsilon$-critical branch with $P_{3}$-part, or the $\alpha$ part has
no $P_{3}$-part in $\varepsilon$-critical branches, and the two $\theta$
formulas with appropriate signs are still $(\Omega,\varepsilon)$-extended
inductive and the $\alpha$ formula is $(\Omega,\varepsilon)$-inductive.

By repeating the rules above, we get inequalities with no $P_{3}$-part on any
$\varepsilon$-critical branch, therefore all the $\varepsilon$-critical
branches in all formulas involved are with at most $P_{1}$ and $P_{2}$-part,
therefore with appropriate signs, they are $(\Omega,\varepsilon)$-inductive. ∎

######  Definition 7.3 ($(\Omega,\varepsilon)$-inner inductive signed
generation tree).

Given an order-type $\varepsilon$ and a dependence order $<_{\Omega}$,
$*\in\\{-,+\\}$, the signed generation tree $*\varphi$ of the formula
$\varphi(p_{1},\ldots,p_{n})$ is _$(\Omega,\varepsilon)$ -inner inductive_ if
it is $(\Omega,\varepsilon)$-extended inductive and the $P_{3},P_{2}$-part on
an $\varepsilon$-critical branch are always empty, i.e. its
$\varepsilon$-critical branches have $P_{1}$-nodes only.

######  Lemma 7.4.

Given inequalities $\mathbf{k}\leq\beta$ and $\beta\leq\neg\mathbf{k}$
obtained from Stage 2.1 where $+\varphi_{i}$ and $-\psi_{i}$ are
$(\Omega,\varepsilon)$-inductive, by applying the rules in Stage 2.2
exhaustively, for each quasi-inequality $\mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$ obtained, the inequalities that we get
in $\mathsf{S}$ are in one of the following forms:

  1. 1.

pure inequalities without propositional variables;

  2. 2.

inequalities of the form $\mathbf{i}\leq\alpha$ where $+\alpha$ is
$(\Omega,\varepsilon)$-inner inductive;

  3. 3.

inequalities of the form $\beta\leq\neg\mathbf{i}$ where $-\beta$ is
$(\Omega,\varepsilon)$-inner inductive.

###### Proof.

Indeed, the rules in Stage 2.2 deal with $P_{2}$ nodes in the signed
generation trees $+\beta$ and $-\beta$. For each rule, without loss of
generality assume we start with an inequality of the form
$\mathbf{i}\leq\alpha$, then by applying the rules in Stage 2.2, the new
inequalities we get are either a pure inequality without propositional
variables, or an inequality where the left-hand side (resp. right-hand side)
is $\mathbf{i}$ (resp. $\neg\mathbf{i}$), and the other side is a formula
$\alpha^{\prime}$ which is a subformula of $\alpha$, such that
$\alpha^{\prime}$ has one root connective less than $\alpha$. Indeed, if
$\alpha^{\prime}$ is on the left-hand side (resp. right-hand side) then
$-\alpha^{\prime}$ ($+\alpha^{\prime}$) is $(\Omega,\varepsilon)$-inductive.

By applying the rules in Stage 2.2 exhaustively, we can eliminate all the
$P_{2}$ connectives in the $\varepsilon$-critical branches, so for non-pure
inequalities, they become of form 2 or form 3. ∎

Now comes the difference between $\mathsf{ALBA}^{@}$ and
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$. We first deal with
$\mathsf{ALBA}^{@}$.

######  Lemma 7.5.

Assume we have an inequality $\mathbf{i}\leq\alpha$ or
$\beta\leq\neg\mathbf{i}$ where $+\alpha$ and $-\beta$ are
$(\Omega,\varepsilon)$-inner inductive, by applying the rules in Stage 2.3,
for each quasi-inequality $\mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$ obtained, the inequalities that we get
in $\mathsf{S}$ are in one of the following forms:

  1. 1.

$\alpha\leq p$, where $\varepsilon(p)=1$, $-\alpha$ does not contain $p$ and
is $\varepsilon^{\partial}$-uniform;

  2. 2.

$p\leq\beta$, where $\varepsilon(p)=\partial$, $+\beta$ does not contain $p$
and is $\varepsilon^{\partial}$-uniform;

  3. 3.

$\gamma\leq\delta$, where $-\gamma,+\delta$ are
$\varepsilon^{\partial}$-uniform.

###### Proof.

For each of the inequality at the beginning of this stage, it is of the form
$\mathbf{i}\leq\alpha$ or $\beta\leq\neg\mathbf{i}$, where

  * •

$+\alpha$ and $-\beta$ are $(\Omega,\varepsilon)$-inner inductive;

  * •

$-\mathbf{i}$ and $+\neg\mathbf{i}$ are $\varepsilon^{\partial}$-uniform;

  * •

for each $\varepsilon$-critical occurrence $p$ in $+\alpha$ (resp. $-\beta$),
$\mathbf{i}$ (resp. $\neg\mathbf{i}$) does not contain $p$.

By applying the splitting rules and the residuation rules in Stage 2.3 to an
inequality $\gamma_{1}\leq\theta_{1}$ or $\theta_{2}\leq\gamma_{2}$ where

  * •

for each $\varepsilon$-critical occurrence $p$ in $+\theta_{1}$ (resp.
$-\theta_{2}$), $\gamma_{1}$ (resp. $\gamma_{2}$) does not contain $p$;

  * •

$-\gamma_{1}$ (resp. $+\gamma_{2}$) is $\varepsilon^{\partial}$-uniform;

  * •

$+\theta_{1}$ (resp. $-\theta_{2}$) is $(\Omega,\varepsilon)$-inner inductive;

it is easy to check that the $\varepsilon^{\partial}$-uniform part will remain
$\varepsilon^{\partial}$-uniform and does not contain the relevant variables,
and the other side is a formula $\theta^{\prime}_{i}$ which is a subformula of
$\theta_{i}$, such that $\theta^{\prime}_{i}$ with appropriate sign is still
$(\Omega,\varepsilon)$-inner inductive but has one root connective less than
$\theta_{i}$.

By applying these rules exhaustively, the $\varepsilon^{\partial}$-uniform
side will remain $\varepsilon^{\partial}$-uniform and does not contain the
relevant variables, the other side is either a propositional variable $p$
which, with appropriate sign, is $(\Omega,\varepsilon)$-inner inductive, or is
a $\varepsilon^{\partial}$-uniform formula (with appropriate sign, which is
also $(\Omega,\varepsilon)$-inner inductive since it contains no
$\varepsilon$-critical branch). Therefore, the inequality is of one of the
three forms indicated. ∎

######  Lemma 7.6.

Assume we have inequalities of the form as described in Lemma 7.5, the
Ackermann rules are applicable and therefore all propositional variables can
be eliminated.

###### Proof.

Immediate observation from the requirements of the Ackermann rules. ∎

###### Proof of Theorem 7.1 for $\mathsf{ALBA}^{@}$.

Assume we have an $(\Omega,\varepsilon)$-extended inductive formula
$\varphi\to\psi$ as input. By Stage 1, we get the quasi-inequality
$\mathbf{i}_{0}\leq\varphi\ \&\ \psi\leq\neg\mathbf{i}_{1}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$. By Lemma 7.2, 7.4, 7.5, we get quasi-
inequalities as described there. Finally by Lemma 7.6, the quasi-inequalities
are in the right shape to apply the Ackermann rules, and thus we can eliminate
all the propositional variables and the algorithm succeeds on the input. ∎

For $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$, in Lemma 7.4, the critical
branches in $(\Omega,\varepsilon)$-inner inductive formulas are without
$P_{1}$-part, so they are either $\varepsilon^{\partial}$-uniform, or they are
already propositional variables, therefore the result for Lemma 7.5 is
automatically satisfied, so by Lemma 7.6,
$\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$ succeeds on all extended skeletal
formulas.

##  8 Completeness results

In this section, we will prove that given any extended skeletal formula
$\varphi\to\psi$, the logic $\mathbf{K}_{\mathcal{H}(@)}+(\varphi\to\psi)$ is
sound and strongly complete with respect to the class of frames defined by
$\varphi\to\psi$. The strategy is the same as [22] and the presentation is
similar.

Our proof strategy is as follows:

  * •

We translate of each system in $\textsf{Pure}(\varphi\to\psi)$ into
$\mathcal{L}(@)$-formulas, which results in a set $\Pi$ of
$\mathcal{L}(@)$-formulas, and we prove that $\varphi\to\psi$ and $\Pi$ define
the same class of frames.

  * •

We then prove that each $\pi\in\Pi$ is provable in
$\mathbf{K}_{\mathcal{H}(@)}+(\varphi\to\psi)$. Therefore, by the Theorem 2.4,
we get the soundness and strong completeness of
$\mathbf{K}_{\mathcal{H}(@)}+(\varphi\to\psi)$.

###  8.1 The translation

As one can easily observe, in $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$, in
the systems obtained in Stage 2, for each inequality in them, either the left-
hand side is $\mathbf{i}$, or the right-hand side is $\neg\mathbf{i}$. Indeed,
the inequality $\mathbf{i}\leq\gamma$ is equivalent to the
$\mathcal{L}(@)$-formula $@_{\mathbf{i}}\gamma$ , and the inequality
$\gamma\leq\neg\mathbf{i}$ is equivalent to the $\mathcal{L}(@)$-formula
$\neg@_{\mathbf{i}}\gamma$. Therefore, the systems obtained in Stage 2 are
equivalent to $\mathcal{L}(@)$-formulas.

######  Definition 8.1 (Translation into $\mathcal{L}(@)$-formulas).

We define the translation of the inequalities of the form
$\mathbf{i}\leq\gamma$, $\gamma\leq\neg\mathbf{i}$ into
$\mathcal{L}(@)$-formulas as follows:

  * •

$\mathsf{Tr}(\mathbf{i}\leq\gamma):=@_{\mathbf{i}}\gamma$;

  * •

$\mathsf{Tr}(\gamma\leq\neg\mathbf{i}):=\neg@_{\mathbf{i}}\gamma$.

When an inequality is of both of the forms above, we can take any of the two
since they are equivalent.

Given a quasi-inequality $\mathsf{Quasi}$ of the form $\mathsf{Ineq}_{1}\ \&\
\ldots\ \&\ \mathsf{Ineq}_{n}\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j}$
where each of $\mathsf{Ineq}_{1},\ldots,\mathsf{Ineq}_{n}$ is of the form
$\mathbf{i}\leq\gamma$ or $\gamma\leq\neg\mathbf{i}$, define

$\mathsf{Tr}(\mathsf{Quasi}):=\mathsf{Tr}(\mathsf{Ineq}_{1})\land\ldots\land\mathsf{Tr}(\mathsf{Ineq}_{n})\to\neg@_{\mathbf{i}}\mathbf{j}$

Given a set $\mathsf{QuasiSet}$ of quasi-inequalities of the form above,
define

$\mathsf{Tr}(\mathsf{QuasiSet}):=\bigwedge_{\mathsf{Quasi}\in\mathsf{QuasiSet}}\mathsf{Tr}(\mathsf{Quasi}).$

######  Proposition 8.2.

For each inequality $\mathsf{Ineq}$ of the form $\mathbf{i}\leq\gamma$ or
$\gamma\leq\neg\mathbf{i}$, each quasi-inequality $\mathsf{Quasi}$ of the form
described above, each set $\mathsf{QuasiSet}$ of quasi-inequalities of the
form above, we have that for any model $\mathbb{M}$,

$\mathbb{M}\Vdash\mathsf{Ineq}\mbox{ iff
}\mathbb{M}\Vdash\mathsf{Tr}(\mathsf{Ineq})$
$\mathbb{M}\Vdash\mathsf{Quasi}\mbox{ iff
}\mathbb{M}\Vdash\mathsf{Tr}(\mathsf{Quasi})$
$\mathbb{M}\Vdash\mathsf{QuasiSet}\mbox{ iff
}\mathbb{M}\Vdash\mathsf{Tr}(\mathsf{QuasiSet}).$

###  8.2 Provability of the translations

######  Lemma 8.3 (Lemma 7.5 in [22]).

For the quasi-inequality $\mathsf{Quasi}:=\mathbf{i}_{0}\leq\varphi\ \&\
\psi\leq\neg\mathbf{i}_{1}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$, then we have that
$\vdash_{\varphi\to\psi}\mathsf{Tr}(\mathsf{Quasi})$.

Now we will prove that for each system $\mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$ obtained during Stage 2,
$\mathsf{Tr}(\mathsf{S}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1})$
is provable.

######  Lemma 8.4.

Given the quasi-inequality $\mathbf{i}_{0}\leq\varphi\ \&\
\psi\leq\neg\mathbf{i}_{1}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$
obtained in Stage 1, for each system $\mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$ obtained during Stage 2,
$\vdash_{\varphi\to\psi}\mathsf{Tr}(\mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})$.

###### Proof.

First of all, since in each inequality in the system, either the left-hand
side is a nominal, or the right-hand side is the negation of a nominal,
$\mathsf{S}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$ can be
translated.

We prove by induction on the algorithm steps in Stage 2 that for each system
$\mathsf{S}\ \Rightarrow\ \mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$ obtained
during Stage 2, $\vdash_{\varphi\to\psi}\mathsf{Tr}(\mathsf{S}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})$ is provable.

  * •

For the basic step, obviously
$\vdash_{\varphi\to\psi}\mathsf{Tr}(\mathbf{i}_{0}\leq\varphi\ \&\
\psi\leq\neg\mathbf{i}_{1}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1})$.

  * •

For Stage 2.1, for the rule (a), it suffices to show that from
$\vdash_{\varphi\to\psi}@_{\mathbf{i}}\theta(@_{\mathbf{j}}\alpha)\land\gamma\to\delta$
one can get
$\vdash_{\varphi\to\psi}@_{\mathbf{i}}\theta(\bot)\land\gamma\to\delta$ and
$\vdash_{\varphi\to\psi}@_{\mathbf{i}}\theta(\top)\land@_{\mathbf{j}}\alpha\land\gamma\to\delta$,
which follows from
$\vdash_{\Sigma}@_{\mathbf{i}}\theta(@_{\mathbf{j}}\alpha)\leftrightarrow@_{\mathbf{i}}\theta(\bot)\lor(@_{\mathbf{i}}\theta(\top)\land@_{\mathbf{j}}\alpha)$
on page 2.3.

For (b),(c),(d), the proofs are similar.

  * •

For the splitting rules involving two systems, we show it for the rule
involving $\lor$. It suffices to show that from
$\vdash_{\varphi\to\psi}@_{\mathbf{i}}(\beta\lor\gamma)\land\theta\to\delta$
one can get $\vdash_{\varphi\to\psi}@_{\mathbf{i}}\beta\land\theta\to\delta$
and $\vdash_{\varphi\to\psi}@_{\mathbf{i}}\gamma\land\theta\to\delta$, which
follows from
$\vdash_{\varphi\to\psi}@_{\mathbf{i}}(\beta\lor\gamma)\leftrightarrow(@_{\mathbf{i}}\beta\lor@_{\mathbf{i}}\gamma)$.

For the rule involving $\land$, the proof is similar.

  * •

For the splitting rules within a single system, the approximation rules for
$\Diamond,\Box,@,\to$, the residuation rules for $\neg$, the proof is similar
to [22, Lemma 7.6].

  * •

In $\mathsf{ALBA}^{@}_{\mathsf{Restricted}}$, there is no Stage 2.3, so this
part can be omitted.

  * •

For the Ackermann rules, the proof is similar to [22, Lemma 7.6].

∎

######  Corollary 8.5.

Given an extended skeletal formula $\varphi\to\psi$, for each quasi-inequality
$\mathsf{Quasi}$ in $\textsf{Pure}(\varphi\to\psi)$, we have that
$\vdash_{\varphi\to\psi}\mathsf{Tr}(\mathsf{Quasi})$, therefore
$\vdash_{\varphi\to\psi}\mathsf{Tr}(\textsf{Pure}(\varphi\to\psi))$.

###  8.3 Main Proof

######  Theorem 8.6 (Similar to Theorem 7.8 in [22]).

For any extended skeletal formula $\varphi\to\psi$,
$\mathbf{K}_{\mathcal{H}(@)}+(\varphi\to\psi)$ is sound and strongly complete
with respect to the class of frames $\mathcal{F}$ defined by $\varphi\to\psi$.

###### Proof.

The proof is the same as [22, Theorem 7.8]. We prove that for any set $\Gamma$
of $\mathcal{L}(@)$-formulas and any $\mathcal{L}(@)$-formula $\gamma$, the
following three conditions are equivalent:

  1. 1.

$\Gamma\vdash_{\varphi\to\psi}\gamma$;

  2. 2.

$\Gamma\Vdash_{\mathcal{F}}\gamma$;

  3. 3.

$\Gamma\vdash_{\mathsf{Tr}(\mathsf{Pure}(\varphi\to\psi))}\gamma.$

  * (1$\Rightarrow$2):

The soundness proof is easy.

  * (2$\Rightarrow$3):

From

| $\mathbb{F}\Vdash\varphi\to\psi$ |
---|---|---
iff | $\mathbb{F}\Vdash\mathsf{Pure}(\varphi\to\psi)$ | (Theorem 6.1)
iff |  $\mathbb{F}\Vdash\mathsf{Tr}(\mathsf{Pure}(\varphi\to\psi))$, | (corollary of Proposition 8.2)

$\mathcal{F}$ is also defined by $\mathsf{Tr}(\mathsf{Pure}(\varphi\to\psi))$.
By Theorem 2.4, we have the completeness of
$\mathbf{K}_{\mathcal{H}(@)}+\mathsf{Tr}(\mathsf{Pure}(\varphi\to\psi))$ with
respect to $\mathcal{F}$.

  * (3$\Rightarrow$1):

By Corollary 8.5,
$\vdash_{\varphi\to\psi}\mathsf{Tr}(\mathsf{Pure}(\varphi\to\psi))$, therefore
all theorems of
$\mathbf{K}_{\mathcal{H}(@)}+\mathsf{Tr}(\mathsf{Pure}(\varphi\to\psi))$ are
also theorems of $\mathbf{K}_{\mathcal{H}(@)}+(\varphi\to\psi)$.

∎

The following corollary follows from an easy adaptation of the previous
results to a set $\Sigma$ of extended skeletal formulas:

######  Corollary 8.7.

For any set $\Sigma$ of extended skeletal formulas,
$\mathbf{K}_{\mathcal{H}(@)}+\Sigma$ is sound and strongly complete with
respect to the class of frames $\mathcal{F}$ defined by $\Sigma$.

#### Acknowledgement

The research of the author is supported by the Taishan Young Scholars Program
of the Government of Shandong Province, China (No.tsqn201909151).

## References

  * [1] N. Bezhanishvili, B. ten Cate, M. Marx, and P. Viana.  Sahlqvist theory and transfer results for hybrid logics.  In R. Schmidt, I. Pratt-Hartmann, M. Reynolds, and H. Wansing, editors, Preliminary proceedings of Advances in Modal Logic 2004, 2004.
  * [2] P. Blackburn and B. ten Cate.  Pure extensions, proof rules, and hybrid axiomatics.  Studia Logica, 84(2):277–322, 2006.
  * [3] P. Blackburn, J. van Benthem, and F. Wolter.  Handbook of modal logic, volume 3.  Elsevier, 2006.
  * [4] W. Conradie.  Completeness and correspondence in hybrid logic via an extension of SQEMA.  Electronic Notes in Theoretical Computer Science, 231:175 – 190, 2009.  Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007).
  * [5] W. Conradie, V. Goranko, and D. Vakarelov.  Algorithmic correspondence and completeness in modal logic. II. Polyadic and hybrid extensions of the algorithm SQEMA.  Journal of Logic and Computation, 16(5):579–612, 09 2006.
  * [6] W. Conradie and A. Palmigiano.  Algorithmic correspondence and canonicity for distributive modal logic.  Annals of Pure and Applied Logic, 163(3):338 – 376, 2012.
  * [7] W. Conradie, A. Palmigiano, and Z. Zhao.  Sahlqvist via translation.  Logical Methods in Computer Science, Volume 15, Issue 1, Feb. 2019.
  * [8] W. Conradie and C. Robinson.  On Sahlqvist theory for hybrid logic.  Journal of Logic and Computation, 27(3):867–900, 2017.
  * [9] G. Gargov and V. Goranko.  Modal logic with names.  Journal of Philosophical Logic, 22(6):607–636, 1993.
  * [10] V. Goranko and D. Vakarelov.  Sahlqvist formulas in hybrid polyadic modal logics.  Journal of Logic and Computation, 11(5):737–754, 10 2001.
  * [11] I. Hodkinson.  Hybrid formulas and elementarily generated modal logics.  Notre Dame Journal of Formal Logic, 47(4):443–478, 10 2006.
  * [12] I. Hodkinson and L. Paternault.  Axiomatizing hybrid logic using modal logic.  Journal of Applied Logic, 8(4):386 – 396, 2010.  Special Issue on Hybrid Logics.
  * [13] A. Palmigiano, S. Sourabh, and Z. Zhao.  Sahlqvist theory for impossible worlds.  Journal of Logic and Computation, 27(3):775–816, 2017.
  * [14] H. Sahlqvist.  Completeness and correspondence in the first and second order semantics for modal logic.  In Studies in Logic and the Foundations of Mathematics, volume 82, pages 110–143. 1975.
  * [15] K. Tamura.  Hybrid logic with pure and Sahlqvist axioms.  http://www.st.nanzan-u.ac.jp/info/sasaki/2005mlg/43-45.pdf.
  * [16] B. ten Cate.  Model theory for extended modal languages.  PhD thesis, University of Amsterdam, 2005.
  * [17] B. ten Cate, M. Marx, and J. P. Viana.  Hybrid logics with Sahlqvist axioms.  Logic Journal of the IGPL, (3):293–300, 2006.
  * [18] J. van Benthem.  Modal logic and classical logic.  Bibliopolis, 1983.
  * [19] H. Wassenaar.  Taming Frankenstein’s logic: How I turned the tables on hybrid logic.  Master’s thesis, University of Groningen, the Netherlands, 2007.
  * [20] Z. Zhao.  Algorithmic correspondence and canonicity for possibility semantics.  Journal of Logic and Computation, 31(2):523–572, 2021.
  * [21] Z. Zhao.  Algorithmic correspondence for hybrid logic with binder.  Logic Journal of the IGPL, 2021.
  * [22] Z. Zhao.  Sahlqvist-type completeness theory for hybrid logic with binder.  submitted. ArXiv preprint arXiv:2207.01288, 2022.