Notions of Instrumentality in Agency Logic

Abstract

We present a logic of agency called LAE whose language includes propositional constants for actions and expectations. The logic is based on Von Wright’s theory of agency in general and his analysis of instrumentality in particular. An axiomatization of the logic, including an independence of agents axiom, is provided and soundness and completeness are shown with respect to its intended class of frames. The framework of LAE will allow us to formally define a manifold of concepts involved in agency theories, including Von Wright’s four elementary forms of action, the notion of forbearance and notions of instrumentality that make reference to an agent’s expectations.

1 Introduction

What do we mean when we ascribe agency to a human being? We most likely assert that this person has the ability to perform an action. This answer highlights two key aspects of agency: ability and action. A third key aspect of agency is that actions can be seen in most cases as means to an end; that is, as instruments. The present work provides a logical framework to reason about the interplay of these three aspects of agency. While the notions of ability and action have been formally addressed for the past few decades, the notion of instrumentality seems to have received minor attention in the literature thus far. Philosophical analyses of instrumentality as such are scarce, although the concept of ‘means to an end’ is paramount to any theory of agency. Despite these limitations, we believe that logical investigations around instrumentality should be established on firm philosophical grounds. The present work aims at providing a formal account of instrumentality within a framework of agency logic and will be largely based on ideas presented by Georg Henrik von Wright [13,14,15], who can be regarded as one of the founding fathers of the logic of action [2].

Two prominent formal frameworks have been developed for the last few decades with respect to the logical treatment of agency: stit-logic [4, 10] and propositional dynamic logic (PDL) [7, 8]. The main difference between the two approaches can be pinpointed as follows: in stit-logic the focus has been largely put on the formal treatment of (explicit) agents on the basis of available choices, whereas in PDL the focus has been put on the formal analysis of (explicit) actions, regarded as transitions between states. In this article we reconstruct both frameworks within a logic including propositional constants for actions and expectations called LAE (logic of actions and expectations); our contribution is related to previous proposals that aim either at extending one framework to include the other, such as [16], or at defining one framework within the other, such as [9]. Our main purpose is to use LAE in order to provide a formal definition of various notions of instrumentality that rely on Von Wright’s ideas. Special attention will be paid to how these notions interact with an agent’s expectations. The article is divided as follows: in Sect. 2 we present and elaborate on Von Wright’s ideas; in Sect. 3 we introduce the system LAE and prove its soundness and completeness. Finally, in Sect. 4, we formally specify the main notions of the theory of agency and instrumentality at issue.

2 A Theory of Agency and Instrumentality

2.1 Acting

To ‘bring about something’ and to ‘prevent something’ are essential characteristics of what it is to act. What is brought about is a state of affairs and, for that reason, to ‘see to it that p’ means that one acts “in such a manner that the state of affairs that p is the result of one’s action” [13, p. 37]. From this account it follows that acting is strongly related to the emergence of a particular result (perhaps not always the desired one). An account of action, hence, heavily depends on the notion of change.

A change is a transition from an initial state to an end-state. These transitions can be triggered by events in which agents play no role (e.g., a moon eclipse); however, in many cases they are triggered by an agent’s behaviour. In particular, an agent may decide to act or not to act in a certain way in a given circumstance and this behaviour may produce several different results (at least, in a non-deterministic world). For this reason, we say that an action triggers a set of possible transitions from an initial state to a set of end-states. To act, then, is to provoke a specific form of change: it is a change brought about by the interference of an agent with the “course of nature” [15, p. 36]; one can a posteriori say that if the agent had not acted, the course of history would have been different. This is what Von Wright calls the counterfactual element of action [13, p. 43].

In order to understand how a result p is related to an action, one also has to take into account whether p holds or not in the initial state. Indeed, an agent may bring about p in two ways: either the initial state is $\lnot p$ and the agent’s behaviour changes it to the result p, or the initial state is p and the agent prevents it from changing to $\lnot p$ [15, p. 42]. Summing up, the analysis in this section provides us with three main characteristics of action: (i) the initial state, (ii) the result of the agent’s behaviour (i.e., the end-state) and (iii) the counterfactual ‘course of nature’. Taking into account also the difference between p and $\lnot p$ as atomic results, Von Wright classifies four elementary forms of agent behaviour; the first two concern actions that ‘bring about’ something, the latter two are actions that ‘prevent’ something from happening [15, pp. 43–44]:

• producing p: constructively bringing p into ‘existence’ (Fig. 1a);¹

• destroying p: without the agent’s acting p would have ‘prevailed’ (Fig. 1b);

• preserving p: if the agent does not act, then p will ‘perish’ (Fig. 1c);

• suppressing p: if the agent does not act, then p will ‘emerge’ (Fig. 1d).

Fig. 1.

Von Wright’s four elementary types of action.

2.2 Actions

Up until now we have been talking about ‘acts’ without specification. Commonly, a distinction is made between two sorts of actions: actions described in an impersonal, generic way (e.g. ‘writing’) and concrete, individual instances of these generic actions, as performed by a particular agent at a particular time (e.g. ‘I am currently writing’). The former are frequently called ‘action-types’, whereas the latter can be named ‘action-tokens’. Following Von Wright, generic actions (i.e., types) can be regarded as ‘categories’ to which individual ‘cases’ (i.e., tokens) belong [15, p. 36].

Here we will generalize this account of actions by considering also negative actions and complex actions. This will enable us to speak of, for instance, the action-type ‘not opening the door’ and the action-type ‘not opening the door or closing the window’. Negative actions are usually not expressible in the language of propositional dynamic logic, but they are taken into account in other formal approaches to agency which make explicit reference to actions, such as [2] and [3]. We will regard both action-types and action-tokens as essential to our logic of agency: As was pointed out in the previous section, an agent’s behaviour at a particular state triggers a set of possible transitions and, therefore, represents an action-token. Moreover, as we will clarify in the next section, a proper notion of instrumentality makes reference to action-types; that is, in order to determine whether an action is a good instrument for a given purpose, one has to consider the outcomes of previous transitions triggered by actions of that type.

2.3 Instrumentality

Actions can be regarded as instrument serving a particular purpose; they are ‘means to an end’. For instance, ‘pressing Y on the keyboard’ and ‘pulling the handbrake of a car’ are respectively instruments to ‘confirm a procedure on a computer terminal’ and to ‘perform an emergency stop’. In this section several distinct forms of instrumentality will be presented that will be formally addressed in subsequent sections. As a philosophical basis, we will borrow from and extend Von Wright’s analysis of instrumental goodness, as presented in [14, pp. 19–40]. To avoid ambiguity, the term ‘proper instrument’ is here regarded as an appropriate synonym for ‘good instrument’ and they will be used interchangeably.

Let us call an intended state of affairs $\phi$ a purpose and an action $\varDelta$ an instrument. Paraphrasing Von Wright, an action $\varDelta$ will qualify as a $\phi$-instrument if and only if $\varDelta$ can serve the purpose $\phi$ [14, p. 21]. It is also important to distinguish between instruments that can serve the purpose $\phi$ simpliciter and those that can serve $\phi$ well. The former will be called $\phi$-instruments and the latter proper $\phi$-instruments.

