2 Stit theory

The seminal contributions of Prior (Reference Prior1967) and Thomason (Reference Thomason1970, Reference Thomason, Gabbay and Guenthner1984) gave rise to the theory of branching time that would later serve as the backbone for stit semantics (Belnap et al., Reference Belnap, Perloff and Xu2001; Horty, Reference Horty2001).Footnote ⁶ The branching-time models originate from a philosophical enquiry into the truth-values of temporal sentences, for example, so-called future contingencies. Belnap et al. (Reference Belnap, Perloff and Xu2001) present a detailed account of how our indeterministic world can be modelled.Footnote ⁷ The fundamental idea is to represent the world as moments ordered in a tree of histories. (It is important to note a possible confusion: “histories” are taken to include future moments.) The upward branching of histories represents the openness of the future. Although histories may branch at a particular moment, it is conceivable that there are moments at which no history branches. The absence of backward branching represents the determinateness of the past, that is, the fact that every moment has only a single past sequence of events. Each history in such a tree-like structure represents a complete temporal evolution of the world.

A branching-time model involves a set of moments M, a set of histories $H\subseteq 2^{M}$ , and a relation $<$ between moment/history pairs which represents the progression of events along a history. We use $m,m'$ as variables for moments in M and $h,h'$ as variables for histories in H. When a moment m and a history h satisfy $m\in h$ , this can be taken to mean that m occurs on h, or that h passes through m. Because of indeterminacy, there may be multiple histories that pass through m, so we let $H_m=\{h\in H\mid m\in h\}$ denote the set of histories through m. We use $m/h$ as variables for moment/history pairs that satisfy $m\in h$ or, equivalently, $h\in H_m$ . It is common to call these moment/history pairs indices; we let $\textit {Ind}$ denote the set of indices. A given index includes the current moment and the complete temporal evolution of the world. Finally, a valuation function V assigns to each propositional variable $q\in \mathcal {P}$ the set of indices $V(q)$ where q obtains.

These branching-time models are typically used to provide semantics for a logical language that includes a past operator $\mathsf {P}$ , a future operator $\mathsf {F}$ , and a historical necessity operator $\Box $ .Footnote ⁹ Intuitively, $\mathsf {P}\varphi $ is true at a moment/history pair $m/h$ if and only if there is a moment $m'$ before m on h where $\varphi $ obtains; $\mathsf {F}\varphi $ holds at a moment/history pair $m/h$ if and only if there is a moment $m'$ after m on h where $\varphi $ obtains. The historical necessity operator $\Box \varphi $ expresses that $\varphi $ holds at the current moment in the moment/history pair $m/h$ regardless of how the future unfolds. The dual $\Diamond \varphi $ expresses that there is a possible way for the future to unfold such that $\varphi $ holds now.

Definition 2.2. (Evaluation Rules Temporal Formulas)

Let $\textit {BTM}$ be a branching-time model, and let $\varphi $ be a formula constructed using propositional constants and temporal operators $\mathsf {P}, \mathsf {F}$ , and $\Box $ . Then the truth of $\varphi $ , in a moment/history pair $m/h$ in $\textit {BTM}$ , notation: $\textit {BTM},m/h\vDash \varphi $ , is given by the following (suppressing the standard propositional clauses and the model $\textit {BTM}$ ):

$$ \begin{align*} \begin{array}{lcl} m/h\vDash\mathsf{P}\varphi & \text{\it iff} & there\ is\ an\ m'\in\ h\ {\it satisfying}\ m'<_h\ m\ and\ m'/h\vDash\varphi;\\ m/h\vDash\mathsf{F}\varphi & \text{\it iff} & there\ is\ an\ m'\in\ h\ {\it satisfying}\ m<_h m'\ and\ m'/h\vDash\varphi;\\ m/h\vDash\Box\varphi & \text{\it iff} & every\ h'\in\ H_m\ {\it satisfies}\ m/h'\vDash\varphi. \end{array} \end{align*} $$

Given these semantics, the idea that the future may still be open is represented by the invalidity of the formula $\mathsf {F}\varphi \to \Box \mathsf {F}\varphi $ . In other words, there is a branching-time model $\textit {BTM}$ and a moment/history pair $m/h$ such that $\textit {BTM},m/h\vDash \mathsf {F}\varphi $ while $\textit {BTM},m/h\nvDash \Box \mathsf {F}\varphi $ .Footnote ¹⁰ Or, equivalently, $\textit {BTM},m/h\vDash \mathsf {F}\varphi \land \Diamond \lnot \mathsf {F}\varphi $ .

The fundamental idea of stit theory is to treat agency as a modality in these branching-time models. At a particular moment m we may view $H_m$ as representing the possibilities that are still open. Conversely, the histories outside $H_m$ are no longer possible, or accessible, at moment m. Given that the histories in $H_m$ are still open, an agent’s action, or choice, is viewed as restricting the possible histories to a subset K of $H_m$ . Accordingly, “the agent sees to it that $\varphi $ ” means that the truth of $\varphi $ is guaranteed by an action or choice K of the agent. When Ann empties her glass of milk, the nature of her action on this view is to constrain the possible histories to those where the glass of milk is emptied. Hence, an action is identified with a subset of the possible histories. This induces the reading that an agent sees to it that $\varphi $ only if she performs an action that constrains the possible worlds to only $\varphi $ -worlds.

