11institutetext: Vrije Universiteit Amsterdam, The Netherlands
22institutetext: Xiamen University, China

# Game semantics for lattice-based modal $\mu$-calculus††thanks: This project
has received funding from the European Union’s Horizon 2020 research and
innovation programme under the Marie Skłodowska-Curie grant agreement No
101007627.The research of the author Krishna Manoorkar is supported by the NWO
grant KIVI.2019.001.

Yiwen Ding Yiwen Ding and Ruoding Wang are supported by the China Scholarship
Council  11 0009-0000-6447-6479 Krishna Manoorkar  11 0000-0003-3664-7757
Mattia Panettiere  11 0000-0002-9218-5449 Apostolos Tzimoulis  11
0000-0002-6228-4198 Ruoding Wang⋆⋆ 1122 0009-0005-3995-3225

###### Abstract

In this paper, we generalize modal $\mu$-calculus to the non-distributive
modal logic. We provide a game semantics for the developed logic. We
generalize the unfolding games on the power-set algebras to the general
lattices and show that it can be used to determine the least and the greatest
fixed points of a monotone operator on a lattice. We use this result to show
the adequacy of the game semantics. Finally, we conclude and provide some
possible applications of the non-distributive modal $\mu$-calculus developed
here.

###### Keywords:

polarity-based semantics non-distributive logics modal $\mu$-calculus game
semantics lattice-based logics.

##  1 Introduction

Fixed point operators and their applications have been studied extensively in
mathematics [9, 1]. One of the most prominent formal languages to study fixed
point operators on power-set algebras in logic is modal $\mu$-calculus [2, 16,
13]. Modal $\mu$-calculus provides a straight-forward expansion of modal logic
which has several applications in formal modelling and theoretical computer
science [14, 16].

Non-distributive modal logics have been studied in recent years as semantics
for theory of categorization [4, 3, 6] and evidential reasoning [7]. Knaster-
Tarski theorem [12, 15] implies that any monotone modal operator on a complete
lattice must have a least and a greatest fixed point operator. In this paper,
we generalize modal $\mu$-calculus to the non-distributive setting to study
these fixed operators on general lattices formally. Fixed point operators
arise in categorization theory naturally in several contexts.

Many categories in social and linguistic context often arise as a fixed point
of some dynamic process or interaction. An important context in which
categories are formed as fixed point is categories formed through optimization
by some classification or clustering algorithm. Many such algorithms perform
some operation iteratively until this iterative process stabilizes, i.e.
reaches a fixed point. Another example of fixed point operators in
categorization theory is provided by the common knowledge operator described
in [4]. Common knowledge in epistemic logic refers to the facts known by all
the agents involved and all the agents know that these facts are known by all
the agents and so on. Thus, the common knowledge operator can be seen as a
fixed point of knowledge of all agents.

##### Structure of the paper:

In Section 2 we gather preliminaries on non-distributive logics, games, fixed
points and the classical modal $\mu$-calculus. In Section 3 we introduce game
semantics for the non-distributive modal logic. In Section 4 we introduce the
non-distributive modal $\mu$-calculus, introduce unfolding games on complete
lattices, introduce the game semantics and show their adequacy. Finally, in 5
we gather concluding remarks.

##  2 Preliminaries

In this section we gather background information fixed points, board games and
the classical modal $\mu$-calculus. We take inspiration in our presentation
from [16]. Finally we present non-distributive modal logics.

###  2.1 Fixed points on lattices

For any complete lattice $\mathbb{L}$ and monotone map
$f:\mathbb{L}\to\mathbb{L}$, we say that $u\in\mathbb{L}$ is a _postfixed
point_ of $f$ if $u\leq f(u)$, a _prefixed point_ of $f$ if $f(u)\leq u$, a
_fixed point_ of $f$ if $f(u)=u$. The following theorem is well known:

######  Theorem 2.1 (Knaster-Tarski)

For any complete lattice $\mathbb{L}$ and monotone map
$f:\mathbb{L}\to\mathbb{L}$, the set of fixed points of $f$ forms a complete
lattice.

In particular, every monotone map $f$ on a complete lattice has a least fixed
point (which is in fact the least prefixed point) and a greatest fixed point
(which is in fact the greatest postfixed point), which we will denote with
$\mathrm{lfp}(f)$ and $\mathrm{gfp}(f)$. Another way to construct the least
(resp. greatest) fixed point above (resp. below) a set $S$ of fixed points is
via the following recursions on ordinals $\alpha$:

  * •

$f^{0}(u)=u=f_{0}(u)$,

  * •

$f^{\alpha+1}(u)=f(f^{\alpha}(u))=f_{\alpha+1}(u)$,

  * •

$f^{\alpha}(u)=\bigvee_{\beta<\alpha}f^{\beta}(u)$ and
$f_{\alpha}(u)=\bigwedge_{\beta<\alpha}f_{\beta}(u)$, where $\alpha$ is a
limit ordinal.

Then $(f^{\alpha}(\bigvee S))_{\alpha\in Ord}$ is an increasing sequence, and
since $\mathbb{L}$ is set-size it reaches a fixed point which is the least
fixed point above $S$. Likewise, $(f_{\alpha}(\bigwedge S))_{\alpha\in Ord}$
is decreasing and hence also reaches eventually a fixed point which is the
greatest fixed point below $S$.

###  2.2 Board games

In the games that we will discuss we will always have two players, Abelard
(denoted $\forall$) and Eloisa (denoted $\exists$). Our games will be played
on a board that will be formally understood as a collection
$(B_{\exists},B_{\forall},\mathcal{M})$, where $B_{\exists}$ and $B_{\forall}$
are disjoint sets, that correspond to the positions on the board (denoted
$B=B_{\exists}\cup B_{\forall}$) on which $\exists$ and $\forall$ are expected
to move, while $\mathcal{M}:B\to\mathcal{P}(B)$ is a function that given a
position indicates the admissible moves the player can make. A (potentially
countable) sequence $(b_{n})_{n\in\omega}$ such that $b_{n}\in B$ and
$b_{n+1}\in\mathcal{M}(b_{n})$ is called a _play starting from $b_{0}$_. If
the play is finite with last element $b_{k}$ such that
$\mathcal{M}(b_{k})\neq\varnothing$, then we call the play _partial_. The
board is accompanied by the winning rules that describe which player wins. In
the games we discuss if a play ends at a position $b\in B_{\ast}$ such that
$\mathcal{M}(b)=\varnothing$, i.e. player $\ast$ has no move, then we say that
the play is losing for $\ast$. The only other winning conditions we entertain
have to do with infinite plays: In this case we designate
$W_{\exists}\subseteq B^{\omega}$ the set of winning plays for $\exists$. In
these games there are no ties and hence $W_{\forall}=B^{\omega}\setminus
W_{\exists}$. The winning conditions for infinite plays in such games concern
only the tails of the sequences, hence if two sequence $(b_{n})_{n\in\omega}$
and $(b^{\prime}_{n})_{n\in\omega}$ are eventually the same then they are
winning for the same player. This condition implies that the games we consider
are _positional_ , i.e. if a play is winning for a player, then any other play
with the same final segment is also winning for that player.

A strategy for $\ast$ for a game is a function
$\sigma_{\ast}:B^{<\omega}\times B_{\ast}\to B$ such that if $(b_{i})_{i\leq
n}$ is a partial play then $\sigma_{\ast}((b_{i})_{i\leq
n})\in\mathcal{M}(b_{n})$, i.e. $\sigma_{\ast}$ takes partial plays that end
with a position that $\ast$ plays and provides a move for $\ast$. A strategy
$\sigma$ is called winning for $\ast$ starting from $b_{0}$, if every play
$(b_{n})_{n}$ starting with $b_{0}$ in which $\ast$ follows $\sigma$ (that is
if $b_{n}\in B_{\ast}$ then $b_{n+1}=\sigma((b_{i})_{i\leq n})$) is winning
for $\ast$. A position is called winning for $\ast$ if $\ast$ has a winning
strategy starting from $b_{0}$. In positional games strategies can be
simplified, given that the history of the game is irrelevant to whether a
player can win from a particular position. Hence in positional games
strategies are functions $\sigma_{\ast}:B_{\ast}\to B$, such that
$\sigma_{\ast}(b)\in\mathcal{M}(b)$.

Given a position $b_{0}$, the _game tree generated from $b_{0}$_ is a tree
defined recursively with root $b_{0}$ and the children of $b$ are exactly
$\mathcal{M}(b)$. Each branch of the tree is a play starting from $b_{0}$.
Given a strategy $\sigma_{\ast}$ and a position $b_{0}$ the game tree
generated by $b_{0}$ following $\sigma_{\ast}$ is defined recursively with
root $b_{0}$, and if $b\in B_{\ast}$ it only has one child $\sigma_{\ast}(b)$,
otherwise the children of $b$ are exactly $\mathcal{M}(b)$. Each branch of
this tree is a play starting from $b_{0}$ according to $\sigma_{\ast}$, and
$\sigma$ is winning for $\ast$ from $b_{0}$, if all the branches of this tree
are winning plays for $\ast$.

Finally, a game is called _determined_ if every position either has a winning
strategy for $\forall$ or for $\exists$. Using backwards induction on game
trees it can be shown that finite board games, i.e. games that all the
branches of the game tree from any point has finite length, are determined.

###  2.3 Unfolding game on power-set algebras

In this section we recall the unfolding games defined on power-set algebras
that provide an alternative way to obtain the greatest and least fixed points
of a monotone map on a Boolean algebra. Let $\mathcal{P}(S)$ be a power-set
algebra and $f$ be a monotone map on it and consider the following game board.

state | player | admissible moves
---|---|---
$a\in S$ | $\exists$ | $\\{A\subseteq S\mid a\in f(A)\\}$
$A\subseteq S$ | $\forall$ | $\\{a\mid a\in A\\}$

We use $G_{\exists}^{f}(a)$ and $G_{\forall}^{f}(a)$ to denote games on the
above board with starting position $a$ and winning condition that infinite
plays are won by $\exists$ and $\forall$ respectively. For the finite play,
the player who has no admissible moves available loses in both cases. The
following lemma says that the unfolding game can be used to describe the least
and the greatest fixed points of $f$.

######  Theorem 2.2 (3.14 in [16])

The set $\\{a\mid\exists\mbox{ has a winning strategy for
}G_{\exists}^{f}(a)\\}$ is the greatest fixed point of $f$ and the set
$\\{a\mid\exists\mbox{ has a winning strategy for }G_{\forall}^{f}(a)\\}$ is
the least fixed points of $f$.

###  2.4 Classical modal $\mu$-calculus

In this section, we give some basic preliminaries on modal $\mu$-calculus. For
more details on modal $\mu$-calculus, we refer to [16]. Let
$\mathrm{P},\mathrm{X}$ be (countable) sets of atomic propositions and
variables. The language of classical modal $\mu$-calculus $\mathcal{L}_{c}$ is
given by the following recursion.

$\varphi::=\,p\mid\neg p\mid
x\mid\bot\mid\top\mid\varphi\vee\varphi\mid\varphi\wedge\varphi\mid\Box\varphi\mid\Diamond\varphi\mid\mu
x.\varphi\mid\nu x.\varphi,$

where $p\in\mathrm{P}$ and $x\in X$. We use $\eta x.\varphi$ to denote a
formula which is of the form $\mu x.\varphi$ or $\nu x.\varphi$. An occurrence
of a variable $x$ is said to be bound in a formula $\varphi$ if it occurs
under the scope of a fixed point operator $\mu x$ or $\nu x$ and free
otherwise. Given a Kripke model $M$ a formula with a free variable $x$ intends
to signify a monotone map on the complex algebra of $M$ with input $x$ build
from the monotone maps that correspond to the language connectives. Then the
formulas $M,w\Vdash\mu x.\varphi$ and $M,w\Vdash\nu x.\varphi$ exactly when
$w$ belongs in the least and greatest fixed points respectively of the map
signified by $\varphi$. It is well known that the variables of any fixed point
formula can be rewritten in such a way that no variable occurs as both free
variable and bound variable. Moreover, every bounded variable occurs in the
scope of only one fixed point operator. Thus, for any bound variable $x$ and
any formula $\varphi$, there exists an unique formula $\psi_{x}$ such that
$\eta x.\psi_{x}$ is a sub-formula of $\varphi$. We define a dependency order
on bounded variables of a formula as follows. For any bounded variables $x$
and $y$ appearing in formula $\varphi$, $x\leq_{\varphi}y$ iff $y$ occurs
freely in $\psi_{x}$.

The semantics of the language of the modal $\mu$-calculus on a Kripke frame
$M=(W,R,V)$ is given through the board game $G(M)$ described in the table
below. Positions are of the form $(w,\varphi)$, where $w\in W$.

state | player | admissible moves
---|---|---
$(w,\varphi_{1}\vee\varphi_{2})$ | $\exists$ | $\\{(w,\varphi_{1}),(w,\varphi_{2})\\}$
$(w,\varphi_{1}\wedge\varphi_{2})$ | $\forall$ | $\\{(w,\varphi_{1}),(w,\varphi_{2})\\}$
$(w,p)$, where $V,w\vdash p$ | $\forall$ | $\emptyset$
$(w,p)$, where $V,w\not\vdash p$ | $\exists$ | $\emptyset$
$(w,\top)$ | $\forall$ | $\emptyset$
$(w,\bot)$ | $\exists$ | $\emptyset$
$(w,\Diamond\varphi)$ | $\exists$ | $\\{(w^{\prime},\varphi)\mid wRw^{\prime}\\}$
$(w,\Box\varphi)$ | $\forall$ | $\\{(w^{\prime},\varphi)\mid wRw^{\prime}\\}$
$(w,\eta x.\varphi_{x})$ | - | $(w,\varphi_{x})$
$(w,x)$ | - | $(w,\eta x.\varphi_{x})$

