# A Logic-Based Analysis of Responsibility

Aldo Iván Ramírez Abarca Utrecht University
Utrecht, The Netherlands<EMAIL_ADDRESS>
###### Abstract

This paper presents a logic-based framework to analyze responsibility, which I
refer to as intentional epistemic act-utilitarian stit theory (IEAUST). To be
precise, IEAUST is used to model and syntactically characterize various modes
of responsibility, where by ‘modes of responsibility’ I mean instances of
Broersen’s three categories of responsibility (causal, informational, and
motivational responsibility), cast against the background of particular
deontic contexts. IEAUST is obtained by integrating a modal language to
express the following components of responsibility on stit models: agency,
epistemic notions, intentionality, and different senses of obligation. With
such a language, I characterize the components of responsibility using
particular formulas. Then, adopting a compositional approach—where complex
modalities are built out of more basic ones—these characterizations of the
components are used to formalize the aforementioned modes of responsibility.

##  1 Introduction

The study of responsibility is a complicated matter. The term is used in
different ways in different fields, and it is easy to engage in everyday
discussions as to why someone should be considered responsible for something.
Typically, the backdrop of these discussions involves social, legal, moral, or
philosophical problems, each with slightly different meanings for expressions
like _being responsible for…_ , _being held responsible for…_ , or _having the
responsibility of…_ , among others. Therefore—to approach such problems
efficiently—there is a demand for clear, taxonomical definitions of
responsibility.

For instance, suppose that you are a judge in Texas. You are presiding over a
trial where the defendant is being charged with first-degree murder. The
alleged crime is horrible, and the prosecution seeks capital punishment. The
case is as follows: driving her car, the defendant ran over a traffic officer
that was holding a stop-sign at a crossing walk, while school children were
crossing the street. The traffic officer was killed, and some of the children
were severely injured. A highly complicated case, the possibility of a death-
penalty sentence means that the life of the defendant is at stake. More than
ever, due process is imperative. As the presiding judge, you must abide by the
prevailing definitions of criminal liability with precision. In other words,
there is little to no room for ambiguity in the ruling, and your handling of
the notions associated with responsibility in criminal law should be
impeccable.

As this example suggests, a framework with intelligible, realistically
applicable definitions of responsibility is paramount in the field of law.
However, responsibility-related problems arise across many other
disciplines—social psychology, philosophy of emotion, legal theory, and
ethics, to name a few [18, 25]. A clear pattern in all these is the intent of
issuing standards for when—and to what extent—an agent should be held
responsible for a state of affairs.

This is where Logic lends a hand. The development of expressive logics—to
reason about agents’ decisions in situations with moral consequences—involves
devising unequivocal representations of components of behavior that are highly
relevant to systematic responsibility attribution and to systematic blame-or-
praise assignment. To put it plainly, expressive syntactic-and-semantic
frameworks help us analyze responsibility-related problems in a methodical
way.111Most likely, this is why the logic-based formalization of
responsibility has become such an important topic in, for instance, normative
multi-agent systems, responsible autonomous agents, and machine ethics for AI
[22, 7]

The main goal of this paper is to present a proposal for a formal theory of
responsibility. Such a proposal relies on (a) a _decomposition_ of
responsibility into specific components and (b) a functional _classification_
of responsibility, where the different categories directly correlate with the
components of the decomposition. As for the decomposition, it is given by the
following list:

  * –

Agency: the process by which agents bring about states of affairs in the
environment. In other words, the phenomenon by which agents choose and perform
actions, with accompanying mental states, that change the environment.

  * –

Knowledge and belief: mental states that concern the information available in
the environment and that explain agents’ particular choices of action.

  * –

Intentions: mental states that determine whether an action was done with the
purpose of bringing about its effects.

  * –

Ought-to-do’s: the actions that agents should perform, complying to the codes
of a normative system. Oughts-to-do’s make up contexts that provide a
criterion for deciding whether an agent should be blamed or praised. I refer
to these contexts as the _deontic contexts_ of responsibility.

As for the classification, it is a refinement of Broersen’s three categories
of responsibility: _causal, informational_ , and _motivational_ responsibility
[5, 10, 15]. I will discuss these categories at length in Section 2. On the
basis of both the decomposition and the classification, here I introduce a
very rich stit logic to analyze responsibility, which I refer to as
_intentional epistemic act-utilitarian stit theory_ (_IEAUST_). More
precisely, I use _IEAUST_ to model and syntactically characterize various
modes of responsibility. By ‘modes of responsibility’ I mean combinations of
sub-categories of the three ones mentioned above, cast against the background
of particular deontic contexts. On the one hand, the sub-categories correspond
to the different versions of responsibility that one can consider according to
the _active_ and _passive_ forms of the notion: while the active form involves
contributions—in terms of explicitly bringing about outcomes—the passive form
involves omissions—which are interpreted as the processes by which agents
allow that an outcome happens while being able, to some extent, to prevent it.
On the other hand, the deontic context of a mode establishes whether and to
what degree the combination of sub-categories involves either blameworthiness
or praiseworthiness.

The logic _IEAUST_ includes a language that expresses agency, epistemic
notions, intentionality, and different senses of obligation. With this
language, I characterize the components of responsibility using particular
formulas. Then, adopting a compositional approach—where complex modalities are
built out of more basic ones—I use these characterizations of the components
to formalize the aforementioned modes of responsibility. An outline of the
paper is included below.

  * •

Section 2 presents an operational definition for responsibility and addresses
the philosophical perspective adopted in my study of the notion.

  * •

Section 3 introduces _IEAUST_ and uses this logic to provide stit-theoretic
characterizations of different modes of responsibility.

  * •

Section 4 presents Hilbert-style proof systems both for _IEAUST_ and for a
technical extension, addressing the status of their soundness & completeness
results.

##  2 Categories of Responsibility

To make a start on formally analyzing responsibility, I identify (a) two
_viewpoints_ for the philosophical study of responsibility, (b) three main
_categories_ for the viewpoint that I focus on, and (c) two _forms_ in which
the elements of the categories can be interpreted.

As for point (a), the philosophical literature on responsibility usually
distinguishes two _viewpoints_ on the notion [23]: _backward-looking
responsibility_ and _forward-looking responsibility_. By backward-looking
responsibility one refers to the viewpoint according to which an agent is
considered to have produced a state of affairs that has already ensued and
lies in the past. This is the viewpoint taken by a judge when, while trying a
murder case, she wants to get to the bottom of things and find out who is
responsible for doing the killing. In contrast, by forward-looking
responsibility one refers to the viewpoint according to which which an agent
is expected to comply with the duty of bringing about a state of affairs in
the future. When one thinks of a student that has to write an essay before its
due date, for instance, this is the view that is being used. In other words,
the writing and the handing in of the essay before the deadline are seen as
responsibilities of the student.

From here on, I will focus on backward-looking responsibility. I work with the
following operational definition: _responsibility_ is a relation between the
agents and the states of affairs of an environment, such that an agent is
responsible for a state of affairs iff the agent’s degree of involvement in
the realization of that state of affairs warrants blame or praise (in light of
a given normative system). As for point (b), I follow [11] and [15] and
distinguish three main _categories_ of responsibility, where each category can
be correlated with the components of responsibility that it involves:222These
categories extend the literature’s common distinction between _causal_ and
_agentive_ responsibility [18, 24, 14], and they were derived by [11] on the
basis of his analysis of the modes of _mens rea_.

  1. 1.

_Causal responsibility_ : an agent is causally responsible for a state of
affairs iff the agent is the material author of such a state of affairs. The
component that this category involves is agency.

  2. 2.

_Informational responsibility_ : an agent is informationally responsible for a
state of affairs iff the agent is the material author and it behaved
knowingly, or consciously, while bringing about the state of affairs. The
components that this category involves are agency, knowledge, and belief.

  3. 3.

_Motivational responsibility_ : an agent is motivationally responsible for a
state of affairs iff the agent is the material author and it behaved knowingly
and intentionally while bringing about the state of affairs. The components
that this category involves are agency, knowledge, and intentions.

Finally, as for point (c), the two _forms_ of responsibility are the _active_
form and the _passive_ form. The active form of responsibility concerns
contributions, and the passive form of responsibility concerns omissions.

Now, key elements in my operational definition of responsibility are the
notions of blame and praise. Intuitively, responsibility can be measured by
how much blame or how much praise an agent gets for its participation in
bringing about a state of affairs. As mentioned before, _ought-to-do’s_ can
provide a criterion for deciding when agents should be blamed and when agents
should be praised. The main idea is as follows: if agent $\alpha$ ought to
have done $\phi$, then having seen to it that $\phi$ makes $\alpha$
praiseworthy, while having refrained from seeing to it that $\phi$ makes
$\alpha$ blameworthy. For a given $\phi$, then, the degrees of $\alpha$’s
praiseworthiness/blameworthiness correspond to the possible combinations
between (a) an agent’s ought-to-do’s and (b) the active/passive forms of the
three categories of responsibility.

##  3 A Logic of Responsibility

We are ready to introduce _intentional epistemic act-utilitarian stit theory_
(_IEAUST_), a stit-theoretic logic of responsibility. Without further ado, let
me address the syntax and semantics of this expressive framework.

###  3.1 Syntax & Semantics

######  Definition 3.1 (Syntax of intentional epistemic act-utilitarian stit
theory).

Given a finite set $Ags$ of agent names and a countable set of propositions
$P$, the grammar for the formal language $\mathcal{L}_{\textsf{R}}$ is given
by

$\begin{array}[]{ll}\phi::=p\mid\neg\phi\mid\phi\wedge\phi\mid\Box\phi\mid[\alpha]\phi\mid
K_{\alpha}\phi\mid
I_{\alpha}\phi\mid\odot_{\alpha}\phi\mid\odot^{\mathcal{S}}_{\alpha}\phi,\end{array}$

where $p$ ranges over $P$ and $\alpha$ ranges over $Ags$.

In this language, $\square\varphi$ is meant to express the historical
necessity of $\varphi$ ($\Diamond\varphi$ abbreviates
$\neg\square\neg\varphi$); $[\alpha]\varphi$ expresses that ‘agent $\alpha$
has seen to it that $\varphi$’; $K_{\alpha}\phi$ expresses that ‘$\alpha$ knew
$\varphi$’; $I_{\alpha}\phi$ expresses that ‘$\alpha$ had a present-directed
intention toward the realization of $\varphi$’; $\odot_{\alpha}\phi$ expresses
that ‘$\alpha$ objectively ought to have seen to it that $\phi$’; and
$\odot^{\mathcal{S}}_{\alpha}\phi$ expresses that ‘$\alpha$ subjectively ought
to have seen to it that $\phi$.’ As for the semantics, the structures on which
the formulas of $\mathcal{L}_{\mathtt{R}}$ are evaluated are based on what I
call _knowledge-intentions-oughts branching-time frames_. Let me first present
the formal definition of these frames and then review the intuitions behind
the extensions.

######  Definition 3.2 (_Kiobt_ -frames & models).

A tuple $\left\langle
M,\sqsubset,Ags,\mathbf{\mathbf{Choice}},\left\\{\sim_{\alpha}\right\\}_{\alpha\in
Ags},\tau,\mathbf{Value}\right\rangle$ is called a _knowledge-intention-oughts
branching-time frame_ (_kiobt_ -frame for short) iff

  * •

$M$ is a non-empty set of moments and $\sqsubset$ is a strict partial ordering
on $M$ satisfying ‘no backward branching.’ Each maximal $\sqsubset$-chain of
moments is called a history, where each history represents a complete temporal
evolution of the world. $H$ denotes the set of all histories, and for each
$m\in M$, $H_{m}:=\\{h\in H;m\in h\\}$. Tuples $\left\langle m,h\right\rangle$
such that $m\in M$, $h\in H$, and $m\in h$, are called _indices_ , and the set
of indices is denoted by $I(M\times H)$. $\mathbf{Choice}$ is a function that
maps each agent $\alpha$ and moment $m$ to a partition
$\mathbf{Choice}^{m}_{\alpha}$ of $H_{m}$, where the cells of such a partition
represent $\alpha$’s available actions at $m$. For $m\in M$ and $h\in H_{m}$,
we denote the equivalence class of $h$ in $\mathbf{Choice}^{m}_{\alpha}$ by
$\mathbf{Choice}^{m}_{\alpha}(h)$. $\mathbf{Choice}$ satisfies two
constraints:

    * $(\mathtt{NC})$

