# IJCAI–24 Formatting Instructions

Qi Shi University of Southampton<EMAIL_ADDRESS>
# Agentive Permissions in Multiagent Systems

Qi Shi University of Southampton<EMAIL_ADDRESS>
###### Abstract

This paper proposes to distinguish four forms of agentive permissions in
multiagent settings. The main technical results are the complexity analysis of
model checking, the semantic undefinability of modalities that capture these
forms of permissions through each other, and a complete logical system
capturing the interplay between these modalities.††This is the full version of
the IJCAI-24 conference paper of the same name. A technical appendix is
attached to the end.

##  1 Introduction

Imagine a large factory being built in a city on a river. The factory will
dump a pollutant into the river. It is known that a small factory located in
another city higher up the river already exists and can dump up to $60$g/day
of the same pollutant. Also, more than $100$g/day of the pollutant dumped into
the river combined by the two factories will kill the fish.

Suppose that the large factory will dump $20$g/day of the pollutant. Then, the
total dumped amount by both factories will not exceed $80$g/day no matter how
much the other factory dumps and thus the fish in the river will survive for
sure. In other words, the action that dumping $20$g/day ensures the survival
of the fish. On the contrary, if the large factory will dump $60$g/day of the
pollutant, then the fish will be killed once the other factory dumps more than
$40$g/day. That is to say, the action that dumping $60$g/day does not ensure
the survival of the fish. However, it still leaves the possibility for the
fish to survive, e.g. when the other factory dumps no more than $40$g/day. In
this situation, we say that the action that dumping $60$g/day admits of the
survival of the fish.

To ensure and to admit show two different types of agency of an action. The
difference comes from that, in multiagent or non-deterministic settings, the
effect of an action of one agent might be affected by the actions of other
agents or the nondeterminacy. It is worth noting that, admitting is the dual
of ensuring. To be specific, if an action of an agent ensures an outcome, then
the action does not admit of the opposite outcome, and vice versa. It is easy
to see that their meanings coincide in single-agent deterministic settings.

In this paper, we consider the two types of agency together with permissions.
Let us come back to the large factory. Suppose the city government passes a
regulation:

The factory is permitted to dump any amount of the pollutant as long as the
fish is not killed.

This regulation can be interpreted in two ways corresponding to two types of
agency. The first could be

any dumping amount that admits of the survival of the fish is permitted. (SA)

In this interpretation, the permitted dumping amount of the factory is any
amount no more than $100$g/day. As long as the factory follows this
regulation, there is a chance for the fish to survive if the other factory
dumps so little that the total dumped amount does not exceed $100$g/day. The
second interpretation of the regulation could be

any dumping amount that ensures the survival of the fish is permitted. (SE)

In this interpretation, the factory should not dump any amount over $40$g/day
and the fish cannot be killed as long as the factory follows the regulation,
no matter how much of the pollutant is dumped by the other factory.

The above two interpretations give the factory two different permissions. It
is worth noting that, either of the permissions enables the factory to take
any of the actions satisfying some criteria. In this paper, we call such
permissions “strong”. Specifically, we refer to (SA) and (SE) as strong
permission to admit and strong permission to ensure, respectively.

Not all permissions are in the same form as strong permissions. Suppose that,
instead of the city’s regulation, the factory is under some contractual
obligation. To satisfy this obligation, the factory has to dump at least
$30$g/day of the pollutant. In this case, not every amount that ensures/admits
of the survival of the fish (e.g. $20$g/day) is contractually permitted to be
dumped. Nevertheless,

there is a permitted dumping amount that ensures the survival of the fish.
(WE)

For example, 35g/day is a contractually permitted dumping amount that ensures
the survival of the fish. Similarly, if the contractual obligation forces the
factory to dump at least $50$g/day of the pollutant, then no contractually
permitted dumping amount ensures the survival of the fish. However,

there is a permitted dumping amount that admits of the survival of the fish.
(WA)

In contrast to strong permissions, the above two permissions express the
capability of the factory to achieve some statements with a permitted action.
We call such permissions “weak”. Specifically, we refer to (WE) and (WA) as
weak permission to ensure and weak permission to admit, respectively.

As shown in Section 2, the terms “strong permission” and “weak permission”
have already existed in the literature for decades Raz (1975); Royakkers
(1997); Governatori et al. (2013). In Section 5, we show the consistency
between how these terms are used in our paper and in the literature. However,
as far as we see, we are the first to make a clear distinction between
“permission to ensure” and “permission to admit”, which are agentive
permissions specific to multiagent settings. We are also the first to cross-
discuss both strong and weak agentive permissions in multiagent settings.

In this paper, we discuss four forms of permissions in multiagent settings
that generalise those expressed in statements (SA), (SE), (WE), and (WA). Our
contribution is three-fold. First, we propose a formal semantics for the four
corresponding modalities in multiagent transition systems (Section 3). We also
consider the model-checking problem (Section 3.1) and the reduction to STIT
logic and ATL (Section 3.2). Second, we prove these modalities are
semantically undefinable through each other (Section 4). This contrasts to the
fact that, when separated from permissions, ensuring and admitting are dual to
each other. Third, we give a sound and complete logical system for the four
modalities (Section 5 and Section 6). This reveals the interplay between the
four forms of permissions and offers an efficient way for permission
reasoning.

##  2 Literature Review and Notion Discussion

Deontic logic McNamara and van de Putte (2022) is an appealing approach to
solving AI ethics problems by enabling autonomous agents to comprehend and
reason about their obligation, permission, and prohibition. It aims at
“translating” the deontic statements in natural languages into logical
propositions and building up a system for plausible deduction. Von Wright von
Wright (1951) launched the active development of symbolic deontic logic from
the analogies between normative and alethic modalities. Several follow-up
works Anderson (1956); Prior (1963) built up the Standard Deontic Logic (SDL),
taking obligation as the basic modality and defining permission as the dual of
obligation and prohibition as the obligation of the negation. Anderson
Anderson (1967) and Kanger Kanger (1971) reduced this system by defining a
propositional constant $d$ for “all (relative) normative demands are met”. By
this means, obligation (modality ${\sf O}$) can be defined as ${\sf
O}\varphi:=\Box(d\to\varphi),$ which is read as “it is necessary that
$\varphi$ is true when all normative demands are met”. As the dual of
obligation, permission (modality ${\sf P}$) is defined as

${\sf P}\varphi:=\Diamond(d\wedge\varphi),$ (1)

which is read as “it is possible that all normative demands are met and
$\varphi$ is true”. In this way, the inference rule

$\dfrac{\varphi\to\psi}{{\sf P}\varphi\to{\sf P}\psi}$ (2)

is valid. The notion of permission that satisfies statement (2) is called weak
permission. There are two well-known related paradoxes about weak permission:

(i) Ross’s paradox Ross (1944). The formula

${\sf P}\varphi\to{\sf P}(\varphi\vee\psi)$ (3)

is valid by statement (2). However, in common sense, for a kid “it is
permitted to eat an apple” is true but “it is permitted to eat an apple or
drink alcohol” should be false, which contradicts statement (3).

(ii) The free choice permission paradox von Wright (1968); Kamp (1973).
According to linguistic intuition, if “it is permitted to eat an apple or a
banana”, then both “eating an apple” and “eating a banana” should be
permitted. This shows that disjunctive permission is treated as free choice
permission, which means the formula

${\sf P}(\varphi\vee\psi)\to{\sf P}\varphi\wedge{\sf P}\psi$ (4)

should be valid. However, statement (4) is not derivable in SDL. Free choice
permission is a form of strong permission Asher and Bonevac (2005), satisfying
the inference rule

$\dfrac{\varphi\to\psi}{{\sf P}^{s}\psi\to{\sf P}^{s}\varphi}.$ (5)

Following Anderson and Kanger’s way, van Benthem van Benthem (1979) captured
the notion of strong permission as

${\sf P}^{s}\varphi=\Box(\varphi\to d),$ (6)

which is read as “it is necessary that if $\varphi$ is true then all normative
demands are met”. He then gave a complete axiom system for obligation (${\sf
O}$) and strong permission (${\sf P}^{s}$).

Most researchers agree that both weak and strong permission makes sense. As
discussed by Lewis Lewis (1979), no universal comprehension of permission
seems to exist. In general, weak permission is treated as the dual of
obligation. Strong permission, as well as free choice permission, is more
intractable and arouses more interesting discussions due to its anti-monotonic
inference property in statement (5). For instance, Anglberger et al.
Anglberger et al. (2015) adopted the notion of strong permission and defined a
notion of obligation as the weakest form of (strong) permission. Wang and Wang
Wang and Wang (2023) axiomatised a logic of strong permission that satisfies
some commonly desirable logical properties. Strong permission is also studied
in defeasible logic Asher and Bonevac (2005); Governatori et al. (2013), which
is believed to be able to capture the logical intuition about permission.

The above discussion of permission applies possible-world semantics without
specifically considering agents and their agency. However, it is noticed that
two kinds of normative statements exist: the agentless norms that talk about
states (e.g. it is permitted to eat an apple) and the agentive norms that talk
about actions (e.g. John is permitted to eat an apple). The possible-world
semantics cannot distinguish them. To fill the gap, Chisholm Chisholm (1964)
proposed a transfer from any agentive norm to an agentless norm. For instance,
the statement “agent $a$ is permitted to do $\varphi$” is transformed into “it
is permitted that agent $a$ does $\varphi$”. Some recent work Kulicki and
Trypuz (2017); Kulicki et al. (2023) aimed at integrating the agentless and
agentive norms in a unified logical frame.

Things become more complicated when agents and their agency are incorporated.
In the literature, STIT logic Chellas (1969); Belnap and Perloff (1988, 1992)
is used to express the agency. Horty and Belnap Horty and Belnap (1995) and
Horty (Horty, 2001, chapter 4) introduced a deontic STIT logic for ought-to-be
and ought-to-do semantics, respectively. The former corresponds to the
agentless obligations while the latter corresponds to the agentive obligations
in STIT models. Horty (Horty, 2001, chapter 3) further showed that the
transfer proposed by Chisholm does not always work properly. Following Horty,
van de Putte van de Putte (2017) briefly discussed the dual of the ought-to-do
obligation, which is the weak permission in deontic STIT logic, and then
defined a form of free choice permission following statement (4). Although the
agency is considered in deontic STIT logic, the distinction between to ensure
and to admit is never discussed there.

In the field of AI, there is a rising interest in applying deontic logic into
agents’ planning: how to achieve a goal while complying with the deontic
constraints Pandžić et al. (2022); Areces et al. (2023). There is also some
discussion of agents’ comprehending and reasoning norms Arkoudas et al.
(2005); Broersen and Ramírez Abarca (2018). However, to the best of our
knowledge, the agentive weak and strong permissions have never been cross-
discussed before.

In this paper, we consider both permission to ensure and permission to admit
in both weak and strong forms that follow statements (1) and (6). In a word,
we consider four forms of permissions as illustrated in statements (SA), (SE),
(WE), and (WA). It is worth mentioning that, our formalisation has a
connection with Horty’s ought-to-do deontic STIT logic Horty (2001). On the
one hand, the notion “ensure” captures the same idea as “see to it that” in
STIT logic. On the other hand, our formalisation can be seen as a reasonable
reduction of Horty’s formalisation. Specifically, Horty’s approach is to,
first, define a preference over the outcomes (i.e. “histories” in STIT models)
of actions in the model, then, apply the dominance act utiliarianism to decide
which actions are permitted (i.e. “optimal” in his work) in semantics, and,
finally, define the ought-to-do obligation based on the permitted actions in
semantics. In particular, an action in the STIT frame is the set of outcomes
that may follow from the action. An action “sees to it that” $\varphi$ if and
only if $\varphi$ is true in all the potential outcomes. Then, “do $\varphi$”
is interpreted as “seeing to it that $\varphi$”. In this paper, we combine the
first two steps of Horty’s approach, directly defining the deontic constraints
on actions in the model and then defining four forms of permissions in
semantics. Note that, the definition of deontic notions is independent of the
process that combines the first two steps in Horty’s approach. In other words,
our work in this paper can easily be transformed from action-based models into
outcome-based models by recovering the step of deciding permitted actions
based on preference over outcomes using dominance act utilitarianism.
Moreover, we give a reduction of our semantics into STIT logic in Section 3.2.

##  3 Syntax and Semantics

In this section, we introduce the syntax and semantics of our logical system.
Throughout the paper, unless stated otherwise, we assume a fixed set
$\mathcal{A}$ of agents and a fixed nonempty set of propositional variables.

######  Definition 1.

A transition system is a tuple $(S,\Delta,D,M,\pi)$:

  1. 1.

$S$ is a (possibly empty) set of states;

  2. 2.

$\Delta=\\{\Delta_{a}^{s}\\}_{s\in S,a\in\mathcal{A}}$ is the action space,
where $\Delta_{a}^{s}$ is a nonempty set of actions available to agent $a$ in
state $s$;

  3. 3.

$D=\\{D_{a}^{s}\\}_{s\in S,a\in\mathcal{A}}$ is the deontic constraints, where
$D_{a}^{s}$ is a set of permitted actions and $\varnothing\subsetneq
D_{a}^{s}\subseteq\Delta_{a}^{s}$;

  4. 4.

$M=\\{M_{s}\\}_{s\in S}$ is the mechanism, where a relation
$M_{s}\subseteq\prod_{a\in\mathcal{A}}\Delta_{a}^{s}\times S$ satisfies the
continuity condition: for each action profile
$\delta\in\prod_{a\in\mathcal{A}}\Delta_{a}^{s}$ there is a state $t\in S$
such that $(\delta,t)\in M_{s}$;

  5. 5.

$\pi(p)\subseteq S$ for each propositional variable $p$.

The continuity condition in item 4 above requires the existence of a “next”
state $t$. We say that a transition system is deterministic if such state $t$
is always unique.

The language $\Phi$ of our logical system is defined by the following grammar:

$\varphi:=p\;|\;\neg\varphi\;|\;\varphi\vee\varphi\;|\;\text{WA}_{a}\varphi\;|\;\text{WE}_{a}\varphi\;|\;\text{SE}_{a}\varphi\;|\;\text{SA}_{a}\varphi,$

where $p$ is a propositional variable and $a\in\mathcal{A}$ is an agent.
Intuitively, we interpret $\text{WA}_{a}\varphi$ as “there is a permitted
action of agent $a$ that admits of $\varphi$”, $\text{WE}_{a}\varphi$ as
“there is a permitted action of agent $a$ that ensures $\varphi$”,
$\text{SE}_{a}\varphi$ as “each action of agent $a$ that ensures $\varphi$ is
permitted”, and $\text{SA}_{a}\varphi$ as “each action of agent $a$ that
admits of $\varphi$ is permitted”. We assume that conjunction $\wedge$,
implication $\to$, and Boolean constants true $\top$ and false $\bot$ are
defined in the usual way. Also, by $\bigwedge_{i\leq n}\varphi_{i}$ and
$\bigvee_{i\leq n}\varphi_{i}$ we denote, respectively, the conjunction and
the disjunction of the formulae $\varphi_{1},\dots\varphi_{n}$. As usual, we
assume that the conjunction and the disjunction of an empty list are $\top$
and $\bot$, respectively.

######  Definition 2.

For each transition system $(S,\Delta,D,M,\pi)$, each state $s\in S$, and each
formula $\varphi\in\Phi$, the satisfaction relation $s\Vdash\varphi$ is
defined recursively as follows:

  1. 1.

$s\Vdash p$, if $s\in\pi(p)$;

  2. 2.

$s\Vdash\neg\varphi$, if $s\nVdash\varphi$;

  3. 3.

$s\Vdash\varphi\vee\psi$, if $s\Vdash\varphi$ or $s\Vdash\psi$;

  4. 4.

$s\Vdash\text{WA}_{a}\varphi$, if $(s,i)\not\rightsquigarrow_{a}\neg\varphi$
for some $i\in D_{a}^{s}$;

  5. 5.

$s\Vdash\text{WE}_{a}\varphi$, if $(s,i)\rightsquigarrow_{a}\varphi$ for some
$i\in D_{a}^{s}$;

  6. 6.

$s\Vdash\text{SE}_{a}\varphi$, if $i\in D_{a}^{s}$ for each $i$ such that
$(s,i)\rightsquigarrow_{a}\varphi$;

  7. 7.

$s\Vdash\text{SA}_{a}\varphi$, if $i\in D_{a}^{s}$ for each $i$ such that
$(s,i)\not\rightsquigarrow_{a}\neg\varphi$,

where the notation $(s,i)\rightsquigarrow_{a}\varphi$ means that, for each
tuple $(\delta,t)\in M_{s}$, if $\delta_{a}=i$, then $t\Vdash\varphi$.