where $\eta=\mu$ or $\eta=\nu$. For a finite play, a player wins if their
opponent gets stuck (i.e. there is no admissible move available). An infinite
play with starting position $(w,\varphi)$ is won by $\exists$ if the
$\leq_{\varphi}$-maximal variable which repeats infinitely often is
$\nu$-variable and by $\forall$ otherwise111That such a maximal variable
exists is not hard to see: if $y$ and $x$ repeat infinitely often in a play
and $x\nleq_{\varphi}y$ then either $y$ appears bounded in $\psi_{x}$, i.e.
$y\leq_{\varphi}x$, or $y$ doesn’t appear in $\psi_{x}$ in which case for $y$
to repeat again after an position of the form $(w,x)$, some variable $z$ that
is free in $\psi_{x}$ must appear such that $z$ is also free in $\psi_{y}$.
See also [16].. The following Lemma draws the connection between the games and
the semantics of the modal $\mu$-calculus.

######  Lemma 1 (Theorem 3.30, [16])

Given a Kripke model $M$, $M,w\Vdash\varphi$ if and only if $\exists$ has a
winning strategy for $G(M)$ from position $(w,\varphi)$.

###  2.5 Non-distributive modal logic

In the present section, we recall the definition and relational semantics of
the basic normal non-distributive modal logic in the modal signature
$\\{\Box,\Diamond\\}$. This and other similar logics have been studied in the
context of a research program aimed at introducing the logical foundations of
categorization theory [5, 4, 3]. In this context, $\Box c$ and $\Diamond c$
can be given e.g. the epistemic interpretation of the categories of the
objects which are certainly, and possibly members of category $c$
respectively. Motivated by these ideas, in [7], possible interpretations of
(modal) non-distributive logics are systematically discussed also in their
connections with their classical interpretation. The presentation below is
based on [8], [10].

####  2.5.1 Basic normal non-distributive modal logic

Let $\mathrm{P}$ be a (countable) set of atomic propositions. The language
$\mathcal{L}$ is defined as follows:

$\varphi::=p\mid\bot\mid\top\mid\varphi\wedge\varphi\mid\varphi\vee\varphi\mid\Box\varphi\mid\Diamond\varphi,$

where $p\in\mathrm{P}$. The basic, or minimal normal $\mathcal{L}$-logic
$\mathbf{L}$ is a set of sequences $\varphi\vdash\psi$ with
$\varphi,\psi\in\mathcal{L}$, containing the following axioms:

$p\vdash p$ |  | $\bot\vdash p$ |  | $p\vdash p\vee q$ |  | $p\wedge q\vdash p$ |  | $\top\vdash\Box\top$ |  | $\Box p\wedge\Box q\vdash\Box(p\wedge q)$
---|---|---|---|---|---|---|---|---|---|---
|  | $p\vdash\top$ |  | $q\vdash p\vee q$ |  | $p\wedge q\vdash q$ |  | $\Diamond\bot\vdash\bot$ |  | $\Diamond(p\vee q)\vdash\Diamond p\vee\Diamond q$

and closed under the following inference rules:

$\frac{\varphi\vdash\chi\quad\chi\vdash\psi}{\varphi\vdash\psi}\ \
\frac{\varphi\vdash\psi}{\varphi\left(\chi/p\right)\vdash\psi\left(\chi/p\right)}\
\ \frac{\chi\vdash\varphi\quad\chi\vdash\psi}{\chi\vdash\varphi\wedge\psi}\ \
\frac{\varphi\vdash\chi\quad\psi\vdash\chi}{\varphi\vee\psi\vdash\chi}\ \
\frac{\varphi\vdash\psi}{\Box\varphi\vdash\Box\psi}\ \
\frac{\varphi\vdash\psi}{\Diamond\varphi\vdash\Diamond\psi}$

####  2.5.2 Polarity-based semantics of non-distributive modal logic

For any relation $R\subseteq G\times M$, and any $H\subseteq G$, $N\subseteq
M$,

$R^{(0)}[N]=\\{g\in G\mid\forall n(n\in N\rightarrow gRn)\\},\quad
R^{(1)}[H]=\\{m\in M\mid\forall h(h\in H\rightarrow hRm)\\}.$

###### Definition 1

A polarity is a structure $\mathbb{P}=(G,M,I)$ such that $G$ and $M$ are sets
and $I\subseteq G\times M$ is a binary relation. For every polarity
$\mathbb{P}$, the maps
$(\cdot)^{\uparrow}:\mathcal{P}(G)\rightarrow\mathcal{P}(M)$ and
$(\cdot)^{\downarrow}:\mathcal{P}(M)\rightarrow\mathcal{P}(G)$ are defined as
follows: $H^{\uparrow}=I^{(1)}[H]$ and $N^{\downarrow}=I^{(0)}[N]$, where
$H\subseteq G$ and $N\subseteq M$. The maps $(\cdot)^{\uparrow}$ and
$(\cdot)^{\downarrow}$ form a Galois connection between
$(\mathcal{P}(G),\subseteq)$ and $(\mathcal{P}(M),\subseteq)$, that is,
$N\subseteq H^{\uparrow}$ iff $H\subseteq N^{\downarrow}$ for all
$H\in\mathcal{P}(G)$ and $N\in\mathcal{P}(M)$.

###### Definition 2

A formal concept of the polarity $\mathbb{P}$ is a pair
$([\\![{c}]\\!],(\\![{c}]\\!))$ such that $[\\![{c}]\\!]\subseteq G$,
$(\\![{c}]\\!)\subseteq M$, and $[\\![{c}]\\!]^{\uparrow}=(\\![{c}]\\!)$,
$(\\![{c}]\\!)^{\downarrow}=[\\![{c}]\\!]$. It follows that $[\\![{c}]\\!]$
and $(\\![{c}]\\!)$ are Galois-stable, i.e.
$[\\![{c}]\\!]^{\uparrow\downarrow}=[\\![{c}]\\!]$ and
$(\\![{c}]\\!)^{\downarrow\uparrow}=(\\![{c}]\\!)$. The set $\mathbb{P}^{+}$
of the formal concepts of $\mathbb{P}$ can be partially ordered as follows:
for any $c,d\in\mathbb{P}^{+}$,

$c\leq d$ iff $[\\![{c}]\\!]\subseteq[\\![{d}]\\!]$ iff
$(\\![{d}]\\!)\subseteq(\\![{c}]\\!)$

With this order, $\mathbb{P}^{+}$, which is called the concept lattice, is a
complete lattice such that for any $\mathcal{K}\subseteq\mathbb{P}^{+}$,

$\bigwedge\mathcal{K}=(\bigcap\\{[\\![{c}]\\!]\mid
c\in\mathcal{K}\\},(\bigcap\\{[\\![{c}]\\!]\mid
c\in\mathcal{K}\\})^{\uparrow})$,

$\bigvee\mathcal{K}=((\bigcap\\{(\\![{c}]\\!)\mid
c\in\mathcal{K}\\})^{\downarrow},\bigcap\\{(\\![{c}]\\!)\mid
c\in\mathcal{K}\\})$.

The following results are standard.

###### Proposition 1

For any polarity $\mathbb{P}=(G,M,I)$, the concept lattice $\mathbb{P}^{+}$ is
completely join-generated by the set
$\\{\textbf{g}:=(g^{\uparrow\downarrow},g^{\uparrow})\mid g\in G\\}$ and is
completely meet-generated by the set
$\\{\textbf{m}:=(m^{\downarrow},m^{\downarrow\uparrow})\mid m\in M\\}$.

######  Theorem 2.3 (Birkhoff’s representation theorem)

Any complete lattice $\mathbb{L}$ is isomorphic to the concept lattice
$\mathbb{P}^{+}$ of some polarity $\mathbb{P}$.

###### Definition 3

An enriched formal context is a tuple
$\mathbb{F}=(\mathbb{P},R_{\Diamond},R_{\Box})$, where $\mathbb{P}=(G,M,I)$ is
a polarity, and $R_{\Diamond}\subseteq M\times G$ and $R_{\Box}\subseteq
G\times M$ are I-compatible relations, i.e., $R^{(0)}_{\Diamond}[g]$ (resp.
$R^{(0)}_{\Box}[m]$) and $R^{(1)}_{\Box}[g]$ (resp. $R^{(1)}_{\Diamond}[m]$)
are Galois-stable for all $g\in G$ and $m\in M$.

###### Definition 4

For any enriched formal context
$\mathbb{F}=(\mathbb{P},R_{\Diamond},R_{\Box})$, let the complex algebra of
$\mathbb{F}$ be
$\mathbb{F}^{+}:=(\mathbb{P}^{+},\Diamond^{\mathbb{P}^{+}},\Box^{\mathbb{P}^{+}})$
where $\mathbb{P}^{+}$ is the concept lattice of $\mathbb{P}$,
$\Diamond^{\mathbb{P}^{+}}$ and $\Box^{\mathbb{P}^{+}}$ are unary operators on
$\mathbb{P}^{+}$ defined as follows: for every $c\in\mathbb{P}^{+}$,

$\Diamond^{\mathbb{P}^{+}}(c):=((R^{(0)}_{\Diamond}[[\\![{c}]\\!]])^{\downarrow},R^{(0)}_{\Diamond}[[\\![{c}]\\!]])$,
$\Box^{\mathbb{P}^{+}}(c):=(R^{(0)}_{\Box}[(\\![{c}]\\!)],(R^{(0)}_{\Box}[(\\![{c}]\\!)])^{\uparrow})$.

Note that $\Diamond^{\mathbb{P}^{+}}$ is completely join-preserving and
$\Box^{\mathbb{P}^{+}}$ is completely meet-preserving.

###### Definition 5

A valuation on an enriched formal context
$\mathbb{F}=(\mathbb{P},R_{\Diamond},R_{\Box})$ is a map
$V:P\to\mathbb{P}^{+}$. For each $p\in P$, we let
$[\\![{p}]\\!]:=[\\![{V(p)}]\\!]$ (resp. $(\\![{p}]\\!):=(\\![{V(p)}]\\!)$)
denote the extension (resp. intension) of the interpretation of $p$ under $V$.
A valuation can be homomorphically extended to a valuation
$\overline{V}:\mathcal{L}\to\mathbb{P}^{+}$ on all the formulas of
$\mathcal{L}$. A model is a pair $(\mathbb{F},V)$, where $\mathbb{F}$ is an
enriched formal context, and $V$ is a valuation.

###### Definition 6

Any model $\mathbb{M}=(\mathbb{F},V)$ induces two ‘forcing’ relations $\Vdash$
and $\succ$ defined as follows for every $\varphi\in\mathcal{L}$:

$\mathbb{M},g\Vdash p$ |  iff $g\in[\\![{p}]\\!]_{\mathbb{M}}$ | $\mathbb{M},m\succ p$ |  iff $m\in(\\![{p}]\\!)_{\mathbb{M}}$
---|---|---|---
$\mathbb{M},g\Vdash\top$ | always | $\mathbb{M},m\succ\top$ |  iff $gIm$ for all $g\in G$
$\mathbb{M},m\succ\bot$ | always | $\mathbb{M},g\Vdash\bot$ |  iff $gIm$ for all $m\in M$
$\mathbb{M},g\Vdash\varphi\wedge\psi$ |  iff $\mathbb{M},g\Vdash\varphi$ and $\mathbb{M},g\Vdash\psi$ | $\mathbb{M},m\succ\varphi\wedge\psi$ |  iff $(\forall g\in G)$ $(\mathbb{M},g\Vdash\varphi\wedge\psi\Rightarrow gIm)$
$\mathbb{M},m\succ\varphi\vee\psi$ |  iff $\mathbb{M},m\succ\varphi$ and $\mathbb{M},m\succ\psi$ | $\mathbb{M},g\Vdash\varphi\vee\psi$ |  iff $(\forall m\in M)$ $(\mathbb{M},g\succ\varphi\vee\psi\Rightarrow gIm)$.

As to the interpretation of modal formulas:

$\mathbb{M},g\Vdash\Box\varphi$ |  iff $(\forall m\in M)(\mathbb{M},m\succ\varphi\Rightarrow gR_{\Box}m)$ |  | $\mathbb{M},m\succ\Box\varphi$ |  iff $(\forall g\in G)(\mathbb{M},g\Vdash\Box\varphi\Rightarrow gIm)$
---|---|---|---|---
$\mathbb{M},m\succ\Diamond\varphi$ |  iff for all $g\in G$, if $\mathbb{M},g\Vdash\varphi$ then $mR_{\Diamond}g$ |  | $\mathbb{M},g\Vdash\Diamond\varphi$ |  iff $(\forall m\in M)(\mathbb{M},m\succ\Diamond\varphi\Rightarrow gIm)$.

##  3 Game semantics for non-distributive modal logic

In this section, we develop the game theoretic semantics for the non-
distributive modal logic $\mathbf{L}$. An alternative game semantics
presentation can be found in [11].

In classical modal logic, the game semantics, as is shown in Lemma 1, take the
form of an “examination” (which also provides the naming convention of the two
players). Abelard is asking Eloisa to show the truthfulness of a formula in a
possible world in a Kripke model. This also provides an assymetry on the
moves. Player $\exists$ moves when the formula under question is defined
existentially, while $\forall$ moves when it is defined universally. As we saw
in Section 2.5, the polarity semantics of lattice based logics require two
relations, $\Vdash$ and $\succ$ and all formulas are recursively defined via
universal statements. Hence the game we define takes a different form. The two
players (finally) stand against each other as equals. Player $\exists$ is
responsible for showing that $g\Vdash\varphi$ and only moves on positions of
the form $(m,\varphi)$, while $\forall$ is responsible for showing that
$m\succ\varphi$ and only moves on positions of the form $(g,\varphi)$.
Concretely, given an enriched polarity $(\mathbb{P},R_{\Diamond},R_{\Box})$
where $\mathbb{P}=(G,M,I)$, the game board is defined by the following table:

