Emiliano Lorini
email: lorini@irit.fr

Temporal STIT logic and its application to normative reasoning

Keywords: STIT logic, temporal logic, axiomatisation, deontic logic

I present a variant of STIT with time, called T-STIT (Temporal STIT), interpreted in standard Kripke semantics. On the syntactic level, T-STIT is nothing but the extension of atemporal individual STIT by: (i) the future tense and past tense operators, and (ii) the operator of group agency for the grand coalition (the coalition of all agents). A sound and complete axiomatisation for T-STIT is given. Moreover, it is shown that T-STIT supports reasoning about interesting normative concepts such as the concepts of achievement obligation and commitment.

Introduction

STIT logic (the logic of Seeing to it That; [START_REF] Belnap | Facing the future: Agents and choices in our indeterminist world[END_REF]) is one of the most prominent formal accounts of agency. It is the logic of sentences of the form 'the agent i sees to it that ϕ is true [START_REF] Horty | Agency and deontic logic[END_REF] extends the STIT logic of [START_REF] Belnap | Facing the future: Agents and choices in our indeterminist world[END_REF] with operators of group agency in order to express sentences of the form 'the group of agents C sees to it that ϕ is true '. Following Lorini and Schwarzentruber (2011), one might use the terms 'individual STIT logic' and 'group STIT logic' to designate respectively the STIT logic of [START_REF] Belnap | Facing the future: Agents and choices in our indeterminist world[END_REF] (in which only the actions of agents are described) and [START_REF] Horty | Agency and deontic logic[END_REF] variant of STIT logic (in which both actions of agents and joint actions of groups are represented).

The original semantics for STIT given by [START_REF] Belnap | Facing the future: Agents and choices in our indeterminist world[END_REF] is defined in terms of BT+AC structures: branching-time structures (BT) augmented by agent choice functions (AC). A BT structure is made of a set of moments and a tree-like ordering over them. An AC for a certain agent i is a function mapping each moment m into a partition of the set of histories passing through that moment, a history h being a maximal set of linearly ordered moments and the equivalence classes of the partition being the possible choices for agent i at moment m. As shown by [START_REF] Balbiani | Alternative axiomatics and complexity of deliberative STIT theories[END_REF], [START_REF] Lorini | A logic for reasoning about counterfactual emotions[END_REF], and [START_REF] Herzig | Properties of logics of individual and group agency[END_REF], however, both 'atemporal individual STIT' (i.e., individual STIT without tense operators in the object language) axiomatised by Belnap et al. (2001, Chapter 17), and 'atemporal group STIT' (i.e., group STIT without tense operators) can be 'simulated' in standard Kripke semantics. A similar idea is proposed by [START_REF] Kooi | Moral conflicts between groups of agents[END_REF], who introduce the concept of 'consequential model'. Consequential models are equivalent to the Kripke atemporal group STIT models used by [START_REF] Herzig | Properties of logics of individual and group agency[END_REF] and [START_REF] Lorini | A logic for reasoning about counterfactual emotions[END_REF], in which the authors abstract away from the branching-time account of STIT.

The present article goes beyond previous work on atemporal STIT by presenting a variant of STIT logic with time interpreted in standard Kripke semantics and by providing a sound and complete axiomatisation for this logic. I call this variant of STIT logic T-STIT (Temporal STIT). On the syntactic level, the logic T-STIT is nothing but the extension of atemporal individual STIT by: (i) the future tense and past tense operators, and (ii) the operator of group agency in [START_REF] Horty | Agency and deontic logic[END_REF] sense for the grand coalition (the coalition of all agents).