Items 4 - 7 above capture the generalised notions of permissions in statements
(WA), (WE), (SE), and (SA) in Section 1. Informally,
$(s,i)\rightsquigarrow_{a}\varphi$ means that that action $i$ of agent $a$ in
state $s$ ensures that $\varphi$ is true in the next state. Accordingly,
$(s,i)\not\rightsquigarrow_{a}\neg\varphi$ means that action $i$ of agent $a$
in state $s$ admits of the situation that $\varphi$ is true in the next state.
Observe that, if a transition system is deterministic and has only one agent
$a$, then $(s,i)\not\rightsquigarrow_{a}\neg\varphi$ if and only if
$(s,i)\rightsquigarrow_{a}\varphi$. Then, the next lemma follows from items 4
- 7 of Definition 2.

######  Lemma 1.

If set $\mathcal{A}$ contains only agent $a$, then for any formula
$\varphi\in\Phi$ and state $s$ of a deterministic transition system,

  1. 1.

$s\Vdash\text{WA}_{a}\varphi$ if and only if $s\Vdash\text{WE}_{a}\varphi$;

  2. 2.

$s\Vdash\text{SA}_{a}\varphi$ if and only if $s\Vdash\text{SE}_{a}\varphi$.

Note that, in other cases (i.e. multiagent or non-deterministic systems),
these modalities are not only semantically inequivalent but also undefinable
through each other. We show this in Section 4.

###  3.1 Model Checking

Following Definition 2, we consider the global model-checking problem Müller-
Olm et al. (1999) of language $\Phi$. For a finite transition system and a
formula $\varphi\in\Phi$, the global model checking determines the truth set
$\llbracket\varphi\rrbracket$ that consists of all states satisfying $\varphi$
in the transition system. Formally, we define the truth set of a formula as
follows.

######  Definition 3.

For any given transition system and any formula $\varphi\in\Phi$, the truth
set $\llbracket\varphi\rrbracket$ is the set $\\{s\;|\;s\Vdash\varphi\\}$.

The global model checking of formula $\varphi$ applies a trivial recursive
process on its structural complexity. The next theorem shows its time
complexity. See Appendix A for the model checking algorithm and detailed
analysis.

######  Theorem 1 (time complexity).

For a finite transition system $(S,\Delta,D,M,\pi)$ and a formula
$\varphi\in\Phi$, the time complexity of global model checking is
$O\big{(}|\varphi|\cdot(|S|\\!+\\!|M|\\!+\\!|\Delta|)\big{)}$, where
$|\varphi|$ is the size of the formula, $|S|$ is the number of states,
$|M|=\sum_{s\in S}|M_{s}|$ is the size of the mechanism, and
$|\Delta|=\sum_{a\in\mathcal{A}}\sum_{s\in S}|\Delta_{a}^{s}|$ is the size of
the action space.

###  3.2 Reduction to Other Logics

Recall statements (1) and (6) in Section 2, which show the way how Anderson
and Kanger reduces SDL. Using a similar technique, we can translate our
modalities into modalities in STIT logic and ATL Alur et al. (2002) after
properly interpreting the transition system in Definition 1.

#### Reduction to STIT

Instead of being about the states, the statements in STIT logic are about
moment-history ($m/h$) pairs. Due to this fact, there is no exact reduction of
our logic to STIT logic. However, we can interpret our modalities in STIT
models in the appearance of the necessity and possibility modalities $\Box$
and $\Diamond$111$m/h\Vdash\Box\varphi$ iff $m/h^{\prime}\\!\Vdash\varphi$ for
each history $h^{\prime}$ such that $m\in h^{\prime}$.. In order to do this,
we first incorporate the deontic constraints into the models as atomic
propositions. To be specific, $m/h\Vdash d_{a}$ represents that the action of
agent $a$ at moment $m$ that includes history $h$ is permitted. We use the
modality XSTIT Broersen (2008, 2011). Informally,
$m/h\Vdash\text{XSTIT}_{a}\varphi$ could be interpreted as “the action of
agent $a$ at moment $m$ that includes history $h$ sees to it that $\varphi$ is
true at the next moment”. Then, our four modalities can be translated as:

$\displaystyle\text{WA}_{a}\varphi:=\Diamond(d_{a}\wedge\neg\text{XSTIT}_{a}\neg\varphi);$
$\displaystyle\text{WE}_{a}\varphi:=\Diamond(d_{a}\wedge\text{XSTIT}_{a}\varphi);$
$\displaystyle\text{SE}_{a}\varphi:=\Box(\text{XSTIT}_{a}\varphi\to d_{a});$
$\displaystyle\text{SA}_{a}\varphi:=\Box(\neg\text{XSTIT}_{a}\neg\varphi\to
d_{a}).$

#### Reduction to ATL

Unlike in STIT logic, in ATL, the statements are about states but there is no
way to express the properties of actions. For this reason, we encode deontic
constraints into the states. To do this, we expand each state in our original
transition system into a set of states in the ATL model. Specifically, each
state $s$ in our original transition system corresponds to a set $\\{\langle
s,\mathcal{D}\rangle\,|\,\mathcal{D}\subseteq\mathcal{A}\\}$ of states in the
ATL model. Informally, the tuple $\langle s,\mathcal{D}\rangle$ encodes the
information that “state $s$ is reached after the agents in set $\mathcal{D}$
taking permitted actions and the others taking non-permitted actions”. Then,
$\langle s,\mathcal{D}\rangle\Vdash d_{a}$ if and only if $a\in\mathcal{D}$.
Also, $\langle s,\mathcal{D}\rangle\Vdash p$ if and only if $s\Vdash p$ in our
original transition system. Correspondingly, the transition $(\langle
s,*\rangle,\langle t,\mathcal{D}\rangle)$ exists in the ATL model if there is
a tuple $(\delta,t)\in M_{s}$ in our original transition system such that
$\mathcal{D}=\\{a\in\mathcal{A}\,|\,\delta_{a}\in D_{a}^{s}\\}$ and $*$ is a
wildcard. Note that, ATL requires the transitions to be deterministic. Thus,
if needed, we incorporate a dummy agent $Nature$ into the agent set
$\mathcal{A}$ to achieve determinacy. Then, we can translate our modalities
into standard ATL syntax as:

$\displaystyle\text{WA}_{a}\varphi:=\langle\\!\langle\mathcal{A}\rangle\\!\rangle{\sf
X}(d_{a}\wedge\varphi);$ $\displaystyle\text{WE}_{a}\varphi:=\langle\\!\langle
a\rangle\\!\rangle{\sf X}(d_{a}\wedge\varphi);$
$\displaystyle\text{SE}_{a}\varphi:=\neg\langle\\!\langle
a\rangle\\!\rangle{\sf X}\neg(\varphi\to d_{a});$
$\displaystyle\text{SA}_{a}\varphi:=\neg\langle\\!\langle\mathcal{A}\rangle\\!\rangle{\sf
X}\neg(\varphi\to d_{a}),$

where $\langle\\!\langle\mathcal{C}\rangle\\!\rangle{\sf X}\varphi$ is
informally interpreted as “the agents in set $\mathcal{C}$ can cooperate to
enforce $\varphi$ in the next state” and $\langle\\!\langle
a\rangle\\!\rangle$ is the abbreviation for
$\langle\\!\langle\\{a\\}\rangle\\!\rangle$.

##  4 Mutual Undefinability

As we define four modalities in the language, we would like to figure out if
all of them are necessary to express the corresponding notions of permission.
Specifically, if some of these modalities are semantically definable through
the others, then the definable ones are not necessary for the language. As an
example, a well-known result in Boolean logic is De Morgan’s laws, which say
conjunction and disjunction are inter-definable in the presence of negation.
Therefore, to consider a “minimal” system for propositional logic, it is not
necessary to include both conjunction and disjunction.

In this section, we consider the definability of modalities in the same way as
De Morgan’s laws (i.e. semantical equivalence). For example, modality WA is
definable through modalities WE, SE, and SA if every formula in language
$\Phi$ is semantically equivalent to a formula using only modalities WE, SE,
and SA. Formally, in the transition systems, we define semantical equivalence
as follows.

######  Definition 4.

Formulae $\varphi$ and $\psi$ are semantically equivalent if
$\llbracket\varphi\rrbracket=\llbracket\psi\rrbracket$ for each transition
system.

We prove that none of the modalities WA, WE, SE, and SA is definable through
the other three. To do this, it suffices to show that, for each modality
$\odot$ of the four modalities, there exists a formula $\odot\varphi\in\Phi$
and a transition system where
$\llbracket\odot\varphi\rrbracket\neq\llbracket\psi\rrbracket$ for each
formula $\psi$ not using modality $\odot$. In particular, we use the truth set
algebra technique Knight et al. (2022). This technique uses one model (i.e.
transition system) and shows that, in this model, the truth sets of all
formulae $\psi$ not using modality $\odot$ form a proper subset of the family
of all truth sets in language $\Phi$, while the truth set of the formula
$\odot\varphi$ does not belong to this subset. We formally state the
undefinability results in the next theorem. A detailed explanation of the
technique and proof can be found in Appendix B.

######  Theorem 2 (undefinability of WA).

The formula $\text{WA}_{a}p$ is not semantically equivalent to any formula in
language $\Phi$ that does not use modality WA.

The formal statements of the undefinability results for modalities WE, SE, and
SA are the same as Theorem 2 except for using the corresponding modalities
instead of WA, see Theorem 5, Theorem 6, and Theorem 7 in Appendix B.

Note that, all four undefinability results, as presented in Appendix B,
require that our language contains at least two agents. In single-agent
settings, if a transition system is non-deterministic, these undefinability
results still hold. This can be observed by modifying the two-agent transition
systems in the proofs into single-agent non-deterministic transition systems
by treating one of the agents as the non-deterministic factor. If a single-
agent transition system is deterministic, then, as observed in Lemma 1,
modalities WA and WE are semantically equivalent, so as modalities SE and SA.
However, modalities WA (WE) and SA (SE) are not definable through each other.
See Appendix B.5 for proof.

##  5 Axioms

In addition to the tautologies in language $\Phi$, our logical system contains
the following schemes of axioms for all agents $a,b\in\mathcal{A}$ and all
formulae $\varphi,\psi\in\Phi$:

  1. A1.

$\neg\text{WA}_{a}\bot$;

  2. A2.

$\text{WE}_{a}\top$;

  3. A3.

$\text{SA}_{a}\bot$;

  4. A4.

$\text{SE}_{a}\top\to\text{SA}_{a}\top$;

  5. A5.

$\text{WA}_{a}(\varphi\vee\psi)\to\text{WA}_{a}\varphi\vee\text{WA}_{a}\psi$;

  6. A6.

$\text{SA}_{a}\varphi\wedge\text{SA}_{a}\psi\to\text{SA}_{a}(\varphi\vee\psi)$;

  7. A7.

$\text{WE}_{a}\varphi\wedge\neg\text{WE}_{a}\psi\to\text{WA}_{a}(\varphi\wedge\neg\psi)$;

  8. A8.

$\neg\text{SE}_{a}\varphi\wedge\text{SE}_{a}\psi\to\neg\text{SA}_{a}(\varphi\wedge\neg\psi)$;

  9. A9.

$\neg\text{WA}_{a}\varphi\wedge\text{SA}_{a}\psi\to\neg\text{WA}_{b}(\varphi\wedge\psi)\wedge\text{SA}_{b}(\varphi\wedge\psi)$.

Axiom A1 says agent $a$ does not have a permitted action that has no next
state. This is true because of the continuity property of the mechanism (item
4 of Definition 1). Axiom A2 says agent $a$ always has a permitted action that
ensures a next state. This is true because of the continuity property and the
nonempty set of permitted actions (item 3 of Definition 1). Axiom A3 says
every action that may have no next state is permitted. This is true because no
such actions exist again due to the continuity property. Axiom A4 is true
because both $\text{SE}_{a}\top$ and $\text{SA}_{a}\top$ mean that every
action of agent $a$ is permitted.

Axiom A5 says, if agent $a$ has a permitted action that admits of
$\varphi\vee\psi$, then agent $a$ either has a permitted action that admits of
$\varphi$ or has a permitted action that admits of $\psi$. This is true
because the permitted action that admits of $\varphi\vee\psi$ indeed either
admits of $\varphi$ or admits of $\psi$ (item 3 of Definition 2). Axiom A6
says, if every action of agent $a$ that admits of $\varphi$ is permitted and
every action of agent $a$ that admits of $\psi$ is permitted, then every
action of agent $a$ that admits of $\varphi\vee\psi$ is permitted. This is
true because any action that admits of $\varphi\vee\psi$ either admits of
$\varphi$ or admits of $\psi$ (item 3 of Definition 2).

Axiom A7 says, if agent $a$ has a permitted action that ensures $\varphi$ and
has no permitted action that ensures $\psi$, then agent $a$ has a permitted
action that admits of $\varphi\wedge\neg\psi$. This is true because the
permitted action $i$ that ensures $\varphi$ does not ensure $\psi$. Hence,
action $i$ admits of $\neg\psi$ while $\varphi$ is ensured to happen. Axiom A8
says, if agent $a$ has a non-permitted action that ensures $\varphi$ and every
action that ensures $\psi$ is permitted, then agent $a$ has a non-permitted
action that admits of $\varphi\wedge\neg\psi$. This is true because the non-
permitted action $j$ that ensures $\varphi$ does not ensure $\psi$. Hence,
action $j$ admits of $\neg\psi$ while $\varphi$ is ensured to happen.

Axiom A9 says, if agent $a$ has no permitted action that admits of $\varphi$
and every action that admits of $\psi$ is permitted, then agent $b$ has no
permitted action that admits of $\varphi\wedge\psi$ and every action of agent
$b$ that admits of $\varphi\wedge\psi$ is permitted. This is true because the
antecedent means agent $a$’s permitted actions ensure $\neg\varphi$ and non-
permitted actions (if existing) ensure $\neg\psi$. Thus, every action of agent
$a$ ensures $\neg\varphi\vee\neg\psi$ (item 3 of Definition 2). Hence,
$\neg(\varphi\wedge\psi)$ is unavoidable in the next state. This implies that
agent $b$ has no permitted action that admits of $\varphi\wedge\psi$, and any
action of agent $b$ that admits of $\varphi\wedge\psi$ is permitted because no
such action of agent $b$ exists.

We write $\vdash\varphi$ and say that formula $\varphi$ is a theorem of our
logical system if it can be derived from the axioms using the following four
inference rules:

  1. IR1.

$\dfrac{\varphi\,,\hskip 8.53581pt\varphi\to\psi}{\psi}$ (Modus Ponens);

  2. IR2.

$\dfrac{\varphi\to\psi}{\text{WA}_{a}\varphi\to\text{WA}_{a}\psi}$;

  3. IR3.

$\dfrac{\varphi\to\psi}{\text{SA}_{a}\psi\to\text{SA}_{a}\varphi}$;

  4. IR4.

$\dfrac{\varphi_{1}\wedge\dots\wedge\varphi_{m}\to\neg\psi_{1}\vee\dots\vee\neg\psi_{n}}{\text{WE}_{a_{1}}\varphi_{1}\wedge\dots\wedge\text{WE}_{a_{m}}\varphi_{m}\to\text{SE}_{b_{1}}\psi_{1}\vee\dots\vee\text{SE}_{b_{n}}\psi_{n}}$,
where agents $a_{1},\dots,a_{m},b_{1},\dots,b_{n}$ are distinct.

Rule IR2 is the monotonicity rule for modality WA. It is valid because, in
each state of each transition system, the permitted action of agent $a$ that
admits of $\varphi$ also admits of $\psi$, as $\varphi\to\psi$ is universally
true. By this rule, modality WA represents a form of weak permission following
statement (2). Rule IR3 is the anti-monotonicity rule for modality SA. It is
valid because, in each state of each transition system, the set of actions
that admits of $\psi$ is a superset of the set of actions that admits of
$\varphi$, as $\varphi\to\psi$ is universally true. Hence, as long as the
actions in the former set are all permitted, those in the latter set are also
permitted. This rule shows that modality SA represents a form of strong
permission following statement (5). It can be derived that modality WE
represents a form of weak permission and modality SE represents a form of
strong permission, see Appendix C.1.

Rule IR4 is a conflict-preventing rule following the notion of “ensure” in
semantics. The premise says, if every one of $\varphi_{1},\dots,\varphi_{m}$
is true, then at least one of $\psi_{1},\dots,\psi_{n}$ is false. The
conclusion says, for a set of distinct agents
$\\{a_{1},\dots,a_{m},b_{1},\dots,b_{n}\\}\subseteq\mathcal{A}$, if every
agent $a_{i}$ has a permitted action to ensure $\varphi_{i}$, then for at
least one agent $b_{j}$, every action that ensures $\psi_{j}$ is permitted.
This is valid because there would be a conflict otherwise. To be specific, if
there is a state $s$ where the conclusion of the rule is false, then, each
agent $a_{i}$ has a permitted action $k_{i}$ that ensures $\varphi_{i}$ and
each agent $b_{j}$ has a non-permitted action $\ell_{j}$ that ensures
$\psi_{j}$. Consider an action profile $\delta$ such that
$\delta_{a_{i}}=k_{i}$ for each $i\leq m$ and $\delta_{b_{j}}=\ell_{j}$ for
each $j\leq n$. By the continuity condition in item 4 of Definition 1, there
is a state $t$ such that $(\delta,t)\in M_{s}$. In such state $t$, each of the
formulae $\varphi_{1},\dots,\varphi_{m},\psi_{1},\dots,\psi_{n}$ is true.
However, this conflicts with the premise of the rule.

