# Correspondence Theory for Modal Fairtlough-Mendler Semantics of
Intuitionistic Modal Logic

Zhiguang Zhao

###### Abstract

We study the correspondence theory of intuitionistic modal logic in modal
Fairtlough-Mendler semantics (modal FM semantics) [13], which is the
intuitionistic modal version of possibility semantics [19]. We identify the
fragment of inductive formulas [14] in this language and give the algorithm
$\mathsf{ALBA}$ [7] in this semantic setting. There are two major features in
the paper: one is that in the expanded modal language, the nominal variables,
which are interpreted as atoms in perfect Boolean algebras, complete join-
prime elements in perfect distributive lattices and complete join-irreducible
elements in perfect lattices, are interpreted as the refined regular open
closures of singletons in the present setting, similar to the possibility
semantics for classical normal modal logic [33]; the other feature is that we
do not use conominals or diamond, which restricts the fragment of inductive
formulas significantly. We prove the soundness of the $\mathsf{ALBA}$ with
respect to modal FM frames and show that the $\mathsf{ALBA}$ succeeds on
inductive formulas, similar to existing settings like [7, 33, 34].

_Keywords_ : possibility semantics, Fairtlough-Mendler semantics,
correspondence theory, nucleus, complete Heyting algebra, intuitionistic modal
logic

##  1 Introduction

##### Possibility Semantics.

Possibility semantics was proposed by Humberstone [20], which is a
generalization of possible world semantics for modal logic, based on partial
possibilities instead of complete possible worlds like the one in standard
possible world semantics. In recent years there have been a lot of studies in
possibility semantics [4, 10, 15, 16, 17, 31], to name but a few. For a
comprehensive study of possibility semantics, see [18, 19].

##### Intuitionistic Study of Possibility Semantics.

In [2], Bezhanishvili and Holliday use the tools of nuclei to study the
equivalence between Fairtlough-Mendler semantics (FM semantics for short)
[13], Dragalin semantics [11, 12] and nuclear semantics of intuitionistic
logic, which can be regarded as different ways to realize possibility
semantics of intuitionistic logic. In [3], Bezhanishvili and Holliday study
the different semantics of intuitionistic logic, which form a hierarchy. Among
these semantics, Dragalin semantics is more like neighbourhood semantics of
modal logic [27, 28, 30] and Beth semantics of intuitionistic logic [1],
nuclear semanrics is more like algebraic semantics, and FM semantics is more
like relational semantics with two relations. In [24], Massas provides choice-
free representation theorems for distributive lattice, Heyting algebras and
co-Heyting algebras. In [26], Massas studies the B-frame duality, where
B-frames can be seen as a generalization of posets, which play an important
role in the representation theory of Heyting algebras.

##### Correspondence Theory for Possibility Semantics.

In [32], Yamamoto studies Sahlqvist correspondence theory for full possibility
frames. In [19, Theorem 7.20], Holliday shows that all inductive formulas are
filter-canonical, therefore every normal modal logic axiomatized by inductive
formulas is sound and complete with respect to its canonical full possibility
frame. In [33], Zhao shows that inductive formulas have first-order
correspondents in full possibility frames as well as in filter-descriptive
possibility frames, using algebraic and algorithmic correspondence theory
methods [6, 7]. In this setting, the algebraic strcuture of regular open
subsets of a given full possibility frame is a complete Boolean algebra with a
complete operator, which is not necessarily an atomic Boolean algebra,
therefore it is not necessarily perfect.

##### Our Methodology.

Our aim is to see if Sahlqvist-type correspondence theory could work for
semantics whose algebraic counterpart is based on locales, i.e. complete
Heyting algebras, which are not necessarily perfect (where every element is
join-generated by complete join-primes).

We study the correspondence theory of intuitionistic modal logic in the modal
version of Fairtlough-Mendler semantics, using algorithmic correspondence
theory methods, as explained in [6, 7]. We define the class of inductive
formulas for this semantics as well as the Ackermann Lemma Based Algorithm
$\mathsf{ALBA}$ which computes the first-order correspondents of inductive
formulas.

Following the methodology of [33], our semantic analysis of the modal FM
frames is base on their dual algebraic structures, which are complete Heyting
algebras with complete operators (not necessarily perfect), where complete
join-primes are not always available, in contrast to settings like [7]. We use
the representation of complete Heyting algebras as the refined regular open
subsets in Fairtlough-Mendler frames, and we identify one Heyting algebra with
an operator (HAO) and one Boolean algebra with an operator (BAO) as the dual
algebraic structures of a given modal FM frame $\mathbb{F}$: namely, the HAO
$\mathbb{H}_{\mathsf{RO}_{12}}$ of refined regular open subsets of
$\mathbb{F}$ and the BAO $\mathbb{B}_{\mathsf{K}}$ of arbitrary subsets of
$\mathbb{F}$. Therefore, we can define a natural order-embedding
$e:\mathbb{H}_{\mathsf{RO}_{12}}\to\mathbb{B}_{\mathsf{K}}$. It is completely
meet-preserving, therefore it has a left adjoint
$c:\mathbb{B}_{\mathsf{K}}\to\mathbb{H}_{\mathsf{RO}_{12}}$ sending a subset
of the domain of $\mathbb{F}$ to the smallest refined regular open subset
containing it. We will use $c$ substantially in the interpretations of the
expanded modal language $\mathcal{L}^{+}$ of the algorithm $\mathsf{ALBA}$,
which will play an important role in the relational semantics and the refined
regular open translation of the expanded modal language.

To summarize, the principles for choosing the interpretations of the expanded
modal language are the following:

  * •

The set of possible interpretations of nominals is join-dense in the complete
algebra of possible values of propositional variables;

  * •

The set of possible interpretations of conominals is meet-dense in the
complete algebra of possible values of propositional variables (only in
settings when this is possible);

  * •

The interpretation of black connectives should be the adjoints of modalities
in the basic propositional language;

  * •

These interpretations should be expressible in a first-order way.

##### Structure of the paper.

The paper is organized as follows: Section 2 introduces some relevant
structures and notions that will be used in later sections. Section 3 presents
preliminaries on modal Fairtlough-Mendler semantics. Section 4 analyzes the
semantic environment for the interpretation of the expanded modal language.
Section 5 introduces the expanded modal language formally as well as the
refined regular open translation. Section 6 gives the syntactic definition of
inductive formulas. Section 7 introduced the algorithm $\mathsf{ALBA}$ with an
example. Section 8 gives its success proof on inductive formulas and Section 9
gives its soundness proof. Section 10 gives the conclusions.

##  2 Preliminaries

In this section, we introduce some topological and relational structures and
the notion of nucleus, which will be useful in later sections. For more
details, see [2, 24, 25].

###  2.1 Topological and Relational Structures

######  Definition 2.1 (Refined Bitopological Space, Definition 5.1.1 in
[24]).

A _refined bitopological space_ is a triple $(X,\tau_{1},\tau_{2})$ where
$\tau_{1}$ and $\tau_{2}$ are topologies on $X$ and
$\tau_{1}\subseteq\tau_{2}$.

######  Definition 2.2 (Refined Birelational Frame).

A _refined birelational frame_ is a tuple $(X,\leq_{1},\leq_{2})$ where
$\leq_{2}\subseteq\leq_{1}$ are both partial orders on $X$.

For any poset $(X,\leq)$, define the topology $\tau_{\leq}$ taking all the
upsets of $(X,\leq)$ as open sets. Therefore we can identify a partial order
$(X,\leq)$ with its corresponding Alexandroff topology $(X,\tau)$. Since
$\leq_{2}\subseteq\leq_{1}$ iff $\tau_{\leq_{1}}\subseteq\tau_{\leq_{2}}$, we
can identify refined birelational frames with their corresponding refined bi-
Alexandroff spaces.

In what follows, we will call refined birelational frames also Fairtlough-
Mendler frames (FM frames for short) [2, 13].

###  2.2 Nucleus

In this subsection we introduce the notion of nucleus on Heyting algebras. For
more details, see [21, 22, 23].

######  Definition 2.3 (Nucleus).

A _nucleus_ on a Heyting algebra $\mathbb{H}$ is a map
$j:\mathbb{H}\to\mathbb{H}$ satisfying the following conditions:

  * •

$j(a\wedge b)=j(a)\wedge j(b)$;

  * •

$a\leq j(a)$.

It is clear that a nucleus on $\mathbb{H}$ is also a closure operator, and the
following properties follow from the definition:

  * •

$j(\top)=\top$;

  * •

if $a\leq b$, then $j(a)\leq j(b)$;

  * •

$j(j(a))=j(a)$.

We call a nucleus _dense_ if $j(\bot)=\bot$.

######  Definition 2.4 (Nuclear algebra).

A _nuclear algebra_ is a pair $(\mathbb{H},j)$ where $\mathbb{H}$ is a Heyting
algebra and $j$ is a nucleus on $\mathbb{H}$. It is a _localic nuclear
algebra_ if $\mathbb{H}$ is a locale, i.e. a complete Heyting algebra.

######  Theorem 2.5.

If $\mathbb{H}=(H,\bot,\top,\land,\lor,\to,j)$ is a nuclear algebra, then
$\mathbb{H}_{j}=(H_{j},\bot_{j},\top,\land_{j},\lor_{j},\to_{j})$ is a Heyting
algebra where $H_{j}=\\{a\in H\mid a=j(a)\\}$ and for $a,b\in H_{j}$:

  * •

$\bot_{j}=j(\bot)$;

  * •

$a\land_{j}b=a\land b$;

  * •

$a\lor_{j}b=j(a\lor b)$;

  * •

$a\to_{j}b=a\to b$.

If $H$ is a localic nuclear algebra, then $H_{j}$ is a locale, where for
$Y\subseteq H_{j}$:

  * •

$\bigwedge_{j}Y=\bigwedge Y$;

  * •

$\bigvee_{j}Y=j(\bigvee Y)$.

In a given refined bitopological space $(X,\tau_{1},\tau_{2})$, we use
$\mathsf{I}_{i}$ to denote the interior map in $\tau_{i}$ and $\mathsf{C}_{i}$
to denote the closure map in $\tau_{i}$. We use $\mathsf{RO}_{12}(X)$ to
denote $\\{Y\subseteq X\mid Y=\mathsf{I}_{1}\mathsf{C}_{2}(Y)\\}$.

######  Lemma 2.6.

Let $\mathbb{F}=(X,\leq_{1},\leq_{2})$ be an FM-frame and
$(X,\tau_{1},\tau_{2})$ be its corresponding refined bitopological space, let
the $\mathbb{H}_{\mathsf{RO}_{12}}$ be the algebra $(\mathsf{RO}_{12}(X)$,
$\varnothing$, $H$, $\cap$, $\lor_{\mathsf{RO}_{12}}$,
$\to_{\mathsf{RO}_{12}})$ where
$Y\lor_{\mathsf{RO}_{12}}Z:=\mathsf{I}_{1}\mathsf{C}_{2}(Y\cup Z)$,
$Y\to_{\mathsf{RO}_{12}}Z:=\mathsf{I}_{1}((X-Y)\cup Z)$. Then the operator
$\mathsf{I}_{1}\mathsf{C}_{2}$ is a nucleus on the complete Heyting algebra of
opens in $\tau_{1}$. Therefore $\mathbb{H}_{\mathsf{RO}_{12}}$ is a complete
Heyting algebra.

##  3 Preliminaries on Modal Fairtlough-Mendler semantics

In the present section we collect the preliminaries on modal Fairtlough-
Mendler semantics. For more details, see e.g., [13, 24, 25]. The style of
presentation follows [7, 33].

###  3.1 Language

Let $\mathsf{Prop}$ be the set of propositional variables. The basic modal
language $\mathcal{L}$ is defined as follows:

$\varphi::=p\mid\bot\mid\top\mid\varphi\land\varphi\mid\varphi\lor\varphi\mid\varphi\to\varphi\mid\Box\varphi,$

where $p\in\mathsf{Prop}$.

In the algorithm, we will use _inequalities_ $\varphi\leq\psi$, whose truth in
a model is equivalent to the global truth of $\varphi\to\psi$ in the model. We
will also define _quasi-inequalities_ $\varphi_{1}\leq\psi_{1}\ \&\ \ldots\
\&\ \varphi_{n}\leq\psi_{n}\Rightarrow\varphi\leq\psi$, where $\&$ is the
meta-level conjunction and $\Rightarrow$ is the meta-level implication. We say
that a formula is _pure_ if it does not contain occurrences of propositional
variables.

###  3.2 Semantics

For any $R\subseteq W\times W$, we denote $R[X]=\\{w\in W\mid(\exists x\in
X)Rxw\\}$, $R^{-1}[X]=\\{w\in W\mid(\exists x\in X)Rwx\\}$, $R[w]:=R[\\{w\\}]$
and $R^{-1}[w]:=R^{-1}[\\{w\\}]$, respectively.

######  Definition 3.1 (Modal FM frames and models).

A _modal FM frame_ is a tuple $\mathbb{F}=(X,\leq_{1},\leq_{2},R)$, where
$(X,\leq_{1},\leq_{2})$ is an FM frame, $R\subseteq W\times W$ such that
$\Box_{\mathsf{RO}_{12}}(X):=\\{w\in W\mid R[w]\subseteq
X\\}\in\mathsf{RO}_{12}(X)$ for any $X\in\mathsf{RO}_{12}(X)$. A _modal FM
model_ is a pair $\mathbb{M}=(\mathbb{F},V)$ where
$V:\mathsf{Prop}\to\mathsf{RO}_{12}(X)$ is a _valuation_ on $\mathbb{F}$.

Given any modal FM model $\mathbb{M}=(X,\leq_{1},\leq_{2},R,V)$ and any $w\in
X$, the _satisfaction relation_ is defined as follows:

$\mathbb{M},w\Vdash p$ | iff | $w\in V(p)$
---|---|---
$\mathbb{M},w\Vdash\bot$ | : | never
$\mathbb{M},w\Vdash\top$ | : | always
$\mathbb{M},w\Vdash\varphi\land\psi$ | iff |  $\mathbb{M},w\Vdash\varphi$ and $\mathbb{M},w\Vdash\psi$
$\mathbb{M},w\Vdash\varphi\lor\psi$ | iff |  $(\forall v\geq_{1}w)(\exists u\geq_{2}v)(\mathbb{M},u\Vdash\varphi$ or $\mathbb{M},u\Vdash\psi)$
$\mathbb{M},w\Vdash\varphi\to\psi$ | iff | $(\forall v\geq_{1}w)(\mathbb{M},v\Vdash\varphi\ \Rightarrow\ \mathbb{M},v\Vdash\psi)$
$\mathbb{M},w\Vdash\Box\varphi$ | iff |  $\forall v(Rwv\ \Rightarrow\ \mathbb{M},v\Vdash\varphi)$.

