# A Modal Logic of Epistemic Games

Emiliano Lorini, François Schwarzentruber

► To cite this version:

Emiliano Lorini, François Schwarzentruber. A Modal Logic of Epistemic Games. Games, 2010, Epistemic Game Theory and Modal Logic, 1 (4), pp.478-526. 10.3390/g1040478. hal-03672510

HAL Id: hal-03672510

https://hal.science/hal-03672510

Submitted on 19 May 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Article

# A Modal Logic of Epistemic Games

Emiliano Lorini¹, François Schwarzentruber¹

¹ Institut de Recherche en Informatique de Toulouse (IRIT), CNRS, France

* Author to whom correspondence should be addressed; lorini@irit.fr, schwarze@irit.fr

Version November 25, 2010 submitted to Games. Typeset by LATEX using class file mdpi.cls

**Abstract:** We propose some variants of a multi-modal logic of joint action, preference and knowledge that support reasoning about epistemic games in strategic form.

The first part of the paper deals with games with complete information. We first provide syntactic proofs of some theorems that are well-known in the area of interactive epistemology and that specify some sufficient epistemic conditions of equilibrium notions such as Nash equilibrium and Iterated Deletion of Strictly Dominated Strategies (IDSDS). Then, we present a variant of the logic extended with dynamic operators of Dynamic Epistemic Logic (DEL). We show that it allows to express the notion IDSDS in a more compact way.

The second part of the paper deals with games with weaker forms of complete information. We first discuss several assumptions on different aspects of perfect information about the game structure (e.g. the assumption that a player has perfect knowledge about the players' strategy sets or about the preference orderings over strategy profiles), and show that every assumption is expressed by a corresponding logical axiom of our logic. Then we provide a proof of Harsanyi's claim that all uncertainty about the structure of a game can be reduced to uncertainty about payoffs.

Sound and complete axiomatizations of the logics presented in the paper are given, as well as some complexity results for the satisfiability problem.

**Keywords:** Game theory; modal logic; Dynamic Epistemic Logic

## 1. Introduction

The aim of this article is to propose a modal logic framework that allows to reason about epistemic games in strategic form. In this kind of games players decide what to do according to some general
principles of rationality while being uncertain about several aspects of the interaction such as other agents' choices, other agents' preferences, etc.

While epistemic games have been extensively studied in economics (in the so-called interactive epistemology area, see e.g. [1–6]) and while there have been few analyses of epistemic games in modal logic (see, e.g., [3,7–9]), no modal logic approach to epistemic games has been proposed up to now which addresses all the following issues at the same time:

* to provide a *logic*, and a corresponding *formal semantics*, which is sufficiently general:

- to express solution concepts like Nash Equilibrium or Iterated Deletion of Strictly Dominated Strategies (IDSDS) and to derive syntactically the epistemic and rationality conditions on which such solution concepts are based,

- to study both epistemic games with *complete* information and with *incomplete* information;

* to prove its *soundness* and *completeness*;

* to study its computational properties like *decidability* and *complexity*.

In this article, we try to fill this gap by proposing some variants of a multi-modal logic of joint action, preference and knowledge interpreted on a Kripke-style semantics, that allow to represent both epistemic games with complete information and epistemic games with different forms of incomplete information about the game structure. We give sound and complete axiomatizations of all these logics as well as some complexity results for the satisfiability problem.

The article is organized in two parts: the first part is focused on strategic games with complete information, while the second one extends the analysis to strategic games with incomplete information.

In Section 2 we present a modal logic, called *MLEG* (*Modal Logic of Epistemic Games*), that supports reasoning about epistemic games with complete information in which an agent can only have uncertainty about other agents’ current choices. A complete axiomatization and complexity results for this logic are given.

Section 3 is devoted to the analysis in *MLEG* of the epistemic conditions of Nash equilibrium and IDSDS. We use the logic *MLEG* in order to provide syntactic proofs of some theorems that are well-known in the area of interactive epistemology such as the theorem that specifies some sufficient epistemic conditions of Nash equilibrium in terms of players’ rationality and knowledge about other players’ choices, and the theorem characterizing IDSDS in terms of common knowledge about rationality.

In Section 4 we make *MLEG* dynamic by extending it with constructions of Dynamic Epistemic Logic (DEL) [10–12], and we show that this dynamic version of *MLEG* allows to express the notion IDSDS in a more compact way than in the static *MLEG*. A complete axiomatization for this dynamic extension of the logic *MLEG* is given.

In Section 5 we show how our logical framework can be easily adapted in order to study strategic interaction with incomplete information about the game structure. In Section 6 we discuss several assumptions on different aspects of complete information about the game structure (e.g. the assumption that a player has perfect knowledge about the players’ strategy sets or about the players’ preference ordering over strategy profiles). We show that every assumption is expressed by a corresponding logical axiom. Consequently, a class of epistemic games characterized by a specific aspect of complete
information about the game structure corresponds to a specific variant of the logic *MLEG*. We present some complexity results for these variants of the logic *MLEG*, that are interesting because they show how complexity of our logic varies from games with complete information to games with incomplete information.

We also provide a formal proof of Harsanyi's claim that all uncertainty about the structure of a game can be reduced to uncertainty about payoffs. The novel aspect of our contribution is that we prove Harsanyi's claim in a purely qualitative setting with no probabilities, while existing proofs are given in a quantitative setting with probabilities (see, e.g., [13]).

Proofs of theorems are given in an Annex at the end of the article.

Before concluding this introduction, we would like to emphasize an aspect of our work that could be interesting for a game-theorist.

As the logics presented in this paper are sound and complete, they allow to study strategic interaction both at the semantic level and at the syntactic level. In this sense, they provide a formal framework which unifies two approaches traditionally opposed by authors working in the area of formal interactive epistemology: the semantic approach and the syntactic approach.<fnref n="1" /> However, it is worth noting that syntactic derivations of various results concerning the epistemic foundations of game theory are not interesting in itself. Instead, this kind of analysis is useful to identify specific features that are important for the foundations of game theory, for example whether certain assumptions on the players’ knowledge are indeed necessary to prove results concerning the epistemic conditions of equilibrium notions such as Nash equilibrium and IDSDS. Typical assumptions on players’ knowledge are for example the assumption that knowledge is positively and negatively introspective (i.e. if I know that $\varphi$ is true then I know that I know that $\varphi$ is true, and if I do not know that $\varphi$ is true then I know that I do not know that $\varphi$ is true), the factivity principle that knowing that $\varphi$ implies that $\varphi$ is true, the assumption that every player knows what he has decided to do, or the assumption that a player has perfect knowledge about some aspects of the game such as the players’ strategy sets and the players’ preference ordering over strategy profiles.

## 2. A logic of joint actions, knowledge and preferences

We present in this section the multi-modal logic *MLEG* (*Modal Logic of Epistemic Games*) integrating the concepts of joint action, belief and preference. This logic supports reasoning about epistemic games in strategic form in which an agent might be uncertain about the current choices of the other agents.

### 2.1. Syntax

The syntactic primitives of *MLEG* are the finite set of agents *Agt*, the set of atomic formulas *Atm*, a nonempty finite set of atomic action names *Act* = {*a*₁, *a*₂, ..., *a*|*Act*|}. Non-empty sets of agents are called *coalitions* or *groups*, noted *C*₁, *C*₂, .... We note 2<sup>*Agt*</sup>\{Ø} the set of coalitions.

To every agent *i* ∈ *Agt* we associate the set *Act*<sub>*i*</sub> of all possible ordered pairs agent/action *i*:a, that is, *Act*<sub>*i*</sub> = {*i*:a | *a* ∈ *Act*}. Besides, for every coalition *C* we note Δ<sub>*C*</sub> the set of all joint actions of this coalition, that is, Δ<sub>*C*</sub> = Π<sub>*i*∈*C*</sub> *Act*<sub>*i*</sub>. Elements in Δ<sub>*C*</sub> are *C*-tuples noted α<sub>*C*</sub>, β<sub>*C*</sub>, γ<sub>*C*</sub>, δ<sub>*C*</sub>, .... If *C* = *Agt*,

<footnote n="1">¹See [2] for an analysis of the relation between the two approaches.</footnote>
we write $\Delta$ instead of $\Delta_{Agt}$. Elements in $\Delta$ are also called strategy profiles. Given $\delta \in \Delta$, we note $\delta_i$ the element in $\delta$ corresponding to agent $i$. Moreover, for notational convenience, we write $\delta_{-i} = \delta_{Agt \setminus \{i\}}$.

The language $\mathcal{L}_{MLEG}$ of the logic MLEG is given by the following rule:

$$ \varphi ::= p \mid \bot \mid \neg \varphi \mid (\varphi \lor \varphi) \mid [\delta_C] \varphi \mid \Box \varphi \mid K_i \varphi \mid [\mathbf{good}]_i \varphi $$

where $p$ ranges over $Atm$, $i$ ranges over $Agt$, and $\delta_C$ ranges over $\bigcup_{C \in 2^{Agt}*} \Delta_C$. The classical Boolean connectives $\wedge$, $\rightarrow$, $\leftrightarrow$ and $\top$ (tautology) are defined from $\bot$, $\vee$ and $\neg$ in the usual manner. We also follow the standard rules for omission of parentheses.

The formula $[\delta_C] \varphi$ reads “if coalition $C$ chooses the joint action $\delta_C$ then $\varphi$ holds”. Therefore, $[\delta_C] \bot$ reads “coalition $C$ does not choose the joint action $\delta_C$”.

$\Box$ is a necessity operator which enables to quantify over possible joint actions of all agents, that is, over the strategy profiles of the current game (the terms “joint actions of all agents” and “strategy profiles” are supposed here to be synonymous). $\Box \varphi$ reads “$\varphi$ holds for every alternative strategy profile of the current game”, or simply “$\varphi$ is necessarily true”.

Operators $K_i$ are standard epistemic modal operators. Construction $K_i\varphi$ is read as usual “agent $i$ knows that $\varphi$ is true”, whereas the construction $[\mathbf{good}]_i\varphi$ is read “$\varphi$ is true in all worlds which are for agent $i$ at least as good as the current one concerning the strategy profile that is chosen”. We define $\langle \mathbf{good} \rangle_i\varphi$ as an abbreviation of $\neg [\mathbf{good}]_i \neg \varphi$. Operators $[\mathbf{good}]_i$ are used in MLEG to define agents’ preference orderings over the strategy profiles of the current game. Similar operators are studied by [14].

We use $EK_C\varphi$ as an abbreviation of $\bigwedge_{i \in C} K_i\varphi$, i.e. every agent in $C$ knows $\varphi$ (if $C = \emptyset$ then $EK_C\varphi$ is equivalent to $\top$). Then we define by induction $EK_C^k\varphi$ for every natural number $k \in \mathbb{N}$:

$$ EK_C^0 \varphi \stackrel{\text{def}}{=} \varphi $$

and for all $k \ge 1$,

$$ EK_C^k \varphi \stackrel{\text{def}}{=} EK_C (EK_C^{k-1} \varphi). $$

We define for all natural numbers $n \in \mathbb{N}$, $MK_C^n\varphi$ as an abbreviation of $\bigwedge_{1 \le k \le n} EK_C^k\varphi$. $MK_C^n\varphi$ expresses $C$'s mutual knowledge that $\varphi$ up to $n$ iterations, i.e. everyone in $C$ knows $\varphi$, everyone in $C$ knows that everyone in $C$ knows $\varphi$, and so on until level $n$.

Finally, $\langle \delta_C \rangle \varphi$ abbreviates $\neg [\delta_C] \neg \varphi$, $\diamond \varphi$ abbreviates $\neg \Box \neg \varphi$ and $\hat{K}_i \varphi$ abbreviates $\neg K_i \neg \varphi$. $\diamond \varphi$ means “$\varphi$ is possibly true”. Therefore $\langle \delta_C \rangle \varphi$ reads “coalition $C$ chooses the joint action $\delta_C$ and $\varphi$ holds”, and $\langle \delta_C \rangle \top$ simply reads “coalition $C$ chooses the joint action $\delta_C$”.

The operator $\diamond$ and the operators $\langle \delta_C \rangle$ can be combined in order to express what a coalition of agents can do. In particular, $\diamond \langle \delta_C \rangle \top$ has to be read “coalition $C$ can choose the joint action $\delta_C$”. For the individual case, $\diamond \langle i:a \rangle \top$ has to be read “agent $i$ can choose action $a$” or also “action $a$ is in the strategy set (action repertoire) of agent $i$”. Furthermore, $\diamond \langle \delta \rangle \top$ is read “coalition $Agt$ can choose the joint action (strategy profile) $\delta$” or also “$\delta$ is a strategy profile of the current game”.

## 2.2. Semantics

In this subsection, we introduce a Kripke-style possible world semantics of our logic MLEG.

**Definition 1 (MLEG-frames).** MLEG-frames are tuples $F = (W, \sim, R, E, \preceq)$ where:
* W is a nonempty set of possible worlds or states;

* ~ is an equivalence relation on W;

* R is a collection of total functions $R_C : W \to \Delta_C$ one for every coalition $C \in 2^{Agt*}$, mapping every world in W to a joint action of the coalition such that:

C1 $\delta_C = R_C(w)$ if and only if for every $i \in C$, $\delta_i = R_i(w)$,<fnref n="2" />

C2 if for every $i \in Agt$ there is $v_i$ such that $w \sim v_i$ and $\delta_i = R_i(v_i)$ then there is a $v$ such that $w \sim v$ and $\delta = R_{Agt}(v)$;

* $E : Agt \to 2^{W \times W}$ maps every agent $i$ to an equivalence relation $E_i$ on W such that:

C3 if $w E_i v$, then $i:a = R_i(w)$ if and only if $i:a = R_i(v)$,

C4 if $w E_i v$ then $w \sim v$;

* $\leq: Agt \to 2^{W \times W}$ maps every agent $i$ to a reflexive, transitive relation $\leq_i$ on W such that:

C5 if $w \leq_i v$ then $w \sim v$,

C6 if $w \sim v$ and $w \sim u$ then $v \leq_i u$ or $u \leq_i v$.

$\delta_C = R_C(w)$ means that coalition $C$ performs the joint action $\delta_C$ at world $w$.

If $w \sim v$ then $w$ and $v$ correspond to alternative strategy profiles of the same game. For short, we say that $v$ is alternative to $w$. Given a world $w$, we use the notation $\sim(w) = \{v | w \sim v\}$ to denote the equivalence class made up of those worlds corresponding to alternative strategy profiles of the game of which $w$ is one of the strategy profile. Consider e.g. $Agt = \{1, 2\}$ and $Act = \{c, d, skip\}$. In the frame in Figure 1 we have $w_1 \sim w_2$. This means that the joint action performed at $w_1$ (viz. $\langle 1:c, 1:d \rangle$) and the one performed at $w_2$ (viz. $\langle 1:c, 1:d \rangle$) are alternative strategy profiles of the same game defined by the equivalence class $\sim(w_1) = \{w_1, w_2, w_3, w_4\}$.

For every $C \subseteq Agt$, if there exists $v \in \sim(w)$ such that $C$ performs $\delta_C$ at $v$ then we say that $\delta_C$ is possible at $w$ (or $\delta_C$ can be performed at $w$).

$w E_i v$ means that, for agent $i$, world $v$ is (epistemically) possible at $w$, whilst $w \leq_i v$ means that for agent $i$, world $v$ is at least as good as world $w$. We write $w =_i v$ iff $w \leq_i v$ and $v \leq_i w$, and $w <_i v$ iff $w \leq_i v$ and not $v \leq_i w$.

Let us discuss the semantic constraints in Definition 1.

According to Constraint **C1**, at world $w$ coalition $C$ chooses the joint action $\delta_C$ if and only if, every agent $i$ in $C$ chooses the action $\delta_i$ at $w$. In other words, a certain joint action is performed by a coalition if and only if every agent in the coalition does his part of the joint action. According to the Constraint **C2**, if every individual action in a joint action $\delta$ is possible at world $w$, then their simultaneous occurrence is also possible at world $w$.

Constraint **C3** just says that an agent knows what he has decided to do. This is a standard assumption in interactive epistemology and epistemic analysis of games (see [3] for instance).

<footnote n="2">²Note that for notational convenience we write $R_i$ instead of $R_{\{i\}}$.</footnote>
**Figure 1.** The equivalence class {$w_1, w_2, w_3, w_4$} represents the Prisoner's Dilemma game [15] between two players 1 and 2 (action $c$ stands for 'cooperate' and action $d$ stands for 'defect'). Thick ellipses are epistemic relations for 1, thin ellipses are epistemic relations for 2 (both 1 and 2 are uncertain about the other's action).

$$ \begin{array}{ccccc} w_2 & <_1 & w_4 & <_1 & w_1 <_1 w_3 \\ w_3 & <_2 & w_4 & <_2 & w_1 <_2 w_2 \end{array} $$

<figure><img src="image_2.png" /></figure>

We suppose complete information about the specification of the game, including the players' strategy sets (or action repertoires) and the players' preference ordering over strategy profiles. This assumption is formally expressed by the Constraint **C4**: if world $v$ is epistemically possible for agent $i$ at $w$, then $w$ and $v$ correspond to alternative strategy profiles of the same game. Complete information about the structure of the game is a standard assumption in game theory. In Section 5, this assumption will be relaxed in order to deal with realistic situations in which an agent might be uncertain about his own utility and other agents' utilities associated to a certain strategy profile, as well as about his own action repertoire and other agents' action repertoires.

Finally, we have two constraints over the relations $\preceq_i$. We suppose that a world $v$ is for agent $i$ at least as good as $w$ only if $v$ is a world which is possible at $w$, i.e. only if $v$ and $w$ correspond to alternative strategy profiles of the same game (Constraint **C5**). Furthermore, we suppose that every agent has a complete preference ordering over the strategy profiles of the current game (Constraint **C6**).

**REMARK.** Note that in the case of complete information (Constraint **C4**) the relation $\sim$ is superfluous because all other relations are included into $\sim$ (Constraints **C5** and **C6**). So in this case we can suppose $\sim$ to be the universal relation $W \times W$ and $\square$ to be the well-known universal modality.<fnref n="3" /> We decided to introduce the relation $\sim$ in this part of the paper in order to be able to generalize the definition of model in the case of imcomplete information (see Section 5). In fact, in the case of games of imcomplete information, a player can imagine alternative games and there is no one-to-one correspondence between models and games (i.e. every model does not necessarily correspond to a unique strategic game). Therefore, the relation $\sim$ can no longer be supposed to be the universal relation.

**Definition 2 (MLEG-models).** *MLEG-models are couples* $F = \langle F, \pi \rangle$ *where:*

<footnote n="3">³ The universal modality has been used since the dawning of modal logic (it is just a plain old S5 operator [16]). More recently, it has been used in several modal logic analysis of preferences and games (see, e.g., [14,17,18]).</footnote>
* F is a *MLEG*-frame;

* $\pi : \mathit{Atm} \to 2^W$ is a valuation function.

The truth conditions for Boolean operators and for operators $[\delta_C]$, $\square$, $K_i$ and $[\mathit{good}]_i$ are:

* $M, w \models p$ iff $w \in \pi(p)$;

* $M, w \models \neg \varphi$ iff not $M, w \models \varphi$;

* $M, w \models \varphi \lor \psi$ iff $M, w \models \varphi$ or $M, w \models \psi$;

* $M, w \models [\delta_C] \varphi$ iff if $R_C(w) = \delta_C$ then $M, w \models \varphi$;

* $M, w \models \Box \varphi$ iff $M, v \models \varphi$ for all $v$ such that $w \sim v$;

* $M, w \models K_i \varphi$ iff $M, v \models \varphi$ for all $v$ such that $w E_i v$;

* $M, w \models [\mathit{good}]_i \varphi$ iff $M, v \models \varphi$ for all $v$ such that $w \preceq_i v$.

A formula $\varphi$ is true in an *MLEG*-model $M$ iff $M, w \models \varphi$ for every world $w$ in $M$. A formula $\varphi$ is *MLEG*-valid (noted $|\models \varphi$) iff $\varphi$ is true in all *MLEG*-models. A formula $\varphi$ is *MLEG*-satisfiable iff $\neg \varphi$ is not *MLEG*-valid.

## 2.3. Axiomatization and complexity results

We call *MLEG* the logic that is axiomatized by the principles given in Figure 2.

Note that the principles of modal logic S5 for the operator $\square$ are: the four axiom schemas (K) ($\Box \varphi \wedge \Box (\varphi \to \psi)$) $\to$ $\Box \psi$, (T) $\Box \varphi \to \varphi$, (4) $\Box \varphi \to \Box \Box \varphi$, (B) $\varphi \to \Box \Diamond \varphi$, and the rule of inference (Necessitation) $\frac{\varphi}{\Box \varphi}$. The principles of modal logic S5 for the operators $K_i$ are: the four axiom schemas (K) ($K_i \varphi \wedge K_i (\varphi \to \psi)$) $\to$ $K_i \psi$, (T) $K_i \varphi \to \varphi$, (4) $K_i \varphi \to K_i K_i \varphi$, (B) $\varphi \to K_i \hat{K}_i \varphi$, and the rule of inference (Necessitation) $\frac{\varphi}{\hat{K}_i \varphi}$. The principles of modal logic S4 for the operators $[\mathit{good}]_i$ are: the three axiom schemas (K) ($[\mathit{good}]_i \varphi \wedge [\mathit{good}]_i (\varphi \to \psi)$) $\to$ $[\mathit{good}]_i \psi$, (T) $[\mathit{good}]_i \varphi \to \varphi$, (4) $[\mathit{good}]_i \varphi \to [\mathit{good}]_i [\mathit{good}]_i \varphi$, and the rule of inference (Necessitation) $\frac{\varphi}{[\mathit{good}]_i \varphi}$.