We write $X\vdash\varphi$ if a formula $\varphi$ can be derived from the
theorems of our logical system and an additional set of assumptions $X$ using
only the Modus Ponens rule. Note that statements $\varnothing\vdash\varphi$
and $\vdash\varphi$ are equivalent. We say that a set of formulae $X$ is
consistent if $X\nvdash\bot$.

######  Lemma 2 (deduction).

If $X,\varphi\vdash\psi$, then $X\vdash\varphi\to\psi$.

See the proof of this lemma in Appendix C.2.

######  Lemma 3 (Lindenbaum).

Any consistent set of formulae can be extended to a maximal consistent set of
formulae.

The standard proof of this lemma can be found in (Mendelson, 2009, Proposition
2.14).

######  Lemma 4.

$\vdash\text{WE}_{a}\varphi\wedge\neg\text{WA}_{a}\psi\to\text{WE}_{a}(\varphi\wedge\neg\psi)$.

######  Lemma 5.

$\vdash\neg\text{SE}_{a}\varphi\wedge\text{SA}_{a}\psi\to\neg\text{SE}_{a}(\varphi\wedge\neg\psi)$.

See the proofs of the above two lemmas in Appendix C.3. The next theorem
follows from the above discussion of the axioms and the inference rules.

######  Theorem 3 (soundness).

If $\vdash\varphi$, then $s\Vdash\varphi$ for each state $s$ of each
transition system.

##  6 Completeness

In this section, we prove the strong completeness of our logical system. As
usual, at the core of the completeness theorem is the canonical model
construction. In our case, it is a canonical transition system.

###  6.1 Canonical Transition System

In this subsection, we define the canonical transition system
$(S,\Delta,D,M,\pi)$.

######  Definition 5.

Set $S$ of states is the family of all maximal consistent subsets of our
language $\Phi$.

For each formula $\varphi\in\Phi$, we introduce two actions: a permitted
action $\varphi^{+}$ and a non-permitted action $\varphi^{-}$. Formally, by
$\varphi^{+}$ and $\varphi^{-}$ we mean the pairs $(\varphi,+)$ and
$(\varphi,-)$, respectively. By item 7 of Definition 2, the formula
$\text{SA}_{a}\top$ expresses that agent $a$ is permitted to use every action.
In other words, if $\text{SA}_{a}\top$ is true, then there are no non-
permitted actions available to agent $a$ in the current state. This explains
the intuition behind the following definition.

######  Definition 6.

For each state $s\in S$ and each agent $a\in\mathcal{A}$,

  * $\Delta^{s}_{a}=\begin{cases}\\{\varphi^{+}\;|\;\varphi\in\Phi\\},&\text{if\; $\text{SA}_{a}\top\in s$},\\\ \\{\varphi^{+},\varphi^{-}\;|\;\varphi\in\Phi\\},&\text{otherwise;}\end{cases}$

  * $D^{s}_{a}=\\{\varphi^{+}\;|\;\varphi\in\Phi\\}.$

The next definition is the key part of the canonical transition system
construction. It specifies the mechanism of the transition system. Recall that
$\neg\text{WA}_{a}\varphi$ means that agent $a$ is not permitted to use any
action that admits of $\varphi$. Hence, each permitted action of $a$ must
ensure $\neg\varphi$. We capture this rule in item 1 of the definition below.
Recall that $\text{WE}_{a}\varphi$ means that agent $a$ has at least one
permitted action that ensures $\varphi$. In the canonical transition system,
this action is defined to be $\varphi^{+}$. The rule captured in item 2 below
guarantees $\varphi$ in the next state whenever agent $a$ uses action
$\varphi^{+}$. Next, $\neg\text{SE}_{a}\varphi$ means that agent $a$ is not
permitted to use at least one action that ensures $\varphi$. We denote such
action by $\varphi^{-}$. The rule captured by item 3 stipulates that action
$\varphi^{-}$ ensures $\varphi$. Finally, $\text{SA}_{a}\varphi$ means that
agent $a$ is permitted to use all actions that admit of $\varphi$. In other
words, $\text{SA}_{a}\varphi$ means that all non-permitted actions ensure
$\neg\varphi$. This is captured by item 4 below.

######  Definition 7.

$(\delta,t)\in M_{s}$ when for each agent $a\in\mathcal{A}$ and each formula
$\varphi\in\Phi$,

  1. 1.

if $\delta_{a}\in D_{a}^{s}$ and $\text{WA}_{a}\varphi\notin s$, then
$\neg\varphi\in t$;

  2. 2.

if $\delta_{a}=\varphi^{+}$ and $\text{WE}_{a}\varphi\in s$, then $\varphi\in
t$;

  3. 3.

if $\delta_{a}=\varphi^{-}$ and $\text{SE}_{a}\varphi\notin s$, then
$\varphi\in t$;

  4. 4.

if $\delta_{a}\in\Delta_{a}^{s}\setminus D_{a}^{s}$ and
$\text{SA}_{a}\varphi\in s$, then $\neg\varphi\in t$.

Note that, each state $s$ is a maximal consistent set by Defintion 5. Hence,
for item 1 above, the statement $\text{WA}_{a}\varphi\notin s$ is equivalent
to $\neg\text{WA}_{a}\varphi\in s$. The same goes for item 3.

######  Definition 8.

$\pi(p)=\\{s\in S\;|\;p\in s\\}$ for each $p$.

This concludes the definition of the canonical transition system
$(S,\Delta,D,M,\pi)$. Next, we show that it satisfies the continuity condition
in item 4 of Definition 1.

######  Lemma 6 (continuity).

For each state $s\in S$ and each action profile
$\delta\in\prod_{a\in\mathcal{A}}\Delta_{a}^{s}$, there is a state $t$ such
that $(\delta,t)\in M_{s}$.

###### Proof.

Consider a partition $\\{A,B\\}$ of the set $\mathcal{A}$ of agents:

$\displaystyle A=\\{a\in\mathcal{A}\,|\,\delta_{a}\in D_{a}^{s}\\};$ (7)
$\displaystyle B=\\{b\in\mathcal{A}\,|\,\delta_{b}\in\Delta_{b}^{s}\setminus
D_{b}^{s}\\}.$ (8)

Then, $\text{SA}_{b}\top\notin s$ for each agent $b\in B$ by Definitions 6.
Hence, $\neg\text{SA}_{b}\top\in s$ for each agent $b\in B$ because $s$ is a
maximal consistent set. Then, by the contrapositive of axiom A4,

$\neg\text{SE}_{b}\top\in s.$ (9)

Consider the set of formulae

$\displaystyle X=$ $\displaystyle\\{\neg\psi\;|\;\exists\,a\in
A\,(\neg\text{WA}_{a}\psi\in s)\\}$ (10)
$\displaystyle\cup\\{\sigma\;|\;\exists\,a\in
A\,(\delta_{a}=\sigma^{+},\text{WE}_{a}\sigma\in s)\\}$
$\displaystyle\cup\\{\neg\chi\;|\;\exists\,b\in B\,(\text{SA}_{b}\chi\in
s)\\}$ $\displaystyle\cup\\{\tau\;|\;\exists\,b\in
B\,(\delta_{b}=\tau^{-},\neg\text{SE}_{b}\tau\in s)\\}.$

######  Claim 1.

Set $X$ is consistent.

  * Proof of Claim. Suppose the opposite. Then, by axiom A2, statements (9) and (10), there are formulae

$\displaystyle\hskip 22.76219pt\neg$
$\displaystyle\text{WA}_{a_{1}}\psi_{11},\dots,\neg\text{WA}_{a_{1}}\psi_{1k_{1}},\text{WE}_{a_{1}}\widehat{\sigma}_{1}\in
s,$ (11) $\displaystyle\cdots$ $\displaystyle\neg$
$\displaystyle\text{WA}_{a_{m}}\psi_{m1},\dots,\neg\text{WA}_{a_{m}}\psi_{mk_{m}},\text{WE}_{a_{m}}\widehat{\sigma}_{m}\in
s,$

and

$\displaystyle\text{SA}_{b_{1}}\chi_{11},\dots,\text{SA}_{b_{1}}\chi_{1\ell_{1}},\neg\text{SE}_{b_{1}}\widehat{\tau}_{1}\in
s,$ (12) $\displaystyle\cdots$
$\displaystyle\text{SA}_{b_{n}}\chi_{n1},\dots,\text{SA}_{b_{n}}\chi_{n\ell_{n}},\neg\text{SE}_{b_{n}}\widehat{\tau}_{n}\in
s,$

where

$a_{1},\dots,a_{m},b_{1},\dots,b_{n}\text{ are distinct agents},$ (13)
$\widehat{\sigma}_{i}=\begin{cases}\sigma_{i},&\text{if
}\delta_{a_{i}}=\sigma_{i}^{+}\text{ and }\text{WE}_{a_{i}}\sigma_{i}\in s,\\\
\top,&\text{otherwise,}\end{cases}$

for each $i\leq m$, and

$\widehat{\tau}_{i}=\begin{cases}\tau_{i},&\text{if
}\delta_{b_{i}}=\tau_{i}^{-}\text{ and }\neg\text{SE}_{b_{i}}\tau_{i}\in s,\\\
\top,&\text{otherwise,}\end{cases}$

for each $i\leq n$, such that

$\bigwedge_{i\leq m}\Big{(}\widehat{\sigma}_{i}\wedge\bigwedge_{j\leq
k_{i}}\\!\\!\\!\neg\psi_{ij}\Big{)}\wedge\bigwedge_{i\leq
n}\Big{(}\widehat{\tau}_{i}\wedge\bigwedge_{j\leq\ell_{i}}\\!\\!\\!\neg\chi_{ij}\Big{)}\vdash\bot.$
(14)

By multiple application of the countrapositive of axiom A5 and propositional
reasoning, statement (11) implies that

$s\vdash\neg\text{WA}_{a_{i}}\Big{(}\bigvee_{j\leq
k_{i}}\psi_{ij}\Big{)}\text{ for each $i\leq m$.}$ (15)

Note that, in the specific case where $k_{i}=0$, statement (15) follows
directly from axiom A1. By Lemma 4, statement (15) and the part
$\text{WE}_{a_{i}}\widehat{\sigma}_{i}\in s$ of statement (11) imply

$s\vdash\text{WE}_{a_{i}}\Big{(}\widehat{\sigma}_{i}\wedge\neg\bigvee_{j\leq
k_{i}}\psi_{ij}\Big{)}\text{ for each $i\leq m$.}$ (16)

Meanwhile, by multiple application of Lemma 2 and propositional reasoning,
statement (14) can be reformulated to

$\vdash\bigwedge_{i\leq m}\Big{(}\widehat{\sigma}_{i}\wedge\neg\bigvee_{j\leq
k_{i}}\psi_{ij}\Big{)}\to\bigvee_{i\leq
n}\neg\Big{(}\widehat{\tau}_{i}\wedge\bigwedge_{j\leq\ell_{i}}\neg\chi_{ij}\Big{)}.$
(17)

By statement (13) and rule IR4, statement (17) implies

$\vdash\bigwedge_{i\leq
m}\text{WE}_{a_{i}}\Big{(}\widehat{\sigma}_{i}\wedge\neg\bigvee_{j\leq
k_{i}}\psi_{ij}\Big{)}\to\bigvee_{i\leq
n}\text{SE}_{b_{i}}\Big{(}\widehat{\tau}_{i}\wedge\bigwedge_{j\leq\ell_{i}}\neg\chi_{ij}\Big{)}.$

Then, by statement (16) and the Modus Ponens rule,

$s\vdash\bigvee_{i\leq
n}\text{SE}_{b_{i}}\Big{(}\widehat{\tau}_{i}\wedge\neg\bigvee_{j\leq\ell_{i}}\chi_{ij}\Big{)}.$
(18)

At the same time, by multiple application of axiom A6 and propositional
reasoning, statement (12) implies

$s\vdash\text{SA}_{b_{i}}\Big{(}\bigvee_{j\leq\ell_{i}}\chi_{ij}\Big{)}\text{
for each $i\leq n$}.$ (19)

Note that, in the specific case where $\ell_{i}=0$, statement (19) follows
directly from axiom A3. By Lemma 5, statement (19) and the part
$\neg\text{SE}_{b_{i}}\widehat{\tau}_{i}\in s$ of statement (12) imply

$s\vdash\neg\text{SE}_{b_{i}}\Big{(}\widehat{\tau}_{i}\wedge\neg\bigvee_{j\leq\ell_{i}}\chi_{ij}\Big{)}\text{
for each $i\leq n$,}$

which contradicts statement (18). $\boxtimes$

Let $t$ be any maximal consistent extension of set $X$. By Lemma 3, such $t$
must exist. Hence, $t\in S$ by Definition 5.

######  Claim 2.

$(\delta,t)\in M_{s}$.

  * Proof of Claim. It suffices to verify that conditions 1 – 4 of Definition 7 are satisfied for the tuple $(\delta,t)$ for each agent $x\in\mathcal{A}$. Recall that sets $A$ and $B$ form a partition of the agent set $\mathcal{A}$. Hence, it suffices to consider the following two cases:

Case 1: $x\in A$. Condition 1 of Definition 7 follows from line 1 of statement
(10) because $X\subseteq t$. Condition 2 follows from line 2 of statement
(10). Conditions 3 and 4 trivially follow from $\delta_{x}\in D_{x}^{s}$ by
statement (7).

Case 2: $x\in B$. Conditions 1 and 2 of Definition 7 trivially follow from
$\delta_{x}\notin D_{x}^{s}$ by statement (8). Condition 3 follows from line 4
of statement (10) because $X\subseteq t$. Condition 4 follows from line 3 of
statement (10). $\boxtimes$

The statement of this lemma follows from Claim 2. ∎

###  6.2 Strong Completeness Theorem

As usual, at the core of the proof of completeness is a truth lemma proven by
induction on the structural complexity of a formula. In our case, it is the
Lemma 7. The completeness result, as shown in Theorem 4, is proved with Lemma
7 in the standard way. We put the formal proofs in Appendix D.

######  Lemma 7.

$s\Vdash\varphi$ if and only if $\varphi\in s$ for each state $s$ of the
canonical transition system and each formula $\varphi\in\Phi$.

######  Theorem 4 (strong completeness).

For each set of formulae $X\subseteq\Phi$ and each formula $\varphi\in\Phi$
such that $X\nvdash\varphi$, there is a state $s$ of a transition system such
that $s\Vdash\chi$ for each $\chi\in X$ and $s\nVdash\varphi$.

##  7 Conclusion and Future Research

We are the first to classify the agentive permissions in multiagent settings
into permissions to ensure and permissions to admit and cross-discuss them in
both weak and strong forms. To do this, we propose and formalise four forms of
agentive permissions in multiagent transition systems, analyse the time
complexity of the model checking algorithm, prove their semantical
undefinability through each other, and give a sound and complete logical
system that reveals their interplay.

Future research could be in two directions. One is to extend the deontic
constraints from one-step actions to multi-step actions. Indeed, multi-step
deontic constraints are commonly seen in application scenarios. For example,
if a child is permitted to eat only one ice cream per day, then whether to eat
an ice cream in the morning affects whether she is permitted to eat one in the
afternoon. This is closely related to conditional norms (e.g. conditional
obligations) discussed in the literature van Fraassen (1973); Chellas (1974);
DeCew (1981); Rulli (2020) but is interpreted in multiagent transition systems
instead of possible-world semantics. The other direction could be the
interaction between permission and responsibility in multiagent settings. It
might have been noticed that our introductory example about factories and fish
is a variant of (Halpern, 2015, Example 3.11) and (Halpern, 2016, Example
6.2.5), which talk about causality and responsibility in multiagent settings.
Indeed, the connection between obligation and responsibility in linguistic
intuition has already been noticed by philosophers van de Poel (2011).
However, a formal investigation of the interaction among norm, causation, and
responsibility in multiagent settings is still lacking.

## Acknowledgements

I would like to express my sincere gratitude to Dr. Pavel Naumov, my PhD
supervisor, for his selfless help in completing this paper. The research is
funded by the China Scholarship Council (CSC No.202206070014).

