# Correspondence and Canonicity Theory of Quasi-Inequalities and
$\Pi_{2}$-Statements in Modal Subordination Algebras

Zhiguang Zhao

###### Abstract

In the present paper, we study the correspondence and canonicity theory of
modal subordination algebras and their dual Stone space with two relations,
generalizing correspondence results for subordination algebras in [13, 14, 15,
25]. Due to the fact that the language of modal subordination algebras
involves a binary subordination relation, we will find it convenient to use
the so-called quasi-inequalities and $\Pi_{2}$-statements. We use an algorithm
to transform (restricted) inductive quasi-inequalities and (restricted)
inductive $\Pi_{2}$-statements to equivalent first-order correspondents on the
dual Stone spaces with two relations with respect to arbitrary (resp.
admissible) valuations.

Keywords: correspondence theory; canonicity; $\Pi_{2}$-statements; modal
subordination algebras

##  1 Introduction

In the study of the relations among logic, algebra and topology, a key tool is
the dualities between algebras and topological spaces. This line of research
started from Stone [26], who showed the duality between Boolean algebras and
compact Hausdorff zero-dimensional spaces (which are now called Stone spaces).
Later on, many other dualities are studied, e.g. Priestley duality for
distributive lattices and Priestley spaces [23, 24], Esakia duality for
Heyting algebras and Esakia spaces [18], Jónsson-Tarski duality for modal
algebras and modal spaces [19, 20], and de Vries duality for de Vries algebras
and compact Hausdorff spaces [16].

De Vries duality connects compact Hausdorff spaces with de Vries algebras,
which are complete Boolean algebras with a binary relation satisfying some
additional properties. Subordination algebras [4] are Boolean algebras with a
binary relation (called the subordination relation) which generalizes de Vries
algebras. Subordinations on Boolean algebras are in 1-1 correspondence with
quasi-modal operators [9]. It is proved in [4] that subordination algebras are
dually equivalent to Stone spaces with a closed relation, which are called
subordination spaces. Modal compact Hausdorff spaces are studied in [2] as a
the compact Hausdorff generalization of modal spaces, whose counterpart of de
Vries duality yields modal de Vries algebras. Therefore, it is natural to
consider the generalizations of modal de Vries algebras, namely modal
subordination algebras, as the background theory of studying modal compact
Hausdorff spaces. Indeed, modal subordination algebras are dually equivalent
to Stone spaces with two relations, one closed relation corresponding to the
subordination relation, and one clopen relation corresponding to the modality.

It is natural to consider the correspondence theory of propositional formulas
on subordination spaces with their first-order corresponding conditions on
subordination spaces. Indeed, in the literature, there are works of
correspondence theory for subordination algebras and subordination spaces. In
[13, 14, 15], de Rudder et al. studied correspondence theory of subordination
algebras in the perspective of quasi-modal operators. In [25], Santoli studied
the topological correspondence theory between conditions on algebras and
first-order conditions on the dual subordination spaces, in the language of a
binary connective definable from the squigarrow associated with the
subordination relation, using the so-called $\forall\exists$-statements [3, 5,
6] (which we call $\Pi_{2}$-statements in the present paper). Balbiani and
Kikot [1] investigated the Sahlqvist theory in the language of region-based
modal logics of space, which uses a contact relation.

Since the language of modal subordination algebras involves a binary
subordination relation, and many natural conditions on subordination algebras
and modal subordination algebras involves quasi-inequalities and
$\Pi_{2}$-statements, we will we follow the approach of Santoli in the sense
of using $\Pi_{2}$-statements, and partly follow the approach of de Rudder in
the sense of using quasi-modal operators which are not closed under the
admissible subsets. We use an algorithm to transform (restricted) inductive
quasi-inequalities and (restricted) inductive $\Pi_{2}$-statements to
equivalent first-order correspondents on the dual Stone spaces with two
relations with respect to arbitrary (resp. admissible) valuations.

The paper is organized as follows: Section 2 gives preliminaries on modal
subordination algebras and Stone space with two relations. In Part I, we study
the correspondence and canonicity theory for quasi-inequalities. Section 3
gives the syntax and semantics of the logic language we are considering.
Section 4 gives preliminaries on algorithmic correspondence. We give the
definition of inductive quasi-inequalities in Section 5, define a version of
the algorithm $\mathsf{ALBA}$ in Section 6, show its soundness in Section 7,
success on inductive quasi-inequalities in Section 8 and the canonicity of
restricted inductive quasi-inequalities in Section 9. Section 10 gives some
examples of the execution of $\mathsf{ALBA}$ on quasi-inequalities. In Part
II, we study the correspondence and canonicity theory for
$\Pi_{2}$-statements. Section 11 gives the syntax and semantics for
$\Pi_{2}$-statements. Section 12 defines inductive $\Pi_{2}$-statements and
restricted inductive $\Pi_{2}$-statements. Section 13 gives a version of the
algorithm $\mathsf{ALBA}^{\Pi_{2}}$ for $\Pi_{2}$-statements. We state its
soundness with respect to arbitrary valuations in Section 14. We prove its
success on inductive and restricted inductive $\Pi_{2}$-statements in Section
15 and canonicity of restricted inductive $\Pi_{2}$-statements in Section 16.
Section 17 gives an example of the execution of $\mathsf{ALBA}$ on a
$\Pi_{2}$-statement. We give some comparisons with existing works in Section
18.

##  2 Modal Subordination Algebras and Stone Space with Two Relations

In this section, we give the definitions of modal subordination algebras and
special classes of modal subordination algebras, as well as their dual Stone
space with two relations. Basically, we generalize upper continuous modal de
Vries algebras (abbreviation: UMDVs, see [2]) to modal subordination algebras.
The reason why we choose UMDVs is that the diamond there is finitely additive
(see Proposition 9), which makes it easier to develop a correspondence theory.

###  2.1 Subordination Algebras, de Vries Algebras and Modal de Vries Algebras

######  Definition 1 (Subordination Algebra, Definition 2.1.1 in [25]).

A _subordination algebra_ is a pair $(B,\prec)$ where $B$ is a Boolean algebra
and $\prec$ is a _subordination_ , which is a binary relation on $B$
satisfying the following properties:

  * •

$0\prec 0$ and $1\prec 1$;

  * •

$a\prec b$ and $a\prec c$ implies $a\prec b\land c$;

  * •

$a\prec c$ and $b\prec c$ implies $a\lor b\prec c$;

  * •

$a\leq b\prec c\leq d$ implies $a\prec d$.

Equivalently, we can describe a subordination $\prec$ on a Boolean algebra $B$
by an operation $\rightsquigarrow:B\times B\to\\{0,1\\}\subseteq B$ such that

  * •

$a\rightsquigarrow b\in\\{0,1\\}$;

  * •

$0\rightsquigarrow 0=1\rightsquigarrow 1=1$;

  * •

$a\rightsquigarrow b=1$ and $a\rightsquigarrow c=1$ implies $a\rightsquigarrow
b\land c=1$;

  * •

$a\rightsquigarrow c=1$ and $b\rightsquigarrow c=1$ implies $a\lor
b\rightsquigarrow c=1$;

  * •

$b\rightsquigarrow c=1$, $a\leq b$ and $c\leq d$ implies $a\rightsquigarrow
d=1$.

Given a subordination $\prec$ on $B$, we can obtain an operation
$\rightsquigarrow:B\times B\to\\{0,1\\}\subseteq B$ satysfying the properties
above by defining $a\rightsquigarrow b=1$ iff $a\prec b$. Given an operation
$\rightsquigarrow:B\times B\to\\{0,1\\}\subseteq B$ satysfying the properties
above, we can obtain a subordination $\prec$ by defining $\prec=\\{(a,b)\in
B\times B:a\rightsquigarrow b=1\\}$. Therefore, we have a 1-1 correspondence
between subordinations $\prec$ and operations $\rightsquigarrow$ satisfying
the properties above.

######  Definition 2 (Contact Algebra, Definition 2.1.3 in [25]).

A _contact algebra_ is a subordination algebra $(B,\prec)$ where $\prec$
satisfies the following two additional properties:

  * •

$a\prec b$ implies $a\leq b$;

  * •

$a\prec b$ implies $\neg b\prec\neg a$.

######  Definition 3 (Compingent Algebra, Definition 2.1.4 in [25]).

A _compingent algebra_ is a contact algebra $(B,\prec)$ where $\prec$
satisfies the following two additional properties:

  * •

$a\prec b$ implies $\exists c:a\prec c\prec b$;

  * •

$a\neq 0$ implies $\exists b\neq 0:b\prec a$.

######  Definition 4 (de Vries Algebra, Definition 2.2.1 in [25]).

A _de Vries algebra_ is a compingent algebra $(B,\prec)$ where $B$ is a
complete Boolean algebra.

######  Definition 5 (Modal de Vries Algebra, Definition 4.7 in [2]).

A _modal de Vries algebra_ is a tuple $(B,\prec,\Diamond)$ where $(B,\prec)$
is a de Vries algebra and $\Diamond$ is _de Vries additive_ , i.e. it
satisfies the following two properties:

  * •

$\Diamond 0=0$;

  * •

for all $a_{1},a_{2},b_{1},b_{2}\in B$, $a_{1}\prec a_{2}$ and $b_{1}\prec
b_{2}$ implies that $\Diamond(a_{1}\lor a_{2})\prec\Diamond(b_{1}\lor b_{2})$.

######  Proposition 6 (Proposition 4.8 in [2]).

In a modal de Vries algebra $(B,\prec,\Diamond)$, $\Diamond$ is proximity
preserving, i.e. $a\prec b$ implies $\Diamond a\prec\Diamond b$ for all
$a,b\in B$.

######  Proposition 7 (Proposition 4.10 in [2]).

In a de Vries algebra $(B,\prec)$, if $\Diamond$ is finitely additive (i.e.
$\Diamond(a\lor b)=\Diamond a\lor\Diamond b$ for all $a,b\in B$) and proximity
preserving, then it is de Vries additive.

Notice that in a modal de Vries algebra $(B,\prec,\Diamond)$, the de Vries
additive operation $\Diamond$ is not necessarily order-preserving or finitely
additive. However, in upper continuous modal de Vries algebras, $\Diamond$ is
finitely additive.

######  Definition 8 (Upper continuity, Definition 4.14 in [2]).

A modal de Vries algebra $(B,\prec,\Diamond)$ is _upper continuous_ , if it
satiesfies the following property:

$\Diamond a=\bigwedge\\{\Diamond b:a\prec b\\}\mbox{ for any }a,b\in B.$

######  Proposition 9 (Proposition 4.15 in [2]).

In an upper continuous modal de Vries algebra $(B,\prec,\Diamond)$, $\Diamond$
is both order-preserving and finitely additive.

###  2.2 Modal Subordination Algebras, Stone Spaces with Two Relations and
their Object-Level Duality

In this subsection we define the modal subordination algebras, and their dual
Stone spaces with two relations, and give their object-level duality. The
reason why we choose to make modal subordination algebras as subordination
algebras with normal and finitely additive operations is that it is easier to
develop the correspondence theory for normal and finitely additive operations.

######  Definition 10 (Modal Subordination Algebra).

A _modal subordination algebra_ is a tuple $(B,\prec,\Diamond)$ where
$(B,\prec)$ is a subordination algebra, $\Diamond$ satisfies the following
conditions: for all $a,b\in B$,

  * •

$\Diamond$ is normal, namely $\Diamond 0=0$;

  * •

$\Diamond$ is finitely additive, namely $\Diamond(a\lor b)=\Diamond
a\lor\Diamond b$.

######  Definition 11.

A modal subordination algebra is

  * •

a _modal contact algebra_ , if $(B,\prec)$ is a contact algebra;

  * •

a _modal compingent algebra_ , if $(B,\prec)$ is a compingent algebra;

  * •

_proximity preserving_ , if for all $a,b\in B$, $a\prec b$ implies that
$\Diamond a\prec\Diamond b$;

  * •

an _additive modal de Vries algebra_ , if $(B,\prec)$ is a de Vries algebra
and $\Diamond$ is proximity preserving;

  * •

an _upper continuous modal de Vries algebra_ , if $(B,\prec,\Diamond)$ is an
additive modal de Vries algebra and $\Diamond$ is upper continuous.

In what follows we will define the dual topological structure of a modal
subordination algebra. Since there is the duality between subordination
algebras and Stone spaces with closed relations (see [25, Section 2.1.1]), and
there is the duality between modal algebras and modal spaces (see [7, Chapter
5]), we can put the two together to obtain the duality between modal
subordination algebras and Stone spaces with _two relations_.

######  Definition 12 (Definition 2.1.9 in [25]).

Take any modal subordination algebra $(B,\prec,\Diamond)$ and any $S\subseteq
B$. We define $\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}S$ to be the
upset of $S$ with respect to the relation $\prec$, i.e.

$\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}S:=\\{b\in B:\exists s\in
S\mbox{ such that }s\prec b\\}.$

######  Definition 13 (Stone Spaces with two relations).

A _Stone space with two relations_ $(X,\tau,R,R^{\prime})$ is defined as
follows:

  * •

$(X,\tau)$ is a Stone space;

  * •

$R$ is a closed relation on $X$, i.e. for each closed subset $F$ of $X$, both
$R[F]$ and $R^{-1}[F]$ are closed;

  * •

$R^{\prime}[x]$ is closed for all $x\in X$ and $R^{\prime-1}[U]$ is clopen for
all clopen $U\subseteq X$.

Given a modal subordination algebra $(B,\prec,\Diamond)$, its dual Stone space
with two relations $(X,\tau,R,R^{\prime})$ is defined as follows:

  * •

$(X,\tau)$ is the dual Stone space of $B$;

  * •

$R$ is such that $xRy$ iff
$\mathrel{\rotatebox{90.0}{$\twoheadrightarrow$}}x\subseteq y$ (It is easy to
check that $R$ is a closed relation on $X$);

  * •

$R^{\prime}$ is such that $xR^{\prime}y$ iff for all $a\in y$, $\Diamond a\in
x$ (It is easy to check that $R^{\prime}[x]$ is closed for all $x\in X$ and
$R^{\prime-1}[U]$ is clopen for all clopen $U\subseteq X$).

Given a Stone space with two relations $(X,\tau,R,R^{\prime})$, its dual modal
subordination algebra $(B,\prec,\Diamond)$ is defined as follows:

  * •

$B$ is the dual Boolean algebra of the Stone space $(X,\tau)$, i.e. $B$
consists of the clopen subsets of $X$;

  * •

$U\prec V$ iff $R[U]\subseteq V$;

  * •

$\Diamond U=R^{\prime-1}[U]$.

###  2.3 Canonical Extensions

In this subsection, we define the canonical extensions of modal subordination
algebras, as well as give the semantic environment of the correspondence and
canonicity theory for modal subordination algebras.

####  2.3.1 Canonical Extensions of Boolean Algebras

######  Definition 14 (Canonical Extension of Boolean Algebras, cf. Chapter 6,
Definition 104 in [8]).

The _canonical extension_ of a Boolean algebra $B$ is a complete Boolean
algebra $B^{\delta}$ containing $B$ as a sub-Boolean algebra such that the
following two conditions hold:

  * (_denseness_) each element of $B^{\delta}$ can be represented both as a join of meets and as a meet of joins of elements from $B$;

  * (_compactness_) for all $X,Y\subseteq B$ with $\bigwedge X\leq\bigvee Y$ in $B^{\delta}$, there are finite subsets $X_{0}\subseteq X$ and $Y_{0}\subseteq Y$ such that $\bigwedge X_{0}\leq\bigvee Y_{0}.$111In fact, this is an equivalent formulation of the definition in [8].

An element $x\in B^{\delta}$ is _open_ (resp.  _closed_) if it is the join
(resp. meet) of some $X\subseteq B$. We use $\mathsf{O}(B^{\delta})$ (resp.
$\mathsf{K}(B^{\delta})$) to denote the set of open (resp. closed) elements of
$B^{\delta}$. It is easy to see that elements in $B$ are exactly the ones
which are both closed and open (i.e.,  _clopen_).

It is well-known that for any given $B$, its canonical extension is unique up
to isomorphism and that assuming the axiom of choice, the canonical extension
of a Boolean algebra is a perfect Boolean algebra, i.e., a complete and atomic
Boolean algebra.

####  2.3.2 Canonical Extensions of Maps

Let $A,B$ be Boolean algebras. There are two canonical ways to extend an
order-preserving map $f:A\rightarrow B$ to a map $A^{\delta}\to B^{\delta}$:

######  Definition 15 ($\sigma$\- and $\pi$-extension).

([8, page 375]) For any order-preserving map $f:A\rightarrow B$ and $u\in
A^{\delta}$, we define

$f^{\sigma}(u)=\bigvee\\{\bigwedge\\{f(a):x\leq a\in A\\}:u\geq
x\in\mathsf{K}(A^{\delta})\\}$ $f^{\pi}(u)=\bigwedge\\{\bigvee\\{f(a):y\geq
a\in A\\}:u\leq y\in\mathsf{O}(A^{\delta})\\}.$

####  2.3.3 Canonical Extensions of Modal Subordination Algebras

Since in a modal subordination algebra $(B,\prec,\Diamond)$, $\Diamond$ is
normal and finitely additive, it is _smooth_ , i.e.,
$\Diamond^{\sigma}=\Diamond^{\pi}$ (cf. [8, Proposition 111(3)]). Therefore,
in the canonical extension we can take either of the two extensions.

For the $\prec$ relation, we define its canonical extension by defining the
$\pi$-extension $\rightsquigarrow_{\prec}^{\pi}:B^{\delta}\times B^{\delta}\to
B^{\delta}$ of the assocciated strict implication $\rightsquigarrow_{\prec}$
and then take the associated subordination
$\prec_{\rightsquigarrow^{\pi}_{\prec}}$ (which we also denote $\prec^{\pi}$)
associated with $\rightsquigarrow^{\pi}_{\prec}$.