Note also that Axiom **Indep** is the *MLEG* counterpart of the so-called *axiom of independence of agents* of STIT logic (the logic of *Seeing to it that*) [19]. This axiom enables to express the basic game theoretic assumption that the set of strategy profiles of a game in strategic form is the cartesian product of the sets of individual actions for the agents in *Agt*.

We write $\vdash_{\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}} \varphi$ if $\varphi$ is a theorem of *MLEG*, that is, if $\varphi$ can be deduced by applying the axioms and the rules of inference of the logic *MLEG*.

As the following theorem 1 highlights, we can prove that the logic *MLEG* is sound and complete with respect to the class of *MLEG*-models.

**Theorem 1.** *MLEG* is determined by the class of *MLEG*-models.
<table><caption>**Figure 2.** Axiomatization of *MLEG*</caption>
  <tr>
    <td>(CPL)</td>
    <td>All principles of classical propositional logic</td>
  </tr>
  <tr>
    <td>(S5<sub>□</sub>)</td>
    <td>All principles of modal logic S5 for □</td>
  </tr>
  <tr>
    <td>(S5<sub>K<sub>i</sub></sub>)</td>
    <td>All principles of modal logic S5 for every K<sub>i</sub></td>
  </tr>
  <tr>
    <td>(S4<sub>[good]<sub>i</sub></sub>)</td>
    <td>All principles of modal logic S4 for every [good]<sub>i</sub></td>
  </tr>
  <tr>
    <td>(Def<sub>[δ<sub>C</sub>]</sub>)</td>
    <td>[δ<sub>C</sub>] φ ↔ (⟨δ<sub>C</sub>⟩<sup>T</sup> → φ)</td>
  </tr>
  <tr>
    <td>(JointAct)</td>
    <td>⟨δ<sub>C</sub>⟩<sup>T</sup> ↔ ⋀<sub>i∈C</sub> ⟨δ<sub>i</sub>⟩<sup>T</sup></td>
  </tr>
  <tr>
    <td>(Active)</td>
    <td>∇<sub>δ<sub>C</sub>∈Δ<sub>C</sub></sub> ⟨δ<sub>C</sub>⟩<sup>T</sup></td>
  </tr>
  <tr>
    <td>(Single)</td>
    <td>⟨δ<sub>C</sub>⟩<sup>T</sup> → [δ'<sub>C</sub>] ⊥ if δ<sub>C</sub> ≠ δ'<sub>C</sub></td>
  </tr>
  <tr>
    <td>(Indep)</td>
    <td>(Λ<sub>i∈A<sub>gt</sub></sub> ♦⟨δ<sub>i</sub>⟩<sup>T</sup>) → ♦⟨δ⟩<sup>T</sup></td>
  </tr>
  <tr>
    <td>(Aware)</td>
    <td>⟨i:a⟩<sup>T</sup> → K<sub>i</sub>⟨i:a⟩<sup>T</sup></td>
  </tr>
  <tr>
    <td>(Incl<sub>[good]<sub>i</sub>,□</sub>)</td>
    <td>□φ → [good]<sub>i</sub> φ</td>
  </tr>
  <tr>
    <td>(PrefConnect)</td>
    <td>(◇φ ∧ ◇ψ) → (◇(φ ∧ ⟨good⟩<sub>i</sub>ψ) ∨ ◇(ψ ∧ ⟨good⟩<sub>i</sub>φ))</td>
  </tr>
  <tr>
    <td>(CompleteInfo)</td>
    <td>□φ → K<sub>i</sub>φ</td>
  </tr>
  <tr>
    <td>(ModusPonens)</td>
    <td>φ, ϕ → ψ<br>ψ</td>
  </tr>
</table>

Moreover we can prove a result about complexity of the satisfiability problem of the logic *MLEG*,
that is, the complexity of the problem of deciding whether a given *MLEG* formula *φ* is *MLEG*-
satisfiable or not. This question is highly related to automated reasoning. Here, we give a lower-bound
and upper-bound for the complexity of the satisfiability problem (for more information about the com-
plexity theory, the reader may refer to [20]):

**Theorem 2.** If the number of agents is greater of equal to 2, the satisfiability problem of *MLEG* is EXPTIME-hard and in NEXPTIME.

We conjecture that the satisfiability problem of *MLEG* is EXPTIME-complete. Indeed, we think that
this can proved by the argument used for proving that the satisfiability problem of S5₂ with common
knowledge [21] or propositional dynamic logic (PDL) [22] is EXPTIME-complete.

2.4. A variant of *MLEG* with joint determinism

We present here a variant of *MLEG* where models have an additional constraint of determinism
for the joint actions of all agents: different worlds in an equivalence class ~ (*w*) correspond to the
occurrences of different strategy profiles:

**CD** if *w* ~ *v* and *δ* = *R*<sub>Agt</sub>(*w*) and *δ* = *R*<sub>Agt</sub>(*v*), then *w* = *v*;
A MLEG-model satisfying the constraint CD is called a MLEGdet-model.

The axiom corresponding to the Constraint CD is:

$$ (\mathbf{JointDet}) \qquad (\langle\delta\rangle\top \wedge \varphi) \rightarrow \Box(\langle\delta\rangle\top \rightarrow \varphi) $$

We call MLEGdet the logic that is axiomatized by the principles given in Figure 2 plus axiom Joint-Det.

**Theorem 3.** MLEGdet is determined by the class of MLEGdet-models.

Although the Constraint CD excludes pure uncertainty about uncertainty (i.e. cases where the same profile is played at two states on the basis of different information), it is interesting because it allows to establish a connection between our logical framework and Coalition Logic (CL) [23,24], where it is assumed that if every agent in Agt opts for an action the next state of the world is uniquely determined. As shown in [25], the logic MLEGdet extended by the operator next of linear temporal logic (LTL) embeds Coalition Logic (CL) [23,24]. In particular, if we extend MLEGdet by the temporal operator X (where X_φ means “φ will be true in the next state”) CL cooperation modalities of the form [C] can be reconstructed in our logic MLEG as follows.

$$ tr([C] \varphi) = \bigvee_{\delta \in \Delta} (\Diamond\langle\delta_C\rangle\top \wedge \Box(\langle\delta_C\rangle\top \rightarrow X_\varphi)) $$

That is, the CL expression “coalition C can enforce an outcome state satisfying φ” (noted [C] φ) is translated in our logic as “there exists a joint action δ_C of the agents in C such that the agents in C can perform δ_C, and necessarily if the agents in C perform δ_C then φ will be true in the next state, no matter what the agents outside C do”.

**REMARK.** It is worth noting that, while MLEGdet embeds Coalition Logic, the basic logic MLEG embeds Chellas’ STIT logic with agents and groups [26], under the hypothesis that the number of agents’ choices is bounded (see [27] for more details). In fact, differently from Coalition Logic, in STIT joint actions of all agents are not necessarily deterministic. STIT logic has formulas of the form [C cstit:φ] that are read “group C sees to it that φ”. The translation of STIT modalities of the form [C cstit:] into MLEG would be the following:

$$ tr([C \ cstit: \varphi]) = \bigvee_{\delta \in \Delta} (\langle\delta_C\rangle\top \wedge \Box(\langle\delta_C\rangle\top \rightarrow \varphi)) $$

That is, the STIT expression “group C sees to it that φ” is translated into DLA as “there exists a joint action δ_C of the agents in C such that the agents in C perform δ_C, and necessarily if the agents in C perform δ_C then φ will be true, no matter what the agents outside C do”.

The constraint of joint determinism CD is also useful for complexity reasons. Indeed, if we add CD to our logic, the complexity of the satisfiability problem drops to NP.

**Theorem 4.** The satisfiability problem of MLEGdet is NP-complete.

### 3. A logical account of epistemic games

This section is devoted to the analysis in the modal logic MLEG of the epistemic aspects of strategic games. We first consider the basic game-theoretic concepts of best response and Nash equilibrium, and their relationships with the notion of epistemic rationality assumed in classical game theory. Finally, we provide an analysis of Iterated Deletion of Strictly Dominated Strategies (IDSDS).
### 3.1. Best Response and Nash Equilibrium

The modal operators $[good]_i$ and $\square$ enable to capture in $\mathcal{MLEG}$ a notion of comparative goodness over formulas of the kind “$\varphi$ is for agent $i$ at least as good as $\psi$”, noted $\psi \le_i \varphi$:

$$ \psi \le_i \varphi \stackrel{\text{def}}{=} \square (\psi \to \langle \text{good} \rangle_i \varphi). $$

According to the previous definition, $\varphi$ is for agent $i$ at least as good as $\psi$ if and only if, for every world $v$ corresponding to a strategy profile of the current game in which $\psi$ is true, there is a world $u$ corresponding to a strategy profile of the current game in which $\varphi$ is true and which is for agent $i$ at least as good as world $v$. We can prove that $\psi \le_i \varphi$ is a total preorder. Indeed, the formulas $\psi \le_i \psi$ (reflexivity), $(\varphi_1 \le_i \varphi_2) \wedge (\varphi_2 \le_i \varphi_3) \to (\varphi_1 \le_i \varphi_3)$ (transitivity) and $(\varphi_1 \le_i \varphi_2) \vee (\varphi_2 \le_i \varphi_1)$ (connectedness, also called completeness) are valid in $\mathcal{MLEG}$. We define the corresponding strict ordering over formulas:

$$ \psi <_i \varphi \stackrel{\text{def}}{=} (\psi \le_i \varphi) \wedge \neg(\varphi \le_i \psi). $$

Formula $\psi <_i \varphi$ has to read “$\varphi$ is for agent $i$ strictly better than $\psi$”. Finally, we define a notion of comparative goodness over strategy profiles and the corresponding strict ordering over strategy profiles:

$$ \delta \le_i \delta' \stackrel{\text{def}}{=} \langle \delta \rangle \top \le_i \langle \delta' \rangle \top \text{ and } \delta <_i \delta' \stackrel{\text{def}}{=} (\delta \le_i \delta') \wedge \neg(\delta' \le_i \delta). $$

Formula $\delta \le_i \delta'$ has to be read “strategy profile $\delta'$ is for agent $i$ at least as good as strategy profile $\delta$” and formula $\delta <_i \delta'$ has to be read “strategy profile $\delta'$ is for agent $i$ strictly better than strategy profile $\delta$”.

Some basic concepts of game theory can be expressed in $\mathcal{MLEG}$ in terms of comparative goodness. We first consider best response. Agent $i$'s action $a$ is said to be a best response to the other agents' joint action $\delta_{-i}$, noted $\text{BR}(i:a, \delta_{-i})$, if and only if $i$ cannot improve his utility by deciding to do something different from $a$ while the others choose the joint action $\delta_{-i}$, that is:

$$ \text{BR}(i:a, \delta_{-i}) \stackrel{\text{def}}{=} \bigwedge_{b \in \text{Act}} ((i:b, \delta_{-i}) \le_i (i:a, \delta_{-i})). $$

**REMARK.** Note that the definition of best response $\text{BR}(i:a, \delta_{-i})$ given above only works for a complete preference relation $\le_i$. To see why, suppose that $\text{Agt} = \{i, j\}$ and $\text{Act} = \{a, b\}$, and consider the model $\mathcal{M} = \langle W, \sim, R, E, \leq, \pi \rangle$ such that $W = \{w_1, w_2\}$, $\sim = W \times W$, $R_{\text{Agt}}(w_1) = \langle i:a, j:a \rangle$, $R_{\text{Agt}}(w_2) = \langle i:b, j:a \rangle$ and $E_i = E_j = \leq_i = \leq_j = \{(w_1, w_1), (w_2, w_2)\}$. Here the relation $\leq_i$ does not satisfy the constraint **C6** (i.e. $\leq_i$ is not complete). Intuitively, $\text{BR}(i:a, j:a)$ should be true at any world of $\mathcal{M}$ because if $i$ plays $a$ while $j$ plays $a$, he does not improve his utility by playing $b$. Nevertheless, as $((\langle i:b \rangle \top \wedge \langle j:a \rangle \top) \le_i ((\langle i:a \rangle \top \wedge \langle j:a \rangle \top))$ is false at any world of $\mathcal{M}$, we have that $\text{BR}(i:a, j:a)$ is also false at every world of $\mathcal{M}$.

Given a certain strategic game, the strategy profile (or joint action) $\delta$ is said to be a *Nash equilibrium* if and only if for every agent $i \in \text{Agt}$, $i$'s action $\delta_i$ is a best response to the other agents' joint action $\delta_{-i}$:

$$ \text{Nash}(\delta) \stackrel{\text{def}}{=} \bigwedge_{i \in \text{Agt}} \text{BR}(\delta_i, \delta_{-i}). $$
From Axiom **CompleteInfo**, S5 for □, Axioms K and T for K<sub>i</sub> the five MLEG-theorems in Proposition 1 are provable. They express complete information about the players' preferences ordering over strategy profiles, complete information about the existence of a Nash equilibrium, and complete information about the players' repertoires. Surprisingly formulas of Proposition 1 are kinds of introspection properties, but they are provable without axioms of positive and negative introspections for knowledge:
(4) K<sub>i</sub>φ → K<sub>i</sub>K<sub>i</sub>φ or (5) ¬K<sub>i</sub>φ → K<sub>i</sub>¬K<sub>i</sub>φ.

**Lemma 1.** For all $i \in Agt$ and $n \in N$:

• $\vdash_{\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}} (\psi \leq_i \varphi) \leftrightarrow \mathrm{MK}_{Agt}^n (\psi \leq_i \varphi);$

• $\vdash_{\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}} (\psi <_i \varphi) \leftrightarrow \mathrm{MK}_{Agt}^n (\psi <_i \varphi);$

• $\vdash_{\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}} \mathrm{Nash}(\delta) \leftrightarrow \mathrm{MK}_{Agt}^n \mathrm{Nash}(\delta);$

• $\vdash_{\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}} \Diamond\langle\delta_i\rangle\top \leftrightarrow \mathrm{MK}_{Agt}^n\Diamond\langle\delta_i\rangle\top;$

• $\vdash_{\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}} \Box[\delta_i]\bot \leftrightarrow \mathrm{MK}_{Agt}^n\Box[\delta_i]\bot$

It has to be noted that weak preference operators [good]<sub>i</sub>, used here to define some basic concepts of game theory, have been studied before by [14,17] and by [18], where complete axiomatizations for different kinds of preference logics and for a combination of preference logic with epistemic logic are given. In [14,17] Liu proposed a complete modal logic of knowledge and preference extended by dynamic operators of knowledge update and preference upgrade in the style of dynamic epistemic logic (DEL). In [18] van Benthem et al. studied different variants of preference logic that allow to express different readings of *ceteris paribus* preferences [28]. They first present a basic modal logic of weak and strict preference which allows to express the “all other things being normal” reading of *ceteris paribus* preferences. Then they present a more general modal logic in which modal operators of weak and strict preference are relativized to sets of formulas representing conditions to be kept equal. They show that this logic allows to express the “all other things being equal” reading of *ceteris paribus* preferences and to characterize the notion of Nash equilibrium as a preference for a given strategy profile for a game, given that *others* keep the same strategy.<fnref n="4" /> One of the main contribution of our work is to propose a modal logic which integrates the notion of weak preference studied by Liu and van Benthem et al. with notions of action and knowledge, and which provides a suitable framework for a logical analysis of epistemic strategic games both with perfect information and with weaker forms of perfect information. The latter are the subject of the second part of the paper (Sections 5 and 6).

## 3.2. Epistemic rationality

The following MLEG formula characterizes a notion of rationality which is commonly supposed in the epistemic analysis of games (see, e.g., [4,7]):

$$ \bigwedge_{a,b \in Act} (\langle i:a \rangle \top \rightarrow \bigvee_{\delta \in \Delta} (\hat{K}_i \langle \delta_{-i} \rangle \top \wedge (\langle \delta_{-i}, i:b \rangle \leq_i \langle \delta_{-i}, i:a \rangle))) $$

<footnote n="4">⁴The normality reading of *ceteris paribus* preferences expresses preferences which hold under certain normal conditions, whereas the equality reading expresses preferences which hold when certain facts are kept constant.</footnote>
This means that an agent *i* is rational if and only if, if he chooses a particular action *a* then for every alternative action *b*, there exists a joint action $\delta_{-i}$ of the other agents that he considers possible such that, playing *a* while the others play $\delta_{-i}$ is for *i* at least as good as playing *b* while the others play $\delta_{-i}$. This means that epistemic rationality simply consists in not choosing a strategy that is strictly dominated within the agent's set of epistemic alternatives.

As in MLEG formula $\delta \leq_i \delta'$ and formula $K_i(\delta \leq_i \delta')$ are equivalent, the previous definition of rationality can be rewritten in the following equivalent form:

$$ \mathrm{Rat}_i \stackrel{\mathrm{def}}{=} \bigwedge_{a,b \in \mathrm{Act}} \left( \langle i:a \rangle \vdash \bigvee_{\delta \in \Delta} \left( \hat{K}_i \langle \delta_{-i} \rangle \vdash \bigwedge K_i (\langle \delta_{-i}, i:b \rangle \leq_i \langle \delta_{-i}, i:a \rangle) \right) \right). $$

**Theorem 5.** For all $i \in \mathrm{Agt}$:

(5a) $\vdash_{\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}} \mathrm{Rat}_i \leftrightarrow K_i \mathrm{Rat}_i$

(5b) $\vdash_{\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}} \neg \mathrm{Rat}_i \leftrightarrow K_i \neg \mathrm{Rat}_i$

Theorem 5 highlights that the concepts of rationality and irrationality are introspective. That is, an agent *i* is (resp. is not) epistemically rational if and only if he knows this. The syntactic proof of Theorem 5a given in the annex shows that it can be proved either by means of Axioms K, T, 4 and 5 for knowledge modal operators or by means of Axioms K, T and 5 for knowledge and a principle of introspection over preferences of the form $((\delta \leq_i \delta') \rightarrow K_i(\delta \leq_i \delta'))$. Theorem 5b is provable from Theorem 5a by means of Axioms T and 5 for knowledge.

The following theorem specifies some sufficient epistemic conditions for guaranteeing that the chosen strategy profile is a Nash equilibrium: if all agents are rational and every agent knows the choices of the other agents, then the selected strategy profile is a Nash equilibrium. This theorem has been stated for the first time by Aumann & Brandeburger [1,5].

**Theorem 6.** For all $\delta \in \Delta$:

$$ \vdash_{\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}} \left( \left( \bigwedge_{i \in \mathrm{Agt}} \mathrm{Rat}_i \right) \wedge \bigwedge_{i \in \mathrm{Agt}} K_i \langle \delta_{-i} \rangle \vdash \right) \rightarrow \mathrm{Nash}(\delta) $$

The syntactic proof of Theorem 6 in the annex at the end of the paper shows that it can be proved just by means of Axioms K and T for the epistemic modal operators. Axiom **CompleteInfo**, positive and negative introspection for knowledge ($K_i\varphi \rightarrow K_iK_i\varphi$ and $\neg K_i\varphi \rightarrow K_i\neg K_i\varphi$) are not needed for the proof.

### 3.3. Iterated deletion of strictly dominated strategies

A strategy *a* for agent *i* is a strictly dominated strategy, noted $\mathrm{SD}^{\leq 0}(i:a)$, if and only if, if *a* can be performed then there is another strategy *b* such that, no matter what joint action $\delta_{-i}$ the other agents choose, playing *b* is for *i* strictly better than playing *a*:

$$ \mathrm{SD}^{\leq 0}(i:a) \stackrel{\mathrm{def}}{=} \diamond \langle i:a \rangle \vdash \rightarrow \bigvee_{b \in \mathrm{Act}} \left( \diamond \langle i:b \rangle \vdash \bigwedge_{\delta \in \Delta} \left( \diamond \langle \delta_{-i} \rangle \vdash \rightarrow \left( \langle \delta_{-i}, i:a \rangle <_i \langle \delta_{-i}, i:b \rangle \right) \right) \right). $$
An example of strictly dominated strategy is cooperation in the Prisoner Dilemma (PD) game: whether ones opponent chooses to cooperate or defect, defection yields a higher payoff than cooperation. Therefore, a rational player will never play a dominated strategy. So when trying to predict the behavior of rational players, we can rule out all strictly dominated strategies. The so-called Iterated Deletion of Strictly Dominated Strategies (IDSDS) (or iterated strict dominance) [15] is a procedure that starts with the original game and, at each step, for every player $i$ removes from the game all $i$'s strictly dominated strategies, thereby generating a subgame of the original game, and that repeats this process again and again. IDSDS can be inductively characterized in our logic $\mathcal{MLEG}$ by defining a concept of strict dominance in the subgame of depth at most $n$, noted $\mathrm{SD}^{\le n}(i:a)$. For every $n \ge 1$:

$$ \mathrm{SD}^{\le n}(i:a) \stackrel{\mathrm{def}}{=} \neg \mathrm{SD}^{\le n-1}(i:a) \rightarrow \\ \bigvee_{b \in \mathrm{Act}} \left( \neg \mathrm{SD}^{\le n-1}(i:b) \wedge \bigwedge_{\delta \in \Delta} \left( \neg \mathrm{SD}^{\le n-1}(\delta_{-i}) \rightarrow (\langle \delta_{-i}, i:a \rangle <_i \langle \delta_{-i}, i:b \rangle) \right) \right). $$