state | player | admissible moves
---|---|---
$(g,p)$, where $V,g\Vdash p$ | $\forall$ | $\emptyset$
$(g,p)$, where $V,g\not\Vdash p$ | $\forall$ | $\\{(m,p)\mid gI^{c}m\\}$
$(m,p)$, where $V,m\succ p$ | $\exists$ | $\emptyset$
$(m,p)$, where $V,m\not\succ p$ | $\exists$ | $\\{(g,p)\mid gI^{c}m\\}$
$(g,\top)$ | $\forall$ | $\emptyset$
$(m,\bot)$ | $\exists$ | $\emptyset$
$(g,\bot)$ | $\forall$ | $\\{(m,\bot)\mid gI^{c}m\\}$
$(m,\top)$ | $\exists$ | $\\{(g,\top)\mid gI^{c}m\\}$
$(m,\varphi_{1}\vee\varphi_{2})$ | $\exists$ | $\\{(m,\varphi_{1}),(m,\varphi_{2})\\}$
$(g,\varphi_{1}\vee\varphi_{2})$ | $\forall$ | $\\{(m,\varphi_{1}\vee\varphi_{2})\mid gI^{c}m\\}$
$(g,\varphi_{1}\wedge\varphi_{2})$ | $\forall$ | $\\{(g,\varphi_{1}),(g,\varphi_{2})\\}$
$(m,\varphi_{1}\wedge\varphi_{2})$ | $\exists$ | $\\{(g,\varphi_{1}\wedge\varphi_{2})\mid gI^{c}m\\}$
$(m,\Diamond\varphi)$ | $\exists$ | $\\{(g,\varphi)\mid mR_{\Diamond}^{c}g\\}$
$(g,\Diamond\varphi)$ | $\forall$ | $\\{(m,\Diamond\varphi)\mid gI^{c}m\\}$
$(g,\Box\varphi)$ | $\forall$ | $\\{(m,\varphi)\mid gR_{\Box}^{c}m\\}$
$(m,\Box\varphi)$ | $\exists$ | $\\{(g,\Box\varphi)\mid gI^{c}m\\}$

Since the moves of the game reduce the complexity of formulas in at most two
moves, every play in this game is finite. Hence a player wins if the other
player has no legitimate move, and so the game is positional and determined.
The lemma below is an analogue of Lemma 1 and shows the correspondence between
the game and the polarity semantics. Given that the game is determined, it’s
enough to show the existence of winning strategies for one player only.

###### Lemma 2

For any valuation $V:\mathrm{P}\to\mathbb{L}$, $\varphi\in\mathbf{L}$, and
$g\in G$ (resp. $m\in M$), $V,g\Vdash\varphi$ (resp. $V,m\not\succ\varphi$)
iff $\exists$ has a winning strategy for the game starting with the initial
position $(g,\varphi)$ (resp. $(m,\varphi)$).

###### Proof

We proceed via induction on $\varphi$. For the base case, assume that
$V,g\Vdash p$. By the rules of the game, $(g,p)$ is a position that $\forall$
has no moves and hence loses, so this is the winning position for $\exists$.
Likewise $V,m\succ p$ is winning for $\forall$. Assume $V,g\not\Vdash p$, then
there exists some $m$, such that $V,m\succ p$ and $gI^{c}m$. Then picking
$(m,p)$ is a winning strategy for $\forall$, and hence $\exists$ doesn’t have
a winning strategy. The case for $V,m\not\succ p$ and when $\varphi$ is $\top$
or $\bot$ is analogous.

We assume this holds for any formula $\varphi$, then we need to prove it also
holds for $\varphi\vee\psi$, $\varphi\wedge\psi$, $\Diamond\varphi$ and
$\Box\varphi$.

Let $\varphi$ be $\varphi_{1}\vee\varphi_{2}$. Assume
$V,m\not\succ\varphi_{1}\vee\varphi_{2}$, then by the definition,
$m\not\succ\varphi_{1}$ or $m\not\succ\varphi_{2}$, and by the induction
hypothesis, at $(m,\varphi_{1})$ $\exists$ has a winning strategy $\sigma_{1}$
or at $(m,\varphi_{2})$ $\exists$ has a winning strategy $\sigma_{2}$, and
assume w.l.o.g. the first is the case. Then the strategy at
$(m,\varphi_{1}\vee\varphi_{2})$ where she picks $(m,\varphi_{1})$ and follows
$\sigma_{1}$ is a winning strategy for $\exists$. Conversely, assume $\exists$
has a winning strategy at $(m,\varphi_{1}\vee\varphi_{2})$, then it means
$\exists$ has a winning strategy $\sigma_{1}$ at $(m,\varphi_{1})$ or she has
a winning strategy $\sigma_{2}$ at $(m,\varphi_{2})$. By induction hypothesis,
$m\not\succ\varphi_{1}$ or $m\not\succ\varphi_{2}$, and by definition,
$m\not\succ\varphi_{1}\vee\varphi_{2}$.

Assume $V,g\Vdash\varphi_{1}\vee\varphi_{2}$, and by definition, for all $m\in
M$, if $m\succ\varphi_{1}$ and $m\succ\varphi_{2}$ then $gIm$, which means for
all $m\in M$ if $gI^{c}m$ then $m\not\succ\varphi_{1}$ or
$m\not\succ\varphi_{2}$, thus for all $m\in M$ if $gI^{c}m$ then
$m\not\succ\varphi_{1}\vee\varphi_{2}$, thus for all $m\in M$ if $gI^{c}m$
then, by what was discussed in the previous paragraph, $\exists$ has a winning
strategy $\sigma_{m}$ at $(m,\varphi_{1}\vee\varphi_{2})$. This means that at
$(g,\varphi_{1}\vee\varphi_{2})$, no matter what $\forall$ chooses, $\exists$
always has a winning strategy, and thus has a winning strategy at
$(g,\varphi_{1}\vee\varphi_{2})$. Conversely, assume that $\exists$ has a
winning strategy $\sigma$ at $(g,\varphi_{1}\lor\varphi_{2})$, which means
that for every $m\in M$ such that $gI^{c}m$, $\exists$ has a winning strategy
at $(m,\varphi_{1}\lor\varphi_{2})$. By what was discussed in the paragraph
above, this means that $V,m\not\succ\varphi_{1}\lor\varphi_{2}$ for all such
$m$. That is, if $V,m\succ\varphi_{1}\lor\varphi_{2}$, then $gIm$, which by
definition means that $V,g\Vdash\varphi_{1}\lor\varphi_{2}$.

Let $\varphi$ be $\varphi_{1}\wedge\varphi_{2}$. Assume
$V,g\Vdash\varphi_{1}\wedge\varphi_{2}$, then by definition,
$g\Vdash\varphi_{1}$ and $g\Vdash\varphi_{2}$, and by the induction
hypothesis, at $(g,\varphi_{1})$ $\exists$ has a winning strategy
$\sigma_{1}$, and at $(g,\varphi_{2})$ $\exists$ has a winning strategy
$\sigma_{2}$. Then at $(g,\varphi_{1}\wedge\varphi_{2})$, if $\forall$ chooses
$(g,\varphi_{1})$ then $\exists$ follows the winning strategy $\sigma_{1}$ and
if $\forall$ chooses $(g,\varphi_{2})$ then $\exists$ follows winning strategy
$\sigma_{2}$. Thus $\exists$ always has a winning strategy at
$(g,\varphi_{1}\wedge\varphi_{2})$. Conversely, assume $\exists$ has a winning
strategy at $(g,\varphi_{1}\wedge\varphi_{2})$, it means $\exists$ has a
winning strategy at both $(g,\varphi_{1})$ and $(g,\varphi_{2})$, and by
induction hypothesis, $g\Vdash\varphi_{1}$ and $g\Vdash\varphi_{2}$, which
means $g\Vdash\varphi_{1}\wedge\varphi_{2}$. The case for
$V,m\not\succ\varphi_{1}\wedge\varphi_{2}$ is verbatim the same as the case
for $V,g\Vdash\varphi_{1}\vee\varphi_{2}$.

Let $\varphi$ be $\Diamond\psi$. Assume $V,m\not\succ\Diamond\psi$, and by
definition, there exists $g_{0}\in G$ such that $g_{0}\Vdash\psi$ but
$mR^{c}_{\Diamond}g_{0}$, and by induction hypothesis, $\exists$ has a winning
strategy $\sigma$ at such $(g_{0},\psi)$. Thus she has a winning strategy at
$(m,\Diamond\psi)$, which is picking $(g,\psi)$ and following $\sigma$
afterwards. Conversely, assume that $\exists$ has a winning strategy at
$(m,\Diamond\psi)$. This means there exists some $g\in G$ such that
$mR^{c}_{\Diamond}g$ and she has a winning strategy at $(g,\psi)$. By the
induction hypothesis $V,g\Vdash\psi$, while $mR^{c}_{\Diamond}g$, and so
$V,m\not\succ\Diamond\psi$.

Assume $g\Vdash\Diamond\psi$, and by definition, for all $m\in M$, if
$gI^{c}m$ then $m\not\succ\Diamond\psi$. By the above $\exists$ has a winning
strategy at $(m,\Diamond\psi)$, for all such $m$. Thus no matter what
$\forall$ plays $\exists$ has a winning strategy, which means $\exists$ has a
winning strategy at $(g,\Diamond\psi)$. Conversely, assume $\exists$ has a
winning strategy at $(g,\Diamond\psi)$. Then for every $m\in M$ such that
$gI^{c}m$, $\exists$ has a winning strategy at $(m,\Diamond\psi)$. By the
paragraph above, this means that $V,m\not\succ\Diamond\psi$ for all such $m$.
That is, if $V,m\succ\Diamond\psi$ then $gIm$ which, by definition, means that
$g\Vdash\Diamond\psi$.

Let $\varphi$ be $\Box\psi$. Assume $g\Vdash\Box\psi$, then by definition, for
all $m\in M$, if $gR^{c}_{\Box}m$ then $m\not\succ\psi$, and by induction
hypothesis, for all $m\in M$, if $gR^{c}_{\Box}m$ then $\exists$ has a winning
strategy at $(m,\psi)$, which means for any move of $\forall$ at
$(g,\Box\psi)$, $\exists$ has a winning strategy, thus $\exists$ has a winning
strategy at $(g,\Box\psi)$. Conversely, assume that $\exists$ has a winning
strategy at $(g,\Box\psi)$, which means that for every $m\in M$ such that
$gR^{c}_{\Box}m$, $\exists$ has a winning strategy at $(m,\psi)$, which by the
induction hypothesis means that $m\not\succ\psi$, for all such $m$. That is,
if $m\succ\psi$ then $gR_{\Box}m$, which, by definition, means that
$g\Vdash\Box\psi$. The case for $m\not\succ\Box\varphi$ is verbatim the same
as that for $g\Vdash\Diamond\psi$.

This concludes the proof.

##  4 Game semantics for non-distributive modal $\mu$-calculus

The aim of this section is to expand the language of lattice-based modal logic
with connectives that allow to describe fixed points, and define adequate game
semantics. We will start by introducing the language and its semantics via the
complex algebra of the polarity. Then we will generalize the unfolding game
defined in Section 2.3. Finally we will introduce the game semantics for the
fixed point connectives and show that they are adequate.

###  4.1 Non-distributive modal $\mu$-calculus

In this section, we develop the non-distributive modal $\mu$-calculus which is
a generalization of modal $\mu$-calculus to non-distributive or lattice-based
modal logic. The language $\mathcal{L}_{N}$ of non-distributive modal
$\mu$-calculus is given by the following recursion. For the sake of our
presentation we will introduce two sets of variables $X$ and $Y$ (in principle
disjoint). Elements $x\in X$ will be exclusively bound by the greatest fixed
point connective, while elements $y\in Y$ will be exclusively bound by the
least fixed point connective. This choice is purely stylistic and is taken to
more clearly present the game semantics later on.

$\varphi::=\,p\mid x\mid
y\mid\bot\mid\top\mid\varphi\vee\varphi\mid\varphi\wedge\varphi\mid\Box\varphi\mid\Diamond\varphi\mid\mu
y.\varphi\mid\nu x.\varphi.$

Again, we assume that the variables of any formula are renamed in such a way
that no variable occurs as both free and bounded variable and every bounded
variable occurs only under the scope of one fixed point operator. Similarly
again, given a formula $\varphi$ we can define the dependency order on its
bound variables, $z_{1}\leq_{\varphi}z_{2}$ iff $z_{2}$ occurs freely in
$\psi_{z_{1}}$.

Given now an enriched polarity based on $\mathbb{P}$, and its concept lattice
$\mathbb{P}^{+}$, any valuation $v$ on atomic propositions and variables
extends to a valuation on every formula. Hence given $v:P\to\mathbb{P}$, we
will treat $\overline{v}(\varphi):\mathbb{P}^{+}\to\mathbb{P}^{+}$, as a
function with input the variables of $\varphi$ and output the interpretation
of $\varphi$ under that assignment of its variables. Then we will interpret
$\overline{v}(\mu y.\varphi)$ as $\mathrm{lfp}(\overline{v}(\varphi)(y))$ and
$\overline{v}(\nu x.\varphi)$ as $\mathrm{gfp}(\overline{v}(\varphi)(x))$.
Finally we have:

$g\Vdash\eta z.\varphi$ iff $\textbf{g}\leq\overline{v}(\eta z.\varphi)$,

$m\succ\eta z.\varphi$ iff $\overline{v}(\eta z.\varphi)\leq\textbf{m}$.

####  4.1.1 Unfolding games with join generators

We consider the following game board:

state | player | admissible moves
---|---|---
$\mathbf{j}\in J^{\infty}(\mathbb{L})$ | $\exists$ | $\\{S\subseteq J^{\infty}(\mathbb{L})\mid\mathbf{j}\leq f(\bigvee S)\\}$
$S\subseteq J^{\infty}(\mathbb{L})$ | $\forall$ | $\\{\mathbf{j}\in J^{\infty}(\mathbb{L})\mid\mathbf{j}\in S\\}$

First, we consider the game in which all infinite plays are won by $\exists$.
We denote this game starting from $\mathbf{j}\in J^{\infty}(\mathbb{L})$ by
$G^{f}_{J^{\infty},\exists}(\mathbf{j})$. We have:

###### Lemma 3

Let $W=\\{\mathbf{j}\in J^{\infty}(\mathbb{L})\mid\exists\mbox{ has a winning
strategy in }G^{f}_{J^{\infty},\exists}(\mathbf{j})\\}$. Then $\bigvee W$ is
the greatest fixed point of $f$.

###### Proof

We show that $\bigvee W$ is a post-fixed point of $f$, namely that $\bigvee
W\leq f(\bigvee W)$, or equivalently that $\mathbf{j}\leq f(\bigvee W)$ for
any $\mathbf{j}\in W$. Let $\mathbf{j}\in W$. Since $\exists$ has a winning
strategy for $\mathbf{j}$, there is a $T\subseteq J^{\infty}(\mathbb{L})$ such
that $\mathbf{j}\leq f(\bigvee T)$ and $\exists$ has a winning strategy for
any move that $\forall$ can make, i.e., $T\subseteq W$. Hence $f(\bigvee
T)\leq f(\bigvee W)$, and since $\mathbf{j}\leq f(\bigvee W)$ we have
$\mathbf{j}\leq f(\bigvee W)$.