######  Proposition 16 (Folklore.).

  * •

$\Diamond^{\sigma}$ is completely join-preserving, i.e. it preserves arbitrary
(including empty) joins.

  * •

$\rightsquigarrow^{\pi}_{\prec}$ is completely join-reversing in the first
coordinate and completely meet-preserving in the second coordinate, i.e.

    * –

$\bigvee\\{a_{i}:i\in
I\\}\rightsquigarrow^{\pi}_{\prec}b=\bigwedge\\{a_{i}\rightsquigarrow^{\pi}_{\prec}b:i\in
I\\}$;

    * –

$a\rightsquigarrow^{\pi}_{\prec}\bigwedge\\{b_{i}:i\in
I\\}=\bigwedge\\{a\rightsquigarrow^{\pi}_{\prec}b_{i}:i\in I\\}$.

Indeed, there is another way of obtaining the canonical extension of the modal
subordination algebras, namely first take its dual space
$(X,\tau,R,R^{\prime})$, and then drop off the topological structure to obtain
a _birelational Kripke frame_ $(X,R,R^{\prime})$, and then define the
canonical extension $(B^{\circ},\prec^{\circ},\Diamond^{\circ})$ as follows:

  * •

$B^{\circ}$ is the power set Boolean algebra of $X$, i.e. $B^{\circ}$ consists
of all subsets of $X$;

  * •

$U\prec^{\circ}V$ iff $R[U]\subseteq V$;

  * •

$\Diamond^{\circ}U=R^{\prime-1}[U]$.

######  Proposition 17.

(Folklore.) The two definitions are equivalent, i.e.
$(B^{\circ},\prec^{\circ},\Diamond^{\circ})=(B^{\delta},\prec^{\pi},\Diamond^{\pi})$.

Therefore, the following diagram describes the relation between modal
subordination algebras and their canonical extensions, as well as their dual
Stone space with two relations, and the birelational Kripke frames obtained by
dropping the topology:

$(B,\prec,\Diamond)$$(B^{\delta},\prec^{\pi},\Diamond^{\pi})$$(X,\tau,R,R^{\prime})$$(X,R,R^{\prime})$$(\cdot)^{\delta}$$U$$\cong^{\partial}$$\cong^{\partial}$

Here $\cong^{\partial}$ means dual equivalence, $U$ is the forgetful functor
dropping the topology and replacing the clopen set Boolean algebra by the
powerset Boolean algebra, and $(\cdot)^{\delta}$ is taking the canonical
extension.

## Part I: Correspondence and Canonicity for Quasi-Inequalities

##  3 Syntax and Semantics

In this section, we introduce the syntax and semantics of the language of
modal subordination algebras.

###  3.1 Language and Syntax

######  Definition 18.

Given a countably infinite set $\mathsf{Prop}$ of propositional variables, the
modal subordination language $\mathcal{L}$ is defined as follows:

$\varphi::=p\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{{\Diamond}\\!\\!\\!\cdot\
}\varphi\mid{\boxdot}\varphi,$

where $p\in\mathsf{Prop}$. We will follow the standard rules for omission of
the parentheses. We also use $\mathsf{Prop}(\varphi)$ to denote the
propositional variables occuring in $\varphi$. We use the notation $\vec{p}$
to denote a set of propositional variables and use $\varphi(\vec{p})$ to
indicate that the propositional variables occur in $\varphi$ are all in
$\vec{p}$. We call a formula _pure_ if it does not contain propositional
variables. We use the notation $\overline{\theta}$ to indicate a finite list
of formulas. We use the notation $\theta(\eta/p)$ to indicate uniformly
substituting $p$ by $\eta$.

In the language of formulas, we use $\Diamond$ and $\Box$ as the syntax for
the normal and finitely additive operation, and use
${{\Diamond}\\!\\!\\!\cdot\ }$ and ${\boxdot}$ as the syntax for the
subordination on the Boolean algebra. We will also use the following syntactic
binary relations $\leq$ and $\prec$ to formalize the “less than or equal to”
relation and the subordination relation, respectively. Therefore, we use both
${{\Diamond}\\!\\!\\!\cdot\ },{\boxdot}$ and $\prec$ to denote the
subordination relation.

######  Definition 19.

  * •

An _inequality_ is of the form $\varphi\leq\psi$ or $\varphi\prec\psi$, where
$\varphi$ and $\psi$ are formulas.

  * •

A _meta-conjunction of inequalities_ is of the form
$\varphi_{1}\triangleleft_{1}\psi_{1}\ \&\ \ldots\ \&\
\varphi_{n}\triangleleft_{n}\psi_{n}$, where $n\geq 1$,
$\triangleleft_{i}\in\\{\leq,\prec\\}$. Typically a meta-conjunction of
inequalities is abbreviated as
$\overline{\varphi}\triangleleft\overline{\psi}$, and if all $\triangleleft$s
are $\leq$ (resp. $\prec$), then it is written as
$\overline{\varphi}\leq\overline{\psi}$ (resp.
$\overline{\varphi}\prec\overline{\psi}$).

  * •

A _quasi-inequality_ is of the form
$\overline{\varphi}\triangleleft\overline{\psi}\ \Rightarrow\
\overline{\gamma}\triangleleft\overline{\delta}$.

###  3.2 Semantics

We interpret formulas on the dual Stone space with two relations, with two
kinds of valuations, namely admissible valuations which interpret
propositional variables as clopen subsets of the space (i.e. interpret them as
elements of the dual modal subordination algebras), and arbitrary valuations
which interpret propositional variables as arbitrary subsets of the space
(i.e. interpret them as elements of the canonical extensions of the dual modal
subordination algebras).

######  Definition 20.

In a Stone space with two relations $(X,\tau,R,R^{\prime})$ (we abuse notation
to use $X$ to denote the space), we call $X$ the _domain_ of the space, and
$R$ is the relation corresponding to the subordination as well as
${{\Diamond}\\!\\!\\!\cdot\ }$ and ${\boxdot}$, and $R^{\prime}$ is the
relation corresponding to the modalities $\Diamond$ and $\Box$.

  * •

A _pointed Stone space with two relations_ is a pair $(X,w)$ where $w\in X$.

  * •

An _admissible model_ is a pair $M=(X,V)$ where $V:\mathsf{Prop}\to Clop(X)$
is an _admissible valuation_ on $X$ such that for all propositional variables
$p$, $V(p)$ is a clopen subset of $X$.

  * •

An _arbitrary model_ is a pair $M=(X,V)$ where $V:\mathsf{Prop}\to P(X)$ is an
_arbitrary valuation_ on $X$ such that for all propositional variables $p$,
$V(p)$ is an arbitrary subset of $X$.

Given a valuation $V$, a propositional variable $p\in\mathsf{Prop}$, a subset
$A\subseteq X$, we can define $V^{p}_{A}$, the _$p$ -variant of $V$_ as
follows: $V^{p}_{A}(q)=V(q)$ for all $q\neq p$ and $V^{p}_{A}(p)=A$.

Now the satisfaction relation can be defined as follows: given any Stone space
with two relations $(X,\tau,R,R^{\prime})$, any (admissible or arbitrary)
valuation $V$ on $X$, any $w\in X$,

$X,V,w\Vdash p$ | iff |  $w\in V(p)$;
---|---|---
$X,V,w\Vdash\bot$ | : | never;
$X,V,w\Vdash\top$ | : | always;
$X,V,w\Vdash\neg\varphi$ | iff |  $X,V,w\nVdash\varphi$;
$X,V,w\Vdash\varphi\land\psi$ | iff |  $X,V,w\Vdash\varphi$ and $X,V,w\Vdash\psi$;
$X,V,w\Vdash\varphi\lor\psi$ | iff |  $X,V,w\Vdash\varphi$ or $X,V,w\Vdash\psi$;
$X,V,w\Vdash\varphi\to\psi$ | iff |  $X,V,w\nVdash\varphi$ or $X,V,w\Vdash\psi$;
$X,V,w\Vdash\Box\varphi$ | iff |  $\forall v(R^{\prime}wv\ \Rightarrow\ X,V,v\Vdash\varphi)$;
$X,V,w\Vdash\Diamond\varphi$ | iff |  $\exists v(R^{\prime}wv\ \mbox{ and }\ X,V,v\Vdash\varphi)$;
$X,V,w\Vdash{\boxdot}\varphi$ | iff |  $\forall v(Rvw\ \Rightarrow\ X,V,v\Vdash\varphi)$;
$X,V,w\Vdash{{\Diamond}\\!\\!\\!\cdot\ }\varphi$ | iff |  $\exists v(Rvw\ \mbox{ and }\ X,V,v\Vdash\varphi)$.

Notice that here ${\boxdot}$ and ${{\Diamond}\\!\\!\\!\cdot\ }$ are
interpreted in the reverse direction of $R$. This is because we would like to
make $\varphi\prec\psi$ (which is interpreted as $R[V(\varphi)]\subseteq
V(\psi)$) equivalent to ${{\Diamond}\\!\\!\\!\cdot\ }\varphi\leq\psi$, so we
need to make ${{\Diamond}\\!\\!\\!\cdot\ }\varphi$ interpreted as
$R[V(\varphi)]$.

For any formula $\varphi$, we let $\llbracket\varphi\rrbracket^{X,V}=\\{w\in
X\mid X,V,w\Vdash\varphi\\}$ denote the _truth set_ of $\varphi$ in $(X,V)$
(sometimes we just use $V(\varphi)$ when the space is clear from the context).

  * •

The formula $\varphi$ is _globally true_ on $(X,V)$ (notation:
$X,V\Vdash\varphi$) if $X,V,w\Vdash\varphi$ for every $w\in W$.

  * •

We say that $\varphi$ is _admissibly valid_ on a Stone space with two
relations $X$ (notation: $X\Vdash_{Clop}\varphi$) if $\varphi$ is globally
true on $(X,V)$ for every admissible valuation $V$.

  * •

We say that $\varphi$ is _valid_ on a Stone space with two relations $X$
(notation: $X\Vdash_{P}\varphi$) if $\varphi$ is globally true on $(X,V)$ for
every arbitrary valuation $V$.

For the semantics of inequalities, meta-conjunctions of inequalities, quasi-
inequalities, they are given as follows:

######  Definition 21.

  * •

An inequality is interpreted as follows:

$X,V\Vdash\varphi\leq\psi\mbox{ iff }V(\varphi)\subseteq V(\psi);$
$X,V\Vdash\varphi\prec\psi\mbox{ iff }R[V(\varphi)]\subseteq V(\psi);$

  * •

A meta-conjunction of inequalities is interpreted as follows:

$X,V\Vdash\varphi_{1}\triangleleft_{1}\psi_{1}\ \&\ \ldots\ \&\
\varphi_{n}\triangleleft_{n}\psi_{n}\mbox{ iff
}X,V\Vdash\varphi_{i}\triangleleft_{i}\psi_{i}\mbox{ for all }i=1,\ldots,n;$

  * •

A quasi-inequality is interpreted as follows:

$X,V\Vdash\overline{\varphi}\triangleleft\overline{\psi}\ \Rightarrow\
\overline{\gamma}\triangleleft\overline{\delta}\mbox{ iff }$
$X,V\Vdash\overline{\gamma}\triangleleft\overline{\delta}\mbox{ holds whenever
}X,V\Vdash\overline{\varphi}\triangleleft\overline{\psi}.$

The definitions of validity are similar to formulas.

##  4 Preliminaries on Algorithmic Correspondence

In this section, we give necessary preliminaries on the correspondence
algorithm $\mathsf{ALBA}$ in the style of [10, 11, 27]. The algorithm
$\mathsf{ALBA}$ transforms the input quasi-inequality

$\varphi_{1}\leq\psi_{1}\ \&\ldots\&\ \varphi_{n}\leq\psi_{n}\ \&\
\gamma_{1}\prec\delta_{1}\ \&\ldots\&\ \gamma_{m}\prec\delta_{m}\ \Rightarrow\
\alpha\triangleleft\beta\mbox{ (where }\triangleleft\in\\{\prec,\leq\\})$

into an equivalent set of pure quasi-inequalities which does not contain
occurrences of propositional variables, and therefore can be translated into
the first-order correspondence language via the standard translation of the
expanded language (see page 4.2).

The ingredients for the algorithmic correspondence proof to go through can be
listed as follows:

  * •

An expanded language as the syntax of the algorithm, as well as its semantics;

  * •

An algorithm $\mathsf{ALBA}$ which transforms a given quasi-inequality into
equivalent pure quasi-inequalities;

  * •

A soundness proof of the algorithm;

  * •

A syntactically identified class of quasi-inequalities (namely the _inductive
quasi-inequalities_) on which the algorithm is successful;

  * •

A first-order correspondence language and first-order translation which
transforms pure quasi-inequalities into their equivalent first-order
correspondents.

  * •

A syntactically identified class of quasi-inequalities (namely the _restricted
inductive quasi-inequalities_) which are canonical.

In the remainder of this part, we will define an expanded language which the
algorithm will manipulate (Section 4.1), define the first-order correspondence
language of the expanded language and the standard translation (Section 4.2).
We give the definition of inductive quasi-inequalities (Section 5), define a
version of the algorithm $\mathsf{ALBA}$ (Section 6), and show its soundness
(Section 7), success on inductive quasi-inequalities (Section 8) and the
canonicity of restricted inductive quasi-inequalities (Section 9).

###  4.1 The expanded hybrid modal language

In the present subsection, we give the definition of the expanded language,
which will be used in the execution of the algorithm:

$\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{{\Diamond}\\!\\!\\!\cdot\
}\varphi\mid{\boxdot}\varphi\mid\blacksquare\varphi\mid\Diamondblack\varphi\mid{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}\varphi\mid{\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}\varphi$

where $\mathbf{i}\in\mathsf{Nom}$ is called a _nominal_. For $\mathbf{i}$, it
is interpreted as a singleton set. For $\blacksquare$ and $\Diamondblack$,
they are interpreted as the box and diamond modality on the inverse relation
$R^{\prime-1}$, and for
${\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$ and
${\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$, they are interpreted as the box and diamond modality on the relation
$R$.

For the semantics of the expanded language, the valuation $V$ is extended to
$\mathsf{Prop}\cup\mathsf{Nom}$ such that $V(\mathbf{i})$ is a singleton for
each $\mathbf{i}\in\mathsf{Nom}$. 222Notice that we allow admissible
valuations to interpret nominals as singletons, even if singletons might not
be clopen. The admissibility restrictions are only for the propositional
variables. The additional semantic clauses can be given as follows:

$X,V,w\Vdash\mathbf{i}$ | iff |  $V(\mathbf{i})=\\{w\\}$;
---|---|---
$X,V,w\Vdash\blacksquare\varphi$ | iff |  $\forall v(R^{\prime}vw\ \Rightarrow\ X,V,v\Vdash\varphi)$;
$X,V,w\Vdash\Diamondblack\varphi$ | iff |  $\exists v(R^{\prime}vw\ \mbox{ and }\ X,V,v\Vdash\varphi)$;
$X,V,w\Vdash{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\ }}}\varphi$ | iff |  $\forall v(Rwv\ \Rightarrow\ X,V,v\Vdash\varphi)$;
$X,V,w\Vdash{\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\ }}}\varphi$ | iff |  $\exists v(Rwv\ \mbox{ and }\ X,V,v\Vdash\varphi)$.

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

In the first-order correspondence language, we have two binary predicate
symbols $R$ and $R^{\prime}$ corresponding to the two binary relations in the
Stone space with two relations, a set of unary predicate symbols $P$
corresponding to each propositional variable $p$.

######  Definition 22.

The standard translation of the expanded language is defined as follows:

  * •

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

  * •

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

  * •

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

  * •

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

  * •

$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(R^{\prime}xy\to ST_{y}(\varphi))$;

  * •

$ST_{x}(\Diamond\varphi):=\exists y(R^{\prime}xy\land ST_{y}(\varphi))$;

  * •

$ST_{x}(\blacksquare\varphi):=\forall y(R^{\prime}yx\to ST_{y}(\varphi))$;

  * •

$ST_{x}(\Diamondblack\varphi):=\exists y(R^{\prime}yx\land ST_{y}(\varphi))$;

  * •

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

  * •

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

  * •

$ST_{x}({\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}\varphi):=\forall y(Rxy\to ST_{y}(\varphi))$;

  * •

$ST_{x}({\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}\varphi):=\exists y(Rxy\land ST_{y}(\varphi))$;

  * •

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

  * •

$ST(\varphi\prec\psi):=\forall x(ST_{x}({{\Diamond}\\!\\!\\!\cdot\
}\varphi)\to ST_{x}(\psi))$;

  * •

$ST(\varphi_{1}\triangleleft_{1}\psi_{1}\ \&\ \ldots\ \&\
\varphi_{n}\triangleleft_{n}\psi_{n}):=ST(\varphi_{1}\triangleleft_{1}\psi_{1})\land\ldots\land
ST(\varphi_{n}\triangleleft_{n}\psi_{n})$;

  * •

$ST(\overline{\varphi}\triangleleft\overline{\psi}\ \Rightarrow\
\overline{\gamma}\triangleleft\overline{\delta}):=ST(\overline{\varphi}\triangleleft\overline{\psi})\to
ST(\overline{\gamma}\triangleleft\overline{\delta})$.

It is easy to see that this translation is correct:

######  Proposition 23.

For any Stone space with two relations $X$, any valuation $V$ on $X$, any
$w\in X$ and any expanded language formula $\varphi$,

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

######  Proposition 24.

For any Stone space with two relations $X$, any valuation $V$ on $X$, and
inequality $\mathsf{Ineq}$, meta-conjunction of inequalities
$\mathsf{MetaConIneq}$, quasi-inequality $\mathsf{Quasi}$,

