11institutetext:  TU-Wien, Austria
11email<EMAIL_ADDRESS>22institutetext: LIPN, CNRS UMR 7030,
Université Sorbonne Paris Nord, France
22email<EMAIL_ADDRESS>
33institutetext: Computer Science Department UCL, UK
33email<EMAIL_ADDRESS>
# Reasoning About Group Polarization:
From Semantic Games to Sequent Systems

Robert Freiman Research supported by FWF project P 18563.11 Carlos Olarte The
work of Olarte has been partially supported by the SGR project PROMUEVA (BPIN
2021000100160) under the supervision of Minciencias (Ministerio de Ciencia
Tecnología e Innovación, Colombia). Olarte acknowledge also support from the
NATO Science for Peace and Security Programme through grant number G6133
(project SymSafe). 22 Elaine Pimentel Pimentel has received funding from the
European Union’s Horizon 2020 research and innovation programme under the
Marie Skłodowska-Curie grant agreement Number 101007627.33 Christian G.
Fermüller 11

###### Abstract

Group polarization, the phenomenon where individuals become more extreme after
interacting, has been gaining attention, especially with the rise of social
media shaping people’s opinions. Recent interest has emerged in formal
reasoning about group polarization using logical systems. In this work we
consider the modal logic PNL that captures the notion of agents agreeing or
disagreeing on a given topic. Our contribution involves enhancing PNL with
advanced formal reasoning techniques, instead of relying on axiomatic systems
for analyzing group polarization. To achieve this, we introduce a semantic
game tailored for (hybrid) extensions of PNL. This game fosters dynamic
reasoning about concrete network models, aligning with our goal of
strengthening PNL’s effectiveness in studying group polarization. We show how
this semantic game leads to a provability game by systemically exploring the
truth in all models. This leads to the first cut-free sequent systems for some
variants of PNL. Using polarization of formulas, the proposed calculi can be
modularly adapted to consider different frame properties of the underlying
model.

##  0.1 Introduction

Group polarization – where the opinions or beliefs of individuals within a
group become more extreme or polarized after interacting with each other – is
rapidly gaining attraction, especially with the advent of social media
platforms that have played a key role in the polarization of social,
political, and democratic processes. This phenomenon is mainly studied in
psychology [22, 16] and political philosophy [29, 30]. More recently,
logicians have taken up the challenge of formal reasoning about social
networks and changes in agents’s beliefs. Take for instance the Facebook logic
[27] (an epistemic logic endowed with a symmetric “friendship” relation); the
Tweeting logic [34] (formalizing announcements in a network); the logic for
reasoning about social belief and change propagation [18], etc.

We focus on the modal logic PNL [33], which refers to Kripke frames with two
types of disjoint and symmetric reachability relations. The individuals in a
social network are identified with worlds of the frame, and they are related
either as “friends” (positive) or as “enemies” (negative), but not both at the
same time. These relationships can be understood in different ways: Instead of
genuine friendship or enduring enmity, they may simply signify agreement or
disagreement on a particular issue. Unlike the aforementioned logics, PNL was
designed to reason about positive and negative relations among agents, a key
aspect for defining and measuring polarization [4]. In fact, polarization can
actually be studied in a neutral, network theory framework. Under the
framework of balance theory, it is possible to investigate the essential
conditions required for network stability in a fully polarized social network.
For instance, the _local balance_ condition that prohibits triangles of nodes
with two positive and one negative connection can be associated with the
formation of clusters of pairwise positively connected nodes that are
negatively connected to all nodes outside the cluster (see Example 1).

We take inspiration from a work by Pedersen, Smets, and Ågnotes [26], where
PNL is extended in various ways to axiomatically characterize modally
undefinable frame properties, including the disjointness of the two relations
and collective connectedness. The main challenge is the axiomatization of the
balance property, which requires extensions of PNL with nominals, dynamic and
hybrid operators.

Our approach to logical reasoning about group polarization is also based on
PNL but focuses on a different aspect of formal reasoning about the
corresponding models via games and proof systems. Games are a powerful tool to
bridge the gap between intended and formal semantics, often offering a
conceptually more natural approach to logic than the common paradigm of model-
theoretic semantics. In semantic games [15], every instance of the game is
played over a formula $\phi$ and a model $\mathbb{M}$ by two players, usually
called _I_ (or _Me_) and _You_. At each point in the game, one of the players
acts as the proponent ($\mathbf{P}$), while the other acts as the opponent
($\mathbf{O}$) of the current formula. The set of actions at each stage is
dictated by the main connective of the current formula. In contrast to
semantic games, provability games [19] do not refer to truth in a particular
model but to logical validity. The game is also played by two players, _Me_
and _You_ , and consists of attacking assertions of formulas made by the other
player and defending against these attacks. In this work, we will introduce
both a semantic game and a provability game for (hybrid) extensions of PNL.

We start by proposing a semantic game that characterizes the truth in a given
network model. This provides an alternative to the standard definition of an
evaluation function which supports a dynamic form of reasoning about concrete
network models (Section 0.2). We move on by arguing that effective formal
reasoning with the relevant logics requires more than (just) Hilbert-style
axiom systems. Rather, the automated search for proofs calls for Gentzen-style
systems that respect (a restricted form of) the subformula property. In proof-
theoretic terms, we are looking for a cut-free sequent system. Hence, our next
step is to turn the semantic game over single models into a provability game
(Section 0.3), characterizing logical validity. To this end, we define
disjunctive states for a game that is not restricted to a single model, but
systematically explores the truth in all models. This method leads to the
first Gentzen-style systems for variants of PNL (Section 0.4), which modularly
adapts to different frame properties by faithfully capturing the rules for
_elementary_ games.

Models of social learning and opinion dynamics aim to understand the role of
certain social factors in the acceptance/rejection of opinions. They can be
useful to explain alternative scenarios, such as consensus or polarization. In
this context, the positive and negative relationships are not permanent.
Instead, they can vary over time when _enemies_ reconcile, new _friendships_
/agreements emerge, or some actors begin to disagree with others. In Section
0.5, we show how the global adding and local link change modalities of [26]
(inspired by sabotage modal logic [2, 3, 31]) can be defined in our framework.
As a plus, we present in [12] a prototypical implementation of the proposed
games using rewriting logic and Maude [21, 6].

##  0.2 A Game Semantics for PNL

In this section, we revisit the positive and negative relations logic [33, 26]
with nominals (PNL) and its standard Kripke semantics, proposing a novel
semantic game for PNL that we prove to be adequate. Paving the way for the
provability game introduced in Section 0.3, we also propose an alternative
presentation of PNL that internalizes the nominals.

###  0.2.1 Kripke semantics for PNL

Let $\mathsf{A}=\\{\mathsf{a},\mathsf{b},\ldots\\}$ be a non-empty set of
agents, $\mathsf{At}=\\{p,q,\ldots\\}$ be a countable set of propositional
variables, and $N=\\{i,j,\ldots\\}$ be a countable set of _nominals_. The
language of PNL is generated by the following grammar:

$\phi::=p\mid R^{+}(i,j)\mid
R^{-}(i,j)\mid\neg\phi\mid\phi\wedge\phi\mid\phi\vee\phi\mid\meddiamondplus\phi\mid\meddiamondminus\phi\mid[A]\phi$

where $p\in\mathsf{At}$, and $i,j\in N$. The propositional connectives $\top$,
$\bot$, $\to$, and the (dual) modalities $\boxplus$ and $\boxminus$ can be
obtained in the usual way.

Formulas of the form $p$, $R^{+}(i,j)$, or $R^{-}(i,j)$ are called
_elementary_. The proposition $R^{+}(i,j)$ states that $i$ is a _friend_ of
(or, more generally, _agrees_ with) $j$, and proposition $R^{-}(i,j)$ states
that agent $i$ is an _enemy_ of (or _disagrees_ with) $j$. The formula
$\meddiamondplus\phi$ (resp. $\meddiamondminus\phi$) states that $\phi$ holds
for a friend (resp. an enemy). The global modality $[A]\phi$ states that
$\phi$ holds for all the agents. We use $R^{\pm}$ to denote either $R^{+}$ or
$R^{-}$, and $\Diamond^{\pm}$ to denote either or .

A model $\mathbb{M}$ is a tuple
$\langle\mathsf{A},\mathsf{R}^{+},\mathsf{R}^{-},\mathsf{V},\mathsf{g}\rangle$
where $\mathsf{A}$ is a set (of agents), $\mathsf{g}:N\rightarrow\mathsf{A}$
is called _denotation function_ ,
$\mathsf{R}^{+},\mathsf{R}^{-}\subseteq\mathsf{A}\times\mathsf{A}$, and
$\mathsf{V}:\mathsf{At}\rightarrow\mathcal{P}(\mathsf{A})$. A model is a PNL-
model if $\mathsf{R}^{+}$ is reflexive, and $\mathsf{R}^{+}$ and
$\mathsf{R}^{-}$ are both symmetric and non-overlapping, i.e., for all
$\mathsf{a},\mathsf{b}\in\mathsf{A}$,
$(\mathsf{a},\mathsf{b})\notin\mathsf{R}^{+}$ or
$(\mathsf{a},\mathsf{b})\notin\mathsf{R}^{-}$. We say that a model
$\mathbb{M}$ is _collectively connected_ , or a cc-PNL-model, if,
additionally, for all $\mathsf{a},\mathsf{b}\in\mathsf{A}$,
$(\mathsf{a},\mathsf{b})\in\mathsf{R}^{+}$ or
$(\mathsf{a},\mathsf{b})\in\mathsf{R}^{-}$. The class of all PNL models (cc-
PNL-models) is denoted by $\mathfrak{M}_{\textit{PNL}}$
($\mathfrak{M}_{\textit{ccPNL}}$).

$\small\qquad\begin{array}[]{lll l lll}\mathbb{M},\mathsf{a}\Vdash p&\text{
iff }\mathsf{a}\in\mathsf{V}(p)&&\mathbb{M},\mathsf{a}\Vdash\neg\phi&\text{
iff }\mathbb{M},\mathsf{a}\not\Vdash\phi\\\ \mathbb{M},\mathsf{a}\Vdash
R^{+}(i,j)&\text{ iff
}(\mathsf{g}(i),\mathsf{g}(j))\in\mathsf{R}^{+}&&\mathbb{M},\mathsf{a}\Vdash
R^{-}(i,j)&\text{ iff }(\mathsf{g}(i),\mathsf{g}(j))\in\mathsf{R}^{-}\\\
\mathbb{M},\mathsf{a}\Vdash\phi\wedge\psi&\text{ iff
}\mathbb{M},\mathsf{a}\Vdash\phi\text{ and
}\mathbb{M},\mathsf{a}\Vdash\psi&&\mathbb{M},\mathsf{a}\Vdash\phi\vee\psi&\text{
iff }\mathbb{M},\mathsf{a}\Vdash\phi\text{ or
}\mathbb{M},\mathsf{a}\Vdash\psi\\\
\mathbb{M},\mathsf{a}\Vdash\meddiamondplus\phi&\lx@intercol\text{ iff there is
}\mathsf{b}\in\mathsf{A}\text{ such that
}(\mathsf{a},\mathsf{b})\in\mathsf{R}^{+}\text{ and
}\mathbb{M},\mathsf{b}\Vdash\phi\hfil\lx@intercol\\\
\mathbb{M},\mathsf{a}\Vdash\meddiamondminus\phi&\lx@intercol\text{ iff there
is }\mathsf{b}\in\mathsf{A}\text{ such that
}(\mathsf{a},\mathsf{b})\in\mathsf{R}^{-}\text{ and
}\mathbb{M},\mathsf{b}\Vdash\phi\hfil\lx@intercol\\\
\mathbb{M},\mathsf{a}\Vdash[A]\phi&\lx@intercol\text{ iff
}\mathbb{M},\mathsf{b}\Vdash\phi\text{ for all
}\mathsf{b}\in\mathsf{A}\hfil\lx@intercol\end{array}$

Figure 1: Kripke semantics for PNL [26].

The Kripke semantics of PNL is in Figure 1. A formula $\phi$ is true over
$\mathbb{M}$, written $\mathbb{M}\Vdash\phi$ iff
$\mathbb{M},\mathsf{a}\Vdash\phi$, for all agent $\mathsf{a}\in\mathsf{A}$.
For a set of formulas $\Phi$, we write $\mathbb{M}\models\Phi$ iff
$\mathbb{M}\Vdash\Phi$ for all $\phi\in\Phi$. A formula $\phi$ is ((cc-)PNL-)
valid iff $\mathbb{M}\Vdash\phi$ for every ((cc-)PNL)-model $\mathbb{M}$. For
a class of models $\mathfrak{M}$, we write $\Phi\models_{\mathfrak{M}}\phi$
iff $\mathbb{M}\Vdash\phi$ for every model $\mathbb{M}\in\mathfrak{M}$ with
$\mathbb{M}\models\Phi$.

A model is called _named_ if its denotation function is surjective, i.e.,
every agent has a name. Let $\mathfrak{M}_{\textit{N}}$ be the class of named
models. The following result is immediate.

######  Lemma 1.

Let $\Phi\cup\\{\phi\\}$ be a finite set of formulas. Then
$\Phi\Vdash_{\mathfrak{M}_{\textit{PNL}}}\phi\iff\Phi\Vdash_{\mathfrak{M}_{\textit{PNL}}\cap\mathfrak{M}_{\textit{N}}}\phi$
and
$\Phi\Vdash_{\mathfrak{M}_{\textit{ccPNL}}}\phi\iff\Phi\Vdash_{\mathfrak{M}_{\textit{ccPNL}}\cap\mathfrak{M}_{\textit{N}}}\phi$.

Using this lemma, we give an alternative presentation of the semantics where
we explicitly test, using elementary formulas, the existence of
$R^{\pm}$-successors. Let $\mathsf{a}=\mathsf{g}(i)$. Then, we define:

$\begin{array}[]{lll}\mathbb{M},\mathsf{a}\Vdash\Diamond^{\pm}\phi&\text{ iff
there is }j\in N\text{ such that }\mathbb{M},\mathsf{g}(j)\Vdash
R^{\pm}(i,j)\text{ and }\mathbb{M},\mathsf{g}(j)\Vdash\phi\\\
\mathbb{M},\mathsf{a}\Vdash[A]\phi&\text{ iff
}\mathbb{M},\mathsf{g}(j)\Vdash\phi,\text{ for all }j\in N,\end{array}$

######  Remark 1.

At a later point, we need the following observation: if $\mathsf{g}$ is
surjective, even if restricted to $N^{\prime}\subseteq N$, then $N$ in the
above truth conditions can equivalently be replaced by $N^{\prime}$.

###  0.2.2 Semantic Game

The proposed _semantic game_ is played over a PNL-model
$\mathbb{M}=(\mathsf{A},\mathsf{R}^{+},\mathsf{R}^{-},\mathsf{V},\mathsf{g})$
by two players, _Me_ and _You_ , who argue about the truth of a formula $\phi$
at an agent $\mathsf{a}$. At each stage of the game, one player acts as
_proponent_ , while the other acts as _opponent_ of the claim that $\phi$ is
true at $\mathsf{a}$. We represent the situation where _I_ am the proponent
(and _You_ are the opponent) by the _game state_ $\mathbf{P},\mathsf{a}:\phi$,
and the situation where _I_ am the opponent (and _You_ are the proponent) by
$\mathbf{O},\mathsf{a}:\phi$. We call a game state _elementary_ if its
involved formula is elementary. For a game state $g$, we denote the game
starting at $g$ over the model $\mathbb{M}$ by $\mathbf{G}_{\mathbb{M}}(g)$.