We use $\llbracket\varphi\rrbracket^{\mathbb{M}}=\\{w\in
X\mid\mathbb{M},w\Vdash\varphi\\}$ to denote the _truth set_ of $\varphi$ in
$\mathbb{M}$. We say that $\varphi$ is _globally true_ on $\mathbb{M}$
(notation: $\mathbb{M}\Vdash\varphi$) if $\mathbb{M},w\Vdash\varphi$ for all
$w\in X$. We say that $\varphi$ is _valid_ on $\mathbb{F}$ (notation:
$\mathbb{F}\Vdash\varphi$) if $\varphi$ is globally true on $(\mathbb{F},V)$
for all $V$ on $X$. The semantics for inequalities and quasi-inequalities is
as follows:

$\mathbb{M}\Vdash\varphi\leq\psi$ | iff | (for all $w\in X$)($\mathbb{M},w\Vdash\varphi\ \Rightarrow\ \mathbb{M},w\Vdash\psi$)
---|---|---
$\mathbb{M}\Vdash\mathop{\mbox{\Large\&}}_{i=1}^{n}(\varphi_{i}\leq\psi_{i})\Rightarrow\varphi\leq\psi$ | iff | ($\mathbb{M}\Vdash\varphi_{i}\leq\psi_{i}$ for all $i)\ \Rightarrow\ (\mathbb{M}\Vdash\varphi\leq\psi$).

An inequality (resp. quasi-inequality) is valid on $\mathbb{F}$ if it is
globally true on $(\mathbb{F},V)$ for all $V$.

######  Proposition 3.2.

For any modal FM model $\mathbb{M}=(X,\leq_{1},\leq_{2},R,V)$ and any $w\in
X$,

$\mathbb{M}\Vdash\varphi\to\psi$ | iff |  $\llbracket\varphi\rrbracket^{\mathbb{M}}\subseteq\llbracket\psi\rrbracket^{\mathbb{M}}$ iff $\mathbb{M}\Vdash\varphi\leq\psi$
---|---|---
$\mathbb{F}\Vdash\varphi\to\psi$ | iff |  $\mathbb{F}\Vdash\varphi\leq\psi$.

##  4 Semantic Environment of our Setting

In this section, we use some algebraic structures to give the semantic
definition how the expanded modal language used in the algorithm will be
defined. The style of presentation follows [33].

###  4.1 The Heyting Algebra with Operator $\mathbb{H}_{\mathsf{RO}_{12}}$

######  Definition 4.1 (Heyting algebra with operator).

A _Heyting algebra with operator_ (HAO) is a tuple
$\mathbb{H}=(H,\bot,\top,\land,\lor,\to,\Box)$, where the $\Box$-free part is
a Heyting algebra and $\Box$ is a unary operation such that $\Box\top=\top$
and $\Box(a\land b)=\Box a\land\Box b$ for any $a,b\in H$. An HAO is
_complete_ if its Heyting algebra part is complete. An HAO is _completely
multiplicative_ if $\Box$ preserves all existing meets.

######  Definition 4.2.

For any modal FM frame $\mathbb{F}=(X,\leq_{1},\leq_{2},R)$, let the
$\mathbb{H}_{\mathsf{RO}_{12}}=(\mathsf{RO}_{12}(X),\varnothing,H,\cap,\lor_{\mathsf{RO}_{12}},\to_{\mathsf{RO}_{12}},\Box_{\mathsf{RO}_{12}})$
where $Y\lor_{\mathsf{RO}_{12}}Z:=\mathsf{I}_{1}\mathsf{C}_{2}(Y\cup Z)$,
$Y\to_{\mathsf{RO}_{12}}Z:=\mathsf{I}_{1}((X-Y)\cup Z)$.

######  Proposition 4.3.

(cf. [19, Theorem 5.6(2)]) For any modal FM frame $\mathbb{F}$,
$\mathbb{H}_{\mathsf{RO}_{12}}$ is a complete and completely multiplicative
HAO.

The essential difference between the correspondence for Kripke semantics for
intuitionistic modal logic and the current setting is that the algebra
$\mathbb{H}_{\mathsf{RO}_{12}}$ is not perfect in general, i.e. they are not
join-generated by completely join-primes.

###  4.2 The Auxiliary BAO $\mathbb{B}_{\mathsf{K}}$

Consider any modal FM-frame $\mathbb{F}=(X,\leq_{1},\leq_{2},R)$, there is
another way of viewing it, namely taking it as a trirelational frame
$\mathbb{F}_{3}=(X,\leq_{1},\leq_{2},R)$, the complex algebra of which is a
Boolean algebra with three operators $\mathbb{B}_{\mathsf{K}}$.

The formal definition of the BAO $\mathbb{B}_{\mathsf{K}}$ is given as
follows:

######  Definition 4.4.

For any modal FM-frame $\mathbb{F}=(X,\leq_{1},\leq_{2},R)$, define
$\mathbb{B}_{\mathsf{K}}=(P(X),\varnothing,W,\cap,\cup,-,\Box_{\mathsf{K}},\Box_{\leq_{1}},\Box_{\leq_{2}})$,
where $\cap,\cup,-$ are set-theoretic intersection, union and complementation
respectively, $\Box_{\mathsf{K}}(a)=\\{w\in W\mid R[w]\subseteq a\\}$, and
$\Box_{\leq_{i}}(a)=\\{w\in W\mid(\forall v\geq_{i}w)(v\in a)\\}$.

Since $\mathsf{RO}_{12}(X)\subseteq P(X)$, we have that
$e:\mathbb{H}_{\mathsf{RO}_{12}}\hookrightarrow\mathbb{B}_{\mathsf{K}}$ is an
order-embedding according to the order of the two algebras. Since in
$\mathbb{H}_{\mathsf{RO}_{12}}$, arbitrary intersections of refined regular
open subsets are again refined regular open, $e$ is completely meet-
preserving. Notice also that $\Box_{\mathsf{RO}_{12}}$ is the restriction of
$\Box_{\mathsf{K}}$ to $\mathbb{H}_{\mathsf{RO}_{12}}$. All these observations
can be summarized as follows:

######  Lemma 4.5.

$e:\mathbb{H}_{\mathsf{RO}_{12}}\hookrightarrow\mathbb{B}_{\mathsf{K}}$ is a
completely meet-preserving order-embedding such that
$e\circ\Box_{\mathsf{RO}_{12}}=\Box_{\mathsf{K}}\circ e$.

However, since $\mathbb{H}_{\mathsf{RO}_{12}}$ and $\mathbb{B}_{\mathsf{K}}$
have different definitions of join, $\mathbb{H}_{\mathsf{RO}_{12}}$ is _not_ a
sublattice of $\mathbb{B}_{\mathsf{K}}$.

We have the following corollary by [9, Proposition 7.34]):

######  Corollary 4.6.

$e:\mathbb{H}_{\mathsf{RO}_{12}}\hookrightarrow\mathbb{B}_{\mathsf{K}}$ has a
left adjoint $c:\mathbb{B}_{\mathsf{K}}\to\mathbb{H}_{\mathsf{RO}_{12}}$
defined, for every $a\in\mathbb{B}_{\mathsf{K}}$, by

$c(a)=\bigwedge_{\mathbb{H}_{\mathsf{RO}_{12}}}\\{b\in\mathbb{H}_{\mathsf{RO}_{12}}\mid
a\leq e(b)\\}.$

Clearly, $c(Y)=\mathsf{I}_{1}\mathsf{C}_{2}(Y)$ for any $\leq_{1}$-upset
$Y\subseteq X$, and $c(Y)=\mathsf{I}_{1}\mathsf{C}_{2}(\uparrow_{1}Y)$ for any
$Y\subseteq W$ where $\uparrow_{1}Y$ is the least $\leq_{1}$-upset containing
$Y$. Indeed, by definition
$c(X)=\bigwedge_{\mathbb{H}_{\mathsf{RO}_{12}}}\\{Y\in\mathsf{RO}_{12}(X)\mid
X\leq e(Y)\\}=\bigcap\\{Y\in\mathsf{RO}_{12}(X)\mid X\subseteq Y\\}$, which is
the smallest refined regular open set containing $X$. The closure operator $c$
will be called the _refined regular open closure map_ and $c(a)$ the _refined
regular open closure_ of $a$.

###  4.3 Interpreting the Additional Symbols

####  4.3.1 Nominals

Nominals are originally introduced in hybrid logic (see e.g. [5, Chapter 14]).
They are used as special propositional variables and are interpreted as
singletons, to refer to a world of the domain. In correspondence theory,
nominals are used for computing the minimal valuation of propositional
variables so as to eliminate them.

In the literature, nominals are interpreted as atoms (in complete atomic
Boolean algebra based settings), completely join-prime elements (in perfect
distributive lattice based settings), completely join-irreducible elements (in
perfect (non-distributive) lattice based settings), regular open closures of
singletons (in the setting of possibility semantics of classical normal modal
logic). The common feature is that the selected class of elements join-
generates the relevant complete lattices.

Therefore, in our setting, we need to find a subset of
$\mathbb{H}_{\mathsf{RO}_{12}}$ which join-generates the whole
$\mathbb{H}_{\mathsf{RO}_{12}}$. We take
$\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}}):=\\{c(\\{x\\})\mid x\in X\\}$ be
the set of refined regular open closures of singletons in
$\mathbb{B}_{\mathsf{K}}$, which will be shown to be the join-dense set of
$\mathbb{H}_{\mathsf{RO}_{12}}$.

Propositional base | Nominals/join-generators
---|---
perfect Boolean algebras | atoms
perfect distributive lattices | complete join-primes
perfect general lattices | complete join-irreducibles
possibility semantics | regular open closures of singletons

######  Proposition 4.7.

For any $Y\in\mathbb{H}_{\mathsf{RO}_{12}}$,

$Y=\bigvee_{\mathsf{RO}_{12}}\\{c(\\{x\\})\mid x\in
Y\\}=\bigvee_{\mathsf{RO}_{12}}\\{Z\in\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}})\mid
Z\subseteq Y\\}.$

###### Proof.

For the first equality, it is easy to see that for any $x\in Y$,
$c(\\{x\\})\subseteq c(Y)=Y$, so $\bigvee_{\mathsf{RO}_{12}}\\{c(\\{x\\})\mid
x\in Y\\}\subseteq Y$. For the other direction, for any $x\in Y$, $x\in
c(\\{x\\})\subseteq\bigvee_{\mathsf{RO}_{12}}\\{c(\\{x\\})\mid x\in Y\\}$. The
second equality is easy. ∎

####  4.3.2 Black Diamond

The black diamond comes from tense logic, which is the backward looking
diamond “there was a moment where…”. When $\Box$ is interpreted on the
relation $R$, is interpreted on the relation $R^{-1}$. These two connectives
has the following property: $\varphi\to\Box\psi$ is globally true in a model
iff $\vardiamond\varphi\to\psi$ is globally true in that model. This property
is called the _adjunction property_ algebraically. In correspondence theory,
we use the black diamond to compute the minimal valuation of a propositional
variable, and the adjunction property is exactly what we need. Therefore, our
task here is to find the left adjoint of $\Box_{\mathsf{RO}_{12}}$.

We know from lattice theory that in complete lattices, a map has a left
adjoint iff it is completely meet-preserving. Since
$\mathbb{H}_{\mathsf{RO}_{12}}$ and $\mathbb{B}_{\mathsf{K}}$ are both
complete, and
$\Box_{\mathsf{RO}_{12}}:\mathbb{H}_{\mathsf{RO}_{12}}\to\mathbb{H}_{\mathsf{RO}_{12}}$
and $\Box_{\mathsf{K}}:\mathbb{B}_{\mathsf{K}}\to\mathbb{B}_{\mathsf{K}}$ are
both completely meet-preserving, therefore they both have left adjoints, which
are denoted by ${}_{\mathsf{RO}_{12}}$ and K, respectively.

######  Lemma 4.8.

(Folklore.) ${}_{\mathsf{K}}(X)=R[X]$ for any $X\subseteq W$.

######  Lemma 4.9.

${}_{\mathsf{RO}_{12}}(Y)=(c\circ{}_{\mathsf{K}}\circ e)(Y)$.

###### Proof.

We have the following chain of equalities:

${}_{\mathsf{RO}_{12}}(Y)$ | = | $\bigwedge_{\mathsf{RO}_{12}}\\{Z\in\mathbb{H}_{\mathsf{RO}_{12}}\mid Y\leq\Box_{\mathsf{RO}_{12}}(Z)\\}$ |
---|---|---|---
| = | $\bigwedge_{\mathsf{RO}_{12}}\\{Z\in\mathbb{H}_{\mathsf{RO}_{12}}\mid e(Y)\leq(\Box_{\mathsf{K}}\circ e)(Z)\\}$ | (Lemma 4.5)
| = | $\bigwedge_{\mathsf{RO}_{12}}\\{Z\in\mathbb{H}_{\mathsf{RO}_{12}}\mid({}_{\mathsf{K}}\circ e)(Y)\leq e(Z)\\}$ |
| = | $\bigwedge_{\mathsf{RO}_{12}}\\{Z\in\mathbb{H}_{\mathsf{RO}_{12}}\mid(c\circ{}_{\mathsf{K}}\circ e)(Y)\leq Z\\}$ |
| = | $(c\circ{}_{\mathsf{K}}\circ e)(Y)$ |
| = | $(c\circ{}_{\mathsf{K}})(Y)$ |
| = | $c(R[Y])$ | (Lemma 4.8)
| = |  $\mathsf{I}_{1}\mathsf{C}_{2}(\uparrow_{1}R[Y])$. | (Corollary 4.6)

∎

##  5 Preliminaries on Algorithmic Correspondence

In the present section, we collect preliminaries on algorithmic correspondence
for modal FM semantics. We will define the expanded modal language
$\mathcal{L}^{+}$ for $\mathsf{ALBA}$, the first-order correspondence language
$\mathcal{L}^{1}$ and the refined regular open translation of
$\mathcal{L}^{+}$ into $\mathcal{L}^{1}$. Our treatment is similar to [7, 33].

###  5.1 The Expanded Modal Language $\mathcal{L}^{+}$