As $\bigvee W$ is a post-fixed point of $f$, it follows that $\bigvee W\leq
v$, where $v$ is the greatest fixed point of $f$. To show the converse
inequality is equivalent to show that $\forall\mathbf{i}(\mathbf{i}\leq
v\Rightarrow\mathbf{i}\leq\bigvee W)$; therefore it is sufficient to show that
any $\mathbf{i}\leq v$ is in $W$. Let $\mathbf{i}$ be any such nominals such
that $\mathbf{i}\leq v$. A winning strategy in the game
$G^{f}_{J^{\infty},\exists}(\mathbf{j})$ for $\exists$ consists in always
picking $\\{\mathbf{j}\in J^{\infty}(\mathbb{L})\mid\mathbf{j}\leq v\\}$: as
$f(v)=v$, it will always be possible for any subsequent choice of $\forall$.
This concludes the proof.

Now consider a variation of the game where all infinite plays are won by
$\forall$. We denote this game by $G^{f}_{J^{\infty},\forall}(\mathbf{j})$,
where $\mathbf{j}\in J^{\infty}(\mathbb{L})$ is the starting position of the
game.

###### Lemma 4

Let $W=\\{\mathbf{j}\in J^{\infty}(\mathbb{L})\mid\exists\mbox{ has a winning
strategy for }G^{f}_{J^{\infty},\forall}(\mathbf{j})\\}$. Then $\bigvee W$ is
the least fixed point of $f$.

###### Proof

We show that $\bigvee W$ is a pre-fixed point of $f$, namely that $f(\bigvee
W)\leq\bigvee W$, or equivalently that $\mathbf{j}\leq\bigvee W$ for any
$\mathbf{j}\leq f(\bigvee W)$. Let $\mathbf{j}\leq f(\bigvee W)$. At position
$\mathbf{j}$, $\exists$ can play $W$. Then $\forall$ must choose a position
$\mathbf{i}\in W$ to play, but this means $\exists$ has winning strategy at
$\mathbf{i}$. Therefore, $\exists$ has a winning strategy at $\mathbf{j}$,
i.e., $\mathbf{j}\in W$. Hence $\mathbf{j}\leq\bigvee W$.

As $\bigvee W$ is a pre-fixed point of $f$, it follows that $u\leq\bigvee W$,
where $u$ is the least fixed point of $f$. To show the converse inequality, it
is enough to show that $\mathbf{j}\leq u$ for any $\mathbf{j}\in W$. Assume
not, i.e., there exists $\mathbf{i}_{0}\in W$ and $\mathbf{i}_{0}\nleq
u=f(u)$. Because $\exists$ has a winning strategy at $\mathbf{i}_{0}$, there
exist a $B_{0}\subseteq J^{\infty}(\mathbb{L})$ such that $\mathbf{i}_{0}\leq
f(\bigvee B_{0})$ and since $B_{0}$ is a winning move, $B_{0}\subseteq W$.
Therefore, $f(\bigvee B_{0})\nleq f(u)$. By the monotonicity of $f$, we have
that $\bigvee B_{0}\nleq u$, i.e.,
$B_{0}\nsubseteq\\{\mathbf{j}\mid\mathbf{j}\leq u\\}$. So there exists a
position $\mathbf{i}_{1}\in B_{0}$ and $\mathbf{i}_{1}\nleq u$, where when
played by $\forall$, $\exists$ has a winning answer $B_{1}$. Continuing
recursively we can define a sequence of winning positions
$(\mathbf{i}_{n})_{n\in\omega}$ and $(B_{n})_{n\in\omega}$, such that
$B_{n}\neq\varnothing$, $B_{n}$ is a winning move of $\exists$ to
$\mathbf{i}_{n}$, and $\mathbf{i}_{n+1}\in B_{n}$. This means that the
sequence $(\mathbf{i}_{n},B_{n})$ is an infinite play, according to a winning
strategy of $\exists$, a contradiction since on infinite plays $\forall$ wins.
This concludes the proof.

####  4.1.2 Unfolding games with meet generators

Dual to the games defined above, we can define the following game board:

state | player | admissible moves
---|---|---
$\mathbf{m}\in M^{\infty}(\mathbb{L})$ | $\forall$ | $\\{S\subseteq M^{\infty}(\mathbb{L})\mid f(\bigwedge S)\leq\mathbf{m}\\}$
$S\subseteq M^{\infty}(\mathbb{L})$ | $\exists$ | $\\{\mathbf{m}\in M^{\infty}(\mathbb{L})\mid\mathbf{m}\in S\\}$

First, we consider the game where infinite plays are won by $\forall$. We
denote this game by $G^{f}_{M^{\infty},\forall}(\mathbf{m})$, where
$\mathbf{m}\in M^{\infty}(\mathbb{L})$ is the starting position of the game.

###### Lemma 5

Let $W=\\{\mathbf{m}\in M^{\infty}(\mathbb{L})\mid\forall\mbox{ has a winning
strategy for }G^{f}_{M^{\infty},\forall}(\mathbf{m})\\}$. Then $\bigwedge W$
is the least fixed point of $f$.

###### Proof

The proof of this lemma is analogous to Lemma 3.

Now consider a variation of the above game in which infinite plays are won by
$\exists$. We denote this game by $G^{f}_{M^{\infty},\exists}(\mathbf{m})$,
where $\mathbf{m}\in M^{\infty}(\mathbb{L})$ is the starting position of the
game.

###### Lemma 6

Let $W=\\{\mathbf{m}\in M^{\infty}(\mathbb{L})\mid\forall\mbox{ has a winning
strategy for }G^{f}_{M^{\infty},\exists}(\mathbf{m})\\}$. Then $\bigwedge W$
is the greatest fixed point of $f$.

###### Proof

The proof of this lemma is analogous to Lemma 4.

####  4.1.3 Considerations on generalizations

Shifting from a powerset algebra to a complete lattice offers a number of
possible generalizations. First, in a powerset algebra the atoms join-generate
the Boolean algebra. Secondly, every subset of atoms correspond to a unique
element of the Boolean algebra. In general complete lattices we might not have
enough join irreducibles (and certainly not enough join prime or atoms) to
generate the lattice and the joins of different sets of join generators may
correspond to the same element. Hence one might consider different
generalizations of the game, such as game $G^{\prime}$ presented in the
following table:

state | player | admissible moves
---|---|---
$\mathbf{j}\in J^{\infty}(\mathbb{L})$ | $\exists$ | $\\{u\in\mathbb{L}\mid\mathbf{j}\leq f(u)\\}$
$u\in\mathbb{L}$ | $\forall$ | $\\{\mathbf{j}\in J^{\infty}(\mathbb{L})\mid\mathbf{j}\leq u\\}$

This game may seem more natural. Player $\exists$ instead of choosing a set of
join generators picks an element of the lattice. The two game boards actually
coincide in the case of powerset algebras where the set of join generators is
the set of atoms. However if $\mathbb{L}$ is infinite and not distributive
then one cannot prove an analogue of Lemma 3. Consider the following lattice

${\top}$${\vdots}$${{a_{n}}}$${\vdots}$${b}$${{a_{2}}}$${{a_{1}}}$${\bot}$

where $f(\bot)=a_{1}$, $f(a_{n})=a_{n+1}$, and $f(b)=f(\top)=\top$. Then, from
point $b$, $\exists$ has only two possible moves ($\top$ or $b$) and from both
of them $\forall$ can play $b$. Hence, $\forall$ has a winning strategy for
$b$, which is below the least fixed point of $f$.

On the other hand, if $\mathbb{L}$ is finite or distributive and
$J^{\infty}(\mathbb{L})$ contains only join prime elements, then we can prove
a version of Lemma 3 as follows:

###### Lemma 7

Let $W=\\{\mathbf{j}\in J^{\infty}(\mathbb{L})\mid\exists\mbox{ has a winning
strategy for }G^{\prime}_{J^{\infty},\forall}(\mathbf{j})\\}$. Then $\bigvee
W$ is the least fixed point of $f$.

###### Proof

For every ordinal $\alpha$, we will show that $\\{\mathbf{j}\in
J^{\infty}(\mathbb{L})\ \mid\ \mathbf{j}\leq f^{\alpha}(\bot)\\}\subseteq W$.
We do this by recursion on $\alpha$. The statement is vacuously true for
$\alpha=0$. Assume that $\\{\mathbf{j}\in J^{\infty}(\mathbb{L})\ \mid\
\mathbf{j}\leq f^{\alpha}(\bot)\\}\subseteq W$ is the case, then for any
$\mathbf{j}\leq f(f^{\alpha}(\bot))$, playing $f^{\alpha}(\bot)$ is a winning
move for $\exists$, hence $\\{\mathbf{j}\in J^{\infty}(\mathbb{L})\ \mid\
\mathbf{j}\leq f^{\alpha+1}(\bot)\\}\subseteq W$. In case $\mathbb{L}$ is
finite, we know that the sequence $f^{\alpha}(\bot)$ is finite, hence we are
done. Now let $\alpha$ be a limit ordinal and assume that $\\{\mathbf{j}\in
J^{\infty}(\mathbb{L})\ \mid\ \mathbf{j}\leq f^{\beta}(\bot)\\}\subseteq W$
for every $\beta<\alpha$. Then $f^{\alpha}(\bot)=\bigvee f^{\beta}(\bot)$. It
follows that if $\mathbf{j}\leq f^{\alpha}(\bot)$, since $\mathbf{j}$ is a
join prime element, there exists a $\beta<\alpha$ such that $\mathbf{j}\leq
f^{\beta}(\bot)$, i.e. $\mathbf{j}\in W$. This concludes the proof.

###  4.2 Game semantics for non-distributive modal $\mu$-calculus

The game semantics for non-distributive modal $\mu$-calculus is obtained by
adding the following rules regarding fixed-point formulas to the game for non-
distributive modal logic. In what follows we use $x$ to denote variables
bounded by $\nu$, and $y$ to denote variables bounded by $\mu$.

state | player | admissible moves
---|---|---
$(g,\nu x.\varphi_{x})$ | - | $(g,\varphi_{x})$
$(g,x)$ | - | $(g,\nu x.\varphi_{x})$
$(m,\nu x.\varphi_{x})$ | $\exists$ | $\\{(g,\nu x.\varphi_{x})\mid gI^{c}m\\}$
$(m,x)$ | $\exists$ | $\\{(g,x)\mid gI^{c}m\\}$
$(m,\mu y.\varphi_{y})$ | - | $(m,\varphi_{y})$
$(m,y)$ | - | $(m,\mu y.\varphi_{y})$
$(g,\mu y.\varphi_{y})$ | $\forall$ | $\\{(m,\mu y.\varphi_{y})\mid gI^{c}m\\}$
$(g,y)$ | $\forall$ | $\\{(m,y)\mid gI^{c}m\\}$

If the game ends in the finite number of moves, then the player who gets stuck
in the end loses the game. In case, the game lasts infinite number of moves,
if the maximal bounded variable in the dependency order which gets repeated
infinite number of times in a play is $\nu$ variable, then the game is won by
$\exists$ and if it is $\mu$ variable then by $\forall$. These games are
parity games, and so are also determined [16, 5.22].

In the theorem below, to simplify notation, $\varphi_{x}$ will be treated both
as a formula and as the map on the concept lattice
$\mathbb{L}=\mathbb{P}^{+}$, given by $\overline{v}(\varphi_{x})$. That is,
$\varphi_{x}:\mathbb{L}\to\mathbb{L}$ given by
$\varphi_{x}(c)=([\\![{\varphi(x)}]\\!],(\\![{\varphi(x)}]\\!))$ where
$([\\![{x}]\\!],(\\![{x}]\\!))$ is set to $c$.

The following theorem says that the game described above is adequate for non-
distributive modal $\mu$-calculus.

###### Theorem 4.1

For any valuation $V:\mathrm{P}\to\mathbb{L}$, $\varphi\in\mathrm{L}_{N}$, and
$g\in G$ (resp. $m\in M$), $V,g\Vdash\varphi$ (resp. $V,m\not\succ\varphi$)
iff $\exists$ has a winning strategy for the game starting with the initial
position $(g,\varphi)$ (resp. $(m,\varphi)$).

###### Proof

The proof is by induction on the complexity of the formula $\varphi$. The base
case and inductive case for propositional and modal operators were already
discussed in the proof of the Lemma 2. Thus, to complete the proof we only
need to show the inductive step for the fixed point operators. Let
$\mathbb{L}=\mathbb{P}^{+}$ where $\mathbb{P}=(G,M,I)$. Suppose $\varphi:=\nu
x.\psi_{x}$ and let $c$ be the greatest fixed point of the function
$\psi_{x}$.

($\Rightarrow$) Let $V,g\Vdash\varphi$. By definition, we have
$g\in[\\![{c}]\\!]$. By Lemma 3, the game
$G^{\psi_{x}}_{J^{\infty},\exists}(g^{\uparrow\downarrow})$ is winning for
$\exists$, and in particular a winning strategy is always playing $c$. Let
$\mathrm{P}^{\prime}=\mathrm{P}\cup\\{x\\}$ and let $V^{\prime}$ be extension
of $V$ to $\mathrm{P}^{\prime}$ with
$V^{\prime}(x)=([\\![{c}]\\!],(\\![{c}]\\!))$. By the rules of the game
$G^{\psi_{x}}_{J^{\infty},\exists}(g^{\uparrow\downarrow})$, we have
$g^{\uparrow\downarrow}\leq\psi_{x}(c)$. Therefore,
$V^{\prime},g\Vdash\psi_{x}$. By the induction hypothesis, at $(g,\psi_{x})$
there exists a strategy $\sigma_{g}$ which is winning for $\exists$. Since $g$
was arbitrary such that $g^{\uparrow\downarrow}\leq c$, the strategy
$\bigcup_{g\in[\\![{c}]\\!]}\sigma_{g}$ is winning for $\exists$ from position
$(g^{\prime},\varphi)$ for any $g^{\prime}\in[\\![{c}]\\!]$. Indeed, either
from one point onwards $\exists$ follows a specific strategy $\sigma_{g}$,
which is winning for her, or $x$ repeats in the play infinitely often, which
means that $\exists$ wins. The proof for $m\succ\varphi$ is similar to e.g.
$m\succ\Box\psi$ from Lemma 2.