$X,V\Vdash\mathsf{Ineq}\mbox{ iff }X,V\vDash ST(\mathsf{Ineq});$
$X,V\Vdash\mathsf{MetaConIneq}\mbox{ iff }X,V\vDash ST(\mathsf{MetaConIneq});$
$X,V\Vdash\mathsf{Quasi}\mbox{ iff }X,V\vDash ST(\mathsf{Quasi}).$

##  5 Inductive Quasi-Inequalities for Modal Subordination Algebras

In this section, we define inductive quasi-inequalities for modal
subordination algebras and Stone spaces with two relations. Here we consider
quasi-inequalities of the form

$\varphi_{1}\leq\psi_{1}\ \&\ldots\&\ \varphi_{n}\leq\psi_{n}\ \&\
\gamma_{1}\prec\delta_{1}\ \&\ldots\&\ \gamma_{m}\prec\delta_{m}\ \Rightarrow\
\alpha\triangleleft\beta\mbox{ (where }\triangleleft\in\\{\prec,\leq\\}),$

where $n,m\geq 0$. We follow the presentation of [12].

######  Definition 25 (Order-type of propositional variables).

(cf. [11, page 346]) For an $n$-tuple $(p_{1},\ldots,p_{n})$ of propositional
variables, an order-type $\varepsilon$ of $(p_{1},\ldots,p_{n})$ is an element
in $\\{1,\partial\\}^{n}$. We say that $p_{i}$ has order-type 1 if
$\varepsilon_{i}=1$, and denote $\varepsilon(p_{i})=1$ or $\varepsilon(i)=1$;
we say that $p_{i}$ has order-type $\partial$ if $\varepsilon_{i}=\partial$,
and denote $\varepsilon(p_{i})=\partial$ or $\varepsilon(i)=\partial$.

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

(cf. [12, Definition 4]) The _positive_ (resp.  _negative_) generation tree of
any given formula $\theta$ is defined by first labelling the root of the
generation tree of $\theta$ with $+$ (resp. $-$) and then labelling the
children nodes as follows:

  * •

Assign the same sign to the children nodes of any node labelled with
$\Box,\Diamond,\boxdot,{\Diamond}\\!\\!\\!\cdot\ $,
$\blacksquare,\Diamondblack,{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}},{\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}},\lor,\land$;

  * •

Assign the opposite sign to the child node of any node labelled with $\neg$;

  * •

Assign the opposite sign to the first child node and the same sign to the
second child node of any node labelled with $\to$.

Nodes in signed generation trees are _positive_ (resp.  _negative_) if they
are signed $+$ (resp. $-$).

Signed generation trees will be used in the quasi-inequalities

$\varphi_{1}\leq\psi_{1}\ \&\ldots\&\ \varphi_{n}\leq\psi_{n}\ \&\
\gamma_{1}\prec\delta_{1}\ \&\ldots\&\ \gamma_{m}\prec\delta_{m}\ \Rightarrow\
\alpha\triangleleft\beta\mbox{ (where }\triangleleft\in\\{\prec,\leq\\}),$

where the positive generation trees $+\psi_{i},+\delta_{j},+\alpha$ and the
negative generation trees $-\varphi_{i},-\gamma_{j},-\beta$ will be
considered. We will also say that a quasi-inequality is _uniform_ in a
variable $p_{i}$ if all occurrences of $p_{i}$ in
$+\psi_{i},+\delta_{j},+\alpha,-\varphi_{i},-\gamma_{j},-\beta$ have the same
sign, and that a quasi-inequality is $\varepsilon$-_uniform_ in an array
$\vec{p}$ if it is uniform in $p_{i}$, occurring with the sign indicated by
$\varepsilon$ (i.e., $p_{i}$ has the sign $+$ if $\varepsilon(p_{i})=1$, and
has the sign $-$ if $\varepsilon(p_{i})=\partial$), for each propositional
variable $p_{i}$ in $\vec{p}$.

For any given formula $\theta(p_{1},\ldots,p_{n})$, any order-type
$\varepsilon$ over $n$, and any $1\leq i\leq n$, an _$\varepsilon$ -critical
node_ in a signed generation tree of $\theta$ is a leaf node $+p_{i}$ when
$\varepsilon_{i}=1$ or $-p_{i}$ when $\varepsilon_{i}=\partial$. An
$\varepsilon$-critical branch in a signed generation tree is a branch from an
$\varepsilon$-critical nodes. The $\varepsilon$-critical occurrences are
intended to be those which the algorithm $\mathsf{ALBA}$ will solve for. We
say that $+\theta$ (resp. $-\theta$) is $\varepsilon$-uniform, and write
$\varepsilon(+\theta)$ (resp. $\varepsilon(-\theta)$), if every leaf node in
the signed generation tree of $+\theta$ (resp. $-\theta$) is
$\varepsilon$-critical.

We will also use the notation $+\iota\ll\ast\theta$ (resp.
$-\iota\ll\ast\theta$) to indicate that an occurence of a subformula $\iota$
inherits the positive (resp. negative) sign from the signed generation tree
$\ast\theta$, where $\ast\in\\{+,-\\}$. We will write
$\varepsilon(\iota)\ll\ast\theta$ (resp.
$\varepsilon^{\partial}(\iota)\ll\ast\theta$) to indicate that the signed
generation subtree $\iota$, with the sign inherited from $\ast\theta$, is
$\varepsilon$-uniform (resp. $\varepsilon^{\partial}$-uniform). We say that a
propositional variable $p$ is _positive_ (resp.  _negative_) in $\theta$ if
$+p\ll+\theta$ (resp. $-p\ll+\theta$).

In what follows, we will use the following classification of nodes:

######  Definition 27.

(Classification of nodes, cf. [12, Definition 5]) Nodes in signed generation
trees are called _$\Delta$ -adjoints_, _syntactically left residual (SLR)_ ,
_syntactically right adjoint (SRA)_ , and _syntactically right residual (SRR)_
, according to Table 1.333For a detailed explanation why these names are used,
see [22, Remark 3.24].

Skeleton | PIA
---|---
$\Delta$-adjoints | SRA
| $+$ | $\vee$ |
---|---|---
$-$ | $\wedge$ |
| $+$ | $\wedge$ | $\neg$ | $\Box$ | $\blacksquare$ | ${\boxdot}$ | ${\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\ }}}$
---|---|---|---|---|---|---
$-$ | $\vee$ | $\neg$ | $\Diamond$ | $\Diamondblack$ | ${{\Diamond}\\!\\!\\!\cdot\ }$ | ${\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\ }}}$
SLR | SRR
| $+$ | $\wedge$ | $\neg$ | $\Diamond$ | $\Diamondblack$ | ${{\Diamond}\\!\\!\\!\cdot\ }$ | ${\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\ }}}$ |
---|---|---|---|---|---|---|---
$-$ | $\vee$ | $\neg$ | $\Box$ | $\blacksquare$ | ${\boxdot}$ | ${\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\ }}}$ | $\to$
| $+$ | $\vee$ | $\to$
---|---|---
$-$ | $\wedge$ |
Table 1: Skeleton and PIA nodes.

######  Definition 28 (Good/PIA/Skeleton branches).

A branch in a signed generation tree is called a

  * •

_good branch_ if it is the concatenation of two paths $P_{1}$ and $P_{2}$, one
of which might be of length $0$, such that $P_{1}$ is a path from the leaf
consisting (apart from variable nodes) of PIA-nodes only, and $P_{2}$ consists
(apart from variable nodes) of Skeleton-nodes only;

  * •

_PIA branch_ if it is a good branch and $P_{2}$ is of length 0;

  * •

_Skeleton branch_ if it is a good branch and $P_{1}$ is of length 0;

######  Definition 29 (Inductive signed generation trees).

(cf. [12, Definition 6]) For any order-type $\varepsilon$ and any irreflexive
and transitive binary relation $<_{\Omega}$ on $p_{1},\ldots p_{n}$ (called
_dependence order_ on the variables), the signed generation tree $*\theta$
$(*\in\\{-,+\\})$ of a formula $\theta(p_{1},\ldots p_{n})$ is
_$(\Omega,\varepsilon)$ -inductive_ if

  1. 1.

for all $1\leq i\leq n$, every $\varepsilon$-critical branch with leaf $p_{i}$
is good;

  2. 2.

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

    1. (a)

$\varepsilon^{\partial}(\iota)\ll\ast\theta$ (cf. page 26), and

    2. (b)

$p_{k}<_{\Omega}p_{i}$ for every $p_{k}$ that occurs in $\iota$.

The definitions above are mostly straightforward adaptations from standard
$\mathsf{ALBA}$ setting for inequalities to the present paper. The following
two definitions are specific in the quasi-inequality setting. Intuitively, the
receiving inequality $\varphi\leq\psi$ (resp. $\gamma\prec\delta$) is used to
receive minimal valuations, while the solvable inequality $\varphi\leq\psi$
(resp. $\gamma\prec\delta$) will be transformed into inequalities with minimal
valuation $\theta\leq p$ (if $\varepsilon(p)=1$) or $p\leq\theta$ (if
$\varepsilon(p)=\partial$), such that all propositional variables $q$
occurring in $\theta$ has dependence order below $p$, i.e. $q<_{\Omega}p$.

######  Definition 30 (Receiving inequality).

An inequality $\varphi\leq\psi$ (resp. $\gamma\prec\delta$) is said to be
$(\Omega,\varepsilon)$-receiving, if both of $-\varphi,+\psi$ (resp.
$-\gamma,+\delta$) are $\varepsilon^{\partial}$-uniform;

######  Definition 31 (Solvable inequality).

An inequality $\varphi\leq\psi$ (resp. $\gamma\prec\delta$) is said to be
$(\Omega,\varepsilon)$-solvable, if

  * •

exactly one of $-\varphi,+\psi$ (resp. $-\gamma,+\delta$) is
$\varepsilon^{\partial}$-uniform (without loss of generality we denote the
$\varepsilon^{\partial}$-uniform one $\star\theta$ and the other one
$*\iota$);

  * •

$*\iota$ is $(\Omega,\varepsilon)$-inductive, and all $\varepsilon$-critical
branches in $*\iota$ are PIA branches;

  * •

for all the $\varepsilon$-critical branches in $*\iota$ ending with $p$, all
propositional variables $q$ in $\star\theta$, we have $q<_{\Omega}p$.

######  Definition 32.

A quasi-inequality

$\varphi_{1}\leq\psi_{1}\ \&\ldots\&\ \varphi_{n}\leq\psi_{n}\ \&\
\gamma_{1}\prec\delta_{1}\ \&\ldots\&\ \gamma_{m}\prec\delta_{m}\ \Rightarrow\
\alpha\triangleleft\beta\mbox{ (where }\triangleleft\in\\{\prec,\leq\\})$

is _$(\Omega,\varepsilon)$ -inductive_ if

  * •

each inequality $\varphi\leq\psi$ and $\gamma\prec\delta$ is either
$(\Omega,\varepsilon)$-receiving or $(\Omega,\varepsilon)$-solvable;

  * •

$+\alpha$ and $-\beta$ are $(\Omega,\varepsilon)$-inductive signed generation
trees;

A quasi-inequality is _inductive_ if it is $(\Omega,\varepsilon)$-inductive
for some ($\Omega$, $\varepsilon$).

##  6 Algorithm

In the present section, we define the algorithm $\mathsf{ALBA}$ which compute
the first-order correspondence of the input quasi-inequality in the style of
[11]. The algorithm $\mathsf{ALBA}$ proceeds in three stages. Firstly,
$\mathsf{ALBA}$ receives a quasi-inequality

$\varphi_{1}\leq\psi_{1}\ \&\ldots\&\ \varphi_{n}\leq\psi_{n}\ \&\
\gamma_{1}\prec\delta_{1}\ \&\ldots\&\ \gamma_{m}\prec\delta_{m}\ \Rightarrow\
\alpha\triangleleft\beta\mbox{ (where }\triangleleft\in\\{\prec,\leq\\})$

as input, which do not contain nominals or black connectives
$\Diamondblack,\blacksquare,{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}},{\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$.

  1. 1.

Preprocessing and first approximation:

    1. (a)

In each inequality $\theta\triangleleft\eta$ (where
$\triangleleft\in\\{\leq,\prec\\}$) in the quasi-inequality, consider the
signed generation trees $+\theta$ and $-\eta$, apply the distribution rules:

      1. i.

Push down $+\Diamond,+{{\Diamond}\\!\\!\\!\cdot\ },-\neg,+\land,-\to$ by
distributing them over nodes labelled with $+\lor$ which are Skeleton nodes
(see Figure 1), and

      2. ii.

Push down $-\Box,-{\boxdot},+\neg,-\lor,-\to$ by distributing them over nodes
labelled with $-\land$ which are Skeleton nodes (see Figure 2).

$+\Diamond$$+\lor$$+\alpha$$+\beta$

$\Rightarrow$

$+\lor$$+\Diamond$$+\alpha$$+\Diamond$$+\beta$

$-\neg$$+\lor$$+\alpha$$+\beta$

$\Rightarrow$

$-\land$$-\neg$$+\alpha$$-\neg$$+\beta$

$+\land$$+\lor$$+\alpha$$+\beta$+$\gamma$

$\ \ \ \ \ \ \ \ \Rightarrow$

$+\lor$$+\land$$+\alpha$$+\gamma$$+\land$$+\beta$$+\gamma$

$+\land$+$\alpha$$+\lor$$+\beta$$+\gamma$

$\ \ \ \ \ \ \ \ \Rightarrow$

$+\lor$$+\land$$+\alpha$$+\beta$$+\land$$+\alpha$$+\gamma$

$+{{\Diamond}\\!\\!\\!\cdot\ }$$+\lor$$+\alpha$$+\beta$

$\Rightarrow$

$+\lor$$+{{\Diamond}\\!\\!\\!\cdot\ }$$+\alpha$$+{{\Diamond}\\!\\!\\!\cdot\
}$$+\beta$

$-\to$$+\lor$$+\alpha$$+\beta$$-\gamma$

$\ \ \ \ \ \ \ \ \Rightarrow$

$-\land$$-\to$$+\alpha$$-\gamma$$-\to$$+\beta$$-\gamma$

Figure 1: Distribution rules for $+\lor$

$-\Box$$-\land$$-\alpha$$-\beta$

$\ \ \ \ \ \ \ \ \Rightarrow$

$-\land$$-\Box$$-\alpha$$-\Box$$-\beta$

$+\neg$$-\land$$-\alpha$$-\beta$

$\Rightarrow$

$+\lor$$+\neg$$-\alpha$$+\neg$$-\beta$

$-\lor$$-\land$$-\alpha$$-\beta$$-\gamma$

$\Rightarrow$

$-\land$$-\lor$$-\alpha$$-\gamma$$-\lor$$-\beta$$-\gamma$

$-\lor$$-\alpha$$-\land$$-\beta$$-\gamma$

$\Rightarrow$

$-\land$$-\lor$$-\alpha$$-\beta$$-\lor$$-\alpha$$-\gamma$

$-{\boxdot}$$-\land$$-\alpha$$-\beta$

$\ \ \ \ \ \ \ \ \Rightarrow$

$-\land$$-{\boxdot}$$-\alpha$$-{\boxdot}$$-\beta$

$-\to$+$\alpha$$-\land$$-\beta$$-\gamma$

$\Rightarrow$

$-\land$$-\to$$+\alpha$$-\beta$$-\to$$+\alpha$$-\gamma$

Figure 2: Distribution rules for $-\land$

    2. (b)

Apply the splitting rules to each inequality occurring in the quasi-
inequality:

$\theta\leq\eta\ \&\
\theta\leq\iota\theta\leq\eta\land\iota\qquad\theta\leq\iota\ \&\
\eta\leq\iota\theta\lor\eta\leq\iota$

$\theta\prec\eta\ \&\
\theta\prec\iota\theta\prec\eta\land\iota\qquad\theta\prec\iota\ \&\
\eta\prec\iota\theta\lor\eta\prec\iota$

    3. (c)

Apply the monotone and antitone variable-elimination rules to the whole quasi-
inequality:

$\overline{\varphi}(\bot)\leq\overline{\psi}(\bot)\ \&\
\overline{\gamma}(\bot)\prec\overline{\delta}(\bot)\ \Rightarrow\
\overline{\alpha}(\bot)\leq\overline{\beta}(\bot)\ \&\
\overline{\xi}(\bot)\prec\overline{\chi}(\bot)\overline{\varphi}(p)\leq\overline{\psi}(p)\
\&\ \overline{\gamma}(p)\prec\overline{\delta}(p)\ \Rightarrow\
\overline{\alpha}(p)\leq\overline{\beta}(p)\ \&\
\overline{\xi}(p)\prec\overline{\chi}(p)$

if $p$ is positive in
$\overline{\varphi},\overline{\gamma},\overline{\beta},\overline{\chi}$ and
negative in
$\overline{\psi},\overline{\delta},\overline{\alpha},\overline{\xi}$;

$\overline{\varphi}(\top)\leq\overline{\psi}(\top)\ \&\
\overline{\gamma}(\top)\prec\overline{\delta}(\top)\ \Rightarrow\
\overline{\alpha}(\top)\leq\overline{\beta}(\top)\ \&\
\overline{\xi}(\top)\prec\overline{\chi}(\top)\overline{\varphi}(p)\leq\overline{\psi}(p)\
\&\ \overline{\gamma}(p)\prec\overline{\delta}(p)\ \Rightarrow\
\overline{\alpha}(p)\leq\overline{\beta}(p)\ \&\
\overline{\xi}(p)\prec\overline{\chi}(p)$

if $p$ is negative in
$\overline{\varphi},\overline{\gamma},\overline{\beta},\overline{\chi}$ and
positive in
$\overline{\psi},\overline{\delta},\overline{\alpha},\overline{\xi}$;

    4. (d)

Apply the subordination rewritting rule to each inequality with $\prec$ in
order to turn it into $\leq$:

${{\Diamond}\\!\\!\\!\cdot\ }\theta\leq\eta\theta\prec\eta$

Now we have a quasi-inequality of the form

$\overline{\varphi}\leq\overline{\psi}\ \Rightarrow\
\overline{\alpha}\leq\overline{\beta},$

which we split into a meta-conjunction of quasi-inequalities

$\overline{\varphi}\leq\overline{\psi}\ \Rightarrow\ \alpha\leq\beta,$

where $\alpha\leq\beta$ belong to $\overline{\alpha}\leq\overline{\beta}$.

We denote Preprocess:=$\\{\overline{\varphi}\leq\overline{\psi}\ \Rightarrow\
\alpha\leq\beta:\alpha\leq\beta\mbox{ belong to
}\overline{\alpha}\leq\overline{\beta}\\}$.

Now for each quasi-inequality in Preprocess, we apply the following first-
approximation rule:

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

Now for each quasi-inequality, we focus on the set of its antecedent
inequalities
$\\{\overline{\varphi}\leq\overline{\psi},\mathbf{i}_{0}\leq\alpha,\beta\leq\neg\mathbf{i}_{1}\\}$,
which we call a _system_.

  2. 2.

The reduction-elimination cycle:

In this stage, for each
$\\{\overline{\varphi}\leq\overline{\psi},\mathbf{i}_{0}\leq\alpha,\beta\leq\neg\mathbf{i}_{1}\\}$,
we apply the following rules together with the splitting rules in the previous
stage to eliminate all the propositional variables in the set of inequalities:

    1. (a)

Residuation rules:

$\Diamond\theta\leq\iota$ ($\Diamond$-Res) $\theta\leq\blacksquare\iota$
$\neg\theta\leq\iota$ ($\neg$-Res-Left) $\neg\iota\leq\theta$

$\theta\leq\Box\iota$ ($\Box$-Res) $\Diamondblack\theta\leq\iota$
$\theta\leq\neg\iota$ ($\neg$-Res-Right) $\iota\leq\neg\theta$

$\theta\land\iota\leq\eta$ ($\land$-Res-1) $\theta\leq\iota\to\eta$
$\theta\leq\iota\lor\eta$ ($\lor$-Res-1) $\theta\land\neg\iota\leq\eta$

$\theta\land\iota\leq\eta$ ($\land$-Res-2) $\iota\leq\theta\to\eta$
$\theta\leq\iota\lor\eta$ ($\lor$-Res-2) $\theta\land\neg\eta\leq\iota$

$\theta\leq\iota\to\eta$ ($\to$-Res-1) $\theta\land\iota\leq\eta$
$\theta\leq\iota\to\eta$ ($\to$-Res-2) $\iota\leq\theta\to\eta$

${{\Diamond}\\!\\!\\!\cdot\ }\theta\leq\iota$ (${{\Diamond}\\!\\!\\!\cdot\
}$-Res)
$\theta\leq{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}\iota$ $\theta\leq{\boxdot}\iota$ (${\boxdot}$-Res)
${\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}\theta\leq\iota$

    2. (b)

Approximation rules:

$\mathbf{j}\leq\theta\ \ \
\mathbf{i}\leq\Diamond\mathbf{j}\mathbf{i}\leq\Diamond\theta\qquad\theta\leq\neg\mathbf{j}\
\ \ \Box\neg\mathbf{j}\leq\neg\mathbf{i}\Box\theta\leq\neg\mathbf{i}$
$\mathbf{j}\leq\theta\ \ \ \mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\
}\mathbf{j}\mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\
}\theta\qquad\theta\leq\neg\mathbf{j}\ \ \
{\boxdot}\neg\mathbf{j}\leq\neg\mathbf{i}{\boxdot}\theta\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)