The expanded modal language $\mathcal{L}^{+}$ contains the basic modal
language $\mathcal{L}$ and a set $\mathsf{Nom}$ of _nominals_ , to be
interpreted as elements in $\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}})$, and
the _black connective_ , to be interpreted as the left adjoint of $\Box$. Its
definition is given as follows:

$\varphi::=p\mid\bot\mid\top\mid\mathbf{i}\mid\varphi\land\varphi\mid\varphi\lor\varphi\mid\varphi\to\varphi\mid\Box\varphi\mid\vardiamond\varphi,$

where $p\in\mathsf{Prop}$ and $\mathbf{i}\in\mathsf{Nom}$.

We extend the valuation $V$ to nominals such that
$V(\mathbf{i})\in\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}})$ and use $i$ to
denote the element that
$V(\mathbf{i})=\mathsf{I}_{1}\mathsf{C}_{2}(\uparrow_{1}\\{i\\})$.

The satisfaction relation for the additional symbols is given as follows:

######  Definition 5.1.

In any modal FM model $\mathbb{M}=(X,\leq_{1},\leq_{2},R,V)$,

$\mathbb{M},w\Vdash\mathbf{i}$ | iff |  $(\forall v\geq_{1}w)(\exists u\geq_{2}v)(i\leq_{1}u)$.
---|---|---
$\mathbb{M},w\Vdash\vardiamond\varphi$ | iff |  $(\forall v\geq_{1}w)(\exists u\geq_{2}v)(\exists t\leq_{1}u)\exists s(Rst$ and $\mathbb{M},s\Vdash\varphi)$.

Truth set and validity are defined similarly to the basic modal language.

###  5.2 The Correspondence Languages $\mathcal{L}^{1}$

In order to express the first-order correspondents of modal formulas, we need
to define the first-order correspondence language $\mathcal{L}^{1}$.

##### Syntax.

The non-logical symbols of the first-order correspondence language
$\mathcal{L}^{1}$ consists of the following:

  * •

a set of unary predicate symbols $P_{n}$, each of which corresponds to a
propositional variable $p_{n}$ and is going to be interpreted as a refined
regular open subset of the domain;

  * •

three binary relation symbols $\leq_{1},\leq_{2}$ and $R$ corresponding to the
relations denoted with the same symbol;

  * •

a set of individual symbols $i_{n}$, each of which corresponds to a nominal
$\mathbf{i}_{n}$. Notice that we allow the individual symbols $i_{n}$ to be
quantified by quantifiers $\forall i_{n},\exists i_{n}$.

###  5.3 The Refined Regular Open Translation

In the present section, we will define the _refined regular open translation_
of $\mathcal{L}^{+}$ into $\mathcal{L}^{1}$.

######  Definition 5.2 (Syntactic Refined Regular Open Closure).

Given a first-order formula $\alpha(x)$ with at most $x$ free, the _syntactic
regular open closure_ $\mathsf{RO}^{12}_{x}(\alpha(x))$ is defined as
$(\forall y\geq_{1}x)(\exists z\geq_{2}y)(\exists
z^{\prime}\leq_{1}z)\alpha(z^{\prime})$.

######  Definition 5.3 (Refined Regular Open Translation).

The regular open translation of a formula in $\mathcal{L}^{+}$ into
$\mathcal{L}^{1}$ is given as follows:

$ST_{x}(p_{i})$ | := |  $P_{i}x$;
---|---|---
$ST_{x}(\bot)$ | := |  $x\neq x$;
$ST_{x}(\top)$ | := |  $x=x$;
$ST_{x}(\mathbf{i})$ | := |  $\mathsf{RO}^{12}_{x}(i=x)$;
$ST_{x}(\varphi_{1}\land\varphi_{2})$ | := |  $ST_{x}(\varphi_{1})\land ST_{x}(\varphi_{2})$;
$ST_{x}(\varphi_{1}\lor\varphi_{2})$ | := |  $(\forall y\geq_{1}x)(\exists z\geq_{2}y)(ST_{z}(\varphi_{1})\lor ST_{z}(\varphi_{2}))$;
$ST_{x}(\varphi_{1}\to\varphi_{2})$ | := |  $(\forall y\geq_{1}x)(ST_{y}(\varphi_{1})\to ST_{y}(\varphi_{2}))$;
$ST_{x}(\Box\varphi)$ | := |  $\forall y(Rxy\to ST_{y}(\varphi))$;
$ST_{x}(\vardiamond\varphi)$ | := |  $\mathsf{RO}^{12}_{x}(\exists y(Ryx\land ST_{y}(\varphi)))$.

The refined regular open translations of inequalities $\varphi\leq\psi$ and
quasi-inequalities are given as follows (notice that they are interpreted on
the level of global truth of models):

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

$ST(\mathop{\mbox{\Large\&}}_{j=1}^{n}(\varphi_{j}\leq\psi_{j})\Rightarrow\varphi\leq\psi):=\bigwedge_{j=1}^{n}\forall
x(ST_{x}(\varphi_{j})\to ST_{x}(\psi_{j}))\to\forall x(ST_{x}(\varphi)\to
ST_{x}(\psi)).$

The following proposition justifies the translation defined above:

######  Proposition 5.4.

For any modal FM model $\mathbb{M}=(X,\leq_{1},\leq_{2},R,V)$, any $w\in X$,
any $\mathcal{L}^{+}$-formula $\varphi$, any $\mathcal{L}^{+}$-inequality
$\mathsf{Ineq}$, any $\mathcal{L}^{+}$-quasi-inequality $\mathsf{Quasi}$,

  * •

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

  * •

$\mathbb{M}\Vdash\varphi\mbox{ iff }\mathbb{M}\models\forall
xST_{x}(\varphi);$

  * •

$\mathbb{M}\Vdash\mathsf{Ineq}\mbox{ iff }\mathbb{M}\models
ST(\mathsf{Ineq});$

  * •

$\mathbb{M}\Vdash\mathsf{Quasi}\mbox{ iff }\mathbb{M}\models
ST(\mathsf{Quasi}).$

##  6 Inductive formulas

In this section, we define inductive formulas for our setting. The definition
is similar to [34].

We define _positive formulas_ with variables in $A\subseteq\mathsf{Prop}$ as
follows:

$\mathsf{POS}_{A}::=p\mid\bot\mid\top\mid\Box\mathsf{POS}_{A}\mid\mathsf{POS}_{A}\land\mathsf{POS}_{A}\mid\mathsf{POS}_{A}\lor\mathsf{POS}_{A}$

where $p\in A$.

We define the _dependence order_ on propositional variables as any irreflexive
and transitive binary relation $<_{\Omega}$ on them.

We define the _PIA formulas_ 111For the name, see e.g. [29, Remark 3.24]. with
main variable $p$ as follows:

$\mathsf{PIA}_{p}::=p\mid\bot\mid\top\mid\Box\mathsf{PIA}_{p}\mid\mathsf{POS}_{A_{p}}\to\mathsf{PIA}_{p}$

where $A_{p}=\\{q\in\mathsf{Prop}\mid q<_{\Omega}p\\}$.

We define the _inductive antecedent_ as follows:

$\mathsf{Ant}::=\mathsf{PIA}_{p}\mid\mathsf{Ant}\land\mathsf{Ant}\mid\mathsf{Ant}\lor\mathsf{Ant}$

where $p\in\mathsf{Prop}$.

We define the _inductive succedent_ as follows:

$\mathsf{Suc}::=\mathsf{POS}_{\mathsf{Prop}}\mid\mathsf{PIA}_{q}\to\mathsf{Suc}\mid\Box\mathsf{Suc}\mid\mathsf{Suc}\land\mathsf{Suc}$

where $q\in\mathsf{Prop}$.

Finally, an _$\Omega$ -inductive formula_ is a formula of the form
$\mathsf{Ant}\to\mathsf{Suc}$. An _inductive formula_ is an $\Omega$-inductive
formula for some $<_{\Omega}$.

######  Remark 6.1.

Since in our settings, we have not yet found meet-dense set of
$\mathbb{H}_{\mathsf{RO}_{12}}$, and we will only compute minimal valuations
rather than maximal valuations, we do not use the order-type and signed
generation tree style definitions like in [7]. In addition, since we do not
have diamond in the basic language, the fragment that we have is much smaller
than typical definitions of inductive formulas in some existing settings like
[7].

##  7 The Algorithm $\mathsf{ALBA}$

In the present section, we define the algorithm $\mathsf{ALBA}$ which compute
the first-order correspondence of the input formula, in the style of [7, 34].

The algorithm $\mathsf{ALBA}$ executes in three stages. $\mathsf{ALBA}$
receives a formula $\mathsf{Ant}\to\mathsf{Suc}$ as input and transforms it
into the inequality $\mathsf{Ant}\leq\mathsf{Suc}$.

  1. 1.

Preprocessing and First approximation:

    1. (a)

We apply the following _distribution rules_ exhaustively:

       * •

In $\mathsf{Ant}$, rewrite every subformula of the former form into the latter
form:

         * –

$(\beta\lor\gamma)\land\alpha$, $(\beta\land\alpha)\lor(\gamma\land\alpha)$

         * –

$\alpha\land(\beta\lor\gamma)$, $(\alpha\land\beta)\lor(\alpha\land\gamma)$

       * •

In $\mathsf{Suc}$, rewrite every subformula of the former form into the latter
form:

         * –

$(\beta\land\gamma)\lor\alpha$, $(\beta\lor\alpha)\land(\gamma\lor\alpha)$

         * –

$\alpha\lor(\beta\land\gamma)$, $(\alpha\lor\beta)\land(\alpha\lor\gamma)$

         * –

$\alpha\to\beta\land\gamma$, $(\alpha\to\beta)\land(\alpha\to\gamma)$

         * –

$\Box(\alpha\land\beta)$, $\Box\alpha\land\Box\beta$

    2. (b)

Apply the _splitting rules_ :

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

Now for each obtained inequality $\varphi_{i}\leq\psi_{i}$, We apply the
_first-approximation rule_ :

$\mathbf{i}_{0}\leq\varphi_{i}\ \Rightarrow\
\mathbf{i}_{0}\leq\psi_{i}\varphi_{i}\leq\psi_{i}$

Now we call each quasi-inequality $\mathbf{i}_{0}\leq\varphi_{i}\ \Rightarrow\
\mathbf{i}_{0}\leq\psi_{i}$ a _system_ , and use $\mathsf{S}$ to denote a
meta-conjunction of inequalities. When $\mathsf{S}$ is empty, we denote it as
$\varnothing$.

  2. 2.

The reduction-elimination cycle:

In this stage, for each system $\mathbf{i}_{0}\leq\varphi_{i}\ \Rightarrow\
\mathbf{i}_{0}\leq\psi_{i}$, we apply the following rules to eliminate all the
propositional variables:

    1. (a)

_Splitting rules_ :

$(\mathsf{S}\ \Rightarrow\ \alpha\leq\beta)\ \ \ (\mathsf{S}\ \Rightarrow\
\alpha\leq\gamma)\mathsf{S}\ \Rightarrow\ \alpha\leq\beta\land\gamma$
$\mathsf{S}\ \&\ \alpha\leq\beta\ \&\ \alpha\leq\gamma\ \Rightarrow\
\varphi\leq\psi\mathsf{S}\ \&\ \alpha\leq\beta\land\gamma\ \Rightarrow\
\varphi\leq\psi$ $(\mathsf{S}\ \Rightarrow\ \alpha\leq\gamma)\ \ \
(\mathsf{S}\ \Rightarrow\ \beta\leq\gamma)\mathsf{S}\ \Rightarrow\
\alpha\lor\beta\leq\gamma$ $\mathsf{S}\ \&\ \alpha\leq\gamma\ \&\
\beta\leq\gamma\ \Rightarrow\ \varphi\leq\psi\mathsf{S}\ \&\
\alpha\lor\beta\leq\gamma\ \Rightarrow\ \varphi\leq\psi$

    2. (b)

_Residuation rules_ :

$\mathsf{S}\ \Rightarrow\ \vardiamond\alpha\leq\beta\mathsf{S}\ \Rightarrow\
\alpha\leq\Box\beta$ $\mathsf{S}\ \&\ \vardiamond\alpha\leq\beta\ \Rightarrow\
\varphi\leq\psi\mathsf{S}\ \&\ \alpha\leq\Box\beta\ \Rightarrow\
\varphi\leq\psi$ $\mathsf{S}\ \Rightarrow\
\alpha\land\beta\leq\gamma\mathsf{S}\ \Rightarrow\ \alpha\leq\beta\to\gamma$
$\mathsf{S}\ \&\ \alpha\land\beta\leq\gamma\ \Rightarrow\
\varphi\leq\psi\mathsf{S}\ \&\ \alpha\leq\beta\to\gamma\ \Rightarrow\
\varphi\leq\psi$

    3. (c)

_Approximation rule_ :

$\mathsf{S}\ \&\ \mathbf{i}\leq\varphi\ \Rightarrow\
\mathbf{i}\leq\psi\mathsf{S}\ \Rightarrow\ \varphi\leq\psi$

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

    4. (d)

_Deleting rules_ :

$\mathsf{S}\ \Rightarrow\ \varphi\leq\psi\mathsf{S}\ \&\ \alpha\leq\top\
\Rightarrow\ \varphi\leq\psi$ $\varnothing\ \Rightarrow\
\alpha\leq\top\mathsf{S}\ \Rightarrow\ \alpha\leq\top$

    5. (e)

_Right-handed Ackermann rule_. This rule eliminates propositional variables
and is the core of the algorithm:

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

where:

      1. i.

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

      2. ii.

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

      3. iii.

$\theta:=\theta_{1}\lor\ldots\lor\theta_{n}$.

  3. 3.

Output: If in Stage 2, the algorithm gets stuck for some systems, i.e. some
propositional variables cannot be eliminated, then the algorithm stops and
output “failure”. Otherwise, each initial system after the first approximation
rule has been reduced to a set of pure quasi-inequalities
Reduce$(\mathbf{i}_{0}\leq\varphi_{i}\ \Rightarrow\
\mathbf{i}_{0}\leq\psi_{i})$, and then the output is a set of pure quasi-
inequalities $\bigcup_{i\in I}$Reduce$(\mathbf{i}_{0}\leq\varphi_{i}\
\Rightarrow\ \mathbf{i}_{0}\leq\psi_{i})$. Then we can use the conjunction of
the refined regular open translations of the quasi-inequalities to obtain the
first-order correspondence (notice that in the standard translation of each
quasi-inequality, we need to universally quantify over all the individual
variables).

######  Example 7.1.

Here we give an example. For the sake of clarity we add propositional
quantifiers and nominal quantifiers before the quasi-inequality.