The main motivation of this work is that past research on the mathematical properties of STIT (e.g., completeness and decidability) has mainly focused on atemporal STIT, while extensions of STIT by tense operators are far less well studied and understood. The interest of studying them is that they offer valuable formal languages for representing a variety of normative concepts such as commitment [START_REF] Bentahar | A logical model for commitment and argument network for agent communication[END_REF][START_REF] Desai | Checking correctness of business contracts via commitments[END_REF][START_REF] Singh | Semantical considerations on dialectical and practical commitments[END_REF] and achievement obligation (i.e., the obligation to perform a given action at some point in the future; [START_REF] Broersen | BDIO-CTL: Obligations and the specification of agent behavior[END_REF][START_REF] Governatori | Norm compliance in business process modeling[END_REF] that have an intrinsic temporal nature. These concepts are fundamental for understanding normative relationships between individuals in a society and have become useful abstractions for the design of multi-agent systems since they can be used to model a variety of interactive situations like contracts, agreements, negotiation, dialogue, and argumentation.

The rest of the article is organised as follows. In Section 2, the logic T-STIT is presented and a complete axiomatisation for this logic is given. An application of T-STIT to the formalisation of normative concepts such as achievement obligation and commitment is given in Section 3. It is shown that that T-STIT allows us to capture subtle temporal properties of these normative concepts such as persistence (i.e., the conditions under which a commitment persists over time). In Section 4, related work on STIT logic is discussed.

A STIT logic with time

This section presents the syntax and a Kripke-style semantics for T-STIT (Subsections 2.1 and 2.2). An axiomatisation of T-STIT is provided in Subsection 2.3, while in Subsection 2. [START_REF][END_REF] it is proved that this axiomatisation is sound and complete with respect to the given semantics.

In the logic T-STIT, the so-called Chellas's STIT operators [START_REF] Chellas | Time and modality in the logic of agency[END_REF] are taken as primitive operators of agency. As pointed out by [START_REF] Xu | Axioms for deliberative STIT[END_REF] and [START_REF] Horty | The deliberative STIT: A study of action, omission, and obligation[END_REF], so-called deliberative STIT operators and Chellas's STIT operators are interdefinable and just differ in the choice of primitive operators.

Syntax

Assume a countably infinite set of propositional atoms denoting basic facts Atm = { p, q, . . .} and a finite set of agents Agt = {1, . . . , n}.

The language L T-STIT (Atm, Agt) of the logic T-STIT is the set of formulas defined by the following BNF:

ϕ:: = p | ¬ϕ | ϕ ∧ ϕ | [i]ϕ | [Agt]ϕ | ϕ | Gϕ | Hϕ
where p ranges over Atm and i ranges over Agt. The other Boolean constructions ⊤, ⊥, ∨, → and ↔ are defined from ¬ and ∧ in the standard way.

Operators of the form [i] are Chellas's STIT operators. The formula [i]ϕ captures the fact that ϕ is guaranteed by a present action of agent i, and has to be read 'agent i sees to it that ϕ regardless of what the other agents do'. I shorten the reading of [i]ϕ to 'agent i sees to it that ϕ'. The crucial aspect of STIT theory is that an agent i's action is described in terms of the result that agent i brings about by her acting. For example, i's action of killing another agent j is described by the fact that i sees to it that j is dead. I define the dual of the operator [i] as follows: i ϕ def = ¬[i]¬ϕ. [Agt] is a group STIT operator which captures the fact that ϕ is guaranteed by a present choice of all agents, and has to be read 'all agents see to it that ϕ by acting together'. The dual of the operator [Agt] is defined as expected: Agt ϕ def = ¬ [Agt]¬ϕ. The modal operator [Agt] will be fundamental in Section 2.2 in order to axiomatise a basic property relating action and time studied in STIT: the so-called property of no choice between undivided histories [START_REF] Belnap | Facing the future: Agents and choices in our indeterminist world[END_REF] [START_REF] Horty | The deliberative STIT: A study of action, omission, and obligation[END_REF]:

[i dstit: ϕ] def = [i]ϕ ∧ ¬ ϕ.
Finally, G and H are tense operators that are respectively used to express facts that are always true in the strict future and facts that are always true in the past. Gϕ means 'ϕ will always be true in the future' and Hϕ means 'ϕ has always been true in the past'. I define the dual of the future tense operator G as follows: Fϕ def = ¬G¬ϕ. Fϕ means 'ϕ will be true at some point in the future'. Moreover, I define the dual of the past tense operator H as follows: Pϕ def = ¬H¬ϕ. Pϕ means 'ϕ has been true at some point in the past'.

The following abbreviations will also be convenient:

G * ϕ def = ϕ ∧ Gϕ; F * ϕ def =
¬G * ¬ϕ. G * ϕ stands for 'ϕ is true in the present and will always be true', whereas F * ϕ stands for 'ϕ is true in the present or will be true at some point in the future'.

A Kripke semantics for STIT logic with time

The basic notion in the semantics is the notion of a temporal Kripke STIT model that is nothing but a multi-relational Kripke model with special constraints on the accessibility relations. For notational convenience, in what follows I am going to use the following abbreviations. Given a set of elements W , an arbitrary binary relation R on W and an element w in W , let R(w) = {v ∈ W |(w, v) ∈ R}. Moreover, given two binary relations R 1 and R 2 on W let R 1 • R 2 be the standard operation of composition between binary relations. Temporal Kripke STIT models can be seen as extensions of [START_REF] Zanardo | Branching-time logic with quantification over branches: The point of view of modal logic[END_REF] Ockhamist frames by a choice component, i.e., by accessibility relations for the individual choices of the agents and an accessibility relation for the collective choice of the grand coalition Agt.

Definition 1 (Temporal Kripke STIT model). The class of temporal Kripke STIT models includes all tuples M

= (W, R , {R i |i ∈ Agt}, R Agt , R G , R H , V) where:
• W is a nonempty set of possible worlds; • R , every R i and R Agt are equivalence relations between worlds in W such that:

(C1) R i ⊆ R ; (C2) for all u 1 , . . . , u n ∈ W : if (u i , u j ) ∈ R for all i, j ∈ {1, . . . , n} then 1≤i≤n R i (u i ) = ∅; (C3) for all w ∈ W : R Agt (w) = i∈Agt R i (w); • R G and R H are binary relations between worlds in W such that R G is serial and transitive, R H is the inverse relation of R G (i.e., R H = R -1 G = {(w, v)|(v, w) ∈ R G }), and: (C4) for all w, v, u ∈ W : if v, u ∈ R G (w) then u ∈ R G (v) or v ∈ R G (u) or u = v; (C5) for all w, v, u ∈ W : if v, u ∈ R H (w) then u ∈ R H (v) or v ∈ R H (u) or u = v; (C6) R G • R ⊆ R Agt • R G ; (C7) for all w ∈ W : if v ∈ R (w) then v ∈ R G (w); • V : Atm -→ 2 W is a valuation function for atomic formulas.
The valuation function V is used to identify those states in a model in which a given atomic proposition is true. Specifically, w ∈ V( p) means that p is true at world w.

R (w) is the set of worlds that are alternative to the world w. Following the Ockhamist's view of time [START_REF] Prior | Past, present, and future[END_REF][START_REF] Thomason | Combinations of tense and modality[END_REF][START_REF] Zanardo | Branching-time logic with quantification over branches: The point of view of modal logic[END_REF], I call the equivalence classes induced by the equivalence relation R moments. 1 The set of all moments in the model M is denoted by Mom and the elements in Mom are denoted by m, m ′ , . . .. R G (w) defines the set of worlds that are in the strict future of world w, where the strict future does not include the present. R H (w) defines the set of worlds that are in the past of world w. The Constraint C7 ensures that if two worlds belong to the same moment then one of them cannot be in the future of the other. Since the relation R is reflexive, the Constraint C7 implies the irreflexivity of the relation R G , i.e., for all w ∈ W we have w ∈ R G (w). The fact that the relation R G is transitive and irreflexive just means that it is a strict partial order on the set W . The Constraint C4 ensures that time is connected towards the future, while the Constraint C5 ensures that time is connected towards the past.

Let T (w) = R H (w) ∪ {w} ∪ R G (w) be the set of worlds that are temporally related with world w. The fact that the relation R G is irreflexive and transitive together with the Constraints C4 and C5 ensure that R G is a strict linear (or total) order on the set T (w). For every world w in W , I call the linearly ordered set (T (w), R G ) the history going through w. For notational convenience, I write h w instead of (T (w), R G ). Note that, because of the seriality of the relation R G , every history h w is infinite.

This highlights that there is a one-to-one correspondence between worlds and histories, as for every world w there exists a unique history going through it. In other words, one can interchangeably use the term 'world' and 'history going through a certain world' without lost of generality. As every world in a model is identified with a unique history going through it, the equivalence relation R can also be understood as an equivalence relation between historic alternatives: (w, v) ∈ R means that the history going through v is alternative to the history going through w.

From the temporal relation R G over worlds in W , we can define the following relation < over moments in Mom, where m < m ′ means that moment m ′ is in the strict future of moment m.

Definition 2 (Ordering of moments). For all m, m ′ ∈ Mom: let m < m ′ if and only if there are w ∈ m and v ∈ m ′ such that (w, v) ∈ R G .

For every world w, the set R i (w) identifies agent i's actual choice at w, that is to say, the set of all alternatives that is forced by agent i's actual choice at w. Because of the one-to-one correspondence between worlds and histories, one can also identify agent i's actual choice at w with the set of histories {h v : v ∈ R i (w)}. In other words, in T-STIT an agent chooses among different sets of histories.

Constraint C1 in Definition 1 just means that an agent can only choose among possible alternatives. This constraint ensures that, for every world w, the equivalence relation R i induces a partition of the set R (w). An element of this partition is a choice that is possible (or available) for agent i at w.

Constraint C2 expresses the so-called assumption of independence of agents or independence of choices: if R 1 (u 1 ) is a possible choice for agent 1, R 2 (u 2 ) is a possible choice for agent 2,…, R n (u n ) is a possible choice for agent n, then their intersection is nonempty. More intuitively, this means that agents can never be deprived of choices due to the choices made by other agents.

For every world w, the set R Agt (w) identifies the actual choice of group Agt at wthat is to say, the set of all alternatives that is forced by the collective choice of all agents at w. Constraint C3 just says that the set of alternatives that is forced by the collective choice of all agents at w is equal to the pointwise intersection of the sets of alternatives that are forced by the individual choices of the agents in Agt at w. In other words, the choice of a group corresponds to the intersection of the choices of the individuals in the group. This corresponds to the notion of joint action proposed by [START_REF] Horty | Agency and deontic logic[END_REF], where the joint action of a group is described in terms of the result that the agents in the group bring about by acting together.

The Constraint C6 expresses a basic relation between action and time: if v is in the future of w and u and v are in the same moment, then there exists an alternative z in the collective choice of all agents at w such that u is in the future of z. This constraint corresponds to the property of no choice between undivided histories given in STIT logic (Belnap et al., 2001, Chapter 7). It captures the idea that if two histories come together in some future moment then, in the present, each agent does not have a choice between these two histories. This implies that if an agent can choose between two histories at a later stage then she does not have a choice between them in the present. The Constraint C6 is crucial in order to prove that the relation < defined above is a tree-like ordering of the moments in Mom.

Proposition 3. The relation < satisfies the following four properties for all m, m

′ , m ′′ ∈ Mom: (Irreflexivity) m ≮ m; (Transitivity) if m < m ′ and m ′ < m ′′ then m < m ′′ ; (Asymmetry) if m < m ′ then m ′ ≮ m; (No backward branching) if m ′ < m and m ′′ < m then m ′ < m ′′ or m ′′ < m ′ or m ′ = m ′′ .
Proof. The irreflexivity of < follows from the Constraint C7. Indeed, suppose that m < m. This implies that there are w, v ∈ W such that (w, v) ∈ R and (w, v) ∈ R G . But this is in contradiction with the Constraint C7.

Transitivity of < follows from the transitivity of the relation R G and from the Constraints C1, C3 and C6. Suppose that m < m ′ and m ′ < m ′′ . Therefore, for some arbitrary worlds w 1 , w 2 , w 3 , w 4 we have

w 1 ∈ m, w 2 , w 3 ∈ m ′ , w 4 ∈ m ′′ , w 2 ∈ R G (w 1 ) and w 4 ∈ R G (w 3 )
. By the Constraint C6, it follows that there is w 5 ∈ R Agt (w 1 ) such that w 3 ∈ R G (w 5 ). The Constraints C1 and C3 together imply that R Agt ⊆ R . Hence, there is w 5 ∈ m such that w 3 ∈ R G (w 5 ). Thus, by the transitivity of R G , there is

w 5 ∈ m such that w 4 ∈ R G (w 5 ). It follows that m < m ′′ .
The asymmetry of < follows from its irreflexivity.

No backward branching follows from the Constraints C5 and C6. Suppose that m ′ < m and m ′′ < m. Therefore, for some arbitrary worlds w 1 , w 2 , w 3 , w 4 we have w 1 , w 2 ∈ m, w 3 ∈ m ′ , w 4 ∈ m ′′ , w 3 ∈ R H (w 1 ) andw 4 ∈ R H (w 2 ). By the Constraint C6, it follows that there is w 5 ∈ R Agt (w 3 ) such that w 5 ∈ R H (w 2 ). Thus, since R Agt ⊆ R , there is w 5 ∈ m ′ such that w 5 ∈ R H (w 2 ). Moreover, by the Constraint C5 and the fact that

w 4 ∈ R H (w 2 ), it follows that there is w 5 ∈ m ′ such that w 5 ∈ R H (w 4 ) or w 4 ∈ R H (w 5 ) or w 4 = w 5 . Since w 4 ∈ m ′′ , the latter implies that m ′ < m ′′ or m ′′ < m ′ or m ′ = m ′′ .
Another interesting property of temporal Kripke STIT models that follows from the Constraints C6 and C7 is the so-called property of past isomorphism (PI), which is similar to the property of past isomorphism of [START_REF] Zanardo | Branching-time logic with quantification over branches: The point of view of modal logic[END_REF] Ockhamist frames.

Proposition 4. For all w, v ∈ W , if (w, v) ∈ R then there exists an order-isomorphism f between R H (w) and R H (v) such that, for all u ∈ R H (w), (u, f (u)) ∈ R Agt . 2
Proof. First of all note that, by Constraints C1 and C3, R Agt ⊆ R .

Assume (w, v) ∈ R . By Constraint C7 and the fact that R Agt ⊆ R , every world has at most one R Agt -equivalent in any history and, hence, by Constraint C6, every world u

such that u ∈ R H (w) has exactly one R Agt -equivalent in R H (v). Therefore, the restriction of R Agt to the set R H (w) × R H (v) is an order-preserving bijective function. Given a temporal Kripke STIT model M = (W, R , {R i |i ∈ Agt}, R Agt , R G , R H , V),
a world w and a formula ϕ, I write M, w |= ϕ to mean that ϕ is true at world w in M. The truth conditions of formulas are then defined as follows:

M, w |= p ⇐⇒ w ∈ V( p) M, w |= ¬ϕ ⇐⇒ M, w |= ϕ M, w |= ϕ ∧ ψ ⇐⇒ M, w |= ϕ and M, w |= ψ M, w |= ϕ ⇐⇒ ∀v ∈ R (w) : M, v |= ϕ M, w |= [i]ϕ ⇐⇒ ∀v ∈ R i (w) : M, v |= ϕ M, w |= [Agt]ϕ ⇐⇒ ∀v ∈ R Agt (w) : M, v |= ϕ M, w |= Gϕ ⇐⇒ ∀v ∈ R G (w) : M, v |= ϕ M, w |= Hϕ ⇐⇒ ∀v ∈ R H (w) : M, v |= ϕ Example 5.
(i.e., M, w |= [1]( p ∨ q))
because either p or q hold at every world in agent 1's choice at w. Finally, at w the group {1, 2} sees to it that q will be true at some point in the future (i.e., M, w |= [{1, 2}]Fq) because q holds at some future point of every history in the group {1, 2}'s choice at w. The following proposition provides an example of interesting T-STIT validities. Proof. I only prove the first validity, as the second one can be proved in a similar way. I prove its contrapositive, namely I prove that [Agt]Fϕ → F F * ϕ is T-STIT valid. Suppose M, w |= [Agt]Fϕ. This means that:

Proposition 6. The following two formulas are T-STIT valid:

G♦G * ϕ → Agt Gϕ G♦(G * ϕ ∧ F * ψ) → Agt (Gϕ ∧ Fψ)
(A) for all v ∈ R Agt (w) there is u ∈ R G (v) such that M, u |= ϕ. Let A ϕ w = u|M, u |= ϕ and ∃v ∈ R Agt (w) such that u ∈ R G (v)
and let

PA ϕ w = ū ∈ R G (w)|∃u ∈ A ϕ w such that ( ū, u) ∈ R .
Moreover let

NB ϕ w = R G (w) \ ū∈PA ϕ w R G ( ū).
I am going to show that NB The latter implies that there exists ū ∈ R G (w) such that w = ū, which is in contradiction with the fact that R G is irreflexive.

Take any world z ∈ NB

ϕ w . Clearly, z ∈ R G (w). I am going to show that (B) for all v ∈ R (z) either M, v |= ϕ or there is u ∈ R G (v) such that M, u |= ϕ. Suppose v ∈ R (z). From z ∈ R G (w)
, by Constraint C6 and the previous observation (A), we have that there are z

′ , v ′ such that z ′ ∈ R Agt (w), v ∈ R G (z ′ ), v ′ ∈ R G (z ′ ) and M, v ′ |= ϕ. Moreover, by Constraint C4, v ′ ∈ R G (v) or v ∈ R G (v ′ ) or v = v ′ . I am going to show that v = v ′ or v ′ ∈ R G (v) by reductio ad absurdum. Suppose v ∈ R G (v ′ ). Clearly, v ′ ∈ A ϕ w . From z ′ ∈ R Agt (w), v ∈ R (z), z ∈ R G (w), v ∈ R G (z ′ ), v ′ ∈ R G (z ′ ) and v ∈ R G (v ′ ), by Proposition 4, it follows that there exists v′ ∈ R G (w) such that v ′ ∈ R Agt ( v′ ) and z ∈ R G ( v′ ). Since R Agt ⊆ R and v ′ ∈ A ϕ w , the latter implies that there exists v′ ∈ R G (w) such that v′ ∈ PA ϕ w , v ′ ∈ R Agt ( v′ ) and z ∈ R G ( v′ ). v′ ∈ PA ϕ w and z ∈ R G ( v′ ) together imply that z ∈ NB ϕ w . But this is in contradiction with the initial hypothesis that z ∈ NB ϕ w . By the previous item (B), we have that M, z |= F * ϕ. Since z ∈ R G (w), M, w |= F F * ϕ.

Axiomatisation

Figure 2 contains a complete axiomatisation with respect to the class of temporal Kripke STIT models. This includes all tautologies of classical propositional calculus (PC) as well as modus ponens (MP). Moreover, we have all the principles of the normal modal logic S5 for every operator [i], for the operator [Agt] and for the operator , all principles of the normal modal logic KD4 for the future tense operator G and all principles of the normal modal logic K for the past tense operator H. That is, we have Axiom K for each operator:

( ϕ ∧ (ϕ → ψ)) → ψ with ∈ { , G, H, [Agt]} ∪ {[i]|i ∈ Agt}.
We have Axiom D for the future tense modality G: ¬(Gϕ ∧G¬ϕ). We have Axiom 4 for , G, [Agt] and for every [i]:

ϕ → ϕ with ∈ { , [Agt], G} ∪ {[i]|i ∈ Agt}.
Furthermore, we have Axiom T for , [Agt] and for every

[i]: ϕ → ϕ with ∈ { , [Agt]} ∪ {[i]|i ∈ Agt}.
We have Axiom B for , [Agt] and for every

[i]: ϕ → ¬ ¬ϕ with ∈ { , [Agt]} ∪ {[i]|i ∈ Agt}.
Finally we have the rule of necessitation for each modal operator:

ϕ ϕ with ∈ { , [Agt], G, H} ∪ {[i]|i ∈ Agt}. In what follows, I write ⊢ T-STIT ϕ if ϕ is a T-STIT theorem. Moreover, I say that ϕ is T-STIT consistent if ⊢ T-STIT ¬ϕ.
( → i) and (AIA) are the two central principles in Xu's (1998) axiomatisation of the Chellas's STIT operators [i]. According to Axiom ( → i), if ϕ is true regardless of what every agent does, then every agent sees to it that ϕ. In other words, an agent brings about those facts that are inevitable. 3 According to Axiom (i → Agt), all agents bring about together what each of them brings about individually.

We have principles for the tense operators and for the relationship between time and action. (Connected G ) and (Connected H ) are the basic axioms for the linearity of the future and the linearity of the past [START_REF] Goldblatt | Logics of time and computation[END_REF]. (Conv G,H ) and (Conv H,G ) are the basic interaction axioms between future and past of minimal tense logic according to which 'what is, will always have been' and 'what is, has always been going to be'.

Axiom (NCUH) establishes a fundamental relationship between action and time and corresponds to the semantic constraint of 'no choice between undivided histories' over temporal Kripke STIT models (Constraint C6): if in some future world ϕ will be possible then the actual collective choice of all agents will possibly result in a state in which ϕ is true.

(IRR) is a variant of the well-known Gabbay's irreflexivity rule that has been widely used in the past for proving completeness results for different kinds of temporal logic in which time is supposed to be irreflexive (see, e.g., [START_REF] Gabbay | Temporal logic: Mathematical foundations and computational aspects[END_REF][START_REF] Reynolds | An axiomatization of Prior's Ockhamist logic of historical necessity[END_REF][START_REF] Von Kutschera | T x W completeness[END_REF][START_REF] Zanardo | Branching-time logic with quantification over branches: The point of view of modal logic[END_REF]. The idea is that the special kind of irreflexivity for the relation R G expressed by the Constraint C7 in Definition 1, although not definable in terms of an axiom, can be characterised in an alternative sense by means of the rule (IRR). This rule is perhaps more comprehensible if we consider its contrapositive: if p does not occur in ϕ and

ϕ is T-STIT consistent, then ¬ p ∧ (G p ∧ H p) ∧ ϕ is T-STIT consistent.
Theorem 7. The set of T-STIT validities is completely axiomatised by the principles given in Figure 2.

Proof of Theorem 7

It is a routine task to show that the axioms given in Figure 2 are valid with respect to the class of temporal Kripke T-STIT models and that the rules of inference preserve validity. Thus, if ϕ is a T-STIT theorem then ϕ is T-STIT valid.

I am going to prove that if ϕ is T-STIT consistent then ϕ is T-STIT satisfiable. The proof is divided into two steps.

First of all, I introduce the class of superadditive temporal Kripke STIT models. While in the temporal Kripke STIT models the collective choice of the grand coalition is equal to the pointwise intersection of the individual choices, in superadditive temporal Kripke STIT models the collective choice of the grand coalition is merely included in the pointwise intersection of the individual choices. I prove that the logic T-STIT does not distinguish the semantics in terms of temporal Kripke STIT models from the more 'liberal' semantics in terms of superadditive temporal Kripke STIT models. That is to say, the set of validities with respect to the class of temporal Kripke STIT models is equal to the set of validities with respect to the class of superadditive temporal Kripke STIT models (Lemma 9).

Secondly, I prove that the set of validities in the class of superadditive temporal Kripke STIT models is completely axiomatised by the principles given in Figure 2 (Lemma 10).

Theorem 7 directly follows from Lemma 10 and Lemma 9.

Let me define the class of superadditive temporal Kripke STIT models.

= (W, R , {R i |i ∈ Agt}, R Agt , R G , R H , V)
where:

• W is a nonempty set of possible worlds;

• R , every R i and R Agt are equivalence relations between worlds in W such that:

(C1) R i ⊆ R ; (C2) for all u 1 , . . . , u n ∈ W : if (u i , u j ) ∈ R for all i, j ∈ {1, . . . , n} then 1≤i≤n R i (u i ) = ∅; (C3 * ) for all w ∈ W : R Agt (w) ⊆ i∈Agt R i (w); • R G and R H are binary relations between worlds in W such that R G is serial and transitive, R H is the inverse relation of R G , and: (C4) for all w, v, u ∈ W : if v, u ∈ R G (w) then u ∈ R G (v) or v ∈ R G (u) or u = v; (C5) for all w, v, u ∈ W : if v, u ∈ R H (w) then u ∈ R H (v) or v ∈ R H (u) or u = v; (C6) R G • R ⊆ R Agt • R G ; (C7) for all w ∈ W : if v ∈ R (w) then v ∈ R G (w); • V : Atm -→ 2 W is a valuation function for atomic formulas.
The only difference between the class of temporal Kripke STIT models and superadditive temporal Kripke STIT models is in the Constraint C3 * . Lemma 9. Let ϕ be a formula in L T-STIT (Atm, Agt). Then, ϕ is satisfiable in the class of temporal Kripke STIT models if and only if it is satisfiable in the class of superadditive temporal Kripke STIT models.

Proof. (⇒)

The left-to-right direction of the equivalence is obvious as the class of temporal Kripke STIT models is included in the class of superadditive temporal Kripke STIT models.

(⇐) As to the right-to-left direction, I am going to show how to transform a superadditive temporal Kripke STIT model into a temporal Kripke STIT model without affecting the satisfiability of a formula. The technique used here is inspired by [START_REF] Vakarelov | A modal theory of arrows: Arrow logics I[END_REF].

Consider a superadditive temporal Kripke STIT model

M = (W, R , {R i |i ∈ Agt}, R Agt , R G , R H , V) and a world w in M such that M, w |= ϕ. I am going to define a temporal Kripke STIT model M ′ = (W ′ , R ′ , {R ′ i |i ∈ Agt}, R ′ Agt , R ′ G , R ′ H , V ′ ) that satisfies ϕ. For every i ∈ Agt, let i = {R i (w)|w ∈ W }
be the partition of W induced by the equivalence class R i . Elements of i are called i's choices. Moreover, let

= {δ ∈ i∈Agt i | i∈Agt δ i = ∅}
be the set of collective choices. Elements of are denoted by δ, δ ′ , . . .. For every δ ∈ , δ i denotes the element in the vector δ corresponding to the agent i. Furthermore, for notational convenience I write δ w to denote the collective choice in that includes the world w. That is, δ w is the collective choice in such that w ∈ i∈Agt δ w i . For every δ ∈ , let

Ŵ δ = {R Agt (w)|w ∈ i∈Agt δ i } be the set of R Agt -equivalence classes that are included in i∈Agt δ i .
For every δ ∈ , let

k δ : [1, . . . , car d(Ŵ δ )] -→ Ŵ δ
be a bijection associating every integer between 1 and car d(Ŵ δ ) to a unique element of Ŵ δ .

In the sequel I write

Ŵ n δ to indicate the element k δ (n) for every 1 ≤ n ≤ car d(Ŵ δ ). For every w ∈ W let TC w = {δ ∈ |∃v ∈ i∈Agt δ i such that v ∈ T (w)}
be the set of collective choices that are temporally related with w, with

T (w) = R H (w) ∪ {w} ∪ R G (w).
Moreover, let

PC w = {δ ∈ |∃v ∈ i∈Agt δ i such that v ∈ R H (w)}
be the set of collective choices that are in the past of w.

Finally, let

FC w = {δ ∈ |∃v ∈ i∈Agt δ i such that v ∈ R G (w)}
be the set of collective choices that are in the future of w. Note that:

(A1) if v ∈ T (w) then TC w = TC v ; (A2) if v ∈ R (w) then PC w = PC v (because of Proposition 4. in Section 2.2); (A3) if v ∈ R Agt (w) then δ w = δ v and PC w = PC v (because of (A2)).
Moreover, let w be the set of all total functions f : TC w -→ Z n that satisfy the following constraint:

• for all δ ∈ TC w and for all -→ x ∈ Z n , if f (δ) = -→ x then there exists v ∈ T (w) such that v ∈ Ŵ

x i ∈{x 1 ,...,xn } x i δ , where Z is the set of integers and -→ x = x 1 , . . . , x n . I write f i (δ) to denote the i-element in the vector f (δ), with 1 ≤ i ≤ n.

Because of the Constraint C7, we have that for all w ∈ W and for all -→ x ∈ Z n :

(B) if v ∈ T (w) and v ∈ Ŵ x i ∈{x 1 ,...,xn } x i δ w then w = v.
Furthermore, because of Proposition 4 in Section 2.2, we have that for all w, v ∈ W and for all -→ x ∈ Z n :

(C) if v ∈ R (w) then there exists u 1 ∈ R H (w) such that u 1 ∈ Ŵ x i ∈{x 1 ,...,xn } x i δ if and only if there exists u 2 ∈ R H (v) such that u 2 ∈ Ŵ x i ∈{x 1 ,...,xn } x i δ .
From the previous item (C) it follows that for all w, v ∈ W :

(D) if f ∈ w and v ∈ R (w) then there exists f ′ ∈ v such that, for all δ ∈ PC w , f ′ (δ) = f (δ).
Moreover, from the previous item (A1), for all w, v ∈ W we have that:

(E) if f ∈ w and v ∈ T (w) then there exists f ′ ∈ v such that, for all δ ∈ TC w , f ′ (δ) = f (δ).

I am now able to define the model

M ′ = (W ′ , R ′ , {R ′ i |i ∈ Agt}, R ′ Agt , R ′ G , R ′ H , V ′ ): • W ′ = {w f |w ∈ W and f ∈ w }; • for all w f , v f ′ ∈ W ′ , (w f , v f ′ ) ∈ R ′ iff (w, v) ∈ R and f (δ) = f ′ (δ) for all δ ∈ PC w ; • for all i ∈ Agt and for all w f , v f ′ ∈ W ′ , (w f , v f ′ ) ∈ R ′ i iff δ w i = δ v i , f i (δ w ) = f ′ i (δ v ) and f (δ) = f ′ (δ) for all δ ∈ PC w ; • for all w f , v f ′ ∈ W ′ , (w f , v f ′ ) ∈ R ′ Agt iff δ w = δ v , f (δ w ) = f ′ (δ v ) and f (δ) = f ′ (δ) for all δ ∈ PC w ; • for all w f , v f ′ ∈ W ′ , (w f , v f ′ ) ∈ R ′ G iff (w, v) ∈ R G and f (δ) = f ′ (δ) for all δ ∈ TC w ; • for all w f , v f ′ ∈ W ′ , (w f , v f ′ ) ∈ R ′ H iff (v f ′ , w f ) ∈ R ′ G ; • for all p ∈ Atm, V ′ ( p) = {w f ∈ W ′ |w ∈ V( p)}.
It is a routine task to check that the mapping f : w f → w defines a bounded morphism from M ′ to M (Blackburn, De Rijke, & Venema, 2001, Definition 2.12). Indeed, it follows from the definitions of R

′ , R ′ i , R ′ Agt , R ′ G and R ′ H that for all w f , v f ′ ∈ W ′ : • (w f , v f ′ ) ∈ R ′ i implies (w, v) ∈ R i ; • (w f , v f ′ ) ∈ R ′ Agt implies (w, v) ∈ R Agt ; • (w f , v f ′ ) ∈ R ′ implies (w, v) ∈ R ; • (w f , v f ′ ) ∈ R ′ G implies (w, v) ∈ R G ; • (w f , v f ′ ) ∈ R ′ H implies (w, v) ∈ R H . For instance, suppose that (w f , v f ′ ) ∈ R ′ i . By definition of R ′ i the latter implies that δ w i = δ v i and w ∈ δ w i and v ∈ δ v i . The latter implies that (w, v) ∈ R i . Now, suppose that (w f , v f ′ ) ∈ R ′ Agt . This implies that δ w = δ v and f (δ w ) = f ′ (δ v ). By the previous observation (B), it follows that w, v ∈ Ŵ f 1 (δ w )+...+ f n (δ w ) δ w . Thus, (w, v) ∈ R Agt .
The other way around we have that for all w f ∈ W ′ :

• if ( f (w f ), v) ∈ R then there is v f ′ such that (w f , v f ′ ) ∈ R ′ ; • if ( f (w f ), v) ∈ R i then there is v f ′ such that (w f , v f ′ ) ∈ R ′ i ; • if ( f (w f ), v) ∈ R Agt then there is v f ′ such that (w f , v f ′ ) ∈ R ′ Agt ; • if ( f (w f ), v) ∈ R G then there is v f ′ such that (w f , v f ′ ) ∈ R ′ G ; • if ( f (w f ), v) ∈ R H then there is v f ′ such that (w f , v f ′ ) ∈ R ′ H .
Let me prove the previous items. The first item is trivial and I do not prove it here. and hence ¬(ϕ∧name ( p)

) ∈ Ŵ (because (ψ 1 ∧. . .∧ψ k ) ∈ Ŵ). But this is in contradiction with ♦(ϕ ∧ name( p)) ∈ Ŵ.
Now, I turn to define an increasing sequence of consistent extensions ( n ) n≥0 such that n ⊆ n+1 for all n.

Assume n ⊆ n+1 has been defined and is consistent. Then, either n ∪ {χ n } is consistent or n ∪ {¬χ n } is consistent.

Case 1: n ∪ {¬χ n } consistent. Take n+1 = n ∪ {¬χ n }. Case 2a: n ∪ {¬χ n } not consistent, n ∪ {χ n } consistent and χ n ∈ . Take n+1 = n ∪ {χ n }.
Case 2b: n ∪ {¬χ n } not consistent, n ∪ {χ n } consistent and χ n ∈ . We have that:

♦((ϕ ∧ name( p)) ∧ ψ∈ n \ 0 ψ ∧ χ n ) ∈ Ŵ.
For, otherwise,

(((ϕ ∧ name( p)) ∧ ψ∈ n \ 0 ψ) → ¬χ n ) ∈ Ŵ and hence, by definition of 0 , ((ϕ ∧ name( p)) ∧ ψ∈ n \ 0 ψ) → ¬χ n ∈ n .
Hence, since

((ϕ ∧ name( p)) ∧ ψ∈ n \ 0 ψ) ∈ n , ¬χ n ∈ n .
This is in contradiction with the fact that n ∪ {χ n } is consistent. Thus, since Ŵ is an IRR theory, for some atom q, we have

♦((ϕ ∧ name( p)) ∧ ψ∈ n \ 0 ψ ∧ χ n (q)) ∈ Ŵ.
It follows that n ∪ {χ n } ∪ {χ n (q)} is consistent. For, otherwise, for some ψ 1 , . . . , ψ k ∈ {ψ| ψ ∈ Ŵ}, we have:

⊢ (ψ 1 ∧ . . . ∧ ψ k ) → ¬((ϕ ∧ name( p)) ∧ ψ∈ n \ 0 ψ ∧ χ n (q)), hence ⊢ (ψ 1 ∧ . . . ∧ ψ k ) → ¬((ϕ ∧ name( p)) ∧ ψ∈ n \ 0 ψ ∧ χ n (q)), and hence ¬((ϕ∧name( p))∧ ψ∈ n \ 0 ψ ∧χ n (q)) ∈ Ŵ (because (ψ 1 ∧. . .∧ψ k ) ∈ Ŵ).
But this is in contradiction with ♦((ϕ

∧ name( p)) ∧ ψ∈ n \ 0 ψ ∧ χ n (q)) ∈ Ŵ. Let n+1 = n ∪ {χ n } ∪ {χ n (q)}.
Thus, the sequence ( n ) n≥0 is defined and, clearly, = n≥0 n is the desired IRR theory such that (Ŵ, ) ∈ R c and ϕ ∈ . Proposition 17. Let Ŵ 1 , . . . , Ŵ n be IRR theories such that for all 1 ≤ i, j ≤ n, (Ŵ i , Ŵ j ) ∈ R c . Then, there exists an IRR theory such that (Ŵ 1 , ) ∈ R c 1 , . . . , (Ŵ n , ) ∈ R c n . Proof. In order to simplify the exposition, let us assume that n = 2. The general case for any arbitrary n can be proved analogously.

Suppose Ŵ 1 and Ŵ 2 are IRR theories such that for all 1 ≤ i, j ≤ 2, (Ŵ i , Ŵ j ) ∈ R c . I am going to show that there exists an IRR theory such that (Ŵ 1 , ) ∈ R c 1 and (Ŵ 2 , ) ∈ R c 2 . Since Ŵ 1 and Ŵ 2 are IRR theories, there exists name( p 1 ) ∈ Ŵ 1 and name( p 2 ) ∈ Ŵ 2 for some atoms p 1 , p 2 .

Let

0 = {name( p 1 )} ∪ {name( p 2 )} ∪ {ψ|[1]ψ ∈ Ŵ 1 } ∪ {ψ|[2]ψ ∈ Ŵ 2 }.
I am going to show that 0 is consistent by reductio ad absurdum.

Suppose 0 is not consistent. Then, for some ψ 1 , . . . , ψ k ∈ 0 , we have:

⊢ (ψ 1 ∧ . . . ∧ ψ k ) → ⊥. Let Y denote the set {ψ 1 , . . . , ψ k }. Moreover, let Y 1 = {ψ ∈ Y |[1]ψ ∈ Ŵ 1 or ψ = name( p 1 )} and Y 2 = {ψ ∈ Y |[2]ψ ∈ Ŵ 2 or ψ = name( p 2 )}. Clearly, Y = Y 1 ∪ Y 2 and: (A) [1] ψ∈Y 1 ψ ∈ Ŵ 1 .
The previous item (A) follows from these two facts: (i) for every ψ ∈ Y 1 such that

ψ = name( p 1 ), [1]ψ ∈ Ŵ 1 (because ψ is of the form [1]χ and [1]χ → [1][1]χ is a T-STIT theorem); and (ii) [1]name( p 1 ) ∈ Ŵ 1 (because name( p 1 ) → [1]name( p 1 ) is a T-STIT theorem). Likewise, we have: (B) [2] ψ∈Y 2 ψ ∈ Ŵ 2 .
From the definition of the accessibility relation R c and the fact that

(Ŵ 1 , Ŵ 2 ) ∈ R c , it follows that ♦[2] ψ∈Y 2 ψ ∈ Ŵ 1 . Moreover, by the T-STIT theorem ⊢ [1]ψ → ♦[1]ψ, we have ♦[1] ψ∈Y 1 ψ ∈ Ŵ 1 . By the Axiom (AIA), it follows that ♦([1] ψ∈Y 1 ψ ∧ [2] ψ∈Y 2 ψ) ∈ Ŵ 1 .
Hence, by Lemma 16, there is an IRR theory such that (Ŵ 1 , ) ∈ R c and ([1] ψ∈Y 1 ψ ∧[2] ψ∈Y 2 ψ) ∈ . Hence, by Axiom T for [i], there is an IRR theory such that (Ŵ 1 , ) ∈ R c and ( ψ∈Y 1 ψ ∧ ψ∈Y 2 ψ) ∈ . The latter implies that ψ∈Y ψ is consistent. Hence,

⊢ (ψ 1 ∧ . . . ∧ ψ k ) → ⊥.
The rest of the proof proceeds in the same way as the proof of Lemma 16. Specifically, I turn to define an increasing sequence of consistent extensions ( n ) n≥0 such that n ⊆ n+1 for all n.

Assume n ⊆ n+1 has been defined and is consistent. Then,

either n ∪ {χ n } is consistent or n ∪ {¬χ n } is consistent. Case 1: n ∪ {¬χ n } consistent. Take n+1 = n ∪ {¬χ n }. Case 2a: n ∪ {¬χ n } not consistent, n ∪ {χ n } consistent and χ n ∈ . Take n+1 = n ∪ {χ n }.
Case 2b: n ∪ {¬χ n } not consistent, n ∪ {χ n } consistent and χ n ∈ . We have that:

1 (name( p 1 ) ∧ ψ∈ n \ 0 ψ ∧ χ n ) ∈ Ŵ 1 .
For, otherwise,

[1]((name( p 1 ) ∧ ψ∈ n \ 0 ψ) → ¬χ n ) ∈ Ŵ 1 and hence, by definition of 0 , (name( p 1 ) ∧ ψ∈ n \ 0 ψ) → ¬χ n ∈ n . Hence, since (name( p 1 ) ∧ ψ∈ n \ 0 ψ) ∈ n , ¬χ n ∈ n . This is in contradiction with the fact that n ∪ {χ n } is consistent.
Therefore, for some atom q,

1 (name( p 1 ) ∧ ψ∈ n \ 0 ψ ∧ χ n (q)) ∈ Ŵ 1 .
It follows that n ∪ {χ n } ∪ {χ n (q)} is consistent. For, otherwise, for some ψ 1 , . . . , ψ k ∈ {ψ|[1]ψ ∈ Ŵ 1 }, we have:

⊢ (ψ 1 ∧ . . . ∧ ψ k ) → ¬(name( p 1 ) ∧ ψ∈ n \ 0 ψ ∧ χ n (q)), hence ⊢ [1](ψ 1 ∧ . . . ∧ ψ k ) → [1]¬(name( p) ∧ ψ∈ n \ 0 ψ ∧ χ n (q)),
and hence

[1]¬(name( p 1 )∧ ψ∈ n \ 0 ψ ∧χ n (q)) ∈ Ŵ 1 (because [1](ψ 1 ∧. . .∧ψ k ) ∈ Ŵ 1 ). But this is in contradiction with 1 (name( p 1 ) ∧ ψ∈ n \ 0 ψ ∧ χ n (q)) ∈ Ŵ 1 . Let n+1 = n ∪ {χ n } ∪ {χ n (q)}.
Thus, the sequence ( n ) n≥0 is defined and, clearly,

= n≥0 n is the desired IRR theory such that (Ŵ 1 , ) ∈ R c 1 and (Ŵ 2 , ) ∈ R c 2 . Proposition 18. Let , Ŵ and Ŵ ′ be IRR theories such that ( , Ŵ) ∈ R c G and (Ŵ, Ŵ ′ ) ∈ R c .
Then, there exists an IRR theory ′ such that ( , ′ ) ∈ R c Agt and

( ′ , Ŵ ′ ) ∈ R c G . Proof. Suppose , Ŵ and Ŵ ′ are IRR theories such that ( , Ŵ) ∈ R c G and (Ŵ, Ŵ ′ ) ∈ R c . It follows that name( p) ∈ for some atom p. Hence, by definition of R c H , Pname( p) ∈ Ŵ. By definition of R c , it follows that ♦Pname( p) ∈ Ŵ ′ .
We have the following T-STIT theorem:

⊢ ♦Pϕ → P Agt ϕ. (1)
The following is the Hilbert-style proof:

are undertaken and established are often institutional contexts. For instance, after signing a contract in the presence of a public notary, a person becomes committed in front of the State to carry out her part of the contract. In this article, I only consider pragmatic commitments and I leave aside propositional commitments (also called dialectical commitments). Pragmatic commitments are about what is to be done whereas propositional commitments are about what is true. Pragmatic commitments concern promises from a debtor to a creditor to perform a given action, while propositional commitments are about positions taken during a dialogue. For example, if i tells to j: 'I will lend you my car for the weekend!' then, he makes a pragmatic commitment to j. On the contrary, if i tells to j: 'Tomorrow, will be sunny. I am sure!' then, he makes a propositional commitment to j.

In order to be able to define social commitment, let us suppose that the set of propositional atoms Atm contains special atoms of the form v i, j , one for every i, j ∈ Agt such that i = j. These are similar to the special atoms for violation that are used in the Anderson's reduction of deontic logic to alethic logic [START_REF] Anderson | A reduction of deontic logic to alethic modal logic[END_REF][START_REF] Lindahl | Stig Kanger's theory of rights[END_REF]. In the semantics, the special atom v i, j is used to identify those worlds in which agent i does not fulfil her commitments to agent j. The atom v i, j has to be read 'in the actual world, agent i does not fulfil her commitment to agent j'. Special atoms v i, j can be combined with the tense operator G * in order to identify those histories in which agent i will never fulfil her commitment to agent j. In particular, formula G * v i, j has to be read 'in the actual history, agent i will never fulfil her commitment to agent j'or also 'in the actual history, agent j is wronged by agent i'.

I say that agent i is committed to agent j to ensure ϕ (denoted by C i: j ϕ) if and only if: (i) all historic alternatives in which i will never see to it that ϕ, are histories in which agent i will never fulfil her commitment to agent j; and (ii) i does not see to it that ϕ. In other words, i will not fulfil her commitment to j unless i will see to it that ϕ at some point in the future. For every i, j ∈ Agt, I define:

C i: j ϕ def = (¬F * [i]ϕ → G * v i, j ) ∧ ¬[i]ϕ.
Let me make three observations about the preceding definition of commitment. First of all, it is worth noting that it is related to the notion of achievement obligation [START_REF] Broersen | BDIO-CTL: Obligations and the specification of agent behavior[END_REF][START_REF] Governatori | Norm compliance in business process modeling[END_REF]. The idea is that an agent has an achievement obligation to bring about ϕ if and only if she has the obligation to bring about ϕ at some point in the future. 4 Thus, commitment can be seen as a specific kind of achievement obligation. Specifically, it can be conceived as a directed achievement obligation from a bearer to a counterparty (for some analysis of the notion of directed obligation in deontic logic, see, e.g., [START_REF] Dignum | Autonomous agents with norms[END_REF][START_REF] Herrestad | Obligations directed from bearers to counterparties[END_REF][START_REF] Kanger | Rights and parliamentarism[END_REF][START_REF] Lindahl | Stig Kanger's theory of rights[END_REF][START_REF] Makinson | On the formal representation of rights relations: Remarks on the work of Stig Kanger and Lars Lindahl[END_REF]. 5 That is to say, agent i is committed to agent j to bring about ϕ if and only if i has the obligation towards j to bring about ϕ at some point in the future. Secondly, the component ¬[i]ϕ expresses that i is committed to j to ensure ϕ only if i has not yet fulfilled her commitment to j by bringing about ϕ. In this sense, the formula [i]ϕ can be conceived as the discharge condition for commitment. Suppose agent i is committed to agent j to ensure ϕ. Then, if i sees to it that ϕ, then her commitment to j is discharged and is no longer active. Finally, according to the preceding definition, the fact that i brought about ϕ in the past (before being committed to j) is irrelevant. Indeed, the general intuition is that being committed now to do some action means being obliged to do the action either in the present or at some point in the strict future. Therefore, while the fact of performing the action in the present is a sufficient condition for discharging an actual commitment, the fact of having performed the action in the past is not.

The following example illustrates the preceding definition of commitment in a concrete scenario.

Example 20. Agent 2 is the programme chair of a given conference. Agent 2 asks agent 1, a member of the programme committee, to review some articles submitted for the conference. Agent 1 accepts agent 2's request by sending a confirmation e-mail (we suppose that the communication between 1 and 2 is made through the Easychair system). Consequently, according to the programme committee of the conference, agent 1 is committed to 2 to review the articles: C 1:2 review. This means that (i) all historic alternatives in which 1 will never review the articles are histories in which 2 is wronged by 1; and (ii) 1 has not yet fulfilled her commitment to 2 by reviewing the articles:

(¬F * [1]review → G * v 1,2 ) ∧ ¬[1]review.
Now, let us consider some logical properties of the commitment operator C i: j .According to the following T-STIT theorem 3, if i is committed to j to ensure ϕ ∧ψ then i is committed to j to ensure ϕ and to ensure ψ. For every i, j ∈ Agt we have:

⊢ T-STIT C i: j (ϕ ∧ ψ) → (C i: j ϕ ∧ C i: j ψ). (3)
Note that the converse of T-STIT theorem 3 is not valid. Indeed, the fact that i is committed to j to ensure ϕ and to ensure ψ (i.e., C i: j ϕ ∧ C i: j ψ) does not necessarily imply that i is committed to j to ensure that ϕ and ψ are true at the same point in the future (i.e., C i: j (ϕ ∧ ψ)). For example, i may be committed to j to lend her a car and to lend her a motorbike at different points in the future without being committed to lending her a car and a motorbike at the same point in the future.

The following theorem 4 highlights that an agent cannot be committed to bring about tautologies:

⊢ T-STIT ¬C i: j ⊤. (4)
Indeed, since [i]⊤ is a T-STIT theorem, agent i's commitment to bring about ⊤ is always discharged.

The following T-STIT theorem 5 is a weakening principle for commitment. A similar property of commitment has been isolated by [START_REF] Singh | Semantical considerations on dialectical and practical commitments[END_REF]. For every i, j ∈ Agt we have:

⊢ T-STIT (C i: j (ϕ ∧ ψ) ∧ [i]ϕ) → C i: j ψ.
(5) This means that if agent i is committed to agent j to ensure ϕ ∧ ψ and agent i sees to it that ϕ, then i is committed to j to ensure ψ. So, if an agent is committed to ensuring two states of affairs ϕ and ψ and her commitment to ensure ϕ is discharged, then the agent is committed to ensuring ψ.

The following T-STIT theorem 6 clarifies how the previous definition of commitment behaves in the case of Moore-like sentences of the form ϕ ∧ ¬[i]ϕ: an agent is committed to ensure that ϕ is true and that she does not see to it that ϕ if and only if the agent is committed to do something inconsistent:

⊢ T-STIT C i: j (ϕ ∧ ¬[i]ϕ) ↔ C i: j ⊥. (6)
The following T-STIT theorem 7 characterises the relationship between commitments about logical equivalent formulas:

⊢ T-STIT G * (ϕ ↔ ψ) → (C i: j ϕ ↔ C i: j ψ). (7)
This means that if ϕ and ψ are equivalent in all future worlds of every history passing through the current moment, then agent i is committed to ensuring ϕ if and only if agent i is committed to ensuring ψ. Note that the formula G * ϕ captures a form of future necessity or, even better, future inevitability. Therefore, theorem 7 captures the idea that if in the future it is inevitable that ϕ and ψ have the same truth value, then one cannot be committed to ensuring ϕ without being committed to ensuring ψ, and one cannot be committed to ensuring ψ without being committed to ensuring ϕ.

The last T-STIT theorem considered here is the following one about the relationship between time and commitment:

⊢ T-STIT C i: j ϕ → F(¬[i]ϕ → C i: j ϕ). (8)
Since the Hilbert-style derivation of this T-STIT theorem is not trivial, I give it here:

1. ⊢ C i: j ϕ def = (¬F * [i]ϕ → G * v i, j ) ∧ ¬[i]ϕ. 2. ⊢ ( (¬F * [i]ϕ → G * v i, j ) ∧ ¬[i]ϕ) → ([Agt](¬F * [i]ϕ → G * v i, j ) ∧ [Agt]¬[i]ϕ). By Axiom ( → i), Axiom (i → Agt) and T-STIT theorem ¬[i]ϕ → [i]¬[i]ϕ. 3. ⊢ ([Agt](¬F * [i]ϕ → G * v i, j ) ∧ [Agt]¬[i]ϕ) → [Agt]((¬F * [i]ϕ → G * v i, j ) ∧ ¬[i]ϕ). By Axiom K for [Agt]. 4. ⊢ [Agt]((¬F * [i]ϕ → G * v i, j ) ∧ ¬[i]ϕ) ↔ [Agt](([i]ϕ ∨ F[i]ϕ ∨ G * v i, j ) ∧ ¬[i]ϕ). 5. ⊢ [Agt](([i]ϕ ∨ F[i]ϕ ∨ G * v i, j ) ∧ ¬[i]ϕ) → [Agt](F[i]ϕ ∨ G * v i, j ). By Axiom K for [Agt]. 6. ⊢ [Agt](F[i]ϕ ∨ G * v i, j ) → [Agt](F[i]ϕ ∨ Gv i, j ).
By Axiom K for [Agt].

7. ⊢ [Agt](F[i]ϕ ∨ Gv i, j ) → F (F * [i]ϕ ∨ G * v i, j ).
By the second T-STIT validity in Proposition 6.

⊢ F (F

* [i]ϕ ∨ G * v i, j ) → F (¬F * [i]ϕ → G * v i, j ). 9. ⊢ F (¬F * [i]ϕ → G * v i, j ) → F(([i]ϕ ∨ ¬[i]ϕ) ∧ (¬F * [i]ϕ → G * v i, j )).
By T-STIT theorem Fϕ → F(⊤ ∧ ϕ).

⊢ F((

[i]ϕ ∨ ¬[i]ϕ) ∧ (¬F * [i]ϕ → G * v i, j )) → F([i]ϕ ∨ C i: j ϕ). 11. ⊢ C i: j ϕ → F(¬[i]ϕ → C i: j ϕ).
From 1-10.

According to the previous T-STIT theorem 8, if agent i is committed to agent j to ensure ϕ then, at some point in the future, either i will see to it that ϕ or i will remain committed to j to ensure ϕ. This captures a kind of persistence of commitment over time. 6 That is, a commitment will persist as long as the committed agent does not perform the action to which she is committed. Note that this property of commitment relies on the assumption that there are no 'external' actions or processes that may cancel a pre-existent commitment independently from the fact that the committed agent performs the action for which she is committed. For instance, getting back to the above example, agent 1's commitment to agent 2 to review the articles could be dropped not only because 1 performs the action for which is committed but also because 2 decides to cancel 1's commitment by assigning to a different programme committee member the reviews that were initially assigned to 1.

Related work

The logic T-STIT presented in Section 2 differs in several aspects from the system proposed by [START_REF] Wölf | Propositional Q-logic[END_REF]. First of all, the language of T-STIT contains the operator [Agt] for the joint action of the grand coalition, while the language of Wölf's logic does not. I have shown that the operator [Agt] is fundamental in order to characterise a basic property relating action and time studied in STIT: the so-called property of no choice between undivided histories. Moreover, different to the system of Wölf, T-STIT does not have extra modal operators such as the difference operator = taken from de Rijke (1992), where = ϕ means that 'ϕ is true in all possible histories that are different from the actual history', and the modal operator ⊟ taken from [START_REF] Maio | A Gabbay-rule free axiomatization of T x W validity[END_REF], where ⊟ϕ means that 'ϕ is true in all possible histories that belong to the current instant'. In this sense, the language of T-STIT is more minimalistic than the language of Wölf's logic, as it contains only those operators which are strictly necessary for talking about tense and action in an interesting way, while Wölf's logic contains the preceding two extra modal operators = and ⊟, which are not necessary for this. Wölf's system and T-STIT are also different at the semantic level. Wölf gives two semantics for his temporal variant of STIT: one based on so-called T × W -based agent frames, which are extensions of T × Wframes [START_REF] Thomason | Combinations of tense and modality[END_REF], and the other based on so-called tree-based agent-frames, which are similar to the BT+AC structures of [START_REF] Belnap | Facing the future: Agents and choices in our indeterminist world[END_REF]. Wölf proves that the two semantics are equivalent. The advantage of the T-STIT semantics given in Section 2.2, compared to Wölf's two semantics, is that the former is closer to the standard semantics of modal logic [START_REF] Blackburn | Modal logic[END_REF], as it is based on the standard notion of Kripke model with accessibility relations. A comparison between the semantics of T-STIT in terms of temporal Kripke STIT models and Wölf's two semantics is deferred to future work.

T-STIT also differs from the system proposed by Broersen (Broersen, 2008a,b) under several aspects. First of all, Broersen presents a variant of STIT called XSTIT in which the temporal dimension and the agency dimension are fused to make up a single modal operator. In particular, in Broersen's logic there are primitive operators describing the effects of an agent's action in 'next' states, where 'next' refers to immediate successors of the present state. On the contrary, in T-STIT, the temporal dimension and the agency dimension are kept separate. Secondly, different to T-STIT, Broersen's logic XSTIT does not have a future tense operator. Thirdly, while the notion of group action used in T-STIT corresponds to the notion of group action given by [START_REF] Horty | Agency and deontic logic[END_REF], the notion of group action in Broersen's XSTIT logic does not. According to Horty's definition, the set of outcomes that is forced by the joint action of a coalition is equal to the pointwise intersection of the sets of outcomes that are forced by the individual actions of the agents in the coalition. In Broersen's logic only the left-to-right direction of [START_REF] Horty | Agency and deontic logic[END_REF] definition holds (i.e., the set of outcomes that is forced by the individual action of an agent in a coalition is included in the set of outcomes that is forced by the joint action of the coalition).

Another logic that is related to the logic T-STIT presented in Section 2 is Schwarzentruber's (2012) variant of STIT with discrete time extended with the tense operator 'next'of linear temporal logic (LTL). Schwarzentruber provides complexity results for this logic without considering the issue of axiomatisation. However, the expressive power of Schwarzentruber's temporal variant of STIT is too limited for modelling normative concepts such as achievement obligation and commitment. Indeed, the tense operator 'next' is insufficient to express temporal properties about commitments such as the fact that an agent is committed to doing something in the future. On the contrary, as I have shown in Section 3, the tense operator G (henceforth) allows us to express such properties.

Conclusion

I have presented in this work a temporal variant of STIT which supports reasoning about the temporal properties of normative concepts such as achievement obligation and commitment. A sound and complete axiomatisation for this logic has been given.

Directions of future work are manifold. I defer to future work an extension of the logic T-STIT by the tense operators until and before of linear temporal logic (LTL; [START_REF] Gabbay | On the temporal analysis of fairness[END_REF]. With these operators it will be possible to provide a definition of commitment based on the notion of deadline of the following form: agent i is committed to agent j to ensure ϕ before the deadline ψ if and only if, if i does not see to it that ϕ before ψ becomes true, then j will be wronged by i.

Another issue that I plan to investigate in future research is a comparison between the Kripke-style semantics of T-STIT given in Section 2 and an alternative semantics for T-STIT based on the original notion of the BT+AC structures of [START_REF] Belnap | Facing the future: Agents and choices in our indeterminist world[END_REF]. Indeed, while the two semantics are clearly equivalent in the case of atemporal individual STIT and atemporal group STIT, one might wonder whether they lead to two different sets of validities in the case of T-STIT and, if so, whether the validities differentiating the two semantics capture interesting and intuitive properties.

Finally, on the technical side, I intend to provide an alternative axiomatisation of T-STIT which does not make use of the Gabbay-style irreflexivity rule (IRR). Indeed, following Zanardo (1996, Theorem 6.12), it seems possible to find such an alternative axiomatisation in which the rule (IRR) is replaced with a set of more complex axiom schemas.

Another issue for future work is decidability of the satisfiability problem of T-STIT. It has been proved by [START_REF] Herzig | Properties of logics of individual and group agency[END_REF] that Horty's group STIT with group agency operators for all coalitions is undecidable. However, the logic T-STIT only has the group agency operator for the grand coalition. Because of this limitation in the expressive power of T-STIT, I believe that its satisfiability problem is decidable.

Figure 1 .

 1 Figure 1. Example of temporal Kripke STIT model. Note: The world w is the actual world. Choices of agent 1 are represented by columns whereas choices of agent 2 are represented by rows. Choices of the group {1, 2} are represented by dotted rectangles. The temporal relation R G is represented by the arrows.

  . Thus, there exists ū ∈ PA ϕ w such that R G (w) = R G ( ū). Hence, by Constraint C5, there exists ū ∈ PA ϕ w such that w = ū.

Figure 2 .

 2 Figure 2. Axiomatisation of T-STIT.

  The last part of the proof consists in proving that the submodel of the canonical model for T-STIT including all IRR theories, i.e., the model M c | IrrTh , is indeed a superadditive temporal Kripke STIT model. The following two propositions ensure that M c | IrrTh satisfies the Constraints C2 and C6.

  , Chapter 7). ϕ stands for 'ϕ is true regardless of what every agent does' or 'ϕ is true no matter what the agents do' or simply 'ϕ is necessarily true'. I define the dual of as follows: ♦ϕ Note that the operators [i] and ♦ can be combined in order to express what agents can do: ♦[i]ϕ means 'agent i can see to it that ϕ'. Moreover, the operators [i] and can be combined in order define the deliberative STIT operators [i dstit: ] studied by

def = ¬ ¬ϕ.

  Given a T-STIT formula ϕ, I say that ϕ is T-STIT valid, denoted by |= T-STIT ϕ, if and only if for every temporal Kripke STIT model M and for every world w in M we have M, w |= ϕ. I say that ϕ is satisfiable in T-STIT if and only if ¬ϕ is not T-STIT valid.

  Definition 8 (Superadditive temporal Kripke STIT model). The class of superadditive temporal Kripke STIT models includes all tuples M

Acknowledgements

The author acknowledges the support of the LabEx project CIMI. Moreover, he is grateful to Valentin Goranko for his helpful comments on the content of this work.

Notes

1. The distinction between the 'Ockhamist' view and the 'Peircean' view of branching time was proposed by [START_REF] Prior | Past, present, and future[END_REF] seminal work on the logic of time. According to the 'Peircean' view, the truth of a temporal formula should be evaluated with respect either to some history or all histories passing through a given moment. The 'Ockhamist' view considers a notion of actual course of events. In particular, according to the 'Ockhamist' view, the truth of a temporal formula should be evaluated with respect to a particular actual history passing through a given moment. 3. Xu (1998) considers a family of axiom schemas (AIA k ) for independence of agents of the form

The function

that is parameterised by the integer k. As pointed out by [START_REF] Belnap | Facing the future: Agents and choices in our indeterminist world[END_REF], (AIA k+1 ) implies (AIA k ). Therefore, as Agt is finite, in T-STIT the family of axiom schemas can be replaced by the single axiom (AIA). [START_REF][END_REF]. The notion of achievement obligation is traditionally opposed to the concept of maintenance obligation (i.e., the obligation to maintain a given state of affairs ϕ). 5. Starting from [START_REF] Hohfeld | Some fundamental legal conceptions as applied in legal reasoning[END_REF], in legal theory it is assumed that a right for j towards i that ϕ is brought about by i typically correlates with a directed obligation for i towards j to bring about ϕ (i.e., a duty of i towards j to bring about ϕ). 6. Note that a similar property of persistence characterises the notion of intention [START_REF] Bratman | Intentions, plans, and practical reason[END_REF] and has been formally characterised in some logical theories of intention [START_REF] Cohen | Intention is choice with commitment[END_REF][START_REF] Lorini | A logic of intention and attempt[END_REF]).

Suppose that w f ∈ W ′ and ( f (w f ), v) ∈ R i . This implies that (w, v) ∈ R i . Therefore, R i (w) = R i (v) as R i is an equivalence relation. Hence, δ v i = δ w i . It follows that (w f , v f ′ ) ∈ R ′ i where the function f ′ is defined as follows: (i) f ′ i (δ v ) = f i (δ w ) and all f ′ j (δ v ) with j = i are such that v ∈ Ŵ

This function f ′ is guaranteed to exist because of the observation (D) above and the fact that R i ⊆ R .

Suppose that w f ∈ W ′ and ( f (w f ), v) ∈ R Agt . This implies that (w, v) ∈ R Agt . Therefore, R Agt (w) = R Agt (v) as R Agt is an equivalence relation. Hence,

Agt where the function f ′ is defined as follows:

. This function f ′ is guaranteed to exist because of the observation (D) above and the fact that R Agt ⊆ R .

Suppose that

In order to terminate the proof we also need to be sure that M ′ is a temporal Kripke STIT model in the sense of Definition 1. It is a routine task to show that R ′ i , R ′ Agt and R ′ are equivalence relations, that the model transformation preserves transitivity and seriality for the relation R ′ G , and that the model M ′ satisfies the Constraints C1, C2, C4, C5 and C7. Let me prove that it also satisfies Constraints C3 and C6.

From the latter and the fact that

This proves that the model M ′ satisfies the Constraint C6. The following lemma provides an axiomatisation result for the class of superadditive temporal Kripke STIT models.

Lemma 10. The set of T-STIT formulas that are valid in the class of superadditive

temporal Kripke STIT models is completely axiomatised by the principles given in Figure 2. Proof. In order to prove Lemma 10, I use a technique similar to the one used by [START_REF] Gabbay | Temporal logic: Mathematical foundations and computational aspects[END_REF] for proving completeness of linear temporal logic and of logic of historical necessity by means of a slightly different variant of the irreflexivity rule (IRR).

Let me start with the following standard definition of canonical model for T-STIT.

Definition 11 (Canonical model for T-STIT). The canonical model M c for T-STIT is the

) where:

H are respectively the canonical relations for , [i], [Agt], G and H, that is:

-

Furthermore, let me introduce the notion of 'diamond'-saturation for maximal consistent sets of T-STIT formulas.

Definition 12 (Diamond saturated set of MCSs). Given a set X of maximal consistent sets of T-STIT formulas, I say that X is a diamond saturated set of MCSs if and only if for each Ŵ ∈ X the following five conditions are satisfied:

Agt and ϕ ∈ ;

H and ϕ ∈ . The following truth lemma is provable in the standard way by induction on ϕ (see Blackburn et al., 2001, Lemma 4.70 The formula name ( p) acts as a sort of 'name' for a given world that ensures irreflexivity of the canonical relation R c

G for the future tense operator G.

Furthermore, let

Finally, for every ϕ = 1 (ψ 1 ∧ 2 (ψ 2 ∧ . . . ∧ n ψ n ) . . .) ∈ and for every atom p, let

.).

A formula of the form ϕ( p) is also used as a 'name' for a given world. In particular, formulas of the form ϕ( p) provide 'names' for worlds that are reachable by any zig-zagging sequence of ♦s, i s, Agt s, Fs and Ps.

Definition 14 (IRR theory). An IRR theory is a maximal consistent set of T-STIT formulas Ŵ such that:

• for some p, name ( p)

The set of all IRR theories is denoted by IrrTh.

The following lemma highlights that every consistent T-STIT formula is included in at least one IRR theory. The rule of inference (IRR) becomes crucial at this point of the proof.

Lemma 15. Let ϕ be a consistent T-STIT formula. Then, there exists an IRR theory Ŵ such that ϕ ∈ Ŵ.

(Sketch). The lemma is proved analogously to Lemma 6.2.4 in Gabbay et al. (1994, Chapter 6). Since the set Atm of propositional atoms is infinite, there exists an infinite number of atomic formulas p not occurring in ϕ. Therefore, thanks to the (IRR) rule, it is straightforward to build step-by-step an IRR theory Ŵ containing ϕ.

The following lemma highlights that the set of all IRR theories satisfies the condition of 'diamond'-saturation defined above (Definition 12).

Lemma 16 (Existence Lemma).

Let Ŵ be an IRR theory. Then:

• if ♦ϕ ∈ Ŵ, then there is an IRR theory such that (Ŵ, ) ∈ R c and ϕ ∈ ;

• if i ϕ ∈ Ŵ, then there is an IRR theory such that (Ŵ, ) ∈ R c i and ϕ ∈ ;

H and ϕ ∈ . Proof. I only prove the first item. The other items can be proved analogously.