The Ackermann rules. These two rules are the core of $\mathsf{ALBA}$, since
their application eliminates propositional variables. In fact, all the
preceding steps are aimed at reaching a shape in which the rules can be
applied. Notice that an important feature of these rules is that they are
executed on the whole set of inequalities, and not on a single inequality.

The right-handed Ackermann rule:

The system $\left\\{\begin{array}[]{ll}\theta_{1}\leq p\\\ \vdots\\\
\theta_{n}\leq p\\\ \eta_{1}\leq\iota_{1}\\\ \vdots\\\
\eta_{m}\leq\iota_{m}\\\ \end{array}\right.$ is replaced by
$\left\\{\begin{array}[]{ll}\eta_{1}((\theta_{1}\lor\ldots\lor\theta_{n})/p)\leq\iota_{1}((\theta_{1}\lor\ldots\lor\theta_{n})/p)\\\
\vdots\\\
\eta_{m}((\theta_{1}\lor\ldots\lor\theta_{n})/p)\leq\iota_{m}((\theta_{1}\lor\ldots\lor\theta_{n})/p)\\\
\end{array}\right.$ 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
i\leq m$.

The left-handed Ackermann rule:

The system $\left\\{\begin{array}[]{ll}p\leq\theta_{1}\\\ \vdots\\\
p\leq\theta_{n}\\\ \eta_{1}\leq\iota_{1}\\\ \vdots\\\ \eta_{m}\leq\iota_{m}\\\
\end{array}\right.$ is replaced by
$\left\\{\begin{array}[]{ll}\eta_{1}((\theta_{1}\land\ldots\land\theta_{n})/p)\leq\iota_{1}((\theta_{1}\land\ldots\land\theta_{n})/p)\\\
\vdots\\\
\eta_{m}((\theta_{1}\land\ldots\land\theta_{n})/p)\leq\iota_{m}((\theta_{1}\land\ldots\land\theta_{n})/p)\\\
\end{array}\right.$ 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
i\leq m$.

  3. 3.

Output: If in the previous stage, for some set of inequalities, the algorithm
gets stuck, i.e. some propositional variables cannot be eliminated by the
application of the reduction rules, then the algorithm halts and output
“failure”. Otherwise, each initial set of inequalities after the first
approximation has been reduced to a set of pure inequalities
Reduce$(\overline{\varphi}\leq\overline{\psi},\mathbf{i}_{0}\leq\alpha,\beta\leq\neg\mathbf{i}_{1})$,
and then the output is a set of quasi-inequalities
$\\{\&$Reduce$(\overline{\varphi}\leq\overline{\psi},\mathbf{i}_{0}\leq\alpha,\beta\leq\neg\mathbf{i}_{1})\Rightarrow\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}\mid\overline{\varphi}\leq\overline{\psi}\
\Rightarrow\ \alpha\leq\beta\in$Preprocess$\\}$. Then we can use the standard
translation of the set of quasi-inequalities to obtain the first-order
correspondence.

##  7 Soundness

In this section we show the soundness of the algorithm with respect to the
arbitrary valuations. The soundness proof follows the style of [11]. For some
of the rules, the soundness proofs are the same to existing literature and
hence are omitted, so we only give details for the proofs which are different.

######  Theorem 7.1 (Soundness).

If $\mathsf{ALBA}$ runs successfully on an input quasi-inequality
$\mathsf{Quasi}$ and outputs a first-order formula $\mathsf{FO(Quasi)}$, then
for any Stone space with two relations $(X,\tau,R,R^{\prime})$,

$X\Vdash_{P}\mathsf{Quasi}\mbox{ iff }X\vDash\mathsf{FO(Quasi)}.$

###### Proof.

The proof goes similarly to [11, Theorem 8.1]. Let

$\overline{\varphi}\leq\overline{\psi}\ \Rightarrow\ \alpha\triangleleft\beta$

denote the input quasi-inequality $\mathsf{Quasi}$, let

$\overline{\varphi}_{i}\leq\overline{\psi}_{i}\ \Rightarrow\
\alpha_{i}\leq\beta_{i},i\in I$

denote the quasi-inequalities before the first-approximation rule, let

$\overline{\varphi}_{i}\leq\overline{\psi}_{i}\ \&\
\mathbf{i}_{i,0}\leq\alpha_{i}\ \&\
\beta_{i}\leq\neg\mathbf{i}_{i,1}\Rightarrow\mathbf{i}_{i,0}\leq\neg\mathbf{i}_{i,1},i\in
I$

denote the quasi-inequalities after the first-approximation rule, let

$\mbox{Reduce}(\overline{\varphi}_{i}\leq\overline{\psi}_{i},\mathbf{i}_{i,0}\leq\alpha,\beta\leq\neg\mathbf{i}_{i,1}),i\in
I$

denote the sets of inequalities after Stage 2, let

$\mathsf{FO(Quasi)}$

denote the standard translation of the quasi-inequalities into first-order
formulas, then it suffices to show the equivalence from (1) to (5) given
below:

$\displaystyle X\Vdash_{P}\overline{\varphi}\leq\overline{\psi}\ \Rightarrow\
\alpha\triangleleft\beta$ (1) $\displaystyle
X\Vdash_{P}\overline{\varphi}_{i}\leq\overline{\psi}_{i}\ \Rightarrow\
\alpha_{i}\leq\beta_{i},\mbox{ for all }i\in I$ (2) $\displaystyle
X\Vdash_{P}\overline{\varphi}_{i}\leq\overline{\psi}_{i}\ \&\
\mathbf{i}_{i,0}\leq\alpha_{i}\ \&\
\beta_{i}\leq\neg\mathbf{i}_{i,1}\Rightarrow\mathbf{i}_{i,0}\leq\neg\mathbf{i}_{i,1},i\in
I$ (3) $\displaystyle
X\Vdash_{P}\mbox{Reduce}(\overline{\varphi}_{i}\leq\overline{\psi}_{i},\mathbf{i}_{i,0}\leq\alpha,\beta\leq\neg\mathbf{i}_{i,1})\
\Rightarrow\ \mathbf{i}_{i,0}\leq\neg\mathbf{i}_{i,1},i\in I$ (4)
$\displaystyle X\vDash\mathsf{FO(Quasi)}$ (5)

  * •

The equivalence between (1) and (2) follows from Proposition 33;

  * •

the equivalence between (2) and (3) follows from Proposition 34;

  * •

the equivalence between (3) and (4) follows from Propositions 35, 36;

  * •

the equivalence between (4) and (5) follows from Proposition 24.

∎

In the remainder of this section, we prove the soundness of the rules in Stage
1, 2 and 3.

######  Proposition 33 (Soundness of the rules in Stage 1).

For the distribution rules, the splitting rules, the monotone and antitone
variable-elimination rules and the subordination rewritting rule, they are
sound in both directions in $X$.

###### Proof.

  1. 1.

For the soundness of the distribution rules, it follows from the fact that the
corresponding distribution laws are valid in $X$, which can be found in [27,
Proposition 6.2].

  2. 2.

For the soundness of the splitting rules, the rules involving $\leq$ are the
same to the same rules in [27, Proposition 6.2]. For the rules involving
$\prec$, it follows from the following fact:

| $X,V\Vdash\theta\prec\eta\land\iota$
---|---
iff | $R[V(\theta)]\subseteq V(\eta\land\iota)$
iff | $R[V(\theta)]\subseteq V(\eta)\cap V(\iota)$
iff |  $R[V(\theta)]\subseteq V(\eta)$ and $R[V(\theta)]\subseteq V(\iota)$
iff |  $X,V\Vdash\theta\prec\eta$ and $X,V\Vdash\theta\prec\iota$.
| $X,V\Vdash\theta\lor\eta\prec\iota$
---|---
iff | $R[V(\theta)\cup V(\eta)]\subseteq V(\iota)$
iff | $R[V(\theta)]\cup R[V(\eta)]\subseteq V(\iota)$
iff |  $R[V(\theta)]\subseteq V(\iota)$ and $R[V(\eta)]\subseteq V(\iota)$
iff |  $X,V\Vdash\theta\prec\iota$ and $X,V\Vdash\eta\prec\iota.$

  3. 3.

For the soundness of the monotone and antitone variable elimination rules, we
show the soundness for the first rule. Suppose $p$ is positive in
$\overline{\varphi},\overline{\gamma},\overline{\beta},\overline{\chi}$ and
negative in
$\overline{\psi},\overline{\delta},\overline{\alpha},\overline{\xi}$.

$(\Downarrow)$: If

$X\Vdash_{P}\overline{\varphi}(p)\leq\overline{\psi}(p)\ \&\
\overline{\gamma}(p)\prec\overline{\delta}(p)\ \Rightarrow\
\overline{\alpha}(p)\leq\overline{\beta}(p)\ \&\
\overline{\xi}(p)\prec\overline{\chi}(p),$

then for all valuations $V$, we have

$X,V\Vdash\overline{\varphi}(p)\leq\overline{\psi}(p)\ \&\
\overline{\gamma}(p)\prec\overline{\delta}(p)\ \Rightarrow\
\overline{\alpha}(p)\leq\overline{\beta}(p)\ \&\
\overline{\xi}(p)\prec\overline{\chi}(p),$

then for the valuation $V^{p}_{\varnothing}$ such that $V^{p}_{\varnothing}$
is the same as $V$ except that $V^{p}_{\varnothing}(p)=\varnothing$,

$X,V^{p}_{\varnothing}\Vdash\overline{\varphi}(p)\leq\overline{\psi}(p)\ \&\
\overline{\gamma}(p)\prec\overline{\delta}(p)\ \Rightarrow\
\overline{\alpha}(p)\leq\overline{\beta}(p)\ \&\
\overline{\xi}(p)\prec\overline{\chi}(p),$

therefore

$X,V\Vdash\overline{\varphi}(\bot)\leq\overline{\psi}(\bot)\ \&\
\overline{\gamma}(\bot)\prec\overline{\delta}(\bot)\ \Rightarrow\
\overline{\alpha}(\bot)\leq\overline{\beta}(\bot)\ \&\
\overline{\xi}(\bot)\prec\overline{\chi}(\bot),$

so

$X\Vdash_{P}\overline{\varphi}(\bot)\leq\overline{\psi}(\bot)\ \&\
\overline{\gamma}(\bot)\prec\overline{\delta}(\bot)\ \Rightarrow\
\overline{\alpha}(\bot)\leq\overline{\beta}(\bot)\ \&\
\overline{\xi}(\bot)\prec\overline{\chi}(\bot).$

$(\Uparrow)$: For the other direction, consider any valuation $V$ on $X$, by
the fact that $p$ is positive in
$\overline{\varphi},\overline{\gamma},\overline{\beta},\overline{\chi}$ and
negative in
$\overline{\psi},\overline{\delta},\overline{\alpha},\overline{\xi}$, we have
that

$X,V\vDash\overline{\psi}(p)\leq\overline{\psi}(\bot)$
$X,V\vDash\overline{\delta}(p)\leq\overline{\delta}(\bot)$
$X,V\vDash\overline{\alpha}(p)\leq\overline{\alpha}(\bot)$
$X,V\vDash\overline{\xi}(p)\leq\overline{\xi}(\bot),$

and

$X,V\vDash\overline{\varphi}(\bot)\leq\overline{\varphi}(p)$
$X,V\vDash\overline{\gamma}(\bot)\leq\overline{\gamma}(p)$
$X,V\vDash\overline{\beta}(\bot)\leq\overline{\beta}(p)$
$X,V\vDash\overline{\chi}(\bot)\leq\overline{\chi}(p).$

Suppose that

$X,V\Vdash\overline{\varphi}(p)\leq\overline{\psi}(p)\ \&\
\overline{\gamma}(p)\prec\overline{\delta}(p),$

then

$X,V\Vdash\overline{\varphi}(\bot)\leq\overline{\varphi}(p)\leq\overline{\psi}(p)\leq\overline{\psi}(\bot)\
\&\
\overline{\gamma}(\bot)\leq\overline{\gamma}(p)\prec\overline{\delta}(p)\leq\overline{\delta}(\bot),$

so

$X,V\Vdash\overline{\varphi}(\bot)\leq\overline{\psi}(\bot)\ \&\
\overline{\gamma}(\bot)\prec\overline{\delta}(\bot),$

therefore by assumption that

$X\Vdash_{P}\overline{\varphi}(\bot)\leq\overline{\psi}(\bot)\ \&\
\overline{\gamma}(\bot)\prec\overline{\delta}(\bot)\ \Rightarrow\
\overline{\alpha}(\bot)\leq\overline{\beta}(\bot)\ \&\
\overline{\xi}(\bot)\prec\overline{\chi}(\bot),$

we have

$X,V\Vdash\overline{\alpha}(\bot)\leq\overline{\beta}(\bot)\ \&\
\overline{\xi}(\bot)\prec\overline{\chi}(\bot),$

so

$X,V\Vdash\overline{\alpha}(p)\leq\overline{\alpha}(\bot)\leq\overline{\beta}(\bot)\leq\overline{\beta}(p)\
\&\
\overline{\xi}(p)\leq\overline{\xi}(\bot)\prec\overline{\chi}(\bot)\leq\overline{\chi}(p),$

then

$X,V\Vdash\overline{\alpha}(p)\leq\overline{\beta}(p)\ \&\
\overline{\xi}(p)\prec\overline{\chi}(p),$

so we get that for all $V$,

$X,V\Vdash\overline{\varphi}(p)\leq\overline{\psi}(p)\ \&\
\overline{\gamma}(p)\prec\overline{\delta}(p)\ \Rightarrow\
\overline{\alpha}(p)\leq\overline{\beta}(p)\ \&\
\overline{\xi}(p)\prec\overline{\chi}(p),$

so

$X\Vdash_{P}\overline{\varphi}(p)\leq\overline{\psi}(p)\ \&\
\overline{\gamma}(p)\prec\overline{\delta}(p)\ \Rightarrow\
\overline{\alpha}(p)\leq\overline{\beta}(p)\ \&\
\overline{\xi}(p)\prec\overline{\chi}(p).$

The soundness of the other variable elimination rule is similar.

  4. 4.

For the subordination rewritting rule, its soundness follows from the
following fact:

| $X,V\Vdash\theta\prec\eta$
---|---
iff | $R[V(\theta)]\subseteq V(\eta)$
iff | $V({{\Diamond}\\!\\!\\!\cdot\ }\theta)\subseteq V(\eta)$
iff |  $X,V\Vdash{{\Diamond}\\!\\!\\!\cdot\ }\theta\leq\eta$.

∎

######  Proposition 34.

(2) and (3) are equivalent, i.e. the first-approximation rule is sound in
$\mathbb{F}$.

###### Proof.

(2) $\Rightarrow$ (3): Suppose
$X\Vdash_{P}\overline{\varphi}\leq\overline{\psi}\ \Rightarrow\
\alpha\leq\beta$. Then for any valuation $V$, if
$V(\overline{\varphi})\subseteq V(\overline{\psi})$,
$X,V\Vdash\mathbf{i}_{0}\leq\alpha$ and
$X,V\Vdash\beta\leq\neg\mathbf{i}_{1}$, then
$X,V,V(\mathbf{i}_{0})\Vdash\alpha$ and $X,V,V(\mathbf{i}_{1})\nVdash\beta$,
so by $X\Vdash_{P}\overline{\varphi}\leq\overline{\psi}\ \Rightarrow\
\alpha\leq\beta$ we have $X,V,V(\mathbf{i}_{0})\Vdash\beta$, so
$V(\mathbf{i}_{0})\neq V(\mathbf{i}_{1})$, so
$X,V\Vdash\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$.

(3) $\Rightarrow$ (2): Suppose
$X\Vdash_{P}\overline{\varphi}\leq\overline{\psi}\ \&\
\mathbf{i}_{0}\leq\alpha\ \&\ \beta\leq\neg\mathbf{i}_{1}\Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$. If
$X\nVdash_{P}\overline{\varphi}\leq\overline{\psi}\ \Rightarrow\
\alpha\leq\beta$, there is a valuation $V$ and a $w\in X$ such that
$V(\overline{\varphi})\subseteq V(\overline{\psi})$, $X,V,w\Vdash\alpha$ and
$X,V,w\nVdash\beta$. Then by taking $V^{\mathbf{i}_{0},\mathbf{i}_{1}}_{w,w}$
to be the valuation which is the same as $V$ except that
$V^{\mathbf{i}_{0},\mathbf{i}_{1}}_{w,w}(\mathbf{i}_{0})=V^{\mathbf{i}_{0},\mathbf{i}_{1}}_{w,w}(\mathbf{i}_{1})=\\{w\\}$,
since $\mathbf{i}_{0},\mathbf{i}_{1}$ do not occur in $\alpha$ and $\beta$, we
have that $X,V^{\mathbf{i}_{0},\mathbf{i}_{1}}_{w,w},w\Vdash\alpha$ and
$X,V^{\mathbf{i}_{0}\mathbf{i}_{1}}_{w,w},w\nVdash\beta$, therefore
$X,V^{\mathbf{i}_{0},\mathbf{i}_{1}}_{w,w}\Vdash\mathbf{i}_{0}\leq\alpha$ and
$X,V^{\mathbf{i}_{0},\mathbf{i}_{1}}_{w,w}\Vdash\beta\leq\neg\mathbf{i}_{1}$.
It is easy to see that
$V^{\mathbf{i}_{0},\mathbf{i}_{1}}_{w,w}(\overline{\varphi})\subseteq
V^{\mathbf{i}_{0},\mathbf{i}_{1}}_{w,w}(\overline{\psi})$. By
$X\Vdash_{P}\overline{\varphi}\leq\overline{\psi}\ \&\
\mathbf{i}_{0}\leq\alpha\ \&\ \beta\leq\neg\mathbf{i}_{1}\Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$, we have that
$X,V^{\mathbf{i}_{0},\mathbf{i}_{1}}_{w,w}\Vdash\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$,
so $X,V^{\mathbf{i}_{0},\mathbf{i}_{1}}_{w,w},w\Vdash\mathbf{i}_{0}$ implies
that $X,V^{\mathbf{i}_{0},\mathbf{i}_{1}}_{w,w},w\Vdash\neg\mathbf{i}_{1}$, a
contradiction. So $X\Vdash_{P}\overline{\varphi}\leq\overline{\psi}\
\Rightarrow\ \alpha\leq\beta$. ∎

The next step is to show the soundness of each rule of Stage 2. For each rule,
before the application of this rule we have a set of inequalities $S$ (which
we call the _system_), after applying the rule we get a set of inequalities
$S^{\prime}$, the soundness of Stage 2 is then the equivalence of the
following two conditions:

  * •

$X\Vdash_{P}\mathop{\mbox{\Large\&}}S\
\Rightarrow\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$;

  * •

$X\Vdash_{P}\mathop{\mbox{\Large\&}}S^{\prime}\
\Rightarrow\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$;

where $\mathop{\mbox{\Large\&}}S$ denote the meta-conjunction of inequalities
of $S$. It suffices to show the following property:

  * •

For any $X$, any valuation $V$, if $X,V\Vdash S$, then there is a valuation
$V^{\prime}$ such that $V^{\prime}(\mathbf{i}_{0})=V(\mathbf{i}_{0})$,
$V^{\prime}(\mathbf{i}_{1})=V(\mathbf{i}_{1})$ and $X,V^{\prime}\Vdash
S^{\prime}$;

  * •

For any $X$, any valuation $V^{\prime}$, if $X,V^{\prime}\Vdash S^{\prime}$,
then there is a valuation $V$ such that
$V(\mathbf{i}_{0})=V^{\prime}(\mathbf{i}_{0})$,
$V(\mathbf{i}_{1})=V^{\prime}(\mathbf{i}_{1})$ and $X,V\Vdash S$.

######  Proposition 35.

The splitting rules, the approximation rules and the residuation rules in
Stage 2 are sound in both directions in $X$.

###### Proof.

The soundness proofs are the same to the soundness of the same rules in [27,
Proposition 6.4-Lemma 6.8, Lemma 6.11-6.12]. ∎

######  Proposition 36.

The Ackermann rules are sound in $X$.

###### Proof.

The proof is similar to the soundness of the Ackermann rules in [11, Lemma
4.2, 4.3, 8.4]. We only prove it for the right-handed Ackermann rule, the
left-handed Ackermann rule is similar. Without loss of generality we assume
that $n=1$. By the discussion on page 7, it suffices to show the following
_right-handed Ackermann lemma_ :

######  Lemma 37 (Right-Handed Ackermann Lemma).

Let $\theta$ be a formula which does not contain $p$, let $\eta_{i}(p)$ (resp.
$\iota_{i}(p)$) be positive (resp. negative) in $p$ for $1\leq i\leq m$, and
let $\vec{q}$ (resp. $\vec{\mathbf{j}}$) be all the propositional variables
(resp. nominals) occurring in $\eta_{1}(p),\ldots,\eta_{m}(p)$,
$\iota_{1}(p),\ldots,\iota_{m}(p),\theta$ other than $p$. Then for all
$\vec{a}\in P(X),\vec{x}\in X$, the following are equivalent:

  1. 1.

$V(\eta_{i}(\theta/p))\subseteq V(\iota_{i}(\theta/p))$ for $1\leq i\leq m$,
where $V(\vec{q})=\vec{a}$, $V(\vec{\mathbf{j}})=\vec{\\{x\\}}$,

  2. 2.

there exists $a_{0}\in P(X)$ such that $V^{\prime}(\theta)\leq a_{0}$ and
$V^{\prime}(\eta_{i}(p))\subseteq V^{\prime}(\iota_{i}(p))$ for $1\leq i\leq
m$, where $V^{\prime}$ is the same as $V$ except that $V^{\prime}(p)=a_{0}$.

$\Rightarrow$: Take $V^{\prime}$ such that $V^{\prime}$ is the same as $V$
except that $V^{\prime}(p)=V(\theta)$. Since $\theta$ does not contain $p$, it
is easy to see that $V(\theta)=V^{\prime}(\theta)$. Therefore we can take
$a_{0}:=V(\theta)$ and get 2.

$\Leftarrow$: It is obvious by monotonicity. ∎

##  8 Success

In this section, we show the success of the algorithm on inductive quasi-
inequalities. Notice that here we do not allow the input quasi-inequality to
contain any black connectives
$\Diamondblack,\blacksquare,{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}},{\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$, but we allow ${{\Diamond}\\!\\!\\!\cdot\ }$ and ${\boxdot}$ to occur in
the input quasi-inequality.

######  Definition 38 (Definite $(\Omega,\varepsilon)$-inductive signed
generation tree).

Given a dependence order $<_{\Omega}$, an order type $\varepsilon$,
$*\in\\{-,+\\}$, the signed generation tree $*\theta$ of the formula
$\theta(p_{1},\ldots,p_{n})$ is _definite $(\Omega,\varepsilon)$-inductive_ if
there is no $+\lor,-\land$ occurring in the Skeleton part on an
$\varepsilon$-critical branch.

######  Lemma 39.

Given an input $(\Omega,\varepsilon)$-inductive quasi-inequality

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{\gamma}\prec\overline{\delta}\ \Rightarrow\
\alpha\triangleleft\beta\mbox{ (where }\triangleleft\in\\{\leq,\prec\\}),$

after the first stage, it is transformed into a quasi-inequality of the form

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\gamma}\leq\overline{\delta}\
\Rightarrow\ \overline{\alpha}\leq\overline{\beta}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\xi}\leq\overline{\chi},$