_No choice between undivided histories_ : For all $h,h^{\prime}\in H_{m}$, if
$m^{\prime}\in h\cap h^{\prime}$ for some $m^{\prime}\sqsupset m$, then $h\in
L$ iff $h^{\prime}\in L$ for every $L\in\mathbf{Choice}^{m}_{\alpha}$.

    * $(\mathtt{IA})$

_Independence of agency_ : A function $s$ on $Ags$ is called a _selection
function_ at $m$ if it assigns to each $\alpha$ a member of
$\mathbf{Choice}^{m}_{\alpha}$. If we denote by $\mathbf{Select}^{m}$ the set
of all selection functions at $m$, then we have that for every $m\in M$ and
$s\in\mathbf{Select}^{m}$, $\bigcap_{\alpha\in Ags}s(\alpha)\neq\emptyset$
(see [9] for a discussion of the property).

  * •

For $\alpha\in Ags$, $\sim_{\alpha}$ is the epistemic indistinguishability
equivalence relation for agent $\alpha$, which satisfies the following
constraints:

    * –

$(\mathtt{OAC})$ _Own action condition_ : if $\langle
m_{*},h_{*}\rangle\sim_{\alpha}\langle m,h\rangle$, then $\langle
m_{*},h_{*}^{\prime}\rangle\sim_{\alpha}\langle m,h\rangle$ for every
$h_{*}^{\prime}\in\mathbf{Choice}^{m_{*}}_{\alpha}(h_{*})$. We refer to this
constraint as the ‘own action condition’ because it implies that agents do not
know more than what they perform.

    * –

$(\mathtt{Unif-H})$ _Uniformity of historical possibility_ : if $\langle
m_{*},h_{*}\rangle\sim_{\alpha}\langle m,h\rangle$, then for every
$h_{*}^{\prime}\in H_{m_{*}}$ there exists $h^{\prime}\in H_{m}$ such that
$\langle m_{*},h_{*}^{\prime}\rangle\sim_{\alpha}\langle m,h^{\prime}\rangle$.
Combined with $(\mathtt{OAC})$, this constraint is meant to capture a notion
of uniformity of strategies, where epistemically indistinguishable indices
should have the same available actions for the agent to choose upon.

For $\langle m,h\rangle$ and $\alpha\in Ags$, the set
$\pi_{\alpha}^{\square}[\langle m,h\rangle]:=\\{\langle
m^{\prime},h^{\prime}\rangle;\exists h^{\prime\prime}\in
H_{m^{\prime}}s.t.\langle m,h\rangle\sim_{\alpha}\langle
m^{\prime},h^{\prime\prime}\rangle\\}$ is known as $\alpha$’s _ex ante
information set_.

  * •

$\tau$ is a function that assigns to each $\alpha\in Ags$ and index $\langle
m,h\rangle$ a topology $\tau_{\alpha}^{\langle m,h\rangle}$ on
$\pi_{\alpha}^{\square}\left[\langle m,h\rangle\right]$. This is the _topology
of $\alpha$’s intentionality at $\langle m,h\rangle$_, where any non-empty
open set is interpreted as a _present-directed intention_ , written ‘p-d
intention’ from here on, of $\alpha$ at $\langle m,h\rangle$. Additionally,
$\tau$ must satisfy the following conditions:

    * –

$(\mathtt{CI})$ _Finitary consistency of intention_ : for every $\alpha\in
Ags$ and index $\langle m,h\rangle$, every non-empty
$U,V\in\tau_{\alpha}^{\langle m,h\rangle}$ are such that $U\cap
V\neq\emptyset$. In other words, every non-empty $U\in\tau_{\alpha}^{\langle
m,h\rangle}$ is $\tau_{\alpha}^{\langle m,h\rangle}$-dense.

    * –

$(\mathtt{KI})$ _Knowledge of intention_ : for every $\alpha\in Ags$ and index
$\langle m,h\rangle$, $\tau_{\alpha}^{\langle
m,h\rangle}=\tau_{\alpha}^{\langle m^{\prime},h^{\prime}\rangle}$ for every
$\langle m^{\prime},h^{\prime}\rangle$ such that
$\pi_{\alpha}^{\square}\left[\langle
m,h\rangle\right]=\pi_{\alpha}^{\square}\left[\langle
m^{\prime},h^{\prime}\rangle\right]$. In other words, $\alpha$ has the same
topology of p-d intentions at all indices lying within $\alpha$’s current _ex
ante_ information set.

  * •

$\mathbf{Value}$ is a deontic function that assigns to each history $h\in H$ a
real number, representing the utility of $h$.

A _kiobt_ -model $\mathcal{M}$, then, results from adding a valuation function
$\mathcal{V}$ to a _kiobt_ -frame, where $\mathcal{V}:P\to 2^{I(M\times H)}$
assigns to each atomic proposition a set of indices.

For $\alpha\in Ags$, the equivalence relation $\sim_{\alpha}$ is the usual
indistinguishability relation, borrowed from epistemic logic, that represents
$\alpha$’s uncertainty: whatever holds at all epistemically accessible indices
is what an agent knows. As for the function $\tau$, it assigns to each agent
the topology of intentions, according to the ideas presented by [4]. The open
sets of any such topology are taken to be p-d intentions for bringing about
circumstances. At each moment, the fact that the non-empty open sets of the
topologies are dense implies that an agent’s intentions are consistent.

Regarding the deontic dimension, the idea is that objective, subjective, and
doxastic ought-to-do’s stem from the optimal actions for an agent: to have
seen to it that $\phi$ is taken to be an obligation of an agent at an index
iff $\phi$ is an effect of all the optimal actions for that agent and index,
where the notion of optimality is based on the deontic value of the histories
in those actions—provided by $\mathbf{Value}$. The semantics for formulas
involving the deontic operators require some previous definitions. For $m\in
M$ and $\beta\in Ags$, we define
$\mathbf{State}_{\beta}^{m}=\left\\{S\subseteq H_{m};S=\bigcap_{\alpha\in
Ags-\\{\beta\\}}s(\alpha),\mbox{ where }s\in\mathbf{Select}^{m}\right\\}$. For
$\alpha\in Ags$ and $m_{*}\in M$, we first define a general ordering $\leq$ on
$\mathcal{P}(H_{m_{*}})$ such that for $X,Y\subseteq H_{m_{*}}$, $X\leq
Y\textnormal{ iff }\mathbf{Value}(h)\leq\mathbf{Value}(h^{\prime})\textnormal{
for every }h\in X,h^{\prime}\in Y$. The _objective_ dominance ordering
$\preceq$ is defined such that for
$L,L^{\prime}\in\mathbf{Choice}_{\alpha}^{m_{*}}$, $L\preceq
L^{\prime}\textnormal{ iff }\mbox{for each
}S\in\mathbf{State}_{\alpha}^{m_{*}},L\cap S\leq L^{\prime}\cap S.$ The
optimal set of actions is taken as
$\mathbf{Optimal}^{m_{*}}_{\alpha}:=\\{L\in\mathbf{Choice}^{m_{*}}_{\alpha};\textnormal{there
is no }L^{\prime}\in\mathbf{Choice}^{m_{*}}_{\alpha}\textnormal{such that
}L\prec L^{\prime}\\}.$

_Subjective_ ought-to-do’s involve a different dominance ordering. To define
it, [12] and [2] introduce the so-called _epistemic clusters_ , which are
nothing more than a given action’s epistemic equivalents in indices that are
indistinguishable to the one of evaluation. Formally, we have that for
$\alpha\in Ags$, $m_{*},m\in M$, and $L\subseteq H_{m_{*}}$, $L$’s _epistemic
cluster_ at $m$ is the set $[L]^{m}_{\alpha}:=\\{h\in H_{m};\exists h_{*}\in
L\ \textnormal{ s.t. }\ \langle m_{*},h_{*}\rangle\sim_{\alpha}\langle
m,h\rangle\\}$. A subjective dominance ordering $\preceq_{s}$ on
$\mathbf{Choice}^{m_{*}}_{\alpha}$ is then defined by the following rule: for
$L,L^{\prime}\subseteq H_{m_{*}}$, $L\preceq_{s}L^{\prime}$ iff $\mbox{for
each }m$ such that $m_{*}\sim_{\alpha}m$, $\mbox{for each
}S\in\mathbf{State}_{\alpha}^{m},[L]^{m}_{\alpha}\cap
S\leq[L^{\prime}]^{m}_{\alpha}\cap S$.333As a convention, I write
$m\sim_{\alpha}m^{\prime}$ if there exist $h\in H_{m}$, $h^{\prime}\in
H_{m^{\prime}}$ such that $\langle m,h\rangle\sim_{\alpha}\langle
m^{\prime},h^{\prime}\rangle$. Just as in the case of objective ought-to-do’s,
this ordering allows us to define a subjectively optimal set of actions
$\mathbf{SOptimal}^{m_{*}}_{\alpha}:=\\{L\in\mathbf{Choice}^{m_{*}}_{\alpha};\textnormal{
there is no }L^{\prime}\in\mathbf{Choice}^{m_{*}}_{\alpha}\textnormal{ s. t.
}L\prec_{s}L^{\prime}\\},$ where I write $L\prec_{s}L^{\prime}$ iff
$L\preceq_{s}L^{\prime}$ and $L^{\prime}\npreceq_{s}L$.

Therefore, _kiobt_ -frames allow us to represent the components of
responsibility discussed in the introduction: agency, knowledge, intentions,
and ought-to-do’s. More precisely, they allow us to provide semantics for the
modalities of $\mathcal{L}_{\textsf{R}}$:

######  Definition 3.3 (Evaluation rules for _IEAUST_).

Let $\mathcal{M}$ be a finite-choice _kiobt_ -model.444Finite-choice _bt_
-models are those for which function $\mathbf{Choice}$ is such that
$\mathbf{Choice}_{\alpha}^{m}$ is finite for every $\alpha\in Ags$ and $m\in
M$. I focus on finite-choice models to simplify the evaluation rules for
objective and subjective ought-to-do’s. The reader is referred to [2] for the
evaluation rules in the case of infinite-choice models. The semantics on
$\mathcal{M}$ for the formulas of $\mathcal{L}_{\textsf{R}}$ are recursively
defined by the following truth conditions:

$\begin{array}[]{lll}\mathcal{M},\langle m,h\rangle\models p&\mbox{ iff
}&\langle m,h\rangle\in\mathcal{V}(p)\\\ \mathcal{M},\langle
m,h\rangle\models\neg\phi&\mbox{ iff }&\mathcal{M},\langle
m,h\rangle\not\models\phi\\\ \mathcal{M},\langle
m,h\rangle\models\phi\wedge\psi&\mbox{ iff }&\mathcal{M},\langle
m,h\rangle\models\phi\mbox{ and }\mathcal{M},\langle m,h\rangle\models\psi\\\
\mathcal{M},\langle m,h\rangle\models\Box\phi&\mbox{ iff }&\mbox{for all
}h^{\prime}\in H_{m},\mathcal{M},\langle m,h^{\prime}\rangle\models\phi\\\
\mathcal{M},\langle m,h\rangle\models[\alpha]\phi&\mbox{ iff }&\mbox{for all
}h^{\prime}\in\mathbf{Choice}^{m}_{\alpha}(h),\mathcal{M},\langle
m,h^{\prime}\rangle\models\phi\\\ \mathcal{M},\langle m,h\rangle\models
K_{\alpha}\phi&\mbox{ iff }&\mbox{for all }\langle
m^{\prime},h^{\prime}\rangle\mbox{ s. t. }\langle
m,h\rangle\sim_{\alpha}\langle m^{\prime},h^{\prime}\rangle,\\\
&&\mathcal{M},\langle m^{\prime},h^{\prime}\rangle\models\phi\\\
\mathcal{M},\langle m,h\rangle\models I_{\alpha}\phi&\mbox{ iff }&\mbox{there
exists }U\in\tau_{\alpha}^{\langle m,h\rangle}\mbox{ s. t.
}U\subseteq\|\phi\|\\\ \mathcal{M},\langle
m,h\rangle\models\odot_{\alpha}\phi&\mbox{ iff }&\mbox{for all
}L\in\mathbf{Optimal}^{m}_{\alpha},\mathcal{M},\left\langle
m,h^{\prime}\right\rangle\models\varphi\\\ &&\mbox{for every }h^{\prime}\in
L\\\ \mathcal{M},\langle
m,h\rangle\models\odot^{\mathcal{S}}_{\alpha}\varphi&\mbox{ iff }&\mbox{for
all }L\in\mathbf{SOptimal}^{m}_{\alpha},\mathcal{M},\left\langle
m^{\prime},h^{\prime}\right\rangle\models\varphi\\\ &&\mbox{for every
}m^{\prime}\mbox{ s. t. }m\sim_{\alpha}m^{\prime}\mbox{ and every
}h^{\prime}\in[L]^{m^{\prime\prime}}_{\alpha}.\\\ \end{array}$

