# Neighbourhood semantics and axioms for strategic fragment of classical stit
logic

Daniil Khaitovich  International Laboratory for Logic, Linguistics and Formal
Philosophy, HSE
Moscow, Russia

###### Abstract

STIT (sees to it that) semantics is one of the most prominent tools in modal
logic of agency, widely used among both philosophers and responsible AI
scholars. STIT logic surveys the properties of agents seeing to it that some
state of affairs holds without specifying concrete actions by which that state
of affairs is guaranteed. In comparison with other multi-agent modal logics,
the main advantage of STIT theories is expressive power. STIT logic allows to
study not only statements about agents’ abilities to perform certain actions
(as it is in variations of Coalition Logic or Propositional Dynamic Logic),
but about what choices they make and what they de-facto achieve as well.

Nevertheless, in some occasions such expressivity may be redundant. This paper
surveys a specific fragment of classical STIT logic, which has only strategic
modal operator $[i]\phi$, what stands for the fact that agent $i$ has an
ability to see to it that $\phi$ holds. The neighbourhood semantics for the
fragment is presented, accompanied with the soundness, canoniciy hence strong
completeness results. Furthermore, the paper presents basic considerations on
epistemic extension of the presented fragment.

###### keywords:

Modal logic, stit logic, neighbourhood semantics.

<EMAIL_ADDRESS>
##  1 Introduction

The stit (abbreviation for “sees to it that”) theory is one of the most
prominent modal theories of agency. In stit framework, actions of individuals
are studied via sentences of the form “agent $i$ sees to it that $\phi$
holds”, where the syntactic construction “agent $i$ sees to it that” is
treated as a modality $[i:stit]$ (we will use a simpler notation:
$[stit]_{i}$). Stit grows out from a tradition of modal theories of
agency222Detailed overview of the stit prehistory could be found in [12] and
originated from a series of seminal articles by Belnap, Perloff and Xu [2].

In classical stit theory, agent’s power to see to it that some state of
affairs holds is called a causal ability. The notion ignores any mental
attitudes, such as desirability, awareness or purposefulness of the potential
action. Casual ability is formalized via a bimodal formula
$\Diamond[stit]_{i}\phi$, i.e. it is possible that agent $i$ sees to it that
$\phi$ obtains. Besides the causal abilities, stit theorists study epistemic
abilities, i.e. agent’s power to knowingly see to it that $\phi$. The
discussion on epistemic abilities and their logical form is still open: Horty
and Pacuit propose to treat epistemic abilities via action types and to
introduce a new modal operator $[kstit]_{i}\phi$, what reads as “agent $i$
executes an action type that she knows to guarantee the truth of $\phi$”:

> If the epistemic sense of ability requires that some single action must be
> known by $i$ to guarantee the truth of $\phi$, then this must be the action
> type, not one of its various tokens [8].

While Broersen argue that epistemic ability may be presented simply by adding
knowledge operator $K_{i}\phi$, which satisfies its standard definition from
modal epistemic logic. In that case, epistemic ability may be represented as
$\Diamond K_{i}[stit]_{i}\phi$ – it is possible that agent $i$ knows that she
sees to it that $\phi$ [3].

In the paper, we study causal ability as a single monotonic modal operator. In
order to present its axiomatisation, we translate standard stit semantics to
neighbourhood one and prove correctness and strong completeness w.r.t. a
specific class of neighbourhood frames. We show that the mentioned class is
modally invariant with BT+AC frames for strandard stit logic. At the end of
the paper, some general considerations on getting the same result for
epistemic abilities are presented.

##  2 Basic theory of sees to it that

The language of ”classical” stit logic $\mathbf{L}_{cstit}$ is defined as
follows. For a countable set of propositional variables
$Var=\\{p_{1},p_{2},\ldots\\}$ and a finite set of agents
$Ags=\\{i_{1},i_{2},\ldots,i_{n}\\}$:

$\phi:=p\>|\>\neg\phi\>|\>\phi\lor\phi\>|\>\Box\phi\>|\>[stit]_{i}\phi$

where $p\in Var,i\in Ags$. Atomic propositions and Boolean connectives have
their standard meaning.

Sees to it that semantics is built upon a branching time structures of the
form $\langle Tree,<\rangle$, where $Tree=\\{m_{1},m_{2},\ldots\\}$ is a non-
empty set of moments and $<$ is a strict partial order on $Tree$, satisfying
backward linearity constraint, i.e. for any $m_{1},m_{2},m_{3}\in Tree$, if
$m_{2}<m_{1}$ ($m_{1}$ is preceded by $m_{2}$) and $m_{3}<m_{1}$, then either
$m_{3}<m_{2}$ or $m_{2}<m_{3}$ or $m_{3}=m_{2}$. It is worth noticing that the
constraint works only for predecessors: it is totally possible that for some
$m_{1},m_{2},m_{3}\in Tree$: $m_{2}<m_{1}$ and $m_{2}<m_{3}$, but $m_{3}$ and
$m_{1}$ are not $<$-comparable at all.

A maximal set of linearly $<$-ordered moments is a history. Each history
represents one of the possible complete courses of events in the world.
Formally speaking, the set of histories is defined as

$\begin{split}H=\\{h\subseteq Tree\>|\>\forall m_{1},m_{2}\in
h(m_{1}<m_{2}\lor m_{2}<m_{1}\lor m_{1}=m_{2})\land\\\ \forall m_{3}\not\in
h\exists m_{4}\in h(\neg(m_{4}<m_{3}\lor m_{3}<m_{4}\lor
m_{4}=m_{3}))\\}\end{split}$

If some moment $m$ occurs somewhere throughout the history $h$, it can be said
that $h$ passing through $m$. The set of histories passing through $m$ is
denoted as $H_{m}$. Moment/history pair of the form $m/h$, such that $h\in
H_{m}$, is usually called an index.