where $\mathrm{SD}^{\le k}(\delta_C)$ is defined as follows

$$ \mathrm{SD}^{\le k}(\delta_C) \stackrel{\mathrm{def}}{=} \bigvee_{i \in C} \mathrm{SD}^{\le k}(\delta_i) $$

for every $k \ge 0$ and for every $\delta_C$. According to this definition, $a$ is a strictly dominated strategy for agent $i$ in a subgame of depth at most $n$, noted $\mathrm{SD}^{\le n}(i:a)$, if and only if, if $a$ is not strictly dominated for $i$ in all subgames of depth $k < n$ then there is another strategy $b$ such that $b$ is not strictly dominated for $i$ in all subgames of depth $k < n$ and, no matter what joint action $\delta_{-i}$ the other agents choose, if the elements in $\delta_{-i}$ are not dominated in all subgames of depth $k < n$ then playing $b$ is for $i$ strictly better than playing $a$. In other terms $\mathrm{SD}^{\le n}(i:a)$ means that strategy $i:a$ does not survive after $n$ rounds of IDSDS. We can prove by recurrence on $n$ that the length of the formula $\mathrm{SD}^{\le n}(\delta)$ is

$$ O(|Act||Agt|)^{2n+1}) $$

where $O(\cdot)$ is the “Big Oh Notation” [20], $|Act|$ is the number of action and $|Agt|$ is the number of agent and $n$ is the number of rounds of IDSDS. That is, the length of the formula $\mathrm{SD}^{\le n}(\delta)$ is exponential in $n$. In Section 4, we are going to extend the language in order to capture the concept of IDSDS with a compact formula.

As the following $\mathcal{MLEG}$-theorems highlight, the truth of $\mathrm{SD}^{\le n}(i:a)$ depends of the game but does not depend on the point where the formula is checked.

**Proposition 1.** For all $a \in \mathrm{Act}$, for all $n \ge 0$, we have:

* $\vdash_{\mathcal{MLEG}} \mathrm{SD}^{\le n}(i:a) \leftrightarrow \Box \mathrm{SD}^{\le n}(i:a);$

* $\vdash_{\mathcal{MLEG}} \neg \mathrm{SD}^{\le n}(i:a) \leftrightarrow \Box \neg \mathrm{SD}^{\le n}(i:a).$

The following Theorem 7 is the qualitative version of a probabilistic-based result of Stalnaker [29] who has been the first to use probabilistic Kripke structures in order to characterize the IDSDS procedure in terms of common knowledge of rationality (see [3,30] for some recent discussion of Stalnaker's
<table><caption>**Table 1.** Some sufficient conditions for Theorems 5, 6, 7</caption><thead><tr><th>Assumptions about knowledge operators</th><th>Assumptions about information over game structure</th><th>Result</th></tr></thead><tbody><tr><td>KT45</td><td>none</td><td>Theorem 5</td></tr><tr><td>KT5</td><td>interspection over preferences: ($\delta \le_i \delta'$) &rarr; $K_i(\delta \le_i \delta')$</td><td>Theorem 5</td></tr><tr><td>KT</td><td>none</td><td>Theorem 6</td></tr><tr><td>KT</td><td>complete information about players preference ordering over strategy profiles: ($\delta \le_j \delta'$) &rarr; $K_i(\delta \le_j \delta')$<br/>($\delta <_j \delta'$) &rarr; $K_i(\delta <_j \delta')$<br/>complete information about players' strategy sets: $\Diamond\langle j:a\rangle \supset \rightarrow K_i\Diamond\langle j:a\rangle \supset$<br/>$\Box[j:a] \perp \rightarrow K_i\Box[j:a] \perp$</td><td>Theorem 7</td></tr></tbody></table>

results). A similar result was also proved, with differing degrees of formality, by Bernheim [31], Pearce [32], Brandenburger & Dekel [33], and Tan & Werlang [34]. Note that Stalnaker's proof is purely semantic. According to the Theorem 7, if there is mutual knowledge of rationality among the players to n levels and the agents play the strategy profile $\delta$ then, for every agent $i$, $\delta_i$ survives IDSDS until the subgame of depth $n+1$.

**Theorem 7.** For all positive integer $n$, for all $\delta \in \Delta$, we have:

$$ \vdash_{ML\Sigma\mathcal{E}\mathcal{G}} \left( \left( \left( \bigwedge_{i \in A_{gt}} \mathrm{MK}_{A_{gt}}^n \bigwedge \mathrm{Rat}_i \right) \wedge \langle \delta \rangle \top \right) \rightarrow \neg \mathrm{SD}^{\le n}(\delta) \right) $$

(note that $\neg \mathrm{SD}^{\le n}(\delta)$ is just the abbreviation of $\bigwedge_{i \in A_{gt}} \neg \mathrm{SD}^{\le k}(\delta_i)$).

The syntactic proof of Theorem 7 given in the annex shows that, although Axiom **CompleteInfo**, positive and negative introspection for knowledge ($K_i\varphi \rightarrow K_i K_i\varphi$ and $\neg K_i\varphi \rightarrow K_i \neg K_i\varphi$) are not needed for the proof, we need to assume that a player has complete information about the players' strategy sets as well as about the players' preference ordering over strategy profiles. Table 1 summarizes the sufficient conditions for the syntactic proof of Theorem 7 together with the sufficient conditions for the syntactic proofs of Theorems 5 and 6. It highlights an interesting aspect of our syntactic analysis of games based on modal logic: the fact that we can easily verify whether certain assumptions about knowledge and information over the game structure are indeed necessary to prove results concerning the epistemic foundations of game theory.

It has to be noted that Theorem 7 provides only one direction of the characterization result for the IDSDS procedure as formulated in the game-theoretic literature, according to which IDSDS is fully
characterized by the epistemic condition of common knowledge of rationality between the players (see, e.g., [3,29,30]).

The other direction states approximately that, for every strategic game, if $\delta$ is the strategy profile that is chosen and that survives to the infinite procedure IDSDS, then there is (a state in) an epistemic model for that game in which the profile $\delta$ is played and the players have common knowledge of rationality.

This statement is formally expressed by the following theorem (a similar result is proved in [3]).

**Theorem 8.** Consider an arbitrary *MLEG*-model $M = \langle W, \sim, R, E, \leq, \pi \rangle$, a world $w$ in $M$ and $\delta \in \Delta$ such that for all positive integers $n$ we have $M, w \models \langle \delta \rangle \top \wedge \neg \mathrm{SD}^{\leq n}(\delta)$. Then, there is a model $M' = \langle W, \sim, R, E', \leq, \pi \rangle$ such that for all positive integers $n$ we have $M', w \models \mathrm{MK}_{Agt}^n \wedge_{i \in Agt} \mathrm{Rat}_i$.

The idea is that, for every strategic game, if $\delta$ is the strategy profile of this game which is chosen and that survives after $n$ rounds of the procedure IDSDS, for all positive integers $n$, then it is possible to find an “epistemic configuration” for the players which satisfies common knowledge of rationality between the players. In other words, if $\delta$ is a strategy profile of a given strategic game that survives after all rounds of the procedure IDSDS then it is always possible to justify the choice of $\delta$ by the fact that the players have common knowledge of rationality.

Note that Theorem 8 is different from stating that the logic *MLEG* cannot prove the negation of conjunctions of this type: a given profile $\delta$ is played, survives after $n$ rounds of IDSDS and rationality of players is common knowledge up to degree $n$. By the completeness of *MLEG* this just means that the conjunction $(\mathrm{MK}_{Agt}^n \wedge_{i \in Agt} \mathrm{Rat}_i) \wedge \langle \delta \rangle \top \wedge \neg \mathrm{SD}^{\leq n}(\delta)$ is consistent in *MLEG*. Indeed, the latter trivially holds, as we can always exhibit the trivial model $M = \langle W, \sim, R, E, \leq, \pi \rangle$ such that $W = \{w\}$, $R_{Agt}(w) = \delta$ and $E'_i(w) = \{w\}$ for every $i \in Agt$, and in which $M, w \models (\mathrm{MK}_{Agt}^n \wedge_{i \in Agt} \mathrm{Rat}_i) \wedge \langle \delta \rangle \top \wedge \neg \mathrm{SD}^{\leq n}(\delta)$ holds for every $n$.

### 3.4. Discussion: related works on modal logic analysis of epistemic games under complete information

Although several modal logics of games in strategic forms have been proposed in recent times (see, e.g., [25,35]), few modal logics of epistemic games under complete information exist. Among them we should mention [3,8,9,36]. Let us compare our modal logic *MLEG* with some of these alternative approaches.

De Bruin [8] has developed a logical framework which enables to reason about the epistemic aspects of strategic games and of extensive games. His system deals with several game-theoretic concepts like the concepts of knowledge, rationality, Nash equilibrium, iterated strict dominance, backward induction. Nevertheless, de Bruin's approach differs from ours in several respects. First of all, our logical approach to epistemic games is *minimalistic* since it relies on few primitive concepts: knowledge, action, historical necessity and preference. All other notions such Nash equilibrium, rationality, iterated strict dominance are defined by means of these four primitive concepts. On the contrary, in de Bruin's logic all those notions are atomic propositions managed by a *ad hoc* axiomatization (see, e.g., [8, pp. 61,65] where special propositions for rationality and iterated strict dominance are introduced). Secondly, we provide a semantics and a complete axiomatics for our logic of epistemic games. De Bruin's approach is purely syntactic: no model-theoretic analysis of games is proposed nor completeness result for the proposed
logic is given. Finally, de Bruin does not provide any complexity results about his logic while we
provide complexity results for the satisfiability problem of our logic.

In [36] van der Hoek & Pauly investigate how modal logics can be used to describe and reason about games. They show how epistemic logic can be combined with constructions expressing agents' preferences over strategy profiles in order to study the epistemic aspects of strategic games and to define a concept of rationality similar to the one discussed in Section 3.2. Although van der Hoek & Pauly discuss the combination of action, preference and epistemics for the analysis of epistemic games they do not provide a unified modal logic framework combining operators for knowledge, for preference and for action with a complete axiomatization and with a study of its computational properties like decidability and complexity. The latter is one of the main contribution of our work.

Roy [9] has recently proposed a modal logic integrating preference, knowledge and intention. In his approach every world in a model is associated to a nominal which directly refers to a strategy profile in a strategic game. This approach is however limited in expressing formally the structure of a strategic game. In particular, in Roy's logic there is no principle like the *MLEG Axiom Indep* explaining how possible actions $\delta_i$ of individual agents are combined to form a strategy profile $\delta$ of the current game. Another limitation of Roy's approach is that it does not allow to express the concept of (weak) rationality that we have been able to define in Section 3.2 (see [9, pp. 101]). As discussed in the previous sections this is a crucial concept in interactive epistemology since it is used for giving epistemic justifications of several solution concepts like Nash equilibrium and IDSDS (see Theorems 6 and 7).

Bonanno [3] integrates modal operators for belief, common belief with constructions expressing agents' preferences over individual actions and strategy profiles, and applies them to the semantic characterization of solution concepts like Iterated Deletion of Strictly Dominated Strategies (IDSDS) and Iterated Deletion of Inferior Profiles (IDIP). As in [9], in Bonanno's logic every world in a model corresponds to a strategy profile of the current game. Although this logic allows to express the concept of weak rationality, it is not sufficiently general to enable to express in the object language solution concepts like Nash equilibrium and IDSDS (note that the latter is defined by Bonanno only in the metalanguage).

It is to be noted that, differently from *MLEG*, most modal logics of epistemic games in strategic form (including Roy's logic and Bonanno's logic) postulate a one-to-one correspondence between models and games (i.e. every model of the logic corresponds to a unique strategic game, and worlds in the model are all strategy profiles of this game). Such an assumption is quite restrictive since it prevents from analyzing in the logic games with incomplete information about the game structure in which an agent can imagine alternative games. We will show in Section 5 that this is something we can do in our logical framework by removing Axiom **CompleteInfo** from *MLEG*.

**4. Game transformation**

We provide in this section an alternative and more compact characterization of the procedure IDSDS in our logic *MLEG*. To this aim, we introduce special events whose effect is to transform the current game by removing certain strategies from it. In particular, these special events can used to delete a strictly dominated strategy from the current game. These special events are similar to the notion of announcement in Dynamic Epistemic Logic (DEL) [10–12].
$\mathcal{L}_{GT}$ is the set of game transformation formulas and is defined by the following rule:

$$ \chi ::= \Box \psi \rightarrow [i:a] \perp | \chi \wedge \chi $$

where $\psi \in \mathcal{L}_{MLEG}$, $i \in Agt$ and $a \in Act$. Thus, game transformation formulas are of the form 'if property $\psi$ necessarily holds in the current game, then action $a$ should not be performed by agent $i$'.

$GT$ is the set of game transformation events and is defined as $GT = \{\chi! | \chi \in \mathcal{L}_{GT}\}$.

We extend the MLEG language with dynamic operators of the form $[\chi!]\varphi$ with $\chi! \in GT$. The formula $[\chi!]\varphi$ has to be read ' $\varphi$ holds, after the occurrence of the game transformation event $\chi!$'. We call MLEG$^{GT}$ the extended logic. The truth condition for $[\chi!]\varphi$ is:

$$ M, w \models [\chi!]\varphi \text{ iff if } M, w \models \chi \text{ then } M^{\chi}, w \models \varphi $$

with $M^{\chi} = \langle W^{\chi}, \sim^{\chi}, R^{\chi}, E^{\chi}, \leq^{\chi}, \pi^{\chi} \rangle$ and:

$$ W^{\chi} = \{w \mid w \in W \text{ and } M, w \models \chi\}; $$

$$ \sim^{\chi} = \sim \cap (W^{\chi} \times W^{\chi}); $$

$$ \text{for every } C \in 2^{Agt*}, R_C^{\chi} = R_C|_{W^{\chi}}; $$

$$ \text{for every } i \in Agt, E_i^{\chi} = E_i \cap (W^{\chi} \times W^{\chi}); $$

$$ \text{for every } i \in Agt, \leq_i^{\chi} = \leq_i \cap (W^{\chi} \times W^{\chi}); $$

$$ \text{for every } p \in Atm, \pi^{\chi}(p) = \pi(p) \cap W^{\chi}. $$

Thus, an event $\chi!$ removes from the model $M$ all worlds in which $\chi$ is false. Every epistemic relations $E_i$, every preference orderings $\leq_i$, every function $R_C$, and the valuation $\pi$ are restricted to the worlds in which $\chi$ is true.

In the resulting structure $M^{\chi}$, the relations $\sim^{\chi}, R_{\delta C}^{\chi}, E_i^{\chi}, \leq_i^{\chi}$ verify the constraints of Definition 1 because of the syntactic restriction $\chi \in \mathcal{L}_{GT}$. This result is summed up in the following theorem:

**Theorem 9.** Let $\chi \in \mathcal{L}_{GT}$. If $M$ is a MLEG model then $M^{\chi}$ is a MLEG model.

**REMARK.** The syntactic restriction on game transformation formulas is given in order to ensure that the updated model $M^{\chi}$ is still a MLEG model. In fact, Theorem 9 does not hold if we allow $\chi$ to be any formula in $\mathcal{L}_{MLEG}$. For instance suppose $M$ is a MLEG model such that $W = \{w, v, u, z\}$, $\sim(w) = \{w, v, u, z\}$, $R_{\{i,j\}}(w) = \langle i:a, j:a \rangle$, $R_{\{i,j\}}(v) = \langle i:a, j:b \rangle$, $R_{\{i,j\}}(u) = \langle i:b, j:a \rangle$ and $R_{\{i,j\}}(z) = \langle i:b, j:b \rangle$. If $\chi = \langle i:a \rangle \top \lor \langle j:b \rangle \top$ then the updated model $M^{\chi}$ is no longer a MLEG-model because it does not satisfy the constraint **C2**.

We have reduction axioms for $\chi!$ which guarantee the completeness of the logic MLEG$^{GT}$ explaining how a dynamic operator $[\chi!]$ interacts with the Boolean operators and modal logic operators of MLEG.
**Theorem 10.** The following schemata are valid in the logic $\mathcal{MLEG}^{GT}$.

$$ \mathbf{R1.} \quad [\chi!]p \leftrightarrow (\chi \to p) $$

$$ \mathbf{R2.} \quad [\chi!]\neg\varphi \leftrightarrow (\chi \to \neg[\chi!]\varphi) $$

$$ \mathbf{R3.} \quad [\chi!](\varphi_1 \wedge \varphi_2) \leftrightarrow ([\chi!]\varphi_1 \wedge [\chi!]\varphi_2) $$

$$ \mathbf{R4.} \quad [\chi!]\Box\varphi \leftrightarrow (\chi \to \Box[\chi!]\varphi) $$

$$ \mathbf{R5.} \quad [\chi!]K_i\varphi \leftrightarrow (\chi \to K_i[\chi!]\varphi) $$

$$ \mathbf{R6.} \quad [\chi!]\text{[good]}_i \varphi \leftrightarrow (\chi \to \text{[good]}_i[\chi!]\varphi) $$

$$ \mathbf{R7.} \quad [\chi!]\delta_C \leftrightarrow (\langle\delta_C\rangle\top \to [\chi!]\varphi) $$

The principles **R1.-R7.** are called reduction axioms because, read from left to right, they reduce the complexity of those operators in a formula. In particular the principles **R1.-R7.** explains how to transform any formula $\varphi$ of the language with dynamic operators in a formula without dynamic operators. More generally, we have an axiomatization result:

**Theorem 11.** The logic $\mathcal{MLEG}^{GT}$ is completely axiomatized by the axioms and inference rules of $\mathcal{MLEG}$ together with the schemata of Theorem 10 together with the following rule of replacement of proved equivalence:

$$ \frac{\psi_1 \leftrightarrow \psi_2}{\varphi \leftrightarrow \varphi[\psi_1 := \psi_2]} $$

where $\varphi[\psi_1 := \psi_2]$ is the formula $\varphi$ in which we have replaced all occurrences of $\psi_1$ by $\psi_2$.

Now, consider the following formula:

$$ \chi_{SD} \stackrel{\text{def}}{=} \bigwedge_{i \in Agt, a \in Act} (\Box SD^{\le 0}(i:a) \to [i:a] \perp). $$

where $SD^{\le 0}(i:a)$ has been defined in Subsection 3.3. The effect of the game transformation event $\chi_{SD}!$ is to delete from every game $\sim(w)$ in the model $M$ all worlds in which a strictly dominated strategy is played by some agent.

As the following Theorem 12 highlights, the procedure IDSDS that we have characterized in Section 3.3 in the static $\mathcal{MLEG}$ can be characterized in a more compact way in $\mathcal{MLEG}^{GT}$. Suppose $\delta$ is the selected strategy profile. Then, for every agent $i$, $\delta_i$ survives IDSDS until the subgame of depth $n+1$ if and only if, the event $\chi_{SD}!$ can occur $n+1$ times in sequence.

**Theorem 12.** For all $\delta \in \Delta$, for all $n \ge 0$,

$$ \vdash_{\mathcal{MLEG}^{GT}} \langle\delta\rangle\top \to (\neg SD^{\le n}(\delta) \leftrightarrow \langle\chi_{SD}!\rangle^{n+1}\top). $$

The above theorem says that if $\delta$ is performed, then the formula $\neg SD^{\le n}(\delta)$, defined in Subsection 3.3, whose length is exponential in $n$ and the more compact formula $\langle\chi_{SD}!\rangle^{n+1}\top$ are equivalent. Indeed the length of the formula $\langle\chi_{SD}!\rangle^{n+1}\top$ is $O(n(|Agt||Act|)^2)$ where $n$ is the number of IDSDS rounds, $|Agt|$ is the number of agents and $|Act|$ is the maximal number of actions.

We conjecture that there is no formula $\varphi \in \mathcal{MLEG}$ more compact than $\neg SD^{\le n}(\delta)$ such that $\vdash_{\mathcal{MLEG}} \langle\delta\rangle\top \to (\neg SD^{\le n}(\delta) \leftrightarrow \varphi)$. If our conjecture is true, Theorem 12 would imply that the representation
of IDSDS in $\mathcal{MLEG}^{GT}$ is necessarily more succinct than the representation of IDSDS in $\mathcal{MLEG}$ (i.e. there is no representation of IDSDS in $\mathcal{MLEG}$ that is equally or more succinct than the representation of IDSDS in $\mathcal{MLEG}^{GT}$). The latter is indeed a variant of the result given in [37] showing that S5 with public announcements is more succinct than S5.

Finally, here is a compact reformulation of Theorem 7 in $\mathcal{MLEG}^{GT}$:

**Theorem 13.** For all $n \ge 0$, $\vdash_{\mathcal{MLEG}^{GT}} (MK_{Agt}^n \wedge \bigwedge_{i \in Agt} \mathrm{Rat}_i) \rightarrow \langle\chi_{SD}!\rangle^{n+1} \top$.

It has to be noted that the approach to game dynamics based on Dynamic Epistemic Logic (DEL) proposed here is inspired by [7] in which strategic equilibrium is defined by fixed-points of operations of repeated announcement of suitable epistemic statements and rationality assertions. However, the analysis of epistemic games proposed in [7] is mainly semantical and the author does not provide a full-fledged modal language for epistemic games which allows to express in the object language solution concepts like Nash Equilibrium or IDSDS, and the concept of rationality. Moreover, van Benthem's analysis does not include any completeness result for the proposed framework and there is no proposal of reduction axioms for a combination of DEL with a static logic of epistemic games. On the contrary, these two aspects are central in our analysis.