The game proceeds by reducing the involved formula $\phi$ to an elementary
formula. The following rules of the game describe the possible choices of the
players depending on the current game state, when playing a game over the
model $\mathbb{M}$.

######  Definition 1.

Let $\mathbb{M}$ be a PNL-model. The semantic game is defined by the rules in
Figure 2.

$(\mathbf{P}_{\wedge})$

At $\mathbf{P},\mathsf{a}:\phi_{1}\wedge\phi_{2}$, _You_ choose between
$\mathbf{P},\mathsf{a}:\phi_{1}$ and $\mathbf{P},\mathsf{a}:\phi_{2}$ to
continue the game.

$(\mathbf{O}_{\wedge})$

At $\mathbf{O},\mathsf{a}:\phi_{1}\wedge\phi_{2}$, _I_ choose between
$\mathbf{O},\mathsf{a}:\phi_{1}$ and $\mathbf{O},\mathsf{a}:\phi_{2}$ to
continue the game.

$(\mathbf{P}_{\vee})$

At $\mathbf{P},\mathsf{a}:\phi_{1}\vee\phi_{2}$, _I_ choose between
$\mathbf{P},\mathsf{a}:\phi_{1}$ and $\mathbf{P},\mathsf{a}:\phi_{2}$ to
continue the game

$(\mathbf{O}_{\vee})$

At $\mathbf{O},\mathsf{a}:\phi_{1}\vee\phi_{2}$, _You_ choose between
$\mathbf{O},\mathsf{a}:\phi_{1}$ and $\mathbf{O},\mathsf{a}:\phi_{2}$ to
continue the game.

$(\mathbf{P}_{\neg})$

At $\mathbf{P},\mathsf{a}:\neg\phi$, the game continues with
$\mathbf{O},\mathsf{a}:\phi$.

$(\mathbf{O}_{\neg})$

At $\mathbf{O},\mathsf{a}:\neg\phi$, the game continues with
$\mathbf{P},\mathsf{a}:\phi$.

$(\mathbf{P}_{\Diamond^{\pm}})$

At $\mathbf{P},\mathsf{a}:\Diamond^{\pm}\phi$, _You_ win if there are no
$\mathsf{R}^{\pm}$-successors of $\mathsf{a}$. Otherwise, _I_ choose an
$\mathsf{R}^{\pm}$-successor $\mathsf{b}$ and the game continues with
$\mathbf{P},\mathsf{b}:\phi$.

$(\mathbf{O}_{\Diamond^{\pm}})$

At $\mathbf{O},\mathsf{a}:\Diamond^{\pm}\phi$, _I_ win if there are no
$\mathsf{R}^{\pm}$-successors of $\mathsf{a}$. Otherwise, _You_ choose an
$\mathsf{R}^{\pm}$-successor $\mathsf{b}$ and the game continues with
$\mathbf{O},\mathsf{b}:\phi$.

$(\mathbf{P}_{[A]})$

At $\mathbf{P},\mathsf{a}:[A]\phi$, _You_ choose an agent $\mathsf{b}$ and the
game continues with $\mathbf{P},\mathsf{b}:\phi$.

$(\mathbf{O}_{[A]})$

At $\mathbf{O},\mathsf{a}:[A]\phi$, _I_ choose an agent $\mathsf{b}$ and the
game continues with $\mathbf{O},\mathsf{b}:\phi$.

$(\mathbf{P}_{el})$

Let $\phi_{e}$ be an elementary formula. _I_ win and _You_ lose at
$\mathbf{P},\mathsf{a}:\phi_{e}$ iff
$~{}\mathbb{M},\mathsf{a}\models\phi_{e}$. Otherwise, _You_ win and _I_ lose.

$(\mathbf{O}_{el})$

At $\mathbf{O},\mathsf{a}:\phi_{e}$, _I_ win and _You_ lose iff
$\mathbb{M},\mathsf{a}\not\models\phi_{e}$. Otherwise, _You_ win and _I_ lose.

Figure 2: Semantic game given a PNL-model $\mathbb{M}$.

In general, every two-person, zero-sum, win-lose game is usually represented
by a _game tree_ , i.e., a labeled tree whose nodes are game states. In our
case, the root of the game tree representing the game
$\mathbf{G}_{\mathbb{M}}(g)$ is $g$. The children of each node in the game
tree are exactly the possible choices of the corresponding player. For
instance, if $h=\mathbf{P},\mathsf{a}:\phi_{1}\wedge\phi_{2}$ appears in the
game tree, then its children are $\mathbf{P},\mathsf{a}:\phi_{1}$ and
$\mathbf{P},\mathsf{a}:\phi_{2}$. Each node in the tree is labeled either “I”,
or “Y”, depending on which player is to move in the corresponding game state,
and we label the nodes $\mathbf{P},\mathsf{a}:\neg\phi$ and
$\mathbf{O},\mathsf{a}:\neg\phi$ with “I” (even though there is no choice
involved in these game states). For instance, the node corresponding to the
game state $h$ above is “Y”, since it is _Your_ choice in
$\mathbf{P}:\phi_{1}\wedge\phi_{2}$. The leaves of the tree receive the label
of the winning player. A _run_ of the game is a maximal path through the game
tree.

######  Example 1.

Let $\mathbf{(4B)}=((\meddiamondplus\meddiamondplus
p\vee\meddiamondminus\meddiamondminus p)\to\meddiamondplus
p)\wedge((\meddiamondplus\meddiamondminus p\vee\meddiamondminus\meddiamondplus
p)\to\meddiamondminus p)$. This formulas specifies _local balance_ [26] and
captures the idea that “the enemy of my enemy is my friend”, “the friend of my
enemy is my enemy”, and “the friend of my friend is my friend”. A collectively
connected network where $[A]4B$ holds is a polarized network, where agents can
be divided into two opposing groups [14]. Notions such a weak-balance [5] can
be also formalized in PNL [26]. I have a winning strategy for the game
$\mathbf{P},\mathsf{a}:4B$ on $\mathbb{M}_{1}$ while You have a winning
strategy for the same game on $\mathbb{M}_{2}$ where (omitting self-loops for
$\mathsf{R}^{+}$):

$\mathbb{M}_{1}=$ |  |  |  $\mathbb{M}_{2}=$ |
---|---|---|---|---

For $\mathbb{M}_{1}$, in the first conjunct, _I_ pick ($\mathbf{P}_{\vee}$)
$\meddiamondplus p$ and then $\mathsf{b}$ in ($\mathbf{P}$); for the second
conjunct, _I_ pick the first disjunction in
$F=(\meddiamondplus\meddiamondminus p\vee\meddiamondminus\meddiamondplus
p)\to\meddiamondminus p)$ where, in any of _Your_ choices ($\mathbf{P}_{\neg}$
followed by $\mathbf{O}_{\vee}$ and $\mathbf{O}_{\Diamond^{\pm}}$), _I_ win
all the elementary states. For $\mathbb{M}_{2}$, _I_ do not have a winning
strategy for the second conjunct: _I_ can neither win $\meddiamondminus p$ (no
$\mathsf{R}^{-}$ successor), nor the first disjunct in $F$ above since, after
$\mathbf{P}_{\neg}$, _You_ choose ($\mathbf{O}_{\vee}$)
$\meddiamondplus\meddiamondminus p$ and select $\mathsf{c}$ and then
$\mathsf{b}$ ($\mathbf{O}_{\Diamond^{\pm}}$) where $p$ holds and _You_ win.
See the complete game in our tool [12].

The following proposition follows from the fact that every rule in the game
decomposes the involved formula in subformulas.

######  Proposition 1.

For all models $\mathbb{M}$ and game states $g$, the game tree of
$\mathbf{G}_{\mathbb{M}}(g)$ is of finite height.

An immediate consequence of this fact is that every semantic game
$\mathbf{G}_{\mathbb{M}}(g)$ is _determined_ , i.e., exactly one of the two
players has a winning strategy.

###  0.2.3 Strategies and adequacy

Now we are ready to define winning strategies and prove the main result of
this section: the adequacy of the proposed game semantics with respect to the
Kripke semantics for PNL.

######  Definition 2.

A _strategy_ for _Me_ in the game $\mathbf{G}_{\mathbb{M}}(g)$ is a subtree
$\sigma$ of the associated game tree such that: (1) $g\in\sigma$, (2) if
$h\in\sigma$ is a node labeled “Y”, then all children of $h$ are in $\sigma$,
(3) if $h\in\sigma$ is a node labeled “I”, then exactly one child of $h$ is in
$\sigma$. The strategy $\sigma$ is called _winning_ if all leaves in the tree
$\sigma$ are labeled “I”. (Winning) strategies for _You_ are defined dually.

Note that every combination of strategies from _Me_ and _You_ defines a unique
run of the game. Alternatively, we can define a strategy $\sigma$ for _Me_ to
be winning iff the run resulting from $\sigma$ and a strategy for _You_ ends
in a winning game state for _Me_.

We can now show the adequacy of the semantic game, i.e., that the existence of
winning strategies for Me in a game and truth in a model coincide (proof in
Appendix .7).

######  Theorem 1.

Let $\mathbb{M}$ be a PNL-model, $\mathsf{a}$ an agent, and $\phi$ a formula.

(1) _I_ have a winning strategy for
$\mathbf{G}_{\mathbb{M}}(\mathbf{P},\mathsf{a}:\phi)$ iff
$\mathbb{M},\mathsf{a}\models\phi$.

(2) _You_ have a winning strategy for
$\mathbf{G}_{\mathbb{M}}(\mathbf{P},\mathsf{a}:\phi)$ iff
$\mathbb{M},\mathsf{a}\not\models\phi$.

#### Internalizing nominals.

Remember that in a named model $\mathbb{M}$, every agent $\mathsf{a}$ has a
name $i$, i.e. there exists $i\in N$ s.t. $\mathsf{g}(i)=\mathsf{a}$.
Therefore, for $\mathbf{Q}\in\\{\mathbf{P},\mathbf{O}\\}$, it is unambiguous
if we write $\mathbf{Q},i:\phi$ for the game state
$\mathbf{Q},\mathsf{a}:\phi$. The fact that $\mathbb{M}\models R^{\pm}(i,j)$
iff $(\mathsf{g}(i),\mathsf{g}(j))\in\mathsf{R}^{\pm}$ gives us the following
equivalent formulations of the rules for , and $[A]$111The outcome of the game
state $\mathbf{Q},k:R^{\pm}(i,j)$ is independent of $k$ (it only depends on
the underlying model $\mathbb{M}$). Hence, we write
$\mathbf{Q},\\_:R^{\pm}(i,j)$ instead of $\mathbf{Q},k:R^{\pm}(i,j)$.:

$(\mathbf{P}_{\Diamond^{\pm}})$

At $\mathbf{P},i:\Diamond^{\pm}\phi$, _I_ choose a nominal $j$, and _You_
decide whether the game ends in the state $\mathbf{P},\\_:R^{\pm}(i,j)$ or
continues with $\mathbf{P},j:\phi$.

$(\mathbf{O}_{\Diamond^{\pm}})$

At $\mathbf{O},i:\Diamond^{\pm}\phi$, _You_ choose $j$, and _I_ choose between
$\mathbf{O},\\_:R^{\pm}(i,j)$ and $\mathbf{O},j:\phi$.

$(\mathbf{P}_{[A]})$

At $\mathbf{P},i:[A]\phi$, _You_ choose a nominal $j$ and the game continues
with $\mathbf{P},j:\phi$.

$(\mathbf{O}_{[A]})$

At $\mathbf{O},i:[A]\phi$, _I_ choose a nominal $j$, and the game continues
with $\mathbf{O},j:\phi$.

Following Remark 1, we can restrict branching over a subset $N^{\prime}$ of
nominals if $g$’s restriction to $N^{\prime}$ is surjective. For future
reference, let us formulate this observation precisely. We denote the game
over $\mathbb{M}$ starting at the game state $g$, where branching is over
$N^{\prime}\subseteq N$ by $\mathbf{G}^{N^{\prime}}_{\mathbb{M}}(g)$. We call
a model $N^{\prime}$-named if $\mathsf{g}:N^{\prime}\rightarrow\mathsf{A}$ is
surjective. We say that two games $\mathbf{G}_{1}$ and $\mathbf{G}_{2}$ are
_strategically equivalent_ , notation $\mathbf{G}_{1}\cong\mathbf{G}_{2}$, iff
_I_ have a winning strategy in both games or in none of the two. We have the
following:

######  Proposition 2.

Let $\mathbb{M}$ be $N^{\prime}$-named, let $g=\mathbf{Q},\mathsf{a}:\phi$ for
some $\mathbf{Q}\in\\{\mathbf{P},\mathbf{O}\\}$, some agent $\mathsf{a}$ and
formula $\phi$, and let $\mathsf{a}=\mathsf{g}(i)$. Then
$\mathbf{G}_{\mathbb{M}}(\mathbf{Q},\mathsf{a}:\phi)\cong\mathbf{G}^{N^{\prime}}_{\mathbb{M}}(\mathbf{Q},i:\phi)$.

##  0.3 The Disjunctive Game

In this section, we lift the semantic game to two different _disjunctive
games_ , one for PNL-validity and one for cc-PNL-validity, which differ only
in their respective winning conditions. We prove that the obtained games are
adequate and can thus be regarded as _provability games_ for their
corresponding logics. The main crucial fact is that the rules of the semantic
game are independent of the underlying model, except for elementary game
states. Using this fact, and identifying certain conditions on winning
strategies, this disjunctive game will be the foundation for the sequent
calculi proposed in Section 0.4.

###  0.3.1 Playing on all models

The disjunctive game $\mathbf{DG}(\mathbf{P},i:\phi)$ can be thought of as
_Me_ and _You_ playing all semantic games $\mathbf{G}(\mathbf{P},i:\phi)$ over
all PNL-models $\mathbb{M}$ simultaneously. We point out that the rules of the
semantic game do not depend on the structure of $\mathbb{M}$ but merely on
$\phi$. Truth degrees are only needed at the atomic level to determine who
wins the particular run of the game. This allows us to require players to play
“blindly”, i.e., without explicitly referencing a model $\mathbb{M}$. Clearly,
if _I_ have a winning strategy in such a game, then _I_ can win in
$\mathbf{G}_{\mathbb{M}}(\mathbf{P},i:\phi)$, for every $\mathbb{M}$, making
this strategy an adequate witness of logical validity.

Defining such a validity game is not straightforward, since the simplest case
of disjunction is already problematic. Let us consider the game
$\mathbf{P},i:p\vee\neg p$. Clearly, _I_ have a winning strategy in the
semantic game over every model. However, there is no uniform way of making a
good choice in the first turn: No matter whether _I_ choose $\mathbf{P},i:p$
or $\mathbf{P},i:\neg p$, there are still models where _You_ win the game
eventually. To compensate for this, we allow _Myself_ to create “backup
copies” and _duplicate_ game states. Formally, disjunctive game states are
finite multisets of the game states defined in Section 0.2.2. We prefer to
write $g_{1}\bigvee...\bigvee g_{n}$ for the disjunctive game state
$\\{g_{1},...,g_{n}\\}$, but keep the convenient notation $g\in D$ if $g$ is
in the multiset $D$. We write $D_{1}\bigvee D_{2}$ for the multiset sum
$D_{1}+D_{2}$ and $D\bigvee g$ for $D+\\{g\\}$. A disjunctive state is called
_elementary_ if all its game states are elementary. We use $\mathbf{DG}(D)$ to
denote the disjunctive game starting at $D$, and we define the cc-disjunctive
game $\mathbf{DG}^{\textbf{cc}}(D)$ which is played over all cc-PNL-models. It
differs from $\mathbf{DG}(D)$ only in its winning conditions (see below).