######  Definition 2.1.

A branching time (BT) frame is a tuple

$\mathcal{F}=\langle Tree,<\rangle$

where $Tree$ is a non-empty set of moments and $<$ is a strict partial
ordering on $Tree$, satisfying the backward linearity condition. BT frame is
extended to a BT model:

$\mathcal{M}=\langle Tree,<,\nu\rangle$

where $\nu:Var\rightarrow 2^{Tree\times H}$ is an evaluation function, mapping
each propositional variable to a set of indices, in which the proposition is
satisfied.

In stit theories, agency is understood as an agents’ ability to restrict the
set of possible histories to a specific subset. I.e., agent i sees to it that
$\phi$ at some moment $m$ means that agent $i$ determines that the world will
evolve according to one of the histories, satisfying $\phi$ at the moment $m$.

In order to formalize that intuition, BT models should be extended with the
finite set of agents $Ags=\\{i_{1},i_{2},\ldots,i_{n}\\}$ and with a specific
function $Choice$, mapping each agent $i$ and moment $m$ into a partition
$Choice^{m}_{i}$ of $H_{m}$. Each element of that partition, $X\in
Choice^{m}_{i}$, represents a set of possible outcomes of $i$’s specific
action at $m$. Respectively, $Choice^{m}_{i}$ is a collection of such sets.
For the sake of simplicity, $X\in Choice^{m}_{i}$, such that $h\in X$, is
denoted as $Choice^{m}_{i}(h)$.

It is important to state that $Choice$ function enjoys the property called
independence of agents. For all $a,b\in Ags,m\in Tree$: $X\in
Choice^{m}_{a}\land Y\in Choice^{m}_{b}\rightarrow X\cap Y\neq\emptyset$ for
any $X,Y\subseteq 2^{H}$. Informally, the property means that every set of
agents’ choices is consistent: there is no way any agent could execute an
action, which would deprive other agents of any choices available for them.

######  Definition 2.2.

BT+AC model

BT+AC model is defined as a tuple

$\mathcal{M}=\langle Tree,<,Ags,Choice,\nu\rangle$

which is BT model extended with a set of agents $Ags$ and $Choice$ function
defined as above.

######  Definition 2.3.

$\mathbf{L}_{cstit}$ semantics

$\mathcal{M},m/h\models p\Leftrightarrow p\in\nu(p)$
$\mathcal{M},m/h\models\neg\phi\Leftrightarrow\mathcal{M},m/h\not\models\phi$
$\mathcal{M},m/h\models\phi\lor\psi\Leftrightarrow\mathcal{M},m/h\models\phi\mbox{
or }\mathcal{M},m/h\models\psi$
$\mathcal{M},m/h\models\Box\phi\Leftrightarrow\forall h^{\prime}\in
H_{m}(\mathcal{M},m/h^{\prime}\models\phi)$
$\mathcal{M},m/h\models[stit]_{i}\phi\Leftrightarrow\forall h^{\prime}\in
Choice^{m}_{i}(h)(\mathcal{M},m/h^{\prime}\models\phi)$

##  3 Translating stit semantics to neighbourhood semantics: strategic case

In this section the strategic fragment of $\mathbf{L}_{cstit}$ is surveyed.
The fragment is obtained by abandonment of $[stit]_{i}\phi$ formulas, allowing
only statements about agents’ abilities. Such statements are treated by a
strategic stit modality: $[i]\phi$ stands here for agent $i$ has an ability to
achieve $\phi$. Strategic stit modality $[i]$ may be seen as an abbreviation
for $\Diamond[stit]_{i}$. The equivalence of such expressions is shown in the
section as well. In order to present strategic stit fragment and its
axiomatisation, the classical Krpke semantics for $\mathbf{L}_{cstit}$ is
changed to neighbourhood semantics, since $[i]$ operator loses normality333the
seminal paper showing why normal moda logic is inadequate for ability: [9]. It
is not hard to notice that $Choice$ function works similarly with
neighbourhood functions for classical modal logic: it takes an index and
returns a collection of subsets of indices [13].

Another feature worth being observed is redundancy of the main branching time
frame component, strict partial order on the set of moments: in
$\mathbf{L}_{cstit}$ there is no formula, whose semantics somehow mentions $<$
relation. To conclude, standard stit model, as it is presented in [8], may be
redefined as atemporal and neighbourhood one. It simplifies the task of
providing logic, complete w.r.t. corresponding class of frames.

###  3.1 Neighbourhood stit: one-shot games and strategic abilities

The one-shot strategic stit logic’s language $\mathbf{L}_{osstit}$ is defined
as follows:

$\phi:=p\>|\>\neg\phi\>|\>\phi\lor\phi\>|\>\Box\phi\>|\>[i]\phi\>|\>[\exists_{i}]\phi$

where $p\in Var,i\in Ags$. $[i]\phi$ stands for “agent $i$ is able to see to
it that $\phi$” (what intuitively corresponds to $\Diamond[stit]_{i}\phi$ in
classical stit), $\langle\exists_{i}\rangle\phi$ – “agent $i$ is able to
execute an action, which does not prevent $\phi$ ” (or “agent $i$ could not
prevent $\phi$ ” for $[\exists_{i}]\phi$), what may be seen as
$\Diamond\neg[stit]\neg\phi$ equivalent. Historical necessity modality, as
well as Boolean connectives, have their standard meanings. Dual of every modal
operator is defined standardly as well.

It is possible to consider a one-shot model, i.e. a model for a set of agents
simultaneously taking some actions at the unique moment.

######  Definition 3.1.

One-shot strategic stit (osstit) frames

$\mathcal{F}=\langle W,\\{Choice_{i}\\}_{i\in Ags}\rangle$

  * •