## 5. Incomplete information

We here consider a more general class of games which includes strategic games with incomplete information about the game structure including the players' strategy sets (or action repertoires) and the players' preference ordering over strategy profiles. This kind of games have been explored in the past by Harsanyi [38]. A more recent analysis is given by [39].

We are interested here in verifying whether the results obtained in Sections 3.2 and 3.3 can be generalized to this kind of games, that is:

1. Are rationality of every player and every agent's knowledge about other agents' choices still sufficient to ensure that the selected strategy profile is a Nash equilibrium in a strategic game with incomplete information about the game structure?

2. Is mutual knowledge of rationality among the players still sufficient to ensure that the selected strategy profile survives iterated deletion of dominated strategies in a strategic game with incomplete information about the game structure?

To answer these questions, we have to remove Axiom **CompleteInfo** of the form $\Box\varphi \rightarrow K_i\varphi$ from $\mathcal{MLEG}$ and the corresponding semantic constraint **C4** from the definition of $\mathcal{MLEG}$ frames expressing the hypothesis of complete information about the game structure. We call $\mathcal{MLEG}^*$ the resulting logic and $\mathcal{MLEG}^*$-models the resulting class of models. Then we have to check whether Theorems 6 and 7 given in Sections 3.2 and 3.3 are still derivable in $\mathcal{MLEG}^*$.

We have a positive answer to the previous first question. Indeed, the formula

$$((\bigwedge_{i \in Agt} \mathrm{Rat}_i) \wedge \bigwedge_{i \in Agt} K_i \langle\delta_{-i}\rangle \top) \rightarrow \mathrm{Nash}(\delta)$$

is derivable in $\mathcal{MLEG}^*$. But we have a negative answer to the second question. Indeed, the following formula is invalid in $\mathcal{MLEG}^*$ for every $\delta \in \Delta$ and for every $n \in \mathbb{N}$ such that $n > 0$:
$$((\text{MK}_{\text{Agt}}^{n} \wedge \bigwedge_{i \in \text{Agt}} \text{Rat}_i) \wedge \langle\delta\rangle \top) \rightarrow \neg \text{SD}^{\leq n}(\delta).$$

This can be proved as follows. We suppose $\text{Agt} = \{1, 2\}$ and we exhibit in Figure 3 a $\mathcal{MLEG}^*$-model $M$ and a world $w_1$ in $M$ in which for all $n$, $(\text{MK}_{\{1,2\}}^n \wedge \bigwedge_{i \in \{1,2\}} \text{Rat}_i) \wedge \langle 1:\text{main} \rangle \top \wedge \text{SD}^{\leq 1}(1:\text{main})$ is true. We call Alarm Game the scenario corresponding to this model.

**Figure 3.** Alarm Game. Again thick circles represent epistemic possibility relations for agent 1 whereas thin circles represent epistemic possibility relations for agent 2. The two equivalence classes $\sim(w_1) = \{w_1, w_2, w_3, w_4\}$ and $\sim(w_5) = \{w_5, w_6, w_7, w_8\}$ correspond to two different games where agents have different preference ordering over strategy profiles.

<figure><img src="image_3.png" /></figure>

**SCENARIO DESCRIPTION.** We call Alarm Game the scenario represented by the model in Figure 3. Agent 1 is a thief who intends to burgle agent 2's apartment. Agent 1 can enter the apartment either by the main door or by the back door (action 1:main or action 1:back). Agent 2 has two actions available. Either he does nothing (action 2:skip) or he follows a security procedure (action 2:proc) which consists in locking the two doors and in activating a surveillance camera on the main door. Entering the apartment by the main door when agent 2 does nothing (i.e. the strategy profile $\langle 1:\text{main}, 2:\text{skip} \rangle$ executed at world $w_2$) and entering by the back door when agent 2 does nothing (i.e. the strategy profile $\langle 1:\text{back}, 2:\text{skip} \rangle$ executed at world $w_4$) are for agent 1 the best situations and are for him equally preferable. Indeed, in both cases agent 1 will successfully enter and burgle the apartment. On the contrary, trying to enter the apartment by the back door when 2 follows the security procedure (i.e. the strategy profile $\langle 1:\text{back}, 2:\text{proc} \rangle$ executed at world $w_3$) is for 1 strictly better than trying to enter by the main door when 2 follows the security procedure (i.e. the strategy profile $\langle 1:\text{main}, 2:\text{proc} \rangle$ executed at world $w_1$). Indeed, in the former case agent 1 will be simply unable to burgle the apartment, in the latter case not only he will be unable to burgle the apartment but also he will disclose his identity. The two possible situations in which agent 1 does not succeed in burgling the apartment (worlds $w_1$ and $w_3$) are equally
preferable for agent 2 and are for 2 strictly better than the situations in which agent 1 successfully burgles the apartment (worlds $w_2$ and $w_4$).

At world $w_1$ agent 1 enters by the main door while agent 2 follows the security procedure. This is the only world in the model $\mathcal{M}$ in which agent 1 has some uncertainty. Indeed, in this world agent 1 can imagine the alternative game defined by the equivalence class $\sim(w_5) = \{w_5, w_6, w_7, w_8\}$ in which he enters by the back door while agent 2 does nothing (world $w_8$). We suppose that in such a game, even if agent 2 follows the security procedure, agent 1 will succeed in burgling his apartment. This is the reason why the four strategy profiles $\langle 1:\text{main}, 2:\text{skip}\rangle$, $\langle 1:\text{back}, 2:\text{skip}\rangle$, $\langle 1:\text{main}, 2:\text{proc}\rangle$ and $\langle 1:\text{back}, 2:\text{proc}\rangle$ are equally preferable for the two agents.

Concerning the automated reasoning aspects of the logic $\mathcal{MLEG}^*$, we conjecture that the complexity of its satisfiability problem is PSPACE. Indeed, we think that it is possible to build a tableau method using only a polynomial amount of memory for the satisfiability problem of $\mathcal{MLEG}^*$. In other terms, we conjecture that if we move from $\mathcal{MLEG}$ to $\mathcal{MLEG}^*$, the complexity decreases from EXPTIME-hard to PSPACE. We here provide an unsurprising lower-bound for the complexity of $\mathcal{MLEG}^*$.

**Theorem 14.** The satisfiability problem of a given formula $\varphi$ in a $\mathcal{MLEG}^*$-model is PSPACE-hard.

The situation is different when we add the Axiom **JointDet** of joint determinism discussed in Section 2.4. Let us call $\mathcal{MLEG}^{det*}$ the logic resulting from adding Axiom **JointDet** of joint determinism to the logic $\mathcal{MLEG}^*$ and $\mathcal{MLEG}^{det*}$-models the class of models resulting from adding the corresponding Constraint **CD** to $\mathcal{MLEG}^*$-models. While the complexity of the satisfiability problem for $\mathcal{MLEG}^{det}$ was NP-complete, it increases to PSPACE-complete for $\mathcal{MLEG}^{det*}$. More precisely:

**Theorem 15.** • If $\text{card}(\text{Agt}) = 1$ and $\text{card}(\text{Act}) = 1$ then the satisfiability problem of a given formula $\varphi$ in a $\mathcal{MLEG}^{det*}$-model is NP-complete.

• If $\text{card}(\text{Agt}) \ge 2$ or $\text{card}(\text{Act}) \ge 2$ the satisfiability problem of a given formula $\varphi$ in a $\mathcal{MLEG}^{det*}$-model is PSPACE-complete.

**6. Weaker forms of complete information**

In the previous section, we have removed Axiom **CompleteInfo** of the form $\Box\varphi \rightarrow K_i\varphi$ from the logic $\mathcal{MLEG}$ to obtain a new logic $\mathcal{MLEG}^*$ in which agents may have incomplete information about all aspects of the game they play, including the players' strategy sets (or action repertoires) and the players' preference ordering over strategy profiles.

Nevertheless, in some cases we would like to suppose that agents have complete information about some specific aspects of the game they play. For example, we would like to suppose that:

1. an agent has complete information about his strategy sets even though he may have incomplete information about other agents' strategy sets or,

2. that an agent has complete information about the strategy set of every agent even though he may have incomplete information about agents' preference ordering over strategy profiles.
The former assumption applies to the scenario in which a robber enters a bank, approaches the bank teller and demands money waving a gun. In this situation the bank teller has complete information about his strategy set: he knows that he can either sound the alarm or do nothing. But the bank teller does not know the robber's strategy set, as he is not sure whether the robber's gun is loaded or not (i.e. the bank teller does not know whether the robber is able to kill him by shooting). The latter assumption applies to a card game like Poker. In Poker a player has complete information about every player's strategy set, as he knows that a given point in the game a player has the option to check (if no bet is in front of him), bet, or fold. However, a Poker player has incomplete information about other players' preference ordering over strategy profiles, as he cannot see other players' cards.

In other terms, we would like to build variants of $\mathcal{MLEG}^*$ in which some formulas of Lemma 1 are derivable.

## 6.1. Complete information about strategy sets

We show here how to relax the Axiom **CompleteInfo** in order to express the assumption of complete information about strategy sets without necessarily assuming complete information over the payoffs.

If we replace Axiom **CompleteInfo** by the following axiom schemas:

$$ (\textbf{CompleteInfoStrategy}_i) \qquad \diamond\langle i:a\rangle\top \rightarrow K_i\diamond\langle i:a\rangle\top $$

for all $i \in Agt$ and $a \in Act$, then every agent $i$ has complete information about his strategy set. That is, if an agent $i$ can perform an action $a$ then agent $i$ knows that he can perform action $a$. Axiom **CompleteInfoStrategy**$_i$ corresponds to the following semantic constraint on models. For every $i \in Agt$ and $a \in Act$:

C7 if $wE_iu$ and there is $v$ such that $w \sim v$ and $i:a = R_i(v)$ then, there is $z$ such that $u \sim z$ and $i:a = R_i(z)$.

If we replace Axiom **CompleteInfo** by the following axiom schemas:

$$ (\textbf{CompleteInfoStrategy}_{i,j}) \qquad \diamond\langle j:a\rangle\top \rightarrow K_i\diamond\langle j:a\rangle\top $$

for all $i, j \in Agt$ and $a \in Act$, then an agent $i$ has complete information about the strategy sets of every agent. That is, if an agent $j$ can perform an action $a$ then every agent $i$ knows that agent $j$ can perform action $a$. Axiom **CompleteInfoStrategy**$_{i,j}$ corresponds to the following semantic constraint on models. For every $i, j \in Agt$ and $a \in Act$:

C8 if $wE_iu$ and there is $v$ such that $w \sim v$ and $j:a = R_j(v)$ then, there is $z$ such that $u \sim z$ and $j:a = R_j(z)$.

Obviously Axiom **CompleteInfoStrategy**$_{i,j}$ is more general than Axiom **CompleteInfoStrategy**$_i$, that is, **CompleteInfoStrategy**$_{i,j}$ implies **CompleteInfoStrategy**$_i$. It is also worth noting that the previous Axiom **CompleteInfoStrategy**$_{i,j}$ together with Axiom **Indep** and Axiom **JointAct** imply $\diamond\langle\delta\rangle\top \rightarrow K_i\diamond\langle\delta\rangle\top$. The latter means that if $\delta$ is a strategy profile of the current game then every agent knows this.
REMARK. Note also that **CompleteInfoStrategy**<sub>*i*</sub> and **CompleteInfoStrategy**<sub>*i*,*j*</sub> are respectively equiv-
alent to □[*i*:*a*]⊥ → K<sub>*i*</sub>□[*i*:*a*]⊥ and □[*j*:*a*]⊥ → K<sub>*i*</sub>□[*j*:*a*]⊥ thanks to Axiom 5 for the epistemic operators
K<sub>*i*</sub>.

In the sequel we call $\mathcal{MLEG}^{**}$ the logic that results from adding the previous Axiom
**CompleteInfoStrategy**<sub>*i*,j*</sub> to the logic $\mathcal{MLEG}^{*}$ discussed in Section 5, and we call $\mathcal{MLEG}^{**}$-models
the corresponding models that results from adding the semantic constraint **C8** to the $\mathcal{MLEG}^{*}$-models.
$\mathcal{MLEG}^{**}$ is the logic of epistemic strategic games in which the only uncertainty is about agents’ prefer-
ence ordering over strategy profiles.

6.2. *An analysis of the Harsanyi transformation*

We conclude our discussion about games with incomplete information by shedding light on Harsanyi’s
claim that all uncertainty about the structure of a game can be reduced to uncertainty about payoffs [38].

Harsanyi proposed a way of transforming a game with uncertainty over both the payoffs and the strat-
egy choices of the players into a game with no strategy-set uncertainty, without affecting the epistemic
implications. More precisely, a player’s choice is rational in the initial game if and only if the player’s
choice will continue to be rational after the game transformation. In other words, according to Harsanyi,
it is always possible to reduce all kinds of incomplete information about the structure of a game to in-
complete information about the strategy choices without affecting the rationality or irrationality of a
player.

The basic idea of Harsanyi's transformation is that having a strategy with a highly undesirable payoff is for a player equivalent to not having the strategy at all. Suppose we start with a game with uncertainty over both the payoffs and the strategy choices of the players. This means that, some player *i* has a strategy *a* in his strategy set and another player *j* does not know this or some player *i* does not have a strategy *a* in his strategy set and another player *j* does not know this. To eliminate player's *j* strategy-set uncertainty is sufficient to add the strategy *a* to the set of strategies which in player *j*'s opinion are included in player *i*'s strategy space and to assign the lowest possible payoff to the new strategy profiles in which player *i* chooses strategy *a*. If player *j* is rational then the game transformation does not affect his choice, as his decision is not affected by the highly undesirable options that have been added by the game transformation.

We here provide a formal proof of Harsanyi's claim in a purely qualitative setting with no probabil-
ities. See [13] for a formal proof of Harsanyi's claim in a quantitative setting using *interactive belief
systems* à la Aumann & Brandeburger [1] with probabilities.

Let us start with a model $M = \langle W, \sim, R, E, \leq, \pi \rangle$ of the logic $\mathcal{MLEG}^*$ in which players may have
incomplete information about all aspects of the game. We want to show that we can build a corresponding
model $M' = \langle W', \sim', R', E', \leq', \pi' \rangle$ of the logic $\mathcal{MLEG}^{**}$ in which players can only have incomplete
information about payoffs and which satisfies the same formulas $\mathrm{Rat}_i$ as $M$.

Let $[W] = \{\sim(w) | w \in W\}$ be the partition of $W$ induced by the equivalence relation $\sim$. We note
$S_1, S_2, \dots$ the elements of $[W]$. Let $\Pi_M = \{\delta | \text{ for every } \delta_i \text{ there is } u \in W \text{ such that } M, u \models \langle\delta_i\rangle^T\}$ be
the set of strategy profiles with respect to the model $M$.

The model $M'$ can be defined as follows.
* for every $S_i \in [W]$, $S'_i = S_i \cup \{w_i^\delta \mid \delta \in \Pi_M$ and there is no $v \in S_i$ such that $M, v \models \langle \delta \rangle \top\}$

* $W' = \bigcup_{S_i \in [W]} S'_i$

* for every $w, v \in W'$, $w \not\sim v$ if and only if there is $S_i \in [W]$ such that $w, v \in S'_i$

* for every $C \in 2^{Agt*}$ and $w \in W$, $R'_C(w) = R_C(w)$

* for every $C \in 2^{Agt*}$ and $w_i^\delta \in W' \setminus W$, $R'_C(w) = \delta_C$

* for every $i \in Agt$ and $w \in W$, $E'_i(w) = E_i(w)$

* for every $i \in Agt$ and $w_i^\delta \in W' \setminus W$, $E'_i(w_i^\delta) = \{w_i^\delta\}$

* for every $i \in Agt$ and $w \in W$, $\leq'_i(w) = \leq_i(w)$

* for every $i \in Agt$ and $w_i^\delta \in W' \setminus W$, $\leq'_i(w_i^\delta) = \sim'(w_i^\delta)$

* for every $p \in Atm$, $\pi'(p) = \pi(p) \cup \{w_i^\delta \mid w_i^\delta \in W'\}$

It is straightforward to check that $M'$ is indeed a $\mathcal{MLEG}^{**}$-model without strategy-set uncertainty.
The following Theorem 16 is a formal characterization of Harsanyi's claim.

**Theorem 16.** For every $w \in W$ and for every $i \in Agt$, $M, w \models Rat_i$ if and only if $M', w \models Rat_i$.

The following corollary of Theorem 16 highlights that Harsanyi transformation does not affect common knowledge about the rationality or irrationality of a player.

**Corollary 1.** For every $w \in W$, for every $i \in Agt$ and for every $C \in 2^{Agt*}$, we have $M, w \models \mathrm{MK}_C^n Rat_i$ if and only if $M', w \models \mathrm{MK}_C^n Rat_i$.

# 7. Conclusion

We have presented a multi-modal logic that enables to reason about epistemic games in strategic form. This logic, called $\mathcal{MLEG}$ (Modal Logic of Epistemic Games), integrates the concepts of joint action, preference and knowledge. We have shown that $\mathcal{MLEG}$ provides a highly flexible formal framework for the analysis of the epistemic aspects of strategic interaction. Indeed, $\mathcal{MLEG}$ can be easily adapted in order to integrate different assumptions on players’ knowledge about the structure of a game.

Directions for future research are manifold. In this article (Section 3.2) we only considered the notion of individualistic rationality assumed in classical game theory: an agent decides to perform a certain action only if the agent believes that this action is a best response to what he expects the others will do. Our plan is to extend the present modal logic analysis of epistemic games to other forms of rationality such as fairness and reciprocity [40]. According to these notions of rationality, rational agents are not necessarily self-interested but they also consider the benefits of their choices for the group. Moreover, their decisions can be affected by their beliefs about other agents’ willingness to act for the well-being of the group. In [41] we did some first steps into this direction.

Another aspect we intend to investigate in the future is a generalization of our approach to mixed strategies. Indeed, at the current stage the multi-modal logic $\mathcal{MLEG}$ only enables to reason about pure
strategies. To this aim, we will have to extend MLEG by modal operators of probabilistic beliefs as
the ones studied by [42,43]. We also postpone to future work an analysis of the epistemic conditions of
Bayesian equilibrium in the resulting logical framework.

References

1. Aumann, R.J.; Brandenburger, A. Epistemic Conditions for Nash Equilibrium. *Econometrica* **1995**, *63*, 1161–1180.

2. Aumann, R. Interactive Epistemology I: Knowledge. *International Journal of Game Theory* **1999**, *28*, 263–300.

3. Bonanno, G. A syntactic approach to rationality in games with ordinal payoffs. Proceedings of the 8th Conference on Logic and the Foundations of Game and Decision Theory (LOFT 2008). Amsterdam University Press, 2008, Texts in Logic and Games Series, pp. 59–86.

4. Battigalli, P.; Bonanno, G. Recent results on belief, knowledge and the epistemic foundations of game theory. *Research in Economics* **1999**, *53*, 149–225.

5. Brandenburger, A. Knowledge and Equilibrium in Games. *Journal of Economic Perspectives* **1992**, *6*, 83–101.

6. Gintis, H. *The Bounds of Reason: Game Theory and the Unification of the Behavioral Sciences*; Princeton University Press, 2009.

7. van Benthem, J. Rational dynamics and epistemic logic in games. *International Game Theory Review* **2007**, *9*, 13–45.

8. de Bruin, B. Explaining games: on the logic of game theoretic explanations. PhD thesis, University of Amsterdam, The Netherlands, 2004.

9. Roy, O. Thinking before acting: intentions, logic, rational choice. PhD thesis, University of Amsterdam, The Netherlands, 2008.

10. van Ditmarsch, H.P.; van der Hoek, W.; Kooi, B. *Dynamic Epistemic Logic*; Kluwer Academic Publishers, 2007.

11. Baltag, A.; Moss, L.S. Logics for Epistemic Programs. *Synthese* **2004**, *139*, 165–224.

12. Gerbrandy, J.; Groeneveld, W. Reasoning about information change. *Journal of Logic, Language, and Information* **1997**, *6*, 147–196.

13. Hu, H.; Stuart, H.W. An epistemic analysis of the Harsanyi transformation. *International Journal of Game Theory* **2001**, *30*, 517–525.

14. van Benthem, J.; Liu, F. Dynamic Logic of preference upgrade. *Journal of Applied Non-Classical Logics* **2007**, *17(2)*, 157–182.

15. Osborne, M.J.; Rubinstein, A. *A course in game theory*; MIT Press, 1994.

16. Lewis, C.I.; Langford, C.H. *Symbolic Logic*; Dover Publications: New York, 1932.

17. Liu, F. Changing for the better: Preference dynamics and agent diversity. PhD thesis, University of Amsterdam, The Netherlands, 2008.

18. van Benthem, J.; Girard, P.; Roy, O. Everything else being equal: a modal logic for *ceteris paribus* preferences. *Journal of Philosophical Logic* **2009**, *38*, 83–125.

19. Belnap, N.; Perloff, M.; Xu, M. *Facing the future: agents and choices in our indeterminist world*; Oxford University Press: New York, 2001.
20. Papadimitriou, C.H. *Computational complexity*; Addison Wesley, 1994.

21. Halpern, J.Y.; Moses, Y. A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief. *Artificial Intelligence* **1992**, *54*, 319–379.