Suppose ♦ϕ ∈ Ŵ. Since Ŵ is an IRR theory, it follows that ♦(ϕ ∧ name( p)) ∈ Ŵ for some atom p. Let 0 = {ϕ ∧ name( p)} ∪ {ψ| ψ ∈ Ŵ}. I am going to show that 0 is consistent by reductio ad absurdum. Suppose 0 is not consistent. Then, for some ψ 1 , . . . , ψ k ∈ {ψ| ψ ∈ Ŵ}, we have: Proof. First of all, it is a routine task to prove that: (i) the canonical relations R c , R c i and

H is the inverse of the canonical relation R c G ; and (iv) the canonical model M c satisfies the Constraints C1, C3 * , C4 and C5.

Indeed, Axioms T, 4 and B for , [i] and for [Agt] are canonical for reflexivity, transitivity and symmetry thereby ensuring that the canonical relations R c , R c i and R Theorem 7 follows from Lemma 9 and Lemma 10.

Application to normative reasoning

Many normative concepts such as achievement obligation, obligation with deadline and social commitment have an intrinsic agentive and temporal nature -that is to say, they cannot be properly understood without considering their relationships with the concepts of action and time. The aim of this section is to show that the logic T-STIT is expressive enough to capture some of these relationships. I focus on the notion of social commitment and on its relationship with the notion of achievement obligation, postponing the logical analysis of obligations with deadline in STIT to future work.

According to [START_REF] Singh | An ontology for commitments in multiagent systems[END_REF] and [START_REF] Castelfranchi | Commitment: From individual intentions to groups and organizations[END_REF], a social commitment is a kind of normative relationship between a debtor and a creditor. The contexts in which commitments