$W=\\{w_{1},w_{2},\ldots\\}$ is a non-empty set of states. It is suitable to
think of $W$ as a set of historically accessible indices, i.e.
$\\{m/h\>|\>h\in H_{m}\\}$ for a unique moment $m$.

  * •

$Choice_{i}:W\rightarrow 2^{2^{W}}$ is a neighbourhood function, defined for
every agent. $Choice_{i}(w)$ is a set of possible outcomes of $i$’s actions,
available for her at $w$.

    * –

Every function $Choice_{i}$ is monotonic (closed under supersets), does not
contain an empty set and contains $W$ itself, i.e. for all $i\in Ags,w\in W$:
$\emptyset\not\in Choice_{i}(w),W\in Choice_{i}(w)$.

    * –

$Choice_{i}\downharpoonright(w)$ denotes a non-monotonic core of neighbourhood
$Choice_{i}(w)$. The non-monotonic core is a set of neighbourhoods, which are
not supersets for any other neighbourhoods:
$Choice_{i}\downharpoonright(w)=\\{X\>|\>X\in Choice_{i}(w)\land\neg\exists
Y\in Choice_{i}(w)(Y\subseteq X)\\}$. $Choice_{i}\downharpoonright(w)$
represents all proper actions, available for $i$ at $w$, without redundant
weaker ones. It should be noted that non-monotonic core enjoys the next
property (un): $\bigcup Choice_{i}\downharpoonright(w)=W$. Informally, it says
that there is no historically possible state, which could not be an outcome of
some proper action of an agent.

    * –

Another crucial property is independence of agents (ind): for all $a,b\in
Ags$, $X,Y\subseteq W$, $w\in W$ : $X\in Choice_{a}(w)\land Y\in
Choice_{b}(w)\rightarrow X\cap Y\neq\emptyset$. Or, interchangeably, $X\in
Choice_{a}(w)\rightarrow W\setminus X\not\in Choice_{b}(w)$. The property
states that every choice of actions is consistent: there is no way for one
agent to take an action, such that another agent would be deprived of some of
her choices.

    * –

Agents’ abilities are historically necessary, i.e. neighbourhoods stay the
same over all states (nec): $\forall w,w^{\prime}\in W\forall X\subseteq
W:X\in Choice_{i}(w)\rightarrow X\in Choice_{i}(w^{\prime})$ for any agent
$i\in Ags$.

The one-shot strategic stit model $\mathcal{M}=\langle\mathcal{F},V\rangle$
extends osstit frame with a standard evaluation function $V:Var\rightarrow
2^{W}$.

######  Definition 3.2.

Neighbourhood strategic stit semantics

$\mathcal{M},w\models p\Leftrightarrow w\in V(p)$
$\mathcal{M},w\models\neg\phi\Leftrightarrow\mathcal{M},w\not\models\phi$
$\mathcal{M},w\models\phi\lor\psi\Leftrightarrow\mathcal{M},w\models\phi\mbox{
or }\mathcal{M},w\models\psi$
$\mathcal{M},w\models\Box\phi\Leftrightarrow\forall w^{\prime}\in
W(\mathcal{M},w^{\prime}\models\phi)$
$\mathcal{M},w\models[i]\phi\Leftrightarrow\llbracket\phi\rrbracket\in
Choice_{i}(w)$
$\mathcal{M},w\models[\exists_{i}]\phi\Leftrightarrow\forall X\in
Choice_{i}\downharpoonright(w)\forall w^{\prime}\in
X(\mathcal{M},w^{\prime}\models\phi)$

As usual, $\llbracket\phi\rrbracket$ abbreviates $\\{w\in
W\>|\>\mathcal{M},w\models\phi\\}$. The reader may observe that the following
definition for $[i]\phi$ is equivalent to the given above:

$\mathcal{M},w\models[i]\phi\Leftrightarrow\exists X\in
Choice_{i}\downharpoonright(w)(X\subseteq\llbracket\phi\rrbracket)$

The equivalence of the definitions immediately follows from $Choice_{i}(w)$
being monotonic. As for the $[\exists_{i}]\phi$, it can be redefined as a
normal modal operator. Consider a binary relation $R_{i}=(\bigcup
Choice_{i}\downharpoonright(w))^{2}$, where $w$ is arbitrary, since
$Choice_{i}\downharpoonright(w)$ be the same for all $w\in W$, what follows
from $(nec)$ property. $R_{i}$ is an equivalence relation, connecting all
elements of $i$’s neighbourhoods from non-monotonic core. Then,

$\mathcal{M},w\models[\exists_{i}]\phi\Leftrightarrow\forall w^{\prime}\in
W(wR_{i}w^{\prime}\rightarrow\mathcal{M},w^{\prime}\models\phi)$

The validity of the given definition can be simply verified.

(PL) | All tautologies of classical propositional logic
---|---
(S5$\Box$) | S5 for $\Box$ modality
(S5$[i]$) | MCT4’B logic for $[\exists_{i}]$
(Incl) | $\Box\phi\rightarrow[i]\phi$
(M) | $[i](\phi\land\psi)\rightarrow([i]\phi\land[i]\psi)$
(N) | $[i]\top$
(D) | $\neg[i]\bot$
(Pos) | $\Box\phi\equiv[\exists_{i}]\phi$
(Nec-A) | $[i]\phi\rightarrow\Box[i]\phi$
(Ind) | $[1]\phi_{1}\land[2]\phi_{2}\land\ldots\land[n]\phi_{n}\rightarrow\Diamond(\phi_{1}\land\phi_{2}\land\ldots\land\phi_{n})$
(RE) | From $\phi\equiv\psi$, infer $[i]\phi\equiv[i]\psi$
(MP) | From $\phi,\phi\rightarrow\psi$, infer $\psi$
Table 1: Axioms for $\mathcal{L}_{osstit}$