and further of the form

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\gamma}\leq\overline{\delta}\
\Rightarrow\ \alpha\leq\beta$

or

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\gamma}\leq\overline{\delta}\
\Rightarrow\ {{\Diamond}\\!\\!\\!\cdot\ }\xi\leq\chi,$

where

  * •

each $\varphi\leq\psi$ or ${{\Diamond}\\!\\!\\!\cdot\ }\gamma\leq\delta$ is
either $(\Omega,\varepsilon)$-receiving or $(\Omega,\varepsilon)$-solvable;

  * •

$+\alpha$ and $-\beta$ (resp. $+{{\Diamond}\\!\\!\\!\cdot\ }\xi$ and $-\chi$)
are definite $(\Omega,\varepsilon)$-inductive signed generation trees;

  * •

each formula contains no black connectives.

###### Proof.

It is easy to see that by applying the distribution rules, in each inequality
$\theta\leq\eta$ or $\theta\prec\eta$, consider the signed generation trees
$+\theta$ and $-\eta$, all occurrences of $+\lor$ and $-\land$ in the Skeleton
part of an $\varepsilon$-critical branch have been pushed up towards the root
of the signed generation trees $+\theta$ and $-\eta$. Then by exhaustively
applying the splitting rules, all such $+\lor$ and $-\land$ are eliminated.

Since by applying the distribution rules, the splitting rules and the
monotone/antitone variable elimination rules do not change the
$(\Omega,\varepsilon)$-inductiveness of a signed generation tree for
$+\alpha$, $-\beta$ (resp. $+\xi$, $-\chi$), and do not change the property of
being $(\Omega,\varepsilon)$-receiving or $(\Omega,\varepsilon)$-solvable for
$\varphi\leq\psi$ or $\gamma\prec\delta$, so in

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\gamma}\leq\overline{\delta}\
\Rightarrow\ \overline{\alpha}\leq\overline{\beta}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\xi}\leq\overline{\chi},$

  * •

each $\varphi\leq\psi$ or ${{\Diamond}\\!\\!\\!\cdot\ }\gamma\leq\delta$ is
either $(\Omega,\varepsilon)$-receiving or $(\Omega,\varepsilon)$-solvable;

  * •

each pair of $+\alpha$ and $-\beta$ (resp. $+{{\Diamond}\\!\\!\\!\cdot\ }\xi$
and $-\chi$) are definite $(\Omega,\varepsilon)$-inductive signed generation
trees.

It is easy to see that no formula contains black connectives since the input
quasi-inequality contains no black connective and no rule in Stage 1
introduces them. ∎

######  Lemma 40.

After first approximation, the input $(\Omega,\varepsilon)$-inductive
inequality

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{\gamma}\prec\overline{\delta}\ \Rightarrow\
\alpha\triangleleft\beta\mbox{ (where }\triangleleft\in\\{\leq,\prec\\})$

is rewritten into the form

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\gamma}\leq\overline{\delta}\ \&\
\mathbf{i}_{0}\leq\alpha\ \&\ \beta\leq\neg\mathbf{i}_{1}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$

or

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\gamma}\leq\overline{\delta}\ \&\
\mathbf{i}_{0}\leq{{\Diamond}\\!\\!\\!\cdot\ }\xi\ \&\
\chi\leq\neg\mathbf{i}_{1}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1},$

where

  * •

each $\varphi\leq\psi$ or ${{\Diamond}\\!\\!\\!\cdot\ }\gamma\leq\delta$ is
either $(\Omega,\varepsilon)$-receiving or $(\Omega,\varepsilon)$-solvable;

  * •

$+\alpha$ and $-\beta$ (resp. $+{{\Diamond}\\!\\!\\!\cdot\ }\xi$ and $-\chi$)
are definite $(\Omega,\varepsilon)$-inductive signed generation trees;

  * •

each formula contains no black connectives.

###### Proof.

Straightforward. ∎

Now we proceed to Stage 2 and work with set of inequalities (i.e. systems).

$\\{\overline{\varphi}\leq\overline{\psi},\overline{{{\Diamond}\\!\\!\\!\cdot\
}\gamma}\leq\overline{\delta},\mathbf{i}_{0}\leq\alpha,\beta\leq\neg\mathbf{i}_{1}\\}$

or

$\\{\overline{\varphi}\leq\overline{\psi},\overline{{{\Diamond}\\!\\!\\!\cdot\
}\gamma}\leq\overline{\delta},\mathbf{i}_{0}\leq{{\Diamond}\\!\\!\\!\cdot\
}\xi,\chi\leq\neg\mathbf{i}_{1}\\}.$

######  Lemma 41.

For each inequality $\mathbf{i}_{0}\leq\alpha$ or
$\beta\leq\neg\mathbf{i}_{1}$ (here we merge the
$\mathbf{i}_{0}\leq{{\Diamond}\\!\\!\\!\cdot\ }\xi$ case into the
$\mathbf{i}_{0}\leq\alpha$ case, and merge the $\chi\leq\neg\mathbf{i}_{1}$
case into the $\beta\leq\neg\mathbf{i}_{1}$ case), by applying the
approximation rules, splitting rules and residuation rules involving $\neg$
exhaustively, we obtain a set of inequalities, each inequality of which
contains no black connectives and belong to one of the three classes:

  * •

it is pure;

  * •

it is $(\Omega,\varepsilon)$-receiving;

  * •

it is of the form $\mathbf{i}\leq\alpha^{\prime}$ or
$\beta^{\prime}\leq\neg\mathbf{i}$, where $+\alpha^{\prime}$ and
$-\beta^{\prime}$ are $(\Omega,\varepsilon)$-inductive and their
$\varepsilon$-critical branches contain only PIA nodes.

###### Proof.

First of all, since the approximation rules, the splitting rules and the
residuation rules involving $\neg$ do not introduce black connectives and
$\alpha,\beta$ do not contain black connectives, so it is easy to see that the
obtained inequalities do not contain black connectives.

Then we prove by induction on the complexity of $+\alpha$ and $-\beta$ to show
that the obtained inequalities can be classified into three classes mentioned
above:

  * •

When $\alpha$ is $p$ and $\varepsilon(p)=1$, then it is obvious that $+p$ is
critical, $\mathbf{i}_{0}\leq\alpha$ belongs to the third class;

when $\alpha$ is $p$ and $\varepsilon(p)=\partial$, then it is obvious that
$+p$ is non-critical, $\mathbf{i}_{0}\leq\alpha$ belongs to the second class;

when $\beta$ is $p$ and $\varepsilon(p)=\partial$, then it is obvious that
$-p$ is critical, $\beta\leq\neg\mathbf{i}_{1}$ belongs to the third class;

when $\beta$ is $p$ and $\varepsilon(p)=1$, then it is obvious that $-p$ is
non-critical, $\beta\leq\neg\mathbf{i}_{1}$ belongs to the second class;

  * •

when $\alpha$ or $\beta$ is $\bot$ or $\top$, then it is already pure, so it
belongs to the first class;

  * •

when $\alpha$ is $\neg\theta$, then since $+\alpha$ is definite
$(\Omega,\varepsilon)$-inductive, $-\theta$ is also definite
$(\Omega,\varepsilon)$-inductive, we first apply ($\neg$-Res-Right) to
$\mathbf{i}_{0}\leq\neg\theta$ to obtain $\theta\leq\neg\mathbf{i}_{0}$, then
we can apply the induction hypothesis to obtain the result;

when $\beta$ is $\neg\theta$, the proof is similar;

  * •

when $\alpha$ is $\Diamond\theta$, then since $+\alpha$ is definite
$(\Omega,\varepsilon)$-inductive, $+\theta$ is also definite
$(\Omega,\varepsilon)$-inductive, we first apply the approximation rule for
$\Diamond$ to $\mathbf{i}_{0}\leq\Diamond\theta$ obtain
$\mathbf{i}_{0}\leq\Diamond\mathbf{j}$ and $\mathbf{j}\leq\theta$. Now the
first inequality belongs to the first class, and we can use the induction
hypothesis to the second inequality, so we obtain the result;

when $\alpha$ is ${{\Diamond}\\!\\!\\!\cdot\ }\theta$, $\beta$ is $\Box\theta$
or ${\boxdot}\theta$, the proof is similar;

  * •

when $\alpha$ is $\Box\theta$, then either $\alpha$ contains no critical
branch or its critical branch is already a PIA branch; in the first case,
$\mathbf{i}\leq\alpha$ is already in the second class; in the second case, it
is already in the third class;

when $\alpha$ is ${\boxdot}\theta$, $\beta$ is $\Diamond\theta$ or
${{\Diamond}\\!\\!\\!\cdot\ }\theta$, the proof is similar;

  * •