where $\|\phi\|$ refers to the set $\left\\{\left\langle m,h\right\rangle\in
I(M\times H);\mathcal{M},\left\langle m,h\right\rangle\models\phi\right\\}$.

###  3.2 Formalization of Sub-Categories of Responsibility

The logic introduced in the previous subsection allows us to formalize
different modes of responsibility by means of formulas of
$\mathcal{L}_{\textsf{R}}$. Before diving into the formulas, let me present an
operational definition for the expression ‘mode of responsibility.’ For
$\alpha\in Ags$, index $\langle m,h\rangle$, and $\phi$ of
$\mathcal{L}_{\textsf{R}}$, a _mode of $\alpha$’s responsibility with respect
to $\phi$ at $\langle m,h\rangle$_ is a tuple consisting of three
constituents: (1) a set of categories, taken from Broersen’s three categories
of responsibility, that applies to the relation between $\alpha$ and $\phi$ at
$\langle m,h\rangle$, (2) the forms of responsibility—active or passive—that
apply to the categories in said set, and (3) a deontic context, determining
whether the forms of the categories are either blameworthy, praiseworthy, or
neutral. As for constituents (1) and (2), observe that the active and passive
forms of the three categories of responsibility lead to sub-categories of the
notion. For clarity, first I will introduce the stit-theoretic
characterizations of these sub-categories; afterwards, in Subsection 3.3,
these sub-categories will be discussed against the backdrop of the deontic
contexts that will decide their degree of blameworthiness or praiseworthiness
(constituent (3) in a given mode).

A maxim usually endorsed in the philosophical literature on moral
responsibility is the _principle of alternate possibilities_. According to
this principle, “a person is morally responsible for what he has done only if
he could have done otherwise” [16]. Following the example of [18], then, I
adopt the intuitions behind deliberative agency and restrict my view on
responsibility to situations where agents can be said to actually have had a
hand in bringing about states of affairs. Therefore, each sub-category of
$\alpha$’s responsibility with respect to $\phi$ at $\langle m,h\rangle$ will
include a positive condition—concerning the realization of $\phi$—and a
negative condition—concerning the realization of $\lnot\phi$. For $\alpha\in
Ags$ and $\phi$ of $\mathcal{L}_{\textsf{R}}$, the main sub-categories of
$\alpha$’s responsibility with respect to $\phi$ are displayed in Table 1.

_Category_ _Form_ |  Active (contributions) |  Passive (omissions)
---|---|---
Causal |  $[\alpha]\phi\land\Diamond[\alpha]\lnot\phi$ |  $\phi\land\Diamond[\alpha]\lnot\phi$
Informational |  $K_{\alpha}[\alpha]\phi\land\Diamond K_{\alpha}[\alpha]\lnot\phi$ |  $\phi\land K_{\alpha}\lnot[\alpha]\lnot\phi\land$ $\Diamond K_{\alpha}[\alpha]\lnot\phi$
Motivational |  $K_{\alpha}[\alpha]\phi\land I_{\alpha}[\alpha]\phi\land$ $\Diamond K_{\alpha}[\alpha]\lnot\phi$ |  $\phi\land K_{\alpha}\lnot[\alpha]\lnot\phi\land$ $I_{\alpha}\lnot[\alpha]\lnot\phi\land\Diamond K_{\alpha}[\alpha]\lnot\phi$
Table 1: Main sub-categories.

Let me explain and discuss Table 1. Let $\mathcal{M}$ be a _kiobt_ -model. For
$\alpha\in Ags$ and index $\langle m,h\rangle$, the sub-categories of
$\alpha$’s responsibility with respect to $\phi$ at $\langle m,h\rangle$ are
defined as follows:

  * •

$\alpha$ was _causal-active responsible_ for $\phi$ at $\langle m,h\rangle$
iff at $\langle m,h\rangle$ $\alpha$ has seen to it that $\phi$ (the positive
condition) and it was possible for $\alpha$ to prevent $\phi$ (the negative
condition). As such, I refer to state of affairs $\phi$ as a causal
contribution of $\alpha$ at $\langle m,h\rangle$. $\alpha$ was _causal-passive
responsible_ for $\phi$ at $\langle m,h\rangle$ iff at $\langle m,h\rangle$
$\phi$ was the case (the positive condition), and $\alpha$ refrained from
preventing $\phi$ while it was possible for $\alpha$ to prevent $\phi$ (the
negative conditions). To clarify, formula $\phi\to\lnot[\alpha]\lnot\phi$ is
valid, so that if $\phi$ was the case then $\alpha$ refrained from preventing
$\phi$. I refer to $\lnot\phi$ as a causal omission of $\alpha$ at $\langle
m,h\rangle$.

  * •

$\alpha$ was _informational-active responsible_ for $\phi$ at $\langle
m,h\rangle$ iff at $\langle m,h\rangle$ $\alpha$ has knowingly seen to it that
$\phi$ (the positive condition) and it was possible for $\alpha$ to knowingly
prevent $\phi$ (the negative condition). I refer to $\phi$ as a conscious
contribution of $\alpha$ at $\langle m,h\rangle$. $\alpha$ was _informational-
passive responsible_ for $\phi$ at $\langle m,h\rangle$ iff at $\langle
m,h\rangle$ $\phi$ was the case (the positive condition), and $\alpha$
knowingly refrained from preventing $\phi$ while it was possible for $\alpha$
to knowingly prevent $\phi$ (the negative conditions). I refer to $\lnot\phi$
as a conscious omission of $\alpha$ at $\langle m,h\rangle$.

  * •

$\alpha$ was _motivational-active responsible_ for $\phi$ at $\langle
m,h\rangle$ iff at $\langle m,h\rangle$ $\alpha$ has both knowingly and
intentionally seen to it that $\phi$ (the positive conditions) and it was
possible for $\alpha$ to knowingly prevent $\phi$ (the negative condition). I
refer to $\phi$ as a motivational contribution of $\alpha$ at $\langle
m,h\rangle$. $\alpha$ was _motivational-passive responsible_ for $\phi$ at
$\langle m,h\rangle$ iff at $\langle m,h\rangle$ $\phi$ was the case (the
positive condition), and $\alpha$ both knowingly and intentionally refrained
from preventing $\phi$ while it was possible for $\alpha$ to knowingly prevent
$\phi$ (the negative conditions). I refer to $\lnot\phi$ as a motivational
omission of $\alpha$ at $\langle m,h\rangle$.

The main reason for setting the negative conditions as stated in Table 1 is
that it greatly simplifies the relation between the active and the passive
forms of responsibility. That said, it is important to mention that these
negative conditions lead to a policy that I call _leniency on blameworthy
agents_.

Two important observations concerning the relations between these sub-
categories are the following:

  1. 1.

    1. (a)

If $\alpha$ was informational-active, resp. informational-passive, responsible
for $\phi$ at $\langle m,h\rangle$, then $\alpha$ was causal-active, resp.
causal-passive, responsible for $\phi$ at $\langle m,h\rangle$; the converse
is not true.

    2. (b)

If $\alpha$ was motivational-active, resp. motivational-passive, responsible
for $\phi$ at $\langle m,h\rangle$, then $\alpha$ was informational-active,
resp. informational-passive, responsible for $\phi$ at $\langle m,h\rangle$;
the converse is not true.

  2. 2.

For all three categories, the active form of responsibility with respect to
$\phi$ implies the passive form.

###  3.3 Formalization of Modes of Responsibility

In Section 2 I explained that obligations provide the deontic contexts of
responsibility, which in turn determine degrees of
praiseworthiness/blameworthiness for instances of the notion. Let
$\mathcal{M}$ be a _kiobt_ -model. Take $\alpha\in Ags$, and let $\phi$ be a
formula of $\mathcal{L}_{\textsf{R}}$. For each index $\langle m,h\rangle$,
there are 4 main possibilities for conjunctions of deontic modalities holding
at $\langle m,h\rangle$, according to whether $\Delta\phi$ or
$\lnot\Delta\phi$ is satisfied at the index, where
$\Delta\in\left\\{\odot_{\alpha},\odot^{\mathcal{S}}_{\alpha}\right\\}$. I
refer to any such conjunction as a _deontic context for $\alpha$’s
responsibility with respect to $\phi$ at $\langle m,h\rangle$_. Thus, these
contexts render 4 main levels of praiseworthiness, resp. blameworthiness,
under the premise that bringing about $\phi$ is praiseworthy and refraining
from bringing about $\phi$ is blameworthy. I use numbers $1$–$4$ to refer to
these levels, so that _Level_ $1$ corresponds the highest level of
praiseworthiness, resp. blameworthiness, and _Level_ $4$ corresponds to the
lowest level.

_Level 1_ : when deontic context
$\odot_{\alpha}\phi\land\odot^{\mathcal{S}}_{\alpha}\phi$ holds at $\langle
m,h\rangle$, which occurs iff at $\langle m,h\rangle$ $\alpha$ objectively and
subjectively ought to have seen to it that $\phi$. _Level 2_ : when deontic
context $\lnot\odot_{\alpha}\phi\land\odot^{\mathcal{S}}_{\alpha}\phi$ holds
at $\langle m,h\rangle$, which occurs iff at $\langle m,h\rangle$ $\alpha$
subjectively ought to have seen to it that $\phi$, but $\alpha$ did not
objectively ought to have seen to it that $\phi$. _Level 3_ : when deontic
context $\odot_{\alpha}\phi\land\lnot\odot^{\mathcal{S}}_{\alpha}\phi$ holds
at $\langle m,h\rangle$, which occurs iff at $\langle m,h\rangle$ $\alpha$
objectively ought to have seen to it that $\phi$, but $\alpha$ did not
subjectively ought to have seen to it that $\phi$. _Level 4_ : when deontic
context $\lnot\odot_{\alpha}\phi\land\lnot\odot^{\mathcal{S}}_{\alpha}\phi$
holds at $\langle m,h\rangle$, where, unless $\alpha$ either objectively or
subjectively ought have seen to it that $\lnot\phi$ at $\langle m,h\rangle$
(which would imply that a deontic context of the previous levels holds with
respect to $\lnot\phi$), neither bringing about $\phi$ nor refraining from
doing so elicits any interest in terms of blame-or-praise assignment.

For each of these deontic contexts, the _basic modes of $\alpha$’s active
responsibility with respect to $\phi$ at $\langle m,h\rangle$_ are displayed
in Table 2, and the _basic modes of $\alpha$’s passive responsibility_ are
obtained by substituting the term ’passive’ for ’active’ in such a table.