Notice that $\Box$ operator can be viewed as a special case of strategic sees
to it that modality, namely, $[\emptyset]$. On semantic level, it could be
defined via a special neighbourhood function $Choice_{\emptyset}$, such that
$Choice_{\emptyset}:w\mapsto\\{\\{W\\}\\}$ for all $w\in W$. In some occasions
it is more suitable to treat $\Box$ as the special case of non-normal
modality, while usually it is addressed as an universal S5 modality.

###  3.2 Axioms for $\mathcal{L}_{osstit}$

######  Theorem 3.3 (Soundness and definability).

Recall that the following three properties hold for one-shot strategic stit
frames:

  * •

(ind) $\forall w\in W\forall X,Y\subseteq W:X\in Choice_{a}(w)\land Y\in
Choice_{b}(w)\rightarrow X\cap Y\neq\emptyset$

  * •

(nec) $\forall w,w^{\prime}\in W\forall X\subseteq W:X\in
Choice_{i}(w)\rightarrow X\in Choice_{i}(w^{\prime})$

  * •

(un) $\bigcup Choice_{i}\downharpoonright(w)=W$

$\mathcal{F}\models[a]\phi\land[b]\psi\rightarrow\Diamond(\phi\land\psi)\Leftrightarrow\mathcal{F}\models(ind)$

######  Proof 3.4.

Left to right – immediately follows from the semantics. Right to left: assume
$\mathcal{F}\not\models(ind)$, i.e. $\exists w\in W\exists X,Y\subseteq W:X\in
Choice_{a}(w)\land Y\in Choice_{b}(w)\land X\cap Y=\emptyset$. Let $V$ be an
evaluation such that $\llbracket\phi\rrbracket=X,\llbracket\psi\rrbracket=Y$.
Consequently, $\llbracket\phi\rrbracket\in
Choice_{a}(w),\llbracket\psi\rrbracket\in Choice_{b}(w)$. By semantic
definition of $[a]\mbox{ and }[b]$,
$\langle\mathcal{F},V\rangle,w\models[a]\phi\land[b]\psi$. Since $X\cap
Y=\emptyset,\llbracket\phi\rrbracket\cap\llbracket\psi\rrbracket=\emptyset$,
i.e. $\langle\mathcal{F},V\rangle\not\models\phi\land\psi$. It follows that
$\langle\mathcal{F},V\rangle,w\models[a]\phi\land[b]\psi\land\neg\Diamond(\phi\land\psi)$
and hence
$\mathcal{F}\not\models[a]\phi\land[b]\psi\rightarrow\Diamond(\phi\land\psi)$.

$\mathcal{F}\models[i]\phi\rightarrow\Box[i]\phi\Leftrightarrow\mathcal{F}\models(nec)$

######  Proof 3.5.

Left to right – immediately follows from the semantics. Right to left: assume
$\mathcal{F}\not\models(nec)$, i.e. $\exists w,w^{\prime}\in W\exists
X\subseteq W:X\in Choice_{i}(w)\land X\not\in Choice_{i}(w^{\prime})$. Let $V$
be a valuation such that $\llbracket\phi\rrbracket=X$. Then,
$\llbracket\phi\rrbracket\in Choice_{i}(w)$ and
$\llbracket\phi\rrbracket\not\in Choice_{i}(w^{\prime})$. By semantics of
$[i]$, $\langle\mathcal{F},V\rangle,w\models[i]\phi$ and
$\langle\mathcal{F},V\rangle,w^{\prime}\not\models[i]\phi$. Since $\Box$ is an
universal modality and there is $w^{\prime}\in W$, not satisfying $[i]\phi$,
we can conclude that $\langle\mathcal{F},V\rangle,w\models\neg\Box[i]\phi$,
i.e. $\langle\mathcal{F},V\rangle,w\models[i]\phi\land\neg\Box[i]\phi$, hence,
$\mathcal{F}\not\models[i]\phi\rightarrow\Box[i]\phi$.

$\mathcal{F}\models\Box\phi\equiv[\exists_{i}]\phi\Leftrightarrow\mathcal{F}\models(un)$

######  Proof 3.6.

Left to right – immediately follows from the semantics. Right to left: Suppose
$\mathcal{F}\not\models(un)$, i.e. $\bigcup Choice_{i}\downharpoonright(w)\neq
W$. The only way that could be true is $\bigcup
Choice_{i}\downharpoonright(w)\subset W$, since every neighbourhood is a
collection of subsets of $W$, consequently, $\bigcup
Choice_{i}\downharpoonright(w)\setminus W=\emptyset$. Let $V$ be a valuation
function such that $\bigcup
Choice_{i}\downharpoonright(w)=\llbracket\phi\rrbracket$. Notice that
$[\exists_{i}]\phi$ is true at $w$ iff $\bigcup
Choice_{i}\downharpoonright(w)\subseteq\llbracket\phi\rrbracket$ by definition
of $[\exists_{i}]\phi$. Hence,
$\langle\mathcal{F},V\rangle,w\models[\exists_{i}]\phi$. By hypothesis,
$W\setminus\bigcup Choice_{i}\downharpoonright(w)$ is not empty, then
$\llbracket\neg\phi\rrbracket\neq\emptyset$ as well, hence
$\langle\mathcal{F},V\rangle\models\neg\Box\phi$. Finally,
$\langle\mathcal{F},V\rangle,w\models[\exists_{i}]\phi\land\neg\Box\phi$, from
which it follows that $\mathcal{F}\not\models\Box\phi\equiv[\exists_{i}]\phi$

Cases for (M), (N), (D), (RE): standard definability results for monotonic
neighbourhood frames such that every neighbourhood contains $W$ and does not
contain $\emptyset$ [6]. (S5) and (Incl) cases: well-established result for
modal logic with universal modality [5].

######  Theorem 3.7 (Completeness).