22. Pratt, V. A near-optimal method for reasoning about action* 1. *Journal of Computer and System Sciences* **1980**, *20*, 231–254.

23. Pauly, M. Logic for Social Software. PhD thesis, University of Amsterdam, The Netherlands, 2001.

24. Pauly, M. A modal logic for coalitional power in games. *Journal of Logic and Computation* **2002**, *12(1)*, 149–166.

25. Lorini, E. A dynamic logic of agency II: deterministic DLA, Coalition Logic, and game theory. *Journal of Logic, Language, Information* **2010**, *19(3)*, 327–351.

26. Horty, J.F. *Agency and Deontic Logic*; Oxford University Press: Oxford, 2001.

27. Herzig, A.; Lorini, E. A dynamic logic of agency I: STIT, abilities and powers. *Journal of Logic, Language and Information* **2010**, *19(1)*, 89–121.

28. von Wright, G.H. *The logic of preference*; Edinburgh University Press: Edinburgh, 1963.

29. Stalnaker, R. On the evaluation of solution concepts. *Theory and decision* **1994**, *37*, 49–73.

30. Board, O. Knowledge, Beliefs, and Game-Theoretic Solution Concepts. *Oxford Review of Economic Policy* **2002**, *18*, 418–432.

31. Bernheim, D. Axiomatic Characterizations of Rational Choice in Strategic Environments. *Scandinavian Journal of Economics* **1986**, *88*, 473–488.

32. Pearce, D. Rationalizable strategic behavior and the problem of perfection. *Econometrica* **1984**, *52*, 1029–1050.

33. Brandeburger, A.; Dekel, E. Rationalizability and correlated equilibria. *Econometrica* **1987**, *55*, 1391–1402.

34. Tan, T.; Werlang, S. The Bayesian foundation of solution concepts of games. *Journal of Economic Theory* **1988**, *45*, 370–391.

35. van der Hoek, W.; Jamroga, W.; Wooldridge, M. A logic for strategic reasoning. Proceedings of the Fourth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2005); New York: ACM Press, 2005; pp. 157–164.

36. van der Hoek, W.; Pauly, M. Modal Logic for Games and Information. In *Handbook of Modal Logic (3)*; Blackburn, P.; Van Benthem, J.; Wolter, F., Eds.; Elsevier: Amsterdam, 2006.

37. Lutz, C. Complexity and succinctness of public announcement logic. Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems. ACM, 2006, pp. 137–143.

38. Harsanyi, J.C. Games with incomplete information played by ‘Bayesian’ players. *Management Science* **1967**, *14*, 159–182.

39. Halpern, J.Y.; Rego, L. Generalized solution concepts in games with possibly unaware players. Proceedings of the Eleventh Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2007), 2007, pp. 253–262.

40. Fehr, E.; Schmidt, K.M. Theories of Fairness and Reciprocity: Evidence and Economic Applications. In *Advances in Economics and Econometrics*; Cambridge University Press, 2003.
41. Lorini, E. *A Logical Account of Social Rationality in Strategic Games*. Proceedings of the 9th Conference on Logic and the Foundations of Game and Decision Theory (LOFT 2010), 2010.

42. Halpern, J. *Reasoning about uncertainty*; MIT Press: Cambridge, 2003.

43. Fagin, R.; Halpern, J. *Reasoning about Knowledge and Probability*. *Journal of the Association for Computing Machinery* **1994**, *41*, 340–367.

44. Blackburn, P.; de Rijke, M.; Venema, Y. *Modal Logic*; Cambridge University Press: Cambridge, 2001.

45. Sahlqvist, H. Completeness and correspondence in the first and second order semantics for modal logics. Proceedings 3rd Scandinavian Logic Symposium 1973, 1975, Vol. number 82 in Studies in Logic.

46. Chen, C.; Lin, I. The complexity of propositional modal theories and the complexity of consistency of propositional modal theories. *Logical Foundations of Computer Science* **1994**, pp. 69–80.

47. Chellas, B.F. *Modal logic: an introduction*; Cambridge University Press, 1980.

48. Savitch, W. Relationships between nondeterministic and deterministic tape complexities*. *Journal of computer and system sciences* **1970**, *4*, 177–192.
# A. ANNEX: Proofs of some theorems

## A.1. *Proof of Theorem 1 and 3*

$\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}$ is determined by the class of $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}$-models. $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\text{det}}$ is determined by the class of $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\text{det}}$-models.

*Proof.* We only provide a sketch of the proof of Theorem 3. The proof of Theorem 1 is a straightforward adaptation of the proof of Theorem 3. It is sufficient to remove the constraint (S6) from the following definition 3.

It is straightforward to show that all axioms in Figure 2 are valid and that the rules of inference preserve validity in the class of $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\text{det}}$-models. The other part of the proof is shown using two major steps.

**Step 1.** We provide an alternative semantics for $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\text{det}}$ in terms of standard Kripke models whose semantic conditions correspond one-to-one to the axioms in Table 2. The definition of Kripke $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\text{det}}$-models is the following one.

**Definition 3 (Kripke $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\text{det}}$-model).** Kripke $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\text{det}}$-models are tuples $M = (W, \sim, R, E, \leq, \pi)$ where:

* $W$ is a nonempty set of possible worlds or states;

* $\sim$ is an equivalence relation on $W$;

* $R: \bigcup_{C \in 2^{Agt}*} \Delta_C \to 2^{W \times W}$ maps every joint action $\delta_C$ to a transition relation $R_{\delta_C} \subseteq W \times W$ between possible worlds such that:

S1 $R_{\delta_C}(w) \neq \emptyset$ if and only if, for every $i \in C$, $R_{\delta_i}(w) \neq \emptyset$,

S2 if $R_{\delta_C}(w) \neq \emptyset$ then $R_{\delta_C}(w) = \{w\}$,

S3 $\bigcup_{\delta_C \in \Delta_C} R_{\delta_C}(w) \neq \emptyset$,

S4 if $\delta_C \neq \delta'_C$ then $R_{\delta_C}(w) = \emptyset$ or $R_{\delta'_C}(w) = \emptyset$,

S5 if for every $i \in Agt$ there is $v_i$ such that $w \sim v_i$ and $R_{\delta_i}(v_i) \neq \emptyset$ then there is a $v$ such that $w \sim v$ and $R_{\delta}(v) \neq \emptyset$;

S6 if $w \sim v$ and $R_{\delta}(w) \neq \emptyset$ and $R_{\delta}(v) \neq \emptyset$, then $w = v$;

* $E: Agt \to W \times W$ maps every agent $i$ to an equivalence relation $E_i$ on $W$ such that:

S6 if $(w, v) \in E_i$, then $i:a = R_i(w)$ if and only if $i:a = R_i(v)$,

S7 if $w \in E_i v$ then $w \sim v$;

* $\leq: Agt \to W \times W$ maps every agent $i$ to a reflexive, transitive relation $\leq_i$ on $W$ such that:

S8 if $w \leq_i v$ then $w \sim v$,

S9 if $w \sim v$ and $w \sim v'$ then $v \leq_i v'$ or $v' \leq_i v$;
• $\pi : \mathit{Atm} \to 2^W$ is a valuation function.

Truth conditions of $\mathcal{MLEG}^{\det}$ formulas in Kripke $\mathcal{MLEG}^{\det}$-models are again standard for atomic formulas and the Boolean operators. The truth conditions for Boolean operators and for operators $\square$, $K_i$ and $[\text{good}]_i$ are the ones of Section 2.2. The truth condition for operators $[\delta_C]$ are:

• $M, w \models [\delta_C] \varphi$ iff $M, v \models \varphi$ for all $v \in R_{\delta_C}(w)$.

It is a routine task to prove that the axiomatic system of the logic $\mathcal{MLEG}^{\det}$ given in Table 2 is sound and complete with respect to this class of Kripke $\mathcal{MLEG}^{\det}$-models via the Sahlqvist theorem, cf. [44, Th. 2.42]. Indeed all axioms in Table 2 are in the so-called Sahlqvist class [45]. Thus, they are all expressible as first-order conditions on Kripke models and are complete with respect to the defined model classes.

**Step 2.** The second step shows that the semantics in terms of $\mathcal{MLEG}^{\det}$-models of Definition 2 and the semantics in terms of Kripke $\mathcal{MLEG}^{\det}$-models of Definition 3 are equivalent. As the logic $\mathcal{MLEG}^{\det}$ is sound and complete for the class of Kripke $\mathcal{MLEG}^{\det}$-models and is sound for the class of $\mathcal{MLEG}^{\det}$-models, we have that for every $\mathcal{MLEG}^{\det}$ formula $\varphi$, if $\varphi$ is valid in the class of Kripke $\mathcal{MLEG}^{\det}$-models then $\varphi$ is valid in the class of $\mathcal{MLEG}^{\det}$-models. Consequently, for every $\mathcal{MLEG}^{\det}$ formula $\varphi$, if $\varphi$ is satisfiable in the class of $\mathcal{MLEG}^{\det}$-models then $\varphi$ is satisfiable in the class of Kripke $\mathcal{MLEG}^{\det}$-models. Therefore, in this second step we just need to show that for every $\mathcal{MLEG}^{\det}$ formula $\varphi$, if $\varphi$ is satisfiable in the class of Kripke $\mathcal{MLEG}^{\det}$-models then $\varphi$ is satisfiable in the class of $\mathcal{MLEG}^{\det}$-models.

Suppose $\varphi$ is satisfiable in the class of Kripke $\mathcal{MLEG}^{\det}$-models. This means that there is a Kripke $\mathcal{MLEG}^{\det}$-model $M = (W, \sim, R, E, \leq, \pi)$ and world $w$ such that $M, w \models \varphi$. We can now build a $\mathcal{MLEG}^{\det}$-model $M' = (W', R', E', \leq', \pi')$ which satisfies $\varphi$. The model $M'$ is defined as follows:

• $W' = W$;

• for every $C \in 2^{Agt}$ and $v \in W'$, $R'_C(v) = \delta_C$ if and only if $R_{\delta_C}(v) \neq \emptyset$;

• for every $i \in Agt$, $E'_i = E_i$;

• for every $i \in Agt$, $\leq'_i = \leq_i$;

• $\pi' = \pi$.

By induction on the structure of $\varphi$, it is just a trivial exercise to show that we have $M', w \models \varphi$. $\square$

<figure><img src="image_4.png" /></figure>

## A.2. *Proof of Theorem 2*

*Proof.* Let us start to prove that the satisfiability problem of $\mathcal{MLEG}$ is EXPTIME-hard when $card(Agt) \geq 2$. Let us consider two distinct agents $i, j \in Agt$. Let us consider a modal formula $\varphi$ made of operators $K_i$, $K_j$ and $\square$. It is easy to check that the following two statements are equivalent:

• $\varphi$ is satisfiable in the logic where $K_i$ and $K_j$ are S5-operators and $\square$ is the universal modality;

• $\varphi$ is satisfiable in $\mathcal{MLEG}$.
So we have a reduction from the satisfiability problem of $\mathcal{MLEG}$ to the satisfiability problem of $S5_2$ plus universal modality $\square$.

But the satisfiability problem of $S5_2$ plus the universal modality $\square$ is EXPTIME-hard as it is the case for the satisfiability problem of K plus the universal modality [46]. Indeed, we can reduce the satisfiability problem of $S5_2$ plus the universal modality $\square$ to the satisfiability problem of K plus the universal modality by translating a formula of K plus the universal modality into $S5_2$ plus universal modality. Let $x$ be an extra proposition. The translation works as follows:

* $\mathrm{tr}_i(\Box\psi) = x \wedge \mathbf{K}_i[\neg x \rightarrow \mathrm{tr}_j(\psi)]$ where $\Box$ is the K-operator;

* $\mathrm{tr}_j(\Box\psi) = \neg x \wedge \mathbf{K}_j[x \rightarrow \mathrm{tr}_i(\psi)]$ where $\Box$ is the K-operator;

* for all $a \in \{i, j\}$, $\mathrm{tr}_a = \Box[\mathrm{tr}_i(\psi) \lor \mathrm{tr}_j(\psi)]$ where $\Box$ is the universal operator.

And $\varphi$ is satisfiable in K plus universal modality iff $\mathrm{tr}_i(\varphi)$ is satisfiable in $S5_2$ plus the universal modality. So $\mathcal{MLEG}$ is EXPTIME-hard.

Now let us prove that the satisfiability problem of $\mathcal{MLEG}$ is NEXPTIME. We are going to prove that we can make a filtration of any $\mathcal{MLEG}$ model, preserving both the semantic constraints of Definition 1 and the truth of formulas (see [47] for a general introduction to the filtration method in modal logic). Let us consider a $\mathcal{MLEG}$-model $M = (W, \sim, R, E, \leq, \pi)$ where we suppose $\sim$ to be the universal modality, without loss of generality. As usual, we consider a formula $\varphi$, the set $\Gamma = SF(\varphi)$ of all subformulas of $\varphi$ and the equivalence relation $\equiv$ over $W$ defined by $w \equiv u$ iff for all $\psi \in \Gamma$, $M, w \models \psi$ iff $M, u \models \psi$. We note $|w|$ the equivalence class of $\equiv$ containing $w$. Let us define $M' = (W', \sim, R', E', \leq', \pi')$ by:

* $W' = \{|w| \mid w \in W\}$;

* $\sim = W' \times W'$;

* $R_C(|w|) = R_C(w)$;

* $|w|E_i|u|$ iff for all formulas $K_i\psi \in \Gamma$, $M, w \models K_i\psi$ iff $M, u \models K_i\psi$ and $R_i(w) = R_i(u)$;

* $|w| \leq'_i |u|$ iff for all formulas $[\mathrm{good}]_i \psi \in \Gamma$, $M, w \models [\mathrm{good}]_i \psi$ implies $M, u \models [\mathrm{good}]_i \psi$;

* $\pi'(p) = \{|w| \mid w \in \pi(p) \text{ and } p \text{ appears in } \varphi\}$.

We leave the reader checking that $M'$ is well-defined, $M'$ satisfies the constraints of Definition 1 and that if $M, w \models \varphi$ then $M', |w| \models \varphi$.

This filtration implies that if a formula $\varphi$ is satisfiable, then it is satisfiable in a model of size $O(2^{|\varphi|})$ where $|\varphi|$ is the length of the formula $\varphi$. A possible algorithm for solving the satisfiability of $\varphi$ may be as follows:

* Guess non-deterministically a $\mathcal{MLEG}$-model $M = (F, \pi)$ whose size is bounded by $O(2^{|\pi|})$ where $\pi$ only gives truthness of propositions occuring in $\varphi$;

* Guess non-deterministically a world $w$ of $M$;

* Check if $M, w \models \varphi$.
This algorithm non-deterministically runs in exponential time. So the satisfiability problem of $\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}$ is in NEXPTIME. □

### A.3. *Proof of Theorem 4*

*Proof.* The satisfiability problem of $\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}^{det}$ is clearly NP-hard because it is a conservative extension of the classical propositional logic whose satisfiability problem in NP-complete (Cook's Theorem [20]).

Now let us prove it is in NP. Clearly if a formula $\varphi$ is $\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}^{det}$-satisfiable, there exists a $\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}^{det}$-model $F = \langle F, \pi \rangle$ whose size is bounded by $card(Act)^{card(Agt)}$. Here is a non-deterministic algorithm to check if a given formula $\varphi$ is satisfiable:

* Guess non-deterministically a $\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}^{det}$-model $M = \langle F, \pi \rangle$ whose size is bounded by $card(Act)^{card(Agt)}$ where $\pi$ only gives truthness of propositions occuring in $\varphi$;

* Guess non-deterministically a world $w$ of $M$;

* Check if $M, w \models \varphi$.

This algorithm non-deterministically runs in polynomial time. So the satisfiability problem of $\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}^{det}$ is in NP. □

### A.4. *Proof of Theorem 5a*

For all $i \in Agt$, we have: $\vdash_{\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}} \mathrm{Rat}_i \leftrightarrow \mathrm{K}_i \mathrm{Rat}_i$

**Lemma 2.** $\vdash_{\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}} [i:a] \perp \rightarrow \mathrm{K}_i[i:a] \perp$

*Proof.* 1. $\vdash_{\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}} \bigvee_{b \in A_{\mathrm{ct}}} \langle i:b \rangle \top$; from **Active**;

2. $\vdash_{\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}} [i:a] \perp \rightarrow [i:a] \perp \wedge \bigvee_{b \in A_{\mathrm{ct}}} \langle i:b \rangle \top$ by 1. and Boolean principles;

3. $\vdash_{\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}} [i:a] \perp \wedge \bigvee_{b \in A_{\mathrm{ct}}} \langle i:b \rangle \top \rightarrow \bigvee_{b \neq a} \langle i:b \rangle \top$ by Boolean principles;

4. $\vdash_{\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}} \langle i:b \rangle \top \rightarrow \mathrm{K}_i \langle i:b \rangle \top$ if $b \neq a$ by **Aware**;

5. $\vdash_{\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}} \bigvee_{b \neq a} \langle i:b \rangle \top \rightarrow \bigvee_{b \neq a} \mathrm{K}_i \langle i:b \rangle \top$ by 4. and Boolean principles;

6. $\vdash_{\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}} \langle i:b \rangle \top \rightarrow [i:a] \perp$ if $b \neq a$; by **Single**;

7. $\vdash_{\mathcal{M\mathcal{L}\mathcal{E}\mathcal{G}}} \mathrm{K}_i(\langle i:b \rangle \top \rightarrow [i:a] \perp)$ if $b \neq a$ by Necessitation of $\mathrm{K}_i$ from 6;
8. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} K_i\langle i:b \rangle \top \rightarrow K_i[i:a] \perp$ if $b \neq a$
by Axiom K for $K_i$ plus **Modus Ponens** from 7;

9. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \bigvee_{b \neq a} K_i \langle i:b \rangle \top \rightarrow K_i [i:a] \perp$
by Boolean principles from 8.

10. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} [i:a] \perp \rightarrow K_i[i:a] \perp$
by 2, 3, 5 and 9.

☐

Now let us prove Theorem 5a. We give here a version of the proof that uses Axioms K, T, 4 and 5 for epistemic modal operators.

*Proof.* 1. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \mathrm{Rat}_i \leftrightarrow \bigwedge_{a,b \in \mathrm{Act}} (\langle i:a \rangle \top \rightarrow \bigvee_{\beta \in \Delta} (\hat{K}_i\langle \beta_{-i} \rangle \top \wedge K_i(\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle)))$
by Definition of Rat$_i$;

2. $\hat{K}_i\langle \beta_{-i} \rangle \top \leftrightarrow K_i \hat{K}_i\langle \beta_{-i} \rangle \top$
by Axiom 5 for $K_i$;

3. $K_i(\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle) \leftrightarrow K_i K_i(\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle)$
by Axiom 4 for $K_i$ plus Boolean principles;

4. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \mathrm{Rat}_i \rightarrow \bigwedge_{a,b \in \mathrm{Act}} (\langle i:a \rangle \top \rightarrow \bigvee_{\beta \in \Delta} (K_i \hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i K_i (\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle)))$
by 1, 2, 3 and Boolean principles;

5. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} K_i \varphi \wedge K_i \psi \dots \leftrightarrow K_i (\varphi \wedge \psi \dots)$
by modal logic K principles;

6. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} [i:a] \perp \rightarrow K_i [i:a] \perp$
by Lemma 2;

7. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \mathrm{Rat}_i \rightarrow \bigwedge_{a,b \in \mathrm{Act}} (K_i[i:a] \perp \bigvee_{\beta \in \Delta} K_i(\hat{K}_i\langle \beta_{-i} \rangle \top \wedge K_i(\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle)))$
by 4, 5, 6 and Boolean principles;

8. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} K_i \varphi \vee K_i \psi \dots \rightarrow K_i (\varphi \vee \psi \dots)$
by modal logic K principles;

9. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \mathrm{Rat}_i \rightarrow K_i \underbrace{\bigwedge_{a,b \in \mathrm{Act}} ([i:a] \perp \bigvee_{\beta \in \Delta} (\hat{K}_i\langle \beta_{-i} \rangle \top \wedge K_i(\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle)))}_{\mathrm{Rat}_i}$
by 7 and 8;

10. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} K_i \mathrm{Rat}_i \rightarrow \mathrm{Rat}_i$
by Axiom T of $K_i$;
11. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \mathrm{Rat}_i \leftrightarrow K_i \mathrm{Rat}_i$
by 9 and 10.

☐

We give another version of the proof of Theorem 5a that uses Axioms K, T and 5 for epistemic modal operators and introspection over preferences “($\delta \le_i \delta'$) $\rightarrow$ $K_i(\delta \le_i \delta'$)”.

*Proof.* 1. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \mathrm{Rat}_i \leftrightarrow (\bigwedge_{a,b \in \mathrm{Act}} (\langle i:a \rangle \top \rightarrow \bigvee_{\beta \in \Delta} (\hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i(\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle))))$ by Definition of $\mathrm{Rat}_i$;

2. $\hat{K}_i \langle \beta_{-i} \rangle \top \leftrightarrow K_i \hat{K}_i \langle \beta_{-i} \rangle \top$
by Axiom 5 for $K_i$;

3. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \mathrm{Rat}_i \leftrightarrow \bigwedge_{a,b \in \mathrm{Act}} (\langle i:a \rangle \top \rightarrow \bigvee_{\beta \in \Delta} (K_i \hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i(\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle)))$ by 1 and 2;

4. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} K_i \varphi \wedge K_i \psi \dots \leftrightarrow K_i (\varphi \wedge \psi \dots)$
by modal logic K principles;

5. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} [i:a] \perp \rightarrow K_i [i:a] \perp$
by Lemma 2;

6. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \mathrm{Rat}_i \leftrightarrow \bigwedge_{a,b \in \mathrm{Act}} (K_i [i:a] \perp \vee \bigvee_{\beta \in \Delta} K_i (\hat{K}_i \langle \beta_{-i} \rangle \top \wedge (\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle)))$ by 2, 4, 5 and Boolean principles;

7. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} K_i \varphi \vee K_i \psi \dots \rightarrow K_i (\varphi \vee \psi \dots)$
by modal logic K principles;

8. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \mathrm{Rat}_i \rightarrow K_i \bigwedge_{a,b \in \mathrm{Act}} ([i:a] \perp \vee \bigvee_{\beta \in \Delta} (\hat{K}_i \langle \beta_{-i} \rangle \top \wedge (\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle)))$

9. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} (\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle) \rightarrow K_i(\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle)$
by Lemma 1 (or introspection over preferences);

10. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \mathrm{Rat}_i \rightarrow K_i \underbrace{\bigwedge_{a,b \in \mathrm{Act}} ([i:a] \perp \vee \bigvee_{\beta \in \Delta} (\hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i(\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:a \rangle)))}_{\mathrm{Rat}_i}$
by 8 and 9;

11. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} K_i \mathrm{Rat}_i \rightarrow \mathrm{Rat}_i$
by Axiom T of $K_i$;

12. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \mathrm{Rat}_i \leftrightarrow K_i \mathrm{Rat}_i$
by 10 and 11.

☐
### A.5. *Proof of Theorem 6*

For all $\delta \in \Delta$, we have:

$$ \vdash_{\mathcal{MLEG}} \left( \left( \bigwedge_{i \in A_{gt}} \mathrm{Rat}_i \right) \wedge \bigwedge_{i \in A_{gt}} K_i \langle \delta_{-i} \rangle \top \right) \rightarrow \mathrm{Nash}(\delta) $$

*Proof.* 1. $\vdash_{\mathcal{MLEG}} \langle \delta_{-i} \rangle \top \rightarrow [\beta_{-i}] \perp \text{ if } \beta_{-i} \neq \delta_{-i}$
by **Single**;

2. $\vdash_{\mathcal{MLEG}} K_i (\langle \delta_{-i} \rangle \top \rightarrow [\beta_{-i}] \perp) \text{ if } \beta_{-i} \neq \delta_{-i}$
by necessitation of $K_i$;

3. $\vdash_{\mathcal{MLEG}} (K_i \langle \delta_{-i} \rangle \top \rightarrow K_i [\beta_{-i}] \perp) \text{ if } \beta_{-i} \neq \delta_{-i}$
by axiom K of $K_i$ plus **Modus Ponens**;

4. $\vdash_{\mathcal{MLEG}} K_i \langle \delta_{-i} \rangle \top \wedge \hat{K}_i \langle \beta_{-i} \rangle \top \leftrightarrow \perp \text{ if } \beta_{-i} \neq \delta_{-i}$
by Boolean principles;

5. $\vdash_{\mathcal{MLEG}} K_j \langle \delta_{-j} \rangle \top \rightarrow \langle \delta_{-j} \rangle \top$
by axiom T of $S_5 K_i$.

6. $\vdash_{\mathcal{MLEG}} \langle \delta_{-j} \rangle \top \rightarrow \langle \delta_i \rangle \top \text{ if } j \neq i$
by **JointAct**;

7. $\vdash_{\mathcal{MLEG}} K_j \langle \delta_{-j} \rangle \top \rightarrow \langle \delta_i \rangle \top \text{ for } j \neq i$
by 5 and 6;