$\forall p(\Box p\to p)$
$\forall p(\Box p\leq p)$
$\forall p\forall\mathbf{i}(\mathbf{i}\leq\Box p\ \Rightarrow\mathbf{i}\leq
p)$
$\forall p\forall\mathbf{i}(\vardiamond\mathbf{i}\leq p\
\Rightarrow\mathbf{i}\leq p)$
$\forall\mathbf{i}(\mathbf{i}\leq\vardiamond\mathbf{i})$
$\forall i\forall x(ST_{x}(\mathbf{i})\to ST_{x}(\vardiamond\mathbf{i}))$
$\forall i\forall x(\mathsf{RO}^{12}_{x}(i=x)\to\mathsf{RO}^{12}_{x}(\exists
y(Ryx\land\mathsf{RO}^{12}_{x}(i=y))))$

##  8 Success

In the present section, we show the success of $\mathsf{ALBA}$ on any
inductive formula $\varphi\to\psi$.

######  Theorem 8.1.

$\mathsf{ALBA}$ succeeds on any inductive formula $\varphi\to\psi$ and outputs
a set of pure quasi-inequalities and a first-order formula.

###### Proof.

We check the shape of the inequalitys or systems in each stage, for the input
formula $\mathsf{Ant}\to\mathsf{Suc}$:

Stage 1.

After applying the distribution rules, it is easy to see that $\mathsf{Ant}$
becomes the form $\bigvee\bigwedge\mathsf{PIA}_{p}$, and $\mathsf{Suc}$
becomes of the form $\bigwedge\mathsf{Suc}^{\prime}$, where

$\mathsf{Suc}^{\prime}::=\mathsf{POS}_{\mathsf{Prop}}\mid\mathsf{PIA}_{q}\to\mathsf{Suc}^{\prime}\mid\Box\mathsf{Suc}^{\prime}.$

Then by applying the splitting rules, we get a set of inequalities of the form
$\bigwedge\mathsf{PIA}_{p}\leq\mathsf{Suc}^{\prime}$.

After the first approximation rule, we get systems of the form
$\mathbf{i}_{0}\leq\bigwedge\mathsf{PIA}_{p}\ \Rightarrow\
\mathbf{i}_{0}\leq\mathsf{Suc}^{\prime}$.

Stage 2. In this stage, we deal with each system
$\mathbf{i}_{0}\leq\bigwedge\mathsf{PIA}_{p}\ \Rightarrow\
\mathbf{i}_{0}\leq\mathsf{Suc}^{\prime}$.

For the inequality $\mathbf{i}_{0}\leq\bigwedge\mathsf{PIA}_{p}$, by first
applying the splitting rule for $\land$ and then exhaustively applying the
residuation rules for $\Box$ and $\to$, we get inequalities of the form
$\mathsf{MinVal}_{p}\leq p$ or $\mathsf{MinVal}_{p}\leq\top$ or
$\mathsf{MinVal}_{p}\leq\bot$, where

$\mathsf{MinVal}_{p}::=\mathbf{i}_{0}\mid\vardiamond\mathsf{MinVal}_{p}\mid\mathsf{MinVal}_{p}\land\mathsf{POS}_{A_{p}},$

where $A_{p}=\\{q\in\mathsf{Prop}\mid q<_{\Omega}p\\}$.

Now we deal with the $\mathbf{i}_{0}\leq\mathsf{Suc}^{\prime}$ part.

  * •

If the system is of the form $\mathsf{S}\ \&\
\mathop{\mbox{\Large\&}}(\mathsf{MinVal}_{p}\leq p)\ \Rightarrow\
\mathbf{i}_{0}\leq\mathsf{PIA}_{q}\to\mathsf{Suc}^{\prime}$, then we have the
following execution of $\mathsf{ALBA}$:

$\mathsf{S}\ \&\ \mathop{\mbox{\Large\&}}(\mathsf{MinVal}_{p}\leq p)\
\Rightarrow\ \mathbf{i}_{0}\land\mathsf{PIA}_{q}\leq\mathsf{Suc}^{\prime}$
$\mathsf{S}\ \&\ \mathop{\mbox{\Large\&}}(\mathsf{MinVal}_{p}\leq p)\ \&\
\mathbf{j}\leq\mathbf{i}_{0}\land\mathsf{PIA}_{q}\ \Rightarrow\
\mathbf{j}\leq\mathsf{Suc}^{\prime}$
$\mathsf{S}\ \&\ \mathop{\mbox{\Large\&}}(\mathsf{MinVal}_{p}\leq p)\ \&\
\mathbf{j}\leq\mathbf{i}_{0}\ \&\ \mathbf{j}\leq\mathsf{PIA}_{q}\ \Rightarrow\
\mathbf{j}\leq\mathsf{Suc}^{\prime}$
$\mathsf{S}\ \&\ \mathop{\mbox{\Large\&}}(\mathsf{MinVal}_{p}\leq p)\ \&\
\mathbf{j}\leq\mathbf{i}_{0}\ \Rightarrow\
\mathbf{j}\leq\mathsf{Suc}^{\prime}.$

  * •

If the system is of the form $\mathop{\mbox{\Large\&}}(\mathsf{MinVal}_{p}\leq
p)\ \Rightarrow\ \mathbf{i}_{0}\leq\Box\mathsf{Suc}^{\prime}$, then we have
the following execution of $\mathsf{ALBA}$:

$\mathop{\mbox{\Large\&}}(\mathsf{MinVal}_{p}\leq p)\ \Rightarrow\
\vardiamond\mathbf{i}_{0}\leq\mathsf{Suc}^{\prime}$
$\mathop{\mbox{\Large\&}}(\mathsf{MinVal}_{p}\leq p)\ \&\
\mathbf{j}\leq\vardiamond\mathbf{i}_{0}\ \Rightarrow\
\mathbf{j}\leq\mathsf{Suc}^{\prime}$

Therefore, by the reduction strategies above, we get a quasi-inequality of the
form (here $\mathsf{Pure}$ is a meta-conjunction of inequalities without
propositional variables):

$\mathop{\mbox{\Large\&}}(\mathsf{MinVal}_{p}\leq p)\ \&\ \mathsf{Pure}\
\Rightarrow\ \mathbf{j}\leq\mathsf{POS}_{\mathsf{Prop}}.$

Now we can apply the right-handed Ackermann rule to an $\Omega$-miminal
variable $q$ to eliminate it. Since there are only finitely many propositional
variables, we can always find another $\Omega$-miminal variable to eliminate.
Finally we eliminate all propositional variables and get pure quasi-
inequalities and the refined regular open translation. ∎

##  9 Soundness

In this section, we prove the soundness of $\mathsf{ALBA}$ with respect to
modal FM frames. The basic proof structure is similar to [7, 8, 34].

######  Theorem 9.1 (Soundness).

If $\mathsf{ALBA}$ runs according to the success proof in the previous section
on an input inductive formula $\varphi\to\psi$ and outputs a first-order
formula $\mathsf{FO(\varphi\to\psi)}$, then for any modal FM frame
$\mathbb{F}=(X,\leq_{1},\leq_{2},R)$,

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

###### Proof.

The proof goes similarly to [7, Theorem 8.1]. Let $\varphi\to\psi$ denote the
input formula, $\\{\mathbf{i}_{0}\leq\varphi_{i}\ \Rightarrow\
\mathbf{i}_{0}\leq\psi_{i}\\}_{i\in I}$ denote the set of systems after the
first-approximation rule, let $\\{\mbox{Reduce}(\mathbf{i}_{0}\leq\varphi_{i}\
\Rightarrow\ \mathbf{i}_{0}\leq\psi_{i})\\}_{i\in I}$ denote the sets of
quasi-inequalities after Stage 2, let $\mathsf{FO(\varphi\to\psi)}$ denote the
refined regular open translation of the quasi-inequalities in Stage 3 into
first-order formulas, then it suffices to show the equivalence from (1) to (4)
given below:

$\displaystyle\mathbb{F}\Vdash\varphi\to\psi$ (1)
$\displaystyle\mathbb{F}\Vdash\mathbf{i}_{0}\leq\varphi_{i}\ \Rightarrow\
\mathbf{i}_{0}\leq\psi_{i},\mbox{ for all }i\in I$ (2)
$\displaystyle\mathbb{F}\Vdash\mbox{Reduce}(\mathbf{i}_{0}\leq\varphi_{i}\
\Rightarrow\ \mathbf{i}_{0}\leq\psi_{i}),\mbox{ for all }i\in I$ (3)
$\displaystyle\mathbb{F}\vDash\mathsf{FO(\varphi\to\psi)}$ (4)

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

The equivalence between (2) and (3) follows from Propositions 9.3, 9.4;

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

In what follows, we will prove the soundness of each rule in each stage.

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

The distribution rules and the splitting rules are sound in both directions in
$\mathbb{F}$.

###### Proof.

For the soundness of the distribution rules, it follows from the validity of
the following equivalences in $\mathbb{F}$:

  * •

$(\alpha\lor\beta)\land\gamma\leftrightarrow(\alpha\land\gamma)\lor(\beta\land\gamma)$;

  * •

$\alpha\land(\beta\lor\gamma)\leftrightarrow(\alpha\land\beta)\lor(\alpha\land\gamma)$;

  * •

$\Box(\alpha\land\beta)\leftrightarrow\Box\alpha\land\Box\beta$;

  * •

$(\alpha\land\beta)\lor\gamma\leftrightarrow(\alpha\lor\gamma)\land(\beta\lor\gamma)$;

  * •

$\alpha\lor(\beta\land\gamma)\leftrightarrow(\alpha\lor\beta)\land(\alpha\lor\gamma)$;

  * •

$(\alpha\to\beta\land\gamma)\leftrightarrow(\alpha\to\beta)\land(\alpha\to\gamma)$.

For the soundness of the splitting rules, it follows from the following fact:

$\mathbb{F}\vDash\alpha\leq\beta\land\gamma\mbox{ iff
}(\mathbb{F}\vDash\alpha\leq\beta\mbox{ and
}\mathbb{F}\vDash\alpha\leq\gamma);$
$\mathbb{F}\vDash\alpha\lor\beta\leq\gamma\mbox{ iff
}(\mathbb{F}\vDash\alpha\leq\gamma\mbox{ and
}\mathbb{F}\vDash\beta\leq\gamma).$

For the soundness of the first-approximation rule, by Proposition 4.7,

$V(\varphi_{i})=\bigvee_{\mathsf{RO}_{12}}\\{Z\in\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}})\mid
Z\subseteq V(\varphi_{i})\\}.$

Now we have the following chain of equivalences:

| $\mathbb{F}\Vdash\varphi_{i}\leq\psi_{i}$
---|---
iff | for any $V$, $\bigvee_{\mathsf{RO}_{12}}\\{Z\in\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}})\mid Z\subseteq V(\varphi_{i})\\}\subseteq V(\psi_{i})$
iff | for any $V$, $(\forall Z\in\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}})\mbox{ s.t. }Z\subseteq V(\varphi_{i}))(Z\subseteq V(\psi_{i}))$
iff | for any $V$, $(\forall Z\in\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}})(Z\subseteq V(\varphi_{i})\ \Rightarrow\ Z\subseteq V(\psi_{i}))$
iff | for any $V^{\prime}$, $V^{\prime}(\mathbf{i})\subseteq V^{\prime}(\varphi_{i})\ \Rightarrow\ V^{\prime}(\mathbf{i})\subseteq V^{\prime}(\psi_{i})$
iff |  $\mathbb{F}\Vdash\mathbf{i}\leq\varphi_{i}\ \Rightarrow\ \mathbf{i}\leq\psi_{i}$.

∎

For the soundness of each rule in Stage 2, we introduce the following
notations: for each rule, before its application we have a system $\mathsf{S}\
\Rightarrow\mathsf{Ineq}$, after its application we get a system
$\mathsf{S}^{\prime}\ \Rightarrow\mathsf{Ineq}^{\prime}$ (indeed, for the
splitting rules we might have two systems after the application, but their
soundness are trivial), the soundness of Stage 2 is then the equivalence of
the following:

  * •

$\mathbb{F}\Vdash\mathsf{S}\ \Rightarrow\mathsf{Ineq}$

  * •

$\mathbb{F}\Vdash\mathsf{S}^{\prime}\ \Rightarrow\mathsf{Ineq}^{\prime}$

It suffices to show the following property for the splitting rules,
residuation rules and the deleting rules:

For any $\mathbb{F}$, any $V$,

$\mathbb{F},V\Vdash\mathsf{S}\ \Rightarrow\mathsf{Ineq}$ iff
$\mathbb{F},V\Vdash\mathsf{S}^{\prime}\ \Rightarrow\mathsf{Ineq}^{\prime}.$

For the first-approximation rule, we prove it directly.

For the right-handed Ackermann rule, we also prove it directly.

######  Proposition 9.3.

The splitting rules, the approximation rule, the residuation rules and the
deleting rules in Stage 2 are sound in both directions in $\mathbb{F}$.

###### Proof.

The soundness proofs for the splitting rules and the residuation rules are
similar to the soundness of the same rules in [7].

  * •

For the splitting rules, it follows from the following equivalence: for any
modal FM frame $\mathbb{F}$, any valuation $V$ on $\mathbb{F}$,

$\mathbb{F},V\Vdash\alpha\leq\beta\land\gamma\mbox{ iff
}\mathbb{F},V\Vdash\alpha\leq\beta\mbox{ and
}\mathbb{F},V\Vdash\alpha\leq\gamma;$
$\mathbb{F},V\Vdash\alpha\lor\beta\leq\gamma\mbox{ iff
}\mathbb{F},V\Vdash\alpha\leq\gamma\mbox{ and
}\mathbb{F},V\Vdash\beta\leq\gamma.$

  * •

For the residuation rules, it follows from the following equivalence: for any
modal FM frame $\mathbb{F}$, any valuation $V$ on $\mathbb{F}$,

    * –

$\mathbb{F},V\Vdash\alpha\leq\Box\beta\mbox{ iff
}\mathbb{F},V\Vdash\vardiamond\alpha\leq\beta;$

    * –

$\mathbb{F},V\Vdash\alpha\leq\beta\to\gamma\mbox{ iff
}\mathbb{F},V\Vdash\alpha\land\beta\leq\gamma.$

The equivalences above follow from the fact that the interpretations of and
$\Box$ form an adjunction pair, and the interpretations of $\land$ and $\to$
form a residuation pair.

  * •

For the approximation rule, the soundness proof is similar to the first-
approximation rule: for any modal FM frame $\mathbb{F}$, any valuation $V$,