Let $\mathbf{C}$ be a class of all osstit frames, corresponding to Definition
7.Let $\mathbf{C}\models\phi$ stand for $\mathcal{F}\models\phi$ for every
$\mathcal{F}\in\mathbf{C}$. As usual, $\Sigma\models_{\mathbf{C}}\phi$ means
that $\phi$ is a semantic consequence of some set of formulas $\Sigma$ in all
$\mathbf{C}$-frames. Then, for arbitrary
$\Gamma\subseteq\mathbf{L}_{osstit},\phi\in\mathbf{L}_{osstit}$, the following
holds:

$\Gamma\models_{\mathbf{C}}\phi\Leftrightarrow\Gamma\vdash_{\mathcal{L}_{osstit}}\phi$

######  Proof 3.8.

See Appendix.

###  3.3 Modal invariance of C and BT+AC frames

It is important to notice that $Choice_{i}\downharpoonright$ function lacks
one crucial feature, which BT+AC $Choice$ function enjoys: while $Choice$
returns a partition of $H_{m}$, $Choice_{i}\downharpoonright$ does not
partition $W$. It is easy to find the exact property of partition, which
$Choice_{i}\downharpoonright$ lacks. A collection of subsets $P\subseteq
2^{W}$ is a partition iff

  1. (1)

$\emptyset\not\in P$

  2. (2)

$\bigcup P=W$

  3. (3)

$\forall X,Y\in P:X\cap Y=\emptyset$

While the first two properties are met by definition of osstit frames, the
third one is failed. Nevertheless, it is not modally definable: if a class of
monotonic neighbourhood frames is modally definable, then it is closed under
disjoint unions, generated submodels, bounded morphic images and ultrafilter
extensions [6]. It is not the case for such class, where a non-monotonic cores
are partitions of the frame’s domain. Let a subclass of C-frames, enjoying a
property (iii) on its non-monotonic cores, be denoted as $\mathbf{P}$.

######  Theorem 3.9.

$\mathbf{P}$ is not modally definable

######  Proof 3.10.

Let $F_{1}^{c}=\langle W_{1},N_{1}^{c}\rangle$ and $F_{2}^{c}=\langle
W_{2},N_{2}^{c}\rangle$ be a non-monotonic cores of two monotonic
neighbourhood frames $F_{1}$ and $F_{2}$.

  1. (1)

$W_{1}=\\{w_{1},w_{2},w_{3},w_{4}\\},N^{c}_{1}(w_{1})=\\{\\{w_{1},w_{2}\\},\\{w_{3},w_{4}\\}\\}$
and for all other worlds, namely, $w_{2},\ldots,w_{4}$,
$N^{c}_{\emptyset}=N^{c}_{1}(w)=\\{W^{c}_{1}\\}$. Obviously,
$F_{1}\in\mathbf{P}$

  2. (2)

$W_{2}=\\{w_{1},w_{2},w_{3}\\},N^{c}_{2}(w_{1})=\\{\\{w_{1},w_{2}\\},\\{w_{2},w_{3}\\}\\}$
and for all other worlds, namely, $w_{2},\ldots,w_{4}$,
$N^{c}_{\emptyset}=N^{c}_{2}(w)=\\{W^{c}_{2}\\}$. It is not hard to see that
$F_{2}\not\in\mathbf{P}$, since $\\{w_{1},w_{2}\\}$, $\\{w_{2},w_{3}\\}\in
N^{c}_{2}(w)$ and $\\{w_{1},w_{2}\\}\cap\\{w_{2},w_{3}\\}\neq\emptyset$

  3. (3)

Let $f:W_{1}^{c}\rightarrow W^{c}_{2}$ be a function, such that

$\displaystyle f:w_{1}$ $\displaystyle\mapsto w_{1}$ $\displaystyle f:w_{2}$
$\displaystyle\mapsto w_{2}$ $\displaystyle f:w_{3}$ $\displaystyle\mapsto
w_{3}$ $\displaystyle f:w_{4}$ $\displaystyle\mapsto w_{2}$

  4. (4)

$f$ is a surjective bounded core morphism from $F_{1}$ to $F_{2}$. For all
$w\in W_{1}$:

    1. (a)

If $X\in N^{c}_{1}(w)$, then $f[X]\in N^{c}_{2}(f(w))$

    2. (b)

If $Y\in N^{c}_{2}(f(w))$, then there is an $X\subseteq W_{1}$, such that
$f[X]=Y$ and $X\in N^{c}_{1}(w)$

As it was noted before, $F_{1}\in\mathbf{P},F_{2}\not\in\mathbf{P}$ and
$F_{2}$ is a bounded morphic image of $F_{1}$. Consequently, $\mathbf{P}$ is
not closed under bounded morphic images and hence not modally definable.

######  Proposition 3.11.

$\mathcal{L}_{osstit}$ is sound and strongly complete w.r.t. a class of Kripke
frames, modally invariant with BT+AC.

One more important fact is that the non-monotonic core of $\mathbf{P}$-frames
may be seen as one-shot classical stit frames, i.e.

$\langle\mathbf{m},Ags,Choice,\nu\rangle$

where $\mathbf{m}=\\{m/h\>|\>m\in Tree,h\in H_{m}\\}$ and $Choice$ is a set of
$N^{c}$-functions, indexed by elements of $Ags$. In these models, the semantic
definition for ability is

$\mathcal{M},m/h\models\Diamond[cstit]_{i}\phi\Leftrightarrow\exists X\in
Choice^{m}_{i}:X\subseteq\llbracket\phi\rrbracket))$

which is equivalent to non-monotonic core version of $[i]\phi$ definition in
$\mathbf{C}$-frames. As it was showed above, $\mathbf{P}$ differs from
$\mathbf{C}$ with the only property, which is modally undefinable. Hence,
$\mathcal{L}_{osstit}$ is sound and strongly complete w.r.t.
$\mathbf{P}$-frames as well.