A branching-time agency model supplements a branching-time model with a finite set of agents $\textit {Ags}$ and sets of available actions, one for each agent at each moment. Given a moment m and an agent i, the set of available actions is given by a collection of subsets of the possible histories $\textit {Act}^{m}_{i}\subset 2^{H_m}$ .Footnote ¹¹ Since a history can be viewed as the complete temporal evolution of the world, it includes the actions that the agents are performing. The particular action that agent i executes at a moment/history pair $m/h$ is given by $\textit {Act}^{m}_{i}(h)$ , which is the action $K\in \textit {Act}^{m}_{i}$ satisfying $h\in K$ .Footnote ¹²

Figure 1 depicts such a branching-time agency frame.Footnote ¹⁴ For example, at $m_1$ , agents i and j both have two available actions, where each action is identified with a subset of the possible histories, in particular, $\textit {Act}_i^{m_1}=\{\{h_1,h_6,h_7\},\{h_2,h_3, h_4,h_5\}\}$ . These branching-time agency models are used to interpret a logical language that includes agency operators $[i\;\mathsf {stit}]$ , one for each agent i. Intuitively, $[i\;\mathsf {stit}]\varphi $ is true at a moment/history pair $m/h$ if and only if the truth of $\varphi $ is guaranteed by the action of the agent i. That is, agent i performs a certain action thereby constraining the possible histories to only those where $\varphi $ holds. It may be useful to add that $[i\;\mathsf {stit}]\varphi $ may be interpreted, relative to a moment/history pair $m/h$ , as “agent i guarantees that $\varphi $ holds regardless of what the others do”.

Fig. 1 A branching-time agency frame.

Definition 2.4. (Evaluation Rule Agency)

Let $\textit {BTAM}=\langle M, H, <, \textit {Ags}, (\textit {Act}^{m}_{i}), V\rangle $ be a branching-time agency model. Then the evaluation rule for the stit operator at a given moment/history pair $m/h$ is given by the following (suppressing the model $\textit {BTAM}$ ):

$$ \begin{align*} \begin{array}{lcl} m/h\vDash [i\;\mathsf{stit}]\varphi & \text{\it iff} & for\ every\ h'\in{Act}^{m}_{i}(h)\ it\ holds\ that\ m/h'\vDash\varphi. \end{array} \end{align*} $$

We will write $\langle i\;\mathsf {stit}\rangle \varphi $ for the dual of $[i\;\mathsf {stit}]\varphi $ , i.e., for $\lnot [i\;\mathsf {stit}]\lnot \varphi $ .

It might be helpful to briefly revisit the branching-time agency frame depicted in Figure 1. Let us focus on moment $m_2$ . At $m_2$ , agent j has two available actions, where each action is identified with a subset of the possible histories, in particular, $\textit {Act}^{m_2}_{j}=\{\{h_2\},\{h_3,h_4\}\}$ . Note that at index $m_2/h_4$ it is the case that q holds even though it is not the case that agent j sees to it that q holds. That is, $m_2/h_4\vDash q\land \lnot [j\;\mathsf {stit}]q$ . The second conjunct follows from the fact that q does not hold at $m_2/h_3$ . This illustrates that it is foreseeable that not everything that happens is brought about by an agent.Footnote ¹⁵

3 Knowledge in stit theory

The branching-time agency models serve as the backbone for epistemic stit models. An epistemic stit model supplements a branching-time agency model with a set of indistinguishability relations $\sim _i\subseteq \textit {Ind}\times \textit {Ind}$ , one for each agent $i\in \textit {Ags}$ . The idea is that whenever $m/h\sim _i m'/h'$ holds, then agent i cannot distinguish these indices. Given such an indistinguishability relation, we can define the information set of agent i at a moment/history pair $m/h$ as the set consisting of those moment/history pairs that the agent cannot distinguish from $m/h$ . More specifically, this information set is given by $\{m'/h'\in \textit {Ind}\mid m'/h'\sim _i m/h\}$ .Footnote ¹⁶ An epistemic stit model is thus best thought of as representing the possibilities, knowledge (or information), and available actions at several moments in time.

To illustrate epistemic stit models, let us consider the two examples that Horty & Pacuit (Reference Horty and Pacuit2017, pp. 623–625, Figures 3 and 4) discuss to motivate the introduction of action types into stit theory, here depicted in Figures 2 and 3. In each of these examples, an agent, called j, first places a coin on the table either heads up, by selecting $K_1$ , or tails up, by selecting $K_2$ . Afterwards the other agent, called i, is offered the option to bet on whether agent j put the coin heads up or tails up. This happens at either moment $m_2$ or moment $m_3$ , depending on agent j’s choice. If agent j chooses to place the coin heads up, then the resulting moment will be $m_2$ , and agent i bets heads by selecting $K_3$ and bets tails by selecting $K_4$ . If agent j chooses to place the coin tails up, then the resulting moment will be $m_3$ , and agent i bets heads by selecting $K_5$ and bets tails by selecting $K_6$ . If we let $\varphi $ denote the state of affairs where agent i bets correctly, then we see that $\varphi $ holds at $m_2/h_1$ and $m_3/h_4$ , and it is false at $m_2/h_2$ and $m_3/h_3$ .