In our running example, _I_ duplicate the game state in the first round and
the game continues with the _disjunctive state_ $\mathbf{P},i:p\vee\neg
p\bigvee\mathbf{P},i:p\vee\neg p$. Now _I_ move to $\mathbf{P},i:p$ in the
first subgame and to $\mathbf{P},i:\neg p$ in the second. After a role switch
in the second subgame, the final state is
$\mathbf{P},i:p\bigvee\mathbf{O},i:p$, where _I_ win regardless of the
underlying model.

The following _winning condition_ reflects the fact that _My_ strategy for the
disjunctive game $\mathbf{DG}(\mathbf{P},i:p\vee\neg p)$ was successful.

######  Definition 3.

Let $D^{el}$ denote the disjunctive state consisting of the elementary game
states of $D$. _I_ win and _You_ lose at $D$ if for every PNL-model there is a
game state in $D^{el}$ where _I_ win the corresponding semantic game. In the
cc-disjunctive game, _I_ win and _You_ lose if for every cc-PNL-model there is
a game state in $D^{el}$ where _I_ win the corresponding semantic game.

In the disjunctive game, _I_ additionally take the role of a _scheduler_ ,
deciding which game is to be played next. We signal the chosen game state by
underlining it as in $\underline{g}$.

(Dupl)

If no state in $D$ is underlined, _I_ can choose a non-elementary $g\in D$ and
the game continues with $D\bigvee g$.

(Sched)

If no state in $D=D^{\prime}\bigvee g$ is underlined, and $g$ is non-
elementary, _I_ can choose to continue the game with
$D^{\prime}\bigvee\underline{g}$.

(Move)

If $D=D^{\prime}\bigvee\underline{g}$ then the player who is to move in the
semantic game $\mathbf{G}(g)$ at $g$ makes a legal move to the game state
$g^{\prime}$ and the game continues with $D^{\prime}\bigvee g^{\prime}$.222For
example, if $g$ is $\mathbf{P},i:\phi_{1}\wedge\phi_{2}$, then _You_ choose a
$k\in\\{1,2\\}$ and the game continues with
$D^{\prime}\bigvee\mathbf{P},i:\phi_{k}$.

(End)

The game ends if there are no non-elementary game states left in $D$, or if no
game state is underlined and _I_ win according to Definition 3. Otherwise, _I_
must move according to (Dupl) or (Sched).

Figure 3: Rules for the disjunctive game.

######  Definition 4 (Disjunctive game).

The rules of the disjunctive game are in Figure 3. Infinite runs, and runs
that end in elementary disjunctive states where _I_ do not win according to
Definition 3, are winning for _You_ and losing for _Me_. (Dupl) is referred to
as the _duplication rule_ and (Sched) as the _scheduling_ , or _underlining
rule_.

It follows from the Gale-Stewart Theorem [13] that every disjunctive game
$\mathbf{DG}(D)$ and every cc-disjunctive game $\mathbf{DG}^{\textbf{cc}}(D)$
is determined.

###  0.3.2 Adequacy and best strategies

Now we state the main result of this section, whose proof is split into two
propositions: The left-to-right direction in Proposition 3 and the right-to-
left direction in Proposition 4 below.

######  Theorem 2.

_I_ have a winning strategy in $\mathbf{DG}(D)$ (in
$\mathbf{DG}^{\textbf{cc}}(D)$) iff for every (cc-) PNL-model $\mathbb{M}$,
there is some $g\in D$ such that _I_ have a winning strategy in
$\mathbf{G}_{\mathbb{M}}(g)$.

######  Corollary 1.

The formula $\phi$ is (cc-) PNL-valid iff _I_ have a winning strategy in
$\mathbf{DG}(\mathbf{P},i:[A]\phi)$ (in
$\mathbf{DG}^{\textbf{cc}}(\mathbf{P},i:[A]\phi)$).

######  Proposition 3.

Let $\mathbb{M}$ be a (cc-) PNL-model. If _I_ have a winning strategy in
$\mathbf{DG}(D)$ (in $(\mathbf{DG}^{\textbf{cc}}(D)$), then there is some
$g\in D$ such that _I_ have a winning strategy in
$\mathbf{G}_{\mathbb{M}}(g)$.

Proof: Let $\sigma$ be _My_ winning strategy in $\mathbf{DG}(D)$. We show the
following claim by bottom-up tree induction on $\sigma$: For every
$H\in\sigma$ there is some $g\in H$ and a winning strategy $\sigma_{H}$ for
_Me_ in $\mathbf{G}_{\mathbb{M}}(g)$. The case for the root, $H=D$, gives the
desired result.

If $H$ is a leaf, then, since $\sigma$ is winning, there is an elementary
$h\in H$ such that _I_ win the semantic game at $h$ over $\mathbb{M}$. In this
case, $\sigma_{H}$ consists of the single leaf $h$.

If _You_ move in $H$, then it must be of the form
$H^{\prime}\bigvee\underline{h}$, where $h$ is labeled “Y” in the semantic
game. By definition of strategy, all successors of $H$ must be in $\sigma$,
and they are of the form $H^{\prime}\bigvee h^{\prime}$, where $h^{\prime}$
ranges over all possible game states immediately after _Your_ choice at $h$.
By inductive hypothesis, for every $h^{\prime}$, $\sigma_{H^{\prime}\bigvee
h^{\prime}}$ is a winning strategy for some $g\in H^{\prime}\bigvee
h^{\prime}$. If for some $h^{\prime}$, $\sigma_{H^{\prime}\bigvee h^{\prime}}$
is a winning strategy for some $g\in H^{\prime}$, then we can set
$\sigma_{H}=\sigma_{H^{\prime}\bigvee h^{\prime}}$. Otherwise, all
$\sigma_{H^{\prime}\bigvee h^{\prime}}$ is a winning strategy for
$h^{\prime}$. Hence, we can connect the roots of all these trees to the new
common root $h$ to obtain a winning strategy for _Me_ in
$\mathbf{G}_{\mathbb{M}}(h)$.

If _I_ move in $H$ according to the rules (Dupl) or (Sched), then the
resulting disjunctive state is still $H$ (except maybe some game state could
be underlined or duplicated). Hence, the claim follows from the inductive
hypothesis. If _I_ move in $H$ according to (Move), then
$H=H^{\prime}\bigvee\underline{h}$, and the unique child of $H$ in $\sigma$ is
$H^{\prime}\bigvee h^{\prime}$, where $h^{\prime}$ is a possible game state
after _My_ move in the semantic game at $h$. By the inductive hypothesis,
$\sigma_{H^{\prime}\bigvee h^{\prime}}$ is a winning strategy for _Me_ in
$\mathbf{G}_{M}(g)$, for some $g\in H^{\prime}\bigvee h^{\prime}$. If $g\in
H^{\prime}$, we proceed as above. If $g=h^{\prime}$, then we can append the
root of $\sigma_{H^{\prime}\bigvee h^{\prime}}$ to $h$ to obtain a winning
strategy for _Me_ in $\mathbf{G}_{\mathbb{M}}(h)$. $\blacksquare$

#### My best way to play.

We will now describe a strategy $\sigma$ for _Me_ for the game
$\mathbf{DG}(D_{0})$. This strategy is – in a way – the optimal way to play
the disjunctive game. Intuitively $\sigma$ exploits all of _My_ possible
choices without sacrificing _My_ winning chances. Consequently, $\sigma$ is
winning iff _I_ can win the game at all. (This claim follows from Proposition
3 by classical reasoning).

Let us fix an enumeration of pairs $(g,h)$ of game states of the semantic game
such that every pair appears in this enumeration infinitely often. Let us
denote by $\\#(g,h)$ the number of the pair $(g,h)$ under this enumeration.
Throughout the game, let us keep track of the number of execution steps $n$ of
$\sigma$. At $D_{0}$, $n=0$. The strategy $\sigma$ is as follows:

  1. (C1)

If in the current disjunctive state $D$, $D^{el}$ is winning, _I_ end the
game.

  2. (C2)

Otherwise, let $n=\\#(g,h)$. If $D=D^{\prime}\bigvee g$, according to the
label of $g$ we have:
(a) “Y” (otherwise, skip), then underline $g$ and _You_ make _Your_ move.
(b) “I” and $h$ is a child of $g$ in the evaluation game (otherwise, skip),
then duplicate $g$, schedule a copy of $g$, and go to $h$ in that copy, i.e.,
the new disjunctive state is $D^{\prime}\bigvee g\bigvee h$.

  3. (C3)

Increase $n$ by 1 and go to (C1).

In words, until the game reaches a winning state, _My_ strategy is to play in
a way such that _I_ always duplicate a state, and then play by exhausting all
possible moves in that state.

Let $\pi$ be the run of the game $\mathbf{DG}(D_{0})$ resulting from _You_
playing according to _Your_ winning strategy and _Me_ playing _My_ best way
$\sigma$. We say that a game state $g$ _appears along_ $\pi$, and write
$g\in\pi$, if it occurs in a disjunctive state in $\pi$. We say that $g$
_disappears_ , if $g\in\pi_{n}$ and for some $m>n$, $g\notin\pi_{m}$. The
following holds (proof in Appendix .7).

######  Lemma 2.

Let $\pi$ be as above. Then:
1) Let $g\in\pi$ be a non-elementary game state labelled “Y” in the semantic
game. Then at least one successor of $g$ appears along $\pi$.
2) Let $g\in\pi$ be a non-elementary game state labeled “I” in the semantic
game. Then all successors of $g$ appear along $\pi$.

We can now show that $\pi$ gives rise to a model $\mathbb{M}_{\pi}$ with the
property that _You_ have a winning strategy for every $g$ appearing along
$\pi$.

######  Definition 5.

Let $\mathcal{E}$ be a set of elementary game states. Let
$\mathbb{M}_{\mathcal{E}}$ be the following named model: \- Agents
$\mathsf{A}$: an agent $\mathsf{a}_{i}$ for each nominal $i$ appearing in
$\mathcal{E}$;

\- Accessibility relations: $\mathsf{R}^{-}_{\mathcal{E}}$ is the least
symmetric relation such that
$\mathsf{a}_{i}\mathsf{R}_{\mathcal{E}}^{-}\mathsf{a}_{j}$ whenever (i)+
$\mathbf{O},\\_:R^{-}(i,j)$ is in $\mathcal{E}$.
$\mathsf{R}^{+}_{\mathcal{E}}$ is the least reflexive symmetric relation such
that (i)- $\mathsf{a}_{i}\mathsf{R}_{\mathcal{E}}^{+}\mathsf{a}_{j}$ whenever
$\mathbf{O},\\_:R^{+}(i,j)$ is in $\mathcal{E}$;

\- Valuation function $\mathsf{V}_{\mathcal{E}}$:
$\mathsf{a}_{i}\in\mathsf{V}_{\mathcal{E}}(p)$ iff the state $\mathbf{O},i:p$
is in $\mathcal{E}$;

\- Assignment $\mathsf{g}_{\mathcal{E}}$:
$\mathsf{g}_{\mathcal{E}}(i)=\mathsf{a}_{i}$.

The model $\mathbb{M}_{\mathcal{E}}^{\textbf{cc}}$ is as
$\mathbb{M}_{\mathcal{E}}$, except $\mathsf{R}^{+}$ also has (ii)+
$\mathsf{a}_{i}\mathsf{R}^{+}\mathsf{a}_{j}$ if
$\mathbf{P},\\_:R^{-}(i,j)\in\mathcal{E}$ or if (iii)+ no
$\mathbf{Q},\\_:R^{\pm}(i,j)$ for $\mathbf{Q}\in\\{\mathbf{P},\mathbf{O}\\}$
is in $\mathcal{E}$, and is closed under reflexivity and symmetry, and
$\mathsf{R}^{-}$ also has (ii)- $\mathsf{a}_{i}R^{-}\mathsf{a}_{j}$ if
$\mathbf{P},\\_:R^{+}(i,j)\in\mathcal{E}$ and is closed under symmetry.

The degree $\delta(\phi)$ of a formula $\phi$ to be 0 if $\phi$ is elementary,
$\delta(\phi_{1}\mathop{\medstar}\nolimits\phi_{2})=\max\\{\delta(\phi_{1}),\delta(\phi_{2})\\}+1$
for a binary and $\delta(\triangle\psi)=\delta(\psi)+1$ for $\triangle$ a
unary operator. We extend $\delta$ to game states by setting
$\delta(\mathbf{Q},i:\phi)=\delta(\phi)$ for
$\mathbf{Q}\in\\{\mathbf{P},\mathbf{O}\\}$.

######  Lemma 3.

Let $\mathbb{M}_{\pi}$ be the model $\mathbb{M}_{\mathcal{E}}$
$(\mathbb{M}_{\mathcal{E}}^{\textbf{cc}}$) from the above definition, where
$\mathcal{E}$ is the set of all elementary game states appearing along $\pi$.
This model is a (cc-) PNL model. Furthermore, if $g$ appears along $\pi$, then
_You_ have a winning strategy for $\mathbf{G}_{\mathbb{M}_{\pi}}(g)$.

Proof: To prove that $\mathbb{M}_{\mathcal{E}}$ is a PNL-model it remains to
show that it is non-overlapping. Towards a contradiction, assume that
$(\mathsf{a}_{i},\mathsf{a}_{j})\in\mathsf{R}_{\pi}^{+}\cap\mathsf{R}_{\pi}^{-}$.
By definition, both $\mathbf{O},\\_:R^{+}(i,j)$ and
$\mathbf{O},\\_:R^{-}(i,j)$ appear333Since the relations are symmetric, we can
identify $R^{\pm}(i,j)$ with $R^{\pm}(j,i)$. along $\pi$. Since the elementary
states of $\pi$ are accumulative, there is a disjunctive state $D$ in $\pi$
containing both of these states. But then _I_ could have won the game in $D$,
since in every PNL-model at least one of $R^{+}(i,j)$ and $R^{-}(i,j)$ must be
false. This is a contradiction to the assumption that $\pi$ results from _You_
playing _Your_ winning strategy.

We show that $\mathbb{M}_{\mathcal{E}}^{\textbf{cc}}$ is a cc-PNL-model.
First, we note that this model is collectively connected, since, $(iii)^{+}$
(see Definition 5) is equivalent to
$\neg((i)^{+}\vee(ii)^{+}\vee(i)^{-}\vee(ii)^{-})$. Also, the model remains
non-overlapping. Suppose, we had
$(\mathsf{a}_{i},\mathsf{a}_{j})\in\mathsf{R}^{+}\cap\mathsf{R}^{-}$.
According to the definition of $\mathsf{R}^{+}$ and $\mathsf{R}^{-}$ all
possible scenarios how this could happen lead to contradiction:

\- (1) $(i)^{+}$ and $(i)^{-}$: At some point, both states appear in a
disjunctive state in $D$. But _I_ would have won the game at $D$, since there
is no non-overlapping model where both $R^{+}(i,j)$ and $R^{-}(i,j)$ are true.

\- (2) $(i)^{+}$ and $(ii)^{-}$: _I_ win the game in a disjunctive state,
where both $\mathbf{O},\\_:R^{+}(i,j),\mathbf{P},\\_:R^{+}(i,j)\in\mathcal{E}$
states occur.