As it was noted in [1], BT+AC frames could be replaced by standard Kripke
frames without loss of modal invariance. The class of such Kripke frames is
nothing but a disjoint union of $\mathbf{P}$ frames, where indices are treated
as possible states. From the basic modal logic theory it is known that modally
definable class of frames is closed under disjoint unions, consequently,
$\mathcal{L}_{osstit}$ is sound and strongly complete w.r.t. Kripke version of
BT+AC frames, defined in accordance with [1].

######  Definition 3.12.

Disjoint Union

Let $\mathbf{M}=\\{\langle W_{n},\\{Choice^{n}_{i}\\}_{i\in
Ags},V_{n}\rangle\>|\>n\in I\\}$ be a collection of disjoint one-shot
strategic stit models. The disjoint union of the models
$\biguplus\limits_{n\in I}\mathbf{M}_{n}=\langle W,\\{Choice_{i}\\}_{i\in
Ags},V\rangle$ is defined as follows:

  1. (1)

$W=\bigcup\limits_{n\in I}W_{n}$

  2. (2)

$V(p)=\bigcup\limits_{n\in I}V_{n}(p)$

  3. (3)

For any $n\in I$, $i\in Ags$, $X\subseteq W$, $w\in W_{n}$: $X\in
Choice_{i}(w)\Leftrightarrow X\cap W_{n}\in Choice^{n}_{i}(w)$

######  Definition 3.13.

Strategic stit to standard stit translation

$tr(p)$ | $p$
---|---
$tr(\neg\phi)$ | $\neg tr(\phi)$
$tr(\phi\lor\psi)$ | $tr(\phi)\lor tr(\psi)$
$tr(\Box\phi)$ | $\Box tr(\phi)$
$tr([i]\phi)$ | $\Diamond[stit]_{i}tr(\phi)$
Table 2: Translation from $\mathbf{L}_{osstit}$ to $\mathbf{L}_{cstit}$

######  Theorem 3.14.

Let $\mathcal{M}=\langle Tree,<,Ags,Choice,\nu\rangle$ be a BT+AC a model.
Then, for a set of one-shot strategic stit models $\mathbf{M}=\\{\langle
W^{m},\\{Choice^{m}\\}_{i\in Ags},V^{m}\rangle\\}_{n\in Tree}$, such that
$W^{m}=\\{m/h\>|\>h\in H_{m}\\}$ for every $m\in Tree$,
$Choice^{m}_{i}(w)=Choice^{m}_{i}\upharpoonright$ 555by
$Choice^{m}_{i}\upharpoonright$ we mean $Choice^{m}_{i}$, closed under
supersets, $V^{m}(p)=\nu(p)|_{W^{m}}$, the following holds:

$\biguplus\mathbf{M},m/h\models\phi\Leftrightarrow\mathcal{M},m/h\models
tr(\phi)$

for every $m/h\in W^{m}$.

######  Proof 3.15.

Follows directly from Definition 3.7 and Proposition 3.6.

##  4 Conclusion and further research

We have proposed a fragment of classical stit logic, $\mathcal{L}_{osstit}$,
with a non-normal strategic modality $[i]\phi$. The neighbourhood semantics
for the fragment was presented, as well as soundness and strong completeness
of $\mathcal{L}_{osstit}$ w.r.t. corresponding class of neighbourhood frames.
The latter was obtained by standard method of canonical model construction.
Nevertheless, a number of issues are open to further investigation.

It is interesting to consider epistemic extensions of $\mathcal{L}_{osstit}$.
It will allow us to reason about epistemic abilities: agent may be able to
knowingly see to it that $\phi$, i.e. she may be aware of the potential result
of an action she is able to execute.

It may be fruitful to construct such extension by adding a $[K_{i}]\phi$
modality, what stands for “agent $i$ has a strategy to knowingly see to it
that $\phi$”. In comparison with causal strategic stit, the behaviour of the
epistemic modality should differ in some aspects.

Consider a case of epistemically ideal agents, i.e. agents’ knowledge is
factual, closed under logical consequence and agents do have positive and
negative introspection. Given absolute rationality, it is natural to assume
that $[K_{i}]$ operator obeys (M), (N) and (D) axioms, just as its “causal
counterpart”$\>[i]$. Epistemic abilities are historically necessary, so
$(Nec)\>[K_{i}]\phi\rightarrow\Box[K_{i}]\phi$ looks intuitive as well.

Obviously, the notion of epistemic ability is stronger than just the causal
one. If an agent is able to knowingly see to it that some state of affairs
holds, then she is causally able to do it as well: on the level of axioms, it
may be represented as $(Kn-A)\>[K_{i}]\phi\rightarrow[i]\phi$.

Another way to construct an epistemic version of strategic stit logic is to
explicitly introduce knowledge in the language by adding $K_{i}\phi$ (agent
$i$ knows that $\phi$) modal operator for every $i\in Ags$. This step allows
to investigate epistemic abilities by treating formulas of the form

$[i]K_{i}\phi$

as well as studying knowledge about ability

$K_{i}[i]\phi$

and their interplay. Nevertheless, on the level of semantics this extension
will require the addition of $\sim_{i}$ relations to the osstit frames. The
desired properties of the indistinguishability relations and their connections
with $Choice$ functions are not clear: the most recent discussions on the
topic could be found in [8], [4].

The computational issues left untouched as well. It is known that the general
group STIT (i.e. allowing expressions of the form $[stit]_{\Gamma}\phi$, where
$\Gamma\subseteq Ags$) without time operators is neither decidable nor
finitely axiomatizable in case $|Ags|>3$ [7]. It is also known that SAT
problem for classical atemporal STIT with single-agent modalities is NEXPTIME-
complete if $|Ags|>2$ [1]. Since $\mathcal{L}_{osstit}$ may be seen as a
fragment of the latter, SAT complexity for it is worth investigating.

