Notions of Instrumentality in Agency Logic

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. 1.

   The term used by Von Wright for this behaviour is ‘doing p’. We avoid this expression because we reserve ‘doing’ for actions, and use ‘producing’ for results.

2. 2.

   We want to stress that the term ‘expectation’ must not be regarded as an epistemic notion, such as knowledge. Although an agent can have expectations about the future, the agent might still have imperfect knowledge of these expected future states.

3. 3.

   The use of propositional constants in modal logic can be traced back at least to [1].

4. 4.

   The ‘independence of agents’ axiom is central to stit-logic; it ensures that when choices are made simultaneously, an agent cannot a priori limit the choices available to the others; see e.g. [4, pp. 217–218]. Axiom A6 allows for the possibility that an agent has contradictory expectations about the future which cannot be realized.

5. 5.

   For instance, suppose that at w it started raining and I decided to take a walk without bringing an umbrella with me. Thus, I am in a state \(w'\) such that in the future of \(w'\) I will very likely get wet; however, had I decided to bring an umbrella with me at w, I would have ended in a state \(w''\) such that in the future of \(w''\) I would not have got wet. Therefore, one can also say that in the actual future of the counterfactual state \(w''\) I would not have got wet.

6. 6.

   Future work can be devoted to extensions of the language of LAE including operators for concatenations and iterations of action-types, in the spirit of [7, 8].

7. 7.

   In the context of ‘next moment’ agency logic there is no need to assign atomic symbols to moment/history pairs, as observed in [6].

8. 8.

   Reference to histories provides a general framework suitable to express more complex notions related to indeterminism; for instance, one could add to the language of LAE an operator saying that something will always hold in one history passing through a given moment. Such an operator is not definable in terms of \(\square \) in infinite trees.

9. 9.

   Notice that, by definition, actual can be a partial function (a moment may have no actual successor even if an agent expects it to have some) and has some remarkable difference with the ‘thin red line’ function of the stit-logic literature [4]; indeed, the thin red line function assigns to each moment m a unique history to which m belongs (the actual history w.r.t. m), whereas actual assigns to m only its actual successor, if the latter exists. This solves some objections raised in [4] against the use of functions to represent actuality in branching-time; for instance, while there are problems of ‘thin red line inheritance’ among states related by <, there is no problem of ‘actual successor inheritance’, since any two states related by < have different actual successors (if any).

This work was funded by the WWTF project MA16-28.

Authors and Affiliations

1. Institute of Logic and Computation, TU Wien, Vienna, Austria

   Kees van Berkel & Matteo Pascucci

Corresponding authors

Correspondence to Kees van Berkel or Matteo Pascucci .

Editors and Affiliations

1. School of Computing and Information Systems, University of Melbourne, Melbourne, Australia

   Tim Miller

2. Department of Computer Science, University of Aberdeen, Aberdeen, UK

   Nir Oren

3. Artificial Intelligence Research Center (AIRC), National Institute of Advanced Industrial Science and Technology (AIST), Tokyo, Japan

   Yuko Sakurai

4. Artificial Intelligence Research Center (AIRC), National Institute of Advanced Industrial Science and Technology (AIST), Tsukuba, Japan

   Itsuki Noda

5. University of Otago, Dunedin, New Zealand

   Bastin Tony Roy Savarimuthu

6. Computer Science Department, New Mexico State University, Las Cruces, USA

   Tran Cao Son

Reprints and permissions

© 2018 Springer Nature Switzerland AG

Policies and ethics