| $\mathbb{F},V\Vdash\varphi_{i}\leq\psi_{i}$
---|---
iff | $V(\varphi_{i})\subseteq V(\psi_{i})$
iff | $\bigvee_{\mathsf{RO}_{12}}\\{Z\in\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}})\mid Z\subseteq V(\varphi_{i})\\}\subseteq V(\psi_{i})$
iff | $(\forall Z\in\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}})\mbox{ s.t. }Z\subseteq V(\varphi_{i}))(Z\subseteq V(\psi_{i}))$
iff |  $(\forall Z\in\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}})(Z\subseteq V(\varphi_{i})\ \Rightarrow\ Z\subseteq V(\psi_{i}))$.

Therefore, if $\mathbb{F}\Vdash\mathsf{S}\ \Rightarrow\
\varphi_{i}\leq\psi_{i}$, then for any $V$, if $\mathbb{F},V\Vdash\mathsf{S}$
and $V(\mathbf{i})\subseteq V(\varphi_{i})$, then $V(\varphi_{i})\subseteq
V(\psi_{i})$, so for
$V(\mathbf{i})\in\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}})$, from the above
equivalences we have $V(\mathbf{i})\subseteq V(\psi_{i})$, i.e.
$\mathbb{F},V\Vdash\mathbf{i}\leq\psi_{i}$. Thus $\mathbb{F}\Vdash\mathsf{S}\
\&\ \mathbf{i}\leq\varphi_{i}\ \Rightarrow\ \mathbf{i}\leq\psi_{i}$.

If $\mathbb{F}\Vdash\mathsf{S}\ \&\ \mathbf{i}\leq\varphi_{i}\ \Rightarrow\
\mathbf{i}\leq\psi_{i}$, then for any valuation $V$, if
$\mathbb{F},V\Vdash\mathsf{S}$, then for any
$Z\in\mathsf{Nom}(\mathbb{H}_{\mathsf{RO}_{12}})$, if $Z\subseteq
V(\varphi_{i})$, take $V^{\prime}:=V^{\mathbf{i}}_{Z}$, then since
$\mathbf{i}$ does not occur in $\mathsf{S}$, we have
$\mathbb{F},V^{\prime}\Vdash\mathsf{S}$. We also have
$V^{\prime}(\mathbf{i})=Z\subseteq V(\varphi_{i})=V^{\prime}(\varphi_{i})$, so
from $\mathbb{F}\Vdash\mathsf{S}\ \&\ \mathbf{i}\leq\varphi_{i}\ \Rightarrow\
\mathbf{i}\leq\psi_{i}$ we get $Z=V^{\prime}(\mathbf{i})\subseteq
V^{\prime}(\psi_{i})=V(\psi_{i})$, therefore
$\mathbb{F},V\Vdash\varphi_{i}\leq\psi_{i}$. Therefore we get
$\mathbb{F}\Vdash\mathsf{S}\ \Rightarrow\ \varphi_{i}\leq\psi_{i}$.

  * •

The soundness of the deleting rule is trivial, since $\alpha\leq\top$ always
holds in any modal FM model.

∎

######  Proposition 9.4.

The right-handed Ackermann rule is sound in $\mathbb{F}$.

###### Proof.

Without loss of generality we assume that $n=1$ and $m=1$. Then it suffices to
show the following equivalence:

  * •

$\mathbb{F}\Vdash\theta\leq p\ \&\ \eta\leq\iota\ \Rightarrow\
\varphi\leq\psi$;

  * •

$\mathbb{F}\Vdash\eta(\theta/p)\leq\iota(\theta/p)\ \Rightarrow\
\varphi(\theta/p)\leq\psi(\theta/p)$.

$\Downarrow$: Assume that $\mathbb{F}\Vdash\theta\leq p\ \&\ \eta\leq\iota\
\Rightarrow\ \varphi\leq\psi.$ Then for any valuation $V$ on $\mathbb{F}$, if
$\mathbb{F},V\Vdash\eta(\theta/p)\leq\iota(\theta/p),$ then take
$V^{\prime}=V^{p}_{V(\theta)}$, then since $p$ does not occur in $\theta$, we
have $V^{\prime}(\theta)=V(\theta)=V^{\prime}(p),$ therefore
$V(\eta(\theta/p))=V^{\prime}(\eta(\theta/p))=V^{\prime}(\eta),$ similarly
$V(\iota(\theta/p))=V^{\prime}(\iota),$ so from
$\mathbb{F},V\Vdash\eta(\theta/p)\leq\iota(\theta/p)$ we get
$V^{\prime}(\eta)\subseteq V^{\prime}(\iota).$ Therefore
$\mathbb{F},V^{\prime}\Vdash\varphi\leq\psi.$ Therefore
$V^{\prime}(\varphi)\subseteq V^{\prime}(\psi)$. Similar to $\eta$ and $\iota$
we get $V^{\prime}(\varphi)=V(\varphi(\theta/p))$ and
$V^{\prime}(\psi)=V(\psi(\theta/p)),$ so
$\mathbb{F},V\Vdash\varphi(\theta/p)\leq\psi(\theta/p).$ By the arbitrariness
of $V$ we get $\mathbb{F}\Vdash\eta(\theta/p)\leq\iota(\theta/p)\ \Rightarrow\
\varphi(\theta/p)\leq\psi(\theta/p).$

$\Uparrow$: Assume $\mathbb{F}\Vdash\eta(\theta/p)\leq\iota(\theta/p)\
\Rightarrow\ \varphi(\theta/p)\leq\psi(\theta/p).$ Then for any valuation $V$
on $\mathbb{F}$, if $\mathbb{F},V\Vdash\theta\leq p\ \&\ \eta\leq\iota,$ then
$V(\theta)\subseteq V(p),V(\eta)\subseteq V(\iota).$ Therefore by the polarity
of $p$ in $\eta(\theta/p)$ and $\iota(\theta/p)$ we have that
$V(\eta(\theta/p))\subseteq V(\eta)\subseteq V(\iota)\subseteq
V(\iota(\theta/p)).$ So from
$\mathbb{F}\Vdash\eta(\theta/p)\leq\iota(\theta/p)\ \Rightarrow\
\varphi(\theta/p)\leq\psi(\theta/p)$ we get $V(\varphi)\subseteq
V(\varphi(\theta/p))\subseteq V(\psi(\theta/p))\subseteq V(\psi),$ so
$\mathbb{F},V\Vdash\varphi\leq\psi$. Therefore by the arbitrariness of $V$ we
get $\mathbb{F}\Vdash\theta\leq p\ \&\ \eta\leq\iota\ \Rightarrow\
\varphi\leq\psi.$ ∎

##  10 Conclusions

In this paper, we study the correspondence theory of intuitionistic modal
logic in modal Fairtlough-Mendler semantics, which is the intuitionistic modal
counterpart of possibility semantics. Our study can be regarded as the study
of correspondence theory for complete Heyting algebras with complete operators
which are not necessarily perfect.

We proposed the general principles to choose the interpretations of the
expanded modal language used in the algorithm $\mathsf{ALBA}$, and apply it in
the current setting. Therefore, we interpret the nominals in our setting as
the refined regular open closures of singletons, which is join-dense in
$\mathbb{H}_{\mathsf{RO}_{12}}$ and can be expressed in a first-order way.

For future directions, we mention the following:

  * •

In the present paper, we use a join-dense set of
$\mathbb{H}_{\mathsf{RO}_{12}}$ to interpret the nominals. Whether a meet-
dense set of $\mathbb{H}_{\mathsf{RO}_{12}}$ which can be expressed in a
first-order way can be found is a question related to whether we can expand
the fragment of inductive formulas here, which is also related to finding
correspondents of the $\mathsf{KC}$ formula $\neg p\lor\neg\neg p$ and the
$\mathsf{LC}$ formula $(p\to q)\lor(q\to p)$ in the present semantic setting.

  * •

In the present paper, we only have $\Box$ as the modality, since it interacts
well with arbitrary intersection. A future direction is to find a way to
incorporate $\Diamond$ into the picture.

  * •

In the present paper, we consider complete Heyting algebra expansions,
therefore it is natural to also consider the correspondence theory of complete
lattice expansions which are not necessarily perfect.

  * •

In the present paper, we do not consider the canonicity and completeness
concepts related to the intuitionistic modal version of possibility semantics,
which is a future direction.

##### Acknowledgement

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

## References

  * [1] E. Beth.  Semantic construction of intuitionistic logic.  Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, 19:357–388, 1956.
  * [2] G. Bezhanishvili and W. H. Holliday.  Locales, nuclei, and Dragalin frames.  Advances in Modal Logic, 11:177–196, 2016.
  * [3] G. Bezhanishvili and W. H. Holliday.  A semantic hierarchy for intuitionistic logic.  Indagationes Mathematicae, 30(3):403–469, 2019.
  * [4] N. Bezhanishvili and W. H. Holliday.  Choice-free stone duality.  Journal of Symbolic Logic, 85(1):109–148, 2020.
  * [5] P. Blackburn, J. F. van Benthem, and F. Wolter.  Handbook of modal logic, volume 3.  Elsevier, 2006.
  * [6] W. Conradie, S. Ghilardi, and A. Palmigiano.  Unified correspondence.  In A. Baltag and S. Smets, editors, Johan van Benthem on Logic and Information Dynamics, volume 5 of Outstanding Contributions to Logic, pages 933–975. Springer International Publishing, 2014.
  * [7] W. Conradie and A. Palmigiano.  Algorithmic correspondence and canonicity for distributive modal logic.  Annals of Pure and Applied Logic, 163(3):338 – 376, 2012.
  * [8] W. Conradie and A. Palmigiano.  Constructive canonicity of inductive inequalities.  Logical Methods in Computer Science, Volume 16, Issue 3, Aug. 2020.
  * [9] B. Davey and H. Priestley.  Introduction to lattices and order.  Cambridge University Press, 2002.
  * [10] Y. Ding and W. H. Holliday.  Another problem in possible world semantics.  In N. Olivetti, R. Verbrugge, S. Negri, and G. Sandu, editors, 13th Conference on Advances in Modal Logic, AiML 2020, Helsinki, Finland, August 24-28, 2020, pages 149–168. College Publications, 2020.
  * [11] A. G. Dragalin.  Matematicheskii Intuitsionizm: Vvedenie v Teoriyu Dokazatelstv.  Matematicheskaya Logika i Osnovaniya Matematiki. Nauka, Moscow, 1979.
  * [12] A. G. Dragalin.  Mathematical intuitionism: introduction to proof theory, volume 67 of Translations of Mathematical Monographs.  American Mathematical Society, Providence, RI, 1988.
  * [13] M. Fairtlough and M. Mendler.  Propositional lax logic.  Information and Computation, 137(1):1–33, 1997.
  * [14] V. Goranko and D. Vakarelov.  Elementary canonical formulae: Extending Sahlqvist’s theorem.  Annals of Pure and Applied Logic, 141(1-2):180–217, 2006.
  * [15] M. Harrison-Trainor.  Worldizations of possibility models.  UC Berkeley Working Paper in Logic and the Methodology of Science, 2016.  URL http://escholarship.org/uc/item/881757qn.
  * [16] M. Harrison-Trainor.  First-order possibility models and finitary completeness proofs.  The Review of Symbolic Logic, 12(4):637–662, 2019.
  * [17] W. H. Holliday.  Partiality and adjointness in modal logic.  Advances in Modal Logic, 10:313–332, 2014.
  * [18] W. H. Holliday.  Possiility semantics.  Selected Topics from Contemporary Logics. College Publications, 2021.
  * [19] W. H. Holliday.  Possibility frames and forcing for modal logic.  UC Berkeley Working Paper in Logic and the Methodology of Science, June 2016.  URL http://escholarship.org/uc/item/9v11r0dq.
  * [20] I. Humberstone.  From worlds to possibilities.  Journal of Philosophical Logic, 10(3):313–339, 1981.
  * [21] P. Johnstone.  Stone Spaces.  Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.
  * [22] D. S. Macnab.  An Algebraic Study of Modal Operators on Heyting Algebras with Applications to Topology and Sheafification.  PhD thesis, PhD thesis, University of Aberdeen, 1976.
  * [23] D. S. Macnab.  Modal operators on heyting algebras.  Algebra Universalis, 12:5–29, 1981.
  * [24] G. Massas.  Possibility spaces, Q-completions and Rasiowa-Sikorski lemmas for non-classical logics.  Master’s thesis, University of Amsterdam, 2016.
  * [25] G. Massas.  Possibility semantics for IPC.  draft, 2018.
  * [26] G. Massas.  B-frame duality.  UC Berkeley Working Paper in Logic and the Methodology of Science, 2022.  URL https://escholarship.org/uc/item/78v634pc.
  * [27] R. Montague.  Universal grammar.  Theoria, 36(3):373–398, 1970.
  * [28] E. Pacuit.  Neighborhood semantics for modal logic.  Short Textbooks in Logic. Springer, Dordrecht, 2017.
  * [29] A. Palmigiano, S. Sourabh, and Z. Zhao.  Sahlqvist theory for impossible worlds.  Journal of Logic and Computation, 27(3):775–816, 2017.
  * [30] D. Scott.  Advice on modal logic, pages 143–173.  Springer Netherlands, Dordrecht, 1970.
  * [31] J. van Benthem, N. Bezhanishvili, and W. H. Holliday.  A bimodal perspective on possibility semantics.  Journal of Logic and Computation, 27(5):1353–1389, 2017.
  * [32] K. Yamamoto.  Modal correspondence theory for possibility semantics.  Journal of Logic and Computation, 27(8):2411–2430, 2016.
  * [33] Z. Zhao.  Algorithmic correspondence and canonicity for possibility semantics.  Journal of Logic and Computation, 31(2):523–572, 02 2021.
  * [34] Z. Zhao.  Correspondence theory for generalized modal algebras.  In A. Ciabattoni, E. Pimentel, and R. J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation, pages 53–69, Cham, 2022\. Springer International Publishing.


# Active Caustics

Rahul Chajwa 1,2, Rajarshi 2, Sriram Ramaswamy 3, Rama Govindarajan 2
1Department of Bioengineering, Stanford University, Stanford CA 94305 USA.
2International Centre for Theoretical Sciences, Tata Institute of Fundamental
Research, Bengaluru 560 089
3Centre for Condensed Matter Theory, Department of Physics, Indian Institute
of Science, Bengaluru 560 012

###### Abstract