To qualify a particular instrument suitable for a particular purpose, we base our judgment on past performance; for example, with respect to questions of instrumentality we often make remarks such as ‘it has worked before’ and ‘it has never disappointed me (thus far)’. In the first case, we recognize a weak criterion; that is, the instrument has served the purpose at least once and, for that reason, it can serve the purpose. In the latter case, we identify a stronger criterion for instrumentality; that is, there have been applications of the instrument and these applications have always served the purpose and, for that reason, the instrument serves the purpose well. Hence, notions of instrumentality are based on past experience. This experience, subsequently, can be either impersonal or personal (e.g., ‘this machine has been tested’ or ‘I have used this tool before’). Thus far, we established two definitions of impersonal instrumentality:

• (1) agent-independent basic instrumentality: action-type $\varDelta$ is a basic $\phi$-instrument if and only if $\varDelta$ has served the purpose $\phi$ at least once in the past.

• (2) agent-independent proper instrumentality: action-type $\varDelta$ is a proper $\phi$-instrument if and only if (i) $\varDelta$ is a basic $\phi$-instrument and (ii) $\varDelta$ has always served the purpose $\phi$ in the past.

Hence, notions of instrumentality relate to both purpose and past performance. However, when we judge that ‘these scissors are a proper instrument for me to cut this piece of paper’, what do we mean? Von Wright briefly remarks that “judgments of instrumental goodness, usually, even if not necessarily, contain a conjectural element” [14, p. 27]. In other words, practical statements about instrumentality also contain reference to expectations about the instrument’s future performance. Hence, agent-bound instrumentality is based on both (i) the past performance of particular action-tokens associated with a certain type and (ii) the expected continuation of this performance in the nearby future. In contrast to agent-independent statements of instrumentality, statements of this form will vary over agents. What is more, the conjectural element of expected performance does not guarantee any future result: the agent might simply be wrong [14, p. 27]. The fact that the instrument has served the purpose well in the past, does not guarantee that it will not fail in the future. In our formal framework we will strongly emphasize these fundamental aspects of agent-bound instrumentality by investigating different notions of instrumentality that are restricted by the agent’s expectations.

Lastly, we emphasize that expectations must be regarded as those future moments which the agent considers more likely to happen. An agent’s expectations about the nearby future are therefore a subset of all possible next moments. We will accordingly introduce a formal restriction on expectations in Sect. 3.²

From the above we derive two agent-bound definitions of instrumentality:

• (3) agent-bound basic instrumentality: An instrument $\varDelta$ is a basic $\phi$-instrument for agent $\alpha$ at moment m if and only if (i) $\varDelta$ is a basic $\phi$-instrument and (ii) $\alpha$ expects that $\varDelta$ will serve $\phi$ at m.

• (4) agent-bound proper instrumentality: An instrument $\varDelta$ is a proper $\phi$-instrument for agent $\alpha$ at moment m if and only if (i) $\varDelta$ is a proper $\phi$-instrument and (ii) $\alpha$ expects that $\varDelta$ will serve $\phi$ at m.

The agent-independent and agent-dependent notions of instrumentality (1)–(4) will be formally addressed in Sect. 4.

In passing, ability can be regarded as an abstract form of agentive instrumentality; namely, saying that ‘an agent is able to behave in a certain way which guarantees a result’ is an abstraction of saying that ‘there exists an instrument (action) which the agent can successfully employ to obtain that result’. Moreover, saying that an agent $\alpha$ is able to obtain $\phi$ through an action $\varDelta$, given that $\varDelta$ has always led $\alpha$ to $\phi$ in the past, is essentially the same as saying that $\alpha$ excels at performing $\varDelta$ to obtain $\phi$. In this sense, Von Wright’s concept of ability, ‘being good at something’, is strongly related to our concept of agent-bound proper instrumentality (cf. the analysis of ‘technical goodness’ as ability and skill in [14, pp. 32–39]).

3 The System LAE

We start our formal presentation with a boolean algebra of actions and subsequently introduce the language of the logic LAE, in which the performance of an action by an agent will be represented by a formula. Let $Action=\{\delta _1,..., \delta _n\}$ be a finite set of atomic action-types. The set $Action^*$ of complex action-types is defined by the following BNF:

$$\begin{aligned} \varDelta \ {::}{=} \ \delta _i | \varDelta \cup \varDelta | \overline{\varDelta } \end{aligned}$$

where $\delta _i\in Action$. The operations $\cup$ and — are respectively used to form disjunctions of action-types (e.g., ‘turning-left or turning-right’) and negations of action-types (e.g., ‘not turning-right’). If $Agent=\{\alpha _1,...,\alpha _m\}$ is a finite set of agent constants, an agent-bound action-type is an expression of kind $\varDelta ^{\alpha _i}$, where $\varDelta \in Action^*$ and $\alpha _i\in Agent$. Let $Var=\{p_1,p_2,p_3,...\}$ be a countable set of propositional variables; furthermore, for any $\alpha _i\in Agent$, let $Wit^{\alpha _i}=\{\mathfrak {d}^{\alpha _i}_1,...,\mathfrak {d}^{\alpha _i}_n\}$ be a set of propositional constants respectively witnessing the performance of the atomic action-types $\delta _1$, ..., $\delta _n$ by $\alpha _i$ and let $\mathfrak {e}^{\alpha _i}$ be a propositional constant witnessing the compatibility of a state with $\alpha _i$’s expectations.³ Notice that $|Wit^{\alpha _i}|=|Action|=n$. The set $\bigcup _{\alpha _i\in Agent}Wit^{\alpha _i}$ can be simply denoted by Wit. The language $\mathcal {L}$ is defined by the following BNF:

$$\begin{aligned} \phi \ {::}{=} \ p_i |\mathfrak {e}^{\alpha _j}| \mathfrak {d}_i^{\alpha _j} | \lnot \phi | \phi \rightarrow \phi | \square \phi | N\phi \end{aligned}$$

for any $p_i\in Var$, $\alpha _j\in Agent$ and $\mathfrak {d}^{\alpha _j}_i\in Wit$. We can read $\square \phi$ as ‘in all successor states $\phi$ is the case’ and $N\phi$ as ‘in the actual successor state $\phi$ is the case’. We use standard definitions for additional boolean and modal operators. For instance, $\lozenge \phi$ abbreviates $\lnot \square \lnot \phi$ and means ‘in some successor state $\phi$ is the case’. Expressions like $\mathfrak {e}^{\alpha _j}$ and $\mathfrak {d}_i^{\alpha _j}$ mean respectively ‘the most recent expectations of agent $\alpha _j$ are met’ and ‘agent $\alpha _j$ has just performed action $\delta _i$’. The set of atomic propositional symbols in $\mathcal {L}$ is $Atom=Var\cup Wit\cup \{\mathfrak {e}^{\alpha _j}:\alpha _j\in Agent\}$.

Let t be a translation function mapping agent-bound action-types to formulas of $\mathcal {L}$ as below:

• for any $\delta _i\in Action$ and $\alpha _j\in Agent$, $t(\delta _i^{\alpha _j})=\mathfrak {d}_i^{\alpha _j}$,

• for any $\varDelta \in Action^*$ and $\alpha _i\in Agent$, $t(\overline{\varDelta ^{\alpha _i}})=\lnot t(\varDelta ^{\alpha _i})$;

• for any $\varDelta ,\varGamma \in Action^*$ and $\alpha _i,\alpha _j\in Agent$, $t(\varDelta ^{\alpha _i}\cup \varGamma ^{\alpha _j})= t(\varDelta ^{\alpha _i})\vee t(\varGamma ^{\alpha _j})$.

Let LAE be the system specified below:

• A0 if $\phi$ is a propositional tautology, then $\vdash _{LAE}\phi$;

• R0 $\phi ,\phi \rightarrow \psi \vdash _{LAE}\psi$;