Fig. 2 The epistemic stit model that Horty & Pacuit (Reference Horty and Pacuit2017, Figure 3) use to depict the first coin example.

Fig. 3 The epistemic stit model that Horty & Pacuit (Reference Horty and Pacuit2017, Figure 4) use to depict the second coin example.

The two coin examples are identical with regard to their causal structure, but they differ in the information that is available to agent i. In the first coin example, agent i knows whether the coin has been placed heads up or tails up. This is represented by the fact that agent i can distinguish between moments $m_2$ and $m_3$ . This indistinguishability relation is represented in the figures by the dashed line between indices.Footnote ¹⁷ More precisely, the indistinguishability relation for agent i is given by the equivalence classes $\{m_2/h_1,m_2/h_2\}$ and $\{m_3/h_3,m_3/h_4\}$ . In the second coin example, agent i does not know whether the coin has been placed heads up or tails up. This is represented by the fact that agent i cannot distinguish between moments $m_2$ and $m_3$ . More precisely, the indistinguishability relation for agent i is given by the single equivalence class $\{m_2/h_1,m_2/h_2,m_3/h_3,m_3/h_4\}$ . We will return to these models in §3.1.

It is common among logicians, computer scientists, and economists to use these epistemic models to provide semantics for a logical language that includes knowledge operators $\mathsf {K}_i$ , one for each agent i. Intuitively, $\mathsf {K}_i\varphi $ is true at a moment/history pair $m/h$ if and only if $\varphi $ is true at every moment/history pair that agent i cannot distinguish from $m/h$ . In other words, we can say that an agent knows something if her information set entails it.

Definition 3.2. (Evaluation Rule Knowledge)

Let $\mathcal {M}$ be an epistemic stit model. Then the evaluation rule for the knowledge operator at a given moment/history pair $m/h$ is given by the following:

$$ \begin{align*} \begin{array}{ll} \mathcal{M}, m/h \vDash \mathsf{K}_i\varphi \quad \text{\it iff} \quad &for\ every\ m'/h'\in{Ind}\ {\it satisfying}\ m/h\sim_i\ m'/h'\ it\ holds \\ & that\ \mathcal{M}, m'/h'\vDash \varphi. \end{array} \end{align*} $$

We will write $\hat {\mathsf {K}}_i\varphi $ for the dual of $\mathsf {K}_i\varphi $ , i.e., for $\lnot \mathsf {K}_i\lnot \varphi $ .

4 Action types

Horty & Pacuit (Reference Horty and Pacuit2017, sec. 4) have recently imported ideas on action types and abilities under uncertainty into stit theory. Simply stated, they submit that agent i is able, in an epistemic sense, to do $\varphi $ if and only if there is an action type available to her that she knows guarantees $\varphi $ . We will first discuss their approach in detail and then establish a correspondence to standard epistemic stit models that eschew action types in §5.

Horty and Pacuit extend traditional epistemic stit models to labeled stit models by postulating a set of action types $\textit {Tps}$ and a label function $\textit {Lbl}$ that maps each action token K to a particular action type $\textit {Lbl}(K)\in \textit {Tps}$ .Footnote ¹⁹ We will often write $\textit {Lbl}_i(m/h)$ , instead of $\textit {Lbl}(\textit {Act}^{m}_{i}(h))$ , to denote the action type that agent i performs at $m/h$ . In addition, a partial execution function $\textit {Exn}$ is added, which maps each action type $\tau \in \textit {Tps}$ , moment m, and agent i to a particular action token $\textit {Exn}^{m}_{i}(\tau )\in \textit {Act}^{m}_{i}$ .Footnote ²⁰ It is partial because there may be moments at which a certain action type is not executable. A labeled stit model is a tuple of the form:

$$ \begin{align*} \langle M, H, <, {Ags}, ({Act}^{m}_{i}), (\sim_i), V, {Tps}, {Lbl}, {Exn}\rangle. \end{align*} $$

With the help of these action types, one can define a new epistemic stit operator, denoted by $[i\;\mathsf {kstit}]$ , which is distinct from the standard stit operator, denoted by $[i\;\mathsf {stit}]$ , and is meant to capture a subjective sense of agency. That is, an agent epistemically sees to it that $\varphi $ if and only if she knows that the action type she performs guarantees $\varphi $ . Or, equivalently, if and only if the action type she performs guarantees $\varphi $ at every indistinguishable index. More formally:

Definition 4.1. (Evaluation Rule Epistemic Agency)

Let $\mathcal {M}$ be a labeled stit model. Then the evaluation rule for the kstit operator is given by:

$$ \begin{align*} \begin{array}{ll} \mathcal{M},m/h\vDash [i\;\mathsf{kstit}]\varphi \qquad \text{\it iff} & \text{\it for}\ every\ m'/h'\ that\ {\it satisfies}\ m'/h'\sim_{i} m/h\ and\ \text{\it for} \\ &any\ m'/h''\ that\ {\it satisfies}\ {Lbl}_{i}(m/h)={Lbl}_{i}(m'/h'')\ it \\ &holds\ that\ m'/h''\vDash\varphi. \end{array} \end{align*} $$