($\Leftarrow$) Assume that $(g,\varphi)$ is winning for $\exists$ and let
$\sigma$ be a winning strategy. We show that $g\in[\\![{c}]\\!]$ by showing
that the game $G^{\psi_{x}}_{J^{\infty},\exists}(g)$ is winning for $\exists$.

Let $\mathcal{T}$ be the game tree generated by the game starting from
$(g,\varphi)$ in which $\exists$ strictly follows $\sigma$. Let

$S_{\mathcal{T}}=\\{g^{\prime}\in G\mid(g^{\prime},x)\in\mathcal{T}\ \&\
((g^{\prime\prime},\psi)<_{\mathcal{T}}(g^{\prime},x)\Rightarrow\psi\neq
x)\\}$

that is the set of all elements of $G$, such that a position $(g^{\prime},x)$
with second component $x$ appears for the first time in a play according to
$\sigma$ from $(g,\varphi)$.

Let $P^{\prime}=P\cup\\{x\\}$ and notice that if we let
$V^{\prime}(x)=S^{\uparrow\downarrow}$, then $\sigma$ is winning for
$(g,\psi_{x})$, and by induction hypothesis $V^{\prime},g\Vdash\psi_{x}$.
Hence $g^{\uparrow\downarrow}\leq\psi_{x}(\bigvee S)$. Then the set $S$ is a
legitimate move for the game $G^{\psi_{x}}_{J^{\infty},\exists}(g)$. Now for
any choice $g^{\prime}$ that $\forall$ makes, we can proceed recursively using
the subtree of $\mathcal{T}$ generated by $(g^{\prime},\varphi)$.

This process recursively defines a strategy $\sigma^{\prime}$ for $\exists$
for the game $G^{\psi_{x}}_{J^{\infty},\exists}(g)$, which is winning since it
provides a play at every step and if the game continues infinitely $\exists$
wins. But then $g$ is a winning position for $\exists$ and by Lemma 3
$g\in[\\![{c}]\\!]$, i.e. $g\Vdash\varphi$.

The case for $\mu x.\psi_{x}$ is verbatim the same, defining a winning
strategy for $\forall$ using the game
$G^{f}_{M^{\infty},\forall}(\mathbf{m})$. This concludes the proof.

##  5 Conclusion and future direction

In this paper, we have generalized modal $\mu$-calculus to complete lattices.
We show that unfolding games can be generalized from power-set algebras to
complete lattices and they can be used to determine the greatest and the least
fixed points of any monotone operator in a complete lattice. We then define an
evaluation game for non-distributive modal $\mu$-calculus in polarity based
semantics and show adequacy of this game. This paper provides several
interesting directions for future research.

##### Model theory for non-distributive modal $\mu$-calculus.

It would be interesting to study model theoretic properties of non-
distributive modal logic. Modal $\mu$-calculus is known to be bisimulation
invariant. It would be interesting to generalize the notion of bisimulation to
the non-distributive setting. This would also provide insights on expressive
power of non-distributive modal $\mu$-calculus. Another interesting model
theoretic property to study for non-distributive modal $\mu$-calculus is
finite model property.

##### Proof theory for non-distributive modal $\mu$-calculus.

In future, we plan to develop a proof system for non-distributive modal
$\mu$-calculus. Completeness of modal $\mu$-calculus with respect to Kozen’s
axiomatization is an important result in the theory of modal $\mu$-calculus.
We would like to explore the possibility of providing similar axiomatization
in non-distributive setting.

##### Modelling categorization dynamics and applications.

As mention in introduction, fixed point operators arise in categorization in
many social and computational dynamic processes. One such example is common
knowledge operator discussed in [4]. We believe several categories formed from
dynamic social interaction can be modelled using fixed point operators. In
future, we intend to apply framework described in this paper to formalize and
reason about such scenarios and processes.

## References

  * [1] Ravi P Agarwal, Maria Meehan, and Donal O’regan.  Fixed point theory and applications, volume 141.  Cambridge university press, 2001.
  * [2] Julian Bradfield and Colin Stirling.  12 modal mu-calculi.  Studies in logic and practical reasoning, 3:721–756, 2007.
  * [3] Willem Conradie, Sabine Frittella, Krishna Manoorkar, Sajad Nazari, Alessandra Palmigiano, Apostolos Tzimoulis, and Nachoem M Wijnberg.  Rough concepts.  Information Sciences, 561:371–413, 2021.
  * [4] Willem Conradie, Sabine Frittella, A Palmigiano, M Piazzai, A Tzimoulis, and Nachoem M Wijnberg.  Toward an epistemic-logical theory of categorization.  Electronic Proceedings in Theoretical Computer Science, EPTCS, 251, 2017.
  * [5] Willem Conradie, Sabine Frittella, Alessandra Palmigiano, Michele Piazzai, Apostolos Tzimoulis, and Nachoem M Wijnberg.  Categories: how i learned to stop worrying and love two sorts.  In International Workshop on Logic, Language, Information, and Computation, pages 145–164. Springer, 2016.
  * [6] Willem Conradie, Alessandra Palmigiano, Claudette Robinson, Apostolos Tzimoulis, and Nachoem M Wijnberg.  The logic of vague categories.  arXiv preprint arXiv:1908.04816, 2019.
  * [7] Willem Conradie, Alessandra Palmigiano, Claudette Robinson, and Nachoem Wijnberg.  Non-distributive logics: from semantics to meaning.  In A. Rezus, editor, Contemporary Logic and Computing, volume 1 of Landscapes in Logic, pages 38–86. College Publications, 2020.
  * [8] Willem Conradie, Alessandra Palmigiano, Claudette Robinson, and Nachoem M. Wijnberg.  Non-distributive logics: from semantics to meaning.  arXiv: Logic, 2020.
  * [9] Andrzej Granas and James Dugundji.  Fixed point theory, volume 14.  Springer, 2003.
  * [10] Giuseppe Greco, Peter Jipsen, Krishna Manoorkar, Alessandra Palmigiano, and Apostolos Tzimoulis.  Logics for rough concept analysis.  ArXiv, abs/1811.07149, 2018.
  * [11] Chrysafis Hartonas.  Game-theoretic semantics for non-distributive logics.  Logic Journal of the IGPL, 27(5):718–742, 2019.
  * [12] Bronisław Knaster.  Un theoreme sur les functions d’ensembles.  Ann. Soc. Polon. Math., 6:133–134, 1928.
  * [13] Dexter Kozen.  Results on the propositional $\mu$-calculus.  Theoretical computer science, 27(3):333–354, 1983.
  * [14] Giacomo Lenzi.  The modal mu-calculus: a survey.  TASK Quarterly. Scientific Bulletin of Academic Computer Centre in Gdansk, 9(3):293–316, 2005.
  * [15] Alfred Tarski.  A lattice-theoretical fixpoint theorem and its applications.  1955\.
  * [16] Yde Venema.  Lectures on the modal $\mu$-calculus.  Renmin University in Beijing (China), 2008.


Multi-centered rotating black holes in
Kaluza–Klein theory
Edward Teo and Thomas Wan

Department of Physics, National University of Singapore, Singapore

Abstract

The most general charged and rotating black hole in Kaluza–Klein theory is
known to be described by the Rasheed–Larsen solution. When the under-rotating
extremal limit of this solution is taken, it falls into a general class of
solutions of Kaluza–Klein theory found by Clément, and is specified by two
harmonic functions on a three-dimensional flat base space. We use this fact to
generalise the single extremal black hole solution to one describing an
arbitrary superposition of such black holes. These black holes carry non-zero
electric and magnetic charges, which we set to be equal for simplicity, and
are in general rotating with parallel or anti-parallel spin vectors. It is
checked that the space-time outside the black holes is free of pathologies
such as naked singularities and closed time-like curves.

##  1 Introduction

Exact solutions of Einstein’s field equations describing two or more black
holes are of great interest, as they provide a window into the nature of the
interactions between black holes. However, due to the non-linearity of the
field equations, such solutions are not easy to come by. An example is the
Israel–Khan solution [1], which describes an arbitrary number of Schwarzschild
black holes placed along a symmetry axis. The black holes are kept in static
equilibrium by conical singularities stretching between them, which are
necessarily present to counterbalance their gravitational attraction.

If we require the space-time to be free of conical singularities and other
defects outside the black holes, then there must be another force present—such
as electromagnetism—to counterbalance gravity. An example is the
Majumdar–Papapetrou solution [2, 3] of Einstein–Maxwell theory, which
describes an arbitrary superposition of Reissner–Nordström black holes. In
this case, the black holes have to be extremally charged, so that the
electrostatic repulsion between them exactly cancels out their gravitational
attraction. Furthermore, the black holes can be located anywhere in the space-
time, unlike those in the Israel–Khan solution.

It is natural to wonder if there exists a rotating generalisation of the
Majumdar–Papapetrou solution. Such a solution was found by Israel and Wilson
[4] and Perjés [5], but it turns out that this solution describes a
superposition of naked singularities rather than black holes. It appears that
a balanced superposition of rotating black holes is not possible in
Einstein–Maxwell theory.

The purpose of this paper is to point out that a balanced superposition of
rotating black holes is possible, if we consider instead Kaluza–Klein theory
[6, 7]. This theory arises from the dimensional reduction of Einstein gravity
in five space-time dimensions, and was originally conceived as a way to unify
the gravitational and electromagnetic forces. However, it also gives rise to a
new massless scalar field, known as the dilaton, which has not been observed.
Nevertheless, the Kaluza–Klein method of dimensional reduction has found
applications in modern theories such as string theory.

The black holes of Kaluza–Klein theory have been extensively studied over the
years, beginning with the pioneering work of [8, 9, 10, 11, 12]. The most
general black hole solution of Kaluza–Klein theory was found by Rasheed [13],
and independently by Larsen [14, 15].111It was also independently found in
[16]. This black hole is specified by four parameters: mass, angular momentum,
electric charge and magnetic charge. Its various properties were studied in
detail in [13, 14, 15]. In particular, it was found that there are two
different ways to take the extremal limit of this black hole.

It is one of these extremal limits, known as the under-rotating limit, that
would be of interest to us. In this limit, the electric and magnetic charges
are both non-zero, and the angular momentum is free to take any value in a
certain range. This results in an extremally charged, rotating black hole
solution that takes a very simple mathematical form. In fact, it falls into a
class of solutions of Kaluza–Klein theory found by Clément [17, 18], and is
specified by a set of two harmonic functions on a three-dimensional flat base
space, which have poles at the location of the black hole. By superposing
multiple copies of these harmonic functions, we are able to construct a multi-
centered generalisation of this black hole.

We note that the use of harmonic functions on a flat base space to construct
multi-centered black hole solutions is common in supergravity theories, with
the balance of forces between the black holes attributed to the presence of
supersymmetry. Supersymmetric solutions describing multi-centered rotating
black holes in four dimensions have been found in, e.g., [19, 20, 21]. Even
the Israel–Wilson–Perjés solution—though not strictly a black hole
solution—can be embedded in $N=2$ supergravity. It is therefore somewhat
unusual that the multi-centered rotating black hole solution constructed in
this paper is not supersymmetric [14, 15], even though the forces between the
black holes balance out.

This paper is organised as follows: In Sec. 2, we review elements of
Kaluza–Klein theory, in particular the formalism of Maison [22], as well as
the general class of solutions found by Clément [17, 18]. In Sec. 3, we
present the Rasheed–Larsen black hole solution, and point out how one of its
extremal limits falls into the class of solutions found by Clément. We then
show in Sec. 4 how this single black hole solution, with equal electric and
magnetic charges, can be generalised to one describing an arbitrary
superposition of such black holes. Various properties of this multi-centered
rotating black hole solution are studied in Sec. 5. In Sec. 6, we present the
explicit solution for two black holes lying along a symmetry axis. The paper
concludes with a summary of the results obtained and some avenues for future
work.

##  2 Kaluza–Klein theory

The starting point of Kaluza–Klein theory is Einstein gravity in five space-
time dimensions, with the assumption that the metric is invariant under
translations of the extra space dimension $x^{5}$. Moreover, it is assumed
that $x^{5}$ is periodic with period $2\pi R_{\rm KK}$. In this case, the
five-dimensional metric can be written in the form

$\displaystyle\text{d}s_{(5)}^{2}={\rm
e}^{-\frac{2\phi}{\sqrt{3}}}\big{(}\text{d}x^{5}+A_{\mu}\text{d}x^{\mu}\big{)}^{2}+{\rm
e}^{\frac{\phi}{\sqrt{3}}}g_{\mu\nu}\text{d}x^{\mu}\text{d}x^{\nu},$ (2.1)

where $\mu,\nu=0,\dots,3$, and the functions $\phi$, $A_{\mu}$ and
$g_{\mu\nu}$ depend only on the coordinates $x^{\mu}$. The five-dimensional
Einstein–Hilbert action then reduces to the four-dimensional action

$\displaystyle 2\pi R_{\rm
KK}\int\text{d}^{4}x\sqrt{-g}\left(R-\frac{1}{2}\partial_{\mu}\phi\partial^{\mu}\phi-\frac{1}{4}{\rm
e}^{-\sqrt{3}\phi}F_{\mu\nu}F^{\mu\nu}\right),$ (2.2)

where $R$ is the four-dimensional Ricci scalar, $g=\det g_{\mu\nu}$, and
$F_{\mu\nu}=\partial_{\mu}A_{\nu}-\partial_{\nu}A_{\mu}$. This shows that
Kaluza–Klein theory can be regarded as a type of Einstein–Maxwell-dilaton
theory in four dimensions. The corresponding field equations are