• A1 $\square (\phi \rightarrow \psi )\rightarrow (\square \phi \rightarrow \square \psi )$;

• R1 if $\vdash _{LAE}\phi$, then $\vdash _{LAE}\square \phi$;

• A2 $N (\phi \rightarrow \psi )\rightarrow ( N \phi \rightarrow N \psi )$;

• A3 $\lnot N \phi \rightarrow N \lnot \phi$;

• A4 $\square \phi \rightarrow N \phi$;

• A5 for any list of (distinct) $\alpha _1,...,\alpha _n\in Agent$ and list of (non-necessarily distinct) $\varDelta _1,...,\varDelta _n\in Action^*$,

  $(\lozenge t(\varDelta _1^{\alpha _1})\wedge ...\wedge \lozenge t(\varDelta _n^{\alpha _n}))\rightarrow \lozenge (t(\varDelta _1^{\alpha _1})\wedge ...\wedge t(\varDelta _n^{\alpha _n}))$;

• A6 for any $\alpha _j\in Agent$, $\lozenge \mathfrak {e}^{\alpha _j}\rightarrow \lozenge \lnot \mathfrak {e}^{\alpha _j}$.

The most relevant axioms of the system S are A3, which guarantees that every state has a unique successor, A4, which says that the actual successor of a state is within the set of its successors, A5, which represents the stit-logic principle known as independence of agents, and A6, which ensures that agents never expect all possible future state-of-affairs to happen (if at a given state there are successor states satisfying an agent’s expectations, then there are also successor states not satisfying the expectations).⁴ The semantics for LAE will clarify that none of these axioms implies that a state has successors. Thus, the system can be used to reason about scenarios in which there are final possible states. Furthermore, it is noteworthy that the principle of ‘independence of agents’ is compatible with a scenario in which an agent ends in a state that does not meet that agent’s (most recent) expectations.

We define the following additional operators:

• E1 for any $\varDelta \in Action^*$ and $\alpha _i\in Agent$,

  $[\varDelta ^{\alpha _i}]^{would}\phi =_{def}\square (t(\varDelta ^{\alpha _i})\rightarrow \phi )$;

• E2 for any $\varDelta \in Action^*$ and $\alpha _i\in Agent$,

  $[\varDelta ^{\alpha _i}]^{could}\phi =_{def}\square (t(\varDelta ^{\alpha _i})\rightarrow \phi )\wedge \lozenge t(\varDelta ^{\alpha _i})$;

• E3 for any $\varDelta \in Action^*$ and $\alpha _i\in Agent$,

  $[\varDelta ^{\alpha _i}]^{will}\phi =_{def}\square (t(\varDelta ^{\alpha _i})\rightarrow \phi )\wedge \lnot N\lnot t(\varDelta ^{\alpha _i})$.

We can read the formula $[\varDelta ^{\alpha _i}]^{would}\phi$ as ‘at the current state, by behaving in accordance with $\varDelta$, $\alpha _i$ would bring about $\phi$’. (Notice that this does not ensure that $\alpha _i$ is currently able to behave in accordance with $\varDelta$.) The formula $[\varDelta ^{\alpha _i}]^{could}\phi$ means ‘at the current state, by behaving in accordance with $\varDelta$, $\alpha _i$ would bring about $\phi$ and $\alpha _i$ could (i.e., is able to) behave in accordance with $\varDelta$’. Finally, the formula $[\varDelta ^{\alpha _i}]^{will}\phi$ means ‘at the current state, by behaving in accordance with $\varDelta$, $\alpha _i$ would bring about $\phi$ and $\alpha _i$ will actually behave in accordance with $\varDelta$’.

A relational frame to interpret the language $\mathcal {L}$ is an ordered tuple $\mathfrak {F}=\langle W,\{W_{\mathfrak {d}_i^{\alpha _j}}:\mathfrak {d}_i^{\alpha _j}\in \mathcal {L}\}, \{W_{\mathfrak {e}^{\alpha _j}}:\mathfrak {e}^{\alpha _j}\in \mathcal {L}\}, R, R_N\rangle$, where $W=\{w_1,w_2,w_3,...\}$ is a set of states, each $W_{\mathfrak {d}_i^{\alpha _j}}$ and each $W_{\mathfrak {e}^{\alpha _j}}$ is a subset of W and R and $R_N$ are binary relations over W. The relation R captures the idea of a transition from a state to one of its immediate successors. As we pointed out in Sect. 2, a transition can be triggered by any event and so it does not require, in general, an active interference of an agent. The relation $R_N$ represents transitions in the course of events that can be considered actual with respect to a given state; namely, we have $wR_Nu$ only if u is an immediate successor of w and belongs to the actual future of w. Thus, the notion of actual future is state-dependent. This allows one to reason about the actual future of counterfactual states as well.⁵

A relational model to interpret $\mathcal {L}$ is an ordered tuple $\mathfrak {M}=\langle \mathfrak {F}, V\rangle$ where $\mathfrak {F}$ is a relational frame and V is a valuation function which maps atomic propositional symbols to sets of states and satisfies the following conditions:

• $V(\mathfrak {d}_i^{\alpha _j})= W_{\mathfrak {d}_i^{\alpha _j}}$, for any $\mathfrak {d}_i^{\alpha _j}\in \mathcal {L}$;

• $V(\mathfrak {e}^{\alpha _j})= W_{\mathfrak {e}^{\alpha _j}}$, for any $\mathfrak {e}^{\alpha _j}\in \mathcal {L}$.

Thus, propositional constants have the same interpretation in all models over a frame. Formulas of $\mathcal {L}$ are evaluated at a state of a model in the customary way. Truth-conditions are defined as follows:

• $\mathfrak {M}, w\vDash \chi$ iff $w\in V(\chi )$, for any $\chi \in Atom$;

• $\mathfrak {M},w\vDash \lnot \phi$ iff $\mathfrak {M}, w\nvDash \phi$;

• $\mathfrak {M}, w\vDash \phi \rightarrow \psi$ iff $\mathfrak {M}, w\nvDash \phi$ or $\mathfrak {M}, w\vDash \psi$;

• $\mathfrak {M}, w\vDash \square \phi$ iff for all $v\in W$ s.t. wRv we have $\mathfrak {M},v\vDash \phi$;

• $\mathfrak {M}, w\vDash N \phi$ iff for all $v\in W$ s.t. $w R_N v$, we have $\mathfrak {M},v\vDash \phi$.

Let $\mathfrak {F},w\vDash \phi$ mean that $\mathfrak {M},w\vDash \phi$ for all models $\mathfrak {M}$ over the frame $\mathfrak {F}$. The notion of validity of a formula with respect to (w.r.t.) a model, a frame, a class of models and a class of frames is defined in the standard way. Finally, for a given formula $\phi \in \mathcal {L}$, let $||\phi ||^\mathfrak {M}=\{w\in W:\mathfrak {M},w\vDash \phi \}$ and $||\phi ||^\mathfrak {F}=\{w\in W:\mathfrak {F},w\vDash \phi \}$. Due to the fixed interpretation of propositional constants and the definition of the translation function t, we have that, given a frame $\mathfrak {F}$ and an arbitrary model $\mathfrak {M}$ over it:

• $||t(\varDelta ^{\alpha _i})||^\mathfrak {F}=||t(\varDelta ^{\alpha _i})||^\mathfrak {M}$, for any $\varDelta \in Action^*$ and any $\alpha _i\in Agent$.

Let $C_f$ be the class of all frames satisfying the following properties:

• p(A3) for all $w\in W$, if there is $u\in W$ s.t. $wR_Nu$, then for all $v\in W$ s.t. $wR_Nv$, we have $v=u$;

• p(A4) for all $w,v\in W$, if $w R_N v$, then wRv;

• p(A5) for all $w\in W$ and for all lists of distinct agents $\alpha _1,...,\alpha _n$, if there are (non-necessarily distinct) action-types $\varDelta _1,...,\varDelta _n$ s.t. for $1\le i \le n$ there is $u_i\in W$ s.t. $wR u_i$ and $u_i\in ||t(\varDelta _i^{\alpha _i})||^\mathfrak {F}$, then there is $v\in W$ s.t. wRv and $v\in ||t(\varDelta _1^{\alpha _1})||^\mathfrak {F}\cap ...\cap ||t(\varDelta _n^{\alpha _n})||^\mathfrak {F}$;

• p(A6) for all $w\in W$ and $\alpha _j\in Agent$, if there is $v\in W$ s.t. wRv and $v\in ||\mathfrak {e}^\mathfrak {\alpha _j}||^\mathfrak {F}$, then there is also $u\in W$ s.t. wRu and $u\notin ||\mathfrak {e}^\mathfrak {\alpha _j}||^\mathfrak {F}$.

The class $C_f$ is non-empty. Indeed, the following is a very simple frame belonging to it: $\mathfrak {F}=\langle W,\{W_{\mathfrak {d}_i^{\alpha _j}}:\mathfrak {d}_i^{\alpha _j}\in \mathcal {L}\}, \{W_{\mathfrak {e}^{\alpha _j}}:\mathfrak {e}^{\alpha _j}\in \mathcal {L}\}, R, R_N\rangle$, where $W=\{w_1,w_2\}$, $W_{\mathfrak {d}_i^{\alpha _j}}=\{w_2\}$ for any $\mathfrak {d}_i^{\alpha _j}\in \mathcal {L}$, $W_{\mathfrak {e}^{\alpha _j}}=\emptyset$ for any $\mathfrak {e}^{\alpha _j}\in \mathcal {L}$ and $R= R_N=\{(w_1,w_2)\}$. It is straightforward to verify that p(A3)-p(A6) are satisfied by $\mathfrak {F}$.

Theorem 1

The system LAE is sound w.r.t. the class $C_f$.

Proof

Axioms A0, A1 and A2 are valid in all relational frames and rules R0 and R1 preserve validity in all relational frames. In the case of A3, take an arbitrary frame $\mathfrak {F}\in C_f$ and a model $\mathfrak {M}$ over it. Assume $\mathfrak {M},w\vDash \lnot N\phi$ for some $w\in W$; from this we can infer that there is $v\in W$ s.t. $wR_Nv$ and $\mathfrak {M},v\vDash \lnot \phi$; by p(A3), it follows that for all $u\in W$ s.t. $wR_N u$, $u=v$. Therefore, $\mathfrak {M},w\vDash N\lnot \phi$. In the case of A4, assume $\mathfrak {M},w\vDash \square \phi$; then, for all $v\in W$ s.t. wRv we have $\mathfrak {M},v\vDash \phi$. By p(A4), we can infer that for all $u\in W$ s.t. $wR_Nu$ we have $\mathfrak {M},u\vDash \phi$. Hence, $\mathfrak {M},w\vDash N\phi$. In the case of A5, let, for some distinct $\alpha _1,...,\alpha _n\in Agent$ and some (non-necessarily distinct) $\varDelta _1,...,\varDelta _n\in Action^*$, $\mathfrak {M},w\vDash \lozenge t(\varDelta ^{\alpha _1}_1) \wedge ... \wedge \lozenge t(\varDelta ^{\alpha _n}_n)$. From this we can infer that there are (non-necessarily distinct) $v_1,...,v_n\in W$ s.t., for $1\le i\le n$, $wRv_i$ and $v_i\in || t(\varDelta ^{\alpha _i}_i)||^\mathfrak {F}$. By p(A5), we can infer that there is $u\in W$ s.t. wRu and $u\in || t(\varDelta ^{\alpha _1}_1)||^\mathfrak {F}\cap ...\cap ||t(\varDelta ^{\alpha _n}_n)||^\mathfrak {F}$. Hence, $\mathfrak {M},w\vDash \lozenge (t(\varDelta ^{\alpha _1}_1) \wedge ...\wedge t(\varDelta ^{\alpha _n}_n))$. In the case of A6, assume $\mathfrak {M},w\vDash \lozenge \mathfrak {e}^{\alpha _j}$ for some $\mathfrak {e}^{\alpha _j}\in \mathcal {L}$. Then, there is $v\in W$ s.t. wRv and $\mathfrak {M},v\vDash \mathfrak {e}^{\alpha _j}$. By p(A6), we can infer that there is $u\in W$ s.t. wRu and $\mathfrak {M},u\vDash \lnot \mathfrak {e}^{\alpha _j}$; hence, $\mathfrak {M},w\vDash \lozenge \lnot \mathfrak {e}^{\alpha _j}$.

Let $\mathfrak {F}^{LAE}$ be the canonical frame for LAE, defined as follows:

• $W^{LAE}$ is the set of all maximally LAE-consistent sets of formulas;

• for any $w,v\in W^{LAE}$, $w R^{LAE} v$ iff $\{\phi :\square \phi \in w\}\subseteq v$;

• for any $w,v\in W^{LAE}$, $w R_N^{LAE} v$ iff $\{\phi : N \phi \in w\}\subseteq v$;

• for any $\mathfrak {d}_i^{\alpha _j}\in \mathcal {L}$, $W^{LAE}_{\mathfrak {d}_i^{\alpha _j}}=\{w\in W^{LAE}:\mathfrak {d}_i^{\alpha _j}\in w\}$;

• for any $\mathfrak {e}^{\alpha _j}\in \mathcal {L}$, $W^{LAE}_{\mathfrak {e}^{\alpha _j}}=\{w\in W^{LAE}:\mathfrak {e}^{\alpha _j}\in w\}$.

The canonical model for LAE, denoted by $\mathfrak {M}^{LAE}$, is obtained by adding a valuation function $V^{LAE}$ s.t.:

• for any $\chi \in Atom$, $V^{LAE}(\chi )=\{w\in W^{LAE}:\chi \in w\}$.

Any alternative valuation function V on the canonical frame must satisfy the aforementioned restrictions on propositional constants (namely, $V(\mathfrak {d}_i^{\alpha _j})=W^{LAE}_{\mathfrak {d}_i^{\alpha _j}}$, etc.). By usual properties of canonical models, for any formula $\phi \in \mathcal {L}$ and any state $w\in W^{LAE}$, we have $\mathfrak {M}^{LAE},w\vDash \phi$ iff $\phi \in w$.

The following theorem illustrates some properties of the frame $\mathfrak {F}^{LAE}$.

Theorem 2

Let $R^{LAE}_{\varDelta ^{\alpha _i}}$ be a binary relation over $W^{LAE}$ s.t., for any $w,v\in W^{LAE}$, $wR^{LAE}_{\varDelta ^{\alpha _i}}v$ iff $\{\phi :[\varDelta ^{\alpha _i}]^{would}\phi \in w\}\subseteq v$; we show some of the properties of this relation:

• (I) $R^{LAE}_{\varDelta ^{\alpha _i}}\subseteq R^{LAE}$;