It is important to emphasize that the analysis of epistemic ability of Horty & Pacuit (Reference Horty and Pacuit2017) relies on two constraints on the labeled stit models. First, they concede that their analysis of epistemic ability “makes most sense, and is most useful, when the indistinguishability relation …can be thought of as a relation, not just between indices, but between moments themselves” (Horty & Pacuit, Reference Horty and Pacuit2017, p. 631—condition C4). That is, they impose the restriction that agents cannot know more about the current moment/history pair than what is historically settled. This requirement can be characterized by the following semantic condition:

• • for any agent i and for all $m/h, m'/h^{\prime }_1$ if $m/h\sim _i m'/h^{\prime }_1$ , then for any $m'/h^{\prime }_2$ it holds that $m/h\sim _i m'/h^{\prime }_2$ . (Settled Knowledge)

This semantic condition can be characterized by an axiom scheme on epistemic frames:

Proposition 4.2. Let $\mathcal {F}$ be an epistemic stit frame. Then, $\mathcal {F}$ satisfies the settled knowledge condition if and only if

$$ \begin{align*} \mathcal{F}\vDash \mathsf{K}_i \varphi \to \mathsf{K}_i\Box \varphi. \end{align*} $$

It is important to flag that this condition aligns with existing frameworks in the computer science literature on knowledge and action. Models in the ATL tradition involve a set of states, and actions are thought of as transitions between such states. In light of the connections between stit theory and ATL (Broersen et al., Reference Broersen, Herzig and Troquard2006a, Reference Broersen, Herzig, Troquard and Samet2007), a state in an ATL model can be thought of as a moment in a stit model. In the ATL tradition, imperfect information is usually modelled using an epistemic indistinguishability relation on states (see van der Hoek & Wooldridge, Reference van der Hoek and Wooldridge2003), which hence corresponds to an epistemic indistinguishability relation on moments.

So, what would an epistemic indistinguishability relation on indices correspond to in ATL models? An index involves a moment and a history and therefore includes a representation of the entire temporal evolution of the world. Since a stit theorist can think of a history as a set of linearly ordered moments, ATL theorists can think of a history as a set of linearly ordered states.Footnote ²¹ We postulate that an ATL theorist should think of an index in stit theory as a dynamic state, where a dynamic state involves the current state and the history of states that represent the temporal evolution of the world or system. (It is important to, once again, note a possible confusion: “histories” are taken to include future states.) In contrast, we propose that a moment be thought of as a static state, which represents the current state but does not include a representation of the temporal evolution of the world or system. Accordingly, we will call an epistemic stit model that satisfies (Settled Knowledge) a static epistemic stit model.

Second, to ensure that the definition of the kstit operator makes sense Horty & Pacuit (Reference Horty and Pacuit2017, p. 628—condition C1) stipulate that labeled stit frames must satisfy an extra condition that might be called uniformity of available action types: This condition says that whenever two indices are indistinguishable for a given agent, then the agent has the same action types available at these indices. Let us use $\textit {Tps}^{m}_{i}$ to denote the action types that are available to agent i at m in a given labeled stit model. That is, $\textit {Tps}^{m}_{i}=\{\tau \in \textit {Tps}\mid $ there is a $h\in H_{m}$ such that $\tau =\textit {Lbl}_{i}(m/h)\}$ . The condition of uniformity of available action types can be expressed by the following semantic condition, which we’ll often abbreviate to (UAAT):