## References

  * Alur et al. (2002) Rajeev Alur, Thomas A Henzinger, and Orna Kupferman.  Alternating-time temporal logic.  Journal of the ACM, 49(5):672–713, 2002.
  * Anderson (1956) Alan Ross Anderson.  The formal analysis of normative systems.  Technical report, Office of Naval Research, 1956.
  * Anderson (1967) Alan Ross Anderson.  Some nasty problems in the formal logic of ethics.  Noûs, pages 345–360, 1967.
  * Anglberger et al. (2015) Albert JJ Anglberger, Nobert Gratzl, and Olivier Roy.  Obligation, free choice, and the logic of weakest permissions.  The Review of Symbolic Logic, 8(4):807–827, 2015.
  * Areces et al. (2023) Carlos Areces, Valentin Cassano, Pablo F Castro, Raul Fervari, and Andrés R Saravia.  A deontic logic of knowingly complying.  In Proceedings of the 22nd International Conference on Autonomous Agents and MultiAgent Systems, volume 23, 2023.
  * Arkoudas et al. (2005) Konstantine Arkoudas, Selmer Bringsjord, and Paul Bello.  Toward ethical robots via mechanized deontic logic.  In AAAI Fall Symposium on Machine Ethics, pages 17–23. The AAAI Press Menlo Park, CA, USA, 2005.
  * Asher and Bonevac (2005) Nicholas Asher and Daniel Bonevac.  Free choice permission is strong permission.  Synthese, 145:303–323, 2005.
  * Belnap and Perloff (1988) Nuel Belnap and Michael Perloff.  Seeing to it that: a canonical form for agentives.  Theoria, 54(3):175–199, 1988.
  * Belnap and Perloff (1992) Nuel Belnap and Michael Perloff.  The way of the agent.  Studia Logica, pages 463–484, 1992.
  * Broersen and Ramírez Abarca (2018) Jan Broersen and Aldo Iván Ramírez Abarca.  Formalising oughts and practical knowledge without resorting to action types.  In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, pages 1877–1879, 2018.
  * Broersen (2008) Jan Broersen.  A complete STIT logic for knowledge and action, and some of its applications.  In Proceedings of the 6th International Workshop on Declarative Agent Languages and Technologies, pages 47–59. Springer, 2008.
  * Broersen (2011) Jan Broersen.  Deontic epistemic STIT logic distinguishing modes of mens rea.  Journal of Applied Logic, 9(2):137–152, 2011.
  * Chellas (1969) Brian Farrell Chellas.  The logical form of imperatives.  Stanford University, 1969.
  * Chellas (1974) Brian F Chellas.  Conditional obligation.  In Logical Theory and Semantic Analysis: Essays Dedicated to Stig Kanger on His Fiftieth Birthday, pages 23–33. Springer, 1974.
  * Chisholm (1964) Roderick M Chisholm.  The ethics of requirement.  American Philosophical Quarterly, 1(2):147–153, 1964.
  * DeCew (1981) Judith Wagner DeCew.  Conditional obligation and counterfactuals.  Journal of Philosophical Logic, pages 55–72, 1981.
  * Governatori et al. (2013) Guido Governatori, Francesco Olivieri, Antonino Rotolo, and Simone Scannapieco.  Computing strong and weak permissions in defeasible logic.  Journal of Philosophical Logic, 42:799–829, 2013.
  * Halpern (2015) Joseph Y Halpern.  A modification of the halpern-pearl definition of causality.  In Proceedings of the 24th International Conference on Artificial Intelligence, pages 3022–3033, 2015.
  * Halpern (2016) Joseph Y Halpern.  Actual causality.  MIT Press, 2016.
  * Horty and Belnap (1995) John F Horty and Nuel Belnap.  The deliberative STIT: a study of action, omission, ability, and obligation.  Journal of Philosophical Logic, 24(6):583–644, 1995.
  * Horty (2001) John F Horty.  Agency and Deontic Logic.  Oxford University Press, 2001.
  * Kamp (1973) Hans Kamp.  Free choice permission.  In Proceedings of the Aristotelian Society, volume 74, pages 57–74. JSTOR, 1973.
  * Kanger (1971) Stig Kanger.  New Foundations for Ethical Theory.  Springer, 1971.
  * Knight et al. (2022) Sophia Knight, Pavel Naumov, Qi Shi, and Vigasan Suntharraj.  Truth set algebra: a new way to prove undefinability.  arXiv:2208.04422, 2022.
  * Kulicki and Trypuz (2017) Piotr Kulicki and Robert Trypuz.  Connecting actions and states in deontic logic.  Studia Logica, 105:915–942, 2017.
  * Kulicki et al. (2023) Piotr Kulicki, Robert Trypuz, Robert Craven, and Marek J Sergot.  A unified logical framework for reasoning about deontic properties of actions and states.  Logic and Logical Philosophy, pages 1–35, 2023.
  * Lewis (1979) David Lewis.  A problem about permission.  In Essays in Honour of Jaakko Hintikka, pages 163–175. Springer, 1979.
  * McNamara and van de Putte (2022) Paul McNamara and Frederik van de Putte.  Deontic logic.  In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, 2022\.
  * Mendelson (2009) Elliott Mendelson.  Introduction to Mathematical Logic.  CRC press, 2009.
  * Müller-Olm et al. (1999) Markus Müller-Olm, David Schmidt, and Bernhard Steffen.  Model-checking: a tutorial introduction.  In Static Analysis: Proceedings of the 6th International Symposium, pages 330–354. Springer, 1999.
  * Pandžić et al. (2022) Stipe Pandžić, Jan Broersen, and Henk Aarts.  Boid*: autonomous goal deliberation through abduction.  In Proceedings of the 21st International Conference on Autonomous Agents and MultiAgent Systems, pages 1019–1027, 2022.
  * Prior (1963) Arthur N Prior.  The logic of modality.  In Formal Logic, pages 186–229. Oxford University Press, 1963.
  * Raz (1975) Joseph Raz.  Permissions and supererogation.  American Philosophical Quarterly, 12(2):161–168, 1975.
  * Ross (1944) Alf Ross.  Imperatives and logic.  Philosophy of Science, 11(1):30–46, 1944.
  * Royakkers (1997) Lamber MM Royakkers.  Giving permission implies giving choice.  In Proceedings of the 8th International Conference on Database and Expert Systems Applications, pages 198–203. IEEE, 1997.
  * Rulli (2020) Tina Rulli.  Conditional obligations.  Social Theory and Practice, pages 365–390, 2020.
  * van Benthem (1979) Johan van Benthem.  Minimal deontic logics.  Bulletin of the Section of Logic, 8(1):36–42, 1979.
  * van de Poel (2011) Ibo van de Poel.  The relation between forward-looking and backward-looking responsibility.  In Moral Responsibility: Beyond Free Will and Determinism, pages 37–52. Springer, 2011.
  * van de Putte (2017) Frederik van de Putte.  Free choice permission in STIT.  In Logica yearbook 2016, pages 289–303. College Publications, 2017\.
  * van Fraassen (1973) Bas C van Fraassen.  The logic of conditional obligation.  In Exact Philosophy, pages 151–172. Springer, 1973.
  * von Wright (1951) Georg Henrik von Wright.  Deontic logic.  Mind, 60(237):1–15, 1951.
  * von Wright (1968) Georg Henrik von Wright.  An Essay in Deontic Logic and the General Theory of Action: With a Bibliography of Deontic and Imperative Logic.  North-Holland Pub. Co, 1968.
  * Wang and Wang (2023) Zilu Wang and Yanjing Wang.  Strong permission bundled: first steps.  In Proceedings of the 16th International Conference on Deontic Logic and Normative Systems, pages 217–234. Springer, 2023.

Technical Appendix

##  Appendix A Model Checking

We consider the global model checking problem in finite transition systems.
Specifically, let us consider an arbitrary finite transition system
$(S,\Delta,D,M,\pi)$. By Definition 2, for each formula $\varphi\in\Phi$, the
calculation of the truth set $\llbracket\varphi\rrbracket$ uses a recursive
process on the structural complexity of $\varphi$:

  1. 1.

if $\varphi$ is a propositional variable, then
$\llbracket\varphi\rrbracket=\pi(\varphi)$;

  2. 2.

if $\varphi=\neg\psi$, then
$\llbracket\varphi\rrbracket=S\setminus\llbracket\psi\rrbracket$;

  3. 3.

if $\varphi=\psi_{1}\vee\psi_{2}$, then
$\llbracket\psi\rrbracket=\llbracket\psi_{1}\rrbracket\cup\llbracket\psi_{2}\rrbracket$;

  4. 4.

if $\varphi=\text{WA}_{a}\psi$, then
$\llbracket\varphi\rrbracket=\llbracket\text{WA}_{a}\psi\rrbracket$ using
Algorithm 1;

  5. 5.

if $\varphi=\text{WE}_{a}\psi$, then
$\llbracket\varphi\rrbracket=\llbracket\text{WE}_{a}\psi\rrbracket$ using
Algorithm 2;

  6. 6.

if $\varphi=\text{SE}_{a}\psi$, then
$\llbracket\varphi\rrbracket=\llbracket\text{SE}_{a}\psi\rrbracket$ using
Algorithm 3;

  7. 7.

if $\varphi=\text{SA}_{a}\psi$, then
$\llbracket\varphi\rrbracket=\llbracket\text{SA}_{a}\psi\rrbracket$ using
Algorithm 4.

Denote by $|S|$ the number of the states in the transition system, by
$|\Delta|=\sum_{s\in S}\sum_{a\in\mathcal{A}}|\Delta_{a}^{s}|$ the size of the
action space, and by $|M|=\sum_{s\in S}|M_{s}|$ the size of the mechanism. We
analyse the computational time complexity of model checking. Note that, for a
finite set $S$ of states, a subset of the states can be represented with a
Boolean array of the size $O(|S|)$. Then, the set operations that determine
whether a set contains an element, add an element to a set, or remove an
element from a set take $O(1)$. The other set operations (union, intersection,
difference and complement) and determining the subset relation take $O(|S|)$.
The same is true for a finite action space.

Since the size of the truth set $\llbracket\varphi\rrbracket$ is $O(|S|)$ for
each formula $\varphi\in\Phi$, the computational complexity of each instance
of the first three types of recursive steps mentioned above is $O(|S|)$. Next,
we analyse the computational complexity of the rest four types of recursive
steps.

Algorithm 1 shows the pseudocode for calculating the truth set
$\llbracket\text{WA}_{a}\psi\rrbracket$, given the transition system, the
agent $a$, and the truth set $\llbracket\psi\rrbracket$. Note that, for each
state $s\in S$, if a tuple $(\delta,t)\in M_{s}$ such that $t\Vdash\psi$
exists, then $(s,\delta_{a})\not\rightsquigarrow_{a}\neg\psi$ by Definition 2;
if $\delta_{a}\in D_{a}^{s}$ is also true, then $s\Vdash\text{WA}_{a}\psi$ by
item 4 of Definition 2. Algorithm 1 first defines an empty set $Collector$
(line 1) to collect all states satisfying $\text{WA}_{a}\psi$. Then, for each
state $s$ (line 1), the algorithm searches for a tuple $(\delta,t)\in M_{s}$
(line 1) such that $\delta_{a}\in D_{a}^{s}$ and $t\Vdash\psi$ (line 1). If
such a tuple is found, then $s\Vdash\text{WA}_{a}\psi$. Thus, the algorithm
adds state $s$ into the set $Collector$ (line 1) and goes to check the next
state (line 1).

Note that, the set $Collector$ defined in line 1 is represented by a Boolean
array of the size $O(|S|)$. Thus, the execution of line 1 takes $O(|S|)$.
Also, the if statement in line 1 is executed at most $\sum_{s\in
S}|M_{s}|=|M|$ times in total. Each execution of line 1 and line 1 takes
$O(1)$. Hence, the time complexity of Algorithm 1 is $O(|S|+|M|)$.

Input: transition system $(S,\Delta,D,M,\pi)$, agent $a$, the truth set
$\llbracket\psi\rrbracket$

Output: the truth set $\llbracket\text{WA}_{a}\psi\rrbracket$

1 $Collector\leftarrow\varnothing$;

2 for  _each state $s\in S$_ do

3 for  _each tuple $(\delta,t)\in M_{s}$_ do

4 if  _$\delta_{a}\in D_{a}^{s}$ and $t\in\llbracket\psi\rrbracket$_ then

5 $Collector$.add($s$);

6 break;

7

8

9

10return $Collector$;

Algorithm 1 Calculation of the truth set
$\llbracket\text{WA}_{a}\psi\rrbracket$

Algorithm 2 shows the pseudocode for calculating the truth set
$\llbracket\text{WE}_{a}\psi\rrbracket$, given the transition system, the
agent $a$, and the truth set $\llbracket\psi\rrbracket$. For each state $s\in
S$, if there is a permitted action $i\in D_{a}^{s}$ such that
$(s,i)\rightsquigarrow_{a}\psi$, then $s\Vdash\text{WE}_{a}\psi$ by item 5 of
Definition 2. Note that, if there exists a tuple $(\delta,t)\in M_{s}$ such
that $t\nVdash\psi$, then $(s,\delta_{a})\not\rightsquigarrow_{a}\psi$ by
Definition 2. Algorithm 2 first defines an empty set $Collector$ (line 2) to
collect all states satisfying $\text{WE}_{a}\psi$. Then, for each state $s$
(line 2), a set $Ensurer$ is initialised to be the set $\Delta_{a}^{s}$ (line
2), from which the actions $i\in\Delta_{a}^{s}$ such that
$(s,i)\not\rightsquigarrow_{a}\psi$ would be removed. After that, the
algorithm checks for each tuple $(\delta,t)\in M_{s}$ (line 2) if
$t\nVdash\psi$ (line 2). If so, then
$(s,\delta_{a})\not\rightsquigarrow_{a}\psi$. Thus, the algorithm removes
action $\delta_{a}$ from the set $Ensurer$ (line 2). When the for loop in
lines 2 \- 2 ends, the set $Ensurer$ consists of all actions
$i\in\Delta_{a}^{s}$ such that $(s,i)\rightsquigarrow_{a}\psi$. Then, the if
statement in line 2 checks if there is a permitted action $i$ of agent $a$ in
state $s$ such that $i\in Ensurer$. If so, then $s\Vdash\text{WE}_{a}\psi$.
Thus, the algorithm adds state $s$ into the set $Collector$ (line 2).

Similar to lines 1 and 1 of Algorithm 1, in Algorithm 2, the execution of line
2 and the if statement in line 2 takes $O(|S|)$ and $O(|M|)$, respectively.
Note that, the set $Ensurer$ defined in line 2 is represented by a Boolean
array of length $|\Delta_{a}^{s}|$. Then, the execution of lines 2 and 2 takes
$O(|\Delta_{a}^{s}|)$ for each state $s$. Thus, the execution of lines 2 and 2
takes $\sum_{s\in S}O(|\Delta_{a}^{s}|)=O(|\Delta|)$ in total. Meanwhile, line
2 are executed $|S|$ times and each execution takes $O(1)$. Hence, the time
complexity of Algorithm 2 is $O(|S|\\!+\\!|M|\\!+\\!|\Delta|)$.

Input: transition system $(S,\Delta,D,M,\pi)$, agent $a$, the truth set
$\llbracket\psi\rrbracket$

Output: the truth set $\llbracket\text{WE}_{a}\psi\rrbracket$

1 $Collector\leftarrow\varnothing$;

2 for  _each state $s\in S$_ do

3 $Ensurer\leftarrow\Delta_{a}^{s}$;

4 for  _each tuple $(\delta,t)\in M_{s}$_ do

5 if  _$t\notin\llbracket\psi\rrbracket$_ then

6 $Ensurer$.remove($\delta_{a}$);

7

8

9 if  _$Ensurer\cap D_{a}^{s}\neq\varnothing$_ then

10 $Collector$.add($s$);

11

12

13return $Collector$;

Algorithm 2 Calculation of the truth set
$\llbracket\text{WE}_{a}\psi\rrbracket$

Algorithm 3 shows the pseudocode for calculating the truth set
$\llbracket\text{SE}_{a}\psi\rrbracket$, given the transition system, the
agent $a$, and the truth set $\llbracket\psi\rrbracket$. For each state $s\in
S$, if $i\in D_{a}^{s}$ for each action $i$ such that
$(s,i)\rightsquigarrow_{a}\psi$, then $s\Vdash\text{SE}_{a}\psi$ by item 6 of
Definition 2. Algorithm 3 first defines an empty set $Collector$ (line 3) to
collect all states satisfying $\text{SE}_{a}\psi$. Lines 3 \- 3 of Algorithm 3
are identical to those of Algorithm 2, where the set $Ensurer$ consists of all
actions $i\in\Delta_{a}^{s}$ such that $(s,i)\rightsquigarrow_{a}\psi$ when
the for loop in lines 3 \- 3 ends. Then, the if statement in line 3 checks if
every action $i\in Ensurer$ is permitted. If so, then
$s\Vdash\text{SE}_{a}\psi$. Thus, the algorithm adds state $s$ into the set
$Collector$ (line 3).