• (II) $R^{LAE}_{\varDelta ^{\alpha _i}\cup \varGamma ^{\alpha _j}}= R^{LAE}_{\varDelta ^{\alpha _i}}\cup R^{LAE}_{\varGamma ^{\alpha _j}}$;

• (III) $R^{LAE}_{\overline{\varDelta ^{\alpha _i}}}=R^{LAE}\cap \overline{R^{LAE}_{\varDelta ^{\alpha _i}}}$.

Proof

Let w be an arbitrary world in the canonical model of LAE.

(I) Assume $wR^{LAE}_{\varDelta ^{\alpha _i}}v$; then, $\{\phi :[\varDelta ^{\alpha _i}]^{would}\phi \in w\}\subseteq v$. Furthermore, let $\lnot (wR^{LAE} v)$; then there is $\square \psi \in w$ s.t. $\psi \notin v$. From this and ordinary modal reasoning it follows that $\square (t(\varDelta ^{\alpha _i}) \rightarrow \psi )\in w$ and $[\varDelta ^{\alpha _i}]^{would}\psi \in w$, so $\psi \in v$, which represents a contradiction.

(II) Assume $w R^{LAE}_{\varDelta ^{\alpha _i}\cup \varGamma ^{\alpha _j}}v$. Then, $\{\phi :[\varDelta ^{\alpha _i}\cup \varGamma ^{\alpha _j}]^{would}\phi \in w\} \subseteq v$, which entails $\{\phi :\square ((t(\varDelta ^{\alpha _i})\vee t(\varGamma ^{\alpha _j})) \rightarrow \phi )\in w\}\subseteq v$ and $\{\phi :\square (t(\varDelta ^{\alpha _i})\rightarrow \phi ) \wedge \square (t(\varGamma ^{\alpha _j}) \rightarrow \phi )\in w\}\subseteq v$, so $\{\phi :[\varDelta ^{\alpha _i}]^{would}\phi \wedge [\varGamma ^{\alpha _j}]^{would} \phi )\in w\}\subseteq v$. Suppose $\lnot (w R^{LAE}_{\varDelta ^{\alpha _i}}\cup R^{LAE}_{\varGamma ^{\alpha _j}}v)$; then, there are $[\varDelta ^{\alpha _i}]^{would}\psi ,[\varGamma ^{\alpha _j}]^{would}\chi \in w$ s.t. $\psi ,\chi \notin v$. From this it follows that $\square (t(\varDelta ^{\alpha _i})\rightarrow \psi ), \square (t(\varGamma ^{\alpha _j})\rightarrow \chi )\in w$. Since $\square (t(\varDelta ^{\alpha _i})\rightarrow ( t(\varDelta ^{\alpha _i})\vee t(\varGamma ^{\alpha _j})))\wedge \square (t(\varGamma ^{\alpha _j})\rightarrow ( t(\varDelta ^{\alpha _i})\vee t(\varGamma ^{\alpha _j})))\in w$, then $t(\varDelta ^{\alpha _i})\vee t(\varGamma ^{\alpha _j})\in v$, which means that either $t(\varDelta ^{\alpha _i})\in v$ or $t(\varGamma ^{\alpha _j})\in v$. Since we know that $wR^{LAE}_{\varDelta ^{\alpha _i}\cup \varGamma ^{\alpha _j}}v$ entails $w R^{LAE} v$, then $\{\phi :\square \phi \in w\}\subseteq v$. This means that if $t(\varDelta ^{\alpha _i})\in v$, then $\psi \in v$; if $t(\varGamma ^{\alpha _j})\in v$, then $\chi \in v$. A contradiction arises in both cases.

Assume $\lnot (w R^{LAE}_{\varDelta ^{\alpha _i}\cup \varGamma ^{\alpha _j}} v)$; then, there is $[\varDelta ^{\alpha _i}\cup \varGamma ^{\alpha _j}]^{would}\psi \in w$ s.t. $\psi \notin v$. Therefore, $\square ((t(\varDelta ^{\alpha _i})\vee t(\varGamma ^{\alpha _j}))\rightarrow \psi )\in w$. Suppose $wR^{LAE} v$ (otherwise the intended result trivially follows); then, since $\square (\lnot \psi \rightarrow \lnot (t(\varDelta ^{\alpha _i})\vee t(\varGamma ^{\alpha _j})))\in w$, then $\lnot (t(\varDelta ^{\alpha _i})\vee t(\varGamma ^{\alpha _j}))\in v$, whence $\lnot t(\varDelta ^{\alpha _i}),\lnot t(\varGamma ^{\alpha _j})\in v$, so $\{\phi :[\varDelta ^{\alpha _i}]^{would}\phi \in w\}\nsubseteq v$ and $\{\phi :[\varGamma ^{\alpha _j}]^{would}\phi \in w\}\nsubseteq v$, hence $\lnot (w R^{LAE}_{\varDelta ^{\alpha _i}}\cup R^{LAE}_{\varGamma ^{\alpha _j}}v)$.

(III) Let $wR^{LAE}_{\overline{\varDelta ^{\alpha _i}}}v$; then, $\{\phi :[\overline{\varDelta ^{\alpha _i}}]^{would}\phi \in w\}\subseteq v$; we know that from this it is possible to infer $w R^{LAE} v$. Since $[\varDelta ^{\alpha _i}]^{would}t(\varDelta ^{\alpha _i}),[\overline{\varDelta ^{\alpha _i}}]^{would}\lnot t(\varDelta ^{\alpha _i})\in w$, then $\lnot t(\varDelta ^{\alpha _i})\in v$ and $t(\varDelta ^{\alpha _i})\notin v$, so $\lnot (w R^{LAE}_{\varDelta ^{\alpha _i}}v)$, which is $w\overline{R^{LAE}_{\varDelta ^{\alpha _i}}}v$, and $wR^{LAE}\cap \overline{R^{LAE}_{\varDelta ^{\alpha _i}}}v$.

Let $\lnot (wR^{LAE}_{\overline{\varDelta ^{\alpha _i}}}v)$; then, there is $[\overline{\varDelta ^{\alpha _i}}]^{would}\psi \in w$ s.t. $\psi \notin v$. Assume $wR^{LAE} v$; since $\square (\lnot t(\varDelta ^{\alpha _i})\rightarrow \psi )\in w$, then $\lnot t(\varDelta ^{\alpha _i})\rightarrow \psi \in v$, so $t(\varDelta ^{\alpha _i})\in v$. Let $[\varDelta ^{\alpha _i}]^{would}\chi \in w$; then, $\square (t(\varDelta ^{\alpha _i})\rightarrow \chi )\in w$ and $\chi \in v$; thus, $\{\phi :[\varDelta ^{\alpha _i}]^{would}\phi \in w\}\subseteq v$, which means $wR^{LAE}_{\varDelta ^{\alpha _i}}v$ and $\lnot (w R^{LAE}\cap \overline{R^{LAE}_{\varDelta ^{\alpha _i}}}v)$.

Theorem 3

The frame $\mathfrak {F}^{LAE}$ belongs to the class $C_f$.

Proof