• • for every $m/h, m'/h'\in \textit {Ind}$ if $m/h\sim _i m'/h'$ then $\textit {Tps}^{m}_{i}=\textit {Tps}^{m'}_{i}$ .Footnote ²² (Uniformity of Available Action Types)

With the exception of §5.2, we assume that labeled stit models meet this requirement in the remainder of the paper.

Horty and Pacuit’s new notion of epistemic agency is then used to characterize the notion of epistemic ability using a combination of epistemic agency and impersonal possibility:

$$ \begin{align*} \Diamond [i\;\mathsf{kstit}]\varphi, \end{align*} $$

that is, this formula “can be taken to represent the idea that the agent i has the ability, in the epistemic sense, to see to it that $\varphi $ ” (Horty & Pacuit, Reference Horty and Pacuit2017, p. 630—notation adapted).

It is helpful to note that the two coin examples of §3 can be represented using the labeled stit models of Figures 4 and 5, respectively. It is straightforward to verify that these labeled stit models give the desired answers regarding epistemic ability. In the first labeled stit model (Figure 4), it is easy to see that $m_2/h_1\vDash [i\;\mathsf {kstit}]\varphi $ , because $\varphi $ holds at any index that is indistinguishable from $m_2/h_1$ and where agent i also executes action type $\tau _1$ . Consequently, we can see that $\Diamond [i\;\mathsf {kstit}]\varphi $ holds at any index that is based on moment $m_2$ or $m_3$ . This means that agent i is able, in the epistemic sense, to do $\varphi $ , regardless of the choice of agent j. Moreover, in the second labeled stit model (Figure 5), it is easy to see that $m_2/h_1\nvDash [i\;\mathsf {kstit}]\varphi $ , because agent i cannot distinguish $m_3/h_3$ from $m_2/h_1$ and executes the same action type at these indices, namely $\tau _1$ . It then follows that $\Diamond [i\;\mathsf {kstit}]\varphi $ never obtains and that agent i is not able, in the epistemic sense, to do $\varphi $ , regardless of what agent j chose. The analysis of Horty and Pacuit thus solves the puzzles alluded to in §3.1.

Fig. 4 The labeled stit model that Horty & Pacuit (Reference Horty and Pacuit2017) use to depict the first coin example.

Fig. 5 The labeled stit model that Horty & Pacuit (Reference Horty and Pacuit2017) use to depict the second coin example.

5 Knowingly doing and the general correspondence result

The source of our disagreement with the analysis of epistemic ability by Horty & Pacuit (Reference Horty and Pacuit2017) is that they end up imposing the semantic condition of settled knowledge on their models. There are two reasons against adopting this semantic condition. First, it is essential for the idea of agency akin to stit theory that alternative histories through a particular moment may witness different actions that the agents can perform. So, given moment/history pair $m/h$ , if an agent cannot distinguish any of the moment/history pairs that emanate from that given moment m, then she does not know anything about the action that she performs at $m/h$ . In particular, the semantic condition of settled knowledge rules out that any agent knows anything about the action she performs. This is one of the main reasons why we reject this assumption and prefer to think of epistemic indistinguishability as a relation between indices, which include histories, rather than between moments.Footnote ²³

Second, abandoning the assumption of settled knowledge yields the benefit of being able to characterize the notion of knowingly doing by a simple combination of knowledge and agency. From the perspective of our formalism, the formula $\mathsf {K}_i[i\;\mathsf {stit}]\varphi $ expresses that agent i knowingly sees to it that $\varphi $ (Broersen, Reference Broersen2011a, sec. 3). Conversely, an agent unknowingly does $\varphi $ if and only if (i) she is performing an action that guarantees $\varphi $ and (ii) she considers it possible that she does not guarantee $\varphi $ . Jan Broersen writes:

The concept of knowingly doing can be naturally related to Horty and Pacuit’s epistemic notion of agency, which relies on action types. Given a labeled stit model, we can construct a transform epistemic stit model such that epistemic agency in the former corresponds to knowingly doing in the latter. This transformation only changes the indistinguishability relations. For a given agent, two indices are indistinguishable in the transform epistemic stit model if and only if these indices are indistinguishable in the original labeled stit model and the agent executes the same action type at each of these indices. More precisely:

To illustrate this transformation, let us present the transformations of the labeled stit models of the coin examples (see Figures 4 and 5) in Figures 6 and 7, respectively. It is straightforward to verify that these transform epistemic stit models give the desired answers regarding epistemic agency as modelled by the notion of knowingly doing. In the first transform epistemic stit model (Figure 6), note that the information state of agent i at index $m_2/h_1$ is given by the set $\{m_2/h_1\}$ . It is then easy to see that $m_2/h_1\vDash \mathsf {K}_i[i\;\mathsf {stit}]\varphi $ . Consequently, we can see that $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi $ holds at any index that is based on moment $m_2$ or $m_3$ . This means that agent i is able to knowingly do $\varphi $ , regardless of what agent j chose. Moreover, in the second transform epistemic stit model (Figure 7), it is easy to see that $m_2/h_1\nvDash \mathsf {K}_i[i\;\mathsf {stit}]\varphi $ , because agent i cannot distinguish $m_3/h_3$ from $m_2/h_1$ and $[i\;\mathsf {stit}]\varphi $ is falsified at $m_3/h_3$ . It then follows that $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi $ never obtains and that agent i is not able to knowingly do $\varphi $ , no matter what agent j chooses.

Fig. 6 The transform epistemic stit model of the labeled stit model of the first coin example (Figure 4).

Fig. 7 The transform epistemic stit model of the labeled stit model of the second coin example (Figure 5).

We propose that the simple formula $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi $ expresses epistemic ability. The above discussion shows that our proposal adequately discriminates between the two coin examples—when they are modelled as in Figures 6 and 7 rather than Figures 2 and 3. In other words, the examples used by Horty and Pacuit point out that epistemic ability can be expressed by a simple combination of impersonal possibility, knowledge, and agency. Moreover, our formalism shows that an analysis of epistemic ability can do without action types.

These last observations regarding the relation between a labeled stit model and its transform epistemic stit model can be generalized. If we limit ourselves to standard stit formulas (without the knowledge operator),Footnote ²⁵ it follows that the epistemic agency operator in the labeled stit model is supported at an index only if the knowingly doing operator is supported at that index in the transform epistemic stit model.

Proposition 5.2. Let $\mathcal {M}$ be a labeled stit model, and let $\mathcal {M}'$ be the associated transform epistemic stit model. Let $i\in \textit {Ags}$ be an agent, $\varphi \in \mathfrak {L}_{\textit {stit}}$ be a standard stit formula, and $m/h$ be an index. Then

$$ \begin{align*} \text{If } \mathcal{M},m/h\vDash [i\;\mathsf{kstit}]\varphi, \text{ then } \mathcal{M}',m/h\vDash \mathsf{K}_i[i\;\mathsf{stit}]\varphi. \end{align*} $$

This observation entails that whenever at a given index in a given labeled stit model it is the case that an agent sees to it that $\varphi $ in the epistemic sense, then that agent knowingly does $\varphi $ at that index in the transform epistemic stit model. Moreover, if an agent unknowingly does $\varphi $ at a given index in the transform epistemic stit model, then that agent does not see to it that $\varphi $ in the epistemic sense at that index in the labeled stit model. However, it may be that an agent knowingly does $\varphi $ at a given index in the transform epistemic stit model while that agent does not see to it that $\varphi $ , in the epistemic sense, at that index in the labeled stit model.Footnote ²⁶

When we restrict our attention to static labeled stit models, then we can expand the previous correspondence result. If we limit ourselves to standard stit formulas (without the knowledge operator), then it follows that the kstit operator in a given static labeled stit model is supported at a given index if and only if the knowingly doing operator is supported at that index in the transform epistemic stit model. Moreover, under these assumptions, the knowledge operator $\mathsf {K}_{i}$ in a given static labeled stit model is supported at a given index if and only if the combination of the knowledge and historical necessity operators is supported in the transform epistemic stit model.

Theorem 5.3. Let $\mathcal {M}$ be a static labeled stit model, and let $\mathcal {M}'$ be the associated transform epistemic stit model. Let $i\in \textit {Ags}$ be an agent, $\varphi \in \mathfrak {L}_{\textit {stit}}$ be a standard stit formula, and $m/h$ be an index. Then the following holds

$$ \begin{align*} \begin{array}{lcl} (1) \mathcal{M},m/h\vDash [i\;\mathsf{kstit}]\varphi & \text{\it if}\ and\ only\ \text{\it if}\ & \mathcal{M}',m/h\vDash \mathsf{K}_{i}[i\;\mathsf{stit}]\varphi;\\ (2) \mathcal{M},m/h\vDash \mathsf{K}_{i}\varphi & \text{\it if}\ and\ only\ \text{\it if} & \mathcal{M}',m/h\vDash \mathsf{K}_{i}\Box\varphi. \end{array} \end{align*} $$

This result yields several important observations. First, the epistemic notion of ability that Horty & Pacuit (Reference Horty and Pacuit2017) capture by the formula $\Diamond [i\;\mathsf {kstit}]\varphi $ corresponds to the formula $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi $ in our formalism. So whenever one wants to analyze the epistemic abilities of a given agent in a particular example, then if one adopts Horty and Pacuit’s analysis in terms of static labeled stit models using the formula $\Diamond [i\;\mathsf {kstit}]\varphi $ , then that analysis can be simulated in terms of epistemic stit models using the formula $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi $ . Notice that the converse may not hold: the jury is out on whether there exist examples where epistemic ability can be analyzed in terms of epistemic stit models using the formula $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi $ yet this analysis cannot be simulated in terms of static labeled stit models using the formula $\Diamond [i\;\mathsf {kstit}]\varphi $ .

Second, our framework captures epistemic ability without any appeal to action types. Horty & Pacuit (Reference Horty and Pacuit2017) argued that stit models need to incorporate action types to address certain puzzles about knowledge and action. We believe their argument is misguided due to their insistence that the indistinguishability relations hold between moments instead of indices. After all, as the above result proves, any static labeled stit model can be transformed into a (non-static) epistemic stit model in such a way that it addresses these puzzles about knowledge and action.

5.1 Two optional conditions on knowledge in stit theory

The transform epistemic stit models, that correspond to a static labeled stit model in light of our transformation, are restricted in important ways. To emphasize these restrictions we present two properties. They can be characterized by axiom schemas or by the corresponding semantic conditions on epistemic stit frames.Footnote ²⁷ They highlight the flexibility and interpretation of the epistemic stit framework.

Proposition 5.4. Let $\mathcal {F}$ be an epistemic stit model. Then

1. (OAC) We say that $\mathcal {F}$ satisfies the own-action condition if and only if

   • • the schema $\mathsf {K}_i\varphi \to \mathsf {K}_i[i\;\mathsf {stit}]\varphi $ is valid on $\mathcal {F}$ .

   • • Or, equivalently, if and only if for all indices $m/h,m'/h^{\prime }_1$ , and $m'/h^{\prime }_2$ , if $m/h\sim _i m'/ h^{\prime }_1$ and $h^{\prime }_2\in \textit {Act}_{i}^{m'}(h^{\prime }_1)$ , then $m/h \sim _i m'/ h^{\prime }_2$ .