$\displaystyle
R_{\mu\nu}=\frac{1}{2}\partial_{\mu}\phi\partial_{\nu}\phi+\frac{1}{2}{\rm
e}^{-\sqrt{3}\phi}\left(F_{\mu\rho}F_{\nu}{}^{\rho}-\frac{1}{4}g_{\mu\nu}F_{\rho\sigma}F^{\rho\sigma}\right),$
(2.3a) $\displaystyle\nabla_{\mu}\big{(}{\rm
e}^{-\sqrt{3}\phi}F^{\mu\nu}\big{)}=0\,,$ (2.3b)
$\displaystyle\nabla_{\mu}\nabla^{\mu}\phi=-\frac{\sqrt{3}}{4}{\rm
e}^{-\sqrt{3}\phi}F_{\mu\nu}F^{\mu\nu}.$ (2.3c)

The field equations (2.3) are difficult to solve without further assumptions.
At this stage, it is usual to assume the solution is stationary and possesses
some spatial symmetry. However, in this paper, we will only assume the former.
As shown by Maison [22], this is sufficient to enable the field equations to
be written in an elegant, simplified form. We now briefly describe this
formalism.

If we further require that the five-dimensional metric (2.1) is invariant
under translations of the time coordinate $x^{0}=t$, it can be written in the
form

$\displaystyle\text{d}s_{(5)}^{2}=\lambda_{ab}\big{(}\text{d}x^{a}+\omega^{a}{}_{i}\text{d}x^{i}\big{)}\big{(}\text{d}x^{b}+\omega^{b}{}_{j}\text{d}x^{j}\big{)}+\frac{1}{\tau}h_{ij}\text{d}x^{i}\text{d}x^{j},$
(2.4)

where $\tau\equiv-\det\lambda_{ab}$. Here, $a,b=0,5$, while $i,j=1,2,3$. The
functions $\lambda_{ab}$, $\omega^{a}{}_{i}$ and $h_{ij}$ depend only on the
three spatial coordinates $x^{i}$. From these functions, we can construct the
symmetric, unimodular $3\times 3$ matrix:

$\displaystyle\chi=\begin{pmatrix}\lambda_{ab}-\frac{1}{\tau}V_{a}V_{b}&\frac{1}{\tau}V_{a}\\\
\frac{1}{\tau}V_{b}&-\frac{1}{\tau}\end{pmatrix},$ (2.5)

where the so-called twist potentials $V_{a}$ are given by

$\displaystyle
V_{a,i}=\tau\lambda_{ab}\varepsilon_{i}{}^{jk}\omega^{b}{}_{j,k}\,.$ (2.6)

Here, the spatial indices $i,j,\dots$ are raised and lowered using the metric
$h_{ij}$, and $,i$ denotes the partial derivative $\frac{\partial}{\partial
x^{i}}$. With the definitions (2.5) and (2.6), the five-dimensional Einstein
equation can be written in the simple and suggestive form:

$\displaystyle R_{ij}=\frac{1}{4}\,{\rm
Tr}\,\big{(}\chi^{-1}\chi_{,i}\chi^{-1}\chi_{,j}\big{)}\,,$ (2.7a)
$\displaystyle\big{(}\chi^{-1}\chi^{,i}\big{)}_{;i}=0\,,$ (2.7b)

where $R_{ij}$ is the three-dimensional Ricci tensor corresponding to
$h_{ij}$, and $;i$ denotes the covariant derivative with respect to $h_{ij}$.

We note that the field equations (2.7) can be obtained from the three-
dimensional $\sigma$-model action

$\displaystyle\int\text{d}^{3}x\sqrt{h}\left[{}^{(3)}R-\frac{1}{4}\,{\rm
Tr}\,\big{(}\chi^{-1}\chi_{,i}\chi^{-1}\chi^{,i}\big{)}\right].$ (2.8)

This action has a manifest $SL(3,\mathbb{R})$ symmetry [22], which can be used
to generate new solutions from known ones. However, we will not use this
approach here; instead, we will construct solutions to the field equations
(2.7) directly.

In this paper, we are specifically interested in the case of a flat three-
dimensional metric $h_{ij}$. A very general class of solutions to (2.7) was
found by Clément [17, 18] for this case. These solutions can be written in the
form

$\displaystyle\chi=\eta{\rm e}^{Af}{\rm e}^{A^{2}g},$ (2.9)

where $\eta$ and $A$ are constant $3\times 3$ matrices, and $f$ and $g$ are
harmonic functions of $x^{i}$. If $f$ and $g$ vanish at infinity, then $\eta$
is given by

$\displaystyle\eta=\begin{pmatrix}-1&0&0\\\ 0&1&0\\\ 0&0&-1\end{pmatrix},$
(2.10)

which will ensure that the four-dimensional space-time is asymptotically
Minkowski. Since $\chi$ is symmetric and unimodular, we require that $A^{\rm
T}=\eta A\eta$, and that $A$ and $A^{2}$ are both traceless. Furthermore, we
require that $A^{3}$ is also traceless, so that (2.7a) is satisfied.

##  3 Rotating black hole solution

The most general rotating black hole solution of Kaluza–Klein theory was first
found by Rasheed [13]. It was constructed by performing a set of SO(1,2)
transformations on the Kerr solution, using the formalism of Maison [22]
reviewed in Sec. 2. This black hole solution can be parameterised by its mass
$M$, angular momentum $J$, electric charge $Q$, and magnetic charge $P$.

Now, the three-dimensional metric $h_{ij}$ of this solution is only flat when
a certain extremal limit is taken, known as the under-rotating limit. The
resulting class of extremal solutions satisfies the conditions [13]

$\displaystyle\Big{(}\frac{P}{M}\Big{)}^{\frac{2}{3}}+\Big{(}\frac{Q}{M}\Big{)}^{\frac{2}{3}}=2^{\frac{2}{3}},\qquad|J|<|PQ|\,.$
(3.1)

In the phase diagram Fig. 2 of [13], it forms a vertical wall (labelled by W)
which joins up to another class of extremal solutions along the $|J|=|PQ|$
curve.

The under-rotating class of extremal solutions is perhaps most compactly
expressed in the form found by Larsen [14]. It can be recovered from the
general solution in [14]222Note that there is a sign error in the general
solution given in [14]. Here, we shall use the corrected form of the solution
given in [23, 24]. by taking the limit $m,a\rightarrow 0$, such that
$\frac{a}{m}\rightarrow j$ where $j$ is a finite constant satisfying $|j|<1$.
We then obtain the five-dimensional metric:

$\displaystyle\text{d}s_{(5)}^{2}$
$\displaystyle=\frac{H_{2}}{H_{1}}\bigg{\\{}\text{d}x^{5}-\left[2\left(r+\frac{p}{2}\right)-{pj\cos\theta}\right]\frac{Q}{H_{2}}\,\text{d}t$
(3.2)
$\displaystyle\quad\qquad-\left[2H_{2}\cos\theta-q\left(r+{\frac{pq}{p+q}}\right)j\sin^{2}\theta\right]\frac{P}{H_{2}}\,\text{d}\varphi\bigg{\\}}^{2}$
(3.3)
$\displaystyle\quad-\frac{{r}^{2}}{H_{2}}\left(\text{d}t+{\frac{2jPQ\sin^{2}\theta\,\text{d}\varphi}{r}}\right)^{2}+H_{1}\left({\frac{{\text{d}r}^{2}}{{r}^{2}}}+{\text{d}\theta}^{2}+\sin^{2}\theta\,{\text{d}\varphi}^{2}\right),$
(3.4)

where

$\displaystyle H_{1}$
$\displaystyle\equiv{r}^{2}+rp+{\frac{{p}^{2}q\left(1+j\cos\theta\right)}{2(p+q)}}\,,$
(3.5a) $\displaystyle H_{2}$
$\displaystyle\equiv{r}^{2}+rq+{\frac{p{q}^{2}\left(1-j\cos\theta\right)}{2(p+q)}}\,.$
(3.5b)

Here, $(r,\theta,\varphi)$ are the standard spherical polar coordinates. The
parameters $p$ and $q$ satisfy $p,q>0$, and are related to the magnetic and
electric charges by

$\displaystyle P^{2}=\frac{{p}^{3}}{4(p+q)}\,,\qquad
Q^{2}=\frac{{q}^{3}}{4(p+q)}\,.$ (3.6)

For simplicity, we shall henceforth assume that $P$ and $Q$ are positive. We
also note that the mass and angular momentum of the black hole are given by

$\displaystyle M=\frac{p+q}{4}\,,\qquad J=jPQ\,.$ (3.7)

It can be checked, after some calculation, that this solution can be written
in the form (2.9), with

$\displaystyle
A=4\begin{pmatrix}-\frac{q}{p+q}&\big{(}\frac{q}{p+q}\big{)}^{\frac{3}{2}}&0\\\
-\big{(}\frac{q}{p+q}\big{)}^{\frac{3}{2}}&-\frac{p-q}{p+q}&\big{(}\frac{p}{p+q}\big{)}^{\frac{3}{2}}\\\
0&-\big{(}\frac{p}{p+q}\big{)}^{\frac{3}{2}}&\frac{p}{p+q}\end{pmatrix}.$
(3.8)

Note that $A^{3}=0$, so that the exponentials in (2.9) have series expansions
that are actually finite. The harmonic functions $f$ and $g$ are given by

$\displaystyle f=\frac{M}{r}\,,\qquad
g=\frac{JM^{2}}{2PQ}\frac{\cos\theta}{r^{2}}\,.$ (3.9)

A particularly simple case of this solution arises when $p=q$, i.e., when the
magnetic and electric charges are equal: $P=Q=\frac{M}{\sqrt{2}}$. In this
case, the matrix $A$ becomes

$\displaystyle A=\begin{pmatrix}-2&\sqrt{2}&0\\\ -\sqrt{2}&0&\sqrt{2}\\\
0&-\sqrt{2}&2\end{pmatrix},$ (3.10)

while the harmonic functions become

$\displaystyle f=\frac{M}{r}\,,\qquad g=\frac{J\cos\theta}{r^{2}}\,.$ (3.11)

The solution (3.2) then becomes

$\displaystyle\text{d}s_{(5)}^{2}$
$\displaystyle=\frac{H_{2}}{H_{1}}\bigg{\\{}\text{d}x^{5}-\sqrt{2}\,H_{2}^{-1}\left[M(r+M)-{2J\cos\theta}\right]\text{d}t$
(3.12)
$\displaystyle\quad\qquad-\sqrt{2}\left[M\cos\theta-2JH_{2}^{-1}(r+M)\sin^{2}\theta\right]\text{d}\varphi\bigg{\\}}^{2}$
(3.13)
$\displaystyle\quad-\frac{{r}^{2}}{H_{2}}\left(\text{d}t+{\frac{2J\sin^{2}\theta\,\text{d}\varphi}{r}}\right)^{2}+H_{1}\left({\frac{{\text{d}r}^{2}}{{r}^{2}}}+{\text{d}\theta}^{2}+\sin^{2}\theta\,{\text{d}\varphi}^{2}\right),$
(3.14)

where now $H_{1,2}=(r+M)^{2}\pm 2J\cos\theta$. The four-dimensional form of
this solution, after substituting in for $H_{1,2}$ and redefining
$r\rightarrow r-M$, is given by

$\displaystyle\text{d}s_{(4)}^{2}$
$\displaystyle=-\frac{(r-M)^{2}}{\left(r^{4}-4J^{2}\cos^{2}\theta\right)^{\frac{1}{2}}}\left(\text{d}t+{\frac{2J\sin^{2}\theta\,\text{d}\varphi}{r-M}}\right)^{2}$
(3.15a)
$\displaystyle\quad+\left(r^{4}-4J^{2}\cos^{2}\theta\right)^{\frac{1}{2}}\left[{\frac{{\text{d}r}^{2}}{{(r-M)}^{2}}}+{\text{d}\theta}^{2}+\sin^{2}\theta\,{\text{d}\varphi}^{2}\right],$
(3.15b) $\displaystyle A_{0}$
$\displaystyle=-\sqrt{2}\,\frac{Mr-2J\cos\theta}{r^{2}-2J\cos\theta}\,,\qquad
A_{\varphi}=-\sqrt{2}\left(M\cos\theta-\frac{2Jr\sin^{2}\theta}{r^{2}-2J\cos\theta}\right),$
(3.15c) $\displaystyle\phi$
$\displaystyle=\frac{\sqrt{3}}{2}\ln\left(\frac{r^{2}+2J\cos\theta}{r^{2}-2J\cos\theta}\right).$
(3.15d)

To our knowledge, the four-dimensional metric (3.15a) first appeared in [13].
When $J=0$, the dilaton vanishes and this solution reduces to the $P=Q$
extremal Reissner–Nordström solution.

##  4 Multi-centered rotating black hole solution

Since the under-rotating extremal black hole solution can be written in the
form (2.9), it is possible to generalise it to a multi-centered solution. For
simplicity, we only consider the case of equal electric and magnetic charges,
where the $A$ matrix is given by (3.10). Using Cartesian coordinates
${\boldsymbol{x}}=(x,y,z)$, we can simply replace the harmonic functions
(3.11) by

$\displaystyle
f=\sum_{n=1}^{N}\frac{M_{n}}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|}\,,\qquad
g=\sum_{n=1}^{N}\frac{J_{n}(z-z_{n})}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|^{3}}\,.$
(4.1)

The corresponding solution then describes a superposition of $N$ black holes
located at ${\boldsymbol{x}}={\boldsymbol{x}}_{n}$, each with mass $M_{n}$,
angular momentum $J_{n}$, and charges $P_{n}=Q_{n}=\frac{M_{n}}{\sqrt{2}}$.
Without loss of generality, we assume that all the black holes have different
positions ${\boldsymbol{x}}_{n}$. Note that the spin vectors of the black
holes are parallel or anti-parallel, in the sense that they point in either
the $+z$ or $-z$ direction, depending on the sign of $J_{n}$. When $J_{n}=0$,
this solution reduces to the Majumdar–Papapetrou solution with
$P_{n}=Q_{n}$.333The five-dimensional form of this solution was studied in
[25].

We can now compute the $\chi$ matrix for this solution using (2.9), and then
extract the various components of the five-dimensional metric (2.4) using
(2.5) and (2.6). In particular, it can be checked that (2.6) is equivalent to
the two equations (written in 3-vector notation):

$\displaystyle\nabla\times{\boldsymbol{\omega}}^{0}=-2\,\nabla
g\,,\qquad\nabla\times{\boldsymbol{\omega}}^{5}=-\sqrt{2}\,\nabla(f+2g)\,.$
(4.2)