We need to show that $\mathfrak {F}^{LAE}$ satisfies the properties p(A3)–p(A6). In the case of p(A3), suppose $wR^{LAE}_N v$, $wR^{LAE}_N u$ and $v\ne u$. Then, there is $\phi$ s.t. $\phi \in v$ and $\phi \notin u$. In the canonical model $\mathfrak {M}^{LAE}$ we have $\mathfrak {M}^{LAE},v\vDash \phi$ and $\mathfrak {M}^{LAE},u\vDash \lnot \phi$, so $\mathfrak {M}^{LAE},w\vDash \lnot N\phi$ and, by A3, $\mathfrak {M}^{LAE},w\vDash N\lnot \phi$, which entails $\mathfrak {M}^{LAE},v\vDash \lnot \phi$, whence $\phi ,\lnot \phi \in v$: contradiction. In the case of p(A4), suppose that $w R^{LAE}_N v$ and $\lnot w R^{LAE} v$. Then there is $\square \phi \in w$ s.t. $\phi \notin v$; however, by A4, $N\phi \in w$ and this entails $\lnot w R^{LAE}_N v$: contradiction. In the case of p(A5), suppose that for a list of distinct agents $\alpha _1,...,\alpha _n$ and for a list of (non-necessarily distinct) action-types $\varDelta _1,...,\varDelta _n$, we have that there are (non-necessarily distinct) worlds $u_1,..., u_n$ s.t., for $1\le i\le n$, $w R^{LAE} u_i$ and $u_i\in ||t(\varDelta ^{\alpha _i}_i)||^\mathfrak {F}$. Then, $w\in ||\lozenge t(\varDelta ^{\alpha _1}_1)||^\mathfrak {F}\cap ...\cap ||\lozenge t(\varDelta ^{\alpha _n}_n)||^\mathfrak {F}$, which entails $\lozenge t(\varDelta ^{\alpha _1}_1)\wedge ...\wedge \lozenge t(\varDelta ^{\alpha _n}_n)\in w$ and, by A4, we get $\lozenge (t(\varDelta ^{\alpha _1}_1)\wedge ...\wedge t(\varDelta ^{\alpha _n}_n))\in w$. Assume that there is no maximally LAE-consistent set v s.t. $\{\phi :\square \phi \in w\}\cup \{(t(\varDelta ^{\alpha _1}_1)\wedge ...\wedge t(\varDelta ^{\alpha _n}_n))\subseteq v$; then, $\vdash _{LAE} (\phi _1\wedge ...\wedge \phi _m)\rightarrow \lnot (t(\varDelta ^{\alpha _1}_1)\wedge ...\wedge t(\varDelta ^{\alpha _n}_n))$ for some $\phi _1,...,\phi _m\in \{\phi :\square \phi \in w\}$. From this one can infer $\vdash _{LAE} \square (\phi _1\wedge ...\wedge \phi _m)\rightarrow \square \lnot (t(\varDelta ^{\alpha _1}_1)\wedge ...\wedge t(\varDelta ^{\alpha _n}_n))$, so $\vdash _{LAE} ( \lozenge t(\varDelta ^{\alpha _1}_1)\wedge ...\wedge \lozenge t(\varDelta ^{\alpha _n}_n) \wedge \square (\phi _1\wedge ...\wedge \phi _m))\rightarrow \lnot \lozenge (t(\varDelta ^{\alpha _1}_1)\wedge ...\wedge t(\varDelta ^{\alpha _n}_n))$; however, this is impossible since we know that $\vdash _{LAE} ( \lozenge t(\varDelta ^{\alpha _1}_1)\wedge ...\wedge \lozenge t(\varDelta ^{\alpha _n}_n)) \rightarrow \lozenge (t(\varDelta ^{\alpha _1}_1)\wedge ...\wedge t(\varDelta ^{\alpha _n}_n))$. Hence, we can conclude that there is a maximally LAE-consistent set v s.t. $wR^{LAE}v$ and $v\in ||(t(\varDelta ^{\alpha _1}_1)||^\mathfrak {F}\cap ...\cap ||t(\varDelta ^{\alpha _n}_n))||^\mathfrak {F}$. In the case of p(A6), assume that $wR^{LAE}v$ and $v\in ||\mathfrak {e}^{\alpha _i}||^\mathfrak {F}$ for some $\mathfrak {e}^{\alpha _i}\in \mathcal {L}$; then, suppose that the set $\{\phi :\square \phi \in w\}\cup \{\lnot \mathfrak {e}^{\alpha _i}\}$ is not LAE-consistent. From this one can infer that $\vdash _{LAE}\square (\phi _1\wedge ...\wedge \phi _n)\rightarrow \lnot \lozenge \lnot \mathfrak {e}^{\alpha _i}$ for some $\phi _1,...,\phi _n\in \{\phi :\square \phi \in w\}$; hence, $\vdash _{LAE}(\square (\phi _1\wedge ...\wedge \phi _n)\wedge \lozenge \mathfrak {e}^{\alpha _i})\rightarrow \lnot \lozenge \lnot \mathfrak {e}^{\alpha _i}$, which contradicts A6. Then, there is a maximally LAE-consistent set u s.t. $\{\phi :\square \phi \in w\}\cup \{\lnot \mathfrak {e}^{\alpha _i}\}\subseteq u$, which means $u\in ||\lnot \mathfrak {e}^{\alpha _i}||^\mathfrak {F}$ and $wR^{LAE}u$.

An immediate consequence of Theorem 3 is that LAE is complete w.r.t. the class $C_f$; hence, together with Theorem 1, this entails that LAE is characterized by the class $C_f$. Furthermore, as a consequence of Theorem 2 and Theorem 3, the following schemata, which capture the properties of a boolean algebra of action-types, are provable in LAE:⁶

• T1 $[\varDelta ^{\alpha _i}\cup \varGamma ^{\alpha _j}]^{would}\phi \equiv [\varGamma ^{\alpha _j}\cup \varDelta ^{\alpha _i}]^{would}\phi$;

• T2 $[\varDelta ^{\alpha _i}\cup (\varGamma ^{\alpha _j}\cup \varSigma ^{\alpha _k})]^{would}\phi \equiv [(\varDelta ^{\alpha _i}\cup \varGamma ^{\alpha _j})\cup \varSigma ^{\alpha _k}]^{would}\phi$;

• T3 $[\overline{\overline{\varDelta ^{\alpha _i}}\cup \varGamma ^{\alpha _j}}\cup \overline{\overline{\varDelta ^{\alpha _i}}\cup \overline{\varGamma ^{\alpha _j}}}]^{would}\phi \equiv [\varDelta ^{\alpha _i}]^{would}\phi$.

We will now show that the system LAE is also characterized by a subclass of $C_f$ that includes only tree-like frames which resemble more familiar structures used in the literature for logics of agency, in particular, diverse stit-logics (e.g. [4, 6, 10, 16]). A branching-time frame with immediate successors is an ordered tuple $\mathfrak {F}= \langle T, \{T_{\mathfrak {d}_i^{\alpha _j}}:\mathfrak {d}_i^{\alpha _j}\in \mathcal {L}\}, \{T_{\mathfrak {e}^{\alpha _j}}:\mathfrak {e}^{\alpha _j}\in \mathcal {L}\},<\rangle$ where $T=\{m_1,m_2,m_3,...\}$ is a set of moments, each $T_{\mathfrak {d}_i^{\alpha _j}}$ and each $T_{\mathfrak {e}^{\alpha _j}}$ is a subset of T and < is a binary asymmetric, intransitive and backward linear relation over T, namely:

• $\forall m,m' \in T: (m<m' \rightarrow \lnot (m'<m))$;

• $\forall m,m',m'' \in T: ((m<m' \wedge m'<m'') \rightarrow \lnot (m<m''))$;

• $\forall m,m',m'' \in T: (m'<m \wedge m''<m) \rightarrow m'=m''$.

We define the usual machinery related to branching-time frames. Let $\ll$ be the transitive closure of <; then, T is partially ordered by $\ll$ and any $\ll$-maximal chain of moments can be called a history. Let H be the set of histories in a given branching-time frame $\mathfrak {F}$ and $H_m=\{h\in H:m\in h\}$ the set of all histories in $\mathfrak {F}$ ‘passing through’ a moment m. A model over a branching-time frame with immediate successors is an ordered tuple $\mathfrak {M}=\langle \mathfrak {F},V\rangle$, where $\mathfrak {F}$ is the underlying frame and V a valuation function mapping atomic propositional symbols to moments and satisfying the usual restrictions on propositional constants.⁷ Formulas of $\mathcal {L}$ are in this case evaluated with reference to a moment/history pair in a model.⁸ Let actual be a function which associates to a moment m the only successor of m (if any) which belongs to the actual future of m, then:⁹

• $\mathfrak {M}, (m/h) \vDash \chi$ iff $m\in V(\chi )$, for any $\chi \in Atom$;

• $\mathfrak {M}, (m/h)\vDash \lnot \phi$ iff $\mathfrak {M}, (m/h)\nvDash \phi$;

• $\mathfrak {M}, (m/h)\vDash \phi \rightarrow \psi$ iff $\mathfrak {M}, (m/h)\nvDash \phi$ or $\mathfrak {M}, (m/h)\vDash \psi$;

• $\mathfrak {M}, (m/h)\vDash \square \phi$ iff for all $m'\in T$ s.t. $m<m'$ and all $h'\in H_{m'}$ we have $\mathfrak {M},(m'/h')\vDash \phi$;