\- (3) $(ii)^{-}$ and $(i)^{-}$: Similar to the case above.

\- (4) $(ii)^{-}$ and $(ii)^{-}$: _I_ would have won in a state containing
$\mathbf{P},\\_:R^{+}(i,j)$ and $\mathbf{P},\\_:R^{-}(i,j)$, since there is no
collectively connected models where both $R^{+}(i,j)$ and $R^{-}(i,j)$ are
false.

\- (5) $(iii)^{+}$, excludes $(i)^{-}$ and $(ii)^{-}$, hence
$(\mathsf{a}_{i},\mathsf{a}_{j})\notin\mathsf{R}^{-}$.

We prove the second claim by induction on the degree of $g$. The elementary
cases where $g$ is of the form $\mathbf{O},i:\phi$ follow directly from the
definition of $\mathbb{M}_{\pi}$. Assume $g=\mathbf{P},i:p$ appears along
$\pi$, but $\mathbb{M}_{\pi},\mathsf{a}_{i}\Vdash p$. The latter implies that
$\mathbf{O},i:p$ appears along $\pi$. Reasoning as above, there is a
disjunctive state $D$ in $\pi$ containing both $\mathbf{P},i:p$ and
$\mathbf{O},i:p$, which means that $D$ would be winning for _Me_. The case for
$\mathbf{P},\\_:R^{\pm}(i,j)$ is similar.

For the inductive step, let $g\in\pi$ be non-elementary with the label “Y”. By
Lemma 2, some child $h$ of $g$ appears along $\pi$. By the inductive
hypothesis, there is a winning strategy $\mu_{h}$ for _You_ for
$\mathbf{G}_{\mathbb{M}_{\pi}}(h)$. Hence, appending the root of $\mu_{h}$ to
$g$ gives a winning strategy for _You_ in $\mu_{g}$ in
$\mathbf{G}_{\mathbb{M}_{\pi}}(g)$. If $g$ is non-elementary with label “I”,
then, by Lemma 2, all children $h$ of $g$ appear along $\pi$. For each $h$
there is a winning strategy for _You_ in $\mathbf{G}_{\mathbb{M}_{\pi}}(h)$.
Thus, appending the roots of all $\mu_{h}$ to the new common root $g$ gives a
winning strategy for _You_ in $\mathbf{G}_{\mathbb{M}_{\pi}}(g)$.
$\blacksquare$

######  Proposition 4.

Assume that for every model $\mathbb{M}$, there is some $g\in D$ such that _I_
have a winning strategy in $\mathbf{G}_{\mathbb{M}}(g)$. Then, _I_ have a
winning strategy in $\mathbf{DG}(D)$.

Proof: Suppose _I_ do not have a winning strategy in $\mathbf{DG}(D)$. By the
Gale-Stewart Theorem, _You_ have a winning strategy in this game. Let _Me_
play according to the strategy $\sigma$ from above, and let $\pi$ be the run
through $\mathbf{DG}(D)$ resulting from _You_ playing _Your_ winning strategy
and _Me_ playing $\sigma$. Let $\mathbb{M}_{\pi}$ be the model from Definition
5. By Lemma 2 and Lemma 3, _You_ have a winning strategy for
$\mathbf{G}_{\mathbb{M}_{\pi}}(g)$ for all $g\in D$. $\blacksquare$

##  0.4 From strategies to Proofs

Theorems 1 and 2 imply that winning strategies for _Me_ in the disjunctive
game correspond to validity. In this section, we will extend this result to
proof systems. This will be done by introducing a sequent calculus
$\mathbf{DS}$, where proofs correspond to _My_ winning strategies in the
disjunctive game. Before that, we will demonstrate that winning strategies can
be finitized.

###  0.4.1 _Your_ optimal choices

In this section, we show how to adapt the disjunctive game so that it becomes
finitely branching in “Y”-nodes. This will help us to conveniently formulate
the disjunctive game as a calculus. Infinite branching occurs only in the case
of the rules $\mathbf{P}_{[A]}$ and $\mathbf{O}_{\Diamond^{\pm}}$ where
branching is parametrized by the nominals. We will show that in these
situations, there is an optimal choice for _You_ , so _I_ can expect _You_ to
play according to this choice.

######  Proposition 5.

Let $j$ be a nominal different from $i$ not occurring in $D$ nor in $\phi$.
Then: (1) _You_ have a winning strategy in
$\mathbf{DG}(D\bigvee\mathbf{P},i:[A]\phi)$ iff _You_ have a winning strategy
in $\mathbf{DG}(D\bigvee\mathbf{P},j:\phi)$, and similarly for
$\mathbf{DG}^{\textbf{cc}}$.

(2) _You_ have a winning strategy in
$\mathbf{DG}(D\bigvee\mathbf{O},i:\Diamond^{\pm}\phi)$ iff _You_ have winning
strategies in both $\mathbf{DG}(D\bigvee\mathbf{P},\\_:R^{\pm}(i,j))$ and
$\mathbf{DG}(D\bigvee\mathbf{O},j:\phi)$, and similarly for
$\mathbf{DG}^{\textbf{cc}}$.

This result implies that _My_ winning strategies in the disjunctive game can
be finitely represented: in every disjunctive state whose children branch over
the nominals, it is enough to consider a single child only, given by a _fresh_
nominal $j$ not appearing in that disjunctive state. Intuitively, the proof of
Proposition 5 runs by transforming a winning strategy for _You_ in the
semantic game for all game states in $D\bigvee\mathbf{P},k:\phi$ (where $k$ is
arbitrary) over a model $\mathbb{M}$ into a winning strategy for _You_ for all
game states in $D\bigvee\mathbf{P},j:\phi$ over a modified model
$\mathbb{M}^{\prime}$, where $j$ is according to the proposition. By the
Theorems 1 and 2, this gives the desired result. The actual proof is carried
out in the appendix.

###  0.4.2 The proof system $\mathbf{DS}$

Now we detail how to formally transform (provability) games into (sequent)
proof systems.

Labeled nominal formulas are either _labeled formulas_ of the form $i:\phi$ or
_relational atoms_ of the form $R(i,j)$, where $i$ and $j$ are nominals and
$\phi$ is a PNL formula.444Observe that here we are abusing the notation,
identifying $k:R(i,j)$ with $R(i,j)$. Recall from Footnote 1 that the truth
value of these atoms depend only on the underlying model. _Labeled sequents_
have the form $\Gamma\Rightarrow\Delta$, where $\Gamma,\Delta$ are multisets
containing labeled nominal formulas.

Starting with sequents, every disjunctive state of the form

$\mathbf{O},i_{1}:\phi_{1}\bigvee\ldots\bigvee\mathbf{O},i_{n}:\phi_{n}\bigvee\mathbf{P},j_{1}:\psi_{1}\bigvee\ldots\bigvee\mathbf{P},j_{m}:\psi_{m}$

can be rewritten as the labeled sequent $\Gamma\Rightarrow\Delta$ where
$\Gamma=\\{i_{1}:\phi_{1},\ldots,i_{n}:\phi_{n}\\}\mbox{ and
}\Delta=\\{j_{1}:\psi_{i},\ldots,j_{m}:\psi_{m}\\}$. In what follows, we will
not distinguish between disjunctive states and their corresponding labeled
sequent. For example, the disjunctive game state
$\mathbf{O},i:(\meddiamondplus\meddiamondplus
p\vee\meddiamondminus\meddiamondminus p)\bigvee\mathbf{P},i:\meddiamondplus p$
will be identified with the sequent $i:(\meddiamondplus\meddiamondplus
p\vee\meddiamondminus\meddiamondminus p)\Rightarrow i:\meddiamondplus p$.

The inference rules must be tailored in such a way that proofs in the sequent
system match exactly _My_ winning strategies in the disjunctive game. This
means that the user of the proof system takes the role of _Me_ , scheduling
game states and choosing moves in _I_ -states. Moreover, provability in the
proof system should correspond to validity in the game. For that, it is
necessary to establish the formal relationship between elementary game states
and logical axioms.

######  Lemma 4.

Let $\Gamma\Rightarrow\Delta$ be composed of elementary game states only. _I_
win the disjunctive game in $\Gamma\Rightarrow\Delta$ iff one of the following
holds555Since relations are symmetric, we will identify $R^{\pm}(i,j)$ with
$R^{\pm}(j,i)$.

i. $R^{-}(i,i)\in\Gamma$ or $R^{+}(i,i)\in\Delta$ for some $i$;

ii. $\\{R^{+}(i,j),R^{-}(i,j)\\}\subseteq\Gamma$ for some $i\not=j$;

iii. $\Gamma\cap\Delta\not=\varnothing$.

In the case of collectively connected models, additionally,

iv. $\\{R^{+}(i,j),R^{-}(i,j)\\}\subseteq\Delta$ for some $i\not=j$.

Proof: By definition of the disjunctive game, it is immediate that _I_ win the
game if (iii) holds. Moreover, _I_ clearly win the game if either (i) or (ii)
hold, since only $R^{+}$ is reflexive and since the relations are non-
overlapping. Finally, if the model is collectively connected, _I_ clearly win
the game if (iv) holds.

Suppose that (i), (ii) and (iii) do not hold. Then _You_ have a winning
strategy in the model $\mathbb{M}_{\Gamma\Rightarrow\Delta}$ from Definition
5. If additionally (iv) does not hold, we choose the model
$\mathbb{M}_{\Gamma\Rightarrow\Delta}^{\textbf{cc}}$.

By proceeding as in Lemma 3, it is easy to see that $R^{+}$ is reflexive,
$R^{\pm}$ is symmetric, both models are non-overlapping and
$\mathbb{M}^{\textbf{cc}}_{\Gamma\Rightarrow\Delta}$ is collectively
connected. $\blacksquare$

Figure 4 presents the labeled sequent systems $\mathbf{DS}$ and
$\mathbf{DS}^{\textbf{cc}}$, with the standard initial axiom and
structural/propositional rules. The modal rules and the relational rules $sym$
and $ref\pm$ coincides with the modal rules originally presented by Viganò in
[32], adapted to multi-relational modal logics.

It is routine to show that the rules $no$ and $cc$ in Figure 4 correspond to
the non-overlapping and collectively connected axioms, respectively

$\forall i,j.\neg(R^{+}(i,j)\wedge R^{-}(i,j))\quad\mbox{and}\quad\forall
i,j.R^{+}(i,j)\vee R^{-}(i,j)$

The following result, proved in Appendix .7, entails a normal form on proofs
in $\mathbf{DS}$, since any proof-search procedure can be restricted so to
start with applications of logical rules followed by relational rules and the
initial axiom.

######  Lemma 5.

In a bottom-up reading of derivations, the relational rules permutes up w.r.t.
any other logical rule in $\mathbf{DS}/\mathbf{DS}^{\textbf{cc}}$. Moreover,
the weakening rules below are admissible in
$\mathbf{DS}/\mathbf{DS}^{\textbf{cc}}$.

$\Gamma,i:\phi\Rightarrow\Delta\Gamma\Rightarrow\Delta\qquad\Gamma\Rightarrow\Delta,i:\phi\Gamma\Rightarrow\Delta$

The following result immediately implies that the disjunctive game
$\mathbf{DG}$ is adequate with respect to the calculus $\mathbf{DS}$.

######  Theorem 3.

_I_ have a winning strategy in the disjunctive game
$\mathbf{DG}(\Gamma\Rightarrow\Delta)$ (in
$\mathbf{DG}^{\textbf{cc}}(\Gamma\Rightarrow\Delta)$) iff
$\Gamma\Rightarrow\Delta$ is provable in $\mathbf{DS}$ (in
$\mathbf{DS}^{\textbf{cc}}$).

Proof: The proof is by case analysis in the rules of the disjunctive game/last
rule applied in the proof, and it is based in the following correspondence:

\- (Dupl) Duplication in the game corresponds to left and right contraction
(Rules $R_{c}$, $L_{c}$).

\- (Sched) Scheduling game moves over non-elementary formulas corresponds to
choosing propositional or modal rules to be applied. Observe that Lemma 5
guarantees that propositional and modal rules in $\mathbf{DS}$ can always be
chosen before dealing with the elementary case.

\- (Move) Applying the rule chosen in (Sched) corresponds to applying the
respective sequent rule in $\mathbf{DS}$. Note that _I_ should be prepared to
any movement from _You_. Hence, branching in _Your_ possible moves corresponds
to branching in a sequent rule. On the other hand, infinite branching is
handled as explained in Section 0.4.1.

\- (End) Due to Lemma 4, winning states are completely captured by the axioms.
$\blacksquare$

Let us write $\models_{\textbf{PNL}}\Gamma\Rightarrow\Delta$ iff for every
PNL-model there is some $i:\gamma\in\Gamma$ such that
$\mathbb{M},\mathsf{g}(i)\not\vdash\gamma$, or there is some
$i:\delta\in\Delta$ such that $\mathbb{M},\mathsf{g}(i)\models\delta$.
Similarly, we define
$\models_{\textbf{cc}\textbf{PNL}}\Gamma\Rightarrow\Delta$. We have the
following consequence of Theorems 1, 2, and 3:

######  Corollary 2.

Let $\Gamma,\Delta$ be multisets of labeled formulas. Then
$\models_{\textbf{PNL}}\Gamma\Rightarrow\Delta$
($\models_{\textbf{cc}\textbf{PNL}}\Gamma\Rightarrow\Delta$) iff there is a
proof of $\Gamma\Rightarrow\Delta$ in $\mathbf{DS}$ (in
$\mathbf{DS}^{\textbf{cc}}$). In particular, $\phi$ is (cc-) PNL-valid iff
there is a proof of $\Rightarrow\phi$ in $\mathbf{DS}$ (in
$\mathbf{DS}^{\textbf{cc}}$).

Axiom and Structural Rules

$1[$$init$]Γ, i: ϕ_el ⇒Δ, i: ϕ_el Γ, i: ϕ, i: ϕ⇒Δ $1[$$(L_{c})$]Γ, i: ϕ⇒Δ Γ⇒i:
ϕ,i: ϕ,Δ $1[$$(R_{c})$]Γ⇒i: ϕ, Δ

Propositional Rules

Γ⇒i: ϕ, Δ $1[$$(L_{\neg})$]Γ, i: ¬ϕ⇒Δ Γ, i: ϕ⇒Δ $1[$$(R_{\neg})$]Γ⇒i: ¬ϕ, Δ

Γ, i: ϕ⇒Δ Γ, i: ψ⇒Δ $2[$$(L_{\vee})$]Γ, i: ϕ∨ψ⇒Δ Γ⇒i: ϕ, Δ
$1[$$(R_{\vee}^{1})$]Γ⇒i: ϕ∨ψ, Δ Γ⇒i: ψ, Δ $1[$$(R_{\vee}^{2})$]Γ⇒i: ϕ∨ψ, Δ

Γ, i: ϕ⇒Δ $1[$$(L_{\wedge}^{1})$]Γ, i: ϕ∧ψ⇒Δ Γ, i: ψ⇒Δ
$1[$$(L_{\wedge}^{2})$]Γ, i: ϕ∧ψ⇒Δ Γ⇒i: ϕ, Δ Γ⇒i: ψ, Δ $2[$$(R_{\wedge})$]Γ⇒i:
ϕ∧ψ, Δ

Modal Rules

Γ, R^±(i,j) ⇒Δ $1[$$(L_{\Diamond^{\pm}})_{1}$]Γ, i: ◇^±ϕ⇒Δ Γ, j:ϕ⇒Δ
$1[$$(L_{\Diamond^{\pm}})_{2}$]Γ, i: ◇^±ϕ⇒Δ