_Deg._ _Att._ |  Praiseworthiness |  Blameworthiness
---|---|---
$\mbox{\emph{Low}}_{A}$ |  Causal-active for $\phi$ ✓ Infor.-active for $\phi$ ✗ Motiv.-active for $\phi$ ✗ |  Causal-active for $\lnot\phi$ ✓ Infor.-active for $\lnot\phi$ ✗ Motiv.-active for $\lnot\phi$ ✗
$\mbox{\emph{Middle}}_{A}$ |  Causal-active for $\phi$ ✓ Infor.-active for $\phi$ ✓ Motiv.-active for $\phi$ ✗ |  Causal-active for $\lnot\phi$ ✓ Infor.-active for $\lnot\phi$ ✓ Motiv.-active for $\lnot\phi$ ✗
$\mbox{\emph{High}}_{A}$ |  Causal-active for $\phi$ ✓ Infor.-active for $\phi$ ✓ Motiv.-active for $\phi$ ✓ |  Causal-active for $\lnot\phi$ ✓ Infor.-active for $\lnot\phi$ ✓ Motiv.-active for $\lnot\phi$ ✓
Table 2: Modes of $\alpha$’s active responsibility with respect to $\phi$.

##  4 Axiomatization

This section is devoted to introducing proof systems for _IEAUST_. More
precisely, I present two systems:

  * •

A sound system for _IEAUST_ , for which achieving a completeness result is
still an open problem.

  * •

A sound and complete system for a technical extension of _IEAUST_ that I refer
to as _bi-valued_ _IEAUST_. Bi-valued _IEAUST_ was devised with the aim of
having a completeness result for a logic that would be reasonably similar to
the one presented in Section 3.

As for the first bullet point, a proof system for _IEAUST_ is defined as
follows:

######  Definition 4.1 (Proof system for _IEAUST_).

Let $\Lambda_{R}$ be the proof system defined by the following axioms and
rules of inference:

  * •

_(Axioms)_ All classical tautologies from propositional logic; the
$\mathbf{S5}$ schemata for $\square$, $[\alpha]$, and $K_{\alpha}$; the
$\mathbf{KD}$ schemata for $I_{\alpha}$; and the schemata given in Table 3.

_Basic-stit-theory schemata_ : $\begin{array}[]{ll}\square\phi\to[\alpha]\phi&(SET)\\\ \mbox{For distinct $\alpha_{1},\dots,\alpha_{m}$},&\\\ \bigwedge\limits_{1\leq k\leq m}\Diamond[\alpha_{i}]\phi_{i}\to\Diamond\left(\bigwedge\limits_{1\leq k\leq m}[\alpha_{i}]\phi_{i}\right)&(IA)\end{array}$ |  _Schemata for knowledge:_ $\begin{array}[]{ll}K_{\alpha}\phi\to[\alpha]\phi&(OAC)\\\ \Diamond K_{\alpha}\phi\to K_{\alpha}\Diamond\phi&(Unif-H)\end{array}$
---|---
_Schemata for objective ought-to-do’s:_ $\begin{array}[]{ll}\odot_{\alpha}(\phi\to\psi)\to(\odot_{\alpha}\phi\to\odot_{\alpha}\psi)&(A1)\\\ \square\phi\to\odot_{\alpha}\phi&(A2)\\\ \odot_{\alpha}\phi\to\square\odot_{\alpha}\phi&(A3)\\\ \odot_{\alpha}\phi\to\odot_{\alpha}([\alpha]\phi)&(A4)\\\ \odot_{\alpha}\phi\to\Diamond[\alpha]\phi&(Oic)\end{array}$ |  _Schemata for subjective ought-to-do’s:_ $\begin{array}[]{ll}\odot^{\mathcal{S}}_{\alpha}(\phi\to\psi)\to(\odot^{\mathcal{S}}_{\alpha}\phi\to\odot^{\mathcal{S}}_{\alpha}\psi)&(A5)\\\ \odot^{\mathcal{S}}_{\alpha}\phi\to\odot^{\mathcal{S}}_{\alpha}(K_{\alpha}\phi)&(A6)\\\ K_{\alpha}\square\phi\to\odot^{\mathcal{S}}_{\alpha}\phi&(SuN)\\\ \odot^{\mathcal{S}}_{\alpha}\phi\to\Diamond K_{\alpha}\phi&(s.Oic)\\\ \odot^{\mathcal{S}}_{\alpha}\phi\to K_{\alpha}\square\odot^{\mathcal{S}}_{\alpha}\phi&(s.Cl)\\\ \odot^{\mathcal{S}}_{\alpha}\phi\to\lnot\odot_{\alpha}\lnot\phi&(ConSO)\end{array}$
_Schemata for intentionality:_ $\begin{array}[]{ll}\square K_{\alpha}\phi\to I_{\alpha}\phi&(InN)\\\ I_{\alpha}\phi\to\square K_{\alpha}I_{\alpha}\phi&(KI)\end{array}$ |
Table 3: Axioms for the modalities’ interactions.

  * •

(Rules of inference) Modus Ponens, Substitution, and Necessitation for all
modal operators.

For a discussion of all these axioms and schemas, the reader is referred to
[2, 19, 4]. An important result for $\Lambda_{R}$, then, is the following
proposition, whose proof is relegated to Appendix A.

######  Proposition 4.2 (Soundness of $\Lambda_{R}$).

The proof system ${\Lambda_{R}}$ is sound with respect to the class of _kiobt_
-models.

Unfortunately, the question of whether $\Lambda_{R}$ is complete with respect
to the class of _kiobt_ -models is still an open problem. Now, in the search
for a complete proof system for _IEAUST_ , and following a strategy found in
my joint works with Jan Broersen [2, 3], I tried to first prove completeness
of $\Lambda_{R}$ with respect to a class of more general models, that I refer
to as _bi-valued_ _kiobt_ -models (Definition 4.3 below). This strategy led to
the need of dropping one of the schemata in $\Lambda_{R}$: $(ConSO)$. More
precisely, if $\Lambda_{R}^{\prime}$ is obtained from $\Lambda_{R}$ by
eliminating $(ConSO)$ in Definition 4.1, then $\Lambda_{R}^{\prime}$ turns out
to be sound and complete with respect to the class of _bi-valued_ _kiobt_
-models. The formal statements are included below.

######  Definition 4.3 (Bi-valued _kiobt_ -frames & models).

$\left\langle
M,\sqsubset,Ags,\mathbf{\mathbf{Choice}},\left\\{\sim_{\alpha}\right\\}_{\alpha\in
Ags},\tau,\mathbf{Value}_{\mathcal{O}},\mathbf{Value}_{\mathcal{S}}\right\rangle$
is called a _bi-valued_ _kiobt_ -frame iff

  * •

$M,\sqsubset,Ags,\mathbf{\mathbf{Choice}}$,
$\left\\{\sim_{\alpha}\right\\}_{\alpha\in Ags}$, and $\tau$ are defined just
as in Definition 3.2.

  * •

$\mathbf{Value}_{\mathcal{O}}$ and $\mathbf{Value}_{\mathcal{S}}$ are
functions that independently assign to each history $h\in H$ a real number.

A _bi-valued kiobt_ -model $\mathcal{M}$, then, results from adding a
valuation function $\mathcal{V}$ to a bi-valued _kiobt_ -frame, where
$\mathcal{V}:P\to 2^{I(M\times H)}$ assigns to each atomic proposition of
$\mathcal{L}_{\textsf{R}}$ a set of indices (recall that $P$ is the set of
propositions in $\mathcal{L}_{\textsf{R}}$).

The two value functions in bi-valued _kiobt_ -frames allow us to redefine the
dominance orderings so that they are independent from one another, something
that proves useful in achieving a completeness result in the style of [2]. For
$\alpha\in Ags$ and $m\in M$, two general orderings $\leq$ and $\leq_{s}$ are
first defined on $2^{H_{m}}$: for $X,Y\subseteq H_{m}$, $X\leq Y$, resp.
$X\leq_{s}Y$, iff
$\mathtt{Value}_{\mathcal{O}}(h)\leq\mathtt{Value}_{\mathcal{O}}(h^{\prime})$,
resp.
$\mathtt{Value}_{\mathcal{S}}(h)\leq\mathtt{Value}_{\mathcal{S}}(h^{\prime})$,
for every $h\in X$ and $h^{\prime}\in Y$. Then, for $\alpha\in Ags$ and $m\in
M$, an objective dominance ordering $\preceq$ is now defined on
$\mathbf{Choice}_{\alpha}^{m}$ by the rule: $L\preceq L^{\prime}$ iff for
every $S\in\mathbf{State}_{\alpha}^{m},L\cap S\leq L^{\prime}\cap S.$ In turn,
for $\alpha\in Ags$ and $m\in M$, a subjective dominance ordering
$\preceq_{s}$ is now defined on $\mathbf{Choice}_{\alpha}^{m}$ by the rule:
$L\preceq_{s}L^{\prime}$ iff for all $m^{\prime}$ such that
$m\sim_{\alpha}m^{\prime}$ and each
$S\in\mathbf{State}_{\alpha}^{m},[L]^{m^{\prime}}_{\alpha}\cap
S\leq_{s}[L^{\prime}]^{m^{\prime}}_{\alpha}\cap S$. With these new notions,
the sets $\mathbf{Optimal}^{m}_{\alpha}$ and $\mathbf{SOptimal}^{m}_{\alpha}$
are redefined accordingly, and the evaluation rules for the formulas of
$\mathcal{L}_{\textsf{R}}$ (with respect to bi-valued _kiobt_ -models) are
given just as in Definition 3.3. As mentioned before, I refer to the resulting
logic as _bi-valued_ _IEAUST_. Bi-valued _IEAUST_ , then, admits the following
metalogic result, whose proof is sketched in Appendix A.

######  Theorem 4.4 (Soundness & Completeness of $\Lambda_{R}^{\prime}$).

Let $\Lambda_{R}^{\prime}$ be the proof system obtained from $\Lambda_{R}$ by
eliminating $(ConSO)$ in Definition 4.1. Then $\Lambda_{R}^{\prime}$ is sound
and complete with respect to the class of bi-valued _kiobt_ -models.

##  5 Conclusion

This paper built a formal theory of responsibility by means of stit-theoretic
models and languages that were designed to explore the interplay between the
following components of responsibility: agency, knowledge, beliefs,
intentions, and obligations. Said models were integrated into a framework that
is rich enough to provide logic-based characterizations for different
instances of three categories of responsibility: causal, informational, and
motivational responsibility.

The developed theory belongs to a relatively recent tradition in the
philosophical literature, that seeks to formalize responsibility allocation by
means of models of agency and logic-based languages (see, for instance, [17],
[18], [6], [20], [21], and [8]). Most of these frameworks characterize
different forms of responsibility as combinations of causal agency, knowledge,
and the principle of alternate possibilities. The novelty of the present
approach, then, lies in the introduction of intentionality and ought-to-do’s.
Such an introduction gives rise to a taxonomy that distinguishes various kinds
of responsibility and blameworthiness/praiseworthiness in a methodical,
meticulous way. Interesting directions for future work, then, involve
extending these models with beliefs and rational decision-making, group
notions (coalitions, group knowledge & belief, collective intentionality,
collective responsibility), temporal modalities, and long-term strategies, for
instance. As for the technical aspects of the formal theory, an important
directions for future work involve checking whether the logic is decidable,
checking for the complexity of its satisfiability problem, and figuring out
its applicability for implementation.555Implementing logics of responsibility
might prove relevant in the design, formal verification, and explainability of
ethical AI (see, for instance, [13]).