When heavy particles in turbulent flow are centrifuged out of vortices they
cluster to form singular features in the number density [Phys Fluids 27,
033305 (2015)], termed caustics for their resemblance to focal surfaces in
optics.We show here that self-propelled particles (SPPs) with Reynolds number
$Re=0$ and thus no mechanical inertia display similar behaviour, thanks to the
persistence of their motion in the direction of their intrinsic orientation.
Using singular perturbation analysis and numerical studies we establish that
SPPs form caustics at a critical distance from the origin of a point vortex.
To capture the dynamics in a generic vortical flow we study SPPs advected by
Navier-Stokes turbulence and find pronounced caustics in straining regions,
for intermediate values of a non-dimensional self-propulsion velocity. Our
work offers a route to singularly high local concentrations in a
macroscopically dilute suspension of zero-Re swimmers, with potentially game-
changing implications for communication and sexual reproduction. An intriguing
open direction is whether the active turbulence of a suspension of swimming
microbes could serve to generate caustics in its own concentration.

##  I Introduction

The motion of particles in an ambient flow governs climate phenomena such as
the formation of droplets in clouds PINSKY19971177 ; Ardekani2012 ;
cloud_microphysics , the drift of atmospheric pollutants Fernando2010 , and
the biological pump of the oceans Boyd , and there is a wide range of
industrial processes where particulate flows are central SAMBORSKA2022110960 .
When particles have appreciable inertia, the coupling between the local flow
profile and particle velocity can lead to long-wavelength inhomogeneities in
particle number density Lillo2004 . Heavy particles in a background turbulent
flow are known to get centrifuged out of regions of vorticity, and so ambient
vortices promote particle collisions, aggregation, and caustics MR1983 ;
Maxey1986 ; Croor2015 ; Wilkinson_2005 , offering a plausible mechanism for
droplet growth in clouds Croor2017 . The theoretical possibility of active
suspensions displaying these singular features, even in the absence of
particle inertia, is the subject of this article. Such singular features can
be consequential in providing increased opportunity for communication and
sexual reproduction BUSKEY199813  for motile organisms with negligible
inertia, especially in marine environments

Biological motility in nature frequently takes place in a fluid medium
Gazzola2014 ; Tuval2020  which is itself dynamic, and can strongly influence
the movement and dispersal of swimmers PhysRevLett.129.064502 ;
PhysRevFluids.6.L012501 . Whether an organism moves by itself to a desired
location or simply follows the ambient flow field $\mathbf{U}$ depends on the
ratio of the flow-induced reorientation time scale
$1/\mathinner{\\!\left\lVert\nabla\mathbf{U}\right\rVert}$ to the self-
propulsion time scale $1/\beta$, where
$\mathinner{\\!\left\lVert\nabla\mathbf{U}\right\rVert}$ is evaluated at the
location of the swimmer, and $1/\beta$ is the time it takes for a swimmer to
move by its own body length in the absence of external flow. Thus
$\beta/\mathinner{\\!\left\lVert\nabla\mathbf{U}\right\rVert}\gg 1$ and
$\beta/\mathinner{\\!\left\lVert\nabla\mathbf{U}\right\rVert}\ll 1$ present
the cases of complete control and no control, respectively, of the organism on
its movement. In this work we explore theoretically the inertia-less limit of
the dynamics, i.e., of vanishing particle-scale Reynolds number $Re\to 0$.
Marine plankton, in particular, operate in this regime, in a vortex-laden
turbulent ecosystem, and several aspects of their life are governed by the
coupling of their motility with ambient flow Denny1997 ; Tuval2020 ;
StockerARFM2012 ; Krishnamurthy2020 ; mousavi2023efficient . Fig. 1 (a)
depicts typical values of
$\beta/\mathinner{\\!\left\lVert\nabla\mathbf{U}\right\rVert}$ and $Re$ for
various swimmers, based on published data on swimming speed and size for
dinoflagellates, ciliates Lauga2019 , larvae Wendt2000 ; Fuchs2004 ;
FUCHS2016109 , copepods FUCHS2016109  and a marine bacterium
10.7554/eLife.22140 ; doi:10.1073/pnas.1602307113 ; and typical shear-rates in
the upper mixed layer of the open ocean StockerARFM2012  (see Supplementary).

Micro-swimmers in externally driven flows, through the coupling of their
orientation to velocity gradients Pedley1992 ; Torney2007 ; Zhan2014 , display
focusing Kessler1985 , aggregation GENIN20043 ; Durham2009 ; Ardekani2012 ,
and expulsion out of vortical regions Durham2013 ; Sokolov2016 ; Durham2009 ,
in a manner reminiscent of inertial particles Croor2015 ; Wilkinson_2005 .
Although their inertia is negligible, their motion is persistent because of
self-propulsion Durham2013 . Moreover, the Hamiltonian structure of bound
orbits of microswimmers in certain flows Stark2012 ; Stark2016 ; Lushi2015 ;
Shelley2019 ; Arguedas_Leiva_2020  suggests a role for the effective inertial
dynamics of active Stokesian suspensions in imposed flows, where the
orientation vector behaves like momentum Chajwa2019 ; Ronojoy2020 ; Chajwa2020
.

Figure 1:  Active dimer model for Self-Propelled particles in ambient flow (a)
Based on published data we depict the typical values of the ratio of flow time
scale $1/\mathinner{\\!\left\lVert\nabla\mathbf{U}\right\rVert}$ to swimming
time scale $1/\beta$, and Reynolds number $Re$ for a marine bacterium Vibrio
alginolyticus 10.7554/eLife.22140 ; doi:10.1073/pnas.1602307113 , various
dinoflagelletes, ciliates Lauga2019 , invertebrate larvae Wendt2000 ;
Fuchs2004 ; FUCHS2016109  and copepod FUCHS2016109 . For
$\mathinner{\\!\left\lVert\nabla\mathbf{U}\right\rVert}$ we substitute the
Kolmogorov shear rate for the range of previously measured energy dissipation
rates in the upper mixed layer of the ocean $10^{-8}-10^{-6}$ m2s-3
StockerARFM2012  (see Supplementary). (b) Schematic of an active dimer of
length $\mathbf{w}$ in a flow $\mathbf{U}$. (c) Inner solution caustics is
marked by the intersection of representative trajectories (blue circles) of
particles starting at closely separated initial radial distances, with
$\alpha=0.1$. A continuous variation in $\tilde{r}_{0}$ would give a
continuous curve. The inset depicts analogous optical caustics on the surface
of coffee in a mug.

We ask if inertia-less swimmers Pedley1992  can display caustics, a
conspicuous encounter-promoting feature of the dynamics of inertial particles
(IPs) in flows, where the calculated worldlines of suspended particles cross,
so the solute velocity field is multivalued Wilkinson_2005 ; Croor2015 . We
investigate this intriguing possibility theoretically, in the simple setting
of a dilute suspension of neutrally buoyant swimmers in two-dimensional
vortical flows. We find that non-inertial active particles can display
caustics even near a single vortex, a building block of turbulence. We show
how far the analogy with IP may be carried, and where the two differ
fundamentally. Our flow geometry allows unambiguous demarcation of the regimes
of caustic formation, and forms the basis for understanding the behavior of
active particles in unsteady vortical flows like turbulence. We study the
flow-coupled dynamics of two simple models of single motile particles: Hookean
and preferred-length active dimers, corresponding, in the presence of noise,
to active Ornstein-Uhlenbeck particles (AOUPs) Howfar2016 ; Bonilla2019  and
active Brownian particles (ABPs) Romanczuk2012  respectively. Our focus is on
the deterministic part of the dynamics, with one-way influence of the fluid on
the particles.

##  II Results

### Mapping active dynamics to inertial

The motion of an IP with position vector $\mathbf{X}$ in a background flow
$\mathbf{U}$ is governed by the Maxey-Riley MR1983  equation which, to leading
order in gradients, reads $\dot{\mathbf{X}}=\mathbf{v}$ and
$\text{St}\,\dot{\mathbf{v}}=\,(\mathbf{U}-\mathbf{v})$, when non-
dimensionalised using a characteristic particle length scale $d$ and a flow
velocity scale $U_{0}$. The Stokes number $\text{St}=\tau U_{0}/d$ is a non-
dimensional measure of inertia, characterised by the relaxation time $\tau$
($=$ mass/Stokes drag coefficient) of a particle. The centrifugation of these
particles away from the vortex centre results in the formation of caustics
within a critical distance from the vortex origin Croor2015 . Setting
$\text{St}=0$ yields tracer particles, which move with $\mathbf{v}=\mathbf{U}$
to trace out circular paths forever.

To demonstrate analytically that caustics and the consequent discontinuities
in particle number densities can arise due to activity, even without inertia,
we consider a Hookean active dimer, with centroid position $\mathbf{X}$ and
end-to-end vector $\mathbf{w}$, placed in an imposed background flow field
$\mathbf{U}$. Neglecting inertia and translational diffusion, the equations of
motion for $\mathbf{X}$ and $\mathbf{w}$ take the first-order form

$\dot{\mathbf{X}}=\mu\mathbf{F}\,+\mathbf{U}\,+\beta\mathbf{w}\,\equiv\,\mathbf{v},$
(1a)
$\dot{\mathbf{w}}=-\frac{\mathbf{w}}{\tau}\,+\,(\alpha\,\mathbb{S}+\mathbb{A}\,)\cdot\,\mathbf{w}-\ell^{2}\nabla^{2}\mathbf{U}\,+\sqrt{2D}\bm{\eta},$
(1b)

where $\mu$ is the Stokesian mobility of the particle, and $\mathbf{U}$,
$\nabla^{2}\mathbf{U}$ and the external force field $\mathbf{F}$ are evaluated
at $\mathbf{X}(t)$. In (1b) $\beta$, with units of inverse time but indefinite
sign, endows a dimer with self-propulsion proportional to its extension, and
the polar flow-alignment parameter $\ell$, with units of length, orients the
dimer along a locally parabolic flow, and vanishes for an apolar, i.e., fore-
aft symmetric, particle. Swimmers without noise, external force or the polar
coupling $\ell$, in Poiseuille flow, have been studied by zottl2013periodic .
The analog of $\ell$ for a collective orientation vector appears in
maitra2014activating . Apolar flow-orientation couplings Jeffery1922  enter
through the strain-rate and vorticity tensors
$\mathbb{S}\equiv(\nabla\mathbf{U}+\nabla\mathbf{U}^{\top})/2$ and
$\mathbb{A}\equiv(\nabla\mathbf{U}-\nabla\mathbf{U}^{\top})/2$ respectively,
with a response parameter $\alpha$ determined by particle shape. In (1b)
$\bm{\eta}$ is a zero-mean, isotropic, gaussian white noise with unit
variance.

For $\beta\neq 0$, (1a) and (1b) yield an equation for the total active-
particle velocity ${\bf v}$ [see (1a)] viewed as a dynamical variable,
displayed here for constant spatially uniform external force ${\bf F}$, and in
general form in the Supplement:

$\frac{\tau}{\mu}\dot{\mathbf{v}}=\left[-{1\over\mu}\mathbb{I}+{\tau\over\mu}(\alpha+1)\mathbb{S}\right]({\bf
v}-{\bf U})+{\bf F}+\frac{\tau}{\mu}(D_{t}-\beta\ell^{2}\nabla^{2}){\bf
U}+{\tau\beta\over\mu}\sqrt{2D}\bm{\eta}$ (2)

where $D_{t}=\partial_{t}+{\bf U}\cdot\nabla$, and all fields are evaluated at
$\mathbf{X}(t)$. In the absence of $\ell^{2}\nabla^{2}\mathbf{U}$ and
$\bm{\eta}$ (1b) is homogeneous, so that $\beta$ can be absorbed into
$\mathbf{w}$ in (1). This is why $\beta$ appears only as a prefactor of
$\nabla^{2}\mathbf{U}$ and $\bm{\eta}$ in (2). However, (1) can be recast as
(2) only if $\mathbf{w}$, i.e., self-propulsion, enters (1a); the degree to
which it does is governed by $\tau$. For $\tau\to 0$, (1b) implies
$\mathbf{w}=0$.

The presence of the external force and the drag, with no prefactors, on the
right-hand side, makes it clear that $\tau/\mu$ plays the role of an effective
mass for this inertia-less active system. Indeed (2) resembles the Maxey-Riley
equation for inertial particles in a flow MR1983 , albeit with important
differences. Among them is the absence here of the Basset-Boussinesq history
term MR1983 ; prasath2019accurate , which arises directly due to particle
inertia.

These intriguing similarities prompt us to explore analogs to passive
inertial-particle behavior in the dynamics of active inertia-less particles in
external flows.

### Caustics near a point vortex flow

We begin with the classic case of motion in the flow field of a point vortex
at the origin. In plane polar coordinates $(r,\theta)$,
$\mathbf{U}=\hat{\theta}\tilde{\Gamma}/r$, with circulation
$2\pi\tilde{\Gamma}$. Note that $\mathbb{A}=0$ for this flow everywhere except
at the origin. Non-dimensionalizing (2) using the natural length
$\sqrt{\tilde{\Gamma}\tau}$ Croor2015  and time $\tau$ gives the coupled
equations

$\ddot{r}-\frac{L^{2}}{r^{3}}=-\dot{r}+\frac{\alpha}{r^{3}}-\frac{(1+\alpha)L}{r^{3}},$
(3a) $\dot{L}=1-L-\frac{(1+\alpha)\dot{r}}{r}+\frac{\lambda}{r^{2}},$ (3b)

(see Supplementary text) for the Lagrangian dynamics of the active particle
whose centroid is at a radial distance of $r$ from a point vortex, where
$L\equiv r^{2}\dot{\theta}$ is the angular momentum per unit mass of the
particle and $\lambda\equiv\beta\ell^{2}/\tilde{\Gamma}$.

Effective centrifugal accelerations, reinforcing the similarity to an IP,
arise through the $L^{2}/r^{3}$ term. Due to the terms containing $\alpha$,
our equations are distinct from those for true IP Croor2015 . We now limit
ourselves to particles with apolar, i.e., fore-aft symmetric, shape, so that
$\lambda=0$. We treat the nonlinearities in (3a) & (3b) perturbatively. A
regular perturbation approach yields absurd solutions near the origin; in fact
equations (3a) and (3b) constitute a singular perturbation problem BO1999 .
The behaviour at very small times and small distances away from the vortex is
singular, and relatively violent, unlike the more gentle relaxation to the
final state at late times. This feature is exploited in the following to
understand the different physics at small and large time.