Γ⇒R^±(i,j), Δ Γ⇒j: ϕ, Δ $2[$$(R_{\Diamond^{\pm}})$]Γ⇒i: ◇^±ϕ,Δ Γ, j: ϕ⇒Δ
$1[$$(L_{[A]})$]Γ, i:[A]ϕ⇒Δ Γ⇒j: ϕ, Δ $1[$$(R_{[A]})$]Γ⇒i:[A]ϕ, Δ

Relational Rules

Γ⇒Δ, R^±(j,i) $1[$$sym$]Γ⇒Δ, R^±(i,j) $1[$$ref+$]Γ⇒Δ, R^+(i,i)

$1[$$ref-$]Γ, R^-(i,i)⇒Δ Γ⇒Δ, R^+(i,j) Γ⇒Δ, R^-(i,j) $2[$$no$]Γ⇒Δ

Collectively Connected (for $\mathbf{DS}^{\textbf{cc}}$)

$1[$$cc$]Γ⇒Δ, R^+(i,j), R^-(i,j)

Figure 4: The proof system $\mathbf{DS}$. In the rule init, $\phi_{el}$
denotes an elementary formula. In the rules $(L_{\Diamond^{\pm}})_{1}$,
$(L_{\Diamond^{\pm}})_{2}$, and $(R_{[A]})$, the nominal $j$ is fresh.The rule
$R$ has the proviso that $i\neq j$. The system $\mathbf{DS}^{\textbf{cc}}$
also includes the rule $cc$ for reasoning about collectively connected
systems.

The next examples shows how $\mathbf{DS}^{\textbf{cc}}$ elegantly captures
collectively connectedness.

######  Example 2 (Connectedness).

The formula $(\boxplus p\to[A]p)\vee(\boxminus p\to[A]p)$, characterizing
collective connectedness [26], has the following proof in
$\mathbf{DS}^{\textbf{cc}}$:

$\Rightarrow i:(\boxplus p\to[A]p)\vee(\boxminus p\to[A]p)\Rightarrow
i:[A]p,i:\meddiamondplus\neg p,i:\meddiamondminus\neg p\Rightarrow
j:p,i:\meddiamondplus\neg p,i:\meddiamondminus\neg
p\lx@proof@logical@and\Rightarrow j:p,i:\meddiamondminus\neg
p,R^{+}(i,j)\lx@proof@logical@and\Rightarrow
j:p,R^{+}(i,j),R^{-}(i,j)\Rightarrow j:p,j:\neg p,R^{+}(i,j)\Rightarrow
j:p,j:\neg p,i:\meddiamondminus\neg p$

Proving cut-admissibility of labeled systems can be cumbersome due to the
presence of relational rules. In [20], a systematic procedure for transforming
axioms into rules was presented, based on focusing and polarities [1]. This
procedure not only allows for generalizing different approaches for
transforming axioms into sequent rules present in the literature [28, 32, 23],
but it also provides a uniform way of proving cut-admissibility for the
resulting systems.

While it is out of the scope of this paper to introduce all this machinery
just to prove cut-admissibility of $\mathbf{DS}/\mathbf{DS}^{\textbf{cc}}$, we
note that it is possible to directly transform the semantic description of
(cc-)PNL into a labeled sequent system equivalent to
$\mathbf{DS}/\mathbf{DS}^{\textbf{cc}}$, by using the methodology in [20] and
adopting the negative polarity to atomic formulas. Hence the cut-admissibility
result for $\mathbf{DS}/\mathbf{DS}^{\textbf{cc}}$ is a particular instance of
the general result in [20].

######  Theorem 4.

The following cut rule is admissible in
$\mathbf{DS}/\mathbf{DS}^{\textbf{cc}}$

$\Gamma\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow\Delta,i:\phi
i:\phi,\Gamma\Rightarrow\Delta$

As a consequence, $\mathbf{DS}/\mathbf{DS}^{\textbf{cc}}$ are consistent,
since the only rules that can be applied in an empty sequent is $no$ and it is
routine to show that it does not trivialize derivations. Moreover, cut-
admissibility also serves as a tool for proving meta-theoretical properties:
$(\boxplus p\to[A]p)\vee(\boxminus p\to[A]p)$ in Example 2 is not provable in
$\mathbf{DS}$, that is, the rule $cc$ is necessary.

##  0.5 Dynamic operators and extensions

In this section we show how the global link-adding and local link change
modalities from [26] can be defined in our framework. Adding such modalities
requires the underlying model $\mathbb{M}$ to be part of the game state, and
calls for a different presentation of resulting sequent calculus.

The logic dPNL extends the syntax in Section 0.2 with the following cases:

$\phi::=\cdots\mid\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle\phi\mid\langle\operatorname*{\wedge\mkern-15.0mu\wedge}-\rangle\phi\mid\langle\operatorname*{\wedge\mkern-15.0mu\wedge}\pm\rangle\phi\mid\langle\oplus\rangle\phi\mid\langle\ominus\rangle\phi$

The global link-adding modalities,
$\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle\phi$ (resp.
$\langle\operatorname*{\wedge\mkern-15.0mu\wedge}-\rangle\phi$) is forced if,
after adding a positive (resp. negative) link _somewhere_ in the network,
$\phi$ holds. $\langle\operatorname*{\wedge\mkern-15.0mu\wedge}\pm\rangle$
adds either a positive or a negative link. The local change modality
$\langle\oplus\rangle\phi$ (resp. $\langle\ominus\rangle\phi$) holds at agent
$\mathsf{a}$ whenever $\phi$ holds after changing one of the $\mathsf{a}$’s
links from negative to positive (resp. from positive to negative).

In the following, if
$\mathbb{M}=\langle\mathsf{A},\mathsf{R}^{+},\mathsf{R}^{-},\mathsf{V},\mathsf{g}\rangle$,
we denote by with
$\mathbb{M}\cup\\{\mathsf{a}R_{\leftrightarrow}^{+}\mathsf{b}\\}$ the model
$\langle\mathsf{A},\mathsf{R}^{+}\cup\\{\mathsf{a}\mathsf{R}^{+}\mathsf{b},\mathsf{b}\mathsf{R}^{+}\mathsf{a}\\},\mathsf{R}^{-},\mathsf{V},\mathsf{g}\rangle$.
Similarly for
$\mathbb{M}\cup\\{\mathsf{a}R_{\leftrightarrow}^{-}\mathsf{b}\\}$. We denote
by $\mathbb{M}\setminus\\{\mathsf{a}R_{\leftrightarrow}^{+}\mathsf{b}\\}$ the
model where both $(\mathsf{a},\mathsf{b})$ and $(\mathsf{b},\mathsf{a})$ are
removed from $\mathsf{R}^{+}$. Similarly for
$\mathbb{M}\setminus\\{\mathsf{a}R_{\leftrightarrow}^{-}\mathsf{b}\\}$.

The semantics of the new operators is the following [26]:

$\small\begin{array}[]{lll}\mathbb{M},\mathsf{a}\Vdash\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle\phi&\text{
iff }\text{ there are }\mathsf{b},\mathsf{c}\in\mathsf{A}\text{ s.t.
}(\mathsf{b},\mathsf{c})\not\in\mathsf{R}^{-}\text{ and
}\mathbb{M}\cup\\{\mathsf{b}R_{\leftrightarrow}^{+}\mathsf{c}\\},\mathsf{a}\Vdash\phi\\\
\mathbb{M},\mathsf{a}\Vdash\langle\operatorname*{\wedge\mkern-15.0mu\wedge}-\rangle\phi&\text{
iff }\text{ there are }\mathsf{b},\mathsf{c}\in\mathsf{A}\text{ s.t.
}(\mathsf{b},\mathsf{c})\not\in\mathsf{R}^{+}\text{ and
}\mathbb{M}\cup\\{\mathsf{b}R_{\leftrightarrow}^{-}\mathsf{c}\\},\mathsf{a}\Vdash\phi\\\
\mathbb{M},\mathsf{a}\Vdash\langle\operatorname*{\wedge\mkern-15.0mu\wedge}\pm\rangle\phi&\text{
iff }\text{ there are }\mathsf{b},\mathsf{c}\in\mathsf{A}\text{ s.t.
}(\mathsf{b},\mathsf{c})\not\in\mathsf{R}^{-}\text{ and
}\mathbb{M}\cup\\{\mathsf{b}R_{\leftrightarrow}^{+}\mathsf{c}\\},\mathsf{a}\Vdash\phi\\\
&\text{ or there are }\mathsf{b},\mathsf{c}\in\mathsf{A}\text{ s.t.
}(\mathsf{b},\mathsf{c})\not\in\mathsf{R}^{+}\text{ and
}\mathbb{M}\cup\\{\mathsf{b}R_{\leftrightarrow}^{-}\mathsf{c}\\},\mathsf{a}\Vdash\phi\\\
\mathbb{M},\mathsf{a}\Vdash\langle\oplus\rangle\phi&\text{ iff }\text{ there
is }\mathsf{b}\in\mathsf{A}\text{ s.t.
}(\mathsf{a},\mathsf{b})\in\mathsf{R}^{-}\text{ and
}\mathbb{M}\cup\\{\mathsf{a}R_{\leftrightarrow}^{+}\mathsf{b}\\}\setminus\\{\mathsf{a}R_{\leftrightarrow}^{-}\mathsf{b}\\},\mathsf{a}\Vdash\phi\\\
\mathbb{M},\mathsf{a}\Vdash\langle\ominus\rangle\phi&\text{ iff }\text{ there
is }\mathsf{b}\in\mathsf{A}\text{ s.t.
}\mathsf{a}\neq\mathsf{b},(\mathsf{a},\mathsf{b})\in\mathsf{R}^{+}\text{ and
}\mathbb{M}\cup\\{\mathsf{a}R_{\leftrightarrow}^{-}\mathsf{b}\\}\setminus\\{\mathsf{a}R_{\leftrightarrow}^{+}\mathsf{b}\\},\mathsf{a}\Vdash\phi\\\
\end{array}$

We consider game states of the form $\mathbf{P},\mathbb{M},\mathsf{a}:\phi$
and $\mathbf{O},\mathbb{M},\mathsf{a}:\phi$, where the model $\mathbb{M}$ over
which the game is played is explicit. Figure 5 presents the rules for the
semantic game dPNL. Adequacy is given by the following result, which has a
similar proof to Theorem 1.

$(\mathbf{P}_{\langle\operatorname*{\wedge\mkern-15.0mu\wedge}-\rangle})$

At
$\mathbf{P},\mathbb{M},\mathsf{a}:\langle\operatorname*{\wedge\mkern-15.0mu\wedge}-\rangle\phi$,
_I_ choose $\mathsf{b},\mathsf{c}\in A$ s.t.
$(\mathsf{b},\mathsf{c})\not\in\mathsf{R}^{+}$ and the game continues with
$\mathbf{P},(\mathbb{M}\cup\\{\mathsf{b}R_{\leftrightarrow}^{-}\mathsf{c}\\}),\mathsf{a}:\phi$.
_You_ win if there are no such $\mathsf{b}$ and $\mathsf{c}$.

$(\mathbf{O}_{\langle\operatorname*{\wedge\mkern-15.0mu\wedge}-\rangle})$

At
$\mathbf{O},\mathbb{M},\mathsf{a}:\langle\operatorname*{\wedge\mkern-15.0mu\wedge}-\rangle\phi$,
_You_ choose $\mathsf{b},\mathsf{c}\in A$ s.t.
$(\mathsf{b},\mathsf{c})\not\in\mathsf{R}^{+}$ and the game continues with
$\mathbf{O},(\mathbb{M}\cup\\{\mathsf{b}R_{\leftrightarrow}^{-}\mathsf{c}\\}),\mathsf{a}:\phi$.
_I_ win if there are no such $\mathsf{b}$ and $\mathsf{c}$.

$(\mathbf{P}_{\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle})$

At
$\mathbf{P},\mathbb{M},\mathsf{a}:\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle\phi$,
_I_ choose $\mathsf{b},\mathsf{c}\in A$ s.t.
$(\mathsf{b},\mathsf{c})\not\in\mathsf{R}^{-}$ and the game continues with
$\mathbf{P},(\mathbb{M}\cup\\{\mathsf{b}R_{\leftrightarrow}^{+}\mathsf{c}\\}),\mathsf{a}:\phi$.

$(\mathbf{O}_{\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle})$

At
$\mathbf{O},\mathbb{M},\mathsf{a}:\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle\phi$,
_You_ choose $\mathsf{b},\mathsf{c}\in A$ s.t.
$(\mathsf{b},\mathsf{c})\not\in\mathsf{R}^{-}$ and the game continues with
$\mathbf{O},(\mathbb{M}\cup\\{\mathsf{b}R_{\leftrightarrow}^{+}\mathsf{c}\\}),\mathsf{a}:\phi$.

$(\mathbf{P}_{\langle\oplus\rangle})$

At $\mathbf{P},\mathbb{M},\mathsf{a}:\langle\oplus\rangle\phi$, _I_ choose
$\mathsf{b}\in A$ s.t. $(\mathsf{a},\mathsf{b})\in\mathsf{R}^{-}$ and the game
continues with
$\mathbf{P},(\mathbb{M}\cup\\{\mathsf{a}R_{\leftrightarrow}^{+}\mathsf{b}\\}\setminus\\{\mathsf{a}R_{\leftrightarrow}^{-}\mathsf{b}\\}),\mathsf{a}:\phi$.
_You_ win if there is no such a $\mathsf{b}$.

$(\mathbf{O}_{\langle\oplus\rangle})$

At $\mathbf{O},\mathbb{M},\mathsf{a}:\langle\oplus\rangle\phi$, _You_ choose
$\mathsf{b}\in A$ s.t. $(\mathsf{a},\mathsf{b})\in\mathsf{R}^{-}$ and the game
continues with
$\mathbf{O},(\mathbb{M}\cup\\{\mathsf{a}R_{\leftrightarrow}^{+}\mathsf{b}\\}\setminus\\{\mathsf{a}R_{\leftrightarrow}^{-}\mathsf{b}\\}),\mathsf{a}:\phi$.
_I_ win if there is no such a $\mathsf{b}$.

Figure 5: Rules for dPNL adding/changing modalities. The rules for
$\langle\operatorname*{\wedge\mkern-15.0mu\wedge}\pm\rangle$, and the rules
$\mathbf{P}_{\langle\ominus\rangle}$ and $\mathbf{O}_{\langle\ominus\rangle}$
are similar and omitted. The global addition modalities do not necessarily add
a _new_ link. In
$\mathbf{P}_{\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle}$, _I_
(and _You_ in
$\mathbf{O}_{\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle}$)
always have a choice, say $(\mathsf{a},\mathsf{a})\notin\mathsf{R}^{-}$.

######  Theorem 5.

Let $\mathbb{M}$ be a PNL-model, $\mathsf{a}$ an agent, and $\phi$ a dPNL
formula. Then: (1) _I_ have a winning strategy for
$\mathbf{G}_{\mathbb{M}}(\mathbf{P},\mathbb{M},\mathsf{a}:\phi)$ iff
$\mathbb{M},\mathsf{a}\models\phi$; and (2) _You_ have a winning strategy for
$\mathbf{G}_{\mathbb{M}}(\mathbf{P},\mathbb{M},\mathsf{a}:\phi)$ iff
$\mathbb{M},\mathsf{a}\not\models\phi$.

######  Example 3.