If we denote
${\boldsymbol{\tilde{\omega}}}^{5}\equiv{\boldsymbol{\omega}}^{5}-\sqrt{2}\,{\boldsymbol{\omega}}^{0}$,
the solutions are given by444Each solution is defined only up to the gradient
of a scalar, but this term can be set to zero by an appropriate transformation
of $t$ and/or $x^{5}$ in (4.4).

$\displaystyle{\boldsymbol{\omega}}^{0}\cdot\text{d}{\boldsymbol{x}}$
$\displaystyle=-\sum_{n=1}^{N}\frac{2J_{n}}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|^{3}}[(y-y_{n})\text{d}x-(x-x_{n})\text{d}y]\,,$
(4.3a)
$\displaystyle{\boldsymbol{\tilde{\omega}}}^{5}\cdot\text{d}{\boldsymbol{x}}$
$\displaystyle=\sqrt{2}\,\sum_{n=1}^{N}\frac{M_{n}(z-z_{n})}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|}\,\frac{(y-y_{n})\text{d}x-(x-x_{n})\text{d}y}{(x-x_{n})^{2}+(y-y_{n})^{2}}\,.$
(4.3b)

After some calculation, we finally arrive at the five-dimensional metric:

$\displaystyle\text{d}s_{(5)}^{2}$
$\displaystyle=\frac{H_{-}}{H_{+}}\left[\text{d}x^{5}-\sqrt{2}\,\text{d}t+\sqrt{2}\,\frac{1+f}{H_{-}}\left(\text{d}t+{\boldsymbol{\omega}}^{0}\cdot\text{d}{\boldsymbol{x}}\right)+{\boldsymbol{\tilde{\omega}}}^{5}\cdot\text{d}{\boldsymbol{x}}\right]^{2}$
(4.4)
$\displaystyle\quad-\frac{1}{H_{-}}\left(\text{d}t+{\boldsymbol{\omega}^{0}}\cdot\text{d}{\boldsymbol{x}}\right)^{2}+H_{+}\,\text{d}{\boldsymbol{x}}\cdot\text{d}{\boldsymbol{x}}\,,$
(4.5)

where $H_{\pm}\equiv(1+f)^{2}\pm 2g$. The four-dimensional form of this
solution, after substituting in for $H_{\pm}$, is given by

$\displaystyle\text{d}s_{(4)}^{2}$
$\displaystyle=-\frac{1}{\left[(1+f)^{4}-4g^{2}\right]^{\frac{1}{2}}}\left(\text{d}t+{\boldsymbol{\omega}^{0}}\cdot\text{d}{\boldsymbol{x}}\right)^{2}+\left[(1+f)^{4}-4g^{2}\right]^{\frac{1}{2}}\text{d}{\boldsymbol{x}}\cdot\text{d}{\boldsymbol{x}}\,,$
(4.6a) $\displaystyle A_{0}$
$\displaystyle=-\sqrt{2}\,\frac{(1+f)f-2g}{(1+f)^{2}-2g}\,,\qquad
A_{i}=\sqrt{2}\,\frac{1+f}{(1+f)^{2}-2g}\,\omega^{0}_{i}+\tilde{\omega}^{5}_{i},$
(4.6b) $\displaystyle\phi$
$\displaystyle=\frac{\sqrt{3}}{2}\ln\left[\frac{(1+f)^{2}+2g}{(1+f)^{2}-2g}\right].$
(4.6c)

##  5 Properties of the multi-centered rotating black hole solution

We begin by briefly recalling some properties of the single black hole
solution (3.15) [13, 14, 15]. It is an asymptotically flat solution, with mass
$M$ and angular momentum $J$. The solution also carries equal magnetic and
electric charges, given by $P=Q=\frac{M}{\sqrt{2}}$. The parameters $M$ and
$J$ are subject to the constraint $|J|<\frac{M^{2}}{2}$. When $M=J=0$, the
solution reduces to empty Minkowski space-time.

There is a degenerate event horizon located at $r=M$, with non-vanishing area
$4\pi\sqrt{M^{4}-4J^{2}}$. There is also a curvature singularity at
$r=\sqrt{2|J\cos\theta|}$, but it will always lie below the event horizon.
These properties are consistent with the interpretation of the solution as an
extremal black hole. However, we note that the event horizon has zero angular
velocity, even if the black hole itself has a non-zero angular momentum.
Moreover, there is no ergoregion present in the space-time. These somewhat
unusual features are common to all the under-rotating extremal solutions.

Equipped with an understanding of the single black hole solution, we now turn
to the multi-centered black hole solution (4.6). From the form of the harmonic
functions $f$ and $g$ in (4.1), we see that it is an asymptotically flat
solution consisting of a superposition of $N$ separate sources in Minkowski
space-time, each with mass $M_{n}$, angular momentum $J_{n}$, and charges
$P_{n}=Q_{n}=\frac{M_{n}}{\sqrt{2}}$. To ensure that each source does indeed
have a consistent interpretation as a black hole, we require the condition

$\displaystyle|J_{n}|<\frac{M_{n}^{2}}{2}$ (5.1)

to hold individually for $n=1,\dots,N$.

The event horizon of the $n$-th black hole is located at
${\boldsymbol{x}}={\boldsymbol{x}}_{n}$. This can be verified by introducing
standard spherical polar coordinates $(r,\theta,\varphi)$ centered at
${\boldsymbol{x}}={\boldsymbol{x}}_{n}$, and taking the limit
$t\rightarrow\frac{t}{\epsilon}$, $r\rightarrow\epsilon r$ and
$\epsilon\rightarrow 0$ of the metric (4.6a). Indeed, we recover the same
near-horizon limit as that of the single black hole metric (3.15a). It follows
that the event horizon at $r=0$ is regular and has a non-vanishing area equal
to $4\pi\sqrt{M_{n}^{4}-4J_{n}^{2}}$.

By inspection of the metric (4.6a), the only other points at which
singularities can occur are where $(1+f)^{2}=2|g|$. By calculating the
curvature invariants, it can be seen that they are curvature singularities. We
now show that these curvature singularities all lie below the event horizons,
in regions of the space-time not covered by the Cartesian coordinates used
here. We first note that, for the $n$-th black hole,

$\displaystyle f_{n}^{2}-2|g_{n}|$
$\displaystyle=\frac{M_{n}^{2}}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|^{2}}-\frac{2|J_{n}||z-z_{n}|}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|^{3}}$
(5.2)
$\displaystyle\geq\frac{M_{n}^{2}-2|J_{n}|}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|^{2}}$
(5.3) $\displaystyle>0\,,$ (5.4)

where we have used the fact that
$|z-z_{n}|\leq|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|$ and (5.1). It follows
that

$\displaystyle(1+f)^{2}-2|g|$
$\displaystyle=\bigg{(}1+\sum_{n}f_{n}\bigg{)}^{2}-2\bigg{|}\sum_{n}g_{n}\bigg{|}$
(5.5) $\displaystyle>1+\sum_{n}f_{n}^{2}-2\sum_{n}|g_{n}|$ (5.6)
$\displaystyle>1\,.$ (5.7)

In the second step, we have used the fact that $f_{n}>0$ (since masses are
always positive) as well as the triangle inequality. Hence $(1+f)^{2}>2|g|$ at
every point on and outside the event horizons.

The existence of closed time-like curves (CTCs) in the space-time (4.6a) can
also be ruled out, if it can be shown that the coordinates $(x,y,z)$ remain
space-like everywhere in the space-time. Since ${\boldsymbol{\omega}^{0}}$ has
both $x$ and $y$ components, this result will follow if
$\left(\begin{smallmatrix}g_{xx}&g_{xy}\cr
g_{xy}&g_{yy}\end{smallmatrix}\right)$ is a positive-definite matrix. This is
equivalent to the positivity of its trace and determinant. Explicitly, these
two conditions are

$\displaystyle
g_{xx}+g_{yy}=\frac{2(1+f)^{4}-8g^{2}-\omega^{2}-\bar{\omega}^{2}}{\left[(1+f)^{4}-4g^{2}\right]^{\frac{1}{2}}}$
$\displaystyle>0\,,$ (5.8a) $\displaystyle
g_{xx}g_{yy}-g_{xy}^{2}=(1+f)^{4}-4g^{2}-\omega^{2}-\bar{\omega}^{2}$
$\displaystyle>0\,,$ (5.8b)

where we have defined $\omega\equiv\omega^{0}_{x}$ and
$\bar{\omega}\equiv\omega^{0}_{y}$ for brevity. Their expressions can be read
off from (4.3a).

It is straightforward to see that the second condition in (5.8) is stronger
than the first. To show that the second condition is satisfied, we first note
that, for the $n$-th black hole,

$\displaystyle f_{n}^{4}-4g_{n}^{2}-\omega_{n}^{2}-\bar{\omega}_{n}^{2}$
$\displaystyle=\frac{M_{n}^{4}}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|^{4}}-\frac{4J_{n}^{2}\left[(x-x_{n})^{2}+(y-y_{n})^{2}+(z-z_{n})^{2}\right]}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|^{6}}$
(5.9)
$\displaystyle=\frac{M_{n}^{4}-4J_{n}^{2}}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|^{4}}$
(5.10) $\displaystyle>0\,,$ (5.11)

where we have used (5.1) in the last step. It follows that

$\displaystyle(1+f)^{4}-4g^{2}-\omega^{2}-\bar{\omega}^{2}$ $\displaystyle=$
$\displaystyle\bigg{(}1+\sum_{n}f_{n}\bigg{)}^{4}-4\bigg{(}\sum_{n}g_{n}\bigg{)}^{2}-\bigg{(}\sum_{n}\omega_{n}\bigg{)}^{2}-\bigg{(}\sum_{n}\bar{\omega}_{n}\bigg{)}^{2}$
(5.12) $\displaystyle>$ $\displaystyle
1+\sum_{n}\left(f_{n}^{4}-4g_{n}^{2}-\omega_{n}^{2}-\bar{\omega}_{n}^{2}\right)$
(5.14) $\displaystyle\hskip 9.39545pt+\sum_{n\neq
m}\left(3f_{n}^{2}f_{m}^{2}-4g_{n}g_{m}-\omega_{n}\omega_{m}-\bar{\omega}_{n}\bar{\omega}_{m}\right)$
$\displaystyle>$ $\displaystyle 1+\sum_{n\neq
m}\left(3f_{n}^{2}f_{m}^{2}-4g_{n}g_{m}-\omega_{n}\omega_{m}-\bar{\omega}_{n}\bar{\omega}_{m}\right).$
(5.15)

In the second step, we have used the fact that $f_{n}>0$. But

$\displaystyle
3f_{n}^{2}f_{m}^{2}-4g_{n}g_{m}-\omega_{n}\omega_{m}-\bar{\omega}_{n}\bar{\omega}_{m}$
$\displaystyle\geq
3f_{n}^{2}f_{m}^{2}-4|g_{n}||g_{m}|-|\omega_{n}||\omega_{m}|-|\bar{\omega}_{n}||\bar{\omega}_{m}|$
(5.16)
$\displaystyle=\frac{3M_{n}^{2}M_{m}^{2}}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|^{2}|{\boldsymbol{x}}-{\boldsymbol{x}}_{m}|^{2}}-\frac{4|J_{n}||J_{m}|}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|^{3}|{\boldsymbol{x}}-{\boldsymbol{x}}_{m}|^{3}}\times$
(5.17)
$\displaystyle\quad\left(|x-x_{n}||x-x_{m}|+|y-y_{n}||y-y_{m}|+|z-z_{n}||z-z_{m}|\right)$
(5.18)
$\displaystyle\geq\frac{3M_{n}^{2}M_{m}^{2}-12|J_{n}||J_{m}|}{|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|^{2}|{\boldsymbol{x}}-{\boldsymbol{x}}_{m}|^{2}}$
(5.19) $\displaystyle>0\,,$ (5.20)

where we have used the fact that
$|x-x_{n}|,|y-y_{n}|,|z-z_{n}|\leq|{\boldsymbol{x}}-{\boldsymbol{x}}_{n}|$ in
the third step. We have also used (5.1) in the last step. Putting (5.12) and
(5.16) together, we see that (5.8b) is satisfied. This implies that (5.8a) is
also satisfied, so the space-time (4.6a) does not contain any CTCs.

We thus conclude that the superposition of multiple rotating sources in (4.1)
does not lead to any new pathologies such as naked singularities or CTCs. The
fact that the metric is smooth and invertible outside the event horizons,
shows that the space-time does not contain other defects such as conical
singularities or Dirac–Misner strings [26]. The interpretation of the solution
(4.6) as a balanced superposition of $N$ rotating black holes thus appears to
be a consistent one.

##  6 Solution for two black holes along a symmetry axis

The general solution (4.6) will simplify considerably when the black holes are
all placed along a straight line in the $z$-direction. This is due to the
solution becoming rotationally symmetric about this axis. In this section, we
will present the explicit form of this solution for the case of two black
holes. Without loss of generality, we choose them to be located at
$(x_{1},y_{1},z_{1})=(0,0,-\alpha)$ and $(x_{2},y_{2},z_{2})=(0,0,\alpha)$,
respectively, where $\alpha$ is a positive constant. If we assume that the
black holes have masses $M_{1}$ and $M_{2}$, and angular momenta $J_{1}$ and
$J_{2}$, respectively, the corresponding harmonic functions are

$\displaystyle f=\frac{M_{1}}{R_{1}}+\frac{M_{2}}{R_{2}}\,,\qquad
g=\frac{J_{1}(z+\alpha)}{R_{1}^{3}}+\frac{J_{2}(z-\alpha)}{R_{2}^{3}}\,,$
(6.1)

where $R_{1}\equiv\sqrt{x^{2}+y^{2}+(z+\alpha)^{2}}$ and
$R_{2}\equiv\sqrt{x^{2}+y^{2}+(z-\alpha)^{2}}$.

It is natural to introduce polar coordinates $(\rho,\varphi)$ given by

$\displaystyle x=\rho\cos\varphi\,,\qquad y=\rho\sin\varphi\,.$ (6.2)

The coordinates $(t,\rho,z,\varphi)$ are then the standard Weyl–Papapetrou
coordinates used for describing stationary and axisymmetric space-times. In
fact, since there are only two black holes in this case, it is possible to
further transform $(\rho,z)$ to prolate spheroidal coordinates $(\xi,\eta)$
given by