2. (Unif-H) We say that $\mathcal {F}$ satisfies the uniformity of historical possibility property if and only if

   • • the schema $\Diamond \mathsf {K}_i \varphi \to \mathsf {K}_i \Diamond \varphi $ is valid on $\mathcal {F}$ .

   • • Or, equivalently, if and only if for all indices $m/h_1, m/h_2$ , and $m'/h^{\prime }_1$ , if $m/h_1\sim _i m'/h^{\prime }_1$ , then there is a history $h^{\prime }_2$ such that $m/h_2\sim _i m'/h^{\prime }_2$ .

It may be helpful to note that the own-action condition is equivalent to $\langle i\;\mathsf {stit}\rangle \varphi \to \hat {\mathsf {K}}_i\varphi $ .Footnote ²⁸ The own-action condition therefore corresponds to the simple frame condition that for any indices $m/h,m/h'$ if $h'\in \textit {Act}^{m}_{i}(h)$ then $m/h \sim _i m/h'$ . That is, any information state in the partition induced by $\sim _i$ is a union of actions from $\textit {Act}^{{}}_{i}$ .Footnote ²⁹

The own-action condition expresses the idea that an agent cannot know more about the current moment/history pair than what she knows about what she herself brings about. In other words, agents can only know something about the current moment/history pair if it is the result of an action they themselves knowingly perform.