Due to the similarity between Algorithm 3 and Algorithm 2, the computational
complexity of Algorithm 3 is the same as that of Algorithm 2, which is
$O(|S|\\!+\\!|M|\\!+\\!|\Delta|)$.

Input: transition system $(S,\Delta,D,M,\pi)$, agent $a$, the truth set
$\llbracket\psi\rrbracket$

Output: the truth set $\llbracket\text{SE}_{a}\psi\rrbracket$

1 $Collector\leftarrow\varnothing$;

2 for  _each state $s\in S$_ do

3 $Ensurer\leftarrow\Delta_{a}^{s}$;

4 for  _each tuple $(\delta,t)\in M_{s}$_ do

5 if  _$t\notin\llbracket\psi\rrbracket$_ then

6 $Ensurer$.remove($\delta_{a}$);

7

8

9 if  _$Ensurer\subseteq D_{a}^{s}$_ then

10 $Collector$.add($s$);

11

12

13return $Collector$;

Algorithm 3 Calculation of the truth set
$\llbracket\text{SE}_{a}\psi\rrbracket$

Algorithm 4 shows the pseudocode for calculating the truth set
$\llbracket\text{SA}_{a}\psi\rrbracket$, given the transition system, the
agent $a$, and the truth set $\llbracket\psi\rrbracket$. Note that, for each
state $s\in S$, if a tuple $(\delta,t)\in M_{s}$ such that $t\Vdash\psi$
exists, then $(s,\delta_{a})\not\rightsquigarrow_{a}\neg\psi$ by Definition 2;
if $\delta_{a}\notin D_{a}^{s}$ is also true, then $s\nVdash\text{SA}_{a}\psi$
by item 7 of Definition 2. Algorithm 4 first defines a set $Sieve$ and
initialises it to be the set of all states (line 4). From the set $Sieve$,
each state not satisfying $\text{SA}_{a}\psi$ would be removed. Then, for each
state $s$ (line 4), the algorithm searches for a tuple $(\delta,t)\in M_{s}$
(line 4) such that $\delta_{a}\notin D_{a}^{s}$ and $t\Vdash\psi$ (line 4). If
such a tuple is found, then $s\nVdash\text{SA}_{a}\psi$. Thus, the algorithm
removes $s$ from the set $Sieve$ (line 4) and goes to check the next state
(line 4).

Due to the similarity between Algorithm 4 and Algorithm 1, it is easy to
observe that the time complexity of Algorithm 4 is $O(|S|+|M|)$.

Input: transition system $(S,\Delta,D,M,\pi)$, agent $a$, the truth set
$\llbracket\psi\rrbracket$

Output: the truth set $\llbracket\text{SA}_{a}\psi\rrbracket$

1 $Sieve\leftarrow S$;

2 for  _each state $s\in S$_ do

3 for  _each tuple $(\delta,t)\in M_{s}$_ do

4 if  _$\delta_{a}\notin D_{a}^{s}$ and $t\in\llbracket\psi\rrbracket$_ then

5 $Sieve$.remove($s$);

6 break;

7

8

9

10return $Sieve$;

Algorithm 4 Calculation of the truth set
$\llbracket\text{SA}_{a}\psi\rrbracket$

To sum up, the model-checking (time) complexity for a formula $\varphi\in\Phi$
is $O\big{(}|\varphi|\cdot(|S|\\!+\\!|M|\\!+\\!|\Delta|)\big{)}$, where
$|\varphi|$ is the size of the formula, $|S|$ is the number of states, $|M|$
is the size of the mechanism, and $|\Delta|$ is the size of the action space.

##  Appendix B Proofs of the Undefinability Results

Figure 1: Toward undefinability of WA through WE, SA, and SE.

We explain the truth set algebra technique while presenting the undefinability
result for modality WA in Subection B.1. The proofs of the undefinability
results for modalities WE, SE, and SA go in a similar way as WA except for
using different transition systems. We sketch the proofs of the other three
undefinability results in Subsection B.2, Subsection B.3, and Subsection B.4.

###  B.1 Undefinability of WA Through WE, SE, and SA

Without loss of generality, in this subsection, we assume that the language
has not only at least two agents but exactly two of them. We refer to these
agents as $a$ and $b$. Additionally, also without loss of generality, we
assume that the language contains a single propositional variable $p$.

Unlike the well-known bisimulation technique, which uses two models to prove
undefinability, the truth set algebra method uses only one model. In our case,
the model is a transition system depicted in the left of Figure 1. This
transition system has three states: $s$, $t$, and $u$ visualised in the
diagram as rectangles. The set $\Delta^{y}_{x}$ of actions available to agent
$x$ in state $y$ is shown inside the corresponding rectangle. For example,
$\Delta^{s}_{a}=\\{1,2\\}$. Note that we use integers to denote actions.
Uniformly, we use positive integers to denote the permitted actions in the set
$D^{y}_{x}$ and negative integers to denote the non-permitted actions in all
the transition systems that will be used to prove our undefinability results.
Specifically, in the transition systems shown in the left of Figure 1, every
action is permitted.

We denote action profiles by pairs $(i,j)$, where $i$ is the action of agent
$a$ and $j$ is the action of agent $b$ under the profile. The mechanism of the
transition system is visualised in the left part of Figure 1 using labelled
arrows. For example, the label $(2,1)$ on the arrow from state $s$ to state
$t$ denotes the fact that $((2,1),t)\in M_{s}$. Finally, we assume that
$\pi(p)=\\{u\\}$.

In the left part of Figure 1, we visualise the transition system that will be
used in the proof. In the middle part and the right part of the same figure,
we use the miniaturisation of the transition system (i.e. diagram) to
visualise a subset of the set of states. For example, in the diagram in the
right part of Figure 1, we visualise the set $\\{s,u\\}$ of states by shading
grey the two rectangles corresponding to states $s$ and $u$. Specifically, we
use the diagrams to denote some truth sets as shown at the bottom of each
diagram.

Let us now consider the family of four truth sets $\mathcal{F}=\\{\llbracket
p\rrbracket,\llbracket\neg
p\rrbracket,\llbracket\top\rrbracket,\llbracket\bot\rrbracket\\}$ as
visualised in the four diagrams in the middle part of Figure 1. Intuitively,
the next lemma shows that, for the above-described transition system, the
family $\mathcal{F}$ is closed with respect to modalities WE, SE, and SA.

######  Lemma 8.

$\llbracket\text{WE}_{x}\varphi\rrbracket,\llbracket\text{SE}_{x}\varphi\rrbracket,\llbracket\text{SA}_{x}\varphi\rrbracket\in\mathcal{F}$
for any agent $x\in\\{a,b\\}$ and any formula $\varphi\in\Phi$ such that
$\llbracket\varphi\rrbracket\in\mathcal{F}$.

###### Proof.

We first show that if $\llbracket\varphi\rrbracket=\llbracket p\rrbracket$,
then $\llbracket\text{WE}_{a}\varphi\rrbracket=\llbracket p\rrbracket$.
Indeed, $\llbracket\varphi\rrbracket=\\{u\\}$.

Note that $D_{a}^{s}=\\{1,2\\}$. When taken by agent $a$ in state $s$, both
actions $1$ and $2$ allow $t$ to be the next state, see Figure 1. Then,
$(s,1)\not\rightsquigarrow_{a}\varphi$ and
$(s,2)\not\rightsquigarrow_{a}\varphi$ as
$\llbracket\varphi\rrbracket=\\{u\\}$. Hence, $s\nVdash\text{WE}_{a}\varphi$
by item 5 of Definition 2 and that $D_{a}^{s}=\\{1,2\\}$. One can similarly
know that $t\notin\llbracket\text{WE}_{a}\varphi\rrbracket$.

On the contrary, the only action available to agent $a$ in state $u$, action
$1$, guarantees that the next state is again $u$. Then,
$(u,1)\rightsquigarrow_{a}\varphi$ for the action $1\in D^{u}_{a}$ as
$\llbracket\varphi\rrbracket=\\{u\\}$. Hence, $u\Vdash\text{WE}_{a}\varphi$ by
item 5 of Definition 2. Therefore,
$u\in\llbracket\text{WE}_{a}\varphi\rrbracket$ by Definition 3.

In conclusion, if $\llbracket\varphi\rrbracket=\llbracket p\rrbracket$, then
$\llbracket\text{WE}_{a}\varphi\rrbracket=\\{u\\}=\llbracket p\rrbracket$. We
visualise this observation by a dashed arrow labelled with $\text{WE}_{a}$ in
the middle part of Figure 1 from the diagram $\llbracket p\rrbracket$ to
itself.

The proofs for the other 23 cases are similar. We show the corresponding
labelled dashed arrows in the middle part of Figure 1. ∎

######  Lemma 9.

$\llbracket\varphi\rrbracket\in\mathcal{F}$ for each formula $\varphi\in\Phi$
that does not contain modality WA.

###### Proof.

We prove the statement of the lemma by induction on the structural complexity
of formula $\varphi$. If formula $\varphi$ is the propositional variable $p$,
then the statement of the lemma holds because $\llbracket
p\rrbracket\in\mathcal{F}$.

Suppose that formula $\varphi$ has the form $\neg\psi$. Then,
$\llbracket\varphi\rrbracket=\\{s,t,u\\}\setminus\llbracket\psi\rrbracket$ by
item 2 of Definition 2 and Definition 3. Observe that family $\mathcal{F}$ is
closed with respect to the complement, see the middle part of Figure 1. Thus,
if $\llbracket\psi\rrbracket\in\mathcal{F}$, then
$\llbracket\varphi\rrbracket\in\mathcal{F}$. Therefore, by the induction
hypothesis, $\llbracket\varphi\rrbracket\in\mathcal{F}$.

Assume that formula $\varphi$ has the form $\psi_{1}\vee\psi_{2}$. Then,
$\llbracket\varphi\rrbracket=\llbracket\psi_{1}\rrbracket\cup\llbracket\psi_{2}\rrbracket$
by item 3 of Definition 2 and Definition 3. Observe that family $\mathcal{F}$
is closed with respect to the union, see the middle part of Figure 1. Thus, if
$\llbracket\psi_{1}\rrbracket,\llbracket\psi_{2}\rrbracket\in\mathcal{F}$,
then $\llbracket\varphi\rrbracket\in\mathcal{F}$. Therefore, by the induction
hypothesis, $\llbracket\varphi\rrbracket\in\mathcal{F}$.

If formula $\varphi$ has one of the forms $\text{WE}_{a}\psi$,
$\text{WE}_{b}\psi$, $\text{SE}_{a}\psi$, $\text{SE}_{b}\psi$,
$\text{SA}_{a}\psi$, or $\text{SA}_{b}\psi$, then the statement of the lemma
follows from the induction hypothesis by Lemma 8. ∎

######  Lemma 10.

$\llbracket\text{WA}_{a}p\rrbracket\notin\mathcal{F}$.

###### Proof.

The truth set $\llbracket\text{WA}_{a}p\rrbracket$ is depicted at the right of
Figure 1. This could be verified using an argument similar to the one used in
the proof of Lemma 8. ∎

Theorem 2 follows from Definition 4 and the two previous lemmas.

Theorem 2 (undefinability of WA) The formula $\text{WA}_{a}p$ is not
semantically equivalent to any formula in language $\Phi$ that does not use
modality WA.

Figure 2: Toward undefinability of WE through WA, SA, and SE.

Figure 3: Toward undefinability of SE through WA, WE, and SA.

Figure 4: Toward undefinability of SA through WA, WE, and SE.

###  B.2 Undefinability of WE Through WA, SE, and SA

In this case, we use the transition system depicted in the left of Figure 2.
We depict the description of the transition system in the same way as in
Figure 1. Note that, the permitted actions are still denoted by positive
integers. The family of truth sets to consider here is
$\mathcal{F}=\\{\llbracket p\rrbracket,\llbracket\neg
p\rrbracket,\llbracket\top\rrbracket,\llbracket\bot\rrbracket\\}$, as
visualised in the middle of Figure 2.

The next three lemmas can be proved in a similar way as Lemma 8, Lemma 9, and
Lemma 10 except for using Figure 2 instead of Figure 4.

######  Lemma 11.

$\llbracket\text{WA}_{x}\varphi\rrbracket,\llbracket\text{SE}_{x}\varphi\rrbracket,\llbracket\text{SA}_{x}\varphi\rrbracket\in\mathcal{F}$
for any agent $x\in\\{a,b\\}$ and any formula $\varphi\in\Phi$ such that
$\llbracket\varphi\rrbracket\in\mathcal{F}$.

######  Lemma 12.

$\llbracket\varphi\rrbracket\in\mathcal{F}$ for each formula $\varphi\in\Phi$
that does not contain modality WE.

######  Lemma 13.

$\llbracket\text{WE}_{a}p\rrbracket\notin\mathcal{F}$.

The next theorem follows from Definition 4, Lemma 12, and Lemma 13.

######  Theorem 5 (undefinability of WE).

The formula $\text{WE}_{a}p$ is not semantically equivalent to any formula in
language $\Phi$ that does not use modality WE.

###  B.3 Undefinability of SE Through WA, WE, and SA

In this case, we use the transition system depicted in the left of Figure 3.
Note that, in this transition system, not all actions are permitted. In
particular, the permitted actions are denoted by positive integers and the
non-permitted actions are denoted by negative integers. It is worth mentioning
that, by the continuity condition in item 4 of Definition 1, a next state
always exists even if the agents take non-permitted actions. The family of
truth sets to consider here is $\mathcal{F}=\\{\llbracket
p\rrbracket,\llbracket\neg
p\rrbracket,\llbracket\top\rrbracket,\llbracket\bot\rrbracket\\}$, as
visualised in the middle of Figure 3.

The next three lemmas can be proved in a similar way as Lemma 8, Lemma 9, and
Lemma 10 except for using Figure 3 instead of Figure 1.

######  Lemma 14.

$\llbracket\text{WA}_{x}\varphi\rrbracket,\llbracket\text{WE}_{x}\varphi\rrbracket,\llbracket\text{SA}_{x}\varphi\rrbracket\in\mathcal{F}$
for any agent $x\in\\{a,b\\}$ and any formula $\varphi\in\Phi$ such that
$\llbracket\varphi\rrbracket\in\mathcal{F}$.

######  Lemma 15.

$\llbracket\varphi\rrbracket\in\mathcal{F}$ for each formula $\varphi\in\Phi$
that does not contain modality SE.

######  Lemma 16.

$\llbracket\text{SE}_{a}p\rrbracket\notin\mathcal{F}$.

The next theorem follows from Definition 4, Lemma 15, and Lemma 16.

######  Theorem 6 (undefinability of SE).

The formula $\text{SE}_{a}p$ is not semantically equivalent to any formula in
language $\Phi$ that does not use modality SE.

###  B.4 Undefinability of SA Through SE, WA, and WE

In this case, we use the transition system depicted in the left part of Figure
4. We consider the family of truth sets $\mathcal{F}=\\{\llbracket
p\rrbracket,\llbracket\neg
p\rrbracket,\llbracket\top\rrbracket,\llbracket\bot\rrbracket\\}$, which are
visualised in the middle of Figure 4.

The next three lemmas can be proved in a similar way as Lemma 8, Lemma 9, and
Lemma 10 except for using Figure 4 instead of Figure 1.

######  Lemma 17.

$\llbracket\text{WA}_{x}\varphi\rrbracket,\llbracket\text{WE}_{x}\varphi\rrbracket,\llbracket\text{SE}_{x}\varphi\rrbracket\in\mathcal{F}$
for any agent $x\in\\{a,b\\}$ and any formula $\varphi\in\Phi$ such that
$\llbracket\varphi\rrbracket\in\mathcal{F}$.

######  Lemma 18.

$\llbracket\varphi\rrbracket\in\mathcal{F}$ for each formula $\varphi\in\Phi$
that does not contain modality SA.

######  Lemma 19.

$\llbracket\text{SA}_{a}p\rrbracket\notin\mathcal{F}$.

The next result follows from Definition 4, Lemma 18, and Lemma 19.

######  Theorem 7 (undefinability of SA).

The formula $\text{SA}_{a}p$ is not semantically equivalent to any formula in
language $\Phi$ that does not use modality SA.

Figure 5: Toward mutual undefinability of WA (top) and SA (bottom) in single-
agent deterministic settings.

###  B.5 Undefinability in Single-Agent Deterministic Settings

To show the mutual undefinability of modalities WA and SA in single-agent
deterministic settings, we use the two transition systems in the left of
Figure 5. The proofs are omitted because they are similar to the proof of
Theorem 2 in Subsection B.1.