when $\alpha$ is $\theta\land\eta$, then since $+\alpha$ is definite
$(\Omega,\varepsilon)$-inductive, $+\theta,+\eta$ are also definite
$(\Omega,\varepsilon)$-inductive, we first apply the splitting rule for
$\land$ to $\mathbf{i}_{0}\leq\theta\land\eta$ to obtain
$\mathbf{i}_{0}\leq\theta$ and $\mathbf{i}_{0}\leq\eta$, and then we can use
the induction hypothesis to obtain the result;

when $\beta$ is $\theta\lor\eta$, the proof is similar;

  * •

when $\alpha$ is $\theta\lor\eta$, since $+\alpha$ is definite
$(\Omega,\varepsilon)$-inductive, either $\alpha$ contains no critical branch
(then $\mathbf{i}_{0}\leq\alpha$ belongs to the second class) or $+\lor$ is on
a critical branch. Since $\Delta$-adjoint $+\lor$s are already eliminated in
Stage 1, so $+\lor$ is an SRR node, so all aritical branches passing through
$+\lor$ are PIA branches, so $\mathbf{i}_{0}\leq\alpha$ belongs to the third
class;

when $\beta$ is $\theta\land\eta$, the proof is similar;

  * •

when $\alpha$ is $\theta\to\eta$, the proof is similar to the
$\alpha=\theta\lor\eta$ case;

  * •

when $\beta$ is $\theta\to\eta$, then since $-\beta$ is definite
$(\Omega,\varepsilon)$-inductive, $+\theta,-\eta$ are also definite
$(\Omega,\varepsilon)$-inductive, we first apply the approximation rule for
$\to$ to $\theta\to\eta\leq\neg\mathbf{i}_{1}$ to obtain
$\mathbf{i}\leq\theta$, $\eta\leq\neg\mathbf{j}$ and
$\mathbf{i}\to\neg\mathbf{j}\leq\neg\mathbf{i}_{1}$, then the last inequality
belongs to the first class, and we can apply the induction hypothesis to
$\mathbf{i}\leq\theta$ and $\eta\leq\neg\mathbf{j}$ obtain the result;

  * •

it is easy to see that $\alpha$ and $\beta$ cannot be of the form
$\Diamondblack\theta$,$\blacksquare\theta$,
${\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}\theta$ or
${\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}\theta$.

∎

######  Lemma 42.

For each $(\Omega,\varepsilon)$-solvable inequality $\varphi\leq\psi$ or
${{\Diamond}\\!\\!\\!\cdot\ }\gamma\leq\delta$, by applying the residuation
rules and splitting rules exhaustively, we obtain a set of inequalities, each
inequality of which belong to one of the three classes:

  * •

it is pure;

  * •

it is $(\Omega,\varepsilon)$-receiving;

  * •

it is of the form $\theta\leq p$ when $\varepsilon(p)=1$, or of the form
$p\leq\theta$ when $\varepsilon(p)=\partial$. In $\theta\leq p$, $-\theta$ is
$\varepsilon^{\partial}$-uniform, and in $p\leq\theta$, $+\theta$ is
$\varepsilon^{\partial}$-uniform. In addition, for all propositional variables
$q$ in $\theta$, we have $q<_{\Omega}p$.

###### Proof.

Since ${{\Diamond}\\!\\!\\!\cdot\ }\gamma\leq\delta$ is the special case of
$\varphi\leq\psi$ when the outermost connective of $\varphi$ is
${{\Diamond}\\!\\!\\!\cdot\ }$, we only consider $\varphi\leq\psi$ here.

Without loss of generality we consider the situation when

  * •

$-\varphi$ is $\varepsilon^{\partial}$-uniform;

  * •

$+\psi$ has $\varepsilon$-critical branches and is
$(\Omega,\varepsilon)$-inductive, and all $\varepsilon$-critical branches in
$+\psi$ are PIA branches;

  * •

for all the $\varepsilon$-critical branches in $+\psi$ ending with $p$, all
propositional variables $q$ in $-\varphi$, we have $q<_{\Omega}p$.

The situation where $+\psi$ is $\varepsilon^{\partial}$-uniform etc. is
symmetric.

We prove by induction on the complexity of $\psi$:

  * •

when $\psi$ is $p$: $\varphi\leq\psi$ belongs to the third class and
$\varepsilon(p)=1$;

  * •

when $\psi$ is $\bot$ or $\top$: it cannot be the case, since $+\psi$ contains
$\varepsilon$-critical branches;

  * •

when $\psi$ is $\neg\theta$: we can first apply the residuation rule for
$\neg$ to $\varphi\leq\neg\theta$ to obtain $\theta\leq\neg\varphi$, and then
we can apply the induction hypothesis for the case where

    * –

$+\neg\varphi$ is $\varepsilon^{\partial}$-uniform;

    * –

$-\theta$ has $\varepsilon$-critical branches and is
$(\Omega,\varepsilon)$-inductive, and all $\varepsilon$-critical branches in
$-\theta$ are PIA branches;

    * –

for all the $\varepsilon$-critical branches in $-\theta$ ending with $p$, all
propositional variables $q$ in $+\neg\varphi$, we have $q<_{\Omega}p$;

  * •

when $\psi$ is $\Diamond\theta$: it cannot be the case, since $\Diamond$ is on
an $\varepsilon$-critical branch in $+\psi$ but it is not a PIA node;

  * •

when $\psi$ is ${{\Diamond}\\!\\!\\!\cdot\ }\theta$: similar to the
$\Diamond\theta$ case;

  * •

when $\psi$ is $\Box\theta$: we can first apply the residuation rule for
$\Box$ to $\varphi\leq\Box\theta$ to obtain $\Diamondblack\varphi\leq\theta$,
and then we can apply the induction hypothesis for the case where

    * –

$-\Diamondblack\varphi$ is $\varepsilon^{\partial}$-uniform;

    * –

$+\theta$ has $\varepsilon$-critical branches and is
$(\Omega,\varepsilon)$-inductive, and all $\varepsilon$-critical branches in
$+\theta$ are PIA branches;

    * –

for all the $\varepsilon$-critical branches in $+\theta$ ending with $p$, all
propositional variables $q$ in $-\Diamondblack\varphi$, we have
$q<_{\Omega}p$;

  * •

when $\psi$ is ${\boxdot}\theta$, the situation is similar to the $\Box\theta$
case;

  * •

when $\psi$ is $\theta\land\eta$, we first apply the splitting rule for
$\land$ to $\varphi\leq\theta\land\eta$ to obtain $\varphi\leq\theta$ and
$\varphi\leq\eta$, then there are two possibilities, namely both of $+\theta$
and $+\eta$ have $\varepsilon$-critical branches, and only one of $+\theta$
and $+\eta$ has $\varepsilon$-critical branches;

for the first possibility, we can apply the induction hypothesis for the case
where

    * –

$-\varphi$ is $\varepsilon^{\partial}$-uniform;

    * –

$+\theta$ and $+\eta$ have $\varepsilon$-critical branches and are
$(\Omega,\varepsilon)$-inductive, and all $\varepsilon$-critical branches in
$+\theta$ and $+\eta$ are PIA branches;

    * –

for all the $\varepsilon$-critical branches in $+\theta$ and $+\eta$ ending
with $p$, all propositional variables $q$ in $-\varphi$, we have
$q<_{\Omega}p$;

for the second possibility, without loss of generality we assume that
$+\theta$ has $\varepsilon$-critical branches and $+\eta$ is
$\varepsilon^{\partial}$-uniform, then $\varphi\leq\eta$ is
$(\Omega,\varepsilon)$-receiving, and we can apply the induction hypothesis to
$\varphi\leq\theta$ for the case where

    * –

$-\varphi$ is $\varepsilon^{\partial}$-uniform;

    * –

$+\theta$ have $\varepsilon$-critical branches and are
$(\Omega,\varepsilon)$-inductive, and all $\varepsilon$-critical branches in
$+\theta$ are PIA branches;

    * –

for all the $\varepsilon$-critical branches in $+\theta$ ending with $p$, all
propositional variables $q$ in $-\varphi$, we have $q<_{\Omega}p$;

  * •

when $\psi$ is $\theta\lor\eta$: since $\lor$ is an SRR node, only one of
$\theta$ and $\eta$ contains $\varepsilon$-critical branches (without loss of
generality we assume that it is $\eta$). Then

    * –

$+\theta$ is $\varepsilon^{\partial}$-uniform;

    * –

for each $p$ in an $\varepsilon$-critical branch in $+\eta$, each $q$ that
occurs in $+\theta$, we have $q<_{\Omega}p$;

Now we apply the residuation rule for $\lor$ to $\varphi\leq\theta\lor\eta$ to
obtain $\varphi\land\neg\theta\leq\eta$, then we can apply the induction
hypothesis for the case where

    * –

$-(\varphi\land\neg\theta)$ is $\varepsilon^{\partial}$-uniform;

    * –

$+\eta$ has $\varepsilon$-critical branches and is
$(\Omega,\varepsilon)$-inductive, and all $\varepsilon$-critical branches in
$+\eta$ are PIA branches;

    * –

for all the $\varepsilon$-critical branches in $+\eta$ ending with $p$, all
propositional variables $q$ in $-(\varphi\land\neg\theta)$, we have
$q<_{\Omega}p$;

  * •

when $\psi$ is $\theta\to\eta$: the situation is similar to the
$\theta\lor\eta$ case (in the sense of using one of the residuation rules for
$\to$).

∎

######  Lemma 43.

Inequalities of the form $\mathbf{i}\leq\alpha^{\prime}$ or
$\beta^{\prime}\leq\neg\mathbf{i}$, where $+\alpha^{\prime}$ and
$-\beta^{\prime}$ are $(\Omega,\varepsilon)$-inductive and their
$\varepsilon$-critical branches contain only PIA nodes are
$(\Omega,\varepsilon)$-solvable, and therefore the previous lemma is
applicable to them.

###### Proof.

Straightforward. ∎

Now the set of inequalities have three kinds of inequalities, namely

  * •

pure inequalities;

  * •

$(\Omega,\varepsilon)$-receiving inequalities;

  * •

$\theta\leq p$ when $\varepsilon(p)=1$, or $p\leq\theta$ when
$\varepsilon(p)=\partial$. In $\theta\leq p$, $-\theta$ is
$\varepsilon^{\partial}$-uniform, and in $p\leq\theta$, $+\theta$ is
$\varepsilon^{\partial}$-uniform. In addition, for all propositional variables
$q$ in $\theta$, we have $q<_{\Omega}p$.

It is ready to repeatedly apply the Ackermann lemmas, and then all
propositional variables are eliminated. Since after the monotone/antitone
variable elimination rules in the first stage, each variable has both critical
branches and non-critical branches in the corresponding signed generation
trees, therefore in Stage 2, they have occurrences in both
$(\Omega,\varepsilon)$-receiving inequalities and inequalities of the form
$\theta\leq p$ or $p\leq\theta$, so they all can be eliminated.

######  Theorem 8.1 (Success Theorem).

For all $(\Omega,\varepsilon)$-inductive quasi-inequalities which do not
contain black connectives, $\mathsf{ALBA}$ successfully reduce them to pure
quasi-inequalities, and therefore can transform them into first-order
correspondents.

##  9 Canonicity

In the present section, we will prove that all inductive quasi-inequalities
which do not contain black connectives or ${{\Diamond}\\!\\!\\!\cdot\
},{\boxdot}$ (we call them _restricted inductive quasi-inequalities_) are
canonical, in the sense that if they are admissibly valid on a Stone space
with two relations, then they are valid on the same space. The proof style is
similar to [11].

######  Definition 44 (Restricted inductive quasi-inequality).