We seek an inner solution at the lowest order for $t\ll 1$ and $r\ll 1$, and
an outer solution for $t\gg 1$, where $r$ could be $O(1)$ or larger. In
contrast to an IP which centrifuges out forever, the outer solution for an
active Hookean dimer is steady rotation with $\mathbf{w}$ and
$\dot{\theta}=1/r_{f}^{2}$ at a constant final distance $r_{f}$ from the
vortex, rendering the particle passive and lifeless at large times. Intriguing
physics appears in the inner region, which sets the stage for the rest of this
article. As is standard in singular perturbation theory, we recast (3a) and
(3b) in the stretched spatial $\tilde{r}\equiv r/\delta$ and temporal
$\tilde{t}\equiv t/\epsilon$ variables, where $\epsilon$ and $\delta$ are as
yet unknown, but will be selected to ensure that all derivatives in the
stretched variables are $\mathcal{O}(1)$. Dominant balance necessitates
$\epsilon=\delta^{2}$, yielding the inner solution

$L=L_{0}-(1+\alpha)\log{\tilde{r}/\tilde{r}_{0}},$ (4)

and

$v_{r}^{2}={v_{0}}^{2}-\frac{\alpha+(L-1-\alpha)^{2}}{\tilde{r}^{2}}+\frac{\alpha+(L_{0}-1-\alpha)^{2}}{\tilde{r}_{0}^{2}},$
(5)

where $v_{r}$ is the radial speed of the particle,
$(\tilde{r}_{0},v_{0},L_{0})$ are the initial stretched radial coordinate,
radial speed and angular momentum respectively.