## Appendix

Let $\mathbf{L}$ language be:

$\phi:=p\>|\>\neg\phi\>|\>\phi\lor\phi\>|\>[i]\phi\>|\>[\exists_{i}]\phi\>|\>\Box\phi$

for $i\in Ags,p\in Var$. Let $F$ be a frame

$F=\langle W,\\{N_{i}\\}_{i\in Ags}\rangle$

(PL) | All tautologies of classical propositional logic
---|---
(S5$\Box$) | S5 for $\Box$ modality
(S5$[\exists_{i}]$) | MCT4’B logic for $[\exists_{i}]$
(Incl) | $\Box\phi\rightarrow[i]\phi$
(M) | $[i](\phi\land\psi)\rightarrow([i]\phi\land[i]\psi)$
(N) | $[i]\top$
(D) | $\neg[i]\bot$
(Pos) | $\Box\phi\equiv[\forall_{i}]\phi$
(Nec-A) | $[i]\phi\rightarrow\Box[i]\phi$
(Ind) | $[1]\phi_{1}\land[2]\phi_{2}\land\ldots\land[n]\phi_{n}\rightarrow\langle\forall\rangle(\phi_{1}\land\phi_{2}\land\ldots\land\phi_{n})$
(RE) | From $\phi\equiv\psi$, infer $[i]\phi\equiv[i]\psi$
(MP) | From $\phi,\phi\rightarrow\psi$, infer $\psi$
Table 3: Axioms for $\mathcal{L}$ (M) | Monotonicity of $N_{i}$
---|---
(N) | $W\in N_{i}(w)$
(D) | $\emptyset\not\in N_{i}(w)$
(T) | $\forall w\in W(w\in N_{i}(w))$
(4’) | $\forall w\in W\>X\subseteq W(X\in N_{i}(w)\rightarrow N^{-1}_{i}(X)\in N_{i}(w))$
(B) | $\forall w\in W\>X\subseteq W(w\in X\rightarrow W\setminus(N^{-1}_{i}(W\setminus X)\in N_{i}(w)))$
(Pos) | $\bigcup N_{i}\downharpoonright(w)=W$
(Nec-A) | $N_{i}(w)=N_{i}(w^{\prime})$
(Ind) | $\forall X\in N_{a}(w),Y\in N_{b}(w)(X\cap Y\neq\emptyset)$
Table 4: Definability

Canonicity: a class of frames satisfying (M), (N), (D) is such frames where
$N_{i}$ is monotonic, does not contain $\emptyset$ and contains $W$. The
corresponding logic $MND$ is canonical, hence, strongly complete w.r.t. that
class of frames [6, p. 31, 44]. A class of frames satisfying
$(S5[\exists_{i}])$ are such frames where $\bigcup N_{i}\downharpoonright$ is
monotonic, closed under intersections, reflexive, transitive and symmetric.
The corresponding logic $(S5[i])$ is canonical hence complete w.r.t. that
class of frames [6, p. 31, 44]. $(S5\Box\bigoplus Incl)$ is strongly complete
w.r.t. the class Kripke frames with total accessibility relation [11, p.100].
Therefore, fusion of all three logics satisfying $MND\bigoplus
S5([\exists_{i}])\bigoplus S5(\Box)$ is canonical hence strongly complete
w.r.t. the class of fusions of corresponding frames, i.e. the frames with
monotonic $N_{i}$ functions not containing $\emptyset$ and containing $W$,
monotonic reflexive transitive symmetric $\bigcup N_{i}\downharpoonright$ and
universal binary relation $R_{i}$.

It is left for us to prove that (Pos), (Nec-A) and (Ind) are canonical as
well.

######  Definition .1.

Minimal canonical model

For a monotonic modal logic $\mathcal{L}$ and the basic modal language
language $\mathbf{L}$, the minimal canonical model is

$\mathcal{M}^{c}=\langle W^{c},N^{c}_{i}\rangle$

such that

  1. (1)

$W^{c}=\\{\Gamma,\Delta,\ldots\\}$ is a set of maximal
$\mathcal{L}$-consistent sets of $\mathbf{L}$-formulas. By $|\phi|\subseteq
W^{c}$ we denote a proof set of $\phi$, i.e.
$|\phi|=\\{\Gamma\>|\>\phi\in\Gamma\\}$

  2. (2)

$N^{c}:W^{c}\rightarrow 2^{2^{W^{c}}}$ such that
$N^{c}(\Gamma)=\\{|\phi|\>|\>\Box\phi\in\Gamma\\}$

  3. (3)

$V^{c}:Var\rightarrow 2^{W^{c}}$ is an evaluation function such that
$\Gamma\in V^{c}(p)$ iff $p\in\Gamma$

It is important to notice that monotonic modal logic $M$ is not valid on its
minimal canonical model, but it is valid on such model, where instead of
$N^{c}$ there are the same function which is closed under supersets [11]. We
will denote it here and further as $N_{c}\upharpoonright$ and call it the
supplementation of $N^{c}$.

Now we are ready to construct a canonical model for our logic.

######  Definition .2.

Canonical model for $\mathcal{L}$

$\mathcal{M}^{c}=\langle W^{c},\\{\nu^{c}_{i}\upharpoonright\\}_{i\in
Ags},V^{c}\rangle$

  1. (1)

$\\{\Gamma,\Delta,\ldots\\}$ is a set of maximal $\mathcal{L}$-consistent sets
of $\mathbf{L}$-formulas.

  2. (2)

$\nu^{c}_{i}:W^{c}\rightarrow 2^{2^{W^{c}}}$ is a minimal $\mathcal{L}$\-
canonical neighbourhood function associated with $[i]$ modality.
$\nu^{c}_{i}\upharpoonright$ is a supplementation for $\nu^{c}_{i}$

  3. (3)