8. $\vdash_{\mathcal{MLEG}} \left( \left( \bigwedge_{i \in A_{gt}} \mathrm{Rat}_i \right) \wedge \bigwedge_{i \in A_{gt}} K_i \langle \delta_{-i} \rangle \top \right)$
$$ \rightarrow \bigwedge_{b \in A_{\mathrm{Act}}} \left( \langle \delta_i \rangle \top \rightarrow \mathrm{V}_{\beta \in \Delta} \left( \hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i \left( \left( \left( \langle i: b, \beta_{-i} \rangle \top \right) \leq_i \left( \langle \delta_i, \beta_{-i} \rangle \top \right) \right) \right) \wedge \langle \delta_i \rangle \top \wedge K_i \langle \delta_{-i} \rangle \top \right) $$
by Boolean principles and 7;

9. $\vdash_{\mathcal{MLEG}} \bigwedge_{b \in A_{\mathrm{Act}}} \left( \langle \delta_i \rangle \top \rightarrow \mathrm{V}_{\beta \in \Delta} \left( \hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i \left( \left( \left( \langle i: b, \beta_{-i} \rangle \top \right) \leq_i \left( \langle \delta_i, \beta_{-i} \rangle \top \right) \right) \right) \wedge \langle \delta_i \rangle \top \wedge K_i \langle \delta_{-i} \rangle \top \right)$
$$ \rightarrow \bigwedge_{b \in A_{\mathrm{Act}}} \mathrm{V}_{\beta \in \Delta} \left( \hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i \left( \left( \left( \langle i: b, \beta_{-i} \rangle \top \right) \leq_i \left( \langle \delta_i, \beta_{-i} \rangle \top \right) \right) \right) \wedge K_i \langle \delta_{-i} \rangle \top $$
by Boolean principle "$A \wedge (A \rightarrow B) \rightarrow B$";

10. $\vdash_{\mathcal{MLEG}} \bigwedge_{b \in A_{\mathrm{Act}}} \mathrm{V}_{\beta \in \Delta} \left( \hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i \left( \left( \left( \langle i: b, \beta_{-i} \rangle \top \right) \leq_i \left( \langle \delta_i, \beta_{-i} \rangle \top \right) \right) \right) \wedge K_i \langle \delta_{-i} \rangle \top$
$$ \rightarrow \bigwedge_{b \in A_{\mathrm{Act}}} \mathrm{V}_{\beta \in \Delta} \left( \hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i \langle \delta_{-i} \rangle \top \wedge K_i \left( \left( \left( \langle i: b, \beta_{-i} \rangle \top \right) \leq_i \left( \langle \delta_i, \beta_{-i} \rangle \top \right) \right) \right) \right) $$
by distributivity of $\wedge$ over $\mathrm{V}_{\beta \in \Delta}$;

11. $\vdash_{\mathcal{MLEG}} \bigwedge_{b \in A_{\mathrm{Act}}} \mathrm{V}_{\beta \in \Delta} \left( \hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i \langle \delta_{-i} \rangle \top \wedge K_i \left( \left( \left( \langle i: b, \beta_{-i} \rangle \top \right) \leq_i \left( \langle \delta_i, \beta_{-i} \rangle \top \right) \right) \right) \right)$
$$ \rightarrow \bigwedge_{b \in A_{\mathrm{Act}}} K_i \left( \left( \left( \langle i: b, \delta_{-i} \rangle \top \right) \leq_i \left( \langle \delta_i, \delta_{-i} \rangle \top \right) \right) \right) $$
by 4 plus Boolean principles;
12. $\vdash_{\mathcal{MLEG}} K_i((\langle i:b, \delta_{-i} \rangle \top \le_i (\langle \delta_i, \delta_{-i} \rangle \top)) \rightarrow (\langle i:b, \delta_{-i} \rangle \top \le_i (\langle \delta_i, \delta_{-i} \rangle \top))$ by Axiom T of $K_i$;

13. $\vdash_{\mathcal{MLEG}} \bigwedge_{b \in Act} K_i((\langle i:b, \delta_{-i} \rangle \top \le_i (\langle \delta_i, \delta_{-i} \rangle \top)) \rightarrow \underbrace{\bigwedge_{b \in Act} (\langle i:b, \delta_{-i} \rangle \top \le_i (\langle \delta_i, \delta_{-i} \rangle \top))}_{\text{BR}(\delta_i, \delta_{-i})}$ by 12 and Boolean principles;

14. $\vdash_{\mathcal{MLEG}} \left( \left( \bigwedge_{i \in Agt} \text{Rat}_i \right) \wedge \bigwedge_{i \in Agt} K_i \langle \delta_{-i} \rangle \top \right) \rightarrow \text{BR}(\delta_i, \delta_{-i})$ by 8, 9, 10, 11 and 13;

15. $\vdash_{\mathcal{MLEG}} \left( \left( \bigwedge_{i \in Agt} \text{Rat}_i \right) \wedge \bigwedge_{i \in Agt} K_i \langle \delta_{-i} \rangle \top \right) \rightarrow \text{Nash}(\delta)$ by 14 and Boolean principles.

□

### A.6. *Proof of Theorem 7*

For all $\delta \in \Delta$, $\vdash_{\mathcal{MLEG}} \left( (\text{MK}_{Agt}^n \wedge \bigwedge_{i \in Agt} \text{Rat}_i) \wedge \langle \delta_C \rangle \top \right) \rightarrow \neg \text{SD}^{\le n}(\delta_C)$

*Proof.*

**Lemma 3.** $\vdash_{\mathcal{MLEG}} \text{SD}^{\le n}(i:a) \rightarrow K_j \text{SD}^{\le n}(i:a)$

*Proof.* The proof of the lemma consists in proving by induction on $n$ that $\vdash_{\mathcal{MLEG}} \text{SD}^{\le n}(i:a) \rightarrow K_j \text{SD}^{\le n}(i:a)$ and $\vdash_{\mathcal{MLEG}} \neg \text{SD}^{\le n}(i:a) \rightarrow K_j \neg \text{SD}^{\le n}(i:a)$. We leave the proof of these two *MLEG*-theorems based on Lemma 1 to the reader.

□

Basic case $n = 0$

Here we prove $\vdash_{\mathcal{MLEG}} \left( \left( \bigwedge_{i \in Agt} \text{Rat}_i \right) \wedge \langle \delta_C \rangle \top \right) \rightarrow \neg \text{SD}^{\le 0}(\delta_C)$.
1. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \langle\delta_C\rangle^\top \rightarrow \bigwedge_{i \in C} \langle\delta_i\rangle^\top$
by Axiom **JointAct**

2. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} K_i(\langle\beta_{-i}, i:b\rangle \le_i \langle\beta_{-i}, i : \delta_i\rangle) \rightarrow (\langle\beta_{-i}, i:b\rangle \le_i \langle\beta_{-i}, i : \delta_i\rangle)$
by Axiom T of $K_i$;

3. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \left( \left( \bigwedge_{i \in A_{gt}} \mathrm{Rat}_i \right) \wedge \langle\delta_C\rangle^\top \right) \rightarrow \langle\delta_i\rangle^\top \wedge \bigwedge_{b \in A_{\mathrm{Act}}} \left( \bigvee_{\beta \in \Delta} \left( \hat{K}_i \langle\beta_{-i}\rangle^\top \wedge (\langle\beta_{-i}, i:b\rangle \le_i \langle\beta_{-i}, i : \delta_i\rangle) \right) \right)$ if $c \in C$
By 1, 2, axiom T for $K_i$ and Boolean principles;

4. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \hat{K}_i \langle\beta_{-i}\rangle^\top \rightarrow \Diamond \langle\beta_{-i}\rangle^\top$
by **CompleteInfo** or (Lemma 1 considered as axioms plus axiom T for $\square$);

5. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \langle\delta_i\rangle^\top \rightarrow \Diamond \langle\delta_i\rangle^\top$
by Axiom T for $\square$;

6. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \langle\delta_i\rangle^\top \wedge \bigwedge_{b \in A_{\mathrm{Act}}} \left( \bigvee_{\beta \in \Delta} \left( \hat{K}_i \langle\beta_{-i}\rangle^\top \wedge (\langle\beta_{-i}, i:b\rangle \le_i \langle\beta_{-i}, i : \delta_i\rangle) \right) \right) \rightarrow \Diamond \langle\delta_i\rangle^\top \wedge \bigwedge_{b \in A_{\mathrm{Act}}} \left( \bigvee_{\beta \in \Delta} (\Diamond \langle\beta_{-i}\rangle^\top \wedge \langle\beta_{-i}, i:b\rangle \le_i \langle\beta_{-i}, i : \delta_i\rangle) \right)$
by 4, 5 and Boolean principles;

7. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \Diamond \langle\delta_i\rangle^\top \wedge \bigwedge_{b \in A_{\mathrm{Act}}} \left( \bigvee_{\beta \in \Delta} (\Diamond \langle\beta_{-i}\rangle^\top \wedge \langle\beta_{-i}, i:b\rangle \le_i \langle\beta_{-i}, i : \delta_i\rangle) \right) \rightarrow \Diamond \langle\delta_i\rangle^\top \wedge \bigwedge_{b \in A_{\mathrm{Act}}} \underbrace{\Diamond \langle i:b\rangle^\top \rightarrow \left( \bigvee_{\beta \in \Delta} (\Diamond \langle\beta_{-i}\rangle^\top \wedge \langle\beta_{-i}, i:b\rangle \le_i \langle\beta_{-i}, i : \delta_i\rangle) \right)}_{\neg\mathrm{SD}^{\le 0}(\delta_i)}$
by Boolean principles;

8. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \left( \left( \bigwedge_{i \in A_{gt}} \mathrm{Rat}_i \right) \wedge \langle\delta_C\rangle^\top \right) \rightarrow \neg\mathrm{SD}^{\le 0}(\delta_i)$ if $c \in C$
by 3, 6, 7 and Boolean principles;

9. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \left( \left( \bigwedge_{i \in A_{gt}} \mathrm{Rat}_i \right) \wedge \langle\delta_C\rangle^\top \right) \rightarrow \neg\mathrm{SD}^{\le 0}(\delta_C)$
by 8 and Boolean principles.

**Inductive case**

let $n \in \mathbb{N}$ and let us prove that if the theorem 7 is true for all $k \le n$ then it is true for $n + 1$.
1. $\vdash_{\mathcal{MLEG}} \left( \left( \mathrm{MK}_{\mathrm{Agt}}^{n+1} \wedge \bigwedge_{i \in \mathrm{Agt}} \mathrm{Rat}_i \right) \wedge \langle \delta_C \rangle \top \right) \rightarrow \left( \left( \mathrm{MK}_{\mathrm{Agt}}^n \wedge \bigwedge_{i \in \mathrm{Agt}} \mathrm{Rat}_i \right) \wedge \langle \delta_C \rangle \top \right)$
by Axiom T for $K_i$ plus Boolean principles;

2. $\vdash_{\mathcal{MLEG}} \left( \left( \mathrm{MK}_{\mathrm{Agt}}^n \wedge \bigwedge_{i \in \mathrm{Agt}} \mathrm{Rat}_i \right) \wedge \langle \delta_C \rangle \top \right) \rightarrow \neg \mathrm{SD}^{\le n}(\delta_C)$
by induction;

3. $\vdash_{\mathcal{MLEG}} \neg \mathrm{SD}^{\le n}(\delta) \rightarrow \neg \mathrm{SD}^{\le n}(\delta_i)$
by Definition of $\neg \mathrm{SD}^{\le n}(\delta)$ and Boolean principles;

4. $\vdash_{\mathcal{MLEG}} \left( \left( \mathrm{MK}_{\mathrm{Agt}}^{n+1} \wedge \bigwedge_{i \in \mathrm{Agt}} \mathrm{Rat}_i \right) \wedge \langle \delta_C \rangle \top \right) \rightarrow \neg \mathrm{SD}^{\le n}(\delta_i)$
by 1, 2, 3;

5. $\vdash_{\mathcal{MLEG}} \left( \left( \mathrm{MK}_{\mathrm{Agt}}^{n+1} \wedge \bigwedge_{i \in \mathrm{Agt}} \mathrm{Rat}_i \right) \wedge \langle \delta_C \rangle \top \right) \rightarrow \mathrm{Rat}_i \wedge K_i \mathrm{MK}_{\mathrm{Agt}}^n \mathrm{Rat}_i \wedge \langle \delta_C \rangle \top$;
by Boolean principles

6. $\vdash_{\mathcal{MLEG}} \mathrm{Rat}_i \wedge K_i \mathrm{MK}_{\mathrm{Agt}}^n \mathrm{Rat}_i \wedge \langle \delta_C \rangle \top$
$\rightarrow \bigwedge_{b \in \mathrm{Act}} \mathrm{V}_{\beta \in \Delta} (\hat{K}_i \langle \beta_{-i} \rangle \top \wedge (\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, \delta_i \rangle) \wedge K_i \mathrm{MK}_{\mathrm{Agt}}^n \mathrm{Rat}_i \text{ if } i \in C$
by **JointAct**, definition of $\mathrm{Rat}_i$ and Boolean principles;

7. $\vdash_{\mathcal{MLEG}} \bigwedge_{b \in \mathrm{Act}} \mathrm{V}_{\beta \in \Delta} (\hat{K}_i \langle \beta_{-i} \rangle \top \wedge (\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, \delta_i \rangle) \wedge K_i \mathrm{MK}_{\mathrm{Agt}}^n \mathrm{Rat}_i$
$\rightarrow \bigwedge_{b \in \mathrm{Act}} \mathrm{V}_{\beta \in \Delta} (\hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i \mathrm{MK}_{\mathrm{Agt}}^n \mathrm{Rat}_i \wedge (\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, \delta_i \rangle))$
by distributivity of $\wedge$ over $\mathrm{V}_{\beta \in \Delta}$;

8. $\vdash_{\mathcal{MLEG}} \hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i \mathrm{MK}_{\mathrm{Agt}}^n \mathrm{Rat}_i \rightarrow \hat{K}_i (\langle \beta_{-i} \rangle \top \wedge \mathrm{MK}_{\mathrm{Agt}}^n \mathrm{Rat}_i)$
by modal logic K principle "$\hat{K}_i A \wedge K_i B \rightarrow \hat{K}_i (A \wedge B)$";

9. $\vdash_{\mathcal{MLEG}} (\langle \beta_{-i} \rangle \top \wedge \mathrm{MK}_{\mathrm{Agt}}^n \mathrm{Rat}_i) \rightarrow \neg \mathrm{SD}^{\le n}(\beta_{-i})$
by induction;

10. $\vdash_{\mathcal{MLEG}} K_i ((\langle \beta_{-i} \rangle \top \wedge \mathrm{MK}_{\mathrm{Agt}}^n \mathrm{Rat}_i) \rightarrow \neg \mathrm{SD}^{\le n}(\beta_{-i}))$
by necessitation rule on 9;

11. $\vdash_{\mathcal{MLEG}} \hat{K}_i (\langle \beta_{-i} \rangle \top \wedge \mathrm{MK}_{\mathrm{Agt}}^n \mathrm{Rat}_i) \rightarrow \hat{K}_i \neg \mathrm{SD}^{\le n}(\beta_{-i})$
by modal logic K principles applied on 10;

12. $\vdash_{\mathcal{MLEG}} \hat{K}_i \neg \mathrm{SD}^{\le n}(\beta_{-i}) \rightarrow \neg \mathrm{SD}^{\le n}(\beta_{-i})$ by Lemma A.6;

13. $\vdash_{\mathcal{MLEG}} \hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i \mathrm{MK}_{\mathrm{Agt}}^n \mathrm{Rat}_i \rightarrow \neg \mathrm{SD}^{\le n}(\beta_{-i})$
from 8, 11 and 12;

14. $\vdash_{\mathcal{MLEG}} \bigwedge_{b \in \mathrm{Act}} \mathrm{V}_{\beta \in \Delta} (\hat{K}_i \langle \beta_{-i} \rangle \top \wedge K_i \mathrm{MK}_{\mathrm{Agt}}^n \mathrm{Rat}_i \wedge (\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, \delta_i \rangle)$
$\rightarrow \bigwedge_{b \in \mathrm{Act}} \mathrm{V}_{\beta \in \Delta} (\neg \mathrm{SD}^{\le n}(\beta_{-i}) \wedge (\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i: \delta_i \rangle))$
by 13 and Boolean principles;
15. $\vdash_{\mathcal{MLEG}} \bigwedge_{b \in Act} \bigvee_{\beta \in \Delta} (\neg \mathrm{SD}^{\le n}(\beta_{-i}) \wedge (\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, i:\delta_i \rangle)) \rightarrow \bigwedge_{b \in Act} (\neg \mathrm{SD}^{\le n}(i:b) \rightarrow \bigvee_{\beta \in \Delta} (\neg \mathrm{SD}^{\le n}(\beta_{-i}) \wedge (\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, \delta_i \rangle)))$
by Boolean principles;

16. $\vdash_{\mathcal{MLEG}} \left( (\mathrm{MK}_{Agt}^{n+1} \bigwedge_{i \in Agt} \mathrm{Rat}_i) \wedge \langle \delta_C \rangle \top \right) \rightarrow \bigwedge_{b \in Act} (\neg \mathrm{SD}^{\le n}(i:b) \rightarrow \bigvee_{\beta \in \Delta} (\neg \mathrm{SD}^{\le n}(\beta_{-i}) \wedge (\langle \beta_{-i}, i:b \rangle \le_i \langle \beta_{-i}, \delta_i \rangle))) \text{ if } c \in C$
by 5, 6, 7, 14, 15;

17. $\vdash_{\mathcal{MLEG}} \left( (\mathrm{MK}_{Agt}^{n+1} \bigwedge_{i \in Agt} \mathrm{Rat}_i) \wedge \langle \delta_C \rangle \top \right) \rightarrow \neg \mathrm{SD}^{\le n+1}(\delta_i) \text{ if } c \in C$
by 4 and 16;

18. $\vdash_{\mathcal{MLEG}} \left( (\mathrm{MK}_{Agt}^{n+1} \bigwedge_{i \in Agt} \mathrm{Rat}_i) \wedge \langle \delta_C \rangle \top \right) \rightarrow \neg \mathrm{SD}^{\le n+1}(\delta_C)$
by 17.

□

### A.7. Proof of Theorem 8

Consider an arbitrary $\mathcal{MLEG}$-model $M = \langle W, \sim, R, E, \preceq, \pi \rangle$, a world $w$ in $M$ and $\delta \in \Delta$ such that for all positive integers $n$ we have $M, w \models \langle \delta \rangle \top \wedge \neg \mathrm{SD}^{\le n}(\delta)$. Then, there is a model $M' = \langle W, \sim, R, E', \preceq, \pi \rangle$ such that for all positive integers $n$ we have $M', w \models \mathrm{MK}_{Agt}^n \bigwedge_{i \in Agt} \mathrm{Rat}_i$.

*Proof.* The proof is based on the following Lemma 4.

**Lemma 4.** For all $\delta \in \Delta$, we have

$$ \vdash_{\mathcal{MLEG}} \neg \mathrm{SD}^{\le n}(i:a) \leftrightarrow \\ (\neg \mathrm{SD}^{\le n-1}(i:a) \wedge \bigwedge_{b \in Act} \bigvee_{\delta \in \Delta} (\neg \mathrm{SD}^{\le n-1}(\delta_{-i}) \wedge (\langle \delta_{-i}, i:b \rangle \le_i \langle \delta_{-i}, i:a \rangle))). $$

In other words, player $i$'s strategy $a$ survives after $n$ rounds of IDSDS if and only if, $a$ survives after $n-1$ rounds of IDSDS and in the subgame of depth $n$, for every alternative strategy $b$ of $i$, there is a joint action $\delta_{-i}$ of the other agents that survives after $n-1$ rounds of IDSDS such that playing $a$ while the others play $\delta_{-i}$ is for $i$ at least as good as playing $b$ while the others play $\delta_{-i}$.

Lemma 4 ensures that the definition of $\mathrm{SD}^{\le n}(i:a)$ can be rewritten in the following shorter equivalent form:

$$ \mathrm{SD}^{\le n}(i:a) \stackrel{\text{def}}{=} \neg \mathrm{SD}^{\le n-1}(i:a) \rightarrow \\ \bigvee_{b \in Act} \bigwedge_{\delta \in \Delta} (\neg \mathrm{SD}^{\le n-1}(\delta_{-i}) \rightarrow (\langle \delta_{-i}, i:a \rangle <_i \langle \delta_{-i}, i:b \rangle)). $$

Let us consider $w$ such that for all positive integers $n$, $M, w \models \langle \delta \rangle \top \wedge \neg \mathrm{SD}^{\le n}(\delta)$. We can now show how to build the accessibility relations $E'_i$ of the model $M'$ in such a way that for all positive integers $n$ $M', w \models \mathrm{MK}_{Agt}^n \bigwedge_{i \in Agt} \mathrm{Rat}_i$. The construction goes as follows.

For all positive integers $n$, let $A_n$ be the subset of all joint actions $\beta \in \Delta$ such that $M, w \models \neg \mathrm{SD}^{\le n}(\beta)$. As $\models_{\mathcal{MLEG}} \neg \mathrm{SD}^{\le n+1}(\beta) \rightarrow \neg \mathrm{SD}^{\le n}(\beta)$, we have $A_{n+1} \subseteq A_n$. Let us define $A_\infty = \bigcap_{n \in \mathbb{N}} A_n$. As $\Delta$
is finite, there exists a positive integer $n_0$ such that $A_\infty = A_{n_0}$ and for all positive integers $n > n_0$, $A_n = A_{n_0}$. Let $\Omega$ be the set of all worlds $u$ such that $u \sim w$ and such that there exists $\beta \in A_\infty$ such that $M, u \models \langle\beta\rangle^\top$. Note that $w \in \Omega$.

For all $i \in Agt$, we define $E'_i$ as follows:

* for all $s, t \in W$, $sE'_it$ iff either $s, t \in \Omega$ and $R_i(s) = R_i(t)$ or $s = t$.

Now, let us prove that for all $i \in Agt$, for all $s \in \Omega$, we have $M', s \models \mathrm{Rat}_i$. Let $a \in \mathrm{Act}$ be such that $s \models \langle i:a \rangle^\top$. As $s \in \Omega$, we have $M', s \models \neg\mathrm{SD}^{\le n_0+1}(i:a)$. By Lemma 4, it implies that for all $b \in \mathrm{Act}$, there exists $\beta \in \Delta$ such that $M', s \models \neg\mathrm{SD}^{\le n_0}(\beta_{-i})$ and $\langle\beta_{-i}, i:b\rangle \le_i \langle\beta_{-i}, i:a\rangle$. But by definition of $E'_i$, we have equivalence between $M', s \models \hat{\mathrm{K}}_i\langle\beta_{-i}\rangle^\top$ and $M', s \models \neg\mathrm{SD}^{\le n_0}(\beta_{-i})$. So for all $s \in \Omega$, we have $M', s \models \mathrm{Rat}_i$. As for all $i \in Agt$ we have $E'_i(w) = \Omega$, we obtain $M', w \models \mathrm{MK}^n_{Agt} \bigwedge_{i \in Agt} \mathrm{Rat}_i$ for all positive integers $n$. $\square$

### A.8. *Proof of Theorem 9*

If $M$ is a $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}$ model then $M^\chi$ is a $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}$ model.

*Proof.* It is just a routine to verify that $\sim^\chi$ and every $E_i^\chi$ are equivalence relations, every $\le_i^\chi$ is reflexive and transitive, and the model $M^\chi$ satisfies the semantic constraints **C1**, **C4**, **C5** and **C6**.

Let us prove that $M^\chi$ satisfies constraints **C2** and **C3**.

We first prove that $M^\chi$ satisfies constraint **C2**. We introduce the following useful notation. Suppose $\chi_1, \chi_2 \in \mathcal{L}_{\mathcal{G}\mathcal{T}}$. Then, $\chi_2 \rightsquigarrow \chi_3$ iff there is $\chi_3 \in \mathcal{L}_{\mathcal{G}\mathcal{T}}$ such that $\chi_1 = \chi_2 \wedge \chi_3$.

Now, suppose for every $i \in Agt$ there is $v_i$ such that $v_i \sim^\chi w$ and $R_i^\chi(v_i) = \delta_i$. It follows that for every $i \in Agt$ there is $v_i$ such that $v_i \sim w$ and $R_i(v_i) = \delta_i$. The latter implies that there is $v$ such that $v \sim w$ and $R_\delta(v) \neq \emptyset$ (by the semantic constraint **C2**). Now, suppose for all $v'$ if $v' \sim^\chi w$ then $R_{Agt}^\chi(v') = \delta$. It follows that: there is $i \in Agt$ and $\psi \in \mathcal{L}_{\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}}$ such that $\Box\psi \rightarrow [\delta_i] \perp \rightsquigarrow \chi$ and $M, v \models \Box\psi$. The latter implies that there is $i \in Agt$ and $\psi \in \mathcal{L}_{\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}}$ such that $\Box\psi \rightarrow [\delta_i] \perp \rightsquigarrow \chi$ and for all $v' \sim w, M, v' \models \Box\psi$. We conclude that there is no $v_i \sim^\chi w$ such that $R_i^\chi(v_i) = \delta_i$ which leads to a contradiction.

We now consider constraint **C3**. Suppose $wE_i^\chi v$ and $R_i^\chi(w) = i:a$. It follows that $wE_i v$ and $R_i(w) = i:a$ which implies $R_i(v) = i:a$, because $M$ satisfies constraint **C3**. The latter implies $R_i^\chi(v) = i:a$. Now, suppose $wE_i^\chi v$ and $R_i^\chi(v) = i:a$. It follows that $wE_i v$ and $R_i(v) = i:a$ which implies $R_i(w) = i:a$, because $M$ satisfies constraint **C3**. The latter implies $R_i^\chi(w) = i:a$. $\square$

### A.9. *Proof of Theorem 10*

*Proof.* The proofs of **R1-R6** go as in Dynamic Epistemic Logic (DEL) (see [10]). We here prove **R7**.

$M, w \models [\chi!] [\delta_C] \varphi,$

IFF if $M, w \models \chi$ then $M^\chi, w \models [\delta_C] \varphi,$

IFF if $M, w \models \chi$ then $M^\chi, w \models \langle\delta_C\rangle^\top \rightarrow \varphi$ (by Axiom **Def**$_{[\delta_C]}$),

IFF if $M, w \models \chi$ then $M^\chi, w \models [\delta_C] \perp$ or $M^\chi, w \models \varphi,$

IFF if $M^\chi, w \models \langle\delta_C\rangle^\top$ then, if $M, w \models \chi$ then $M^\chi, w \models \varphi,$
IFF if $M^{\chi}, w \models \langle\delta_C\rangle^{\top}$ then, $M, w \models [\chi!]\varphi$,

IFF if $M, w \models \langle\delta_C\rangle^{\top}$ then, $M, w \models [\chi!]\varphi$,

IFF if $M, w \models \langle\delta_C\rangle^{\top} \rightarrow [\chi!]\varphi$.

☐

### A.10. *Proof of Theorem 11*

The logic $\mathcal{MLEG}^{GT}$ is completely axiomatized by the axioms and inference rules of $\mathcal{MLEG}$ together with the schemata of Theorem 10.

*Proof.* By means of the principles **R1-R7** in Theorem 10, it is straightforward to prove that for every $\mathcal{MLEG}^{GT}$ formula there is an equivalent $\mathcal{MLEG}$ formula. In fact, each reduction axiom **R2-R7**, when applied from the left to the right by means of the rule of replacement of proved equivalence, yields a simpler formula, where 'simpler' roughly speaking means that the dynamic operator is pushed inwards. Once the dynamic operator attains an atom it is eliminated by the equivalence **R1**. Hence, the completeness of $\mathcal{MLEG}^{GT}$ is a straightforward consequence of Theorem 1. ☐

### A.11. *Proof of Theorem 12*

For all $\delta \in \Delta$, for all $n \ge 0$,
$$ \vdash_{\mathcal{MLEG}^{GT}} \langle\delta\rangle^{\top} \rightarrow (\neg\mathbf{SD}^{\le n}(\delta) \leftrightarrow \langle\chi_{\mathbf{SD}!}\rangle^{n+1}\top). $$

**Lemma 5.** $\vdash_{\mathcal{MLEG}} \bigvee_{a \in A_{\mathbf{ct}}} \neg\mathbf{SD}^{\le 0}(i:a)$.

*Proof.*
1. $\vdash_{\mathcal{MLEG}} \bigvee_{a_1 \in A_{\mathbf{ct}}} \langle i: a_1 \rangle^{\top}$
by **Active**;

2. $\vdash_{\mathcal{MLEG}} \bigvee_{a_1 \in A_{\mathbf{ct}}} \diamond\langle i: a_1 \rangle^{\top}$
by 1 and T for ☐ and Boolean principles;

3. $\vdash_{\mathcal{MLEG}} \bigvee_{\beta \in \Delta} \langle\beta_{-i}\rangle^{\top}$
by **Active**;

4. $\vdash_{\mathcal{MLEG}} \bigvee_{\beta \in \Delta} \diamond\langle\beta_{-i}\rangle^{\top}$
by 3;

5. $\vdash_{\mathcal{MLEG}} \bigwedge_{a \in A_{\mathbf{ct}}} \mathbf{SD}^{\le 0}(i:a) \rightarrow \bigwedge_{a \in A_{\mathbf{ct}}} \mathbf{SD}^{\le 0}(i:a) \wedge \bigvee_{a \in A_{\mathbf{ct}}} \diamond\langle i:a \rangle^{\top} \wedge \bigvee_{\beta \in \Delta} \diamond\langle \beta_{-i} \rangle^{\top}$
by 2 and 4;

6. $\vdash_{\mathcal{MLEG}} \diamond\langle\beta_{-i}\rangle^{\top} \wedge \mathbf{SD}^{\le 0}(i:a) \wedge \diamond\langle i:a \rangle^{\top} \rightarrow \bigvee_{b \in A_{\mathbf{ct}}} (\langle\beta_{-i}, i:a\rangle <_i \langle\beta_{-i}, i:b\rangle \wedge \diamond\langle i:b \rangle^{\top})$
by Definition $\mathbf{SD}^{\le 0}(i:a)$ and Boolean principles;

7. $\vdash_{\mathcal{MLEG}} \diamond\langle\beta_{-i}\rangle^{\top} \wedge \bigwedge_{a \in A_{\mathbf{ct}}} \mathbf{SD}^{\le 0}(i:a) \wedge \diamond\langle i:a \rangle^{\top}$
$$ \rightarrow \bigvee_{b \in A_{\mathbf{ct}}} (\langle\beta_{-i}, i:a\rangle <_i \langle\beta_{-i}, i:b\rangle \wedge \diamond\langle\beta_{-i}\rangle^{\top} \wedge \bigwedge_{a \in A_{\mathbf{ct}}} \mathbf{SD}^{\le 0}(i:a) \wedge \diamond\langle i:b\rangle^{\top}) $$
by 6 and Boolean principles to propagate $\bigwedge_{a \in A_{\mathbf{ct}}} \mathbf{SD}^{\le 0}(i:a);$
8. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \Diamond\langle\beta_{-i}\rangle\top \wedge \bigwedge_{a\in Act} \mathrm{SD}^{\le 0}(i:a) \wedge \Diamond\langle i:a\rangle\top$
$$ \rightarrow \bigvee_{b_1\in Act} \bigvee_{b_2\in Act} \dots \bigvee_{b_n\in Act} \langle\beta_{-i}, i:a\rangle <_i \langle\beta_{-i}, i:b_1\rangle \langle\beta_{-i}, i:b_1\rangle <_i \langle\beta_{-i}, i:b_2\rangle \dots $$
$$ \qquad \langle\beta_{-i}, i:b_{n-1}\rangle <_i \langle\beta_{-i}, i:b_n\rangle \text{ for all } n \ge 1; $$
by 7 and Boolean principles (induction on n);

9. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \bigvee_{b_1\in Act} \bigvee_{b_2\in Act} \dots \bigvee_{b_n\in Act} \langle\beta_{-i}, i:a\rangle <_i \langle\beta_{-i}, i:b_1\rangle \langle\beta_{-i}, i:b_1\rangle <_i \langle\beta_{-i}, i:b_2\rangle \dots$
$$ \langle\beta_{-i}, i:b_{n-1}\rangle <_i \langle\beta_{-i}, i:b_n\rangle $$
$\rightarrow \bigvee_{b\in Act} \langle\beta_{-i}, i:b\rangle <_i \langle\beta_{-i}, i:b\rangle \text{ if } n > \mathrm{card}(Agt)$
by Boolean principles and because $<_i$ is transitive (as $n > \mathrm{card}(Agt)$, all sequence $b_1, \dots, b_n$ are such that there exists $i \neq j$ such that $b_i = b_j$);

10. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \langle\beta_{-i}, i:b\rangle <_i \langle\beta_{-i}, i:b\rangle \rightarrow \bot$
by Definition of $<_i$ and Boolean principles;

11. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \Diamond\langle\beta_{-i}\rangle\top \wedge \bigwedge_{a\in Act} \mathrm{SD}^{\le 0}(i:a) \wedge \Diamond\langle i:a\rangle\top \rightarrow \bot$
by 8, 9, 10;

12. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \bigwedge_{a\in Act} \mathrm{SD}^{\le 0}(i:a) \wedge \bigvee_{a\in Act} \Diamond\langle i:a\rangle\top \wedge \bigvee_{\beta\in\Delta} \Diamond\langle\beta_{-i}\rangle\top \rightarrow \bot$
by 11 and Boolean principles;

13. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \bigwedge_{a\in Act} \mathrm{SD}^{\le 0}(i:a) \rightarrow \bot$
by 5 and 12;

14. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}} \bigvee_{a\in Act} \neg\mathrm{SD}^{\le 0}(i:a)$
by 13 and Boolean principle.

□

**Lemma 6.** $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \neg\mathrm{SD}^{\le n}(i:a) \wedge \chi_{\mathrm{SD}} \leftrightarrow \langle\chi_{\mathrm{SD}}!\rangle\neg\mathrm{SD}^{\le n-1}(i:a)$.

*Proof.* We prove it by induction. Let us consider the case $n = 0$ where $\neg\mathrm{SD}^{\le -1}(i:a) = \Diamond\langle i:a\rangle\top$ by convention.
1. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \neg\mathbf{SD}^{\le 0}(i:a) \rightarrow \diamond\langle i:a\rangle^\top$
by Definition of $\neg\mathbf{SD}^{\le 0}(i:a)$ and Boolean principles;

2. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \bigwedge_{j \in A_{gt}} \bigvee_{b \in A_{ct}} \neg\mathbf{SD}^{\le 0}(j:b)$
by Lemma 5 and Boolean principles;

3. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \bigwedge_{j \in A_{gt}} \bigvee_{b \in A_{ct}} \neg\mathbf{SD}^{\le 0}(j:b) \leftrightarrow \bigwedge_{j \in A_{gt}} \bigvee_{b \in A_{ct}} \neg\mathbf{SD}^{\le 0}(j:b) \wedge \diamond\langle j:b\rangle^\top$
by 1 and Boolean principles;

4. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \bigwedge_{j \in A_{gt}} \bigvee_{b \in A_{ct}} \neg\mathbf{SD}^{\le 0}(j:b) \wedge \diamond\langle j:b\rangle^\top$
by 2 and 3;

5. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \neg\mathbf{SD}^{\le 0}(i:a) \wedge \chi_{\mathbf{SD}} \leftrightarrow \neg\mathbf{SD}^{\le 0}(i:a) \wedge \chi_{\mathbf{SD}} \wedge \diamond\langle i:a\rangle^\top$
by 1 and Boolean principles;

6. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \neg\mathbf{SD}^{\le 0}(i:a) \wedge \chi_{\mathbf{SD}} \wedge \diamond\langle i:a\rangle^\top \leftrightarrow \neg\mathbf{SD}^{\le 0}(i:a) \wedge \chi_{\mathbf{SD}} \wedge \diamond\langle i:a\rangle^\top \wedge \bigwedge_{j \in A_{gt}} \bigvee_{b \in A_{ct}} \neg\mathbf{SD}^{\le 0}(j:b) \wedge \diamond\langle j:b\rangle^\top$
by 4 and Boolean principles;

7. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \neg\mathbf{SD}^{\le 0}(i:a) \wedge \chi_{\mathbf{SD}} \wedge \diamond\langle i:a\rangle^\top \wedge \bigwedge_{j \in A_{gt}} \bigvee_{b \in A_{ct}} \neg\mathbf{SD}^{\le 0}(j:b) \wedge \diamond\langle j:b\rangle^\top$
$\rightarrow \chi_{\mathbf{SD}} \wedge \bigvee_{\beta \in \Delta} (\neg\mathbf{SD}^{\le 0}(\beta_{-i}, i:a) \wedge \diamond\langle \beta_{-i}, i:a\rangle^\top)$
by Boolean principles and **Indep**;

8. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \chi_{\mathbf{SD}} \wedge \bigvee_{\beta \in \Delta} (\neg\mathbf{SD}^{\le 0}(\beta_{-i}, i:a) \wedge \diamond\langle \beta_{-i}, i:a\rangle^\top)$
$\rightarrow \chi_{\mathbf{SD}} \wedge \bigvee_{\beta \in \Delta} \diamond(\neg\mathbf{SD}^{\le 0}(\beta_{-i}, i:a) \wedge \langle \beta_{-i}, i:a\rangle^\top)$
by Proposition 1 and K(□) principles;

9. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \chi_{\mathbf{SD}} \wedge \bigvee_{\beta \in \Delta} \diamond(\neg\mathbf{SD}^{\le 0}(\beta_{-i}, i:a) \wedge \langle \beta_{-i}, i:a\rangle^\top)$
$\rightarrow \chi_{\mathbf{SD}} \wedge \bigvee_{\beta \in \Delta} \diamond(\chi_{\mathbf{SD}} \wedge \langle i:a\rangle^\top)$
by definitions of $\chi_{\mathbf{SD}}$, $\neg\mathbf{SD}^{\le 0}(\beta_{-i}, i:a)$, **JointAct** and Boolean principles;

10. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \langle\chi_{\mathbf{SD}}!\rangle\langle i:a\rangle^\top \leftrightarrow \langle i:a\rangle^\top \wedge \chi_{\mathbf{SD}}$ by **R2.** and **R7**.

11. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \chi_{\mathbf{SD}} \wedge \bigvee_{\beta \in \Delta} \diamond(\chi_{\mathbf{SD}} \wedge \langle i:a\rangle^\top) \rightarrow \chi_{\mathbf{SD}} \wedge \diamond(\chi_{\mathbf{SD}} \wedge \langle i:a\rangle^\top)$;
by Boolean principles;

12. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \chi_{\mathbf{SD}} \wedge \diamond(\chi_{\mathbf{SD}} \wedge \langle i:a\rangle^\top) \leftrightarrow \chi_{\mathbf{SD}} \wedge \diamond(\langle\chi_{\mathbf{SD}}!\rangle\langle i:a\rangle^\top)$
by Boolean principles and 10;

13. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \chi_{\mathbf{SD}} \wedge \diamond(\langle\chi_{\mathbf{SD}}!\rangle\langle i:a\rangle^\top) \leftrightarrow \langle\chi_{\mathbf{SD}}!\rangle\diamond\langle i:a\rangle^\top$.
by **R2.** and **R4.**;

14. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{GT}} \neg\mathbf{SD}^{\le 0}(i:a) \wedge \chi_{\mathbf{SD}} \rightarrow \langle\chi_{\mathbf{SD}}!\rangle\neg\mathbf{SD}^{\le -1}(i:a)$
by 5, 6, 7, 8, 9, 11, 12, 13.
15. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} \langle\chi_{\text{SD}}!\rangle \neg\text{SD}^{\leq-1}(i:a) \rightarrow \chi_{\text{SD}} \wedge \diamond(\chi_{\text{SD}} \wedge \langle i:a \rangle \top)$
by 13, 12;

16. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} \langle i:a \rangle \top \wedge \chi_{\text{SD}} \rightarrow \neg\text{SD}^{\leq 0}(i:a) \wedge \chi_{\text{SD}}$;
by Definition of $\chi_{\text{SD}}$ and Boolean principles;

17. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} \chi_{\text{SD}} \wedge \diamond(\chi_{\text{SD}} \wedge \langle i:a \rangle \top) \rightarrow \chi_{\text{SD}} \wedge \diamond \neg \text{SD}^{\leq 0}(i:a)$
by 16, modal logic K(□) principles and Boolean principles;

18. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} \diamond \neg \text{SD}^{\leq 0}(i:a) \wedge \chi_{\text{SD}} \rightarrow \neg \text{SD}^{\leq 0}(i:a) \wedge \chi_{\text{SD}}$
by $\diamond \neg \text{SD}^{\leq 0}(i:a) \leftrightarrow \neg \text{SD}^{\leq 0}(i:a)$;

19. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} \langle\chi_{\text{SD}}!\rangle \neg\text{SD}^{\leq-1}(i:a) \rightarrow \neg\text{SD}^{\leq 0}(i:a) \wedge \chi_{\text{SD}}$
by 15, 17, 18;

20. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} \neg\text{SD}^{\leq 0}(i:a) \wedge \chi_{\text{SD}} \leftrightarrow \langle\chi_{\text{SD}}!\rangle \neg\text{SD}^{\leq-1}(i:a)$
by 14 and 19.

Now let us consider the inductive case.
1. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} \neg\mathrm{SD}^{\le n}(\delta) \rightarrow \neg\mathrm{SD}^{\le n-1}(\delta)$
by definition of $\neg\mathrm{SD}^{\le n}(\delta)$ and Boolean principles;

2. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} \neg\mathrm{SD}^{\le n}(\delta) \rightarrow \neg\mathrm{SD}^{\le 0}(\delta)$
by 1 and Boolean principles (induction on $n$);

3. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} \neg\mathrm{SD}^{\le 0}(\delta) \wedge (\delta)\top \rightarrow \chi_{\mathrm{SD}}$
by Boolean principles (see definition of $\chi_{\mathrm{SD}}$);

4. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} (\delta)\top \wedge \chi_{\mathrm{SD}} \leftrightarrow (\chi_{\mathrm{SD}}!) (\delta)\top$
by rule **R7.**;

5. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} (\delta)\top \wedge \neg\mathrm{SD}^{\le n}(\delta) \wedge \chi_{\mathrm{SD}} \rightarrow (\chi_{\mathrm{SD}}!) ((\delta)\top \wedge \neg\mathrm{SD}^{\le n-1}(\delta) \wedge \chi_{\mathrm{SD}})$
by 3, 4, Lemma 6, **R2.** and **R3.**;

6. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} (\delta)\top \wedge \neg\mathrm{SD}^{\le n}(\delta) \wedge \chi_{\mathrm{SD}} \rightarrow (\chi_{\mathrm{SD}}!)^{n+1} ((\delta)\top)$
by induction with 5;

7. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} (\delta)\top \wedge (\chi_{\mathrm{SD}}!)^{n+1}\top \rightarrow (\chi_{\mathrm{SD}}!)((\delta)\top \wedge (\chi_{\mathrm{SD}}!)^n\top)$
by rule **R2.** and **R3.**;

8. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} (\delta)\top \wedge (\chi_{\mathrm{SD}}!)^{n+1}\top \rightarrow (\chi_{\mathrm{SD}}!)^{n+1} (\delta)\top$
by 7 and induction;

9. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} (\chi_{\mathrm{SD}}!)^{n+1} (\delta)\top \rightarrow (\chi_{\mathrm{SD}}!)^{n+1} \diamond (\delta)\top$
by **R2.**, **R4.** and T for $\square$ and Boolean principles;

10. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} (\chi_{\mathrm{SD}}!)^{n+1} \diamond (\delta)\top \rightarrow \neg\mathrm{SD}^{\le n}(\delta)$
by Lemma 6 and induction;

11. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} (\delta)\top \rightarrow (\neg\mathrm{SD}^{\le n}(\delta) \rightarrow (\chi_{\mathrm{SD}}!)^{n+1}\top)$
by 2, 3, 6;

12. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} (\delta)\top \rightarrow ((\chi_{\mathrm{SD}}!)^{n+1}\top \rightarrow \neg\mathrm{SD}^{\le n}(\delta))$
by 8, 9, 10;

13. $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} (\delta)\top \rightarrow ((\chi_{\mathrm{SD}}!)^{n+1}\top \leftrightarrow \neg\mathrm{SD}^{\le n}(\delta))$
by 11 and 12.

□

A.12. *Proof of Theorem 13.*

For all $n \ge 0$, $\vdash_{\mathcal{ML}\mathcal{E}\mathcal{G}^{\text{GT}}} (\mathrm{MK}_{Agt}^n \wedge_{i \in Agt} \mathrm{Rat}_i) \rightarrow (\chi_{\mathrm{SD}}!)^{n+1}\top$.
*Proof.* By Theorem 7, Theorem 12 and Boolean principles. $\square$

### A.13. *Proof of Theorem 14*

The satisfiability problem of a given formula $\varphi$ in a $\mathcal{M}L\mathcal{E}\mathcal{G}^*$-model is PSPACE-hard.

*Proof.* Let us prove that the satisfiability problem of $\mathcal{M}L\mathcal{E}\mathcal{G}^*$ is PSPACE-hard. Let $i$ be an agent. Let us consider a formula $\varphi$ written only with atomic propositions and with modal operators $\square$ and $K_i$. We have equivalence between:

1. $\varphi$ is satisfiable in a $\mathcal{M}L\mathcal{E}\mathcal{G}^*$-model;

2. $\varphi$ is satisfiable in a model of the logic $S5_2(\square, K_i)$ (i.e. the fusion of the logic S5 for $\square$ and S5 for $K_i$).

Hence, we have reduced the satisfiability problem of a given formula $\varphi$ in a $\mathcal{M}L\mathcal{E}\mathcal{G}^*$-model to the satisfiability problem of a given formula $\varphi$ of $S5_2(\square, K_i)$ which is PSPACE-hard. So the satisfiability problem of a given formula $\varphi$ in a $\mathcal{M}L\mathcal{E}\mathcal{G}^*$-model is PSPACE-hard. $\square$

### A.14. *Proof of Theorem 15*

* If $card(Agt) = 1$ and $card(Act) = 1$ then the satisfiability problem of a given formula $\varphi$ in a $\mathcal{M}L\mathcal{E}\mathcal{G}^{det*}$-model is NP-complete.

* If $card(Agt) \geq 2$ or $card(Act) \geq 2$ the satisfiability problem of a given formula $\varphi$ in a $\mathcal{M}L\mathcal{E}\mathcal{G}^{det*}$-model is PSPACE-complete.

*Proof.* We give here some hint for the proof. When there is only one agent and $card(Act) = 1$ then the games are trivial and reduced to singletons. In these settings, a $\mathcal{M}L\mathcal{E}\mathcal{G}^{det*}$-frame $F = \langle W, \sim, R, E, \preceq \rangle$ is such that $\sim$ and $\preceq_i$ for each agent $i$ are equal to the relation $\{(w, w) | w \in W\}$. So the modal operators $[good]_i$ and $\square$ are superfluous. The operator $[\delta_C]$ can be treated as a proposition. Hence the logic is similar to the logic S5 which is NP. This is the main argument why when there is only one agent and $card(Act) = 1$ the logic $\mathcal{M}L\mathcal{E}\mathcal{G}^{det*}$ is NP. NP-hardness is granted because $\mathcal{M}L\mathcal{E}\mathcal{G}^{det*}$ is a conservative extension of Classical Propositional Logic.

Now let us prove that the satisfiability problem of a given formula $\varphi$ in a $\mathcal{M}L\mathcal{E}\mathcal{G}^{det*}$-model is PSPACE-hard in other cases. First let us consider the case where $card(Agt) \geq 2$. Let us consider two distinct agents $i, j \in Agt$. Let $\varphi$ be a formula written only with atomic propositions and with epistemic modal operators $K_i$ and $K_j$. We have equivalence between:

1. $\varphi$ is satisfiable in a $\mathcal{M}L\mathcal{E}\mathcal{G}^{det*}$-model;

2. $\varphi$ is satisfiable in the logic $S5_2(K_i, K_j)$ (i.e. the fusion of the logic S5 for $K_i$ and S5 for $K_j$).

The direction 1. $\rightarrow$ 2. is straightforward and is already true with the assumption of the Axiom **Complete-Info**. The direction 2. $\rightarrow$ 1. comes from the fact that the Constraint **C4** (corresponding to the Axiom **CompleteInfo**) has disappeared. So we can easily transform a model of the epistemic modal logic into
a $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\det*}$-model. Note that in the case of the logic $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\det}$, the direction 2. $\rightarrow 1.$ is not true any-
more. Indeed, it is not possible to transform a model of $S_2(K_a, K_b)$ with more than $card(Act)^{card(Agt)}$
worlds into a $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\det}$-model. Hence, we have reduced the satisfiability problem of a given formula
$\varphi$ in a $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\det*}$-model into the satisfiability problem of a given formula $\psi$ of $S_2(K_i, K_j)$ which is
PSPACE-hard. So the satisfiability problem of a given formula $\varphi$ in a $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\det*}$-model is PSPACE-
hard.

Now let us consider the case where $Agt = \{i\}$ and $card(Act) \ge 2$. Let $a$ and $b$ be two distinct
actions. We prove that we can reduce the satisfiability problem of a given formula $\varphi$ in a $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\det*}$-
model to the satisfiability problem of K. Here is a possible translation:

* $tr_0(\blacksquare\psi) = i:a \wedge \diamond K_i tr_1(\psi)$ where $\blacksquare$ is the K-operator;

* $tr_1(\blacksquare\psi) = i:b \wedge \diamond K_i tr_0(\psi)$ where $\blacksquare$ is the K-operator;

* $tr_0(p) = i:a \wedge p$ for all propositions $p$;

* $tr_1(p) = i:b \wedge p$ for all propositions $p$.

And $\varphi$ is satisfiable in K iff $tr_0(\varphi)$ is satisfiable in $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\det*}$. Hence, the logic $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\det*}$ is also
PSPACE-hard in this case.

Now we are going to prove that the satisfiability problem of $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^{\det*}$ is PSPACE. We do not give
all the details but we give the idea for a tableau method [21] for the logic $\mathcal{M}\mathcal{L}\mathcal{E}\mathcal{G}^*$. The tableau method
is a non-deterministic procedure. The creation of a model proceeds as follows:

* We start the procedure by guessing a "grid", that is to say an equivalence class for the relation $\sim$
of maximal size $card(Act)^{card(Agt)}$ and also its preference relation as in the algorithm of Theorem 2. We also choose non-deterministically a world $w$ in this class.

* We adapt the classical tableau method rules for the epistemic modal logic [21], that is to say:

- Suppose that a world $w$ contains a formula of the form $K_i\psi$. Then we propagate the formula $\psi$ in all nodes $v$ such that $wE_i v$.

- Suppose that a world $w$ contains a formula of the form $\hat{K}_i\psi$. Then we create an equivalence class for $\sim$, we choose a point $v$ such that $R_i(v) = R_i(w)$ in this equivalence class and we propagate $\psi$ in $v$.

* Suppose that a node $w$ contains a formula $\Box\psi$. Then we propagate the formula $\psi$ in all nodes $v$
such that $v \sim w$;

* Suppose that a node $w$ contains a formula $\diamond\psi$. Then we choose non-deterministically a world $v$
such that $v \sim w$ and we propagate $\psi$ in $v$.

* Suppose that a node $w$ contains a formula $[good]_i\varphi\psi$. Then we propagate the formula $\psi$ in all nodes $v$ such that $v \preceq_i w$;

* Suppose that a node $w$ contains a formula $\langle good \rangle_i\psi$. Then we choose non-deterministically a world $v$ such that $v \preceq_i w$ and we propagate $\psi$ in $v$.
During the construction, we explore the structure in depth first so that we only need to have one branch in memory at each step. Thus, the algorithm is a non-deterministic procedure that uses only a polynomial amount of memory. So the satisfiability problem of $\mathcal{MLEG}^{det*}$ is in NPSPACE. According to the Savitch's theorem [48], it is in PSPACE.

□

### A.15. *Proof of Theorem 16*

For every $w \in W$ and for every $i \in Agt$, $M, w \models Rat_i$ if and only if $M', w \models Rat_i$.

*Proof.* (⇒) We first prove the left-to-right direction. Suppose that $M, w \models \langle i:a \rangle \top$ and $M, w \models Rat_i$. The latter means that for every $b \in Act$ there is $\delta \in \Delta$ such that $M, w \models \hat{K}_i(\delta_{-i}) \top \wedge K_i(\langle \delta_{-i}, i:b \rangle \le_i \langle \delta_{-i}, i:a \rangle)$.

The latter means that for every $b \in Act$ there is $\delta \in \Delta$ such that:

A. there is $v \in E_i(w)$ such that $R'_{-i}(v) = \delta_{-i}$ and

B. for all $u, v \in W$ if $v \in E_i(w)$ and $u \sim v$ and $R_{Agt}(u) = \langle \delta_{-i}, i:b \rangle$ then there is $z \in W$ such that $u \preceq_i z$ and $R_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$.

Consider an arbitrary $b \in Agt$. It follows that there is an element $\delta$ of $\Delta$ which satisfies the previous conditions A and B. By definition of $E'_i(w)$ and $R'_{-i}(v)$ we have that: if there is $v \in E_i(w)$ such that $R'_{-i}(v) = \delta_{-i}$ then there is $v \in E'_i(w)$ such that $R'_{-i}(v) = \delta_{-i}$. Therefore, from item A, we conclude:

C. there is $v \in E'_i(w)$ such that $R'_{-i}(v) = \delta_{-i}$.

Take two arbitrary worlds $u, v \in W'$ and suppose that $v \in E'_i(w)$ and $u \sim' v$ and $R'_{Agt}(u) = \langle \delta_{-i}, i:b \rangle$. By definition of $M'$, we have $v \in E_i(w)$ and $\langle \delta_{-i}, i:a \rangle \in \Pi_M$. Consider now the following three cases.

**CASE 1.** Suppose $u \in W$. Then, by definition of $M'$, we have that $u \sim v$ and $R_{Agt}(u) = \langle \delta_{-i}, i:b \rangle$. Therefore, from item B, it follows that there is $z \in W$ such that $u \preceq_i z$ and $R_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$. From the latter, by definition of $M'$, we conclude that there is $z \in W'$ such that $u \preceq'_i z$ and $R'_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$.

**CASE 2.** Suppose that $u \notin W$ and that there is $z \in W$ such that $z \sim v$ and $R_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$. From the former, by definition of $M'$, it follows that $\preceq'_i(u) = \sim'(u)$. From the latter, by definition of $M'$, it follows that there is $z \in W'$ such that $z \sim' v$ and $R'_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$. Therefore, we have that there is $z \in W'$ such that $u \preceq'_i z$ and $R'_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$.

**CASE 3.** Suppose that $u \notin W$ and that there is no $z \in W$ such that $z \sim v$ and $R_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$. From the former, by definition of $M'$, it follows that $\preceq'_i(u) = \sim'(u)$. From the latter, by definition of $M'$ (and the fact that $\langle \delta_{-i}, i:a \rangle \in \Pi_M$), it follows that there is $z \in W'$ such that $z \sim' v$ and $R'_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$ and $\preceq'_i(z) = \sim'(z)$. Therefore, we have that there is $z \in W'$ such that $u \preceq'_i z$ and $R'_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$.

From the previous three cases, it follows that:

D. for all $u, v \in W'$ if $v \in E'_i(w)$ and $u \sim' v$ and $R'_{Agt}(u) = \langle \delta_{-i}, i:b \rangle$ then there is $z \in W'$ such that $u \preceq'_i z$ and $R'_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$.
From the items C and D we conclude that $M', w \models \mathrm{Rat}_i$.

($\Leftarrow$) Let us prove the right-to-left direction. Suppose that $M', w \models \langle i:a \rangle \top$ and $M', w \models \mathrm{Rat}_i$. The latter means that for every $b \in \mathrm{Act}$ there is $\delta \in \Delta$ such that $M', w \models \hat{\mathrm{K}}_i(\delta_{-i}) \top \wedge \mathrm{K}_i(\langle \delta_{-i}, i:b \rangle \le_i \langle \delta_{-i}, i:a \rangle)$.

The latter means that for every $b \in \mathrm{Act}$ there is $\delta \in \Delta$ such that:

E. there is $v \in E'_i(w)$ such that $R'_{-i}(v) = \delta_{-i}$ and

F. for all $u, v \in W'$ if $v \in E'_i(w)$ and $u \sim' v$ and $R'_{Agt}(u) = \langle \delta_{-i}, i:b \rangle$ then there is $z \in W'$ such that $u \preceq'_i z$ and $R'_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$.

Consider an arbitrary $b \in \mathrm{Agt}$. It follows that there is an element $\delta$ of $\Delta$ which satisfies the previous conditions E and F. By definition of $E'_i(w)$ and $R'_{-i}(v)$ we have that: if there is $v \in E'_i(w)$ such that $R'_{-i}(v) = \delta_{-i}$ then there is $v \in E_i(w)$ such that $R_{-i}(v) = \delta_{-i}$. Therefore, from item E, we conclude:

G. there is $v \in E_i(w)$ such that $R_{-i}(v) = \delta_{-i}$.

Take two arbitrary worlds $u, v \in W$ and suppose that $v \in E_i(w)$ and $u \sim v$ and $R_{Agt}(u) = \langle \delta_{-i}, i:b \rangle$. By Definition of $E'_i(w)$, $\sim'$ and $R'_{Agt}(u)$ we have $v \in E'_i(w)$ and $u \sim' v$ and $R'_{Agt}(u) = \langle \delta_{-i}, i:b \rangle$. Thus by F. there is $z \in W'$ such that $u \preceq'_i z$ and $R'_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$. But as $u \in W$ we have $\preceq'_i(u) = \preceq_i(u)$. Thus $z \in W$ and $R'_{Agt}(z) = R_{Agt}(z)$.

It follows that:

H. for all $u, v \in W$ if $v \in E_i(w)$ and $u \sim v$ and $R_{Agt}(u) = \langle \delta_{-i}, i:b \rangle$ then there is $z \in W$ such that $u \preceq_i z$ and $R_{Agt}(z) = \langle \delta_{-i}, i:a \rangle$.

From the items G and H we conclude that $M, w \models \mathrm{Rat}_i$.

□

### A.16. *Proof of Corollary 1*

For every $w \in W$, for every $i \in \mathrm{Agt}$ and for every $C \in 2^{Agt*}$, we have $M, w \models \mathrm{MK}_C^n \mathrm{Rat}_i$ if and only if $M', w \models \mathrm{MK}_C^n \mathrm{Rat}_i$.

*Proof.* Define a world $v$ to be *C-reachable from world w in n steps* (with $n \ge 1$), and note this $wE_{C,n}v$, if and only if there exist worlds $w_0, \dots, w_n$ such that $w_0 = w$ and $w_n = v$ and for all $0 \le k \le n-1$, there exists $i \in C$ such that $w_k E_i w_{k+1}$. Define $E_{C,n}(w) = \{v \mid wE_{C,n}v\}$. We have $M, w \models \mathrm{MK}_C^n \varphi$ if and only if $M, v \models \varphi$ for all $v \in E_{C,n}(w)$.

By definition of $M'$, we have $E_{C,n}(w) = E'_{C,n}(w)$ for all $w \in W$. Therefore, $M, w \models \mathrm{MK}_C^n \mathrm{Rat}_i$ if and only if $M, v \models \mathrm{Rat}_i$ for all $v \in E'_{C,n}(w)$.

Moreover, according to Proposition 16, for every $v \in W$ we have $M, v \models \mathrm{Rat}_i$ if and only if $M', v \models \mathrm{Rat}_i$. Therefore, we have that $M, v \models \mathrm{Rat}_i$ for all $v \in E'_{C,n}(w)$ if and only if $M', v \models \mathrm{Rat}_i$ for all $v \in E'_{C,n}(w)$.

It follows that, $M, w \models \mathrm{MK}_C^n \mathrm{Rat}_i$ if and only if $M', w \models \mathrm{MK}_C^n \mathrm{Rat}_i$.

□