## References

  * [1]
  * [2] Aldo Iván Ramírez Abarca & Jan Broersen (2019): _A Logic of Objective and Subjective Oughts_.  In: European Conference on Logics in Artificial Intelligence, Springer, pp. 629–641, 10.1007/978-3-030-19570-0_41.
  * [3] Aldo Iván Ramírez Abarca & Jan Broersen (2021): _A Deontic Stit Logic Based on Beliefs and Expected Utility_.  Electronic Proceedings in Theoretical Computer Science 335, pp. 281–294, 10.4204%2Feptcs.335.27.
  * [4] Aldo Iván Ramírez Abarca & Jan Broersen (2023): _A stit logic of intentionality_.  In Carlos Areces & Diana Costa, editors: Dynamic Logic. New Trends and Applications, Springer, pp. 125–153, 10.1007/978-3-031-26622-5_8.
  * [5] Thomas Ågotnes (2006): _Action and knowledge in alternating-time temporal logic_.  Synthese 149(2), pp. 375–407, 10.1007/s11229-005-3875-8.
  * [6] Natasha Alechina, Joseph Y Halpern & Brian Logan (2017): _Causality, Responsibility and Blame in Team Plans_.  In: Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, pp. 1091–1099.  Available at https://dl.acm.org/doi/10.5555/3091125.3091279.
  * [7] Alejandro Barredo Arrieta, Natalia Díaz-Rodríguez, Javier Del Ser, Adrien Bennetot, Siham Tabik, Alberto Barbado, Salvador García, Sergio Gil-López, Daniel Molina & Richard Benjamins (2020): _Explainable Artificial Intelligence (XAI): Concepts, taxonomies, opportunities and challenges toward responsible AI_.  Information Fusion 58, pp. 82–115, 10.1016/j.inffus.2019.12.012.
  * [8] Christel Baier, Florian Funke & Rupak Majumdar (2021): _A Game-Theoretic Account of Responsibility Allocation_.  In: Thirtieth International Joint Conference on Artificial Intelligence, IJCAI, pp. 1773–1779, 10.24963/ijcai.2021/244.
  * [9] N. Belnap, M. Perloff & M. Xu (2001): _Facing the future: agents and choices in our indeterminist world_.  Oxford University Press.
  * [10] Jan Broersen (2008): _A complete stit logic for knowledge and action, and some of its applications_.  In: International Workshop on Declarative Agent Languages and Technologies, Springer, pp. 47–59, 10.1007/978-3-540-93920-7_4.
  * [11] Jan Broersen (2011): _Deontic epistemic stit logic distinguishing modes of mens rea_.  Journal of Applied Logic 9(2), pp. 137–152, 10.1016/j.jal.2010.06.002.
  * [12] Jan Broersen & Aldo Iván Ramírez Abarca (2018): _Formalising Oughts and Practical Knowledge without Resorting to Action Types_.  In: Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems, International Foundation for Autonomous Agents and Multiagent Systems, pp. 1877–1879.  Available at https://dl.acm.org/doi/abs/10.5555/3237383.3238009.
  * [13] Roberta Calegari, Giovanni Ciatto, Enrico Denti & Andrea Omicini (2020): _Logic-based technologies for intelligent systems: State of the art and perspectives_.  Information 11(3), p. 167, 10.3390/info11030167.
  * [14] Roger Crisp (2014): _Aristotle: Nicomachean Ethics_.  Cambridge University Press.
  * [15] Hein Duijf (2018): _Let’s do it!: Collective responsibility, joint action, and participation_.  Ph.D. thesis, Utrecht University.
  * [16] Harry Frankfurt (2018): _Alternate possibilities and moral responsibility_.  In: Moral Responsibility and Alternative Possibilities, Routledge, pp. 17–25, 10.2307/2023833.
  * [17] Tiago de Lima, Lambér Royakkers & Frank Dignum (2010): _A logic for reasoning about responsibility_.  Logic Journal of the IGPL 18(1), pp. 99–117, 10.1093/jigpal/jzp073.
  * [18] Emiliano Lorini, Dominique Longin & Eunate Mayor (2014): _A logical analysis of responsibility attribution: emotions, individuals and collectives_.  Journal of Logic and Computation 24(6), pp. 1313–1339, 10.1093/logcom/ext072.
  * [19] Yuko Murakami (2004): _Utilitarian deontic logic_.  Advances in Modal Logic 287\.
  * [20] Pavel Naumov & Jia Tao (2019): _Blameworthiness in strategic games_.  In: Proceedings of the AAAI Conference on Artificial Intelligence, 33, pp. 3011–3018, 10.1609/aaai.v33i01.33013011.
  * [21] Pavel Naumov & Jia Tao (2020): _An epistemic logic of blameworthiness_.  Artificial Intelligence 283, p. 103269, 10.1016/j.artint.2020.103269.
  * [22] Luís Moniz Pereira & Ari Saptawijaya (2016): _Programming machine ethics_.  26, Springer, 10.1007/978-3-319-29354-7_8.
  * [23] Ibo van de Poel (2011): _The relation between forward-looking and backward-looking responsibility_.  In: Moral Responsibility, Springer, pp. 37–52, 10.1007/978-94-007-1878-4_3.
  * [24] Gary Watson (1996): _Two faces of responsibility_.  Philosophical Topics 24(2), pp. 227–248, 10.5840/philtopics199624222.
  * [25] Bernard Weiner (1995): _Judgments of responsibility: A foundation for a theory of social conduct_.  Guilford Press.
  * [26] Ming Xu (1994): _Decidability of deliberative stit theories with multiple agents_.  In: International Conference on Temporal Logic, Springer, pp. 332–348, 10.1007/BFb0013997.

##  A Metalogic Results for _IEAUST_

##  Appendix A Soundness

######  Proposition A.1 (Soundness of ${\Lambda_{R}}$).

The system ${\Lambda_{R}}$ (Definition 4) is sound with respect to the class
of _kiobt_ -models.

###### Proof.

The proof of soundness is routine: the validity of the $\mathbf{S5}$ schemata
for $\square$ and $[\alpha]$, as well as that of $(SET)$ and $(IA)$, is
standard from [26]; the validity of the $\mathbf{S5}$ schemata for
$K_{\alpha}$ is standard from epistemic logic; the validity of schemata
$(A1)$–$(A4)$, as well as that of $(Oic)$, is standard from [19]; the validity
of the $\mathbf{KD}$ schemata for $I_{\alpha}$, as well as that of $(InN)$,
follows from Definitions 3.2 and 3.3; and the validity of $(KI)$ follows from
frame condition $(\mathtt{KI})$; and the validity of schemata $(OAC)$,
$(Unif-H)$, $(A5)$ and $(A6)$, as well as that of $(SuN)$, $(s.Oic)$,
$(s.Cl)$, and $(ConSO)$ can be shown as follows:

To see that $\mathcal{M}\models(OAC)$, take $\left\langle m,h\right\rangle$
such that $\mathcal{M},\left\langle m,h\right\rangle\models
K_{\alpha}\varphi$. Take $h^{\prime}\in\mathbf{Choice}_{\alpha}^{m}(h)$. Frame
condition $(\mathtt{OAC})$ implies that $\left\langle
m,h\right\rangle\sim_{\alpha}\left\langle m,h^{\prime}\right\rangle$. The
assumption that $\mathcal{M},\left\langle m,h\right\rangle\models
K_{\alpha}\varphi$ then implies that $\mathcal{M},\left\langle
m,h^{\prime}\right\rangle\models\varphi$. Therefore, for any
$h^{\prime}\in\mathbf{Choice}_{\alpha}^{m}(h)$, $\mathcal{M},\left\langle
m,h^{\prime}\right\rangle\models\varphi$, which implies that
$\mathcal{M},\left\langle m,h\right\rangle\models[\alpha]\varphi$.

To see that $\mathcal{M}\models(Unif-H)$, take $\left\langle m,h\right\rangle$
such that $\mathcal{M},\left\langle m,h\right\rangle\models\Diamond
K_{\alpha}\varphi$. Let $\left\langle m^{\prime},h^{\prime}\right\rangle$ be
an index such that $\left\langle m,h\right\rangle\sim_{\alpha}\left\langle
m^{\prime},h^{\prime}\right\rangle$. We want to show that
$\mathcal{M},\left\langle
m^{\prime},h^{\prime}\right\rangle\models\Diamond\varphi$. The fact that
$\mathcal{M},\left\langle m,h\right\rangle\models\Diamond K_{\alpha}\varphi$
implies that there exists $h_{*}\in H_{m}$ such that $(\star)$
$\mathcal{M},\left\langle m,h_{*}\right\rangle\models K_{\alpha}\varphi$.
Frame condition $(\mathtt{Unif-H})$ implies that there exists
$h_{*}^{\prime}\in H_{m^{\prime}}$ such that $\left\langle
m,h_{*}\right\rangle\sim_{\alpha}\left\langle
m^{\prime},h_{*}^{\prime}\right\rangle$. With $(\star)$, this last fact
implies that $\mathcal{M},\left\langle
m^{\prime},h_{*}^{\prime}\right\rangle\models\varphi$, which in turn implies
that $\mathcal{M},\left\langle
m^{\prime},h^{\prime}\right\rangle\models\Diamond\varphi$. Therefore,
$\mathcal{M},\left\langle m,h\right\rangle\models K_{\alpha}\Diamond\varphi$.

To see that $\mathcal{M}\models(A6)$, take $\left\langle m,h\right\rangle$
such that $\mathcal{M},\left\langle
m,h\right\rangle\models\odot^{\mathcal{S}}_{\alpha}\varphi$. We want to show
that, for every $L\in\mathbf{Choice}^{m}_{\alpha}$ such that
$[L]^{m^{\prime}}\not\subseteq\left|K_{\alpha}\varphi\right|^{m^{\prime}}$
(for some $m^{\prime}$ such that $m\sim_{\alpha}m^{\prime}$), there is
$L^{\prime}\in\mathbf{Choice}_{\alpha}^{m}$ such that $L\prec_{s}L^{\prime}$
and, if $L^{\prime\prime}=L^{\prime}$ or
$L^{\prime}\preceq_{s}L^{\prime\prime}$, then
$[L^{\prime\prime}]^{m^{\prime\prime}}_{\alpha}\subseteq\left|K_{\alpha}\varphi\right|^{m^{\prime\prime}}$
for every $m^{\prime\prime}$ such that $m\sim_{\alpha}m^{\prime\prime}$. Take
$L\in\mathbf{Choice}^{m}_{\alpha}$ such that there exists $m^{\prime}\in M$
such that $m\sim_{\alpha}m^{\prime}$ and
$[L]^{m^{\prime}}\not\subseteq|K_{\alpha}\varphi|^{m^{\prime}}$. This implies
that
$[L]^{m^{\prime\prime\prime}}\not\subseteq\left|\phi\right|^{m^{\prime\prime\prime}}$
for some $m^{\prime\prime\prime}$ such that
$m^{\prime}\sim_{\alpha}m^{\prime\prime\prime}$. Now, transitivity of
$\sim_{\alpha}$ implies that $m\sim_{\alpha}m^{\prime\prime\prime}$.
Therefore, the assumption that $\mathcal{M},\left\langle
m,h\right\rangle\models\odot^{\mathcal{S}}_{\alpha}\varphi$ implies that there
is $L^{\prime}\in\mathbf{Choice}_{\alpha}^{m}$ such that
$L\prec_{s}L^{\prime}$ and, if $L^{\prime\prime}=L^{\prime}$ or
$L^{\prime}\preceq_{s}L^{\prime\prime}$, then
$[L^{\prime\prime}]^{m^{\prime\prime}}_{\alpha}\subseteq\left|\varphi\right|^{m^{\prime\prime}}$
for every $m^{\prime\prime}$ such that $m\sim_{\alpha}m^{\prime\prime}$. By
definition of epistemic clusters and transitivity of $\sim_{\alpha}$, this
last clause implies that if $L^{\prime\prime}=L^{\prime}$ or
$L^{\prime}\preceq_{s}L^{\prime\prime}$ then
$[L^{\prime\prime}]^{m^{\prime\prime}}_{\alpha}\subseteq\left|K_{\alpha}\varphi\right|^{m^{\prime\prime}}$
for every $m^{\prime\prime}$ such that $m\sim_{\alpha}m^{\prime\prime}$. Thus,
$L^{\prime}$ attests to the fact that $\mathcal{M},\left\langle
m,h\right\rangle\models\odot^{\mathcal{S}}_{\alpha}\left(K_{\alpha}\varphi\right)$.