We might say that the own-action condition is a consequence of the assumption that agents cannot know what actions other agents perform concurrently.Footnote ³⁰ The independence-of-agency condition (see Definition 2.3) guarantees that agents’ choices always refine the choices of others. So if an agent knows about the choices of other agents, then she knows more about the future than what is guaranteed by her own choice.

The uniformity of historical possibility property expresses the idea that whenever it is possible for agent i to know $\varphi $ , then she knows that $\varphi $ is possible. It is easy to verify that the semantic condition also corresponds to $\mathsf {K}_{i}\Box \varphi \to \Box \mathsf {K}_i\varphi $ .Footnote ³¹ This means that whenever an agent knows that $\varphi $ is historically settled, then it is historically settled that she knows $\varphi $ . Or, equivalently, it rules out that agents know that a given proposition is historically settled in case it is possible that she does not know that proposition.

Why are these two conditions important for the analysis of epistemic ability? We can show that the transform epistemic stit models validate both of these conditions:

Theorem 5.5. Let $\mathcal {M}$ be a static labeled stit model, and let $\mathcal {M}'$ be the associated transform epistemic stit model. Let $i\in \textit {Ags}$ be an agent, $\varphi \in \mathfrak {L}_{\textit {stit}}$ be a standard stit formula, and $m/h$ be an index. Then the following holds

$$ \begin{align*} \begin{array}{rl} {\mathsf{\bf (OAC)}} & \mathcal{M}', m/h\vDash \mathsf{K}_{i}\varphi\to \mathsf{K}_{i}[i\;\mathsf{stit}]\varphi; \\ \mathbf{(Unif}\textbf{-}\mathbf{H)} & \mathcal{M}',m/h\vDash \Diamond\mathsf{K}_{i}\varphi\to \mathsf{K}_{i}\Diamond\varphi. \end{array} \end{align*} $$

It may be helpful to remark that Theorems 5.3 and 5.5 jointly entail two further equivalences:

$$ \begin{align*} \begin{array}{lcl} (1*)\ \mathcal{M},m/h\vDash [i\;\mathsf{kstit}]\varphi & \text{if and only if} & \mathcal{M}',m/h\vDash \mathsf{K}_{i}\varphi;\\ (2*)\ \mathcal{M},m/h\vDash \mathsf{K}_{i}\varphi & \text{if and only if} & \mathcal{M}',m/h\vDash \Box\mathsf{K}_{i}\varphi. \end{array} \end{align*} $$

That is, epistemic agency in a given static labeled stit model is equivalent to knowledge in the transform epistemic stit model; and knowledge in a given static labeled stit model is equivalent to settled knowledge in the transform epistemic stit model.

These equivalences naturally relate to a distinction from economics between information at different stages of decision-making: “an agent’s ex ante knowledge is the information available to the agent without taking into account any actions she is currently executing, while the agent’s ex interim knowledge is information that does take into account whatever actions the agent is currently executing, along with the effects of these actions” (Horty & Pacuit, Reference Horty and Pacuit2017, pp. 31–32—emphasis added).Footnote ³² In light of these equivalences, we submit that the notion of knowledge in our formalism relates to ex interim knowledge while the simple combination of impersonal necessity and knowledge relates to ex ante knowledge.

Let us finish with briefly mentioning a few ramifications of this result for the analysis of epistemic ability. From the perspective of our formalism, the transform epistemic stit models validate the own-action condition and the uniformity of historical possibility condition. More precisely, this is the case if the initial labeled stit model satisfies the conditions (UAAT) and (Settled Knowledge) (see §4). This means that Horty and Pacuit’s analysis of epistemic ability only applies to epistemic stit models that validate the conditions (OAC) and (Unif-H). Moreover, Proposition 5.4 reveals that if one is interested in the subclass of epistemic stit models that validate one or the other property, then the resulting logic is obtained by adding the respective logical schemata.

It is unclear whether Horty and Pacuit’s analysis applies to all models that validate (OAC) and (Unif-H). In analogy with Theorem 5.3, an affirmative answer would require that one be able to transform any epistemic stit model that validates (OAC) and (Unif-H) into a static labeled stit model such that our analysis of epistemic ability, using the formula $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi $ , can be simulated by their analysis of epistemic ability, using the formula $\Diamond [i\;\mathsf {kstit}]\varphi $ .Footnote ³³

Finally, it is unclear whether Horty and Pacuit’s analysis extends to models that violate any of these conditions. Our formalism is more flexible in that it does not rely on these limitations. In fact, we are unsure whether these conditions are desirable or natural to impose on the models. Although an elaborate discussion of our worries has to be postponed to another occasion, it may be helpful to, once again, note that the own-action condition can be thought of as the requirement that agents do not know more about the current moment/history pair than what she knows about what she herself brings about. It, however, seems plausible that there are cases where agents have knowledge about their own future actions or about the actions of other agents.Footnote ³⁴ Within our formalism, one could hence study whether the characterization of epistemic ability, by the formula $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi $ , is supported in cases where any of these conditions is dropped.Footnote ³⁵

5.2 Uniformity of available action types

We would like to close this section by briefly revisiting the semantic condition of uniformity of available action types, abbreviated to: (UAAT) (see §4). The aim is two-fold: (i) we would like to investigate whether there exists an axiom schema that characterizes this semantic condition; and (ii) we would like to study its logical relation to the condition of uniformity of historical possibility (see Proposition 5.4). To address the first issue, we broaden our attention to the class of static labeled stit models that includes models that violate (UAAT). This semantic condition can then be characterized by an axiom schema:Footnote ³⁶