$V^{c}:Var\rightarrow 2^{W^{c}}$ is an evaluation function such that
$\Gamma\in V^{c}(p)$ iff $p\in\Gamma$

  4. (4)

Notice that if $|\phi|=W^{c}$, then $|\Box\phi|=W^{c}$; if $\phi$ is
consistent (i.e. $|\phi|\neq\emptyset$), then $|\Diamond\phi|=W^{c}$.

  5. (5)

As for $[\exists_{i}]\phi$, it is contained in some $\Gamma\in W^{c}$ iff
$\bigcup\nu^{c}_{i}(\Gamma)\subseteq|\phi|$.

Given the soundness and definability results from Theorem 3.3, the task is to
show that (Pos), (Ind) and (Nec-A) are valid in that canonical model.

######  Theorem .3 ((Pos), (Ind) and (Nec-A) are valid on
$\mathcal{L}$-canonical model).

######  Proof .4.

(Pos)

$\mathcal{M}^{c}\models\Box\phi\equiv[\exists_{i}]\phi$

The left-to-right direction is obvious, so we concentrate on right to left. We
prove it by contraposition.

Suppose there is a $\Gamma\in W^{c}$, such that
$\mathcal{M},\Gamma\models[\exists_{i}]\phi\land\neg\Box\phi$. Then,
$\bigcup\nu^{c}_{i}(\Gamma)\subseteq\phi$ (hence, by definition
$[\exists_{i}]\phi\in\Gamma$ and from the $\Gamma$ $\mathcal{L}$-consistency
of $\Gamma$ it follows that $\Box\phi\in\Gamma$) and
$W^{c}\setminus|\phi|\neq\emptyset$ (by semantics definition of
$\neg\Box\phi$). From the latter it is follows that $\neg\phi$ is consistent,
i.e. $|\neg\phi|\neq\emptyset$. Then, $|\neg\Box\phi|=W^{c}$, and if it is so,
then $\Gamma\in|\neg\Box\phi|$, i.e. $\neg\Box\phi\in\Gamma$. Hence, $\Gamma$
contains both $\Box\phi$ and $\neg\Box\phi$, so it is inconsistent, what leads
to contradiction.

######  Proof .5.

(Ind)

$\mathcal{M}^{c}\models[a]\phi\land\ldots\land[b]\psi\rightarrow\Diamond(\phi\land\ldots\land\psi)$

Suppose that for arbitrary $\Gamma$ it is true that
$\mathcal{M}^{c},\Gamma\models[a]\phi\land[b]\psi$. By definition,
$|\phi|\in\nu^{c}_{a}\upharpoonright(\Gamma)$ and
$|\psi|\in\nu^{c}_{b}\upharpoonright(\Gamma)$. From that, by definition of
$\nu^{c}_{i}\upharpoonright$, $[a]\phi\land[b]\psi\in\Gamma$. Then, since
$\Gamma$ is $\mathcal{L}$-consistent, $(Ind)\in\Gamma$ and $\Gamma$ is closed
under Modus Ponens, so that, $\Diamond(\phi\land\psi)\in\Gamma$. From that, by
definition $|\phi\land\psi|\neq\emptyset$, i.e.
$\mathcal{M}^{c}\models\Diamond(\phi\land\psi)$

######  Proof .6.

(Nec-A)

$\mathcal{M}^{c}\models[i]\phi\rightarrow\Box[i]\phi$

Suppose that for some $\Gamma$ it is the case that
$\mathcal{M}^{c},\Gamma\models[i]\phi$, i.e.
$|\phi|\in\nu^{c}_{i}\upharpoonright(\Gamma)$, then $[i]\phi\in\Gamma$. Since
$\Gamma$ is $\mathcal{L}$-consistent, $\Box[i]\phi\in\Gamma$, i.e.
$|[i]\phi|=W^{c}$ hence $\mathcal{M}^{c}\models\Box\phi$

## References

  * [1] Balbiani, P., A. Herzig and N. Troquard, Alternative axiomatics and complexity of deliberative stit theories, Journal of Philosophical Logic 37 (2008), pp. 387–406.
  * [2] Belnap, N., M. Perloff and M. Xu, “Facing the future: agents and choices in our indeterminist world,” Oxford University Press, 2001.
  * [3] Broersen, J., Deontic epistemic stit logic distinguishing modes of mens rea, Journal of Applied Logic 9 (2011), pp. 137–152.
  * [4] Duijf, H., J. Broersen, A. Kuncova and A. I. R. Abarca, Doing without action types, The Review of Symbolic Logic 14 (2021), pp. 380–410.
  * [5] Goranko, V. and S. Passy, Using the universal modality: gains and questions, Journal of Logic and Computation 2 (1992), pp. 5–30.
  * [6] Hansen, H. H., Monotonic modal logics (2003)
  * [7] Herzig, A. and F. Schwarzentruber, Properties of logics of individual and group agency., Advances in modal logic 7 (2008), pp. 133–149.
  * [8] Horty, J. and E. Pacuit, Action types in stit semantics, The Review of Symbolic Logic 10 (2017), pp. 617–637.
  * [9] Kenny, A., Human abilities and dynamic modalities, in: Essays on explanation and understanding, Springer, 1976 pp. 209–232.
  * [10] Kracht, M. and F. Wolter, Normal monomodal logics can simulate all others, The Journal of Symbolic Logic 64 (1999), pp. 99–138.
  * [11] Pacuit, E., “Neighborhood semantics for modal logic,” Springer, 2017.
  * [12] Segerberg, K., J.-J. Meyer and M. Kracht, The logic of action (2009)
  * [13] Segerberg, K. K., “An essay in classical modal logic,” Stanford University, 1971.