##  Appendix C Proofs Toward Section 5

###  C.1 WE is “Weak”, SE is “Strong”

######  Theorem 8.

The rule $\dfrac{\varphi\to\psi}{\text{WE}_{a}\varphi\to\text{WE}_{a}\psi}$ is
admissible.

###### Proof.

Suppose that $\vdash\varphi\to\psi$. Then,
$\vdash\varphi\wedge\neg\psi\to\bot$ by the laws of propositional reasoning.
Thus, by inference rule IR2,
$\vdash\text{WA}_{a}(\varphi\wedge\neg\psi)\to\text{WA}_{a}\bot$. Then, by the
law of contraposition,
$\vdash\neg\text{WA}_{a}\bot\to\neg\text{WA}_{a}(\varphi\wedge\neg\psi)$.
Hence, by axiom A1 and the Modus Ponens rule,
$\vdash\neg\text{WA}_{a}(\varphi\wedge\neg\psi)$. Thus,
$\vdash\neg\text{WE}_{a}\varphi\vee\text{WE}_{a}\psi$ by the contrapositive of
axiom A7. Therefore, $\vdash\text{WE}_{a}\varphi\to\text{WE}_{a}\psi$ by
propositional reasoning. ∎

Theorem 8 shows that WE is a form of weak permission.

######  Theorem 9.

The rule $\dfrac{\varphi\to\psi}{\text{SE}_{a}\psi\to\text{SE}_{a}\varphi}$ is
admissible.

###### Proof.

Suppose that $\vdash\varphi\to\psi$. Then,
$\vdash\varphi\wedge\neg\psi\to\bot$ by the laws of propositional reasoning.
Thus, by inference rule IR3,
$\vdash\text{SA}_{a}\bot\to\text{SA}_{a}(\varphi\wedge\neg\psi)$. Hence, by
axiom A3 and the Modus Ponens rule,
$\vdash\text{SA}_{a}(\varphi\wedge\neg\psi)$. Thus,
$\vdash\text{SE}_{a}\varphi\vee\neg\text{SE}_{a}\psi$ by the contrapositive of
axiom A8. Therefore, by propositional reasoning,
$\vdash\text{SE}_{a}\psi\to\text{SE}_{a}\varphi$. ∎

Theorem 9 shows that SE is a form of strong permission.

###  C.2 Proof of Lemma 2

Lemma 2 (deduction) If $X,\varphi\vdash\psi$, then $X\vdash\varphi\to\psi$.

###### Proof.

Suppose that sequence $\psi_{1},\dots,\psi_{n}$ is a proof of $\psi$ from set
$X\cup\\{\varphi\\}$ and the theorems of our logical system that uses the
Modus Ponens rule only. In other words, for each $k\leq n$, either

  1. 1.

$\vdash\psi_{k}$, or

  2. 2.

$\psi_{k}\in X$, or

  3. 3.

$\psi_{k}$ is equal to $\varphi$, or

  4. 4.

there are $i,j<k$ such that formula $\psi_{j}$ has the form of
$\psi_{i}\to\psi_{k}$.

It suffices to show that $X\vdash\varphi\to\psi_{k}$ for each $k\leq n$. We
prove this by induction on $k$ by considering the four cases above separately.

Case 1: $\vdash\psi_{k}$. Note that $\psi_{k}\to(\varphi\to\psi_{k})$ is a
propositional tautology, and thus, is an axiom of our logical system. Hence,
$\vdash\varphi\to\psi_{k}$ by the Modus Ponens rule. Therefore,
$X\vdash\varphi\to\psi_{k}$.

Case 2: $\psi_{k}\in X$. Then, $X\vdash\psi_{k}$.

Case 3: Formula $\psi_{k}$ is equal to $\varphi$. Thus, $\varphi\to\psi_{k}$
is a propositional tautology. Hence, $X\vdash\varphi\to\psi_{k}$.

Case 4: Formula $\psi_{j}$ is equal to $\psi_{i}\to\psi_{k}$ for some $i,j<k$.
In this case, by the induction hypothesis, $X\vdash\varphi\to\psi_{i}$ and
$X\vdash\varphi\to(\psi_{i}\to\psi_{k})$. Note that formula

$(\varphi\to\psi_{i})\to\big{(}(\varphi\to(\psi_{i}\to\psi_{k}))\to(\varphi\to\psi_{k})\big{)}$

is a propositional tautology. Therefore, $X\vdash\varphi\to\psi_{k}$ by
applying the Modus Ponens rule twice. ∎

###  C.3 Proofs of Lemma 4 and Lemma 5

#### Lemma 4.
$\vdash\text{WE}_{a}\varphi\wedge\neg\text{WA}_{a}\psi\to\text{WE}_{a}(\varphi\wedge\neg\psi)$.

###### Proof.

The propositional tautology $\varphi\wedge\neg(\varphi\wedge\neg\psi)\to\psi$,
by rule IR2, implies

$\vdash\text{WA}_{a}(\varphi\wedge\neg(\varphi\wedge\neg\psi))\to\text{WA}_{a}\psi.$

Then, by the instance

$\text{WE}_{a}\varphi\wedge\neg\text{WE}_{a}(\varphi\wedge\neg\psi)\to\text{WA}_{a}(\varphi\wedge\neg(\varphi\wedge\neg\psi))$

of axiom A7 and propositional reasoning

$\vdash\text{WE}_{a}\varphi\wedge\neg\text{WE}_{a}(\varphi\wedge\neg\psi)\to\text{WA}_{a}\psi.$

Therefore,
$\vdash\text{WE}_{a}\varphi\wedge\neg\text{WA}_{a}\psi\to\text{WE}_{a}(\varphi\wedge\neg\psi)$
again by propositional reasoning. ∎

#### Lemma 5.
$\vdash\neg\text{SE}_{a}\varphi\wedge\text{SA}_{a}\psi\to\neg\text{SE}_{a}(\varphi\wedge\neg\psi)$.

###### Proof.

The propositional tautology $\varphi\wedge\neg(\varphi\wedge\neg\psi)\to\psi$,
by rule IR3, implies

$\vdash\text{SA}_{a}\psi\to\text{SA}_{a}(\varphi\wedge\neg(\varphi\wedge\neg\psi)).$

By contraposition, the above statement implies

$\vdash\neg\text{SA}_{a}(\varphi\wedge\neg(\varphi\wedge\neg\psi))\to\neg\text{SA}_{a}\psi.$

Then, by the instance

$\neg\text{SE}_{a}\varphi\wedge\text{SE}_{a}(\varphi\wedge\neg\psi)\to\neg\text{SA}_{a}(\varphi\wedge\neg(\varphi\wedge\neg\psi))$

of axiom A8 and propositional reasoning,

$\vdash\neg\text{SE}_{a}\varphi\wedge\text{SE}_{a}(\varphi\wedge\neg\psi)\to\neg\text{SA}_{a}\psi.$

Therefore,
$\vdash\neg\text{SE}_{a}\varphi\wedge\text{SA}_{a}\psi\to\neg\text{SE}_{a}(\varphi\wedge\neg\psi)$
again by propositional reasoning. ∎

##  Appendix D Proof Toward Subsection 6.2

To improve the readability, in Subsection D.1, we first show four auxiliary
lemmas used in the induction steps of the proof for Lemma 7. Then, in
Subsection D.2, we prove Lemma 7. After that, we prove Theorem 4 in Subsection
D.3.

###  D.1 Auxiliary Lemmas

Let us first see a theorem of the logic system that will be used in the proofs
of the four auxiliary lemmas.

######  Lemma 20.

$\vdash\neg\text{WA}_{a}\varphi\wedge\text{SA}_{a}\top\to\neg\text{WA}_{b}\varphi\wedge\text{SA}_{b}\varphi$
.

###### Proof.

The propositional tautology $\varphi\to\varphi\wedge\top$, by rule IR2 and
propositional reasoning, implies

$\vdash\neg\text{WA}_{b}(\varphi\wedge\top)\to\neg\text{WA}_{b}\varphi,$

and by rule IR3, implies

$\vdash\text{SA}_{b}(\varphi\wedge\top)\to\text{SA}_{b}\varphi.$

Then, by propositional reasoning,

$\vdash\neg\text{WA}_{b}(\varphi\wedge\top)\wedge\text{SA}_{b}(\varphi\wedge\top)\to\neg\text{WA}_{b}\varphi\wedge\text{SA}_{b}\varphi.$

Thus, by the instance

$\neg\text{WA}_{a}\varphi\wedge\text{SA}_{a}\top\to\neg\text{WA}_{b}(\varphi\wedge\top)\wedge\text{SA}_{b}(\varphi\wedge\top),$

of axiom A9 and propositional reasoning,

$\vdash\neg\text{WA}_{a}\varphi\wedge\text{SA}_{a}\top\to\neg\text{WA}_{b}\varphi\wedge\text{SA}_{b}\varphi.$

∎

Now, we prove four auxiliary properties of the canonical model as four
separated lemmas.

######  Lemma 21.

For any state $s\in S$ and any formula $\text{WA}_{a}\varphi\in s$, there is a
tuple $(\delta,t)\in M_{s}$ such that $\delta_{a}\in D^{s}_{a}$ and
$\varphi\in t$.

###### Proof.

Consider the sets of agents

$\displaystyle B=$ $\displaystyle\\{b\in\mathcal{A}\;|\;b\neq
a,\text{SA}_{b}\top\in s\\},$ (20) $\displaystyle C=$
$\displaystyle\\{c\in\mathcal{A}\;|\;c\neq a,\neg\text{SA}_{c}\top\in s\\}.$
(21)

and the set of formulae

$\displaystyle X=$
$\displaystyle\\{\varphi\\}\cup\\{\neg\psi\;|\;\neg\text{WA}_{a}\psi\in s\\}$
(22) $\displaystyle\cup\\{\neg\chi\;|\;\exists\,b\in
B(\neg\text{WA}_{b}\chi\in s)\\}$
$\displaystyle\cup\\{\neg(\tau\wedge\sigma)\;|\;\exists\,c\in
C(\neg\text{WA}_{c}\tau\in s,\text{SA}_{c}\sigma\in s)\\}.$

######  Claim 3.

Set $X$ is consistent.

  * Proof of Claim. Suppose the opposite, then there are formulae

$\displaystyle\neg$
$\displaystyle\text{WA}_{a}\psi_{1},\dots,\neg\text{WA}_{a}\psi_{k}\in s,$
(23) $\displaystyle\neg$
$\displaystyle\text{WA}_{b_{1}}\chi_{1},\dots,\neg\text{WA}_{b_{\ell}}\chi_{\ell}\in
s,$ (24) $\displaystyle\neg$
$\displaystyle\text{WA}_{c_{1}}\tau_{1},\dots,\neg\text{WA}_{c_{m}}\tau_{m}\in
s,$ (25)
$\displaystyle\text{SA}_{c_{1}}\sigma_{1},\dots,\text{SA}_{c_{m}}\sigma_{m}\in
s,$ (26)

where

$\displaystyle b_{1},\dots,b_{\ell}\in B,$ (27) $\displaystyle
c_{1},\dots,c_{m}\in C,$ (28)

such that

$\varphi\wedge\bigwedge_{i\leq
k}\neg\psi_{i}\wedge\bigwedge_{i\leq\ell}\neg\chi_{i}\wedge\bigwedge_{i\leq
m}\neg(\tau_{i}\wedge\sigma_{i})\vdash\bot.$ (29)

By Lemma 20 and propositional reasoning, statements (24), (27), and (20) imply
that

$s\vdash\neg\text{WA}_{a}\chi_{i}\text{ for each $i\leq\ell$}.$ (30)

At the same time, by axiom A9 and propositional reasoning, statements (25) and
(26) imply that

$s\vdash\neg\text{WA}_{a}(\tau_{i}\wedge\sigma_{i})\text{ for each $i\leq
m$}.$ (31)

On the other hand, by Lemma 2 and propositional reasoning, statement (29)
implies that

$\vdash\varphi\to\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i}).$

By rule IR2, the above statement implies that

$\vdash\text{WA}_{a}\varphi\to\text{WA}_{a}\Big{(}\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i})\Big{)}.$

Thus, by the assumption $\text{WA}_{a}\varphi\in s$ of the lemma and the Modus
Ponens rule,

$s\vdash\text{WA}_{a}\Big{(}\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i})\Big{)}.$ (32)

Note that in the special case when $k=\ell=m=0$, statement (32) has the form
$s\vdash\text{WA}_{a}\bot$. This implies inconsistency of set $s$ due to axiom
A1. Thus, without loss of generality, we can assume that at least one of the
integers $k$, $\ell$, and $m$ is positive. Hence, by multiple applications of
axiom A5 and the laws of propositional reasoning, statement (32) implies that

$s\vdash\bigvee_{i\leq
k}\text{WA}_{a}\psi_{i}\vee\bigvee_{i\leq\ell}\text{WA}_{a}\chi_{i}\vee\bigvee_{i\leq
m}\text{WA}_{a}(\tau_{i}\wedge\sigma_{i}).$

This statement contradicts statements (23), (30), and (31) because set $s$ is
consistent. $\boxtimes$

Let $t$ be any maximal consistent extension of set $X$. Such $t$ exists by
Lemma 3. Then, $t\in S$ by Definition 5.

######  Claim 4.

For each agent $c\in C$, at least one of the following statements is true:

  1. 1.

$\neg\tau\in t$ for each formula $\neg\text{WA}_{c}\tau\in s$, or

  2. 2.

$\neg\sigma\in t$ for each formula $\text{SA}_{c}\sigma\in s$.

  * Proof of Claim. Suppose the opposite. Then, there are formulae $\neg\text{WA}_{c}\tau\in s$ and $\text{SA}_{c}\sigma\in s$ such that $\neg\tau\notin t$ and $\neg\sigma\notin t$. Thus, $\tau\in t$ and $\sigma\in t$ because $t$ is a maximal consistent set. Hence, $t\vdash\tau\wedge\sigma$ by propositional reasoning. Then, $\neg(\tau\wedge\sigma)\notin t$ because set $t$ is consistent. Therefore, $\neg(\tau\wedge\sigma)\notin X$ because $X\subseteq t$, which contradicts line 3 of statement (22). $\boxtimes$

Note that the sets $\\{a\\}$, $B$, and $C$ form a partition of the set
$\mathcal{A}$ of all agents due to statements (20) and (21). Consider any
action profile $\delta$ that satisfies the following conditions:

  1. 1.

$\delta_{x}=\top^{+}$ for each $x\in\\{a\\}\cup B$;

  2. 2.

$\delta_{c}\in\\{\top^{+},\top^{-}\\}$ for each $c\in C$ such that

    1. (a)

if $\delta_{c}=\top^{+}$, then $\neg\tau\in t$ for each
$\neg\text{WA}_{c}\tau\in s$;

    2. (b)

if $\delta_{c}=\top^{-}$, then $\neg\sigma\in t$ for each
$\text{SA}_{c}\sigma\in s$.

The existence of at least one such action profile $\delta$ follows from
Definition 6 and Claim 4.

######  Claim 5.

$(\delta,t)\in M_{s}$.

  * Proof of Claim. It suffices to verify that conditions 1-4 of Definition 7 are satisfied for the tuple $(\delta,t)$ for each agent $x\in\mathcal{A}$. Recall that the sets $\\{a\\},B,C$ form a partition of the set $\mathcal{A}$ due to statements (20) and (21). Thus, it suffices to consider the following three cases:

Case 1: $x\in\\{a\\}\cup B$. Then, $\delta_{x}=\top^{+}$ by the choice of
profile $\delta$. Condition 1 of Definition 7 follows from lines 1 and 2 of
statement (22) and $X\subseteq t$. Conditions 2 and 3 are satisfied because
$\top\in t$. Condition 4 is satisfied because $\delta_{x}=\top^{+}\in
D^{s}_{x}$.

Case 2: $x\in C$ and $\delta_{x}=\top^{+}$. Condition 1 follows from item 2(a)
of the choice of profile $\delta$. Conditions 2, 3, and 4 are similar to the
previous case.

Case 3: $x\in C$ and $\delta_{x}=\top^{-}$. Condition 1 is satisfied because
$\delta_{x}=\top^{-}\notin D^{s}_{x}$. Conditions 2 and 3 are satisfied
because $\top\in t$. Condition 4 follows from item 2(b) of the choice of
profile $\delta$. $\boxtimes$

To finish the proof of the lemma, note that $\delta_{a}=\top^{+}\in D^{s}_{a}$
by the choice of profile $\delta$ and Definition 6. Also, observe that
$\varphi\in X\subseteq t$ by line 1 of statement (22) and the formation of set
$t$. ∎

######  Lemma 22.

For any state $s\in S$, any formula $\neg\text{WE}_{a}\varphi\in s$, and any
action $i\in D_{a}^{s}$, there is a tuple $(\delta,t)\in M_{s}$ such that
$\delta_{a}=i$ and $\neg\varphi\in t$.