Let $\mathbb{M}_{2}$ be as in Example 1. _I_ have a winning strategy for the
game state $\mathbf{P},\mathbb{M}_{2},\mathsf{a}:\langle\ominus\rangle(4B)$:
_I_ just need to change the relation $\mathsf{a}\mathsf{R}^{+}\mathsf{c}$ to
obtain the model $\mathbb{M}_{1}$ (where _I_ have a winning strategy for
$4B$). _You_ do not have a winning strategy for
$\mathbf{O},\mathbb{M}_{2},\mathsf{a}:\langle\ominus\rangle\langle\ominus\rangle(4B)$
(and _I_ win
$\mathbf{P},\mathbb{M}_{2},\mathsf{a}:\neg(\langle\ominus\rangle\langle\ominus\rangle(4B))$).
In words, _You_ cannot enforce _balance_ by making $\mathsf{a}$ disagree with
her two friends. Finally, the formula $[A]\boxminus\bot$ characterizes
“reconciliation” in a network [26], where there are no disagreements between
agents. _I_ have a winning strategy in the game
$\mathbf{P},\mathbb{M}_{2},\mathsf{a}:\meddiamondplus\langle\oplus\rangle[A]\boxminus\bot$.
(See the outputs of the tool in Section .8 and [12]).

Defining a sequent system for dPNL would require passing through a provability
game $\mathbf{dDG}$ as done in Section 0.3. We skip this step since it is
similar to the case of PNL. Instead, we will go directly to the design of a
proof system, which turns out to be a non-trivial task.

The problem is that the new modalities update the relational values and
multisets contexts are not adequate for handling this linear behavior. Hence
relational atoms will be stored in a separate linear context, where
information can be updated. A relational context $\mathcal{R}$ is a _set_
containing only relational predicates, and a relational sequent has the form
$\mathcal{R};\Gamma\Rightarrow\Delta$, where $\Gamma,\Delta$ are multisets of
labeled formulas (hence no relational atoms).

The label sequent system $\mathbf{dDS}$ for dPNL is depicted in Figure 6. The
rules for the other connectives are obtained by adapting those in Figure 4
with relational contexts. Rule $L_{\Diamond^{\pm}}$ introduces the predicate
$R(i,j)$, for a fresh $j$, into the context $\mathcal{R}$. The proviso of the
rules for the global adding-link modalities guarantee non-overlapping, and the
rules for $\langle\oplus\rangle$ forbid adding into $\mathcal{R}$ the atom
$R^{-}(i,i)$. Moreover, the only way of adding new elements into $\mathcal{R}$
is using the rules $L_{\Diamond^{\pm}}$ and those for
$\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle$,
$\langle\operatorname*{\wedge\mkern-15.0mu\wedge}-\rangle$ and
$\langle\operatorname*{\wedge\mkern-15.0mu\wedge}\pm\rangle$. This explains
the additional hypothesis in the theorem below, which is proved in Appendix
.7.

R,R^+(i,j);Γ,k:ϕ⇒Δ $1[$$(L_{\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle})$]R;Γ,k:⟨∧∧+ ⟩ϕ⇒Δ |  R,R^+(i,j);Γ⇒Δ,k:ϕ $1[$$(R_{\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle})$]R;Γ⇒Δ,k:⟨∧∧+ ⟩ϕ |  R,R^-(i,j);Γ,k:ϕ⇒Δ $1[$$(L_{\langle\operatorname*{\wedge\mkern-15.0mu\wedge}-\rangle})$]R;Γ,k:⟨∧∧-⟩k:ϕ⇒Δ
---|---|---
R,R^-(i,j);Γ⇒Δ,k:ϕ $1[$$(R_{\langle\operatorname*{\wedge\mkern-15.0mu\wedge}-\rangle})$]R;Γ⇒Δ,k:⟨∧∧-⟩ϕ |  R,R^+(i,j);Γ,k:ϕ⇒Δ $1[$$(L_{\langle\oplus\rangle})$]R,R^-(i,j);Γ,k:⟨⊕⟩ϕ⇒Δ |  R,R^+(i,j);Γ⇒Δ,k:ϕ $1[$$(R_{\langle\oplus\rangle})$]R,R^-(i,j);Γ⇒Δ,k:⟨⊕⟩ϕ
R,R^-(i,j);Γ,k:ϕ⇒Δ $1[$$(L_{\langle\ominus\rangle})$]R,R^+(i,j);Γ,k:⟨⊖⟩ϕ⇒Δ |  R,R^-(i,j);Γ⇒Δ,k:ϕ $1[$$(R_{\langle\ominus\rangle})$]R,R^+(i,j);Γ⇒Δ,k:⟨⊖⟩ϕ |  R, R^±(i,j) ;Γ, j:ϕ⇒Δ $1[$$(L_{\Diamond^{\pm}})$]R;Γ, i: ◇^±ϕ⇒ Δ

Figure 6: System $\mathbf{dDS}$. Rules
$L/R_{\langle\operatorname*{\wedge\mkern-15.0mu\wedge}+\rangle}$ (resp.
$L/R_{\langle\operatorname*{\wedge\mkern-15.0mu\wedge}-\rangle}$) have the
proviso that $R^{-}(i,j)\not\in\mathcal{R}$ (resp.
$R^{+}(i,j)\not\in\mathcal{R}$), modulo symmetry (see Footnote 5). In rules
$L/R_{\langle\ominus\rangle}$, $i\neq j$. Rules for
$\langle\operatorname*{\wedge\mkern-15.0mu\wedge}\pm\rangle$ are similar and
omitted. In $L_{\Diamond^{\pm}}$, $j$ is fresh.

######  Theorem 6.

Let $\Gamma$ and $\Delta$ be multisets of dPNL formulas not containing
relational predicates. _I_ have a winning strategy in the disjunctive game
$\mathbf{dDG}(\Gamma\Rightarrow\Delta)$ iff $\Gamma\Rightarrow\Delta$ is
provable in $\mathbf{dDS}$.

##  0.6 Concluding Remarks

We have introduced two new techniques for PNL [26], with the aim of formally
reasoning about positive and negative relations among agents and group
polarization: a satisfiability game that allows for the verification of
properties within concrete networks of agents; and a validity game with the
corresponding cut-free sequent calculus. Our contributions offer promising
avenues for automated reasoning, as demonstrated by our prototypical tool
[12]. Furthermore, by showing that reasoning about frame properties of the
underlying model can be delayed until reaching elementary games/formulas, we
can modularly adapt to different relational properties.

Currently, we are exploring extensions that relax symmetry assumptions,
allowing for representing situations where agent $a$ may influence the opinion
of $b$ but not the other way around. Additionally, we are investigating the
concept of “budget” as in the game proposed in [17] to characterize scenarios
where proponents and opponents operate within a limited _political capital_ ,
where adding/changing relations can potentially decrease such a capital. To
this end, the preference of spending as little capital as possible could be
expressed in a combination of PNL with a suitable _choice logic_ , i.e., a
logic where preferences are definable at the object level. Semantic games for
choice logics have been investigated in [10] and the lifting of game-induced
choice logic, GCL, to a provability game and proof system was demonstrated in
[11]. Finally, following the techniques developed in [24] for analyzing
sequent systems in rewrite logic, we are extending our tool [12] to also
support the sequent calculi proposed here.

This work can be seen as a continuation of a program of lifting semantic games
to analytic calculi [7, 25]. Our approach is a refinement of previous work on
modal logic [8, 9] as it replaces model checking at the level of axioms with
explicit rules for the classes of PNL and cc-PNL models. We therefore provide
hand-tailored systems for reasoning about group polarization and opens up the
aforementioned routes to mechanization.

## References

  * [1] Jean-Marc Andreoli.  Logic programming with focusing proofs in linear logic.  J. Log. Comput., 2(3):297–347, 1992.
  * [2] Carlos Areces, Raul Fervari, and Guillaume Hoffmann.  Relation-changing modal operators.  Log. J. IGPL, 23(4):601–627, 2015.
  * [3] Guillaume Aucher, Johan van Benthem, and Davide Grossi.  Modal logics of sabotage revisited.  J. Log. Comput., 28(2):269–303, 2018.
  * [4] Aaron Bramson, Patrick Grim, Daniel J. Singer, William J. Berger, Graham Sack, Steven Fisher, Carissa Flocken, and Bennett Holman.  Understanding polarization: Meanings, measures, and model evaluation.  Philosophy of Science, 84(1):115–159, 2017.
  * [5] James A. Davis.  Clustering and structural balance in graphs.  Human Relations, 20(2):181–187, 1967.
  * [6] Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, and Carolyn L. Talcott.  Programming and symbolic computation in Maude.  J. Log. Algebraic Methods Program., 110, 2020.
  * [7] Christian G. Fermüller and George Metcalfe.  Giles’s game and the proof theory of Lukasiewicz logic.  Stud Logica, 92(1):27–61, 2009.
  * [8] Robert Freiman.  Games for hybrid logic - from semantic games to analytic calculi.  In Alexandra Silva, Renata Wassermann, and Ruy J. G. B. de Queiroz, editors, WoLLIC 2021, volume 13038 of LNCS, pages 133–149. Springer, 2021.
  * [9] Robert Freiman.  Games for hybrid logic.  Journal of Logic and Computation, to appear.
  * [10] Robert Freiman and Michael Bernreiter.  Truth and preferences - A game approach for qualitative choice logic.  In Sarah Alice Gaggl, Maria Vanina Martinez, and Magdalena Ortiz, editors, Logics in Artificial Intelligence - JELIA 2023, Proceedings, volume 14281 of LNCS, pages 547–560. Springer, 2023.
  * [11] Robert Freiman and Michael Bernreiter.  Validity in choice logics - A game-theoretic investigation.  In Helle Hvid Hansen, Andre Scedrov, and Ruy J. G. B. de Queiroz, editors, WoLLIC 2023, volume 13923 of LNCS, pages 211–226. Springer, 2023.
  * [12] Robert Freiman, Carlos Olarte, Elaine Pimentel, and Christian G. Fermüller.  Reasoning about group polarization: From semantic games to sequent systems. Technical report and tool available at https://github.com/promueva/PNL-game.git.  2024\.
  * [13] David Gale and F. M. Stewart.  Infinite games with perfect information, pages 245–266.  Princeton University Press, 1953.
  * [14] Frank Harary.  On the notion of balance of a signed graph.  Michigan Mathematical Journal, 2:143–146, 1953.
  * [15] Jaakko Hintikka.  Logic, language-games and information, Kantian themes in the philosophy of logic.  Revue Philosophique de la France Et de l’Etranger, 163:477–478, 1973.
  * [16] Daniel J Isenberg.  Group polarization: A critical review and meta-analysis.  Journal of Personality and Social Psychology, 50(6):1141, 1986\.
  * [17] Timo Lang, Carlos Olarte, Elaine Pimentel, and Christian G. Fermüller.  A game model for proofs with costs.  In Serenella Cerrito and Andrei Popescu, editors, TABLEAUX, volume 11714 of LNCS, pages 241–258. Springer, 2019.
  * [18] Fenrong Liu, Jeremy Seligman, and Patrick Girard.  Logical dynamics of belief change in the community.  Synth., 191(11):2403–2431, 2014.
  * [19] Paul Lorenzen and Kuno Lorenz, editors.  Dialogische Logik.  Wissenschaftliche Buchgesellschaft, [Abt. Verl.], Darmstadt, 1978.
  * [20] Sonia Marin, Dale Miller, Elaine Pimentel, and Marco Volpe.  From axioms to synthetic inference rules via focusing.  Ann. Pure Appl. Log., 173(5):103091, 2022.
  * [21] José Meseguer.  Twenty years of rewriting logic.  J. Log. Algebraic Methods Program., 81(7-8):721–781, 2012.
  * [22] David G Myers and Helmut Lamm.  The group polarization phenomenon.  Psychological Bulletin, 83(4):602, 1976.
  * [23] Sara Negri.  Proof analysis in modal logic.  J. Philosophical Logic, 34(5-6):507–544, 2005.
  * [24] Carlos Olarte, Elaine Pimentel, and Camilo Rocha.  A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems.  J. Log. Algebraic Methods Program., 130:100827, 2023.
  * [25] Alexandra Pavlova, Robert Freiman, and Timo Lang.  From semantic games to provability: The case of Gödel logic.  Studia Logica, 110:429–456, 2021.
  * [26] Mina Young Pedersen, Sonja Smets, and Thomas Ågotnes.  Modal logics and group polarization.  J. Log. Comput., 31(8):2240–2269, 2021.
  * [27] Jeremy Seligman, Fenrong Liu, and Patrick Girard.  Facebook and the epistemic logic of friendship.  In Burkhard C. Schipper, editor, Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, 2013.
  * [28] Alex K. Simpson.  The Proof Theory and Semantics of Intuitionistic Modal Logic.  PhD thesis, College of Science and Engineering, School of Informatics, University of Edinburgh, 1994.
  * [29] Cass R Sunstein.  The law of group polarization.  University of Chicago Law School, John M. Olin Law & Economics Working Paper, (91), 1999.
  * [30] Cass R Sunstein.  Group polarization and 12 angry men.  Negotiation Journal, 23(4):443–447, 2007.
  * [31] Johan van Benthem, Lei Li, Chenwei Shi, and Haoxuan Yin.  Hybrid sabotage modal logic.  J. Log. Comput., 33(6):1216–1242, 2023.
  * [32] Luca Viganò.  Labelled Non-Classical Logics.  Kluwer Academic Publishers, 2000.
  * [33] Zuojun Xiong and Thomas Ågotnes.  On the logic of balance in social networks.  J. Log. Lang. Inf., 29(1):53–75, 2020.
  * [34] Zuojun Xiong, Thomas Ågotnes, Jeremy Seligman, and Rui Zhu.  Towards a logic of tweeting.  In Alexandru Baltag, Jeremy Seligman, and Tomoyuki Yamada, editors, LORI, volume 10455 of LNCS, pages 49–64. Springer, 2017.

##  .7 Some selected proofs

Theorem 1. Let $\mathbb{M}$ be a PNL-model, $\mathsf{a}$ an agent, and $\phi$
a formula.

  1. 1.

_I_ have a winning strategy for
$\mathbf{G}_{\mathbb{M}}(\mathbf{P},\mathsf{a}:\phi)$ iff
$\mathbb{M},\mathsf{a}\models\phi$.

  2. 2.

_You_ have a winning strategy for
$\mathbf{G}_{\mathbb{M}}(\mathbf{P},\mathsf{a}:\phi)$ iff
$\mathbb{M},\mathsf{a}\not\models\phi$.

Proof: Both directions of (1) and (2) are shown simultaneously by induction on
the degree666Observe that, at this point of the text, the degree has not been
introduced yet. Its definition can be found just above Lemma 3 on page 8. of
the game state $g=\mathbf{P},\mathsf{a}:\phi$.

If $\phi$ is elementary, then the result trivially follows by the definition.

If $g=\mathbf{P},\mathsf{a}:\phi_{1}\wedge\phi_{2}$ then _I_ have a winning
strategy for
$\mathbf{G}_{\mathbb{M}}(\mathbf{P},\mathsf{a}:\phi_{1}\wedge\phi_{2})$ iff
_I_ have winning strategies for both
$\mathbf{G}_{\mathbb{M}}(\mathbf{P},\mathsf{a}:\phi_{1})$ and
$\mathbf{G}_{\mathbb{M}}(\mathbf{P},\mathsf{a}:\phi_{2})$. By the inductive
hypothesis, this is the case iff $\mathbb{M},\mathsf{a}\models\phi_{1}$ and
$\mathbb{M},\mathsf{a}\models\phi_{2}$, which is equivalent to
$\mathbb{M},\mathsf{a}\models\phi_{1}\wedge\phi_{2}$.