• $\mathfrak {M}, (m/h)\vDash N \phi$ iff $\mathfrak {M},(actual(m)/h')\vDash \phi$ for all $h'\in H_{actual(m)}$.

Notice that according to the definition of actual(m), if m has no actual successor, then $\mathfrak {M},(m/h)\vDash N\phi$ for every $\phi \in \mathcal {L}$. In order to formally specify a class of branching time frames with immediate successors contained in $C_f$, we define the relations R and $R_N$ in terms of moment/history pairs and the relation <, as follows:

• $(m/h)R (m'/h')$ iff $m< m'$, $h\in H_m$ and $h'\in H_{m'}$;

• $(m/h)R_{N} (m'/h')$ iff $m'=actual(m)$, $h\in H_m$ and $h'\in H_{m'}$.

The last two semantic clauses are then respectively equivalent to:

• $\mathfrak {M}, (m/h)\vDash \square \phi$ iff for all $(m'/h')$ s.t. $(m/h)R(m'/h')$, $\mathfrak {M},(m'/h')\vDash \phi$;

• $\mathfrak {M}, (m/h)\vDash N \phi$ iff for all $(m'/h')$ s.t. $(m/h) R_N (m'/h')$, $\mathfrak {M},(m'/h')\vDash \phi$.

Let us say that a branching-time frame with immediate successors is an lae-frame iff it satisfies the properties p(A3)-p(A6). The class of all lae-frames can be denoted by $C^{lae}_f$; clearly, $C^{lae}_f\subset C_f$. In order to claim that LAE is also characterized by $C^{lae}_f$, one needs to show that the additional properties of lae-frames cannot be forced by any formula of the language $\mathcal {L}$. But this follows from well-known results concerning the correspondence theory of propositional modal languages. We sketch the proof below, relying on notions illustrated in [5].

Theorem 4

For any $\phi \in \mathcal {L}$, if $C^{lae}_f\vDash \phi$, then $C_f\vDash \phi$.

Proof

By contraposition, assume that $\phi$ is not valid in some model $\mathfrak {M}$ over a frame $\mathfrak {F}$ in $C_f$. This means that for some world $w^*$ in the domain of $\mathfrak {M}$, we have $\mathfrak {M},w^*\vDash \lnot \phi$. Let $\mathfrak {M}'$ be the submodel of $\mathfrak {M}$ generated by $w^*$; then $\mathfrak {M}',w^*\vDash \lnot \phi$. $\mathfrak {M}'$ can be transformed into a model $\mathfrak {M}^t$ over an asymmetric, intransitive tree $\mathfrak {F}^t$ rooted in $w^*$, whose set of states $W^t$ consists of the sequences $\langle w_1,...,w_n\rangle$ s.t. $w_1,...,w_n\in W'$, $w_1=w^*$ and $w_1 R' w_2,..., w_{n-1}R'w_n$ ($W'$ and $R'$ being respectively the domain and the accessibility relation associated with $\square$ in $\mathfrak {M}'$) and whose relations $R^t$ and $R^t_N$ are defined as follows:

• for any $u,v{\in } W^t$, $u R^tv$ iff $u{=}\langle w_1,...,w_n\rangle$, $v{=}\langle w_1,...,w_n,w_{n+1}\rangle$ and $w_n R' w_{n+1}$;

• for any $u,v{\in } W^t$, $u R_N^tv$ iff $u{=}\langle w_1,...,w_n\rangle$, $v{=}\langle w_1,...,w_n,w_{n+1}\rangle$ and $w_n R'_N w_{n+1}$.

Let $\varPi$ be a function from $W'$ to $\wp (W^t)$ s.t. $\varPi (u)=\{\langle w_1,...,w_n\rangle :w_n=u\}$; then, for all $u\in W'$ and all $\psi \in \mathcal {L}$ we have $\mathfrak {M}',u\vDash \psi$ iff $\mathfrak {M}^t,x\vDash \psi$ for every $x\in \varPi (u)$. Therefore, since $\varPi (w^*)\supseteq \{w^*\}$, we get $\mathfrak {M}^t,w^*\vDash \lnot \phi$. Finally, let $H^t$ be the set of histories in $\mathfrak {M}^t$; transform $\mathfrak {M}^t$ into a model $\mathfrak {M}^{fin}$ obtained by replacing every state $u\in W^t$ with a state $u_\sim =\{(w/h): u\in \varPi (w)$ and $h\in H^t_u\}$. Define a binary relation $<^{fin}$ over $W^{fin}$ s.t. $u_\sim <^{fin} v_\sim$ iff $u R^t v$; it follows that, for all $u_\sim \in W^{fin}$, $H^{fin}_{u_\sim }= H^t_u$. Let $R^{fin}$ and $R^{fin}_N$ be defined in terms of $<^{fin}$ as in branching-time frames with immediate successors, where $actual(w_\sim )= w'_\sim$ iff $w R^t_N w'$. $\mathfrak {M}^{fin}$ is a model over an lae-frame by construction. It can be easily proved that for all $u\in W^t$ and all $\psi \in \mathcal {L}$, we have $\mathfrak {M}^t,u\vDash \psi$ iff $\mathfrak {M}^{fin}, (w/h)\vDash \psi$ for every $(w/h)\in u_\sim$ iff $\mathfrak {M}^{fin}, u_\sim \vDash \psi$, hence $\mathfrak {M}^{fin},w^*_\sim \vDash \lnot \phi$.

We conclude with some theorems of LAE involving the operators in $E1-E3$:

• T4 $([\varDelta _1^{\alpha _1}]^{could} \phi _1 \wedge ... \wedge [\varDelta _n^{\alpha _n}]^{could}\phi _n)\rightarrow [\varDelta _1^{\alpha _1} \cap ...\cap \varDelta _n^{\alpha _n}]^{could}(\phi _1 \wedge ... \wedge \phi _n)$, where $\alpha _1$,...,$\alpha _n$ are distinct;

• T5 $[\varDelta ^{\alpha _i}]^{could}\phi \rightarrow \lnot [\varDelta ^{\alpha _i}]^{could}\lnot \phi$;

• T6 $[\varDelta ^{\alpha _i}]^{will}\phi \rightarrow \lnot [\varDelta ^{\alpha _i}]^{will}\lnot \phi$;

• T7 $[\varDelta ^{\alpha _i}]^{will} \phi \rightarrow [\varDelta ^{\alpha _i}]^{could}\phi$;

• T8 $[\varDelta ^{\alpha _i}]^{could}\phi \rightarrow [\varDelta ^{\alpha _i}]^{would}\phi$.

T4 expresses the familiar ‘independence of agents’ principle in its agency appearance; T4 equivalents for ‘will’ and ‘would’ are also provable in LAE. T5 and T6 express that the defined operators for ‘could’ and ‘will’ behave in accordance with seriality. Clearly, we do not have a T5 equivalent for ‘would’. T7 and T8 are bridge-theorems that express the relations between ‘will’, ‘could’ and ‘would’. Finally, notice that the operators in E1-E3 can be modified by taking into account also agents’ expectations, as illustrated below:

• $\mathfrak {M}, (m/h)\vDash [\varDelta ^{\alpha _i}]^{would}_{ex} \phi$ iff $\mathfrak {M}, (m/h)\vDash \square ((t(\varDelta ^{\alpha _i}) \wedge \mathfrak {e}^{\alpha _i}) \rightarrow \phi )$;

• $\mathfrak {M}, (m/h)\vDash [\varDelta ^{\alpha _i}]^{could}_{ex} \phi$ iff $\mathfrak {M}, (m/h)\vDash \square ((t(\varDelta ^{\alpha _i}) \wedge \mathfrak {e}^{\alpha _i}) \rightarrow \phi )$ and $\mathfrak {M}, (m/h)\vDash \lozenge ( t(\varDelta ^{\alpha _i}) \wedge \mathfrak {e}^{\alpha _i})$;

• $\mathfrak {M}, (m/h)\vDash [\varDelta ^{\alpha _i}]^{will}_{ex} \phi$ iff $\mathfrak {M}, (m/h)\vDash \square ((t(\varDelta ^{\alpha _i}) \wedge \mathfrak {e}^{\alpha _i}) \rightarrow \phi )$ and $\mathfrak {M}, (actual(m)/h')\vDash t(\varDelta ^{\alpha _i}) \wedge \mathfrak {e}^{\alpha _i}$ for all $h'\in H_{actual(m)}$.

4 Discussion and Final Remarks

Performing Actions. Several concepts pertaining to the theory of agency introduced in this paper can be formally specified within the syntactical and semantic framework of the logic LAE. Recall (Sect. 2) that, by making reference to initial states, end-states, and counterfactual states, Von Wright derives four elementary forms of action: producing, destroying, preserving and suppressing. Although a formal approach to these terms is not new (cf. [2, 11]), the logic LAE allows us to expand them to more complex notions interacting with actions, expectations, instrumentality and ability:

The above formulae allow us to make explicit reference to the instruments that lead to producing, destroying, preserving and suppressing p, respectively. (Notice that (a)–(d) refer to atomic results.) We provide the intuitive reading of (a), the others will be similar: ‘at the current state, by behaving in accordance with $\varDelta$, $\alpha _i$ produces p’ means that ‘(i) $\lnot p$ is currently the case; (ii) $\alpha$ actually behaves in accordance with $\varDelta$; (iii) p will actually be the case immediately after and (iv) $\lnot p$ could otherwise be the case immediately after’.

Von Wright’s reading of the four actions is stronger than ours, since he represents them in a binary setting: through agent $\alpha$’s conduct p will be the case, whereas through $\alpha$’s not-acting $\lnot p$ would be the case. We believe that this account is too strong: it gives the agent $\alpha$ complete power over the faith of p. Definitions (a)–(d), instead, exemplify that $\alpha$ has the capability of determining the faith of p with some behaviour $\varDelta$, but cannot determine the faith of p through not acting.

Furthermore, observe that in our framework we can also redefine these four elementary actions in terms of could and would, as well as with reference to an agent’s expectations. For the sake of discussion, we only provide the definition of ‘agent $\alpha$ could destroy p by behaving in accordance with $\varDelta$’:

Definitions (a)–(d) entail that propositions true at every next state, can neither be brought about nor prevented by any agent. Such definitions can therefore be seen as strong notions of deliberative action (cf. ‘dstit’ in [10]). This result brings us to the concept of forbearance (omission). Following Von Wright [15, p. 45], to forbear is stronger than to merely not act. In fact, it presupposes the ability to perform what is forborne. We introduce the following definition:

Forbearance explicitly refers to actions: the usage of $\top$ (i.e., ‘tautology’) in (e) refers to the possibility to behave in accordance with action $\varDelta$ and is interpreted as ‘agent $\alpha$ forbears to behave in accordance with $\varDelta$’ if and only if ‘$\alpha$ could behave in accordance with $\varDelta$, but will behave in accordance with $\overline{\varDelta }$ instead’.

Definitions (a)–(e) can be easily extended to formal notions of forbearance relating to results. We only illustrate the notion of ‘forbearing to destroy p’:

Instrumentality. In Sect. 2 we made a distinction between weak and strong concepts of instrumentality, as well as agent-independent and agent-bound concepts. We will now provide their formalizations in the framework of LAE:

Definitions (f) and (g) employ the will-operator to ensure that, in the past, $\phi$ has been the actual result of behaviour in accordance with $\varDelta$ and not just the result of lucky coincidence. Furthermore, (f) and (g) express instrumentality independent of past expectations. Moreover, (g) requires that, everywhere in the past, behaviour in accordance with $\varDelta$ would have led to $\phi$.

Definitions (h) and (i), instead, introduce respectively weak and strong agent-bound notions of instrumentality, the difference with the former two is that (h) and (i) consist of both future expectations and past experience: the agent expects the continuation of the instrument’s past performance. We don’t limit past experience to past expectations since an agent might discover concrete rules of instrumentality through the experience of unexpected results and actions. Observe that agent-bound instrumentality is defined through all three terms ‘could’, ‘will’ and ‘would’, relating respectively to ‘the present state’, ‘a past state’ and ‘all past states’. Lastly, we emphasize that all formal definitions (f)–(i) allow for the agent to be disenchanted; that is, even proper-instruments might presently fail to lead to the intended result and agents might end in a state in which their expectations are not met.

In conclusion, taking both agent-dependent expectations and actions as the basis of our logic of agency we were able to construct three different notions of agency: would, could and will, each with its corresponding expectation-variant. Together, these concepts were sufficient to address several extensions of Von Wright’s elementary actions, including forbearance, as well as several formal definitions of instrumentality. As a final remark, we mention that both the process of generalizing actions and deriving notions of instrumentality are associated with induction and, for that reason, with the problems that come with it. Here, we only accentuate that the above formalization is in line with Von Wright’s division of the problem of induction into two distinct problems [12]. First, there is the problem of justifying whether generalized statements are true for all observed cases (i.e., with respect to the past). This part is formally represented by definition (g). Secondly, there is the problem of using these generalized statements for future predictions. Von Wright remarks that here we seem to be satisfied with something less stringent: “Scarcely anybody would pretend that predictions, even when based upon the safest inductions, might not fail sometimes” [12, p. 51]. The latter is captured through the formal behaviour of expectations in LAE and the first clauses of definitions (h) and (i).