Given an order-type $\varepsilon$ and a dependence order $<_{\Omega}$, we say
that a quasi-inequality is $(\Omega,\varepsilon)$-restricted inductive, if it
is $(\Omega,\varepsilon)$-inductive and does not contain nominals,
${{\Diamond}\\!\\!\\!\cdot\ },{\boxdot}$ or black connectives
$\Diamondblack,\blacksquare,{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}},{\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$.

######  Definition 45 (Canonicity).

We say that a quasi-inequality is _canonical_ if whenever it is admissibly
valid on a Stone space with two relations, it is also valid on it.

By the duality theory of modal subordination algebras, the canonicity
definition above is equivalent to the preservation under taking canonical
extensions of modal subordination algebras.

###  9.1 U-Shaped Argument

To prove the canonicity of inductive quasi-inequalities, we use the
canonicity-via-correspondence argument, which is a variation of the standard
U-shaped argument (cf. [11]) represented in the diagram below. To go through
the U-shaped argument, we show that _topologically correct executions_ of
$\mathsf{ALBA}$ is sound with respect to the Stone spaces with two relations,
while we replace validity (with respect to arbitrary valuations) by admissible
validity (with respect to clopen/admissible valuations).

$X\Vdash_{Clop}\mathsf{Quasi}$ |  | $X\Vdash_{P}\mathsf{Quasi}$
---|---|---
$\Updownarrow$ |  |  $\Updownarrow$
$X\vDash\mathsf{FO(Quasi)}$ |  $\Leftrightarrow$ | $X\vDash\mathsf{FO(Quasi)}$

This argument starts from the top-left corner with the validity of the input
quasi-inequality $\mathsf{Quasi}$ on $X$, then uses topologically correct
executions of $\mathsf{ALBA}$ to transform the quasi-inequality into an
equivalent set of quasi-inequalities as well as its first-order translation
$\mathsf{FO(Quasi)}$. Since the validity of the first-order formulas does not
depend on the admissible set, the bottom equivalence is obvious. The right
half of the argument goes on the side of arbitrary valuations, the soundness
of which was already shown in Section 7.

We will focus on the equivalences of the left-arm, i.e., the soundness of
topologically correct executions of $\mathsf{ALBA}$ with respect to admissible
valuations.

###  9.2 Topological Correct Executions

In the present subsection, we show that $\mathsf{ALBA}$ can be executed in a
topologically correct way on restricted inductive quasi-inequalities (see
Definition 44), which paves the way for the use of the topological Ackermann
lemmas in the next subsection.

We first define syntactically closed and syntactically open formulas as
follows:

######  Definition 46 (Syntactically closed and open formulas).

  1. 1.

A formula is _syntactically closed_ if all occurrences of nominals and
$\Diamondblack,{{\Diamond}\\!\\!\\!\cdot\
},{\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$ are positive, and all occurrences of
$\blacksquare\,,{\boxdot},{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$ are negative;

  2. 2.

A formula is _syntactically open_ if all occurrences of nominals and
$\Diamondblack,{{\Diamond}\\!\\!\\!\cdot\
},{\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$ are negative, and all occurrences of
$\blacksquare\,,{\boxdot},{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$ are positive.

As is discussed in [11, Section 9], the underlying idea of the definitions
above is that given an admissible valuation, the truth set of a syntactically
closed (resp. open) formula is always a closed (resp. open) subset in $X$ (see
Definition 13).

We recall the right-handed and left-handed Ackermann rule:

The right-handed Ackermann rule:

The system $\left\\{\begin{array}[]{ll}\theta_{1}\leq p\\\ \vdots\\\
\theta_{n}\leq p\\\ \eta_{1}\leq\iota_{1}\\\ \vdots\\\
\eta_{m}\leq\iota_{m}\\\ \end{array}\right.$ is replaced by
$\left\\{\begin{array}[]{ll}\eta_{1}((\theta_{1}\lor\ldots\lor\theta_{n})/p)\leq\iota_{1}((\theta_{1}\lor\ldots\lor\theta_{n})/p)\\\
\vdots\\\
\eta_{m}((\theta_{1}\lor\ldots\lor\theta_{n})/p)\leq\iota_{m}((\theta_{1}\lor\ldots\lor\theta_{n})/p)\\\
\end{array}\right.$ where:

  1. 1.

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

  2. 2.

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

The left-handed Ackermann rule:

The system $\left\\{\begin{array}[]{ll}p\leq\theta_{1}\\\ \vdots\\\
p\leq\theta_{n}\\\ \eta_{1}\leq\iota_{1}\\\ \vdots\\\ \eta_{m}\leq\iota_{m}\\\
\end{array}\right.$ is replaced by
$\left\\{\begin{array}[]{ll}\eta_{1}((\theta_{1}\land\ldots\land\theta_{n})/p)\leq\iota_{1}((\theta_{1}\land\ldots\land\theta_{n})/p)\\\
\vdots\\\
\eta_{m}((\theta_{1}\land\ldots\land\theta_{n})/p)\leq\iota_{m}((\theta_{1}\land\ldots\land\theta_{n})/p)\\\
\end{array}\right.$ where:

  1. 1.

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

  2. 2.

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

######  Definition 47 (Topologically Correct Executions).

  * •

We call an execution of the Ackermann rule _topologically correct_ , if for
each non-pure inequality in the system, the left-hand side is syntactically
closed, and the right-hand side is syntactically open.

  * •

We call an execution of $\mathsf{ALBA}$ _topologically correct_ , if each
execution of right-handed and left-handed Ackermann lemma is topologically
correct.

######  Theorem 9.1.

Given a restricted inductive quasi-inequality as input, ALBA can topologically
correctly execute on it.

###### Proof.

We basically follow the success proof in Section 8, while pay attention to
some details (on the topological correctness) of the execution. From the proof
of Lemma 39, given an $(\Omega,\varepsilon)$-restricted inductive quasi-
inequality

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{\gamma}\prec\overline{\delta}\ \Rightarrow\
\alpha\triangleleft\beta\mbox{ (where }\triangleleft\in\\{\leq,\prec\\}),$

after the first stage, it is transformed into a set of quasi-inequalities of
the form

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\gamma}\leq\overline{\delta}\
\Rightarrow\ \alpha\leq\beta$

or

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\gamma}\leq\overline{\delta}\
\Rightarrow\ {{\Diamond}\\!\\!\\!\cdot\ }\xi\leq\chi,$

where

  * •

each $\varphi\leq\psi$ or ${{\Diamond}\\!\\!\\!\cdot\ }\gamma\leq\delta$ is
either $(\Omega,\varepsilon)$-receiving or $(\Omega,\varepsilon)$-solvable;

  * •

$+\alpha$ and $-\beta$ (resp. $+{{\Diamond}\\!\\!\\!\cdot\ }\xi$ and $-\chi$)
are definite $(\Omega,\varepsilon)$-inductive signed generation trees;

  * •

each formula contains no black connectives.

Since for the rules in the Stage 1, only the subordination rewritting rule
introduce ${{\Diamond}\\!\\!\\!\cdot\ }$ and ${{\Diamond}\\!\\!\\!\cdot\ }$
only occurs in the outermost level, it is easy to see that
$\varphi,\psi,\gamma,\delta,\alpha,\beta,\xi,\chi$ do not contain
${{\Diamond}\\!\\!\\!\cdot\
},{\boxdot},{\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}},{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$, so they are both syntactically closed and open.

Therefore, if we apply the first-approximation rule to the quasi-inequality,
we obtain

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\gamma}\leq\overline{\delta}\ \&\
\mathbf{i}_{0}\leq\alpha\ \&\ \beta\leq\neg\mathbf{i}_{1}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$

or

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\gamma}\leq\overline{\delta}\ \&\
\mathbf{i}_{0}\leq{{\Diamond}\\!\\!\\!\cdot\ }\xi\ \&\
\chi\leq\neg\mathbf{i}_{1}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1},$

where

  * •

each $\varphi\leq\psi$ or ${{\Diamond}\\!\\!\\!\cdot\ }\gamma\leq\delta$ is
either $(\Omega,\varepsilon)$-receiving or $(\Omega,\varepsilon)$-solvable;

  * •

$+\alpha$ and $-\beta$ (resp. $+{{\Diamond}\\!\\!\\!\cdot\ }\xi$ and $-\chi$)
are definite $(\Omega,\varepsilon)$-inductive signed generation trees;

  * •

each of $\varphi,\psi,\gamma,\delta,\alpha,\beta,\xi,\chi$ is both
syntactically closed and open.

For the second case, we apply the approximation rule for
${{\Diamond}\\!\\!\\!\cdot\ }$ and get

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{{{\Diamond}\\!\\!\\!\cdot\ }\gamma}\leq\overline{\delta}\ \&\
\mathbf{i}_{0}\leq{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{j}\ \&\
\mathbf{j}\leq\xi\ \&\ \chi\leq\neg\mathbf{i}_{1}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}.$

Now in both cases, we have a quasi-inequality of the following form:

$\overline{\varphi}\leq\overline{\psi}\ \&\ \mathbf{i}\leq\alpha^{\prime}\ \&\
\beta\leq\neg\mathbf{i}_{1}\ \&\ \mathsf{Pure}\ \Rightarrow\
\mathbf{i}_{0}\leq\neg\mathbf{i}_{1}$

where

  * •

each $\varphi\leq\psi$ is either $(\Omega,\varepsilon)$-receiving or
$(\Omega,\varepsilon)$-solvable;

  * •

$+\alpha^{\prime}$ and $-\beta$ are definite $(\Omega,\varepsilon)$-inductive
signed generation trees;

  * •

each of $\varphi,\beta$ is syntactically closed and each of
$\psi,\alpha^{\prime}$ is syntactically open.

Now we can easily check that the following property holds for the quasi-
inequality:

In the antecedent of the quasi-inequality, in each non-pure inequality, the
left-hand side is syntactically closed and the right-hand side is
syntactically open.

It is easy to check that for each rule in Stage 2, it does not break this
property, so for each execution of the Ackermann rule, it is topologically
correct, and after the execution of the Ackermann rule, it still satisfies the
property stated above. Therefore, the execution of $\mathsf{ALBA}$ is
topologically correct. ∎

###  9.3 Topological Ackermann Lemmas

In the present section we will prove the soundness of the algorithm
$\mathsf{ALBA}$ with respect to admissible validity on Stone spaces with two
relations. Indeed, similar to other semantic settings (see e.g., [11]), the
soundness proof on the admissible valuation side goes similar to that of the
arbitrary valuation side (i.e., Theorem 7.1), and for every rule except for
the Ackermann rules, the proof goes without modification. Thus we will only
focus on the Ackermann rules here, which are justified by the topological
Ackermann lemmas given below. The proof is similar to [11], so we only state
the lemmas without giving proof details of the lemmas.

For the Ackermann rules, the soundness proof with respect to arbitrary
valuations is justified by the Ackermann lemmas (see Lemma 36). As discussed
in the literature (e.g., [11, Section 9]), the soundness proof of the
Ackermann rules, namely the Ackermann lemmas, cannot be straightforwardly
adapted to the setting of admissible valuations, since formulas in the
expanded language might be interpreted as non-clopen subsets even if all the
propositional variables are interpreted as clopen subsets in $X$. Thus by
taking $a_{0}=\bigvee_{i}V(\theta_{i})$, we cannot guarantee that $a_{0}$ is a
clopen subset of $X$. Therefore, some adaptations are necessary based on the
syntactic shape of the formulas, which are defined in the previous subsection.

Now we state the topological Ackermann lemmas without proofs. Similar proofs
can be found in [11, Section 9].

######  Lemma 48 (Right-handed topological Ackermann lemma).

Let $\theta$ be a syntactically closed formula which does not contain $p$, let
$\eta_{i}(p)$ (resp. $\iota_{i}(p)$) be syntactically closed (resp. open) and
positive (resp. negative) in $p$ for $1\leq i\leq m$, and let $\vec{q}$ (resp.
$\vec{\mathbf{j}}$) be all the propositional variables (resp. nominals)
occurring in $\eta_{1}(p),\ldots,\eta_{m}(p)$,
$\iota_{1}(p),\ldots,\iota_{m}(p),\theta$ other than $p$. Then for all
$\vec{a}\in Clop(X),\vec{x}\in X$, the following are equivalent:

  1. 1.

$V(\eta_{i}(\theta/p))\subseteq V(\iota_{i}(\theta/p))$ for $1\leq i\leq m$,
where $V(\vec{q})=\vec{a}$, $V(\vec{\mathbf{j}})=\\{\vec{x}\\}$,

  2. 2.

there exists $a_{0}\in Clop(X)$ such that $V^{\prime}(\theta)\leq a_{0}$ and
$V^{\prime}(\eta_{i}(p))\subseteq V^{\prime}(\iota_{i}(p))$ for $1\leq i\leq
m$, where $V^{\prime}$ is the same as $V$ except that $V^{\prime}(p)=a_{0}$.

######  Lemma 49 (Left-handed topological Ackermann lemma).

Let $\theta$ be a syntactically open formula which does not contain $p$, let
$\eta_{i}(p)$ (resp. $\iota_{i}(p)$) be syntactically closed (resp. open) and
negative (resp. positive) in $p$ for $1\leq i\leq m$, and let $\vec{q}$ (resp.
$\vec{\mathbf{j}}$) be all the propositional variables (resp. nominals)
occurring in $\eta_{1}(p),\ldots,\eta_{m}(p)$,
$\iota_{1}(p),\ldots,\iota_{m}(p),\theta$ other than $p$. Then for all
$\vec{a}\in Clop(X),\vec{x}\in X$, the following are equivalent:

  1. 1.

$V(\eta_{i}(\theta/p))\subseteq V(\iota_{i}(\theta/p))$ for $1\leq i\leq m$,
where $V(\vec{q})=\vec{a}$, $V(\vec{\mathbf{j}})=\\{\vec{x}\\}$,

  2. 2.

there exists $a_{0}\in Clop(X)$ such that $a_{0}\leq V^{\prime}(\theta)$ and
$V^{\prime}(\eta_{i}(p))\subseteq V^{\prime}(\iota_{i}(p))$ for $1\leq i\leq
m$, where $V^{\prime}$ is the same as $V$ except that $V^{\prime}(p)=a_{0}$.

The proof of the topological Ackermann lemmas is similar to [21, Section B],
and therefore is omitted. We only show how these lemmas justify the soundness
of the topologically correct executions of the Ackermann rules.

######  Proposition 50.

The topologically correct executions of the Ackermann rules are sound with
respect to the admissible valuations.

###### Proof.

Here we prove it for the right-handed Ackermann lemma, and the left-handed
Ackermann lemma is similar. Without loss of generality we assume that $n=1$,
then for a topological correct execution of this rule, the system $S$ before
execution is of the following shape:

$\left\\{\begin{array}[]{ll}\theta\leq p\\\ \eta_{1}\leq\iota_{1}\\\ \vdots\\\
\eta_{m}\leq\iota_{m}\\\ \mathsf{Pure}\end{array}\right.$

where:

  1. 1.

$p$ does not occur in $\theta$ and $\theta$ is syntactically closed;

  2. 2.

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

  3. 3.

$\mathsf{Pure}$ is pure;

the system $S^{\prime}$ after the execution is of the following shape:

$\left\\{\begin{array}[]{ll}\eta_{1}(\theta/p)\leq\iota_{1}(\theta/p)\\\
\vdots\\\ \eta_{m}(\theta/p)\leq\iota_{m}(\theta/p)\\\
\mathsf{Pure}\end{array}\right.$

Similar to the discussion of page 7, it suffices to show the following:

  1. 1.

For any $X$, any admissible valuation $V_{0}$, if $X,V_{0}\Vdash S$, then
there is an admissible valuation $V_{1}$ such that
$V_{1}(\mathbf{i}_{0})=V_{0}(\mathbf{i}_{0})$,
$V_{1}(\mathbf{i}_{1})=V_{0}(\mathbf{i}_{1})$ and $X,V_{1}\Vdash S^{\prime}$;

  2. 2.

For any $X$, any admissible valuation $V_{1}$, if $X,V_{1}\Vdash S^{\prime}$,
then there is an admissible valuation $V_{0}$ such that
$V_{0}(\mathbf{i}_{0})=V_{1}(\mathbf{i}_{0})$,
$V_{0}(\mathbf{i}_{1})=V_{1}(\mathbf{i}_{1})$ and $X,V_{0}\Vdash S$.

  1. Proof of 1.

Consider any $X$ and admissible valuation $V_{0}$ on $X$. If $X,V_{0}\Vdash
S$, then take $a_{0}=V_{0}(p)$, we have:

$\left\\{\begin{array}[]{ll}V_{0}(\theta)\leq V_{0}(p)=a_{0}\\\
V_{0}(\eta_{i})\leq V_{0}(\iota_{i})\mbox{ for }1\leq i\leq m\\\
\mathsf{Pure}\mbox{ is true under }V_{0},\end{array}\right.$

so condition 2. holds, by the right-handed Ackermann lemma, condition 1 holds,
so $V_{1}(\eta_{i}(\theta/p))\subseteq V_{1}(\iota_{i}(\theta/p))$ for $1\leq
i\leq m$ and some admissible valuation $V_{1}$ which differs from $V_{0}$ at
most at $p$. It is easy to see that $\mathsf{Pure}$ is true under $V_{0}$ iff
it is true under $V_{1}$, so $X,V_{1}\Vdash S^{\prime}$;

  2. Proof of 2.

Consider any $X$ and admissible valuation $V_{1}$ on $X$. If $X,V_{1}\Vdash
S^{\prime}$, then we have:

$\left\\{\begin{array}[]{ll}V_{1}(\eta_{i}(\theta/p))\leq
V_{1}(\iota_{i}(\theta/p))\mbox{ for }1\leq i\leq m\\\ \mathsf{Pure}\mbox{ is
true under }V_{1},\end{array}\right.$

so condition 1. holds, by the right-handed Ackermann lemma, condition 2 holds,
so there exists $a_{0}\in Clop(X)$ such that $V_{0}(\theta)\leq a_{0}$ and
$V_{0}(\eta_{i}(p))\subseteq V_{0}(\iota_{i}(p))$ for $1\leq i\leq m$, where
$V_{0}$ is the same as $V_{1}$ except that $V_{0}(p)=a_{0}$. It is easy to see
that $\mathsf{Pure}$ is true under $V_{1}$ iff it is true under $V_{0}$,

$\left\\{\begin{array}[]{ll}V_{0}(\theta)\leq V_{0}(p)=a_{0}\\\
V_{0}(\eta_{i})\leq V_{0}(\iota_{i})\mbox{ for }1\leq i\leq m\\\
\mathsf{Pure}\mbox{ is true under }V_{0},\end{array}\right.$

so $X,V_{0}\Vdash S$.

∎

##  10 Examples

######  Example 10.1.

Given a modal subordination algebra $(B,\prec,\Diamond)$, it is proximity
preserving iff its dual Stone space with two relations $(X,\tau,R,R^{\prime})$
satisfies the following interaction condition:

$\forall w(R[R^{\prime-1}(w)]\subseteq R^{\prime-1}[R(w)]),\mbox{ i.e.\ }$
$\mbox{for all }u,v,w\in X\mbox{ such that }vR^{\prime}w\mbox{ and }vRu,\mbox{
there exists a }t\in X\mbox{ such that }wRt\mbox{ and }uR^{\prime}t.$

###### Proof.

It suffices to show that

$(B,\prec,\Diamond)\Vdash(a\prec b)\Rightarrow(\Diamond a\prec\Diamond b)$

iff its dual

$(X,\tau,R,R^{\prime})\vDash\forall w(R[R^{\prime-1}(w)]\subseteq
R^{\prime-1}[R(w)]).$

Indeed,

| $(B,\prec,\Diamond)\Vdash(a\prec b)\Rightarrow(\Diamond a\prec\Diamond b)$
---|---
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall a\forall b((a\prec b)\Rightarrow(\Diamond a\prec\Diamond b))$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall a\forall b({{\Diamond}\\!\\!\\!\cdot\ }a\leq b\Rightarrow{{\Diamond}\\!\\!\\!\cdot\ }\Diamond a\leq\Diamond b)$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall a\forall b\forall\mathbf{i}\forall\mathbf{j}({{\Diamond}\\!\\!\\!\cdot\ }a\leq b\ \&\ \mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\ }\Diamond a\ \&\ \Diamond b\leq\neg\mathbf{j}\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall a\forall b\forall\mathbf{i}\forall\mathbf{j}\forall\mathbf{k}({{\Diamond}\\!\\!\\!\cdot\ }a\leq b\ \&\ \mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\ }\Diamond\mathbf{k}\ \&\ \mathbf{k}\leq a\ \&\ \Diamond b\leq\neg\mathbf{j}\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall b\forall\mathbf{i}\forall\mathbf{j}\forall\mathbf{k}({{\Diamond}\\!\\!\\!\cdot\ }\mathbf{k}\leq b\ \&\ \mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\ }\Diamond\mathbf{k}\ \&\ \Diamond b\leq\neg\mathbf{j}\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall\mathbf{i}\forall\mathbf{j}\forall\mathbf{k}(\mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\ }\Diamond\mathbf{k}\ \&\ \Diamond{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{k}\leq\neg\mathbf{j}\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall\mathbf{k}({{\Diamond}\\!\\!\\!\cdot\ }\Diamond\mathbf{k}\leq\Diamond{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{k})$
iff |  $(X,\tau,R,R^{\prime})\vDash\forall w(R[R^{\prime-1}(w)]\subseteq R^{\prime-1}[R(w)])$.

∎

######  Example 10.2 (See Lemma 2.1.12 in [25]).

Given a modal subordination algebra $(B,\prec,\Diamond)$ and its dual Stone
space with two relations $(X,\tau,R,R^{\prime})$,

  1. 1.

$(B,\prec,\Diamond)\Vdash\forall a\forall b(a\prec b\Rightarrow a\leq b)$ iff
$R$ is reflexive;

  2. 2.

$(B,\prec,\Diamond)\Vdash\forall a\forall b(a\prec b\Rightarrow\neg b\prec\neg
a)$ iff $R$ is symmetric.

###### Proof.

  1. 1.

It suffices to show that

$(B,\prec,\Diamond)\Vdash a\prec b\Rightarrow a\leq b$

iff its dual

$(X,\tau,R,R^{\prime})\vDash\forall wRww.$

Indeed,

| $(B,\prec,\Diamond)\Vdash a\prec b\ \Rightarrow\ a\leq b$
---|---
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall a\forall b(a\prec b\ \Rightarrow\ a\leq b)$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall a\forall b({{\Diamond}\\!\\!\\!\cdot\ }a\leq b\ \Rightarrow\ a\leq b)$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall a\forall b\forall\mathbf{i}\forall\mathbf{j}({{\Diamond}\\!\\!\\!\cdot\ }a\leq b\ \&\ \mathbf{i}\leq a\ \&\ b\leq\neg\mathbf{j}\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall b\forall\mathbf{i}\forall\mathbf{j}({{\Diamond}\\!\\!\\!\cdot\ }\mathbf{i}\leq b\ \&\ b\leq\neg\mathbf{j}\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall\mathbf{i}\forall\mathbf{j}({{\Diamond}\\!\\!\\!\cdot\ }\mathbf{i}\leq\neg\mathbf{j}\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall\mathbf{i}(\mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{i})$
iff | $(X,\tau,R,R^{\prime})\vDash\forall w(w\in R[w])$
iff |  $(X,\tau,R,R^{\prime})\vDash\forall wRww$.

  2. 2.

It suffices to show that

$(B,\prec,\Diamond)\Vdash\forall a\forall b(a\prec b\Rightarrow\neg b\prec\neg
a)$

iff its dual

$(X,\tau,R,R^{\prime})\vDash\forall w\forall v(Rvw\to Rwv).$

Indeed,

| $(B,\prec,\Diamond)\Vdash a\prec b\ \Rightarrow\ \neg b\prec\neg a$
---|---
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall a\forall b(a\prec b\ \Rightarrow\ \neg b\prec\neg a)$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall a\forall b({{\Diamond}\\!\\!\\!\cdot\ }a\leq b\ \Rightarrow\ {{\Diamond}\\!\\!\\!\cdot\ }\neg b\leq\neg a)$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall a\forall b\forall\mathbf{i}\forall\mathbf{j}({{\Diamond}\\!\\!\\!\cdot\ }a\leq b\ \&\ \mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\ }\neg b\ \&\ \neg a\leq\neg\mathbf{j}\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall a\forall b\forall\mathbf{i}\forall\mathbf{j}\forall\mathbf{k}({{\Diamond}\\!\\!\\!\cdot\ }a\leq b\ \&\ \mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{k}\ \&\ \mathbf{k}\leq\neg b\ \&\ \neg a\leq\neg\mathbf{j}\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall a\forall b\forall\mathbf{i}\forall\mathbf{j}\forall\mathbf{k}({{\Diamond}\\!\\!\\!\cdot\ }a\leq b\ \&\ \mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{k}\ \&\ \mathbf{k}\leq\neg b\ \&\ \mathbf{j}\leq a\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall b\forall\mathbf{i}\forall\mathbf{j}\forall\mathbf{k}({{\Diamond}\\!\\!\\!\cdot\ }\mathbf{j}\leq b\ \&\ \mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{k}\ \&\ \mathbf{k}\leq\neg b\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall\mathbf{i}\forall\mathbf{j}\forall\mathbf{k}(\mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{k}\ \&\ \mathbf{k}\leq\neg{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{j}\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall\mathbf{i}\forall\mathbf{j}(\mathbf{i}\leq{{\Diamond}\\!\\!\\!\cdot\ }\neg{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{j}\ \Rightarrow\ \mathbf{i}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall\mathbf{j}({{\Diamond}\\!\\!\\!\cdot\ }\neg{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{j}\leq\neg\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall\mathbf{j}(\mathbf{j}\leq\neg{{\Diamond}\\!\\!\\!\cdot\ }\neg{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall\mathbf{j}(\mathbf{j}\leq{\boxdot}{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\Vdash_{Clop}\forall\mathbf{j}({\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\ }}}\mathbf{j}\leq{{\Diamond}\\!\\!\\!\cdot\ }\mathbf{j})$
iff | $(X,\tau,R,R^{\prime})\vDash\forall w(R^{-1}[w]\subseteq R[w])$
iff |  $(X,\tau,R,R^{\prime})\vDash\forall w\forall v(Rvw\to Rwv)$.

∎

## Part II: Correspondence and Canonicity for $\Pi_{2}$-statements

In this part, we focus on _$\Pi_{2}$ -statements_ of the form
$\overline{\varphi}\triangleleft\overline{\psi}\ \Rightarrow\
\exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$,444Here we
call it a $\Pi_{2}$-statement is because the statement is implicitly
universally quantified when talking about its validity, therefore it is of the
$\forall\exists$-form. and develop their correspondence and canonicity theory.
We will define inductive $\Pi_{2}$-statements and restricted inductive
$\Pi_{2}$-statements (Section 12), give a version of the algorithm
$\mathsf{ALBA}^{\Pi_{2}}$ for $\Pi_{2}$-statements (Section 13), state its
soundness with respect to arbitrary valuations (Section 14), success on
inductive and restricted inductive $\Pi_{2}$-statements (Section 15), and
canonicity of restricted inductive $\Pi_{2}$-statements (Section 16).

##  11 Syntax and Semantics

For $\Pi_{2}$-statements, the special feature of its syntax is the
propositional quantifiers of the form $\exists q$. The semantics of the
propositional quantifiers is already different between admissible valuations
and arbitrary valuations. The semantics of propositional quantifiers are given
as follows: for any Stone space with two relations $X$,

  * •

for any admissible valuation $V_{0}$, $(X,V_{0})\Vdash\exists
q\exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$ iff there
exist $A\in Clop(X)$ such that
$X,(V_{0})^{q}_{A}\Vdash\exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$;

  * •

for any arbitrary valuation $V_{1}$, $(X,V_{1})\Vdash\exists
q\exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$ iff there
exist $A\in P(X)$ such that
$X,(V_{1})^{q}_{A}\Vdash\exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$.

For the semantics of $\Pi_{2}$-statements, the global satisfaction relation
for $\Pi_{2}$-statements is defined differently between admissible valuations
and arbitrary valuations. It is given as follows:

######  Definition 51.

Given a $\Pi_{2}$-statement $\overline{\varphi}\triangleleft\overline{\psi}\
\Rightarrow\ \exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$,
a Stone space with two relations $X$, an admissible valuation $V_{0}$, an
arbitrary valuation $V_{1}$,

  * •

$X,V_{0}\Vdash\overline{\varphi}\triangleleft\overline{\psi}\ \Rightarrow\
\exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$ iff whenever
$X,V_{0}\Vdash\overline{\varphi}\triangleleft\overline{\psi}$, there exist
$\vec{A}\in Clop(X)$ such that
$X,(V_{0})^{\vec{q}}_{\vec{A}}\Vdash\overline{\gamma}\triangleleft\overline{\delta}$;

  * •

$X,V_{1}\Vdash\overline{\varphi}\triangleleft\overline{\psi}\ \Rightarrow\
\exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$ iff whenever
$X,V_{1}\Vdash\overline{\varphi}\triangleleft\overline{\psi}$, there exist
$\vec{A}\in P(X)$ such that
$X,(V_{1})^{\vec{q}}_{\vec{A}}\Vdash\overline{\gamma}\triangleleft\overline{\delta}$.

  * •

$\overline{\varphi}\triangleleft\overline{\psi}\ \Rightarrow\
\exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$ is admissibly
valid in $X$, i.e.
$X\Vdash_{Clop}\overline{\varphi}\triangleleft\overline{\psi}\ \Rightarrow\
\exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$ iff
$X,V_{0}\Vdash\overline{\varphi}\triangleleft\overline{\psi}\ \Rightarrow\
\exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$ for all
admissible valuations $V_{0}$;

  * •

$\overline{\varphi}\triangleleft\overline{\psi}\ \Rightarrow\
\exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$ is valid in
$X$, i.e. $X\Vdash_{P}\overline{\varphi}\triangleleft\overline{\psi}\
\Rightarrow\ \exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$
iff $X,V_{1}\Vdash\overline{\varphi}\triangleleft\overline{\psi}\ \Rightarrow\
\exists\vec{q}(\overline{\gamma}\triangleleft\overline{\delta})$ for all
arbitrary valuations $V_{1}$.

##  12 Inductive and Restricted Inductive $\Pi_{2}$-Statements

In the present section, we define inductive and restricted inductive
$\Pi_{2}$-statements of the shape

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{\chi}\prec\overline{\xi}\Rightarrow\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\
\&\ \overline{\gamma}\prec\overline{\delta})$

where each of $\varphi,\psi,\chi,\xi,\alpha,\beta,\gamma,\delta$ has certain
syntactic restrictions.

###  12.1 Intuitive ideas behind the definition

  1. 1.

The basic idea behind defining inductive $\Pi_{2}$-statements is as follows:
We divide the algorithm into two parts, the first part of the algorithm
equivalently transforms $\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\
\&\ \overline{\gamma}\prec\overline{\delta})$ part into a meta-conjunction of
inequalities $\mathsf{MetaConIneq}$, such that

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{\chi}\prec\overline{\xi}\Rightarrow\ \mathsf{MetaConIneq}$

is an inductive quasi-inequality, and we can then use the second part of the
algorithm (which is the same as the algorithm $\mathsf{ALBA}$ for quasi-
inequalities) to transform it into a set of pure quasi-inequalities. The first
part of the algorithm eliminate all the existential propositional quantifiers
by application of Ackermann rules, but this time we do not have nominals in
the elimination of existential propositional quantifiers like in the
elimination of the (implicit) universal propositional quantifiers (which is
what will be done in the second part of the algorithm).

  2. 2.

For the elimination of the existential propositional quantifiers, we again
divide the set of inequalities in

$\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\ \&\
\overline{\gamma}\prec\overline{\delta})$

into two parts:

     * •

One part is the solvable inequalities, which will finally be transformed into
inequalities of the form $\theta\leq q$ or $q\leq\theta$. The solvable
inequalities will be used to compute the minimal valuations of the
propositional variables in $\exists\vec{q}$.

     * •

The other part is the receiving inequalities, which will be used to receive
minimal valuations.

  3. 3.

For the canonicity proof, we again need to guarantee certain syntactic
topological properties, which will be further explained in the canonicity
proof. These restrictions lead to the definition of restricted inductive
$\Pi_{2}$-statements.

###  12.2 The Definition of Inductive $\Pi_{2}$-Statements

In this section, we will define inductive $\Pi_{2}$-statements in the language
without black connectives
$\Diamondblack,\blacksquare,{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}},{\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$ or nominals, which will be shown to have first-order correspondents over
arbitrary valuations on Stone spaces with two relations. This definition will
not be given in a syntactic description, for a syntactic definition we will
leave to future work.

Before defining inductive $\Pi_{2}$-statements, we first define the so-called
first-round good $\exists$-statements of the form
$\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\ \&\
\overline{\gamma}\prec\overline{\delta})$, which are the ones that can be
equivalently transformed into a “good” meta-conjunction of inequalities
without existential propositional quantifiers:

######  Definition 52 ($(\Omega,\varepsilon_{\vec{p}})$-First-Round Good
$\exists$-Statements).

Given an order-type $\varepsilon_{\vec{p}}$ for $\vec{p}$, and a dependence
order $<_{\Omega}$ on $\vec{p}$, an $\exists$-statement
$\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\ \&\
\overline{\gamma}\prec\overline{\delta})$ is
$(\Omega,\varepsilon_{\vec{p}})$-first-round good, if by the first part of the
algorithm $\mathsf{ALBA}^{\Pi_{2}}$ defined in Section 13, it can be
transformed into a meta-conjunction of inequalities $\mathsf{MetaConIneq}$,
each inequality in which is $(\Omega,\varepsilon_{\vec{p}})$-inductive (i.e.
the positive tree of the left-hand side and the negative tree of the right-
hand side are both $(\Omega,\varepsilon_{\vec{p}})$-inductive, which might
contain black connectives) for the same $(\Omega,\varepsilon_{\vec{p}})$.

######  Definition 53 (Inductive $\Pi_{2}$-Statements).

Given an order-type $\varepsilon_{\vec{p}}$ for $\vec{p}$, and a dependence
order $<_{\Omega}$ on $\vec{p}$, a $\Pi_{2}$-statement

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{\chi}\prec\overline{\xi}\Rightarrow\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\
\&\ \overline{\gamma}\prec\overline{\delta})$

is $(\Omega,\varepsilon_{\vec{p}})$-inductive, if

  * •

it does not contain nominals or black connectives
$\Diamondblack,\blacksquare,{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}},{\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$;

  * •

$\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\ \&\
\overline{\gamma}\prec\overline{\delta})$ is
$(\Omega,\varepsilon_{\vec{p}})$-first-round good;

  * •

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{\chi}\prec\overline{\xi}\Rightarrow\mathsf{MetaConIneq}$ is an
$(\Omega,\varepsilon_{\vec{p}})$-inductive quasi-inequality (which might
contain black connectives), where $\mathsf{MetaConIneq}$ is defined as in
Definition 54.

A $\Pi_{2}$-statement is inductive, if it is
$(\Omega,\varepsilon_{\vec{p}})$-inductive for some $\varepsilon_{\vec{p}}$
and $<_{\Omega}$.

###  12.3 The Definition of Restricted Inductive $\Pi_{2}$-Statements

In this section, we will define restricted inductive $\Pi_{2}$-statements,
which will be shown to be canonical. For this class of $\Pi_{2}$-statements,
we will give a syntactic description.

Again, before defining restricted inductive $\Pi_{2}$-statements, we first
defined the restricted first-round good $\exists$-statements.

######  Definition 54 ($(\Omega,\varepsilon_{\vec{q}})$-Restricted First-Round
Good $\exists$-Statements).

Given order-types $\varepsilon_{\vec{p}}$ and $\varepsilon_{\vec{q}}$ for
$\vec{p}$ and $\vec{q}$, and a dependence order $<_{\Omega}$ on $\vec{p}$ and
$\vec{q}$ such that $p<_{\Omega}q$ for all $p$ in $\vec{p}$ and $q$ in
$\vec{q}$, an $\exists$-statement
$\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\ \&\
\overline{\gamma}\prec\overline{\delta})$ is
$(\Omega,\varepsilon_{\vec{q}})$-restricted first-round good, if inequalities
in $\overline{\alpha}\leq\overline{\beta}\ \&\
\overline{\gamma}\prec\overline{\delta}$ can be divided into the following two
kinds:

  * •

$\theta\triangleleft\eta$, which we call
$(\Omega,\varepsilon_{\vec{q}})$-restricted receiving inequality, where

    * –

all branches in $-\theta$ and $+\eta$ ending with propositional variables in
$\vec{q}$ are $\varepsilon_{\vec{q}}^{\partial}$-critical (i.e. in the first
half of the algorithm, the inequality $\theta\triangleleft\eta$ is a
“receiving” inequality);

    * –

all branches of $+\theta$ and $-\eta$ are Skeleton branches (i.e. in the
second half of the algorithm, their branches behave like Skeleton branches);

  * •

$\iota\triangleleft\zeta$, which we call
$(\Omega,\varepsilon_{\vec{q}})$-restricted solvable inequality, where

    * –

exactly one of $-\iota,+\zeta$ is such that all branches ending with
propositional variables in $\vec{q}$ are
$\varepsilon_{\vec{q}}^{\partial}$-critical (without loss of generality we
denote this generation tree $\star\rho$ and the other one $*\kappa$), and the
other contains $\varepsilon_{\vec{q}}$-critical branches;

    * –

$*\kappa$ is $(\Omega,\varepsilon_{\vec{q}})$-inductive, and all
$\varepsilon_{\vec{q}}$-critical branches in $*\kappa$ are PIA branches;

    * –

for all the $\varepsilon_{\vec{q}}$-critical branches in $*\kappa$ ending with
$q$, all propositional variables $r$ in $\star\rho$, we have $r<_{\Omega}q$.

    * –

for every branch in $-\iota$ and $+\zeta$ which is not
$\varepsilon_{\vec{q}}$-critical, it is a Skeleton branch in $+\iota$ and
$-\zeta$.

The basic idea behind the “solvable inequality” is that after the application
of residuation rules exhaustively, the resulting inequality is of the form
$\upsilon\leq r$ (when $\varepsilon(r)=1$) or of the form $r\leq\upsilon$
(when $\varepsilon(r)=\partial$) where all branches in $+\upsilon$ (resp.
$-\upsilon$) ending with $p$ in $\vec{p}$ is a Skeleton branch.

######  Definition 55 (Restricted Inductive $\Pi_{2}$-Statements).

Given order-types $\varepsilon_{\vec{p}}$, $\varepsilon_{\vec{q}}$ for
$\vec{p}$, $\vec{q}$, and a dependence order $<_{\Omega}$ on $\vec{p}$ and
$\vec{q}$ such that $p<_{\Omega}q$ for all $p$ in $\vec{p}$ and $q$ in
$\vec{q}$, a $\Pi_{2}$-statement

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{\chi}\prec\overline{\xi}\Rightarrow\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\
\&\ \overline{\gamma}\prec\overline{\delta})$

is $(\Omega,\varepsilon_{\vec{p}})$-restricted inductive,

  * •

it does not contain nominals or black connectives
$\Diamondblack,\blacksquare,{\blacksquare\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}},{\Diamondblack\\!\\!\\!{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\cdot\
}}}$ or ${{\Diamond}\\!\\!\\!\cdot\ },{\boxdot}$;

  * •

$\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\ \&\
\overline{\gamma}\prec\overline{\delta})$ is
$(\Omega,\varepsilon_{\vec{q}})$-restricted first-round good;

  * •

each inequality in $\varphi\leq\psi$ and $\chi\prec\xi$ is either
$(\Omega,\varepsilon_{\vec{p}})$-receiving or
$(\Omega,\varepsilon_{\vec{p}})$-solvable.

A $\Pi_{2}$-statement is restricted inductive, if it is
$(\Omega,\varepsilon_{\vec{p}})$-restricted inductive for some
$\varepsilon_{\vec{p}}$ and $<_{\Omega}$.

##  13 The Algorithm $\mathsf{ALBA}^{\Pi_{2}}$

The algorithm $\mathsf{ALBA}^{\Pi_{2}}$ transforms the input
$\Pi_{2}$-statement

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{\chi}\prec\overline{\xi}\Rightarrow\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\
\&\ \overline{\gamma}\prec\overline{\delta})$

into an equivalent set of pure quasi-inequalities which does not contain
occurrences of propositional variables or propositional quantifiers, and
therefore can be translated into the first-order correspondence language via
the standard translation of the expanded language (see page 4.2). The language
on which we manipulate the algorithm is almost the same as the algorithm for
quasi-inequalities, except that we have additional existential propositional
quantifiers $\exists q$.

Now we define the algorithm in two halves, the first half aims at reducing

$\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\ \&\
\overline{\gamma}\prec\overline{\delta})$

into a meta-conjunction of inequalities, and the second half is just the
algorithm $\mathsf{ALBA}$ for quasi-inequalities.

##### First Half

The algorithm receives a $\Pi_{2}$-statement

$\overline{\varphi}\leq\overline{\psi}\ \&\
\overline{\chi}\prec\overline{\xi}\Rightarrow\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\
\&\ \overline{\gamma}\prec\overline{\delta})$

as input. The first half of the algorithm operates on the $\exists$-statement
$\exists\vec{q}(\overline{\alpha}\leq\overline{\beta}\ \&\