If $g=\mathbf{P},\mathsf{a}:\Diamond^{\pm}\phi$, _I_ have a winning strategy
for $\mathbf{G}_{\mathbb{M}}(\mathbf{P},\mathsf{a}:\Diamond^{\pm}\phi)$ iff
there is a $\mathsf{R}^{\pm}$-successor $\mathsf{b}$ of $\mathsf{a}$ and _I_
have a winning strategy for $\mathbf{P},\mathsf{b}:\phi$. By the inductive
hypothesis, this occurs iff $\mathbb{M},\mathsf{b}\models\phi$, but then
$\mathbb{M},\mathsf{a}\models\Diamond^{\pm}\phi$.

The other cases are similar. $\blacksquare$

Lemma 2. Let $\pi$ be as above. Then:
1) Let $g\in\pi$ be a non-elementary game state labelled “Y” in the semantic
game. Then at least one successor of $g$ appears along $\pi$.
2) Let $g\in\pi$ be a non-elementary game state labeled “I” in the semantic
game. Then all successors of $g$ appear along $\pi$.

Proof: First, note that since _You_ play according to _Your_ winning strategy,
$\pi$ does not end in a winning disjunctive state whose elementary party is
winning for _Me_. This means that case (C1) in the definition of $\sigma$ is
never reached.

  1. 1.

Suppose $g$ appeared in $\pi$ at stage $n\geq 0$ in the above construction.
Since every pair appears in the enumeration infinitely often, there is some
minimal $m\geq n$ such that $m=\\#(g,h)$, for some $h$. At step $m$ in the
execution of $\sigma$ against _Your_ winning strategy, the current disjunctive
state is of the form $D^{\prime}\bigvee g$. According to $\sigma$, _I_
underline $g$ and _You_ move to some successor $h^{\prime}$, according to
_Your_ winning strategy. This means the new game state is of the form
$D^{\prime}\bigvee h^{\prime}$, hence $h^{\prime}$ is the successor of $g$
appearing along $\mathfrak{h}$.

  2. 2.

Suppose $g$ appeared in $\pi$ at stage $n\geq 0$. Now we additionally fix an
arbitrary successor $h$ of $g$ in the evaluation game. By the properties of
$\\#$, there is a minimal $m\geq n$ such that $m=\\#(g,h)$. Since _I_ always
first duplicate game states labeled “I”, before _I_ make a move into them, $g$
does not disappear. Hence, at step $m$ in the execution of $\sigma$, the
current disjunctive state is of the form $D^{\prime}\bigvee g$. According to
$\sigma$, _I_ duplicate $g$ and go to $h$ in one copy, i.e. the new
disjunctive state is $D^{\prime}\bigvee g\bigvee h$, which shows that $h$
appears along $\pi$.

$\blacksquare$

Proposition 5 Let $j$ be a nominal different from $i$ not occurring in $D$ nor
in $\phi$. Then: (1) _You_ have a winning strategy in
$\mathbf{DG}(D\bigvee\mathbf{P},i:[A]\phi)$ iff _You_ have a winning strategy
in $\mathbf{DG}(D\bigvee\mathbf{P},j:\phi)$, and similarly for
$\mathbf{DG}^{\textbf{cc}}$.

(2) _You_ have a winning strategy in
$\mathbf{DG}(D\bigvee\mathbf{O},i:\Diamond^{\pm}\phi)$ iff _You_ have winning
strategies in both $\mathbf{DG}(D\bigvee\mathbf{P},\\_:R^{\pm}(i,j))$ and
$\mathbf{DG}(D\bigvee\mathbf{O},j:\phi)$, and similarly for
$\mathbf{DG}^{\textbf{cc}}$.

The proof is split into a sequence of lemmas. First, we need to define
substitutions formally. For a sequence $x$ of finite or infinite length, let
$x_{n}$ denote its $n$-th element (if defined), and let
$\mathrm{range}(x)=\\{x_{i}:i\in\mathbb{N}\\}$. Let $\phi$ be a formula and
$a$ and $b$ two sequences of nominals of the same length, where every nominal
occurs only once in each sequence. We define $\phi[a/b]$ as the formula
obtained by simultaneously substituting for every number $n$ all occurrences
of $a_{n}$ in $\phi$ with $b_{n}$. For example, let $a=\langle i,j\rangle$,
$b=\langle k,l\rangle$ and $\phi=R^{+}(i,j)\vee R^{-}(j,l)$. Then
$\phi[a/b]=R^{+}(k,l)\vee R^{-}(l,l)$. As another example let $a=\langle
i_{1},i_{2},...\rangle$ and $b=\langle i_{2},i_{3},...\rangle$. Then
$R^{+}(i_{1},i_{2})[a/b]=R^{+}(i_{2},i_{3})$, since the substitution happens
simultaneously. We extend the notion of substitution to game states: for a
game state $g=\mathbf{Q},i:\phi$ of the evaluation game and two sequences of
nominals $a,b$, we define the substitution $g[a/b]$ as
$\mathbf{Q},i[a/b]:\phi[a/b]$. Similarly to histories, strategies, and
disjunctive states.

######  Lemma 6.

Let
$\mathbb{M}_{1}=(\mathsf{A},\mathsf{R}^{+},\mathsf{R}^{-},\mathsf{V},\mathsf{g}_{1})$
and
$\mathbb{M}_{2}=(\mathsf{A},\mathsf{R}^{+},\mathsf{R}^{-},\mathsf{V},\mathsf{g}_{2})$
be named and $\mathsf{g}_{2}(i[b/a])=\mathsf{g}_{1}(i)$ for all nominals $i$.
Then for all game states $g$,
$\mathbf{G}_{\mathbf{M}_{1}}(g)\cong\mathbf{G}_{\mathbb{M}_{2}}(g[b/a])$.

Proof: By the assumption, $\mathsf{g}_{2}$ is surjective, even if restricted
to $N[b/a]=\\{i[b/a]:i\in N\\}$. By Proposition 2, it is, therefore, enough to
prove
$\mathbf{G}_{\mathbb{M}_{1}}(g)\cong\mathbf{G}^{N[b/a]}_{\mathbb{M}_{2}}(g[b/a])$.
We proceed by induction on the degree of $g$.

If $g$ is elementary and of the form $\mathbf{P},i:j$ then it is winning for
_Me_ over $\mathbb{M}_{1}$ if and only if
$\mathsf{g}_{1}(i)=\mathsf{g}_{1}(j)$. By assumption, this is equivalent to
$\mathsf{g}_{2}(i[b/a])=g_{2}(i[b/a])$, which means that
$\mathbf{O},i[b/a]:j[b/a]$ is winning for me over $\mathbb{M}_{2}$. The other
elementary cases are similar.

As an example of a simple induction step, we consider
$\mathbf{P},i:\phi_{1}\vee\phi_{2}$. If _I_ have a winning strategy for this
game state over $\mathbb{M}_{1}$, then there is some $k\in\\{1,2\\}$ such that
_I_ have a winning strategy in $\mathbf{P},i:\phi_{k}$. By the inductive
hypothesis, _I_ have a winning strategy in $\mathbf{P},i[b/a]:\phi_{k}[b/a]$
over $\mathbb{M}_{2}$. Hence, _I_ have a winning strategy in
$(\mathbf{P},i:\phi_{1}\vee\phi_{2})[b/a])$ over that model. The other
direction is similar.