$\displaystyle\rho=\alpha\sqrt{(\xi^{2}-1)(1-\eta^{2})}\,,\qquad
z=\alpha\xi\eta\,.$ (6.3)

These new coordinates take the range $1\leq\xi<\infty$ and $-1\leq\eta\leq 1$.
The two black holes are then located at $(\xi,\eta)=(1,-1)$ and
$(\xi,\eta)=(1,1)$, respectively. They divide the $z$-axis into three parts:
the inner part between the black holes is given by $\xi=1$, while the two
outer parts that extend to infinity are given by $\eta=\pm 1$. Asymptotic
infinity itself is reached when $\xi\rightarrow\infty$ while keeping $\eta$
fixed.

It can be checked that, in prolate spheroidal coordinates, the four-
dimensional metric (4.6a) is given by

$\displaystyle\text{d}s_{(4)}^{2}$
$\displaystyle=-\frac{\alpha^{2}(\xi^{2}-\eta^{2})^{3}}{(H_{+}H_{-})^{\frac{1}{2}}}\left(\text{d}t+\omega_{\varphi}\,\text{d}\varphi\right)^{2}$
(6.4)
$\displaystyle\quad+\frac{(H_{+}H_{-})^{\frac{1}{2}}}{(\xi^{2}-\eta^{2})^{2}}\,\bigg{\\{}\frac{\text{d}\xi^{2}}{\xi^{2}-1}+\frac{\text{d}\eta^{2}}{1-\eta^{2}}+\frac{(\xi^{2}-1)(1-\eta^{2})\,\text{d}\varphi^{2}}{\xi^{2}-\eta^{2}}\bigg{\\}}\,,$
(6.5)

where

$\displaystyle\omega_{\varphi}$
$\displaystyle\equiv{\frac{2({\xi}^{2}-1)(1-\eta^{2})\left[(\xi-\eta)^{3}J_{1}+(\xi+\eta)^{3}J_{2}\right]}{\alpha({\xi}^{2}-\eta^{2})^{3}}}\,,$
(6.6a) $\displaystyle H_{\pm}$
$\displaystyle\equiv({\xi}^{2}-\eta^{2})\left[\alpha({\xi}^{2}-\eta^{2})+(\xi-\eta)M_{1}+(\xi+\eta)M_{2}\right]^{2}$
(6.6b) $\displaystyle\quad\pm
2\left[(\xi-\eta)^{3}(1+\xi\eta)J_{1}-(\xi+\eta)^{3}(1-\xi\eta)J_{2}\right].$
(6.6c)

The gauge fields (4.6b) and dilaton field (4.6c) are given by

$\displaystyle A_{0}$
$\displaystyle=\frac{\sqrt{2}}{H_{-}}\Big{\\{}-({\xi}^{2}-\eta^{2})\left[(\xi-\eta)M_{1}+(\xi+\eta)M_{2}\right]$
(6.7a) $\displaystyle\hskip
43.36243pt\times\left[\alpha({\xi}^{2}-\eta^{2})+(\xi-\eta)M_{1}+(\xi+\eta)M_{2}\right]$
(6.7b) $\displaystyle\hskip
43.36243pt+2\left[(\xi-\eta)^{3}(1+\xi\eta)J_{1}-(\xi+\eta)^{3}(1-\xi\eta)J_{2}\right]\Big{\\}}\,,$
(6.7c) $\displaystyle A_{\varphi}$
$\displaystyle=\frac{\sqrt{2}}{H_{-}}\Big{\\{}-\left[(\xi-\eta)(1+\xi\eta)M_{1}-(\xi+\eta)(1-\xi\eta)M_{2}\right]$
(6.7d) $\displaystyle\hskip
43.36243pt\times\left[\alpha({\xi}^{2}-\eta^{2})+(\xi-\eta)M_{1}+(\xi+\eta)M_{2}\right]^{2}$
(6.7e) $\displaystyle\hskip
43.36243pt+2(\xi-\eta)^{2}\big{[}({\xi}^{2}-\eta^{2})M_{1}+({\xi}^{2}-2+\eta^{2})M_{2}\big{]}J_{1}$
(6.7f) $\displaystyle\hskip
43.36243pt+2(\xi+\eta)^{2}\big{[}({\xi}^{2}-2+\eta^{2})M_{1}+({\xi}^{2}-\eta^{2})M_{2}\big{]}J_{2}$
(6.7g) $\displaystyle\hskip
43.36243pt+2\alpha({\xi}^{2}-1)(1-\eta^{2})\left[(\xi-\eta)^{3}J_{1}+(\xi+\eta)^{3}J_{2}\right]\Big{\\}}\,,$
(6.7h) $\displaystyle\phi$
$\displaystyle=\frac{\sqrt{3}}{2}\ln\left(\frac{H_{+}}{H_{-}}\right).$ (6.7i)

The advantage of using these coordinates is that the square-root functions
$R_{1}$ and $R_{2}$ have become algebraic functions of $\xi$ and $\eta$. This
would make the solution more convenient to study than in the original
coordinates.

##  7 Conclusion

In this paper, we have presented a solution of Kaluza–Klein theory describing
an arbitrary superposition of extremally charged, rotating black holes. Each
black hole carries equal electric and magnetic charge, and has an angular
momentum that is allowed to lie in a certain range. The spin vectors of the
black holes are parallel or anti-parallel, in the sense that they point in the
same or opposite direction.

This solution is specified by two harmonic functions on a three-dimensional
flat base space, which have poles at the locations of the black holes. By
choosing the harmonic functions appropriately, we can obtain interesting
special cases of this solution. We have considered one special case in this
paper, when the two black holes are placed along the $z$-axis, so that the
solution has a rotational symmetry. An even more interesting example would be
if the two black holes are not placed along the $z$-axis, but say along the
$x$-axis. Such a solution will not have any spatial symmetry, and so will be
considerably more complicated than the previous example.

The fact that the black holes in our solution are in static equilibrium, means
that there is an exact cancellation of the forces between them. When the black
holes are non-rotating, this cancellation of forces is well understood in the
limit of large separation: the electrostatic and magnetostatic repulsion
between them balances out their Newtonian gravitational attraction. But when
the black holes are rotating, they each acquire electric and magnetic dipole
moments, thus complicating the interactions between them. Besides the spin-
spin and dipole-dipole interactions (familiar from the Israel–Wilson–Perjés
solution [27]), there are also dipole-monopole interactions to consider.
Moreover, there will be interactions arising from the dilaton field. It would
be interesting to understand how the various forces balance out in this case.

One can also consider possible generalisations of the solution found in this
paper. For simplicity, we have only considered the case of equal electric and
magnetic charges. It should be possible to extend the solution to the more
general case of unequal electric and magnetic charges, with the ratio between
them the same for each black hole. A more intriguing question is whether the
condition of parallel or anti-parallel black hole spins can be relaxed. This
would require one to consider a more general form for the harmonic function
$g$ than in (4.1), and find the corresponding set of solutions to (4.2). We
leave these interesting questions for future work.

## Acknowledgements

ET wishes to thank Brenda Chng, for her collaboration at the early stages of
this work. He also wishes to thank Yu Chen and Kenneth Hong for helpful
discussions.

## References

  * [1] W. Israel and K. A. Khan, “Collinear particles and Bondi dipoles in general relativity,” Nuovo Cim. 33 (1964) 331 [doi:10.1007/BF02750196].
  * [2] S. D. Majumdar, ‘‘A class of exact solutions of Einstein’s field equations,’’ Phys. Rev. 72 (1947) 390 [doi:10.1103/PhysRev.72.390].
  * [3] A. Papapetrou, ‘‘A static solution of the equations of the gravitational field for an arbitrary charge distribution,’’ Proc. Roy. Irish Acad. A 51 (1947) 191.
  * [4] W. Israel and G. A. Wilson, ‘‘A class of stationary electromagnetic vacuum fields,’’ J. Math. Phys. 13 (1972) 865 [doi:10.1063/1.1666066].
  * [5] Z. Perjés, ‘‘Solutions of the coupled Einstein--Maxwell equations representing the fields of spinning sources,’’ Phys. Rev. Lett. 27 (1971) 1668 [doi:10.1103/PhysRevLett.27.1668].
  * [6] T. Kaluza, ‘‘Zum Unitätsproblem der Physik,’’ Sitzungsber. Preuss. Akad. Wiss. Phys. Math. K1 (1921) 966, reprinted in Int. J. Mod. Phys. D 27 (2018) 1870001 [doi:10.1142/S0218271818700017].
  * [7] O. Klein, ‘‘Quantentheorie und fünfdimensionale Relativitätstheorie,’’ Z. Phys. 37 (1926) 895 [doi:10.1007/BF01397481].
  * [8] H. Leutwyler, ‘‘La solution statique à symétrie sphérique en théorie pentadimensionnelle,’’ Arch. Sci. Genève 13 (1960) 549.
  * [9] P. Dobiasch and D. Maison, ‘‘Stationary, spherically symmetric solutions of Jordan’s unified theory of gravity and electromagnetism,’’ Gen. Rel. Grav. 14 (1982) 231 [doi:10.1007/BF00756059].
  * [10] A. Chodos and S. Detweiler, ‘‘Spherically symmetric solutions in five-dimensional general relativity,’’ Gen. Rel. Grav. 14 (1982) 879 [doi:10.1007/BF00756803].
  * [11] D. Pollard, ‘‘Antigravity and classical solutions of five-dimensional Kaluza--Klein theory,’’ J. Phys. A: Math. Gen. 16 (1983) 565 [doi:10.1088/0305-4470/16/3/015].
  * [12] G. W. Gibbons and D. L. Wiltshire, ‘‘Black holes in Kaluza--Klein theory,’’ Annals Phys. 167 (1986) 201, erratum ibid. 176 (1987) 393 [doi:10.1016/S0003-4916(86)80012-4].
  * [13] D. Rasheed, ‘‘The rotating dyonic black holes of Kaluza--Klein theory,’’ Nucl. Phys. B 454 (1995) 379 [doi:10.1016/0550-3213(95)00396-A,arXiv:hep-th/9505038].
  * [14] F. Larsen, ‘‘Rotating Kaluza--Klein black holes,’’ Nucl. Phys. B 575 (2000) 211 [doi:10.1016/S0550-3213(00)00064-X,arXiv:hep-th/9909102].
  * [15] F. Larsen, ‘‘Kaluza--Klein black holes in string theory,’’ in Proceedings of the 7th International Symposium on Particles, Strings and Cosmology (PASCOS 99) [doi:10.1142/9789812792433_0006,arXiv:hep-th/0002166].
  * [16] T. Matos and C. Mora, ‘‘Stationary dilatons with arbitrary electromagnetic field,’’ Class. Quant. Grav. 14 (1997) 2331 [doi:10.1088/0264-9381/14/8/027,arXiv:hep-th/9610013].
  * [17] G. Clément, ‘‘Solutions of five-dimensional general relativity without spatial symmetry,’’ Gen. Rel. Grav. 18 (1986) 861 [doi:10.1007/BF00770206].
  * [18] G. Clément, ‘‘Rotating Kaluza--Klein monopoles and dyons,’’ Phys. Lett. A 118 (1986) 11 [doi:10.1016/0375-9601(86)90524-4].
  * [19] F. Denef, ‘‘Supergravity flows and D-brane stability,’’ JHEP 08 (2000) 050 [doi:10.1088/1126-6708/2000/08/050, arXiv:hep-th/0005049].
  * [20] F. Denef, ‘‘On the correspondence between D-branes and stationary supergravity solutions of type II Calabi--Yau compactifications,’’ in Workshop on Strings, Duality and Geometry, CRM Montreal, March 2000 [doi:10.1090/amsip/033,arXiv:hep-th/0010222].
  * [21] B. Bates and F. Denef, ‘‘Exact solutions for supersymmetric stationary black hole composites,’’ JHEP 11 (2011) 127 [doi:10.1007/JHEP11(2011)127, arXiv:hep-th/0304094].
  * [22] D. Maison, ‘‘Ehlers--Harrison-type transformations for Jordan’s extended theory of gravitation,’’ Gen. Rel. Grav. 10 (1979) 717 [doi:10.1007/BF00756907].
  * [23] R. Emparan and A. Maccarrone, ‘‘Statistical description of rotating Kaluza--Klein black holes,’’ Phys. Rev. D 75 (2007) 084006 [doi:10.1103/PhysRevD.75.084006, arXiv:hep-th/0701150].
  * [24] T. Azeyanagi, N. Ogawa and S. Terashima, ‘‘Holographic duals of Kaluza--Klein black holes,’’ JHEP 04 (2009) 061 [doi:10.1088/1126-6708/2009/04/061, arXiv:0811.4177 [hep-th]].
  * [25] K. Matsuno, H. Ishihara, M. Kimura and T. Tatsuoka, ‘‘Kaluza--Klein vacuum multi-black holes in five dimensions,’’ Phys. Rev. D 86 (2012) 044036 [doi:10.1103/PhysRevD.86.044036,arXiv:1206.4818 [hep-th]].
  * [26] J. B. Hartle and S. W. Hawking, ‘‘Solutions of the Einstein--Maxwell equations with many black holes,’’ Commun. Math. Phys. 26 (1972) 87 [doi:10.1007/BF01645696].
  * [27] D. Kastor and J. H. Traschen, ‘‘BPS force balances via spin-spin interactions,’’ Class. Quant. Grav. 16 (1999) 1265 [doi:10.1088/0264-9381/16/4/014,arXiv:hep-th/9811088].


Stable finite difference methods for Kirchhoff-Love plates on
overlapping grids

ul]Longfei Licor1RCSThanks

ucla]Hangjie Ji

lanl]Qi Tang

[ul]Department of Mathematics, University of Louisiana at Lafayette, Lafayette, LA  70504, USA.
[ucla]Department of Mathematics, University of California Los Angeles, Los Angeles, CA 90095, USA.
[lanl]Los Alamos National Laboratory, Los Alamos, NM 87545, USA.
[cor1]Corresponding author.

[RCSThanks]Research supported by the  Louisiana Board of Regents Support Fund under contract No. LEQSF(2018-21)-RD-A-23.