###### Proof.

By the assumption $i\in D_{a}^{s}$ of the lemma and Definition 6,

$i=\varepsilon^{+}$ (33)

for some $\varepsilon\in\Phi$. Let

$\widehat{\varepsilon}=\begin{cases}\varepsilon,&\text{if
}\text{WE}_{a}\varepsilon\in s;\\\ \top,&\text{otherwise.}\end{cases}$ (34)

Note that, by axiom A2, statement (34) implies that

$\text{WE}_{a}\widehat{\varepsilon}\in s.$ (35)

Consider the sets of agents

$\displaystyle B=$ $\displaystyle\\{b\in\mathcal{A}\;|\;b\neq
a,\text{SA}_{b}\top\in s\\},$ (36) $\displaystyle C=$
$\displaystyle\\{c\in\mathcal{A}\;|\;c\neq a,\neg\text{SA}_{c}\top\in s\\},$
(37)

and the set of formulae

$\displaystyle X=$
$\displaystyle\\{\neg\varphi,\widehat{\varepsilon}\;\\}\cup\\{\neg\psi\;|\;\neg\text{WA}_{a}\psi\in
s\\}$ (38) $\displaystyle\cup\\{\neg\chi\;|\;\exists\,b\in
B(\neg\text{WA}_{b}\chi\in s)\\}$
$\displaystyle\cup\\{\neg(\tau\wedge\sigma)\;|\;\exists\,c\in
C(\neg\text{WA}_{c}\tau\in s,\text{SA}_{c}\sigma\in s)\\}.$

######  Claim 6.

Set $X$ is consistent.

  * Proof of Claim. Suppose the opposite, then there are formulae

$\displaystyle\neg$
$\displaystyle\text{WA}_{a}\psi_{1},\dots,\neg\text{WA}_{a}\psi_{k}\in s,$
(39) $\displaystyle\neg$
$\displaystyle\text{WA}_{b_{1}}\chi_{1},\dots,\neg\text{WA}_{b_{\ell}}\chi_{\ell}\in
s,$ (40) $\displaystyle\neg$
$\displaystyle\text{WA}_{c_{1}}\tau_{1},\dots,\neg\text{WA}_{c_{m}}\tau_{m}\in
s,$ (41)
$\displaystyle\text{SA}_{c_{1}}\sigma_{1},\dots,\text{SA}_{c_{m}}\sigma_{m}\in
s,$ (42)

where

$\displaystyle b_{1},\dots,b_{\ell}\in B,$ (43) $\displaystyle
c_{1},\dots,c_{m}\in C,$ (44)

such that

$\neg\varphi\wedge\widehat{\varepsilon}\wedge\bigwedge_{i\leq
k}\neg\psi_{i}\wedge\bigwedge_{i\leq\ell}\neg\chi_{i}\wedge\bigwedge_{i\leq
m}\neg(\tau_{i}\wedge\sigma_{i})\vdash\bot.$ (45)

Note that, by axiom A7, statement (35) and the assumption
$\neg\text{WE}_{a}\varphi\in s$ of the lemma imply that

$s\vdash\text{WA}_{a}(\,\widehat{\varepsilon}\,\wedge\neg\varphi).$ (46)

By Lemma 20 and propositional reasoning, statements (40), (43), and (36) imply
that

$s\vdash\neg\text{WA}_{a}\chi_{i}\text{ for each }i\leq\ell.$ (47)

At the same time, by axiom A9 and propositional reasoning, statements (41) and
(42) imply that

$s\vdash\neg\text{WA}_{a}(\tau_{i}\wedge\sigma_{i})\text{ for each }i\leq m.$
(48)

By applying the contrapositive of axiom A5 multiple times, statements (39),
(47) and (48) imply that

$s\vdash\neg\text{WA}_{a}\Big{(}\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i})\Big{)}.$ (49)

In the special case where $k=\ell=m=0$, statement (49) follows directly from
axiom A1.

On the other hand, by Lemma 2 and propositional reasoning, statement (45)
implies that

$\vdash(\,\widehat{\varepsilon}\,\wedge\neg\varphi)\to\Big{(}\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i})\Big{)}.$

By rule IR2, the above statement implies that

$\vdash\text{WA}_{a}(\,\widehat{\varepsilon}\,\wedge\neg\varphi)\to\text{WA}_{a}\Big{(}\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i})\Big{)}.$

Together with statement (46) and the Modus Ponens rule, the above statement
implies that

$s\vdash\text{WA}_{a}\Big{(}\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i})\Big{)},$

which contradicts statement (49) because $s$ is consistent. $\boxtimes$

Let $t$ be any maximal consistent extension of set $X$. Such $t$ exists by
Lemma 3. Then, $t\in S$ by Definition 5.

######  Claim 7.

For each agent $c\in C$, at least one of the following statements is true:

  1. 1.

$\neg\tau\in t$ for each formula $\neg\text{WA}_{c}\tau\in s$, or

  2. 2.

$\neg\sigma\in t$ for each formula $\text{SA}_{c}\sigma\in s$.

  * Proof of Claim. Suppose the opposite. Then, there are formulae $\neg\text{WA}_{c}\tau\in s$ and $\text{SA}_{c}\sigma\in s$ such that $\neg\tau\notin t$ and $\neg\sigma\notin t$. Thus, $\tau\in t$ and $\sigma\in t$ because $t$ is a maximal consistent set. Hence, $t\vdash\tau\wedge\sigma$ by propositional reasoning. Then, $\neg(\tau\wedge\sigma)\notin t$ because set $t$ is consistent. Therefore, $\neg(\tau\wedge\sigma)\notin X$ because $X\subseteq t$, which contradicts line 3 of statement (38). $\boxtimes$

Note that the sets $\\{a\\}$, $B$, and $C$ form a partition of the set
$\mathcal{A}$ of all agents due to statements (36) and (37). Consider any
action profile $\delta$ that satisfies the following conditions:

  1. 1.

$\delta_{a}=\varepsilon^{+}$;

  2. 2.

$\delta_{b}=\top^{+}$ for each $b\in B$;

  3. 3.

$\delta_{c}\in\\{\top^{+},\top^{-}\\}$ for each $c\in C$ such that

    1. (a)

if $\delta_{c}=\top^{+}$, then $\neg\tau\in t$ for each
$\neg\text{WA}_{c}\tau\in s$;

    2. (b)

if $\delta_{c}=\top^{-}$, then $\neg\sigma\in t$ for each
$\text{SA}_{c}\sigma\in s$.

The existence of at least one such action profile $\delta$ follows from
Definition 6 and Claim 7.

######  Claim 8.

$(\delta,t)\in M_{s}$.

  * Proof of Claim. It suffices to verify that conditions 1-4 of Definition 7 are satisfied for the tuple $(\delta,t)$ for each agent $x\in\mathcal{A}$. Recall that the sets $\\{a\\},B,C$ form a partition of the set $\mathcal{A}$ due to statements (36) and (37). Thus, by the choice of profile $\delta$, it suffices to consider the following four cases:

Case 1: $x=a$. Then, $\delta_{x}=\varepsilon^{+}$ by the choice of profile
$\delta$. Condition 1 of Definition 7 follows from line 1 of statement (38)
and $X\subseteq t$. Condition 2 is satisfied because of statement (34), line 1
of statement (38), and $X\subseteq t$. Conditions 3 and 4 are satisfied
because $\delta_{x}=\varepsilon^{+}\in D_{x}^{s}$.

Case 2: $x\in B$. Then, $\delta_{x}=\top^{+}$ by the choice of $\delta$.
Condition 1 of Definition 7 is satisfied by line 2 of statement (38) and
$X\subseteq t$. Conditions 2 and 3 are satisfied because $\top\in t$.
Condition 4 is satisfied because $\delta_{x}=\top^{+}\in D^{s}_{x}$.

Case 3: $x\in C$ and $\delta_{x}=\top^{+}$. Condition 1 follows from item 3(a)
of the choice of profile $\delta$. Conditions 2, 3, and 4 are similar to the
previous case.

Case 4: $x\in C$ and $\delta_{x}=\top^{-}$. Conditions 1 and 2 are satisfied
because $\delta_{x}=\top^{-}\notin D^{s}_{x}$. Condition 3 is satisfied
because $\top\in t$. Condition 4 follows from item 3(b) of the choice of
profile $\delta$. $\boxtimes$

To finish the proof of this lemma, note that $\delta_{a}=\varepsilon^{+}=i$ by
the choice of profile $\delta$ and statement (33). At the same time,
$\neg\varphi\in X\subseteq t$ by line 1 of statement (38) and the formation of
set $t$. ∎

######  Lemma 23.

For any state $s\in S$, any formula $\text{SE}_{a}\varphi\in s$, and any
action $i\in\Delta_{a}^{s}\setminus D_{a}^{s}$, there is a tuple
$(\delta,t)\in M_{s}$ such that $\delta_{a}=i$ and $\neg\varphi\in t$.

###### Proof.

By the assumption $i\in\Delta_{a}^{s}\setminus D_{a}^{s}$ of the lemma and
Definition 6,

$i=\varepsilon^{-}$ (50)

for some $\varepsilon\in\Phi$. Let

$\widehat{\varepsilon}=\begin{cases}\varepsilon,&\text{if
}\neg\text{SE}_{a}\varepsilon\in s;\\\ \top,&\text{otherwise.}\end{cases}$
(51)

Note that the assumptions $\delta_{a}=i\in\Delta_{a}^{s}\setminus D_{a}^{s}$
of the lemma imply that $\text{SA}_{a}\top\notin s$ by Definition 6. Since $s$
is a maximal consistent set, $\neg\text{SA}_{a}\top\in s$. Then,
$\neg\text{SE}_{a}\top\in s$ by the contrapositive of axiom A4. Thus, by
statement (51),

$\neg\text{SE}_{a}\widehat{\varepsilon}\in s.$ (52)

Consider the sets of agents

$\displaystyle B=$ $\displaystyle\\{b\in\mathcal{A}\;|\;b\neq
a,\text{SA}_{b}\top\in s\\},$ (53) $\displaystyle C=$
$\displaystyle\\{c\in\mathcal{A}\;|\;c\neq a,\neg\text{SA}_{c}\top\in s\\},$
(54)

and the set of formulae

$\displaystyle X=$
$\displaystyle\\{\neg\varphi,\widehat{\varepsilon}\;\\}\cup\\{\neg\psi\;|\;\text{SA}_{a}\psi\in
s\\}$ (55) $\displaystyle\cup\\{\neg\chi\;|\;\exists\,b\in
B(\neg\text{WA}_{b}\chi\in s)\\}$
$\displaystyle\cup\\{\neg(\tau\wedge\sigma)\;|\;\exists\,c\in
C(\neg\text{WA}_{c}\tau\in s,\text{SA}_{c}\sigma\in s)\\}.$

######  Claim 9.

Set $X$ is consistent.

  * Proof of Claim. Suppose the opposite, then there are formulae

$\displaystyle\text{SA}_{a}\psi_{1},\dots,\text{SA}_{a}\psi_{k}\in s,$ (56)
$\displaystyle\neg$
$\displaystyle\text{WA}_{b_{1}}\chi_{1},\dots,\neg\text{WA}_{b_{\ell}}\chi_{\ell}\in
s,$ (57) $\displaystyle\neg$
$\displaystyle\text{WA}_{c_{1}}\tau_{1},\dots,\neg\text{WA}_{c_{m}}\tau_{m}\in
s,$ (58)
$\displaystyle\text{SA}_{c_{1}}\sigma_{1},\dots,\text{SA}_{c_{m}}\sigma_{m}\in
s,$ (59)

where

$\displaystyle b_{1},\dots,b_{\ell}\in B,$ (60) $\displaystyle
c_{1},\dots,c_{m}\in C,$ (61)

such that

$\neg\varphi\wedge\widehat{\varepsilon}\wedge\bigwedge_{i\leq
k}\neg\psi_{i}\wedge\bigwedge_{i\leq\ell}\neg\chi_{i}\wedge\bigwedge_{i\leq
m}\neg(\tau_{i}\wedge\sigma_{i})\vdash\bot.$ (62)

Note that, by axiom A8, statement (52) and the assumption
$\text{SE}_{a}\varphi\in s$ of the lemma imply that

$s\vdash\neg\text{SA}_{a}(\,\widehat{\varepsilon}\,\wedge\neg\varphi).$ (63)

By Lemma 20 and propositional reasoning, statements (57), (60), and (53) imply
that

$s\vdash\text{SA}_{a}\chi_{i}\text{ for each }i\leq\ell.$ (64)

At the same time, by axiom A9 and propositional reasoning, statements (58) and
(59) imply that

$s\vdash\text{SA}_{a}(\tau_{i}\wedge\sigma_{i})\text{ for each }i\leq m.$ (65)

By applying axiom A6 multiple times, statements (56), (64) and (65) imply that

$s\vdash\text{SA}_{a}\Big{(}\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i})\Big{)}.$ (66)

In the special case where $k=\ell=m=0$, statement (66) follows directly from
axiom A3.

On the other hand, by Lemma 2 and propositional reasoning, statement (62)
implies that

$\vdash(\,\widehat{\varepsilon}\,\wedge\neg\varphi)\to\Big{(}\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i})\Big{)}.$

By rule IR3, the above statement implies

$\vdash\text{SA}_{a}\Big{(}\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i})\Big{)}\to\text{SA}_{a}(\,\widehat{\varepsilon}\,\wedge\neg\varphi).$

Together with statement (66) and the Modus Ponens rule, the above statement
implies that

$s\vdash\text{SA}_{a}(\,\widehat{\varepsilon}\,\wedge\neg\varphi),$

which contradicts statement (63) because $s$ is consistent. $\boxtimes$

Let $t$ be any maximal consistent extension of set $X$. Such $t$ exists by
Lemma 3. Then, $t\in S$ by Definition 5.

######  Claim 10.

For each agent $c\in C$, at least one of the following statements is true:

  1. 1.

$\neg\tau\in t$ for each formula $\neg\text{WA}_{c}\tau\in s$, or

  2. 2.

$\neg\sigma\in t$ for each formula $\text{SA}_{c}\sigma\in s$.

  * Proof of Claim. Suppose the opposite. Then, there are formulae $\neg\text{WA}_{c}\tau\in s$ and $\text{SA}_{c}\sigma\in s$ such that $\neg\tau\notin t$ and $\neg\sigma\notin t$. Thus, $\tau\in t$ and $\sigma\in t$ because $t$ is a maximal consistent set. Hence, $t\vdash\tau\wedge\sigma$ by propositional reasoning. Then, $\neg(\tau\wedge\sigma)\notin t$ because set $t$ is consistent. Therefore, $\neg(\tau\wedge\sigma)\notin X$ because $X\subseteq t$, which contradicts line 3 of statement (55). $\boxtimes$

Note that the sets $\\{a\\}$, $B$, and $C$ form a partition of the set
$\mathcal{A}$ of all agents due to statements (53) and (54). Consider any
action profile $\delta$ that satisfies the following conditions:

  1. 1.

$\delta_{a}=\varepsilon^{-}$;

  2. 2.

$\delta_{b}=\top^{+}$ for each $b\in B$;

  3. 3.

$\delta_{c}\in\\{\top^{+},\top^{-}\\}$ for each $c\in C$ such that

    1. (a)

if $\delta_{c}=\top^{+}$, then $\neg\tau\in t$ for each
$\neg\text{WA}_{c}\tau\in s$;

    2. (b)

if $\delta_{c}=\top^{-}$, then $\neg\sigma\in t$ for each
$\text{SA}_{c}\sigma\in s$.

The existence of at least one such action profile $\delta$ follows from
Definition 6 and Claim 10.

######  Claim 11.

$(\delta,t)\in M_{s}$.

  * Proof of Claim. It suffices to verify that conditions 1-4 of Definition 7 are satisfied for the tuple $(\delta,t)$ for each agent $x\in\mathcal{A}$. Recall that the sets $\\{a\\},B,C$ form a partition of the set $\mathcal{A}$ due to statements (53) and (54). Thus, by the choice of profile $\delta$, it suffices to consider the following four cases:

Case 1: $x=a$. Then, $\delta_{x}=\varepsilon^{-}$ by the choice of $\delta$.
Conditions 1 and 2 of Definition 7 follows from
$\delta_{x}=\varepsilon^{-}\notin D_{x}^{s}$. Condition 3 is satisfied because
of statement (51), line 1 of statement (55), and $X\subseteq t$. Condition 4
follows from line 1 of statement (55) and $X\subseteq t$.