To see that $\mathcal{M}\models(SuN)$, take $\left\langle m,h\right\rangle$
such that $\mathcal{M},\left\langle m,h\right\rangle\models
K_{\alpha}\square\varphi$. Take $L\in\mathbf{Choice}^{m}_{\alpha}$, and let
$m^{\prime}\in M$ be such that $m\sim_{\alpha}m^{\prime}$ (which means that
there exist $j\in H_{m}$, $j^{\prime}\in H_{m^{\prime}}$ such that
$\left\langle m,j\right\rangle\sim_{\alpha}\left\langle
m^{\prime},j^{\prime}\right\rangle$). Condition ($\mathtt{Unif-H}$) ensures
that there exists $h^{\prime}\in H_{m^{\prime}}$ such that $\left\langle
m,h\right\rangle\sim_{\alpha}\left\langle m^{\prime},h^{\prime}\right\rangle$.
The assumption that $\mathcal{M},\left\langle m,h\right\rangle\models
K_{\alpha}\square\varphi$ then implies that $\mathcal{M},\left\langle
m^{\prime},h^{\prime}\right\rangle\models\square\varphi$. Thus, for any
$h^{\prime\prime}\in[L]^{m^{\prime}}_{\alpha}$, the fact that
$h^{\prime\prime}\in H_{m^{\prime}}$ yields that $\mathcal{M},\left\langle
m^{\prime},h^{\prime\prime}\right\rangle\models\varphi$. Therefore, for all
$L\in\mathbf{Choice}^{m}_{\alpha}$ and $m^{\prime}$ such that
$m\sim_{\alpha}m^{\prime}$,
$[L]^{m^{\prime}}_{\alpha}\subseteq\left|\phi\right|^{m^{\prime}}$, which
vacuously implies that $\mathcal{M},\left\langle
m,h\right\rangle\models\odot^{\mathcal{S}}_{\alpha}\varphi$.

To see that $\mathcal{M}\models(s.Oic)$, take $\left\langle m,h\right\rangle$
such that $\mathcal{M},\left\langle
m,h\right\rangle\models\odot^{\mathcal{S}}_{\alpha}\varphi$. This implies that
there exists $L\subseteq H_{m}$ such that
$[L]^{m^{\prime\prime}}_{\alpha}\subseteq\left|\phi\right|^{m^{\prime\prime}}$
for every $m^{\prime\prime}\in M$ such that $m\sim_{\alpha}m^{\prime\prime}$.
Since $\sim_{\alpha}$ is reflexive,
$[L]^{m}_{\alpha}\subseteq\left|\phi\right|^{m}$. Now, take $h_{0}\in L$. Let
$\left\langle m^{\prime},h^{\prime}\right\rangle$ be an index such that
$\left\langle m,h_{0}\right\rangle\sim_{\alpha}\left\langle
m^{\prime},h^{\prime}\right\rangle$. From the definition of epistemic
clusters, $h^{\prime}\in[L]^{m^{\prime}}_{\alpha}$, so the fact that
$[L]^{m^{\prime}}_{\alpha}\subseteq\left|\phi\right|^{m^{\prime}}$ implies
that $\mathcal{M},\left\langle
m^{\prime},h^{\prime}\right\rangle\models\varphi$. Therefore, history
$h_{0}\in H_{m}$ is such that, for every $\left\langle
m^{\prime},h^{\prime}\right\rangle$ with $\left\langle
m,h_{0}\right\rangle\sim_{\alpha}\left\langle
m^{\prime},h^{\prime}\right\rangle$, $\mathcal{M},\left\langle
m^{\prime},h^{\prime}\right\rangle\models\varphi$. This means that
$\mathcal{M},\left\langle m,h_{0}\right\rangle\models K_{\alpha}\varphi$,
which implies that $\mathcal{M},\left\langle m,h\right\rangle\models\Diamond
K_{\alpha}\varphi$.

To see that $\mathcal{M}\models(s.Cl)$, take $\left\langle
m_{*},h_{*}\right\rangle$ such that $\mathcal{M},\left\langle
m_{*},h_{*}\right\rangle\models\odot^{\mathcal{S}}_{\alpha}\varphi$. Let
$\left\langle m,j\right\rangle$ be such that $\left\langle
m_{*},h_{*}\right\rangle\sim_{\alpha}\left\langle m,j\right\rangle$. Take
$h\in H_{m}$. We want to show that, for every
$L\in\mathbf{Choice}^{m}_{\alpha}$ such that
$[L]^{m^{\prime}}\not\subseteq\left|\phi\right|^{m^{\prime}}$ (for some
$m^{\prime}$ such that $m\sim_{\alpha}m^{\prime}$), there is
$L^{\prime}\in\mathbf{Choice}_{\alpha}^{m}$ such that $L\prec_{s}L^{\prime}$
and, if $L^{\prime\prime}=L^{\prime}$ or
$L^{\prime}\preceq_{s}L^{\prime\prime}$, then
$[L^{\prime\prime}]^{m^{\prime\prime}}_{\alpha}\subseteq\left|\phi\right|^{m^{\prime\prime}}$
for every $m^{\prime\prime}$ such that $m\sim_{\alpha}m^{\prime\prime}$. Take
$L\in\mathbf{Choice}^{m}_{\alpha}$ such that there exists $m^{\prime}\in M$
such that $m\sim_{\alpha}m^{\prime}$ and
$[L]^{m^{\prime}}\not\subseteq\left|\phi\right|^{m^{\prime}}$. Let $N_{L}$ be
an action in $\mathbf{Choice}^{m_{*}}_{\alpha}$ such that
$N_{L}\subseteq[L]^{m_{*}}_{\alpha}$, where we know that such an action exists
in virtue of $(\mathtt{Unif-H})$ and $(\mathtt{OAC})$. Notice that
transitivity of $\sim_{\alpha}$ entails that
$\left[N_{L}\right]^{o}_{\alpha}=[L]^{o}_{\alpha}$ for any moment $o$, so that
$\left[N_{L}\right]^{m^{\prime}}_{\alpha}\not\subseteq\left|\phi\right|^{m^{\prime}}$.
Since $\mathcal{M},\left\langle
m_{*},h_{*}\right\rangle\models\odot^{\mathcal{S}}_{\alpha}\varphi$, there
must exist $N\in\mathbf{Choice}^{m_{*}}_{\alpha}$ such that $N_{L}\prec_{s}N$
and, if $N^{\prime}=N$ or $N\preceq_{s}N^{\prime}$, then
$[N^{\prime}]^{m^{\prime\prime}}_{\alpha}\subseteq\left|\phi\right|^{m^{\prime\prime}}$
for every $m^{\prime\prime}$ such that $m_{*}\sim_{\alpha}m^{\prime\prime}$.
Now, let $L_{N}$ be an action in $\mathbf{Choice}^{m}_{\alpha}$ such that
$L_{N}\subseteq[N]^{m}_{\alpha}$ (which implies that
$\left[L_{N}\right]^{o}_{\alpha}=[N]^{o}_{\alpha}$ for any moment $o$). We
claim that $L\prec_{s}L_{N}$, and show our claim with the following argument:
let $m^{\prime\prime}\in M$ be such that $m\sim_{\alpha}m^{\prime\prime}$, and
take $S\in\mathbf{State}^{m^{\prime\prime}}_{\alpha}$; on the one hand,
($\star$) $[L]^{m^{\prime\prime}}_{\alpha}\cap
S=\left[N_{L}\right]^{m^{\prime\prime}}_{\alpha}\cap
S\leq[N]^{m^{\prime\prime}}_{\alpha}\cap
S=\left[L_{N}\right]^{m^{\prime\prime}}_{\alpha}\cap S$; on the other hand, we
know that there exist a moment $m^{\prime\prime\prime}$ and a state
$S_{0}\in\mathbf{State}^{m^{\prime\prime\prime}}_{\alpha}$ such that
$m_{*}\sim_{\alpha}m^{\prime\prime\prime}$ and such that
$[N]^{m^{\prime\prime\prime}}_{\alpha}\cap
S_{0}\not\leq\left[N_{L}\right]^{m^{\prime\prime\prime}}_{\alpha}\cap S_{0}$;
therefore, $(\star\star)$
$\left[L_{N}\right]^{m^{\prime\prime\prime}}_{\alpha}\cap
S_{0}=[N]^{m^{\prime\prime\prime}}_{\alpha}\cap
S_{0}\not\leq\left[N_{L}\right]^{m^{\prime\prime\prime}}_{\alpha}\cap
S_{0}=[L]^{m^{\prime\prime\prime}}_{\alpha}\cap S_{0}$. Together, $(\star)$
and $(\star\star)$ entail that $L\prec_{s}L_{N}$, proving our claim. Now, let
$L^{\prime\prime}\in\mathbf{Choice}^{m}_{\alpha}$ be such that
$L^{\prime\prime}=L_{N}$ or $L_{N}\preceq_{s}L^{\prime\prime}$. If
$L^{\prime\prime}=L_{N}$, then
$[L^{\prime\prime}]^{m^{\prime\prime}}_{\alpha}=[N]^{m^{\prime\prime}}_{\alpha}\subseteq\left|\phi\right|^{m^{\prime\prime}}$
for every $m^{\prime\prime}$ such that $m\sim_{\alpha}m^{\prime\prime}$. If
$L_{N}\prec_{s}L^{\prime\prime}$, then an argument similar to the one used to
show that our claim was true renders that there is an action
$N_{L^{\prime\prime}}\in\mathbf{Choice}^{m_{*}}_{\alpha}$ such that
$N_{L^{\prime\prime}}\subseteq[L^{\prime\prime}]^{m_{*}}_{\alpha}$ and
$N\preceq_{s}N_{L^{\prime\prime}}$. Thus,
$[L^{\prime\prime}]^{m^{\prime\prime}}_{\alpha}=[N_{L^{\prime\prime}}]^{m^{\prime\prime}}_{\alpha}\subseteq\left|\phi\right|^{m^{\prime\prime}}$.
With this, we have shown that $\mathcal{M},\left\langle
m,h\right\rangle\models\odot^{\mathcal{S}}_{\alpha}\varphi$ for every $h\in
H_{m}$, so that $\mathcal{M},\left\langle
m,j\right\rangle\models\square\odot^{\mathcal{S}}_{\alpha}\varphi$. But
$\left\langle m,j\right\rangle$ was an arbitrary index such that $\left\langle
m_{*},h_{*}\right\rangle\sim_{\alpha}\left\langle m,j\right\rangle$. Thus,
$\mathcal{M},\left\langle m_{*},h_{*}\right\rangle\models
K_{\alpha}\square\odot^{\mathcal{S}}_{\alpha}\varphi$.

Let us show that $\mathcal{M}\models(ConSO)$. First of all, let us show that,
for all $L,L^{\prime}\in\mathbf{Choice}_{\alpha}^{m}$, if
$L\preceq_{s}L^{\prime}$, then $L\preceq L^{\prime}$. Take
$L,L^{\prime}\in\mathbf{Choice}_{\alpha}^{m}$. If $L\preceq_{s}L^{\prime}$,
then, for each $m^{\prime}$ such that $m\sim_{\alpha}m^{\prime}$,
$\mathbf{Value}(h)\leq\mathbf{Value}(h^{\prime})$ for every
$h\in[L]^{m^{\prime}}_{\alpha},h^{\prime}\in[L^{\prime}]^{m^{\prime}}_{\alpha}$.
Reflexivity of $\sim_{\alpha}$ implies both that $m\sim_{\alpha}m^{\prime}$
and that $L\subseteq[L]^{m}_{\alpha}$ and
$L^{\prime}\subseteq[L^{\prime}]^{m}_{\alpha}$. Therefore, for all
$h^{\prime\prime}\in L$ and $h^{\prime\prime\prime}\in L^{\prime}$,
$\mathbf{Value}(h^{\prime\prime})\leq\mathbf{Value}(h^{\prime\prime\prime})$,
which implies that $L\preceq L^{\prime}$.