The most interesting induction step is for the modal rules, so let us consider
$\mathbf{O},i:\meddiamondplus\psi$. Suppose, _I_ have a winning strategy in
$\mathbf{G}_{\mathbb{M}_{1}}(\mathbf{O},i:\meddiamondplus\psi)$. Then, for
every nominal $j$, _I_ have winning strategies in
$\mathbf{G}_{\mathbb{M}_{1}}(\mathbf{P},j:R(i,j))$ and
$\mathbf{G}_{\mathbb{M}_{1}}(\mathbf{O},j:\psi)$. By the inductive hypothesis,
_I_ have winning strategies in
$\mathbf{G}^{N[b/a]}_{\mathbb{M}_{2}}(\mathbf{P},j[b/a]:R(i[b/a],j[b/a]))$ and
$\mathbf{G}^{N[b/a]}_{\mathbb{M}_{2}}(\mathbf{O},j[b/a]:\psi[b/a])$. In other
words, _I_ have winning strategies in
$\mathbf{G}^{N[b/a]}_{\mathbb{M}_{2}}(\mathbf{P},k:R(i[b/a],k)$ and
$\mathbf{G}^{N[b/a]}_{\mathbb{M}_{2}}(\psi[b/a])$, for every $k\in N[b/a]$.
Since branching in this game is restricted over $N[b/a]$, we conclude that _I_
have a winning strategy in
$\mathbf{G}^{N[b/a]}_{\mathbb{M}_{2}}((\mathbf{P},i:\meddiamondplus\psi)[b/a])$.
The other direction, as well as the other cases of induction steps, are
similar. $\blacksquare$

######  Lemma 7.

If $\mathsf{g}(k)=\mathsf{g}(l)$, then
$\mathbf{G}_{\mathbb{M}}(g)\cong\mathbf{G}_{\mathbb{M}}(g[k/l])$.

Proof: We show that $\mathsf{g}(i[k/l])=\mathsf{g}(i)$ for all nominals $i$.
If $i\neq k$, then $\mathsf{g}(i[k/l])=\mathsf{g}(i)$. If $i=k$, then by the
assumption, $\mathsf{g}(i[k/l])=\mathsf{g}(l)=\mathsf{g}(k)=\mathsf{g}(i)$.
The statement of the lemma follows from this fact and Lemma 6. $\blacksquare$

For a model $\mathbb{M}$ and two sequences of nominals $a,b$, let
$\mathbb{M}[a/b]$ be the same as $\mathbb{M}$, except for the denotation
function: $\mathsf{g}_{[a/b]}(i)=\mathsf{g}(i[a/b])$.

######  Lemma 8.

Let $\mathbb{M}$ be named and $a,b$ two sequences of nominals with
$\mathrm{range}(a)\subseteq\mathrm{range}(b)$. Then $\mathbb{M}{[a/b]}$ is
$N[b/a]$-named. Furthermore,
$\mathbf{G}_{\mathbb{M}}(g)\cong\mathbf{G}_{\mathbb{M}[a/b]}(g[b/a])$.

Proof: We have to show that $\mathsf{g}_{[a/b]}$ is surjective when restricted
to $N[b/a]=\\{i[b/a]:i\in N\\}$. Let $\mathsf{a}$ be an agent and $i$ its name
under $\mathsf{g}$. If $i\notin\mathrm{range}(b)$, then
$i\notin\mathrm{range}(b)$ and we have $i[b/a][a/b]=i[a/b]=i$. If
$i\in\mathrm{b}$, then $i=b_{m}$ for some $m$. Then
$i[b/a][a/b]=b_{m}[b/a][a/b]=a_{m}[a/b]=b_{m}=i$. This shows that
$\mathsf{g}_{[a/b]}(i[b/a])=\mathsf{g}(i[b/a][a/b])=\mathsf{g}(i)$, i.e.
$\mathsf{a}$ has a name in $N[b/a]$ under $g_{[a/b]}$. This identity together
with Lemma 6 also implies the strategic equivalence of the game
$\mathbf{G}_{\mathbb{M}}(g)$ and $\mathbf{G}_{\mathbb{M}[a/b]}(g[b/a])$.
$\blacksquare$

We are now ready to prove Proposition 5.

Proof: [Proposition 5] We will show (2), since (1) is similar and simpler.
From right to left is trivial. For the other direction, assume that _You_ have
a winning strategy in $\mathbf{DG}(D\bigvee\mathbf{O},i:\meddiamondplus\phi)$
with $j$ as in the assumption. By Theorem 2, there is a named model
$\mathbb{M}$ such that _You_ have winning strategies in
$\mathbf{G}_{\mathbb{M}}(g)$ for all $g\in D$ and in
$\mathbf{O},i:\meddiamondplus\phi$. The latter implies that _You_ have winning
strategies in $\mathbf{G}_{\mathbb{M}}(\mathbf{O},\\_:R^{\pm}(i,k))$ and
$\mathbf{G}_{\mathbb{M}}(\mathbf{O},k:\phi)$ for some nominal $k$.

Let $j_{1},j_{2},...$ be a sequence of nominals not occurring in $D$ or $\phi$
and different from $k$, $j$, and $i$. Let $a=\langle j,j_{1},j_{2},...\rangle$
and $b=\langle k,j,j_{1},j_{2},...\rangle$. We have that
$\mathrm{range}(a)\subseteq\mathrm{range}(b)$, therefore Lemma 8 applies. We
have the following chain of equivalences:

$\displaystyle\mathbf{G}_{\mathbb{M}}(\mathbf{O},k:\phi)$
$\displaystyle\cong\mathbf{G}_{\mathbb{M}[a/b]}(\mathbf{O},k[b/a]:\phi[b/a])$
by Lemma 8
$\displaystyle=\mathbf{G}_{\mathbb{M}[a/b]}(\mathbf{O},j:\phi[k/j])$
$\displaystyle\text{by conditions on }i,j,k$
$\displaystyle=\mathbf{G}_{\mathbb{M}[a/b]}(\mathbf{O},j[k/j]:\phi[k/j])$
$\displaystyle\cong\mathbf{G}_{\mathbb{M}[a/b]}(\mathbf{O},j:\phi)$
$\displaystyle\text{by Lemma~{}\ref{lem:samename}}\text{ and
}\mathsf{g}_{[a/b]}(j)=\mathsf{g}_{[a/b]}(k)$

A similar argument shows that
$\mathbf{G}_{\mathbb{M}}(\mathbf{O},\\_:R^{\pm}(i,k))\cong\mathbf{G}_{\mathbb{M}[a/b]}(\mathbf{O},\\_:R^{\pm}(i,j))$.
By this equivalence and the assumption, _You_ have winning strategies in
$\mathbf{O},\\_:R^{\pm}(i,j)$ and $\mathbf{O},j:\phi$ over $\mathbb{M}[a/b]$.
Moreover, we obtain a winning strategy for _You_ for $g\in D$ by using the
equivalence
$\mathbf{G}_{\mathbb{M}}(g)\cong\mathbf{G}_{\mathbb{M}[a/b]}(g[b/a])\cong\mathbf{G}_{\mathbb{M}[a/b]}(g[k/j])\cong\mathbf{G}_{\mathbb{M}[a/b]}(g)$,
the same lemmas as before and the fact that no nominals from $a$ appear in
$g$. Since _You_ have winning strategies for the semantic games for every
$g\in D$ and $\mathbf{O},\\_:R^{\pm}(i,j)$ over $\mathbb{M}[a/b]$, _You_ have
a winning strategy in $\mathbf{DG}(D\bigvee\mathbf{O},\\_:R^{\pm}(i,j))$, by
Proposition 2 and the determinacy of the game. Similarly, we conclude that
_You_ have a winning strategy in $\mathbf{DG}(D\bigvee\mathbf{O},j:\phi)$.
$\blacksquare$

Lemma 4. Let $\Gamma\Rightarrow\Delta$ be composed of elementary game states
only. _I_ win the disjunctive game in $\Gamma\Rightarrow\Delta$ iff one of the
following holds

  * i.

$R^{-}(i,i)\in\Gamma$ or $R^{+}(i,i)\in\Delta$ for some $i$;

  * ii.

$\\{R^{+}(i,j),R^{-}(i,j)\\}\subseteq\Gamma$ for some $i\not=j$;

  * iii.

$\Gamma\cap\Delta\not=\varnothing$.

In the case of collectively connected models, additionally,

  * iv.

$\\{R^{+}(i,j),R^{-}(i,j)\\}\subseteq\Delta$ for some $i\not=j$

Proof: $\mathbb{M}_{\Gamma\Rightarrow\Delta}$ is non-overlapping: this follows
by (ii). $\mathbb{M}_{\Gamma\Rightarrow\Delta}^{\textbf{cc}}$ is collectively
connected, since $(iii)^{+}$ in the definition of $\mathsf{R}^{+}$ equivalent
to $\neg((i)^{+}\vee(ii)^{+}\vee(i)^{-}\vee(ii)^{-})$.
$\mathbb{M}^{\textbf{cc}}_{\Gamma\Rightarrow\Delta}$ is non-overlapping:
Suppose, $(\mathsf{a}_{i},\mathsf{a}_{j})\in\mathsf{R}^{+}\cap\mathsf{R}^{-}$.
This is impossible since all possible cases in the definitions, in which
$\mathsf{a}_{i}$ and $\mathsf{a}_{j}$ are connected by both relations, are
excluded by our assumptions:

  * •

$(i)^{+}$ and $(i)^{-}$: Excluded by $\neg(ii)$.

  * •

$(i)^{+}$ and $(ii)^{-}$: Excluded by $\neg(iii)$.

  * •

$(ii)^{-}$ and $(i)^{-}$: Excluded by $\neg(iii)$.

  * •

$(ii)^{-}$ and $(ii)^{-}$: Excluded by $\neg(iv)$.

  * •

$(iii)^{+}$, excludes $(i)^{-}$ and $(ii)^{-}$, hence
$(\mathsf{a}_{i},\mathsf{a}_{j})\notin\mathsf{R}^{-}$.

By definition of the models, $\mathsf{a}_{i}\in\mathsf{V}(p)$, whenever
$i:p\in\Gamma$, $\mathsf{a}_{i}\notin\mathsf{V}(p)$, whenever $i:p\in\Delta$,
$(\mathsf{a}_{i},\mathsf{a}_{j})\in\mathsf{R}^{\pm}$, whenever
$R^{\pm}(i,j)\in\Gamma$. If $R^{\pm}(i,j)\in\Delta$, then
$(\mathsf{a}_{i},\mathsf{a}_{j})\in\mathsf{R}^{\mp}$. Since both models are
non-overlapping, $(\mathsf{a}_{i},\mathsf{a}_{j})\notin\mathsf{R}^{\pm}$.
Hence, all game states in $\Gamma\Rightarrow\Delta$ are winning for _You_.
$\blacksquare$

Lemma 5. The following weakening rules are admissible in $\mathbf{DS}$

$\Gamma,i:\phi\Rightarrow\Delta\Gamma\Rightarrow\Delta\qquad\Gamma\Rightarrow\Delta,i:\phi\Gamma\Rightarrow\Delta$

Moreover, in a bottom-up reading of derivations, the relational rules permutes
up w.r.t. any other logical rule in $\mathbf{DS}$.

Proof: The proof of weakening is standard. The proof of permutability is by
straightforward case analysis. For example,

$\Gamma,i:\meddiamondminus\phi\Rightarrow\Delta\lx@proof@logical@and\Gamma,i:\meddiamondminus\phi\Rightarrow\Delta,R^{+}(k,l)\Gamma,j:\phi\Rightarrow\Delta,R^{+}(k,l)\pi_{1}\Gamma,i:\meddiamondminus\phi\Rightarrow\Delta,R^{-}(k,l)\pi_{2}$

with $j$ free, can be transformed to

$\Gamma,i:\meddiamondminus\phi\Rightarrow\Delta\Gamma,i:\meddiamondminus\phi,i:\meddiamondminus\phi\Rightarrow\Delta\Gamma,j:\phi,i:\meddiamondminus\phi\Rightarrow\Delta\lx@proof@logical@and\Gamma,j:\phi,i:\meddiamondminus\phi\Rightarrow\Delta,R^{+}(k,l)\pi_{1}^{w}\Gamma,j:\phi,i:\meddiamondminus\phi\Rightarrow\Delta,R^{-}(k,l)\pi_{2}^{w}$

where $\pi_{1}^{w},\pi_{2}^{w}$ are the weakened versions of $\pi_{1},\pi_{2}$
respectively. $\blacksquare$

Theorem 6. Let $\Gamma$ and $\Delta$ be multisets of dPNL formulas not
containing relational predicates. _I_ have a winning strategy in the
disjunctive game $\mathbf{dDG}(\Gamma\Rightarrow\Delta)$ iff
$\Gamma\Rightarrow\Delta$ is provable in $\mathbf{dDS}$.

Proof: First of all, we observe that the rule

R^±(i,j),Γ, j:ϕ⇒Δ $1[$$(L^{\prime}_{\Diamond^{\pm}})$]Γ, i: ◇^±ϕ⇒Δ

is admissible in $\mathbf{DS}$. In fact, this is an easy consequence of the
presence of the contraction rules. Hence, although the rule
$(L_{\Diamond^{\pm}})$ in $\mathbf{dDS}$ is not directly defined via a
provability game, it is equivalent to its contracted version. The rest of the
proof follows the same lines as the proof in Theorem 3. $\blacksquare$

##  .8 Examples

Below we present _My_ strategy for winning the game on model $\mathbb{M}_{1}$
in Example 1. 777The notation $[\checkmark,\texttt{Q}]$ means that _I_ have a
winning strategy starting in that state where $Q\in\\{\emph{I},\emph{You}\\}$
moves. The notation $[\times,\texttt{Q}]$ means that _You_ have a winning
strategy where $Q\in\\{\emph{I},\emph{You}\\}$ moves.

python main.py examples/model-M1.maude a "lb(p)"[$\checkmark$,Y] : P @ a : (¬
( p $\vee$ p) $\vee$ p) $\wedge$ ¬ ( p $\vee$ p) $\vee$ p├── [$\checkmark$,I]
: P @ a : ¬ ( p $\vee$ p) $\vee$ p│ └── [$\checkmark$,I] : P @ a : p│ └──
[$\checkmark$,I] : P @ b : p└── [$\checkmark$,I] : P @ a : ¬ ( p $\vee$ p)
$\vee$ p └── [$\checkmark$,I] : P @ a : ¬ ( p $\vee$ p) └── [$\checkmark$,Y] :
O @ a : p $\vee$ p ├── [$\checkmark$,Y] : O @ a : p │ ├── [$\checkmark$,Y] : O
@ a : p │ │ └── [$\checkmark$,Y] : O @ c : p │ └── [$\checkmark$,Y] : O @ b :
p │ └── [$\checkmark$,Y] : O @ c : p └── [$\checkmark$,Y] : O @ a : p └──
[$\checkmark$,Y] : O @ c : p └── [$\checkmark$,Y] : O @ c : p

_I_ do not have a winning strategy for the game on the model $\mathbb{M}_{2}$
in Example 1:

python main.py examples/model-M2.maude a "lb(p)" --tree[$\times$,Y] : P @ a :
(¬ ( p $\vee$ p) $\vee$ p) $\wedge$ ¬ ( p $\vee$ p) $\vee$ p├── [$\times$,I] :
P @ a : ¬ ( p $\vee$ p) $\vee$ p│ ├── [$\times$,I] : P @ a : ¬ ( p $\vee$ p)│
│ └── [$\times$,Y] : O @ a : p $\vee$ p│ │ ├── [$\times$,Y] : O @ a : p│ │ │
├── [$\times$,Y] : O @ c : p│ │ │ │ └── [$\times$,Y] : O @ b : p│ │ │ ├──
[$\checkmark$,Y] : O @ a : p│ │ │ └── [$\checkmark$,Y] : O @ b : p│ │ │ └──
[$\checkmark$,Y] : O @ c : p│ │ └── [$\checkmark$,Y] : O @ a : p│ └──
[$\times$,I] : P @ a : p└── [$\checkmark$,I] : P @ a : ¬ ( p $\vee$ p) $\vee$
p ├── [$\times$,I] : P @ a : ¬ ( p $\vee$ p) │ └── [$\times$,Y] : O @ a : p
$\vee$ p │ ├── [$\times$,Y] : O @ a : p │ │ ├── [$\times$,Y] : O @ a : p │ │ │
├── [$\times$,Y] : O @ b : p │ │ │ ├── [$\checkmark$,Y] : O @ a : p │ │ │ └──
[$\checkmark$,Y] : O @ c : p │ │ ├── [$\times$,Y] : O @ b : p │ │ │ ├──
[$\times$,Y] : O @ b : p │ │ │ └── [$\checkmark$,Y] : O @ a : p │ │ └──
[$\checkmark$,Y] : O @ c : p │ │ ├── [$\checkmark$,Y] : O @ a : p │ │ └──
[$\checkmark$,Y] : O @ c : p │ └── [$\checkmark$,Y] : O @ a : p └──
[$\checkmark$,I] : P @ a : p ├── [$\times$,I] : P @ a : p ├── [$\times$,I] : P
@ c : p └── [$\checkmark$,I] : P @ b : p

And _I_ certainly win in the negated formula:

python main.py examples/model-M2.maude a "~ lb(p)"[$\checkmark$,I] : P @ a : ¬
((¬ ( p $\vee$ p) $\vee$ p) $\wedge$ ¬ ( p $\vee$ p) $\vee$ p)└──
[$\checkmark$,I] : O @ a : (¬ ( p $\vee$ p) $\vee$ p) $\wedge$ ¬ ( p $\vee$ p)
$\vee$ p └── [$\checkmark$,Y] : O @ a : ¬ ( p $\vee$ p) $\vee$ p ├──
[$\checkmark$,I] : O @ a : ¬ ( p $\vee$ p) │ └── [$\checkmark$,I] : P @ a : p
$\vee$ p │ └── [$\checkmark$,I] : P @ a : p │ └── [$\checkmark$,I] : P @ c : p
│ └── [$\checkmark$,I] : P @ b : p └── [$\checkmark$,Y] : O @ a : p

The winning strategy for the game
$\mathbf{P},\mathbb{M}_{2},\mathsf{a}:\langle\ominus\rangle(4B)$ is the
following:

python main.py examples/model-M2.maude a " (-) lb(p)"[$\checkmark$,I] : P @ a
: (-)((¬ ( p $\vee$ p) $\vee$ p) $\wedge$ ¬ ( p $\vee$ p) $\vee$ p)└──
[$\checkmark$,Y] : P @ a : (¬ ( p $\vee$ p) $\vee$ p) $\wedge$ ¬ ( p $\vee$ p)
$\vee$ p ├── [$\checkmark$,I] : P @ a : ¬ ( p $\vee$ p) $\vee$ p │ └──
[$\checkmark$,I] : P @ a : ¬ ( p $\vee$ p) │ └── [$\checkmark$,Y] : O @ a : p
$\vee$ p │ ├── [$\checkmark$,Y] : O @ a : p │ │ ├── [$\checkmark$,Y] : O @ a :
p │ │ │ ├── [$\checkmark$,Y] : O @ a : p │ │ │ └── [$\checkmark$,Y] : O @ c :
p │ │ └── [$\checkmark$,Y] : O @ c : p │ │ ├── [$\checkmark$,Y] : O @ a : p │
│ └── [$\checkmark$,Y] : O @ c : p │ └── [$\checkmark$,Y] : O @ a : p │ └──
[$\checkmark$,Y] : O @ b : p │ ├── [$\checkmark$,Y] : O @ a : p │ └──
[$\checkmark$,Y] : O @ c : p └── [$\checkmark$,I] : P @ a : ¬ ( p $\vee$ p)
$\vee$ p └── [$\checkmark$,I] : P @ a : p └── [$\checkmark$,I] : P @ b : p

and _I_ can win the following game in Example 3.

python main.py examples/model-M2.maude a " ~ ( (-) (-) lb(p))"[$\checkmark$,I]
: P @ a : ¬ ((-)(-)((¬ ( p $\vee$ p) $\vee$ p) $\wedge$ ¬ ( p $\vee$ p) $\vee$
p))└── [$\checkmark$,Y] : O @ a : (-)(-)((¬ ( p $\vee$ p) $\vee$ p) $\wedge$ ¬
( p $\vee$ p) $\vee$ p) ├── [$\checkmark$,Y] : O @ a : (-)((¬ ( p $\vee$ p)
$\vee$ p) $\wedge$ ¬ ( p $\vee$ p) $\vee$ p) │ └── [$\checkmark$,I] : O @ a :
(¬ ( p $\vee$ p) $\vee$ p) $\wedge$ ¬ ( p $\vee$ p) $\vee$ p │ └──
[$\checkmark$,Y] : O @ a : ¬ ( p $\vee$ p) $\vee$ p │ ├── [$\checkmark$,I] : O
@ a : ¬ ( p $\vee$ p) │ │ └── [$\checkmark$,I] : P @ a : p $\vee$ p │ │ └──
[$\checkmark$,I] : P @ a : p │ │ └── [$\checkmark$,I] : P @ c : p │ │ └──
[$\checkmark$,I] : P @ b : p │ └── [$\checkmark$,Y] : O @ a : p │ └──
[$\checkmark$,Y] : O @ a : p └── [$\checkmark$,Y] : O @ a : (-)((¬ ( p $\vee$
p) $\vee$ p) $\wedge$ ¬ ( p $\vee$ p) $\vee$ p) └── [$\checkmark$,I] : O @ a :
(¬ ( p $\vee$ p) $\vee$ p) $\wedge$ ¬ ( p $\vee$ p) $\vee$ p └──
[$\checkmark$,Y] : O @ a : ¬ ( p $\vee$ p) $\vee$ p ├── [$\checkmark$,I] : O @
a : ¬ ( p $\vee$ p) │ └── [$\checkmark$,I] : P @ a : p $\vee$ p │ └──
[$\checkmark$,I] : P @ a : p │ └── [$\checkmark$,I] : P @ c : p │ └──
[$\checkmark$,I] : P @ b : p └── [$\checkmark$,Y] : O @ a : p └──
[$\checkmark$,Y] : O @ a : p

In the same example, this is _My_ winning strategy for
$\mathbf{P},\mathbb{M}_{2},\mathsf{a}:\meddiamondplus\langle\oplus\rangle[A]\boxminus\bot$:

python main.py examples/model-M2.maude a "<+> (+) [A] [-] (p /\ ~
p)"[$\checkmark$,I] : P @ a : (+)[A]¬ ( ¬ (p $\wedge$ ¬ p))└──
[$\checkmark$,I] : P @ b : (+)[A]¬ ( ¬ (p $\wedge$ ¬ p)) └── [$\checkmark$,Y]
: P @ b : [A]¬ ( ¬ (p $\wedge$ ¬ p)) ├── [$\checkmark$,I] : P @ a : ¬ ( ¬ (p
$\wedge$ ¬ p)) │ └── [$\checkmark$,Y] : O @ a : ¬ (p $\wedge$ ¬ p) ├──
[$\checkmark$,I] : P @ b : ¬ ( ¬ (p $\wedge$ ¬ p)) │ └── [$\checkmark$,Y] : O
@ b : ¬ (p $\wedge$ ¬ p) └── [$\checkmark$,I] : P @ c : ¬ ( ¬ (p $\wedge$ ¬
p)) └── [$\checkmark$,Y] : O @ c : ¬ (p $\wedge$ ¬ p)