Case 2: $x\in B$. Then, $\delta_{x}=\top^{+}$ by the choice of $\delta$.
Condition 1 of Definition 7 follows from line 2 of statement (55) and
$X\subseteq t$. Conditions 2 and 3 are satisfied because $\top\in t$.
Condition 4 is satisfied because
$\delta_{x}=\top^{+}\notin\Delta_{x}^{s}\setminus D^{s}_{x}$.

Case 3: $x\in C$ and $\delta_{x}=\top^{+}$. Condition 1 follows from item 3(a)
of the choice of profile $\delta$. Conditions 2, 3, and 4 are similar to the
previous case.

Case 4: $x\in C$ and $\delta_{x}=\top^{-}$. Conditions 1 and 2 are satisfied
because $\delta_{x}=\top^{-}\notin D^{s}_{x}$. Condition 3 is satisfied
because $\top\in t$. Condition 4 follows from item 3(b) of the choice of
profile $\delta$. $\boxtimes$

To finish the proof of this lemma, note that $\delta_{a}=\varepsilon^{-}=i$ by
the choice of profile $\delta$ and statement (50). Also, note that
$\neg\varphi\in X\subseteq t$ by line 1 of statement (55) and the formation of
set $t$. ∎

######  Lemma 24.

For any state $s\\!\in\\!S$ and any formula $\neg\text{SA}_{a}\varphi\in s$,
there is a tuple $(\delta,t)\in M_{s}$ such that
$\delta_{a}\in\Delta_{a}^{s}\setminus D_{a}^{s}$ and $\varphi\in t$.

###### Proof.

Consider the sets of agents

$\displaystyle B=$ $\displaystyle\\{b\in\mathcal{A}\;|\;b\neq
a,\text{SA}_{b}\top\in s\\},$ (67) $\displaystyle C=$
$\displaystyle\\{c\in\mathcal{A}\;|\;c\neq a,\neg\text{SA}_{c}\top\in s\\},$
(68)

and the set of formulae

$\displaystyle X=$
$\displaystyle\\{\varphi\\}\cup\\{\neg\psi\;|\;\text{SA}_{a}\psi\in s\\}$ (69)
$\displaystyle\cup\\{\neg\chi\;|\;\exists\,b\in B(\neg\text{WA}_{b}\chi\in
s)\\}$ $\displaystyle\cup\\{\neg(\tau\wedge\sigma)\;|\;\exists\,c\in
C(\neg\text{WA}_{c}\tau\in s,\text{SA}_{c}\sigma\in s)\\}.$

######  Claim 12.

Set $X$ is consistent.

  * Proof of Claim. Suppose the opposite, then there are formulae

$\displaystyle\text{SA}_{a}\psi_{1},\dots,\text{SA}_{a}\psi_{k}\in s,$ (70)
$\displaystyle\neg$
$\displaystyle\text{WA}_{b_{1}}\chi_{1},\dots,\neg\text{WA}_{b_{\ell}}\chi_{\ell}\in
s,$ (71) $\displaystyle\neg$
$\displaystyle\text{WA}_{c_{1}}\tau_{1},\dots,\neg\text{WA}_{c_{m}}\tau_{m}\in
s,$ (72)
$\displaystyle\text{SA}_{c_{1}}\sigma_{1},\dots,\text{SA}_{c_{m}}\sigma_{m}\in
s,$ (73)

where

$\displaystyle b_{1},\dots,b_{\ell}\in B,$ (74) $\displaystyle
c_{1},\dots,c_{m}\in C,$ (75)

such that

$\varphi\wedge\bigwedge_{i\leq
k}\neg\psi_{i}\wedge\bigwedge_{i\leq\ell}\neg\chi_{i}\wedge\bigwedge_{i\leq
m}\neg(\tau_{i}\wedge\sigma_{i})\vdash\bot.$ (76)

By Lemma 20 and propositional reasoning, statements (71), (74), and (67) imply
that,

$s\vdash\text{SA}_{a}\chi_{i}\text{ for each $i\leq\ell$}.$ (77)

At the same time, by axiom A9 and propositional reasoning, statements (72) and
(73) imply that,

$s\vdash\text{SA}_{a}(\tau_{i}\wedge\sigma_{i})\text{ for each $i\leq m$}.$
(78)

By applying axiom A6 multiple times, statements (70), (77) and (78) imply that

$s\vdash\text{SA}_{a}\Big{(}\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i})\Big{)}.$ (79)

In the special case where $k=\ell=m=0$, statement (79) follows directly from
axiom A3.

On the other hand, by Lemma 2 and propositional reasoning, statement (76)
implies that

$\vdash\varphi\to\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i}).$

By rule IR3, this implies that

$\vdash\text{SA}_{a}\Big{(}\bigvee_{i\leq
k}\psi_{i}\vee\bigvee_{i\leq\ell}\chi_{i}\vee\bigvee_{i\leq
m}(\tau_{i}\wedge\sigma_{i})\Big{)}\to\text{SA}_{a}\varphi.$

Together with statement (79) and the Modus Ponens rule, the above statement
implies that

$s\vdash\text{SA}_{a}\varphi,$

which contradicts the assumption $\neg\text{SA}_{a}\varphi\in s$ of the lemma
because set $s$ is consistent. $\boxtimes$

Let $t$ be any maximal consistent extension of set $X$. Such $t$ exists by
Lemma 3. Then, $t\in S$ by Definition 5.

######  Claim 13.

For each agent $c\in C$ at least one of the following statements is true:

  1. 1.

$\neg\tau\in t$ for each formula $\neg\text{WA}_{c}\tau\in s$, or

  2. 2.

$\neg\sigma\in t$ for each formula $\text{SA}_{c}\sigma\in s$.

  * Proof of Claim. Suppose the opposite. Then, there are formulae $\neg\text{WA}_{c}\tau\in s$ and $\text{SA}_{c}\sigma\in s$ such that $\neg\tau\notin t$ and $\neg\sigma\notin t$. Thus, $\tau\in t$ and $\sigma\in t$ because $t$ is a maximal consistent set. Hence, $t\vdash\tau\wedge\sigma$ by propositional reasoning. Then, $\neg(\tau\wedge\sigma)\notin t$ because set $t$ is consistent. Therefore, $\neg(\tau\wedge\sigma)\notin X$ because $X\subseteq t$, which contradicts line 3 of statement (69). $\boxtimes$

Note that the sets $\\{a\\}$, $B$, and $C$ form a partition of the set
$\mathcal{A}$ of all agents due to statements (67) and (68). Consider any
action profile $\delta$ that satisfies the following conditions:

  1. 1.

$\delta_{a}=\top^{-}$

  2. 2.

$\delta_{b}=\top^{+}$ for each $b\in B$;

  3. 3.

$\delta_{c}\in\\{\top^{+},\top^{-}\\}$ for each $c\in C$ such that

    1. (a)

if $\delta_{c}=\top^{+}$, then $\neg\tau\in t$ for each
$\neg\text{WA}_{c}\tau\in s$;

    2. (b)

if $\delta_{c}=\top^{-}$, then $\neg\sigma\in t$ for each
$\text{SA}_{c}\sigma\in s$.

The existence of at least one such action profile $\delta$ follows from
Definition 6 and Claim 13.

######  Claim 14.

$(\delta,t)\in M_{s}$.

  * Proof of Claim. It suffices to verify that conditions 1-4 of Definition 7 are satisfied for the tuple $(\delta,t)$ for each agent $x\in\mathcal{A}$. Recall that the sets $\\{a\\},B,C$ form a partition of the set $\mathcal{A}$ due to statements (67) and (68). Thus, by the choice of profile $\delta$, it suffices to consider the following four cases:

Case 1: $x=a$. Then, $\delta_{x}=\top^{-}$ by the choice of profile $\delta$.
Conditions 1 and 2 of Definition 7 are satisfied because
$\delta_{x}=\top^{-}\notin D_{x}^{s}$. Condition 3 is satisfied because
$\top\in t$. Condition 4 follows from line 1 of statement (69) and $X\subseteq
t$.

Case 2: $x\in B$. Then, $\delta_{x}=\top^{+}$ by the choice of $\delta$.
Condition 1 of Definition 7 follows from line 2 of statement (69) and
$X\subseteq t$. Conditions 2 and 3 are satisfied because $\top\in t$.
Condition 4 is satisfied because
$\delta_{x}=\top^{+}\notin\Delta_{x}^{s}\setminus D^{s}_{x}$.

Case 3: $x\in C$ and $\delta_{x}=\top^{+}$. Condition 1 follows from item 3(a)
of the choice of profile $\delta$. Conditions 2, 3, and 4 are similar to the
previous case.

Case 4: $x\in C$ and $\delta_{x}=\top^{-}$. Conditions 1, 2 and 3 are similar
to case 1. Condition 4 follows from item 3(b) of the choice of profile
$\delta$. $\boxtimes$

As the ending of the proof of the lemma, first, note that
$\delta_{a}=\top^{-}\in\Delta_{a}^{s}\setminus D^{s}_{a}$ by the choice of
profile $\delta$ and Definition 6. Second, note that $\varphi\in X\subseteq t$
by line 1 of statement (69) and the formation of set $t$. ∎

###  D.2 Proof of Lemma 7

Lemma 7 $s\Vdash\varphi$ if and only if $\varphi\in s$ for each state $s$ of
the canonical model and each formula $\varphi\in\Phi$.

###### Proof.

We prove the lemma by induction on the structural complexity of formula
$\varphi$. If $\varphi$ is a propositional variable, then the statement of the
lemma follows from item 1 of Definition 2 and Definition 8. If formula
$\varphi$ is a negation or a disjunction, then the statement of the lemma
follows from the induction hypothesis, items 2 and 3 of Definition 2 and the
maximality and consistency of set $s$ in the standard way.

Suppose that formula $\varphi$ has the form $\text{WA}_{a}\psi$.

$\Rightarrow:$ Assume that $s\Vdash\text{WA}_{a}\psi$. Then, by item 4 of
Definition 2, there exists an action $i\in D^{s}_{a}$ such that
$(s,i)\not\rightsquigarrow_{a}\neg\psi$. Hence, by Definition 2, there is a
tuple $(\delta,t)\in M_{s}$ such that $\delta_{a}=i$ and $t\nVdash\neg\psi$.
Then, $t\Vdash\psi$ by item 2 of Definition 2. Thus, $\psi\in t$ by the
induction hypothesis. Hence, $\neg\varphi\notin t$ because set $t$ is
consistent. Note that $\neg\varphi\notin t$ and $\delta_{a}=i\in D^{s}_{a}$.
Therefore, $\text{WA}_{a}\psi\in s$ by Condition 1 of Definition 7.

$\Leftarrow:$ Assume that $\text{WA}_{a}\psi\in s$. Then, by Lemma 21, there
is a tuple $(\delta,t)\in M_{s}$ such that $\delta_{a}\in D^{s}_{a}$ and
$\psi\in t$. Hence, $t\Vdash\psi$ by the induction hypothesis. Thus,
$t\nVdash\neg\psi$ by item 2 of Definition 2. Then,
$(s,\delta_{a})\not\rightsquigarrow_{a}\neg\psi$ by Definition 2. Therefore,
$s\Vdash\text{WA}_{a}\psi$ by item 4 of Definition 2.

Suppose that formula $\varphi$ has the form $\text{WE}_{a}\psi$.

$\Rightarrow:$ Assume that $\text{WE}_{a}\psi\notin s$. Then,
$\neg\text{WE}_{a}\psi\in s$ because $s$ is a maximal consistent set. Hence,
by Lemma 22, for each action $i\in D_{a}^{s}$, there is a tuple $(\delta,t)\in
M_{s}$ such that $\delta_{a}=i$ and $\neg\psi\in t$. Then, $\psi\notin t$
because $t$ is a maximal consistent set. Thus, $t\nVdash\psi$ by the induction
hypothesis. Hence, $(s,i)\not\rightsquigarrow_{a}\psi$ for each action $i\in
D_{a}^{s}$ by Definition 2. Therefore, $s\nVdash\text{WE}_{a}\psi$ by item 5
of Definition 2.

$\Leftarrow:$ Assume that $s\nVdash\text{WE}_{a}\psi$. Then,
$(s,\psi^{+})\not\rightsquigarrow_{a}\psi$ by item 5 of Definition 2. Thus,
there is a tuple $(\delta,t)\in M_{s}$ such that $\delta_{a}=\psi^{+}$ and
$t\nVdash\psi$ by Definition 2. Then, $\psi\notin t$ by the induction
hypothesis. Note that $\delta_{a}\\!=\\!\psi^{+}$ and $\psi\notin t$.
Therefore, $\text{WE}_{a}\psi\notin s$ by Condition 2 of Definition 7.

Suppose that formula $\varphi$ has the form $\text{SE}_{a}\psi$.

$\Rightarrow:$ Assume that $s\Vdash\text{SE}_{a}\psi$. Then,
$(s,\psi^{-})\not\rightsquigarrow_{a}\psi$ by item 6 of Definition 2 because
$\psi^{-}\notin D_{a}^{s}$. Thus, there is a tuple $(\delta,t)\in M_{s}$ such
that $\delta_{a}=\psi^{-}$ and $t\nVdash\psi$ by Definition 2. Then,
$\psi\notin t$ by the induction hypothesis. Thus, $\delta_{a}=\varphi^{-}$ and
$\psi\notin t$. Therefore, $\text{SE}_{a}\psi\in s$ by Condition 3 of
Definition 7.

$\Leftarrow:$ Assume that $\text{SE}_{a}\psi\in s$. Then, by Lemma 23, for
each action $i\in\Delta_{a}^{s}\setminus D_{a}^{s}$, there is a tuple
$(\delta,t)\in M_{s}$ such that $\delta_{a}=i$ and $\neg\psi\in t$. Thus,
$\psi\notin t$ because $t$ is a maximal consistent set. Then, $t\nVdash\psi$
by the induction hypothesis. Hence, $(s,i)\not\rightsquigarrow_{a}\psi$ for
each action $i\in\Delta_{a}^{s}\setminus D_{a}^{s}$ by Definition 2. Then, by
contraposition, $i\in D_{a}^{s}$ for each action $i$ such that
$(s,i)\rightsquigarrow_{a}\psi$. Therefore, $s\Vdash\text{SE}_{a}\psi$ by item
6 of Definition 2.

Suppose that formula $\varphi$ has the form $\text{SA}_{a}\psi$.

$\Rightarrow:$ Assume that $\text{SA}_{a}\psi\notin s$. Then,
$\neg\text{SA}_{a}\psi\in s$ because $s$ is a maximal consistent set. Thus, by
Lemma 24, there is a tuple $(\delta,t)\in M_{s}$ such that
$\delta_{a}\in\Delta_{a}^{s}\setminus D_{a}^{s}$ and $\psi\in t$. Then, by the
induction hypothesis, $t\Vdash\psi$. Thus, $t\nVdash\neg\psi$ by item 2 of
Definition 2. Hence, $(s,\delta_{a})\not\rightsquigarrow_{a}\neg\psi$ by
Definition 2. Therefore, $s\nVdash\text{SA}_{a}\psi$ by item 7 of Definition 2
and because $\delta_{a}\in\Delta_{a}^{s}\setminus D_{a}^{s}$.

$\Leftarrow:$ Assume that $s\nVdash\text{SA}_{a}\psi$. Then, by item 7 of
Definition 2, there is an action $i\in\Delta_{a}^{s}\setminus D_{a}^{s}$ such
that $(s,i)\not\rightsquigarrow_{a}\neg\psi$. Thus, there is a tuple
$(\delta,t)\in M_{s}$ such that $\delta_{a}=i$ and $t\nVdash\neg\psi$ by
Definition 2. Then, $t\Vdash\psi$ by item 2 of Definition 2. Hence, $\psi\in
t$ by the induction hypothesis. Then, $\neg\psi\notin t$ because $t$ is a
maximal consistent set. Note that $\delta_{a}=i\in\Delta_{a}^{s}\setminus
D_{a}^{s}$ and $\neg\psi\notin t$. Hence, $\text{SA}_{a}\psi\notin s$ by
Condition 4 of Definition 7. ∎

###  D.3 Proof of Theorem 4

Theorem 4 For each set of formulae $X\subseteq\Phi$ and each formula
$\varphi\in\Phi$ such that $X\nvdash\varphi$, there is a state $s$ of a
transition system such that $s\Vdash\chi$ for each $\chi\in X$ and
$s\nVdash\varphi$.

###### Proof.

Suppose that $X\nvdash\varphi$. Then, the set $X\cup\\{\neg\varphi\\}$ is
consistent. According to Lemma 3, there is a maximal consistent extension $s$
of the set $X\cup\\{\neg\varphi\\}$. Then, $s\in S$ by Definition 5. Note that
$\chi\in s$ for each $\chi\in X$ because $X\subseteq s$. Also, $\varphi\notin
s$ due to the consistency of set $s$. Hence, $s\Vdash\chi$ for each $\chi\in
X$ and $s\nVdash\varphi$ by Lemma 7. ∎