Now, let $\langle m,h\rangle$ be an index. Assume for a contradiction that
($\star$) $\mathcal{M},\left\langle
m,h\right\rangle\models\odot_{\alpha}^{\mathcal{S}}\varphi$ and that
($\star\star$) $\mathcal{M},\left\langle
m,h\right\rangle\models\odot_{\alpha}\lnot\varphi$. On the one hand,
assumption $(\star)$ implies that there is
$L_{*}\in\mathbf{Choice}_{\alpha}^{m}$ such that
$L_{*}\subseteq\left|\phi\right|^{m}$. Thus, assumption ($\star\star$) yields
that there is $L_{*}^{\prime}\in\mathbf{Choice}_{\alpha}^{m}$ such that
$L_{*}\prec L_{*}^{\prime}$ and, if $N=L_{*}^{\prime}$ or
$L_{*}^{\prime}\preceq N$, then $N\subseteq|\lnot\phi|^{m}$. In particular,
$L_{*}^{\prime}\subseteq|\lnot\phi|^{m}$. Assumption ($\star$) then implies
that there is $L_{*}^{\prime\prime}\in\mathbf{Choice}_{\alpha}^{m}$ such that
$L_{*}^{\prime}\prec_{s}L_{*}^{\prime\prime}$ and, if $N=L_{*}^{\prime\prime}$
or $L_{*}^{\prime\prime}\preceq_{s}N$, then
$N\subseteq[N]^{m}_{\alpha}\subseteq\left|\phi\right|^{m}$. In particular,
$L_{*}^{\prime\prime}\subseteq\left|\phi\right|^{m}$. On the other hand, by
the first observation in the proof, the fact that
$L_{*}^{\prime}\prec_{s}L_{*}^{\prime\prime}$ implies that
$L_{*}^{\prime}\preceq L_{*}^{\prime\prime}$, so that assumption
($\star\star$) yields that $L_{*}^{\prime\prime}\subseteq|\lnot\phi|^{m}$,
which contradicts the previously shown fact that
$L_{*}^{\prime\prime}\subseteq\left|\phi\right|^{m}$. Thus,
$\mathcal{M},\left\langle
m,h\right\rangle\models\odot_{\alpha}^{\mathcal{S}}\varphi\to\lnot\odot_{\alpha}\lnot\varphi$
for every index $\left\langle m,h\right\rangle$, so that
$\odot_{\alpha}^{\mathcal{S}}\varphi\to\lnot\odot_{\alpha}\lnot\varphi$ is
indeed valid.

It is clear that the rules of inference _Modus Ponens_ , Substitution, and
Necessitation for the modal operators all preserve validity. ∎

##  Appendix B Completeness

As mentioned in the main body of the paper, whether $\Lambda_{R}$ is complete
with respect to the class of _kiobt_ -models is still an open problem.
However, the proof system $\Lambda_{R}^{\prime}$—obtained from $\Lambda_{R}$
by eliminating $(ConSO)$ in Definition 4.1—is sound and complete with respect
to the class of bi-valued _kiobt_ -models (Definition 4.3). Soundness follows
from Proposition A.1, and the proof of completeness is obtained by integrating
the proofs of completeness in [2] and [4]. More precisely, the proof of
completeness will be sketched below as a two-step process. First, I introduce
a Kripke semantics for _bi-valued_ _IEAUST_ , where the formulas of
$\mathcal{L}_{\textsf{R}}$ are evaluated on bi-valued Kripke-_kios_ -models
(Definition A.2). Completeness of ${\Lambda_{R}}$’ with respect to the class
of these structures is shown via the well-known technique of canonical models.
Secondly, a truth-preserving correspondence between bi-valued Kripke-_kios_
-models and a sub-class of bi-valued _kiobt_ -models is used to prove
completeness with respect to bi-valued _kiobt_ -models via completeness with
respect to bi-valued Kripke-_kios_ -models.

A Kripke semantics for _IEAUST_ is defined as follows:

######  Definition A.2 (Bi-valued Kripke-_kios_ -frames & models).

A tuple

$\left\langle
W,Ags,R_{\square},\mathbf{\mathbf{Choice}},\left\\{\approx_{\alpha}\right\\}_{\alpha\in
Ags},\left\\{R_{\alpha}^{I}\right\\}_{\alpha\in
Ags},\mathtt{Value}_{\mathcal{O}},\mathtt{Value}_{\mathcal{S}}\right\rangle$

is called a _bi-valued_ Kripke-_kios_ -frame iff

  * •

$W$ is a set of possible worlds. $R_{\square}$ is an equivalence relation over
$W$. For $w\in W$, the class of $w$ under $R_{\square}$ is denoted by
$\overline{w}$. $\mathtt{Choice}$ is a function that assigns to each
$\alpha\in Ags$ and $\square$-class $\overline{w}$ a partition
$\mathtt{Choice}_{\alpha}^{\overline{w}}$ of $\overline{w}$ given by an
equivalence relation denoted by $R_{\alpha}^{\overline{w}}$. $\mathtt{Choice}$
must satisfy the following constraint:

    * –

$\mathtt{(IA)_{K}}$ For all $w\in W$, each function $s:Ags\to
2^{\overline{w}}$ that maps $\alpha$ to a member of
$\mathtt{Choice}^{\overline{w}}_{\alpha}$ is such that $\bigcap_{\alpha\in
Ags}s(\alpha)\neq\emptyset$ (where the set of all functions $s$ that map
$\alpha$ to a member of $\mathtt{Choice}^{\overline{w}}_{\alpha}$ is denoted
by $\mathtt{Select}^{\overline{w}}$).

For $\alpha\in Ags$, $w\in W$, and $v\in\overline{w}$, the class of $v$ in the
partition $\mathtt{Choice}^{\overline{w}}_{\alpha}$ is denoted by
$\mathtt{Choice}^{\overline{w}}_{\alpha}(v)$. Now, for $\beta\in Ags$ and
$w\in W$,
$\mathtt{State}_{\beta}^{\overline{w}}:=\left\\{S\subseteq\overline{w};S=\bigcap_{\alpha\in
Ags-\left\\{\beta\right\\}}s(\alpha),\mbox{ for
}s\in\mathtt{Select}^{\overline{w}}\right\\}$, where
$\mathtt{Select}^{\overline{w}}$ denotes the set of all selection functions at
$\overline{w}$ (i.e., functions that assign to each $\alpha$ a member of
$\mathtt{Choice}^{\overline{w}}_{\alpha}$).

  * •

For all $\alpha\in Ags$, $\approx_{\alpha}$ is an (epistemic) equivalence
relation on $W$. The following conditions must be satisfied:

    * –

$\mathtt{(OAC)_{\mathtt{K}}}$ For all $\alpha\in Ags$, $w\in W$, and
$v\in\overline{w}$, $v\approx_{\alpha}u$ for every
$u\in\mathtt{Choice}^{\overline{w}}_{\alpha}(v)$.

    * –

$\mathtt{(Unif-H)_{\mathtt{K}}}$ For all $\alpha\in Ags$, if $v,u\in W$ are
such that $v\approx_{\alpha}u$, then for all $v^{\prime}\in\overline{v}$ there
exists $u^{\prime}\in\overline{u}$ such that
$v^{\prime}\approx_{\alpha}u^{\prime}$.

For $\alpha\in Ags$ and $w\in W$, $\alpha$’s __ex ante_ information set at
$w$_ is defined as
$\pi_{\alpha}^{\square}[w]:=\left\\{v;w\approx_{\alpha}\circ
R_{\square}v\right\\}$, which by frame condition
$(\mathtt{Unif-H})_{\mathtt{K}}$ coincides with the set
$\left\\{v;wR_{\square}\circ\approx_{\alpha}v\right\\}$. To clarify,
$(\mathtt{Unif-H})_{\mathtt{K}}$ implies that
$R_{\square}\circ\approx_{\alpha}=\approx_{\alpha}\circ R_{\square}$. Thus,
$\approx_{\alpha}\circ R_{\square}$ is an equivalence relation such that
$\pi_{\alpha}^{\square}[w]=\pi_{\alpha}^{\square}[v]$ for every $w,v\in W$
such that $w\approx_{\alpha}\circ R_{\square}v$.

  * •

For $\alpha\in Ags$, $R_{\alpha}^{I}$ is a serial, transitive, and euclidean
relation on $W$ such that $R_{\alpha}^{I}\subseteq\approx_{\alpha}\circ
R_{\square}$ and such that the following condition is satisfied:

    * –

$\mathtt{(Den)_{K}}$ For all $v,u\in W$ such that $v\approx_{\alpha}\circ
R_{\square}u$, there exists $z\in W$ such that $vR_{\alpha}^{I}z$ and
$uR_{\alpha}^{I}z$.

For $\alpha\in Ags$, $R_{\alpha}^{I+}$ denotes the reflexive closure of
$R_{\alpha}^{I}$. For $w\in W$, $w\uparrow_{R_{\alpha}^{I+}}$ denotes the set
$\left\\{v\in W;wR_{\alpha}^{I+}v\right\\}$.

For $w,v\in W$, I write $\overline{w}\approx_{\alpha}\overline{v}$ iff there
exist $w^{\prime}\in\overline{w}$ and $v^{\prime}\in\overline{v}$ such that
$w^{\prime}\approx_{\alpha}v^{\prime}$. For $w,v\in W$ such that
$\overline{w}\approx_{\alpha}\overline{v}$ and
$L\in\mathtt{Choice}^{\overline{w}}_{\alpha}$, $L$’s epistemic cluster at
$\overline{v}$ is the set
$\left[\\!\left[L\right]\\!\right]_{\alpha}^{\overline{v}}:=\left\\{u\in{\overline{v}};\mbox{
there is }o\in L\ \textnormal{ such that }\ o\approx_{\alpha}u\right\\}.$

  * •

$\mathtt{Value}_{\mathcal{O}}$ and $\mathtt{Value}_{\mathcal{S}}$ are
functions that independently assign to each world $w\in W$ a real number.

These functions are used to define an objective ordering $\preceq$ and a
subjective ordering $\preceq_{s}$ of choices. Formally, for $\alpha\in Ags$
and $w\in W$, one first defines two general orderings $\leq$ and $\leq_{s}$ on
$2^{W}$ by the rules: $X\leq Y$ iff
$\mathtt{Value}_{\mathcal{O}}(w)\leq\mathtt{Value}_{\mathcal{O}}(w^{\prime})$
for all $w\in X$ and $w^{\prime}\in Y$; and $X\leq_{s}Y$ iff
$\mathtt{Value}_{\mathcal{S}}(w)\leq\mathtt{Value}_{\mathcal{S}}(w^{\prime})$
for all $w\in X$ and $w^{\prime}\in Y$. An objective dominance ordering
$\preceq$ is then defined on $\mathtt{Choice}_{\alpha}^{\overline{w}}$ by the
rule: $L\preceq L^{\prime}$ iff $L\cap S\leq L^{\prime}\cap S$ for every
$S\in\mathtt{State}_{\alpha}^{\overline{w}}$. In turn, a subjective dominance
ordering $\preceq_{s}$ is then defined on
$\mathtt{Choice}_{\alpha}^{\overline{w}}$ by the rule:
$L\preceq_{s}L^{\prime}$ iff
$\left[\\!\left[L\right]\\!\right]^{\overline{v}}_{\alpha}\cap
S\leq_{s}\left[\\!\left[L^{\prime}\right]\\!\right]^{\overline{v}}_{\alpha}\cap
S$ for every $v$ such that $w\approx_{\alpha}v$ and every
$S\in\mathtt{State}_{\alpha}^{\overline{v}}$. I write $L\prec L^{\prime}$ iff
$L\preceq L^{\prime}$ and $L^{\prime}\npreceq L$, and I write
$L\prec_{s}L^{\prime}$ iff $L\preceq_{s}L^{\prime}$ and
$L^{\prime}\npreceq_{s}L$, so that
$\mathtt{Optimal}_{\alpha}^{\overline{w}}:=\left\\{L\in\mathtt{Choice}^{\overline{w}}_{\alpha};\textnormal{
there is no }L^{\prime}\in\mathtt{Choice}^{\overline{w}}_{\alpha}\textnormal{
s. t. }L\prec L^{\prime}\right\\}$ and
$\mathtt{SOptimal}_{\alpha}^{\overline{w}}:=\left\\{L\in\mathtt{Choice}^{\overline{w}}_{\alpha};\textnormal{
there is no }L^{\prime}\in\mathtt{Choice}^{\overline{w}}_{\alpha}\textnormal{
s. t. }L\prec_{s}L^{\prime}\right\\}$.

A Kripke-_kios_ -model $\mathcal{M}$ consists of the tuple that results from
adding a valuation function $\mathcal{V}$ to a Kripke-_kios_ -frame, where
$\mathcal{V}:P\to 2^{W}$ assigns to each atomic proposition a set of worlds
(recall that $P$ is the set of propositions in $\mathcal{L}_{\textsf{R}}$).

Kripke-_kios_ -models allow us to evaluate the formulas of
$\mathcal{L}_{\textsf{R}}$ with semantics that are analogous to the ones
provided for _kiobt_ -models:

######  Definition A.3 (Evaluation rules on Kripke models).

Let $\mathcal{M}$ be a Kripke-_kios_ -model, the semantics on $\mathcal{M}$
for the formulas of $\mathcal{L}_{\textsf{KO}}$ are defined recursively by the
following truth conditions, evaluated at world $w$:

$\begin{array}[]{lll}\mathcal{M},w\models p&\mbox{iff}&w\in\mathcal{V}(p)\\\
\mathcal{M},w\models\neg\phi&\mbox{iff}&\mathcal{M},w\not\models\phi\\\
\mathcal{M},w\models\phi\wedge\psi&\mbox{iff}&\mathcal{M},w\models\phi\mbox{
and }\mathcal{M},w\models\psi\\\
\mathcal{M},w\models\Box\phi&\mbox{iff}&\mbox{for each
}v\in\overline{w},\mathcal{M},v\models\phi\\\
\mathcal{M},w\models[\alpha]\phi&\mbox{iff}&\mbox{for each
}v\in\mathtt{Choice}^{\overline{w}}_{\alpha}(w),\mathcal{M},v\models\phi\\\
\mathcal{M},w\models K_{\alpha}\phi&\mbox{iff}&\mbox{for each }v\mbox{ s. t.
}w\approx_{\alpha}v,\mathcal{M},v\models\phi\\\ \mathcal{M},w\models
I_{\alpha}\phi&\mbox{ iff }&\mbox{there exists
}x\in\pi_{\alpha}^{\square}[w]\mbox{ s. t.
}x\uparrow_{R_{\alpha}^{I+}}\subseteq|\phi|\\\
\mathcal{M},w\models\odot_{\alpha}\varphi&\mbox{iff}&\mbox{for all
}L\in\mathtt{Choice}^{\overline{w}}_{\alpha}\mbox{ s. t.
}\mathcal{M},v\not\models\varphi\mbox{ for some }v\in L,\mbox{ there is}\\\
&&L^{\prime}\in\mathtt{Choice}_{\alpha}^{\overline{w}}\mbox{ s. t. }L\prec
L^{\prime}\mbox{ and, if }L^{\prime\prime}=L^{\prime}\mbox{ or
}L^{\prime}\preceq_{s}L^{\prime\prime},\\\ &&\mbox{then
}\mathcal{M},w^{\prime}\models\varphi\mbox{ for every }w^{\prime}\in
L^{\prime\prime}_{\alpha}\\\
\mathcal{M},w\models\odot^{\mathcal{S}}_{\alpha}\varphi&\mbox{iff}&\mbox{for
all }L\in\mathtt{Choice}^{\overline{w}}_{\alpha}\mbox{ s. t.
}\mathcal{M},v\not\models\varphi\mbox{ for some }w^{\prime}\mbox{ s. t.
}w\approx_{\alpha}w^{\prime}\\\ &&\mbox{and some
}v\in\left[\\!\left[L\right]\\!\right]^{w^{\prime}}_{\alpha},\mbox{ there is
}L^{\prime}\in\mathtt{Choice}_{\alpha}^{\overline{w}}\mbox{ s. t.
}L\prec_{s}L^{\prime}\\\ &&\mbox{and, if }L^{\prime\prime}=L^{\prime}\mbox{ or
}L^{\prime}\preceq_{s}L^{\prime\prime},\mbox{then
}\mathcal{M},w^{\prime\prime\prime}\models\varphi\mbox{ for every
}w^{\prime\prime}\\\ &&\mbox{s. t.
}\overline{w}\approx_{\alpha}\overline{w^{\prime\prime}}\mbox{ and every
}w^{\prime\prime\prime}\in\left[\\!\left[L^{\prime\prime}\right]\\!\right]^{w^{\prime\prime}}_{\alpha},\end{array}$

where I write $|\phi|$ to refer to the set $\left\\{w\in
W;\mathcal{M},w\models\phi\right\\}$. Satisfiability, validity on a frame, and
general validity are defined as usual.

A truth-preserving correspondence between Kripke-_kios_ -models and _kiobt_
-models is shown as follows:

######  Definition A.4 (Associated _kiobt_ -frame).

Let

$\mathcal{F}=\left\langle
W,Ags,R_{\square},\mathtt{Choice},\left\\{\mathtt{\approx}_{\alpha}\right\\}_{\alpha\in
Ags},\left\\{R_{\alpha}^{I}\right\\}_{\alpha\in
Ags},\mathtt{Value}_{\mathcal{O}},\mathtt{Value}_{\mathcal{S}}\right\rangle$

be a bi-valued Kripke-_kios_ -frame.

Then $\mathcal{F}^{T}:=\left\langle
M_{W},\sqsubset,Ags,\mathbf{Choice},\left\\{\sim_{\alpha}\right\\}_{\alpha\in
Ags},\tau,\mathbf{Value}_{\mathcal{O}},\mathbf{Value}_{\mathcal{S}}\right\rangle$
is called the bi-valued _kiobt_ -frame associated with $\mathcal{F}$ iff

  * •

$M_{W},\sqsubset,\mathbf{Choice}$, $\left\\{\sim_{\alpha}\right\\}_{\alpha\in
Ags}$, and $\tau$ are defined just as in Definition 11 in [4].

  * •

$\mathbf{Value}_{\mathcal{O}}$ and $\mathbf{Value}_{\mathcal{S}}$ are defined
by the following rules: for $h_{v}\in H$,
$\mathbf{Value}_{\mathcal{O}}(h_{v})=\mathtt{Value}_{\mathcal{O}}(v)$, and
$\mathbf{Value}_{\mathcal{S}}(h_{v})=\mathtt{Value}_{\mathcal{S}}(v)$.

######  Proposition A.5.

Let $\mathcal{F}$ be a bi-valued Kripke-_kios_ -frame. Then $\mathcal{F}^{T}$
is a bi-valued _kiobt_ -frame, indeed.

###### Proof.

Follows from Proposition 2 in [4] and Definition A.4. ∎

######  Lemma A.6.

Let $\mathcal{M}$ be a bi-valued Kripke-_kios_ -model, and let
$\mathcal{M}^{T}$ be its associated bi-valued _kiobt_ -model. For all
$\alpha\in Ags$, $w\in W$, and
$L,N\in\mathtt{Choice}^{\overline{w}}_{\alpha}$, the following conditions
hold:

  1. (a)

$L\preceq N$ iff $L^{T}\preceq N^{T}$ and $L\prec N$ iff $L^{T}\prec N^{T}$.

  2. (b)

$L\preceq_{s}N$ iff $L^{T}\preceq_{s}N^{T}$ and $L\prec_{s}N$ iff
$L^{T}\prec_{s}N^{T}$.

  3. (c)

$L\in\mathtt{Optimal}^{\overline{w}}_{\alpha}$ iff
$L^{T}\in\mathbf{Optimal}^{\overline{w}}_{\alpha}$.

  4. (d)

$L\in\mathtt{S-Optimal}^{\overline{w}}_{\alpha}$ iff
$L^{T}\in\mathbf{S-Optimal}^{\overline{w}}_{\alpha}$.

###### Proof.

The reader is referred to the proof of Proposition 4 in
https://doi.org/10.48550/arXiv.1903.10577 for a proof. ∎

######  Proposition A.7 (Truth-preserving correspondence).

Let $\mathcal{M}$ be a bi-valued Kripke-_kios_ -model, and let
$\mathcal{M}^{T}$ be its associated bi-valued _kiobt_ -model. For all $\phi$
of $\mathcal{L}_{\textsf{R}}$ and $w\in W$, $\mathcal{M},w\models\phi$ iff
$\mathcal{M}^{T},\left\langle\overline{w},h_{w}\right\rangle\models\phi$.

###### Proof.

We proceed by induction on the complexity of $\phi$. For the base case, the
cases of Boolean connectives, and the cases of all modal operators except
$I_{\alpha}$, the proofs are exactly the same as their analogs’ in Proposition
4 in https://doi.org/10.48550/arXiv.1903.10577. For the case of $I_{\alpha}$,
the proof is the same as its analog in Proposition 3 in [4].

∎

Thus, completeness with respect to bi-valued _kiobt_ -models is proved with
Propositions A.8 and A.9 below.

######  Proposition A.8 (Completeness w.r.t. bi-valued Kripke-_kios_ -models).

The proof system ${\Lambda_{R}}$’ is complete with respect to the class of bi-
valued Kripke-_kios_ -models.

###### Proof.

Completeness with respect to bi-valued Kripke-_kios_ -models is shown via
canonical models. To be precise, one defines a structure
$\mathcal{M}:=\left\langle
W^{\Lambda_{R}^{\prime}},R_{\square},\mathtt{Choice},\left\\{\mathtt{\approx}_{\alpha}\right\\}_{\alpha\in
Ags},\left\\{R_{\alpha}^{I}\right\\}_{\alpha\in
Ags}\mathtt{Value}_{\mathcal{O}},\mathtt{Value}_{\mathcal{S}},\mathcal{V}\right\rangle$,
where $W^{\Lambda_{R}^{\prime}}=\left\\{w;w\mbox{ is a
}{\Lambda_{R}^{\prime}}\textnormal{-MCS}\right\\}$, where
$R_{\square},\mathtt{Choice},\left\\{\mathtt{\approx}_{\alpha}\right\\}_{\alpha\in
Ags}$, $\left\\{R_{\alpha}^{I}\right\\}_{\alpha\in Ags}$, and $\mathcal{V}$
are defined just as in Definition 12 in [4], and where
$\mathtt{Value}_{\mathcal{O}}$ and $\mathtt{Value}_{\mathcal{S}}$ are defined
as follows: for $\alpha\in Ags$ and $w\in W^{\Lambda}$, one first defines
$\Sigma_{\alpha}^{w}:=\\{[\alpha]\phi;\odot[\alpha]\phi\in w\\}$ and
$\Gamma_{\alpha}^{w}:=\\{K_{\alpha}\phi;\odot_{\mathcal{S}}[\alpha]\phi\in
w\\}$. Then, taking $\Sigma^{w}=\bigcup_{\alpha\in Ags}\Sigma_{\alpha}^{w}$
and $\Gamma^{w}=\bigcup_{\alpha\in Ags}$, the deontic functions are given by

$\begin{array}[]{ll}\mathtt{Value}_{\mathcal{O}}(w)&=\left\\{\begin{array}[]{lll}1\mbox{
iff }\Sigma^{w}\subseteq w,&\\\ 0\mbox{ otherwise}.&\end{array}\right.\\\
\mathtt{Value}_{\mathcal{S}}(w)&=\left\\{\begin{array}[]{lll}1\mbox{ iff
}\Gamma^{w}\subseteq w,&\\\ 0\mbox{ otherwise}.&\end{array}\right.\\\
\end{array}$

The canonical structure $\mathcal{M}$ is shown to be a bi-valued Kripke-_kios_
-model just as in Proposition 4 in [4]. Then, the so-called _truth lemma_ is
shown by merging Lemma 2 in [4] and Lemma 4 in
https://doi.org/10.48550/arXiv.1903.10577. This renders completeness with
respect to bi-valued Kripke-_kios_ -models. ∎

######  Proposition A.9 (Completeness w.r.t. bi-valued _kiobt_ -models).

The proof system ${\Lambda_{R}}$’ is complete with respect to the class of bi-
valued _kiobt_ -models.

###### Proof.

Let $\phi$ be a ${\Lambda_{R}^{\prime}}$-consistent formula of
$\mathcal{L}_{\textsf{R}}$. Proposition A.8 implies that there exists a bi-
valued Kripke-_kios_ -model $\mathcal{M}$ and a world $w$ in its domain such
that $\mathcal{M},w\models\phi$. Proposition A.7 then ensures that the bi-
valued _kiobt_ -model $\mathcal{M}^{T}$ associated with $\mathcal{M}$ is such
that $\mathcal{M}^{T},\left\langle\overline{w},h_{w}\right\rangle\models\phi$.
∎

Therefore, Proposition A.1 and Proposition A.9 imply that the following
result, appearing in the main body of the paper, is true:

See 4.4