Each solution is a ray in the $(t,r)$ plane, and some representative rays are
shown in Fig. 1. Caustics arise when two particles collide, i.e., occupy the
same spatial location at the same time. If we start out with two rings of
particles at slightly different initial radii (say $r_{0}$ and $r_{0}+\Delta
r$, then the intersection of their rays in the $r,t$ plane represents an
overtaking of the outer ring by the inner, i.e., the occurrence of caustics.
Intersections, or caustics, for a few chosen $r_{0}$, and extremely small
$\Delta r$ are shown by the blue circles in Fig.1(c). For the purpose of
demonstration we have here taken $r^{*}=1$, and equal initial speeds.
Performing this exercise for all $r_{0}$ yields an envelope, shown by the
curve joining the blue circles, representing the smallest radial distance at a
given time for the occurrence of caustics. This picture is akin to geometrical
optics, where a caustic is an envelope tangent to the light rays
eggers_fontelos_2015 .

Figure 2: Centrifugation and caustics of dimer in point vortex: (a) Time
frames showing the positions of the particles (blue dots) around a point
vortex at the origin for IP and noiseless AOUP respectively [see Supplementary
video 3.1 & 3.2]. Particles were initialised with uniformly random initial
positions and orientations/velocities. (b) An initially homogeneous number-
density (grey circles) peaks near a critical radial distance (green) in the
steady state, compared to unsteady density of IP (purple) at a representative
$t\gg 1$. (c) Trajectory (rays) of particles averaged over all initial
orientations. The envelope of rays, for particles starting at various initial
$r$, gives rise to caustics (red circles). The green curve shows $R=t^{\nu}$,
with $\nu=2/3$. In (b), (c) & (d), $\alpha=1$. (d) The crossing time of
adjacent rays separated by $\Delta r=0.001$ starting at various radial
distances $r$, averaged over uniformly random initial orientations, diverges
at a finite critical radius $r_{c}$ for an active particle (red) and for an
inertial particle (blue) averaged over uniformly random initial velocity of
unit magnitude. (e) For various $\alpha$, plotting $r_{c}$ demarcates the
region of caustics, which is the radial distance below which adjacent rays
cross each other in a finite time.

We now numerically solve the full equations (1a) & (1b), without noise and
external force ${\bf F}$, with the polar flow coupling $\lambda=0$ (see
Supplementary video 3.2). In this case the self-propulsion $\beta$ can be
absorbed in the definition of $\mathbf{w}$.

Figure 3:  Caustics in turbulent flow. The blue-yellow colorbar represents the
vorticity magnitude in the ambient turbulent flow scaled by the root-mean-
square velocity gradient $\kappa$ and black speckles are the locations of the
geometric centers of $10^{5}$ active dimers with preferred length $w_{0}$. (a)
$\ell^{2}/w_{0}=1.0$ with (from left to right) $w_{0}\tilde{\beta}=0.0118$ m,
$0.118$ m, and $1.18$ m. (b) $\ell^{2}/w_{0}=0$ with (left to right)
$w_{0}\tilde{\beta}=0.0118$ m, $w_{0}\tilde{\beta}=0.118$ m, and
$w_{0}\tilde{\beta}=1.18$ m, where $\tilde{\beta}\equiv\beta/\kappa$. For
intermediate activity the particles display pronounced caustics [see
Supplementary video].(c) heat-map of the number-density fluctuation plotted in
$(w_{0}\tilde{\beta},w_{0}\tilde{\ell}^{2})$ plane in meters. The vertical
dashed lines, from left to right respectively, depict typical
$w_{0}\tilde{\beta}$ for dinoflagellates, ciliates, invertebrate larvae and
copepods for a turbulence energy dissipation rate of $10^{-8}$ m2 s-3 (d)
number-density fluctuation as a function of activity, showing pronounced
agglomeration for intermediate levels of activity. (e) Okubo-Weiss parameter
plotted for $l=0$ and various values of $w_{0}\tilde{\beta}$. (f) Density
field of the particles overlaid on the heat-map of
$\mathinner{\\!\left\lVert\nabla\mathbf{v}\right\rVert}^{2}$ s-2 where
$\mathbf{v}$ is the velocity field of particles.

Early in the process, when $t=\mathcal{O}(\tau)$, we find that noiseless AOUP,
i.e., active Hookean dimers, behave similar to IP, in that they both display
centrifugation close to the vortex [see middle panel of Fig. 2(a)]. Such
voiding of vortical regions has been observed previously for rigid gyrotactic
swimmers Durham2011  and bacteria Sokolov2016 ; Ardekani2012 , and is shown to
be critical for their transport in turbulent environments Zhan2014 ;
Torney2007 . However, the identification of a singularity, namely caustics,
for this flow- and motility-induced spatial organisation was missing. At long
times, the radial profile of number density reaches a steady state, with a
peak at a particular radius [Fig. 2(b)] The extension of the dimer relaxes to
zero, so in the absence of noise the AOUP at long time behaves like a tracer
particle, consistent with our asymptotic analysis. In contrast, IPs centrifuge
out forever, though slower and slower as time progresses. This feature of IPs
is closely mimicked by a more robustly motile particle, which we discuss
below. The sharp peak in the number density at a particular radial distance
suggests the formation of caustics. To confirm this, we study as before the
trajectories of pairs of particles separated by $\Delta r_{0}$ in their radial
position at the initial time, averaged over uniformly random initial
orientations. Caustics are seen in Fig. 2(c) with an envelope as predicted by
the inner solution (5). The scaling of this caustics curve near the vortex
singularity is $r\sim t^{2/3}$ [green curve in Fig. 2(c)], is reminiscent of
the swallowtail catastrophe in optical caustics eggers_fontelos_2015  [Fig.
1(c) inset].

We demarcate the regions in the $r_{0}-\alpha$ plane where caustics occur as
those where an intersection of adjacent rays (see Fig 2) takes place in finite
time. For each value of $\alpha$, we start a pair of particles at $r_{0}$ and
$r_{0}+\Delta r_{0}$ and measure $t_{x}$, the time taken for these nearby
trajectories to intersect. The crossing time is averaged over uniformly random
initial orientations. At a particular $r_{0}=r_{c}$, $t_{x}$ diverges [see
Fig. 2 (d)], and caustics do not occur when the initial particle position is
beyond this critical radius. This is seen to be comparable to that for IP
Croor2015 . Both Active Hookean dimer and IP show power-law behaviour, but
with different slopes, for caustics formation time as a function of $r_{0}$.
At long times, the number density of the particles peaks around $r_{c}$, shown
as a vertical dashed line (red) in Figure 2 (b) for $\alpha=1.0$.

The flow coupling $\alpha$ has a dual role at small to moderate distances from
the vortex: (i) it aligns the dimer along the stable principal axis of
$\mathbb{S}$, which has a non-zero radial component; (ii) once aligned, it
extends the dimer along this axis, thus competing with the $1/\tau$ relaxation
to zero-motility. However, when the dimers have been centrifuged out to large
$r$, the relaxation term takes over, leading to tracer-like dynamics, and the
caustics radii lie at intermediate values of $r$ [see Fig 2 (b)].

### Active caustics in turbulent flows

Although Active Hookean dimers are analytically tractable and offer a
conceptual understanding of the coupling between flow and the activity of
deformable swimmers, their extension, and hence their intrinsic speed, relax
to zero in the absence of noise and flow. The motility parameter $\beta$
defines a speed only when multiplied by a preferred scale of ${\bf w}$, say
its RMS value. In nature, motile organisms generally possess an intrinsic
speed scale independent of noise. To study such a case, we consider the
equations for position $\mathbf{X}$ and extension $\mathbf{w}$ for an active
dimer with a strongly preferred value of $|\mathbf{w}|=w_{0}$,

$\displaystyle\dot{\mathbf{X}}$
$\displaystyle=\mu\mathbf{F}+\mathbf{U}+\beta{\mathbf{w}}$ (6)
$\displaystyle\dot{\mathbf{w}}$
$\displaystyle={1\over\tau}\left(1-{|\mathbf{w}|^{2}\over
w_{0}^{2}}\right)\mathbf{w}\,+\,(\alpha\mathbb{S}+\mathbb{A})\cdot\mathbf{w}$
$\displaystyle-{\ell}^{2}\nabla^{2}\mathbf{U}\,+\sqrt{2D}\bm{\eta}(t),$ (7)

which introduces a fixed size scale $w_{0}$ and speed $v=\beta w_{0}$.
Equations (6) and (7) describe an active Brownian particle (ABP) in a flow.
The difference between our preferred-length model and the traditional ABP, in
which $|{\bf w}|$ is constant, is unimportant. The dynamics resulting from the
preferred-length dimer in a point vortex flow also gives rise to caustics in
the inner region (see Supplementary), with the motility $\beta$ playing a more
conspicuous role than in AOUP dynamics.

To explore the dynamics of a collection of ABPs in unsteady vortical flows, we
write a pseudospectral code to solve the Navier-Stokes equations in a $2\pi$
periodic domain with $512^{2}$ collocation points and a deterministic external
forcing $F_{0}q\cos{qx}$, in the stream-function/vorticity formulation [Table
1]. This gives the flow $\mathbf{U}$ that drives the particle dynamics [see
Supplementary]. A one-way coupling is assumed, wherein the ambient flow stirs
the particles but particles do not generate flows.

Domain |  $k_{f}$ |  $F_{0}$ |  $\nu$ |  $\mu$
---|---|---|---|---
5122 |  3 m-1 |  0.1 ms-1 |  $5\times 10^{-6}$ m2s-1 |  0.01 s-1
Table 1: Spectral DNS Parameters

We use $w_{0}$ and the inverse of the root-mean-square velocity gradient
$\kappa\equiv\sqrt{\langle\nabla\mathbf{U}\mathrel{\mathop{\mathchar
58\relax}}\nabla\mathbf{U}\rangle}$ of the background flow in the turbulent
steady state as length and time scales respectively, which gives the non-
dimensional parameters,
$({\beta/\kappa},\tau\kappa,\alpha,{\ell}^{2}/w^{2}_{0})$ and noise strength
$\sqrt{2D/w^{2}_{0}\kappa}$. We fix $\alpha=1$ and $\tau=1$, leaving a two-
dimensional parameter space $({\beta/\kappa},\,{\ell}^{2}/w^{2}_{0})$ of
activity and polar alignability respectively.

In a turbulent steady state, we initialise the particles with uniformly random
initial position and orientations. In the steady state of particle dynamics,
we find tracer-like behavior for small values of motility strength $\beta$ in
which the swimmers get trapped within the vortices, consistent with the single
vortex study [see Supplementary video]. For large values of $\beta$, swimmers
exhibit ballistic dynamics, leading to a homogeneous number density of
particles. The compelling features of caustics appear at intermediate values
of $\beta$ (see Supplementary movie), where we see preferential sampling and
clustering [see Fig. 3 (a) & (b)]. We quantify caustics-induced clustering by
measuring the density fluctuation with respect to the initial homogeneous
state [see Supplementary methods], and find pronounced caustics for a range of
$\tilde{\ell}$ and $\tilde{\beta}$ [see Fig. 3 (c)]. We find that for
intermediate values of activity $\tilde{\beta}$, increasing $\tilde{\ell}$
sharpens the caustics filaments. The density fluctuation exhibits a peak
around $w_{0}\tilde{\beta}\simeq 10^{-1}$ m [see Fig. 3 (d)], which is similar
to the dynamics of IP, where for intermediate values of Stokes number $St$,
particles display clustering EATON1994169  and sharp caustics Wilkinson_2005 ,
as compared to large and small values of $St$. To quantify how swimmers sample
the flow, we calculate the Okubo-Weiss parameter,
$\mathcal{W}=\omega^{2}-2\mathbb{S}\mathrel{\mathop{\mathchar
58\relax}}\mathbb{S}$ at the location of particles, where $\mathbb{S}$ is the
symmetric part of the velocity gradient tensor Jason2018  and $\omega$ the
vorticity. $\mathcal{W}>0$ implies that the particles are in a vortical
region, and $\mathcal{W}<0$ means they are located in a straining region. The
distribution of $\mathcal{W}$ sampled over all particle locations gives the
deviation from homogeneous sampling of the flow; when compared with the
distribution of $\mathcal{W}$ over the entire flow domain [see Fig. 3 (e)]. We
find that particles cluster preferentially in the straining regions, which
coincides with the peaks in the coarse-grained field
$\mathinner{\\!\left\lVert\nabla\mathbf{v}\right\rVert}$ [see Fig. 3], that
marks caustics of active particles in flow, akin to the inertial case
Wilkinson_2005 , as might have been anticipated from our stationary vortex
studies. We expect some manifestation of “active caustics” in small swimming
organisms like ciliates, invertebrate larvae and copepods when the turbulence
energy dissipation rates are towards the lower end of the range of values
observed in the upper mixed layer of the ocean $10^{-8}-10^{-6}$ m2s-3
StockerARFM2012  [see Fig. 1 (a)].

##  III Summary

We investigate the deterministic dynamics of active dimers in vortical flows,
using two different models of active dimers, namely the noiseless limits of
AOUPs and ABPs. In the illustrative setting of a single point vortex, we
highlight the distinctions and similarities between the centrifugation of IP
and the effective centrifugation of motile inertialess particles. We show the
formation of caustics in both the dimer types, by analysing the intersection
of rays in the $r-t$ plane. For a range of the strain-rate/orientation
coupling parameter $\alpha$, we demarcate the regimes in the ${\alpha}-r$
plane where caustics occur. We study the effect of advection by more general
vortical flows in the form of two-dimensional Navier-Stokes turbulence
generated by direct numerical simulation. We use the Okubo-Weiss parameter to
characterize the preferential sampling of straining regions by the swimmers.
We find that for intermediate values of the dimensionless motility
$\tilde{\beta}$ (self-propulsion speed scaled by flow-velocity difference on
the scale of a swimmer), clustering and caustics are more pronounced, similar
to the dynamics of IP as the Stokes number St is varied, suggesting that
$\tilde{\beta}$ plays the same role as St. This hitherto unexplored caustics
regime is of interest for two reasons. In a formal sense the crossing of
worldlines of active particles renders their velocity field multiple-valued.
Arguably more important, it is a strikingly effective natural mechanism for
close encounters between organisms at low mean concentrations, which should
enhance communication and reproduction. Although coarse-graining eliminates
multivalued-ness of the velocity field, the accompanying singularity in the
density field persists. In natural systems, however, the divergence in
particle number density would likely be regularized by inter-particle
hydrodynamic, steric and/or behavioral interactions. The possibility of
caustics in scenarios like the clustering of phytoplankton in upwelling
GENIN20043 , or biofilm formation in microfluidic vortices Ardekani2012 ,
offers a mechanism for enhanced interactions in such systems even when quite
dilute on the average, and poses formal challenges for describing singular
particle-velocity fields.

## Acknowledgements

SR acknowledges support from the Science and Engineering Research Board,
India, and from the Tata Education and Development Trust, and discussions in
the Program on Complex Lagrangian Problems of Particles in Flows, ICTS-TIFR,
Bangalore, R & RG acknowledge support from the Department of Atomic Energy,
Government of India, under project no. RTI4001. RC acknowledges support from
the International Human Frontier Science Program Organization, thanks Michael
Shelley for fruitful discussions, and the Prakash lab for valuable insights
into plankton dynamics.

## References

  * (1) M. Pinsky and A. Khain, “Turbulence effects on droplet growth and size distribution in clouds—a review,” Journal of Aerosol Science, vol. 28, no. 7, pp. 1177–1214, 1997.
  * (2) S. Yazdi and A. M. Ardekani, “Bacterial aggregation and biofilm formation in a vortical flow,” Biomicrofluidics, vol. 6, no. 4, p. 044114, 2012.
  * (3) H. Morrison, M. van Lier-Walqui, A. M. Fridlind, W. W. Grabowski, J. Y. Harrington, C. Hoose, A. Korolev, M. R. Kumjian, J. A. Milbrandt, H. Pawlowska, D. J. Posselt, O. P. Prat, K. J. Reimel, S.-I. Shima, B. van Diedenhoven, and L. Xue, “Confronting the challenge of modeling cloud and precipitation microphysics,” Journal of Advances in Modeling Earth Systems, vol. 12, no. 8, p. e2019MS001689, 2020.  e2019MS001689 2019MS001689.
  * (4) H. J. S. Fernando, D. Zajic, S. Di Sabatino, R. Dimitrova, B. Hedquist, and A. Dallman, “Flow, turbulence, and pollutant dispersion in urban atmospheres,” Physics of Fluids, vol. 22, no. 5, p. 051301, 2010.
  * (5) P. W. Boyd, H. Claustre, M. Levy, D. A. Siegel, and T. Weber, “Multi-faceted particle pumps drive carbon sequestration in the ocean,” Nature, vol. 568, pp. 327–335, 2019.
  * (6) K. Samborska, S. Poozesh, A. Barańska, M. Sobulska, A. Jedlińska, C. Arpagaus, N. Malekjani, and S. M. Jafari, “Innovations in spray drying process for food and pharma industries,” Journal of Food Engineering, vol. 321, p. 110960, 2022.
  * (7) G. Boffetta, F. De Lillo, and A. Gamba, “Large scale inhomogeneity of inertial particles in turbulent flows,” Physics of Fluids, vol. 16, no. 4, pp. L20–L23, 2004.
  * (8) M. R. Maxey and J. J. Riley, “Equation of motion for a small rigid sphere in a nonuniform flow,” The Physics of Fluids, vol. 26, no. 4, pp. 883–889, 1983\.
  * (9) M. R. Maxey and S. Corrsin, “Gravitational settling of aerosol particles in randomly oriented cellular flow fields,” Journal of Atmospheric Sciences, vol. 43, no. 11, pp. 1112 – 1134, 1986.
  * (10) S. Ravichandran and R. Govindarajan, “Caustics and clustering in the vicinity of a vortex,” Physics of Fluids, vol. 27, no. 3, p. 033305, 2015.
  * (11) M. Wilkinson and B. Mehlig, “Caustics in turbulent aerosols,” Europhysics Letters (EPL), vol. 71, pp. 186–192, jul 2005.
  * (12) P. Deepu, S. Ravichandran, and R. Govindarajan, “Caustics-induced coalescence of small droplets near a vortex,” Phys. Rev. Fluids, vol. 2, p. 024305, Feb 2017.
  * (13) E. J. Buskey, “Components of mating behavior in planktonic copepods,” Journal of Marine Systems, vol. 15, no. 1, pp. 13–21, 1998.
  * (14) M. Gazzola, M. Argentina, and L. Mahadevan, “Scaling macroscopic aquatic locomotion,” Nature Physics, vol. 10, pp. 758–761, Sept. 2014.
  * (15) G. Basterretxea, J. S. Font-Muñoz, and I. Tuval, “Phytoplankton orientation in a turbulent ocean: A microscale perspective,” Frontiers in Marine Science, vol. 7, 2020.
  * (16) R. Monthiller, A. Loisy, M. A. R. Koehl, B. Favier, and C. Eloy, “Surfing on turbulence: A strategy for planktonic navigation,” Phys. Rev. Lett., vol. 129, p. 064502, Aug 2022.
  * (17) S. A. Berman, J. Buggeln, D. A. Brantley, K. A. Mitchell, and T. H. Solomon, “Transport barriers to self-propelled particles in fluid flows,” Phys. Rev. Fluids, vol. 6, p. L012501, Jan 2021.
  * (18) A. Abelson and M. Denny, “Settlement of marine organisms in flow,” Annual Review of Ecology and Systematics, vol. 28, no. 1, pp. 317–339, 1997\.
  * (19) J. S. Guasto, R. Rusconi, and R. Stocker, “Fluid mechanics of planktonic microorganisms,” Annual Review of Fluid Mechanics, vol. 44, no. 1, pp. 373–400, 2012.
  * (20) D. Krishnamurthy, H. Li, F. B. du Rey, P. Cambournac, A. G. Larson, E. Li, and M. Prakash, “Scale-free vertical tracking microscopy,” Nature Methods, vol. 17, pp. 1040–1051, Aug. 2020.
  * (21) N. Mousavi, J. Qiu, B. Mehlig, L. Zhao, and K. Gustavsson, “Efficient survival strategy for zooplankton in turbulence,” 2023.
  * (22) M. Lisicki, M. F. Velho Rodrigues, R. E. Goldstein, and E. Lauga, “Swimming eukaryotic microorganisms exhibit a universal speed distribution,” eLife, vol. 8, p. e44907, jul 2019.
  * (23) D. Wendt, “Energetics of larval swimming and metamorphosis in four species of bugula (bryozoa),” The Biological Bulletin, vol. 198, no. 3, pp. 346–356, 2000.
  * (24) H. L. Fuchs, L. S. Mullineaux, and A. R. Solow, “Sinking behavior of gastropod larvae (ilyanassa obsoleta) in turbulence,” Limnology and Oceanography, vol. 49, no. 6, pp. 1937–1948, 2004.
  * (25) H. L. Fuchs and G. P. Gerbi, “Seascape-level variation in turbulence- and wave-generated hydrodynamic signals experienced by plankton,” Progress in Oceanography, vol. 141, pp. 109–129, 2016.
  * (26) M. Chen, Z. Zhao, J. Yang, K. Peng, M. A. Baker, F. Bai, and C.-J. Lo, “Length-dependent flagellar growth of Vibrio alginolyticus revealed by real time fluorescent imaging,” eLife, vol. 6, p. e22140, jan 2017.
  * (27) K. Son, F. Menolascina, and R. Stocker, “Speed-dependent chemotactic precision in marine bacteria,” Proceedings of the National Academy of Sciences, vol. 113, no. 31, pp. 8624–8629, 2016.
  * (28) T. J. Pedley and J. O. Kessler, “Hydrodynamic phenomena in suspensions of swimming microorganisms,” Annual Review of Fluid Mechanics, vol. 24, no. 1, pp. 313–358, 1992.
  * (29) C. Torney and Z. Neufeld, “Transport and aggregation of self-propelled particles in fluid flows,” Phys. Rev. Lett., vol. 99, p. 078101, Aug 2007\.
  * (30) C. Zhan, G. Sardina, E. Lushi, and L. Brandt, “Accumulation of motile elongated micro-organisms in turbulence,” Journal of Fluid Mechanics, vol. 739, p. 22–36, 2014.
  * (31) J. O. Kessler, “Hydrodynamic focusing of motile algal cells,” Nature, vol. 313, pp. 218–220, Jan. 1985.
  * (32) A. Genin, “Bio-physical coupling in the formation of zooplankton and fish aggregations over abrupt topographies,” Journal of Marine Systems, vol. 50, no. 1, pp. 3–20, 2004.  The Role of Biophysical Coupling in Concentrating Marine Organisms Around Shallow Topographies.
  * (33) W. M. Durham, J. O. Kessler, and R. Stocker, “Disruption of vertical motility by shear triggers formation of thin phytoplankton layers,” Science, vol. 323, no. 5917, pp. 1067–1070, 2009.
  * (34) W. M. Durham, E. Climent, M. Barry, F. De Lillo, G. Boffetta, M. Cencini, and R. Stocker, “Turbulence drives microscale patches of motile phytoplankton,” Nature Communications, vol. 4, no. 2148, 2013.
  * (35) A. Sokolov and I. S. Aranson, “Rapid expulsion of microswimmers by a vortical flow,” Nature Communications, vol. 7, no. 11114, 2016.
  * (36) A. Zöttl and H. Stark, “Nonlinear dynamics of a microswimmer in poiseuille flow,” Phys. Rev. Lett., vol. 108, p. 218104, May 2012.
  * (37) H. Stark, “Swimming in external fields,” The European Physical Journal Special Topics, vol. 225, p. 2369–2387, 2016.
  * (38) E. Lushi and P. M. Vlahovska, “Periodic and chaotic orbits of plane-confined micro-rotors in creeping flows,” Journal of Nonlinear Science, vol. 25, p. 1111–1123, October 2015.
  * (39) N. Oppenheimer, D. B. Stein, and M. J. Shelley, “Rotating membrane inclusions crystallize through hydrodynamic and steric interactions,” Phys. Rev. Lett., vol. 123, p. 148101, Oct 2019.
  * (40) J.-A. Arguedas-Leiva and M. Wilczek, “Microswimmers in an axisymmetric vortex flow,” New Journal of Physics, vol. 22, p. 053051, may 2020.
  * (41) R. Chajwa, N. Menon, and S. Ramaswamy, “Kepler orbits in pairs of disks settling in a viscous fluid,” Phys. Rev. Lett., vol. 122, p. 224501, Jun 2019.
  * (42) A. Bolitho, R. Singh, and R. Adhikari, “Periodic orbits of active particles induced by hydrodynamic monopoles,” Phys. Rev. Lett., vol. 124, p. 088003, Feb 2020.
  * (43) R. Chajwa, N. Menon, S. Ramaswamy, and R. Govindarajan, “Waves, algebraic growth, and clumping in sedimenting disk arrays,” Phys. Rev. X, vol. 10, p. 041016, Oct 2020.
  * (44) E. Fodor, C. Nardini, M. E. Cates, J. Tailleur, P. Visco, and F. van Wijland, “How far from equilibrium is active matter?,” Phys. Rev. Lett., vol. 117, p. 038103, Jul 2016.
  * (45) L. L. Bonilla, “Active ornstein-uhlenbeck particles,” Phys. Rev. E, vol. 100, p. 022601, Aug 2019.
  * (46) P. Romanczuk, M. Bär, W. Ebeling, B. Lindner, and L. Schimansky-Geier, “Active brownian particles,” The European Physical Journal Special Topics, vol. 202, no. 1, pp. 1–162, 2012.
  * (47) A. Zöttl and H. Stark, “Periodic and quasiperiodic motion of an elongated microswimmer in poiseuille flow,” The European Physical Journal E, vol. 36, pp. 1–10, 2013.
  * (48) A. Maitra, P. Srivastava, M. Rao, and S. Ramaswamy, “Activating membranes,” Physical review letters, vol. 112, no. 25, p. 258101, 2014.
  * (49) G. B. Jeffery and L. N. G. Filon, “The motion of ellipsoidal particles immersed in a viscous fluid,” Proceedings of the Royal Society of London. Series A, Containing Papers of a Mathematical and Physical Character, vol. 102, no. 715, pp. 161–179, 1922.
  * (50) S. G. Prasath, V. Vasan, and R. Govindarajan, “Accurate solution method for the maxey-riley equation, and the effects of basset history,” Journal of Fluid Mechanics, vol. 868, pp. 428–460, 2019.
  * (51) C. M. Bender and S. A. Orzag, Advanced mathematical methods for scientists and engineers i: Asymptotic methods and perturbation theory.  New York: Springer, 1999.
  * (52) J. Eggers and M. A. Fontelos, Singularities: Formation, Structure, and Propagation.  Cambridge Texts in Applied Mathematics, Cambridge University Press, 2015\.
  * (53) W. M. Durham, E. Climent, and R. Stocker, “Gyrotaxis in a steady vortical flow,” Phys. Rev. Lett., vol. 106, p. 238102, Jun 2011.
  * (54) J. Eaton and J. Fessler, “Preferential concentration of particles by turbulence,” International Journal of Multiphase Flow, vol. 20, pp. 169–209, 1994.
  * (55) J. R. Picardo, D. Vincenzi, N. Pal, and S. S. Ray, “Preferential sampling of elastic chains in turbulent flows,” Phys. Rev. Lett., vol. 121, p. 244501, Dec 2018.