Proposition 5.6. Let $\mathcal {F}$ be a static labeled stit frame. Then $\mathcal {F}$ satisfies the semantic condition of uniformity of available action types if and only if the following schema is valid on $\mathcal {F}$ :

$$ \begin{align*} \Diamond [i\;\mathsf{kstit}]\varphi\to\mathsf{K}_i\Diamond[i\;\mathsf{stit}]\varphi. \end{align*} $$

Let $\mathcal {F}'$ be the transform epistemic stit frame of $\mathcal {F}$ . Then the semantic condition holds at $\mathcal {F}$ only if the following schema is valid on $\mathcal {F}'$ :

$$ \begin{align*} \Diamond\mathsf{K}_i[i\;\mathsf{stit}]\varphi\to\mathsf{K}_i\Diamond[i\;\mathsf{stit}]\varphi. \end{align*} $$

This proposition shows that a static labeled stit frame validates the semantic condition (UAAT) only if the formula $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi \rightarrow \mathsf {K}_i\Diamond [i\;\mathsf {stit}]\varphi $ is valid on the transform epistemic stit frame.Footnote ³⁷ However, it turns out that there are static labeled stit frames that violate the semantic condition (UAAT) even though that formula is valid in the corresponding transform stit frame. These labeled stit models are rather peculiar. More precisely, let us say that a labeled stit model is label-consistent if and only if whenever $m/h\sim _i m'/h'$ then $\textit {Tps}^{m}_{i}\cap \textit {Tps}^{m'}_{i}\neq \emptyset $ .Footnote ³⁸ Whenever a labeled stit model violates label-consistency, then it can happen that a given agent cannot distinguish two indices even though there is no action type that is available at both of them. In other words, a labeled stit model is label-consistent if and only if whenever a given agent cannot distinguish two indices that emanate from two given moments, there is an action type that she can execute that is consistent with each of these moments.Footnote ³⁹ As the reader can easily verify, there is a label-inconsistent static labeled stit frame that violates the semantic condition of uniformity of available action types even though the associated transform epistemic stit frame validates the formula $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi \rightarrow \mathsf {K}_i\Diamond [i\;\mathsf {stit}]\varphi $ . This is impossible for label-consistent static labeled stit frames:

Proposition 5.7. Let $\mathcal {F}$ be a label-consistent static labeled stit frame. Let $\mathcal {F}'$ be the transform epistemic stit frame of $\mathcal {F}$ . Then $\mathcal {F}$ satisfies the semantic condition of uniformity of available action types if and only if the following schema is valid on $\mathcal {F}'$ :

$$ \begin{align*} \Diamond\mathsf{K}_i[i\;\mathsf{stit}]\varphi\to\mathsf{K}_i\Diamond[i\;\mathsf{stit}]\varphi. \end{align*} $$

Let us finish with addressing the second issue, regarding the relation between (Unif-H) and (UAAT). In light of the above result, let us call the formula $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi \rightarrow \mathsf {K}_i\Diamond [i\;\mathsf {stit}]\varphi $ the (UAAT) schema. It is then interesting to investigate the logical relation between the (UAAT) schema and the schema for the uniformity of historical possibility property (Unif-H). It is fairly easy to see that the validity of the (Unif-H) schema entails the validity of the (UAAT) schema. It may, however, be surprising that the converse also holds:Footnote ⁴⁰

Proposition 5.8. Let $\mathcal {M}$ be an epistemic stit model. Then

1. 1. If $\mathcal {M}$ validates the schema (Unif-H) $\Diamond \mathsf {K}_i\varphi \to \mathsf {K}_i\Diamond \varphi $ , then $\mathcal {M}$ validates the schema (UAAT) $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi \to \mathsf {K}_i\Diamond [i\;\mathsf {stit}]\varphi $ ;

2. 2. If $\mathcal {M}$ validates the schema (UAAT) $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi \to \mathsf {K}_i\Diamond [i\;\mathsf {stit}]\varphi $ , then $\mathcal {M}$ validates the schema (Unif-H) $\Diamond \mathsf {K}_i\varphi \to \mathsf {K}_i\Diamond \varphi $ .

The above discussion yields a consideration that speaks in favour of dropping (Unif-H). The above proposition demonstrates that whenever (Unif-H) holds, then this entails that the condition of uniformity of available action types holds. It is standard to distinguish between games of complete information and games of incomplete information. The latter drop the assumption of uniformity of available action types. That is, games of incomplete information include scenarios where I may not know which action types are available to myself and others. Since Horty and Pacuit’s analysis of epistemic ability (and the treatment of abilities under imperfect information in ATEL) is based on the assumption of uniformity of available action types, it is unclear how this analysis can be applied or extended to abilities under incomplete information. From the perspective of our formalism, this yields the question of whether $\Diamond \mathsf {K}_i[i\;\mathsf {stit}]\varphi $ adequately expresses that an agent is able to $\varphi $ in the epistemic sense in epistemic stit models that violate (Unif-H). A detailed analysis of abilities under incomplete information within stit theory, and the particular question we raised, must be postponed to another occasion.