Emiliano Lorini

A Logical Account of Social Rationality in Strategic Games

Keywords:

We propose a modal logic that enables to reason about different kinds of rationality in strategic games. This logic integrates the concepts of joint action, belief, individual preference and group preference. The first part of the article is focused on the notion of individualistic rationality assumed in classical game theory: an agent decides to perform a certain action only if the agent believes that this action is a best response to what he expects the others will do. The second part of the article explores different kinds of social rationality such as fairness and reciprocity. Differently from individualistically rational agents (alias self-interested agents), social rational agents also consider the benefits of their choice for the group. Moreover, their decisions can be affected by their beliefs about other agents' willingness to act for the wellbeing of the group. In the article we also provide a complete axiomatization of our logic of joint action, belief, individual preference and group preference.

Introduction

In recent times economic theory has started to refute the standard assumption that people are individualistically rational, that is, that they are necessarily motivated by their material self-interest. Several experiments have demonstrated that people are often driven by otherregarding motives, and by social preferences. Consequently, the classical game-theoretic framework has been revised and extended in order to incorporate new important concepts such as fairness, inequity aversion, altruism and reciprocity. Several models of social rationality have been developed in recent years showing that the phenomena observed in experiments with humans can be explained in a rigorous and tractable manner. Following [START_REF] Fehr | Theories of fairness and reciprocity: Evidence and economic applications[END_REF], we can distinguish two families of models of social rationality in economics. Some models assume that players are only concerned about the distributional consequences of their acts but they do not care about the intentions that lead their opponents to choose these acts. For example, according to [START_REF] Fehr | A theory of fairness, competition, and cooperation[END_REF], players are inequity averse and may also care about how much material resources are allocated to other players. Other models assume that the behavior of a player during social interaction depends on the player's beliefs and expectations about the intention of the opponent. 1 For example, according to Rabin's model of reciprocity [START_REF] Rabin | Incorporating fairness into game theory and economics[END_REF], a person is willing to be kind with another person if she believes that the other has been kind to her. On the contrary, a person has a desire to retaliate, if she believes that the other person wanted to hurt her.

Although social preferences and social rationality have been extensively studied in experimental economics, no logical analysis of these concepts has been proposed up to now. In this article, we try to fill this gap by proposing a sound and complete modal logic which enables to model social preferences and to reason about different kinds of social rationality in strategic games. This logic is based on the primitive concepts of joint action, belief, individual preference and group preference.

We think that developing logical models of social interaction integrating social preferences is a promising research avenue especially for the area of multi-agent systems and for the area of social software. Indeed, existing logical models of social interaction proposed in these areas are still anchored to the basic assumption of classical game theory that agents are self-interested. As emphasized above, this assumption is unrealistic for human agents. Therefore, to take the presence of other-regarding preferences into account becomes extremely important when developing formal models of social procedures to be applied to human societies, and when developing logical models of artificial agents which have to interact with human agents (e.g. trading agents, recommender systems, tutoring agents, etc.).

The remainder of the article is organized as follows. In Section 2 we present a modal logic of epistemic strategic games called L integrating the concepts of joint action, individual preference and belief. Section 3 is devoted to the analysis in L of some basic gametheoretic concepts such as best response and Nash equilibrium, and of the notion of individualistic rationality assumed in classical game theory (i.e. agents are self-interested). In Section 4 the logic L is extended by operators of group preference. Section 5 explores two different kinds of social rationality: fairness and reciprocity. Differently from individual-istically rational agents (alias self-interested agents), social rational agents also consider the benefits o f t heir c hoice f or t he g roup. M oreover, t heir d ecisions c an b e a ffected by their beliefs about other agents' willingness to act for the well-being of the group. Section 6 discusses related works in the area of modal logics for game theory.

A logic of epistemic strategic games

We present in this section the modal logic L integrating the concepts of joint action, belief and individual preference. This logic supports reasoning about epistemic games in strategic form in which an agent might be being uncertain about the current choices of the other agents.

Syntax

The syntactic primitives of L are the finite set of agents Agt, the set of atomic formulas Atm, a nonempty finite s et o f a tomic a ction n ames A ct = {a 1 , a 2 , . . . , a |Act| }, a nonempty finite set of n integers I = {0, . . . , n }. Non-empty sets of agents are called coalitions or groups, noted C 1 , C 2 , . . .. We note 2 Agt * = 2 Agt \ ∅ the set of coalitions.

To every agent i ∈ Agt we associate the set Act i of all possible ordered pairs i:a, that is, Act i = {i:a | a ∈ Act}. Besides, for every coalition C we note ∆ C the set of all joint actions of this coalition, that is,

∆ C = i∈C Act i . Elements in ∆ C are C-tuples noted α C , β C , γ C , δ C , . . .. If C = Agt, we write ∆ instead of ∆ Agt .
Elements in ∆ are also called strategy profiles. Given δ ∈ ∆, we note δ i the element in δ corresponding to agent i. Moreover, for notational convenience, we write δ -i = δ Agt\{i} .

The language L of the logic L is given by the following BNF:

ϕ ::= p | ⊥ | ¬ϕ | ϕ ∨ ϕ | [δ C ]ϕ | ϕ | [B i ]ϕ | [≥ k i ]ϕ
where p ranges over Atm, i ranges over Agt, δ C ranges over C∈2 Agt * ∆ C , and k ranges over I. The classical Boolean connectives ∧, →, ↔ and (tautology) are defined from ⊥, ∨ and ¬ in the usual manner.

The formula [δ C ]ϕ reads "if coalition C chooses the joint action δ C then ϕ holds". Therefore, [δ C ]⊥ reads "coalition C does not choose the joint action δ C ".

The operator is an universal modality, which quantifies over all worlds of the current model. Since in our framework, there is a one-to-one correspondence between models and games (i.e. a model corresponds to a unique strategic game), and every world in a model corresponds to a unique strategy profile of a strategic game, is used to quantify over the strategy profiles of the current game. ϕ reads "ϕ holds for all strategies profiles of the current game", or simply "ϕ is necessarily true". The formula [B i ]ϕ is read as usual "agent i believes that ϕ", whereas the formula [≥ k i ]ϕ is read "ϕ is true in all states which are good for agent i at least to degree k". Operators [≥ k i ] are used in L to define agents' preference orderings over the strategy profiles of the current game.

Moreover, we have the following abbreviations:

δ C ϕ def = ¬[δ C ]¬ϕ, ♦ϕ def = ¬ ¬ϕ, B i ϕ def = ¬[B i ]¬ϕ, ≥ k i ϕ def = ¬[≥ k i ]¬ϕ.
♦ ϕ has to be read "ϕ is possibly true", and δ C ϕ has to be read "coalition C chooses the joint action δ C and ϕ holds". Therefore, δ C simply means "coalition C chooses the joint action δ C ". ≥ k i ϕ has to read "ϕ is true in at least one state which is good for agent i at least to degree k". B i ϕ has to be read "agent i thinks that ϕ is possible".

Semantics

Definition 1 (L-model). L-models are tuples M = W, R, B, P, π where:

• W is a nonempty set of possible worlds or states;

• R is a collection of total functions R C : W -→ ∆ C one for every coalition C ∈ 2 Agt * , mapping every world in W to a joint action of the coalition such that:

C1 δ C = R C (w) if and only if, for every i ∈ C δ i = R i (w), and
C2 if for every i ∈ Agt there is w i ∈ W such that δ i = R i (w i ) then there is a w ∈ W such that δ = R Agt (w), C3 if δ = R Agt (w) and δ = R Agt (v), then w = v; • B : Agt -→ 2 W ×W is
⊆ P k-1 i ; • π : Atm -→ 2 W is a valuation function.
For every coalition C, δ C = R C (w) means that at world w coalition C chooses the joint action δ C . Furthermore, if there exists w ∈ W such that C performs δ C at w then we say that δ C is possible or that δ C can be performed. Thus, δ can be performed if and only if δ is a strategy profile of the current game.

For every agent i, (w, v) ∈ B i means that at world w, according to agent i, world v is possible. Finally, the function P is used to specify the degree of goodness of a certain world according to a given agent. In particular, for every k ∈ I and i ∈ Agt, P k i is the set of worlds that are good for agent i at least to degree k.

Let us discuss the six semantic constraints C1-C6 in Definition 1.

According to Constraint C1, at world w coalition C chooses the joint action δ C if and only if, every agent i in C chooses the action δ i at w. In other words, a certain joint action is performed by a coalition if and only if every agent in the coalition does his part of the joint action. According to the Constraint C2, if every individual action in a joint action δ is possible, then their simultaneous occurrence is also possible. We moreover suppose determinism for the joint actions of all agents: different worlds in the same model correspond to the occurrences of different strategy profiles (Constraint C3).

Constraint C4 just says that agents believe what they are doing. This is a standard assumption in interactive epistemology and epistemic analysis of games (see [START_REF] Bonanno | A syntactic approach to rationality in games with ordinal payoffs[END_REF] for instance).

According to Constraint C5, every world is good for an agent i at least to minimal degree 0. This implies that an agent can always compare the goodness of two different worlds. According to the Constraint C6, for every integer k ∈ I \ {0}, the set of worlds that are good for agent i at least to degree k is a subset of of the set of worlds that are good for agent i at least to degree k-1. This means that worlds in a model are ordered according to their degrees of goodness for an agent and form a "system of spheres" [START_REF] Lewis | Counterfactuals[END_REF] for every agent i. In particular, an ordinal conditional function (OCF) κ i : W -→ I in Spohn's sense [START_REF] Spohn | Ordinal conditional functions: a dynamic theory of epistemic states[END_REF] can be associated with every agent i, where κ i (w) corresponds to the exact degree of goodness of world w for agent i. 2Definition 2 ( κ i ). For every i ∈ Agt and for every w ∈ W we define:

• κ i (w) = n if and only if w ∈ P n i ; • for every k ∈ I such that k < n, κ i (w) = k if and only if w ∈ P k i and w ∈ P k+1 i .
Example 1. By way of example, consider a two-player Prisoner Dilemma (PD) game [START_REF] Osborne | A course in game theory[END_REF]. We suppose Agt = {i 1 , i 2 } and ACT = {c, d } where c is the action of cooperating and d is the action of defecting. In order to model PD game we just need four different degrees of goodness I = {0, 1, 2, 3}. The elements W, R and P of the model M corresponding to the two-player PD game are defined as follows:

• W = {w 1 , w 2 , w 3 , w 4 }; • R {i 1 ,i 2 } (w 1 ) = i 1 :c, i 2 :c , R {i 1 ,i 2 } (w 2 ) = i 1 :d, i 2 :d , R {i 1 ,i 2 } (w 3 ) = i 1 :c, i 2 :d , R {i 1 ,i 2 } (w 4 ) = i 1 :d, i 2 :c ; • P 3 i 1 = {w 4 }, P 2 i 1 = {w 1 , w 4 }, P 1 i 1 = {w 1 , w 2 , w 4 }, P 0 i 1 = {w 1 , w 2 , w 3 , w 4 }; • P 3 i 2 = {w 3 }, P 2 i 2 = {w 1 , w 3 }, P 1 i 2 = {w 1 , w 2 , w 3 }, P 0 i 2 = {w 1 , w 2 , w 3 , w 4 }.
World w 3 (resp. w 4 ) belongs to P 0 i 1 (resp. P 0 i 2 ) and does not belong to P 1 i 1 (resp. P 1 i 2 ), hence it is a world that is good for agent i 1 (resp. agent i 2 ) exactly to degree 0. That is,

κ i 1 (w 3 ) = 0 (resp. κ i 2 (w 4 ) = 0).
World w 2 belongs to P 1 i 1 (resp. P 1 i 2 ) and does not belong to

P 2 i 1 (resp. P 2 i 2 ), hence it is a world that is good for agent i 1 (resp. agent i 2 ) exactly to degree 1. That is, κ i 1 (w 2 ) = 1 (resp. κ i 2 (w 2 ) = 1).
World w 1 belongs to P 2 i 1 (resp. P 2 i 2 ) and does not belong to

P 3 i 1 (resp. P 3 i 2 ), hence it is a world that is good for agent i 1 (resp. agent i 2 ) exactly to degree 2. That is, κ i 1 (w 1 ) = 2 (resp. κ i 2 (w 1 ) = 2).
World w 4 (resp. w 3 ) belongs to

P 3 i 1 (resp. P 3 i 2 ), hence it is a world that is good for agent i 1 (resp. agent i 2 ) exactly to degree 3. That is, κ i 1 (w 4 ) = 3 (resp. κ i 2 (w 3 ) = 3).
For every OCF function κ i , we define the corresponding preference order i over the worlds in W .

Definition 3 ( i ). For every i ∈ Agt and for every w, v ∈ W we have w i v if and only if κ

i (w) ≤ κ i (v).
Truth conditions for atomic formulas and the Boolean operators are entirely standard. The truth conditions for the operators of the logic L are:

• M, w |= [δ C ]ϕ ⇐⇒ if δ C = R C (w) then M, w |= ϕ; • M, w |= ϕ ⇐⇒ M, v |= ϕ for all v such that v ∈ W ; • M, w |= [B i ]ϕ ⇐⇒ M, v |= ϕ for all v such that (w, v) ∈ B i ; • M, w |= [≥ k i ]ϕ ⇐⇒ M, v |= ϕ for all v such that v ∈ P k i . A formula ϕ is true in an L-model M iff M, w |= ϕ for every world w in M . ϕ is L-valid (noted |= ϕ) iff ϕ is true in all L-models. ϕ is L-satisfiable iff ¬ϕ is not L-valid.

Axiomatization

All principles of classical propositional logic (CPL)

All principles of modal logic S5 for (S5 )

All principles of modal logic KD45 for every

[B i ] (S5 [B i ] ) All principles of modal logic K for every [≥ k i ] (K [≥ k i ] ) [δ C ]ϕ ↔ ( δ C → ϕ) (Def [δ C ] ) δ C ↔ i∈C δ i (JointAct) δ C ∈∆ C δ C (Active) δ C → [δ C ]⊥ if δ C = δ C (Single)   i∈Agt ♦ δ i   → ♦ δ (Indep) ( δ ∧ ϕ) → ( δ → ϕ) (JointDet) i:a ↔ [B i ] i:a (Aware) ϕ → [B i ]ϕ (Incl ,[B i ] ) ϕ → [≥ k i ]ϕ (Incl ,[≥ k i ] ) [≥ 0 i ]ϕ ↔ ϕ (Def [≥ 0 i ] ) [≥ k-1 i ]ϕ → [≥ k i ]ϕ (Incl [≥ k-1 i ],[≥ k i ] ) [≥ k i ]ϕ → [≥ k i ]ϕ (PNec [≥ k i ] ) ¬[≥ k i ]ϕ → ¬[≥ k i ]ϕ (NNec [≥ k i ] )
Table 1: Axiomatization of L

We call L the logic that is axiomatized by the principles given in Table 1, and we write

L ϕ if ϕ is a theorem of L.
Note that Axiom Indep is the L counterpart of the so-called axiom of independence of agents of STIT logic [START_REF] Belnap | Facing the future: agents and choices in our indeterminist world[END_REF]. This axiom enables to express the basic game theoretic assumption that the set of strategy profiles o f a g ame i n s trategic f orm i s t he cartesian product of the sets of individual actions for the agents in Agt. Note also that Axiom Def [δ C ] could be replaced by the simpler Axiom ϕ → [δ C ]ϕ. We have chosen Def [δ C ] because we think that it better expresses the meaning of the operators [δ C ]. Furthermore, by the Axiom Def [δ C ] , we can prove that every operator [δ C ] satisfies all principles of the basic modal logic K and, in particular, Axiom K:

(1) L ([δ C ]ϕ ∧ [δ C ](ϕ → ψ)) → [δ C ]ψ,
and the rule of necessitation:

(2) if L ϕ then L [δ C ]ϕ.
The following property is also derivable by Axiom T for and Axiom

Def [δ C ] : L ϕ → [δ C ]ϕ.
Theorem 1. The logic L is sound and complete with respect to the class of L-models.

Proof. We here provide a sketch of the proof.

It is straightforward to show that all our axioms are valid and that the rules of inference preserve validity in the class of L-models. The other part of the proof is shown using two major steps.

Step 1. We provide an alternative semantics for L in terms of standard Kripke models whose semantic conditions correspond one-to-one to the axioms in Table 1. The definition of Kripke L-models is the following one.

Definition 4 (Kripke L-model). Kripke L-models are tuples M = W, ∼, R, B, P, π where:

• W is a nonempty set of possible worlds or states;

• ∼ is an equivalence relation on W ; • R : C∈2 Agt * ∆ C -→ 2 W ×W maps every joint action δ C to a transition relation R δ C ⊆ W × W between possible worlds such that: S1 R δ C (w) = ∅ if and only if, for every i ∈ C R δ i (w) = ∅, S2 if R δ C (w) = ∅ then R δ C (w) = {w}, S3 δ C ∈∆ C R δ C (w) = ∅, S4 if δ C = δ C then R δ C (w) = ∅ or R δ C (w) = ∅, S5 if for every i ∈ Agt there is v i such that w ∼ v i and R δ i (v i ) = ∅ then there is a v such that w ∼ v and R δ (v) = ∅, S6 if w ∼ v and R δ (w) = ∅ and R δ (v) = ∅, then w = v; • B : Agt -→ 2 W ×W is
S7 if (w, v) ∈ B i , then i:a = R i (w) if and only if i:a = R i (v), S8 if (w, v) ∈ B i then w ∼ v;
• P : I × Agt -→ 2 W ×W maps every integer k in I and agent i in Agt to a binary relation

P k i on W such that: S9 P 0 i (w) =∼(w), S10 P k i (w) ⊆∼(w), S11 if k ∈ I \ {0} then P k i (w) ⊆ P k-1 i (w), S12 if w ∼ v then P k i (w) ⊆ P k i (v), S13 if w ∼ v then P k i (v) ⊆ P k i (w); • π : Atm -→ 2 W is a valuation function.
As in the previous Constraint C2, accessibility relations on W can be viewed as functions from W to 2 W . Therefore, we write

∼(w) = {v | w ∼ v}, P k i (w) = {v | (w, v) ∈ P k i }, etc.
Truth conditions of L formulas in Kripke L-models are again standard for atomic formulas and the Boolean operators. The truth conditions for the other operators are:

• M, w |= [δ C ]ϕ ⇐⇒ M, v |= ϕ for all v ∈ R δ C (w); • M, w |= ϕ ⇐⇒ M, v |= ϕ for all v ∈∼(w); • M, w |= [B i ]ϕ ⇐⇒ M, v |= ϕ for all v ∈ B i (w); • M, w |= [≥ k i ]ϕ ⇐⇒ M, v |= ϕ for all v ∈ P k i (w).
It is a routine task to prove that the axiomatic system of the logic L given in Table 1 is sound and complete with respect to this class of Kripke L-models via the Sahlqvist theorem, cf. [6, Th. 2.42]. Indeed all axioms in Table 1 are in the so-called Sahlqvist class [START_REF] Sahlqvist | Completeness and correspondence in the first and second order semantics for modal logics[END_REF]. Thus, they are all expressible as first-order conditions on Kripke models and are complete with respect to the defined model classes.

Step 2. The second step shows that the semantics in terms of L-models of Definition 1 and the semantics in terms of Kripke L-models of Definition 4 are equivalent. As the logic L is sound and complete for the class of Kripke L-models and is sound for the class of L-models, we have that for every L formula ϕ, if ϕ is valid in the class of Kripke L-models then ϕ is valid in the class of L-models. Consequently, for every L formula ϕ, if ϕ is satisfiable in the class of L-models then ϕ is satisfiable in the class of Kripke L-models. Therefore, in this second step we just need to show that for every L formula ϕ, if ϕ is satisfiable in the class of Kripke L-models then ϕ is satisfiable in the class of L-models.

Suppose ϕ is satisfiable in the class of Kripke L-models. This means that there is a Kripke L-model M = W, ∼, R, B, P, π and world w such that M, w |= ϕ. We can now build a L-model M = W , R , B , P , π which satisfies ϕ. The construction of the model M is made in two steps. We first consider the submodel M w = W w , ∼ w , R w , B w , P w , π w generated from M and w: by the generated submodel property [START_REF] Blackburn | Modal Logic[END_REF] we have M w , w |= ϕ. M w is also a Kripke L-model, and ∼ w = W w × W w . The latter means that is interpreted as a universal modal operator. Finally, we can define M = W , R , B , P , π as follows:

• W = W w ; • for every C ∈ 2 Agt * and v ∈ W , R C (v) = δ C if and only if R δ C ,w (v) = ∅; • for every i ∈ Agt, B i = B i,w ;
• for every i ∈ Agt and k ∈ I, P k i = P k i,w (w);

• π = π w .
It is a routine task to check that M is indeed a L-model and, by induction on the structure of ϕ, that we have M , w |= ϕ.

Strategic games with individual rationality

This section is devoted to the analysis in the logic L of strategic games in which agents are self-interested. We first define preference operators. Then, we consider the basic gametheoretic concepts of best response and Nash equilibrium, and their relationships with the notion of individualistic rationality assumed in classical game theory.

Preferences over formulas

For every i ∈ Agt, we define a preference relation over formulas:

ψ ≤ i ϕ def = k∈I ( ≥ k i ψ → ≥ k i ϕ).
According to this definition "ϕ is for agent i at least as good as ψ" (noted ψ ≤ i ϕ) if and only if for every integer k ∈ I if ψ is true in at least one state which is good for agent i at least to degree k then ϕ is also true in at least one state which is good for agent i at least to degree k. The following are central properties of the operator ≤ i . For every i ∈ Agt we have:

L ψ ≤ i ψ (3) L ((ϕ 1 ≤ i ϕ 2 ) ∧ (ϕ 2 ≤ i ϕ 3 )) → (ϕ 1 ≤ i ϕ 3 ) (4) L (ϕ 1 ≤ i ϕ 2 ) ∨ (ϕ 2 ≤ i ϕ 1 ) (5) L ⊥ ≤ i (6) if L ϕ → (ψ 1 ∨ ... ∨ ψ s ) then L (ϕ ≤ i ψ 1 ) ∨ ... ∨ (ϕ ≤ i ψ s ) (7)
The L-theorems 3-5 highlight that ≤ i is a total preorder. The L-theorems 4-6 are exactly the three fundamental principles of Lewis's conditional logic (called VN ) [START_REF] Lewis | Counterfactuals[END_REF]. The language of Lewis's logic VN is that of classical logic augmented with a dyadic connective ≤. In this sense, the operators ≥ k i enables to reconstruct Lewis' dyadic connective. A similar result has been proved by del Cerro & Herzig [START_REF] Del Cerro | A modal analysis of possibility theory[END_REF] in the 90ies. The two authors have developed a modal logic of possibility called PL in which a normal operator of the form [x] for every parameter x in a set of parameters P is introduced (the dual of [x] is noted x ). In a way similar to the L formula [≥ k i ]ϕ, the PL formula [x] ϕ is read "the necessity of formula ϕ is at least degree x". PL have the standard axioms and rules of inference of system K for every operator [x] plus the following two axioms:

PL1 ¬ [1] ⊥ PL2 ([x] ϕ → [y] ϕ) ∨ ([x] ϕ → [y] ϕ) for every x, y ∈ P
where 1 is a particular element in the set of parameters P . The two authors reconstruct Lewis's preferential operators by means of the following translation from PL to Lewis's conditional logic: ψ ≤ ϕ def = x∈P ( x ψ → x ϕ). 3 We can easily prove that our logic L satisfies the previous two properties of del Cerro & Herzig's logic. Indeed, the following L-theorem is provable by Axiom Def [≥ 0 i ] and by Axiom T for : [START_REF] Boutilier | Modal logics for qualitative possibility and beliefs[END_REF] L ¬[≥ 0 i ]⊥. This L-theorem corresponds to Axiom PL1 of PL. Moreover, by the

L Axiom Incl [≥ k-1 i ],[≥ k i ] ,
the following L-theorem is also provable for every k, h ∈ I:

(9) L ([≥ k i ]ϕ → [≥ h i ]ϕ) ∨ ([≥ k i ]ϕ → [≥ h i ]ϕ)
This L-theorem corresponds to Axiom PL2 of PL. On the contrary in PL we cannot infer a theorem which corresponds to the L Axiom

Incl [≥ k-1 i ],[≥ k i ]
, that is, in PL we cannot infer as a theorem something like [x] ϕ → [y] ϕ if x < y. In this sense, the fragment of our logic L with preferential operators of type [≥ k i ] can be seen as a generalization of PL.

Before concluding let us define ψ <

i ϕ def = (ψ ≤ i ϕ) ∧ ¬(ϕ ≤ i ψ), δ ≤ i δ def = δ ≤ i δ and δ < i δ def = (δ ≤ i δ ) ∧ ¬(δ ≤ i δ).

Best response and Nash equilibrium

Some basic concepts of game theory can be expressed in L in terms of comparative goodness. We first consider best response. Agent i's action a is said to be a best response to the other agents' joint action δ -i , noted BR(i:a,δ -i ), if and only if i cannot improve his utility by deciding to do something different from a while the others choose the joint action δ -i , that is:

BR(i:a,δ -i ) def = b∈Act (( i:b ∧ δ -i ) ≤ i ( i:a ∧ δ -i )).
Given a certain strategic game, the strategy profile (or joint action) δ is said to be a Nash equilibrium if and only if for every agent i ∈ Agt, i's action δ i is a best response to the other agents' joint action δ -i :

Nash(δ) def = i∈Agt BR(δ i ,δ -i ).
Example In order to show that the previous formalization of Nash equilibrium is correct, we need to introduce the definition of strategic game in the game-theoretic sense, and then we need a notion of correspondence between strategic games and L-models.

Definition 5 (Strategic g ame). A strategic game is a tuple Γ = N, A, U where N is a finite set of agents and:

• A is a collection of sets of actions A i one for every agent i ∈ N ;

• U is a collection of total preorders ≤ U i over i∈Agt A i , one for every agent i ∈ Agt.

The strategy profile δ is a Nash equilibrium in the game Γ if and only if, for every i ∈ N and for every

δ i ∈ A i , (δ i , δ -i ) ≤ U i (δ i , δ -i ).
Definition 6 (Γ ≈ M ). We say that a strategic game Γ corresponds to a L-model M = W, R, B, P, π , noted Γ ≈ M , if and only if the following conditions are met:

• Agt = N ;
• for every i ∈ Agt, A i = {i:a | a ∈ Act and there is w ∈ W such that R i (w) = i:a};

• for every i ∈ Agt, and for every δ, δ

∈ i∈Agt A i , δ ≤ U i δ if and only if R -1 Agt (δ ) i R -1 Agt (δ);
where R -1 Agt is the inverse function of R Agt . 4Proposition 1. Suppose that Γ ≈ M and δ ∈ i∈Agt A i . Then, we have M, w |= Nash(δ) for every w ∈ W if and only if, δ is a Nash equilibrium in the game Γ.

Individualistic rationality

The following L formula characterizes a notion of individualistic rationality which is commonly supposed in the epistemic analysis of games (see, e.g., [START_REF] Battigalli | Recent results on belief, knowledge and the epistemic foundations of game theory[END_REF][START_REF] Van Benthem | Rational dynamics and epistemic logic in games[END_REF]):

a,b∈Act ( i:a → δ∈∆ ( B i δ -i ∧ ( δ -i , i:b ≤ i δ -i , i:a ))
). This means that an agent i is (individualistically) rational if and only if, if he chooses a particular action a then for every alternative action b, there exists a joint action δ -i of the other agents that he considers possible such that, playing a while the others play δ -i is for i at least as good as playing b while the others play δ -i . As in L δ ≤ i δ and [B i ](δ ≤ i δ ) are equivalent, the previous definition of rationality can be rewritten in the following equivalent form:

IRat i def = a,b∈Act i:a → δ∈∆ ( B i δ -i ∧ [B i ] ( δ -i , i:b ≤ i δ -i , i:a )) .
For every i ∈ Agt we have:

L IRat i ↔ [B i ]IRat i (10) L ¬IRat i ↔ [B i ]¬IRat i (11)
L-theorems 10 and 11 highlight that the concepts of individualistic rationality and irrationality are positively and negatively introspective. The following theorem specifies some sufficient conditions for guaranteeing that the chosen strategy profile is a Nash equilibrium: if all agents are individualistically rational (alias self-interested) and every agent knows the choices of the other agents, then the selected strategy profile is a Nash equilibrium. For every δ ∈ ∆ we have: [START_REF] Dubois | Possibility theory: an approach to computerized processing of uncertainty[END_REF] L ( i∈Agt

(IRat i ∧ [B i ] δ -i ) ∧ δ ) → Nash(δ)
A similar theorem has been stated for the first time by Aumann & Brandeburger [START_REF] Aumann | Epistemic conditions for Nash equilibrium[END_REF][START_REF] Brandenburger | Knowledge and equilibrium in games[END_REF]. The only difference is that Aumann & Brandeburger used knowledge instead of belief.

An extension with group preferences

In this section we extend the logic L by operators of group preferences of the form

[≥ k C ]. We call L + the extended logic. Operators [≥ k C ] are just a generalization of the operators of individual preference of the form [≥ k i ].
In the present approach a preference for a group C is given by the intersection of the preferences of the agents in the group.

Syntax

The language of the logic L + is obtained by extending the language of the logic L by formulas [≥ k C ]ϕ where C ranges over 2 Agt * and k ranges over I. The formula [≥ k C ]ϕ has to be read "ϕ is true in all states which are good for group C at least to degree k". We define

≥ k C ϕ def = ¬[≥ k C ]¬ϕ. ≥ k
C ϕ has to be read "ϕ is true in at least one state which is good for group C at least to degree k".

Semantics

Definition 7 (L + -model). L + -models are tuples M = W, R, B, P, GP , π where:

• M = W, R, B, P, π is a L-model; • GP : I × 2 Agt * -→ 2 W
is a function mapping every integer k in I and coalition C to a (possibly empty) set of worlds GP k C such that:

C7 GP k C = i∈C P k i .
The function GP is used to specify the degree of goodness of a certain world according to a given group of agents. In particular, for every k ∈ I and C ∈ 2 Agt * , GP k C is the set of worlds that are good for group C at least to degree k.

Let us generalize the functions κ i à la Spohn and the preference orders i of Section 2.2 to groups. Definition 8 (κ C ). For every C ∈ 2 Agt * and for every w ∈ W we define:

• κ C (w) = n if and only if w ∈ GP n C ; • for every k ∈ I such that k < n, κ C (w) = k if and only if w ∈ GP k C and w ∈ GP k+1 C .
Definition 9 ( C ) . For every C ∈ 2 Agt * and for every w, v ∈ W we have

w C v if and only if κ C (w) ≤ κ C (v).
Definition 10 (Max C ) . For every C ∈ 2 Agt * we define Ma x C = ma x w∈W κ C (w).

The following propositions highlight some interesting aspect of the present notion of group preference.

Proposition 2. κ C (w) ≤ κ C (v) if and only if min C κ i (w) ≤ min i∈C κ i (v).
According to Proposition 2, for the group of agents C the degree of goodness of world v is higher than the degree of goodness of world w if and only if, the lowest degree of goodness of world v for an agent in the group C is higher than the lowest degree of goodness of world w for an agent in the group C.

Proposition 3. w ∈ Max C if and only if w ∈ max v∈W min i∈C κ i (v).
Proposition 3 is about a maximin principle for group preferences: the degree of goodness of world w for group C is maximal if and only if, w belongs to the set of worlds whose lowest degree of goodness for an agent in the group C is maximal. Note that since [START_REF] Rawls | A theory of Justice[END_REF], social procedures based on a maximin principle have been considered appropriate for ensuring fairness and justice. Consequently, we think that maximin is also a good method for defining the concept of group preference.

• W = {w 1 , w 2 , w 3 , w 4 }; • R {i 1 ,i 2 } (w 1 ) = i 1 :c, i 2 :c , R {i 1 ,i 2 } (w 2 ) = i 1 :d, i 2 :d , R {i 1 ,i 2 } (w 3 ) = i 1 :c, i 2 :d , R {i 1 ,i 2 } (w 4 ) = i 1 :d, i 2 :c ; • P 3 i 1 = {w 4 }, P 2 i 1 = {w 1 , w 4 }, P 1 i 1 = {w 1 , w 2 , w 4 }, P 0 i 1 = {w 1 , w 2 , w 3 , w 4 }; • P 3 i 2 = {w 3 }, P 2 i 2 = {w 1 , w 3 }, P 1 i 2 = {w 1 , w 2 , w 3 }, P 0 i 2 = {w 1 , w 2 , w 3 , w 4 }.
Consider now group preferences. We have:

• GP 2 {i 1 ,i 2 } = {w 1 }, GP 1 {i 1 ,i 2 } = {w 1 , w 2 }, GP 0 {i 1 ,i 2 } = {w 1 , w 2 , w 3 , w 4 }. Therefore, w 1 ∈ Max {i 1 ,i 2 } .
In other words, the state in which both i 1 and i 2 cooperate is the best state for the group {i 1 , i 2 }. Indeed, this is the state whose lowest degree of goodness for an agent in {i 1 , i 2 } is maximal.

Before concluding we have to provide the truth condition for

[≥ k C ]ϕ: M, w |= [≥ k C ]ϕ ⇐⇒ M, v |= ϕ for all v such that v ∈ GP k C .

Axiomatization

Every operator [≥ k C ] satisfies the principles of the basic modal logic K plus the following two additional principles:

[≥ k i ]ϕ ↔ [≥ k {i} ]ϕ (Def [≥ k i ] ) ≥ k C δ ↔ ( i∈C ≥ k i δ ) (GroupPref)
Note that Axiom GroupPref is the fundamental principle relating group preferences with individual preferences.

We call L + the logic axiomatized by the principles of the logic L given in Section 2.3 (Table 1) plus the axioms and the rules of inference of the basic system K for every operator [≥ k C ] and the previous two Axioms Def [≥ k i ] and GroupPref. Definitions of validity and theoremhood for the logic L + are just standard. We write |= L + ϕ if formula ϕ is valid in all L + -models. We write L + ϕ if formula ϕ is a theorem of L + .

The following Theorem 2 can be proved in a way similar to Theorem 1.

Theorem 2. The logic L + is sound and complete with respect to the class of L + -models.

The following are some properties of the operators of collective preference. For every B, C ∈ 2 Agt * such that B ⊆ C and for every k ∈ I we have:

L + [≥ k B ]ϕ → [≥ k C ]ϕ (13) L + [≥ 0 C ]ϕ ↔ ϕ (14) L + [≥ k-1 C ]ϕ → [≥ k C ]ϕ (15)

Strategic games with social rationality

In this section we explore strategic games in which agents are driven by other-regarding motives and social preferences. We consider two different kinds of social rationality: fairness and reciprocity.

Group preferences over formulas and fairness equilibrium

We can now generalize the notion of preference over formulas to groups. For every C ∈ 2 Agt * , we define ψ ≤ C ϕ ("ϕ is for group C at least as good as ψ") as follows:

ψ ≤ C ϕ def = k∈I ( ≥ k C ψ → ≥ k C ϕ).
As the following L + -theorems highlight the operators ≤ C are also total preorders. For every C ∈ 2 Agt * we have:

L + ψ ≤ C ψ (16) L + ((ϕ 1 ≤ C ϕ 2 ) ∧ (ϕ 2 ≤ C ϕ 3 )) → (ϕ 1 ≤ C ϕ 3 ) (17) L + (ϕ 1 ≤ C ϕ 2 ) ∨ (ϕ 2 ≤ C ϕ 1 ) (18) We define ψ < C ϕ = def ( ψ ≤ C ϕ) ∧ ¬ (ϕ ≤ C ψ ), δ ≤ C δ d ef = δ ≤ C δ and δ < C δ def = (δ ≤ C δ ) ∧ ¬(δ ≤ C δ).
The notion of best response of Section 3.2 can also be generalized to groups. We say that agent i's action a is for the group C a best response to the other agents' joint action δ -i , noted BR C (i:a,δ -i ), if and only if i cannot improve the utility of group C by deciding to do something different from a while the others choose the joint action δ -i , that is:

BR C (i:a,δ -i ) def = b∈Act (( i:b ∧ δ -i ) ≤ C ( i:a ∧ δ -i )).
Note that the notion of best response of Section 3.2 is just a special case of the previous definition, when C = {i}. In fact, BR {i} (i:a,δ -i ) is logically equivalent to BR(i:a,δ -i ).

Before concluding this section, we provide a notion of fairness equilibrium. Basically, fairness equilibrium is the collective counterpart of the individualistic notion of Nash equilibrium. Given a certain strategic game, the strategy profile (or joint action) δ is said to be a fairness equilibrium if and only if for every agent i ∈ Agt, i's action δ i is for the entire group Agt a best response to the other agents' joint action δ -i :

FairEq(δ) def = i∈Agt BR Agt (δ i ,δ -i ).
In other words, in a fairness equilibrium every agent chooses an action that, given what the others choose, maximizes the utility of the entire group of agents Agt.

Social rationality

It is time to look at social rationality. Differently from individualistically rational agents defined in Section 3.3, social rational agents also consider the benefits of their choice for the group. Moreover, their decisions can be affected by their beliefs about other agents' willingness to act for the well-being of the group.

We first define fairness. For every i ∈ Agt and C ∈ 2 Agt * such that i ∈ C:

Fair i,C def = a,b∈Act ( i:a → δ∈∆ ( B i δ -i ∧ ( δ -i , i:b ≤ C δ -i , i:a ))).
According to the previous definition, an agent i is fair with respect to his group C (noted Fair i,C ) if and only if, if he chooses action a then for every alternative action b, there exists a joint action δ -i of the other agents that he considers possible such that, playing a while the others play δ -i is for group C at least as good as playing b while the others play δ -i . Reciprocity can be defined from individualistic rationality and fairness. For every i ∈ Agt and C ∈ 2 Agt * such that i ∈ C: It has to be noted that the previous two notions of social rationality are also positively and negatively introspective. For every i ∈ Agt and C ∈ 2 Agt * we have:

Rec i,C def = ([B i ]( j∈C\{i} Fair j,C ) → Fair i,C ) ∧ (¬[B i ]( j∈C Fair j,C ) → IRat i ).
L + Fair i,C ↔ [B i ]Fair i,C (19) L + ¬Fair i,C ↔ [B i ]¬Fair i,C (20) L + Rec i,C ↔ [B i ]Rec i,C (21) L + ¬Rec i,C ↔ [B i ]¬Rec i,C (22)
The following L + -theorems specify some sufficient conditions for fairness equilibrium. For every δ ∈ ∆ we have:

L + ( i∈Agt (Fair i ∧ [B i ] δ -i ) ∧ δ ) → FairEq(δ) (23) L + ( i∈Agt (Rec i ∧ [B i ]( j =i Fair j ) ∧ [B i ] δ -i ) ∧ δ ) → FairEq(δ) (24) L + ( i∈Agt (Rec i ∧ ¬[B i ]( j =i Fair j ) ∧ [B i ] δ -i ) ∧ δ ) → Nash(δ) (25)
According to L + -theorem 23 if all agents are fair and every agent knows the choices of the other agents, then the selected strategy profile is a fairness equilibrium. According to L +theorem 24 if all agents are reciprocator, every agent believes that all other agents are fair, and every agent knows the choices of the other agents, then the selected strategy profile is a fairness equilibrium. According to L + -theorem 25 if all agents are reciprocator, every agent does not believe that all other agents are fair, and every agent knows the choices of the other agents, then the selected strategy profile is a Nash equilibrium.

Related works

As emphasized in the introduction, although social preferences and social rationality have been extensively studied in experimental economics, no logical analysis of these concepts has been proposed up to now. However, several logical systems exist which support reasoning about strategic games (see, e.g., [START_REF] Van Der Hoek | A logic for strategic reasoning[END_REF][START_REF] Troquard | A logic of games and propositional control[END_REF][START_REF] Lorini | A dynamic logic of agency II: deterministic DLA, Coalition Logic, and game theory[END_REF]) and epistemic strategic games (see, e.g., [START_REF] De Bruin | Explaining games: on the logic of game theoretic explanations[END_REF][START_REF] Roy | Thinking before acting: intentions, logic, rational choice[END_REF][START_REF] Bonanno | A syntactic approach to rationality in games with ordinal payoffs[END_REF][START_REF] Lorini | Epistemic Games in Modal Logic: Joint Actions, Knowledge and Preferences all together[END_REF]). Let us briefly discuss the latter.

De Bruin [START_REF] De Bruin | Explaining games: on the logic of game theoretic explanations[END_REF] has developed a very rich logical framework which enables to reason about the epistemic aspects of strategic games and of extensive games. His system deals with several game-theoretic concepts like the concepts of knowledge, rationality, Nash equilibrium, iterated strict dominance, backward induction. Nevertheless, de Bruin's approach differs from our logical approach to epistemic strategic games in several respects. First of all, our approach is minimalistic since it relies on few primitive concepts: joint action, belief, (individual and group) preference. All other notions such Nash equilibrium and (individual and social) rationality are defined by means of these three primitive concepts. On the contrary, in de Bruin's logic all those notions are atomic propositions managed by a ad hoc axiomatization (see, e.g., [10, pp. 61,65] where special propositions for rationality are introduced). Secondly, we provide a semantics and a complete axiomatics for our logic of epistemic games. De Bruin's approach is purely syntactic: no model-theoretic analysis of games is proposed nor completeness result for the proposed logic is given.

Roy [START_REF] Roy | Thinking before acting: intentions, logic, rational choice[END_REF] has recently proposed a modal logic integrating preference, knowledge and intention. In his approach every world in a model is associated to a nominal which directly refers to a strategy profile in a strategic g ame. This approach is however limited in expressing formally the structure of a strategic game. In particular, in Roy's logic there is no principle like the L Axiom Indep explaining how possible actions δ i of individual agents are combined to form a strategy profile δ of the current game. Another limitation of Roy's approach is that it does not enable to express the concept of individualistic rationality that we have been able to define in Section 3.3 (see [24, pp. 101]).

Bonanno [START_REF] Bonanno | A syntactic approach to rationality in games with ordinal payoffs[END_REF] integrates modal operators for belief, common belief with constructions expressing agents' preferences over individual actions and strategy profiles, and applies them to the semantic characterization of solution concepts like Iterated Deletion of Strictly Dominated Strategies (IDSDS). Although this logic enables to express the concept of individualistic rationality assumed in classical game theory, it is not sufficiently general to enable to express in the object language solution concepts like Nash equilibrium and IDSDS (note that the latter is defined by Bonanno only in the metalanguage).

Lorini et al. [START_REF] Lorini | Epistemic Games in Modal Logic: Joint Actions, Knowledge and Preferences all together[END_REF] have recently developed a modal logic of epistemic strategic games which overcomes the previous limitations. It enables to express in the object language solution concepts such as Nash equilibrium and IDSDS, and the concept of individualistic rationality. A complete axiomatization of this logic is given and its complexity is studied. However this logic does not have operators for group preference which support reasoning about different kinds of social rationality such as fairness and reciprocity.

Example 3 .

 3 REMARK. Note that the maximin principle also ensures Pareto optimality. In particular, if w ∈ Max C then w ∈ Pareto C , where Pareto C = {v|∀ u ∈ W, ∃i ∈ C: u i v}. Consider again the two-player Prisoner Dilemma (PD) game illustrated in the Example 1 of Section 2.2 with Agt = {i 1 , i 2 } and ACT = {c, d} where c is the action of cooperating and d is the action of defecting. The PD game just needs four different degrees of goodness I = {0, 1, 2, 3} and corresponds to the model M whose elements W, R, P are defined as follows:

Example 4 .

 4 In the Prisoner Dilemma there are two fairness equilibria: mutual cooperation and mutual defection. Hence, in the model illustrated in the Example 1 of Section 2.2 we have that formulas FairEq( i 1 :c, i 2 :c ) and FairEq( i 1 :d, i 2 :d ) are both true at each world w 1 , w 2 , w 3 , w 4 of the model M .

  2. It is well-known that in the Prisoner Dilemma the only Nash equilibrium is mutual defection. Hence, in the model illustrated in the Example 1 of Section 2.2 we have that formula Nash( i 1 :d, i 2 :d ) is true at each world w 1 , w 2 , w 3 , w 4 of the model M .

  That is, an agent i is a reciprocator with respect to his group C (noted Rec i,C ) if and only if, if he believes that the other agents in C \ {i} play fair then he plays fair, otherwise he plays egoistic. For notational convenience we write Fair i instead of Fair i,Agt and Rec i instead of Rec i,Agt .

These models adopt the concept of 'psychological game theory' introduced by[START_REF] Geanakoplos | Psychological games and sequential rationality[END_REF] and recently elaborated by[START_REF] Battigalli | Dynamic psychological games[END_REF]. In psychological game theory, utilities do not only depend on terminal-node payoffs but also on players' beliefs.

On this issue, see also[START_REF] Laverny | From knowledge-based programs to graded belief-based programs, part II: off-line reasoning[END_REF].

An additional result proved by the two authors is that Lewis's conditional logic is nothing more that the logic of qualitative possibility developed by Dubois & Prade[START_REF] Dubois | Possibility theory: an approach to computerized processing of uncertainty[END_REF]. On this see also[START_REF] Boutilier | Modal logics for qualitative possibility and beliefs[END_REF].

Note that this function exists, as Constraint C3 on L-models ensures that R Agt is a bijection.


Emiliano Lorini

A Logical Analysis of Commitment Dynamics

The aim of this work is to propose a model-theoretic semantics and a complete logic for the dynamics of commitments. In the first part of the article, a formalization of the concept of social commitment in STIT logic is presented. STIT is one of the most prominent formal accounts of agency. It is the logic of constructions of the form "agent i sees to it that ϕ". In the second part, the article presents an extension of STIT logic by dynamic operators which enable to describe two basic operations on commitment: commitment creation and commitment cancelation. The logic is used to develop an axiomatic and semantic analysis of commitment change in multi-agent systems.

Introduction

Social commitment is a fundamental concept for understanding normative relationships between individuals in a society. It has become a valuable abstraction for the design of multi-agent systems since it can be used to model a variety of interactive situations like contracts, agreements, negotiation, dialogue, and argumentation.

Although formal analysis of commitment are available in the literature (see, e.g., [START_REF] Verdicchio | A logical model of social commitment for agent communication[END_REF][START_REF] Singh | Semantical considerations on dialectical and practical commitments[END_REF][START_REF] Bentahar | A logical model for commitment and argument network for agent communication[END_REF]) and commitments have been extensively used for applications in the area of multi-agent systems (see, e.g., [START_REF] Desai | Checking correctness of business contracts via commitments[END_REF] for an application of commitment to business protocols), there is still no formal approach which provides at the same time a modeltheoretic semantics, and a sound and complete logic for the dynamics of commitments. I agree indeed with Singh [23, pp. 176] when he says that "...it was a sensible research strategy to first establish that commitments were a useful concept. However, now that the case for commitments has been made well, further progress is hampered by the lack of a clear model-theoretic semantics."

The aim of this article is to fill this existing gap in the literature on commitments by providing a model-theoretic semantics, and sound and complete logic for the dynamics of commitments. In order to formalize commitments STIT logic is used. STIT (the logic of Seeing to it That) is a logic of agency that has been developed in the 90ies in the domain of philosophy of action by Belnap, Horty and colleagues (see, e.g., [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]). It is the logic of constructions of the form "agent i sees to it that ϕ".

In this article STIT logic is extended by modal operators which enable to express what is true according to the regulation of a given institution. With STIT logic augmented with these modal operators, I define commitments in institutional contexts. In particular, I define the concept of 'agent i's commitment towards agent j in the context of institution x to ensure a certain state of affairs ϕ' by the fact that, according to the regulation of institution x, if agent i does not see to it that ϕ then then agent j will be wronged by i.

The rest of the article is organized as follows. In Section 2, the STIT-based logical framework for the analysis of commitments is introduced. A formalization of the concept of social commitment is given in Section 3. In Section 4 an extension of the logic of Section 2 by dynamic operators is presented. These dynamic operators enable to describe two basic operations on commitment: commitment creation and commitment cancelation. The proposed logic is used to develop an axiomatic and semantic analysis of commitment change in multi-agent systems.

A logic of actions and institutions

In order to be able to reason about actions of agents and about pragmatic commitments in institutional contexts, I introduce here STIT logic extended by modal operators which enable to express what is true according to the regulation of a given institution. STIT logic (the logic of Seeing to it That) [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] is one of the most prominent formal accounts of agency. It is the logic of constructions of the form "agent i sees to it that ϕ". STIT has a non-standard semantics based on the concepts of moment and history. However, as shown by Balbiani et al. [START_REF] Balbiani | Alternative axiomatics and complexity of deliberative STIT theories[END_REF], the basic STIT language without temporal operators axiomatized by Xu in [START_REF] Xu | Axioms for deliberative STIT[END_REF] and [START_REF] Belnap | Facing the future: agents and choices in our indeterminist world[END_REF]Chap. 17] can be 'simulated' in a standard Kripke semantics. Similarly to Balbiani et al., I use here a Kripke semantics for interpreting STIT modal operators.

Xu mainly focuses on Chellas's STIT operators named after his proponent [START_REF] Chellas | Time and modality in the logic of agency[END_REF]. As pointed out in [START_REF] Xu | Axioms for deliberative STIT[END_REF][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. Following Xu, I focus here on Chellas's STIT operators and I take them as primitive.

Syntax

Assume a countable set of atomic propositions denoting facts Atm = {p, q, . . .}, a finite set of agents Agt = {i 1 , . . . , i |Agt| } and a finite set of institutional contexts Inst = {x 1 , . . . , x |Inst| }. In order to be able to define social commitment in Section 3, let me add to the language special atoms as in the reduction of deontic logic to alethic logic [START_REF] Anderson | A reduction of deontic logic to alethic modal logic[END_REF]. In particular, let me introduce atoms of the form wr i,j,x in Lindhal's style [START_REF] Lindahl | Stig Kanger's theory of rights[END_REF] one for every i, j ∈ Agt such that i = j and x ∈ Inst. I call Wr the corresponding set, that is, Wr = {wr i,j,x |i, j ∈ Agt and i = j and x ∈ Inst}. In the semantics, special atoms wr i,j,x are used to identify those states in which, according to the regulation of a given institution x, an agent i wrongs (or gives offence to) another agent j. An atom wr i,j,x has to be read 'agent j is wronged by agent i in the context of institution x'. I denote Atm + = Atm ∪ Wr the extended set of propositional atoms. I write α, β, . . . the elements in Atm + .

The language L of the logic L is the set of formulas defined by the following BNF:

ϕ ::= α | ¬ϕ | ϕ ∧ ϕ | [i]ϕ | ϕ | D x ϕ
where α ranges over Atm + , i ranges over Agt and x ranges over Inst. The other Boolean constructions , ⊥, ∨, → and ↔ are defined from ¬ and ∧ in the standard way.

Operators [i] are Chellas's STIT operators. Formula [i]ϕ captures the fact that ϕ is guaranteed by a present choice 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 ϕ'. I define the dual of the operator [i] as follows: i ϕ def = ¬[i]¬ϕ. ϕ stands for 'ϕ is settled true regardless of what every agent does' or simply 'ϕ is settled true'. I define the dual of as follows: ♦ϕ def = ¬ ¬ϕ. 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 in [START_REF] Horty | The deliberative STIT: A study of action, omission, and obligation[END_REF]:

[i dstit: ϕ] def = [i]ϕ ∧ ¬ ϕ.
Finally, modal operators D x enable to describe what is true according to the regulation of a given institution. In particular, formula D x ϕ has the following reading 'ϕ is true, according to the regulation of the institution x' or more simply 'ϕ is true, according to the institution x'. For example, if the meaning of formula ϕ is that two persons are married and x denotes a certain State, formula D x ϕ means that, according to the regulation of this State, these persons are considered as two legally married persons. However, it may happen that with respect to the regulation of another State y they are not married. I define the dual of the operator D x as follows: D x ϕ def = ¬D x ¬ϕ. Formula D x ϕ has the following reading 'the regulation of the institution x admits a situation in which ϕ is true' or more simply 'the regulation of the institution x admits ϕ'.

This kind of modal operators were introduced for the first time by Jones & Sergot [START_REF] Jones | A formal characterization institutionalised power[END_REF]. Similar operators were recently studied by Grossi et al. [START_REF] Grossi | Classificatory aspects of counts-as: An analysis in modal logic[END_REF]. It has to be noted that Jones & Sergot's operators and Grossi et al.'s operators have slightly different properties. While the former satisfy the system KD and are interpreted by means of standard accessibility relations between worlds in a model, the latter are K45 operators which are interpreted by taking subsets of the set of worlds in a model. In this article, I adopt Jones & Sergot's solution by supposing that every D x is a KD operator and by interpreting it by means of standard accessibility relations (see Section 2.3 below).

Semantics

I use a standard possible worlds semantics. Possible worlds are understood as in the logics of knowledge and of belief.

Definition 1 (L-model). L-models are tuples M = W, R , {R i |i ∈ Agt}, {D x |x ∈ Inst}, V where:
-W is a nonempty set of possible worlds or states; -R is an equivalence relation between worlds in W ; for every i ∈ Agt, R i is an equivalence relations between worlds in W such that:

(C1) R i ⊆ R , ( C2
) for all w ∈ W , for all (w j ) j∈Agt ∈ R (w) n , j∈Agt R j (w j ) = ∅; for every x ∈ Inst, D x is a serial relation between worlds in W such that:

(C3) if (w, v) ∈ D x and (v, u) ∈ R then (w, u) ∈ D x ; -V : Atm + -→ 2 W is a valuation function.
For every w ∈ W , I write |w| = {α ∈ Atm + |w ∈ V(α)}.

As in the previous Constraint C2, accessibility relations on W can be viewed as functions from W to 2 W . Therefore, I write

R i (w) = {v|(w, v) ∈ R i }, R (w) = {v|(w, v) ∈ R } and D x (w) = {v|(w, v) ∈ D x }.
For every world w ∈ W and for every agent i ∈ Agt, R i (w) is the set of worlds that agent i brings about at world w or the set of outcomes of the action chosen by agent i at w. R i (w) can also be called the outcome state of agent i at world w. R is the relation over all possible outcomes. If v ∈ R (w) then v is a possible outcome at w. R (w) is therefore called the set of possible outcomes at world w. If v ∈ R (w), we can also say that v is a possible alternative of world w.

Thus, Constraint C1 in Definition 1 just means that all outcomes brought about by an agent i are possible outcomes. Constraint C2 expresses a so-called assumption of independence of agents: if w 1 , . . . , w n are possible outcomes at w then the intersection of the set of outcomes that agent 1 brings about at w 1 , and the set of outcomes that agent 2 brings about at w 2 ,..., and the set of outcomes that agent n brings about at w n is not empty. More intuitively, this means that agents can never be deprived of choices due to the choices made by other agents.

Just as in epistemic logic an information state of an agent i is the set of worlds that agent i considers possible, the set D x (w) is the regulation state of institution x at world w, that is, the set of worlds which are admitted by institution x's regulation at w. For example, suppose that x is a certain State and world v corresponds to the situation in which a couple {i 1 , i 2 } applies for a divorce in x, and i 1 and i 2 are x's citizens, that is, {citizens i1,i2,x , divorce i1,i2,x } ⊆ |v|. Then, v ∈ D x (w) just means that world v, in which a couple {i 1 , i 2 } applies for a divorce in x and i 1 and i 2 are x's citizens, is admitted by State x's regulation at w.

Hence, Constraint C3 in Definition 1 just means that: if v is in the regulation state of an institution x at a world w then, all possible alternatives of v are worlds which are in the regulation state of institution x at world w.

Given a model M , a world w and a formula ϕ, we write M, w |= ϕ to mean that ϕ is true at world w in M . The truth conditions of formulas are defined as follows:

-M, w |= α iff w ∈ V(α); -M, w |= ¬ϕ iff not M, w |= ϕ; -M, w |= ϕ ∧ ψ iff M, w |= ϕ and M, w |= ψ; -M, w |= ϕ iff M, v |= ϕ for all v such that v ∈ R (w); -M, w |= [i]ϕ iff M, v |= ϕ for all v such that v ∈ R i (w); -M, w |= D x ϕ iff M, v |= ϕ for all v such that v ∈ D x (w). I write |= L ϕ if ϕ is valid in L (ϕ is true in all L-models).

Axiomatization

KD(x)

All KD-principles for the operators Dx

( → i) ϕ → [i]ϕ (AIA k ) (♦[1]ϕ1 ∧ . . . ∧ ♦[k]ϕ k ) → ♦([1]ϕ1 ∧ . . . ∧ [k]ϕ k ) (x → x ) Dxϕ → Dx ϕ
Fig. 1. Axiomatization of L [START_REF] Xu | Axioms for deliberative STIT[END_REF]. According to Axiom ( → i), if ϕ is settled true then every agent sees to it that ϕ.

In other words, an agent brings about those facts that are inevitable. (AIA k ) is a family of axiom schemes for independence of agents that is parameterized by the integer k. As noted in [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, the family of axiom schemas can be replaced by the single (AIA |Agt| ). Finally, Axiom (x → x ) relates the modal operator with the institution operators D x . It says that if ϕ holds according to the institution x then, according to the institution x, ϕ is settled true. I call L the logic axiomatized by the principles given in Fig. 1.

I write L ϕ if ϕ is a L-theorem.
Theorem 1. The logic L is completely axiomatized by the principles in Fig. 1.

Proof. It is a routine task to check that the axioms of the logic L correspond one-to-one to their semantic counterparts on the models. In particular, S5( ) and S5(i) correspond to the fact that R and every R i are equivalence relations, while KD(x) corresponds to the seriality of every D x . Axiom ( → i) corresponds to the Constraint C1 in Definition 1, while Axiom (x → x ) corresponds to the Constraint C3. Finally, as noted in Section 2.3, since Agt is finite, the family of axiom schemas (AIA k ) can be replaced by the single (AIA |Agt| ). The latter corresponds to the Constraint C2 in Definition 1.

It is routine, too, to check that all axioms of the logic L are in the Sahlqvist class. This means that the axioms are all expressible as first-order conditions on models and that they are complete with respect to the defined model classes, cf. [7, Th. 2.42].

Commitments in institutional contexts: a formalization

According to [START_REF] Singh | An ontology for commitments in multiagent systems[END_REF][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 in a given context. The contexts in which commitments 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 takes a pragmatic commitment towards j. On the contrary, if i tells to j: "Tomorrow, will be sunny. I am sure!" then, he takes a propositional commitment towards j.

In order to define the concept of social commitment, I use the special atoms wr i,j,x denoting that 'an agent j is wronged by another agent i in the context of institution x'. I say that agent i is committed to agent j in the context of institution x to ensure ϕ (noted C i:j:x ϕ) if and only if, according to the institution x if i does not see to it that ϕ then j will be wronged by i in x, and the institution x admits a situation in which i does not see to it that ϕ. For every i, j ∈ Agt and x ∈ Inst I define:

C i:j:x ϕ def = D x (¬[i]ϕ → wr i,j,x ) ∧ D x ¬[i]ϕ.
The component D x ¬[i]ϕ expresses that i is committed to j in the context of institution x to ensure ϕ, only if the situation in which i does not see to it that ϕ (and j is therefore wronged by j) is compatible with the institution x's regulation. It has also to be noted that a commitment of agent i to agent j to ensure ϕ in the context of institution x can be conceived as a kind of directed obligation from a bearer to a counterparty in a given institutional context (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] for some analysis of the notion of directed obligation in deontic logic). 1Example 1. Agent i 2 is the program chair of a given conference. Agent i 2 asks agent i 1 , a member of the program committee, to review some articles submitted to the conference. Agent i 1 accepts agent's i 2 request by sending a confirmation e-mail (we suppose that the communication between i 1 and i 2 is made through the Easychair system). Consequently, according to the program committee of the conference, agent i 1 is committed to i 2 to review the articles: C i1:i2:PC review . This means that, according to the program committee, if i 1 does not review the articles then i 2 will be wronged by i 1 . Moreover, the program committee admits a situation in which i 1 does not accomplish his duty to review the articles:

D PC (¬[i 1 ]review → wr i1,i2,PC ) ∧ D PC ¬[i 1 ]review .
Let me generalize the previous definition to conditional commitments. I say that agent i is committed to agent j in the context of institution x to ensure ϕ under condition ψ (noted C i:j:x (ψ,ϕ)) if and only if, according to the institution x, if i does not see to it that ϕ and ψ is true then j will be wronged by i, and the institution x admits a situation in which ψ is true and agent i does not see to it that ϕ. For every i, j ∈ Agt and x ∈ Inst I define:

C i:j:x (ψ,ϕ) def = D x ((ψ ∧ ¬[i]ϕ) → wr i,j,x ) ∧ D x (ψ ∧ ¬[i]ϕ).
Again the formula D x (ψ ∧ ¬[i]ϕ) expresses that i is committed to j in the context of institution x to ensure ϕ under condition ψ, only if the situation in which ψ is true and i does not see to it that ϕ is compatible with the institution x's regulation. Note also that D x ¬ψ implies ¬C i:j:x (ψ,ϕ) for every formula ϕ and for every couple of agents i and j. That is, if the institution x does not admit a situation in which ψ is true then, for every formula ϕ and for every couple of agents i and j, there is no commitment of i towards j in the context of institution x to ensure ϕ under condition ψ.

Example 2. Agent i 1 and agent i 2 have concluded a contract in front of a notary of a certain State x. Agent i 1 has declared in front of the notary that he will sell to i 2 a certain property if i 2 will pay him 10K Euros. Consequently, according to the State x, i 1 is conditionally committed to i 2 to sell to i 2 the property under the condition that i 2 pays him 10K Euros:

C i1:i2:x ([i 2 ]pay10K i1 ,sellProperty i2
). This means that, according to the State x, if i 1 does not sell to i 2 the property when i 2 pays him 10K Euros then i 2 will be wronged by i 2 , and the State x admits a situation in which i 1 does not sell to i 2 the property while i 2 pays him 10K Euros:

D x (([i 2 ]pay10K i1 ∧ ¬[i 1 ]sellProperty i2 ) → wr i1,i2,x )∧ D x ([i 2 ]pay10K i1 ∧ ¬[i 1 ]sellProperty i2 ).
As the following L-theorem highlights in the present approach unconditional commitments are special cases of conditional commitments where the antecedent is true:

(1) L C i:j:x ϕ ↔ C i:j:x ( ,ϕ).
It is also interesting to note that the previous definition satisfies some intuitive properties of conditional commitments. For every i, j ∈ Agt and for every x ∈ Inst we have:

L D x ϕ → ¬C i:j:x (ψ,ϕ) (2) L (C i:j:x (ψ,ϕ) ∧ D x ψ) → C i:j:x ϕ (3) L (C i:j:x (ψ,ϕ) ∧ C i:j:x (χ,ϕ)) → C i:j:x (ψ ∨ χ,ϕ) (4) L (C i:j:x (ψ,ϕ) ∧ C i:j:x (ψ,χ)) → C i:j:x (ψ,ϕ ∧ χ) (5) L (C i:j:x (ψ,ϕ ∧ χ) ∧ D x χ) → C i:j:x (ψ,ϕ) (6)
Proof. We prove L-theorem 5 as an example.

1. L (C i:j:x (ψ,ϕ) ∧ C i:j:x (ψ,χ)) ↔ (D x ((ψ ∧ ¬[i]ϕ) → wr i,j,x ) ∧ D x ((ψ ∧ ¬[i]χ) → wr i,j,x )) 2. L (D x ((ψ ∧ ¬[i]ϕ) → wr i,j,x ) ∧ D x ((ψ ∧ ¬[i]χ) → wr i,j,x )) → D x ((ψ ∧ (¬[i]ϕ ∨ ¬[i]χ)) → wr i,j,x ) by standard modal principles for D x 3. L D x ((ψ ∧ (¬[i]ϕ ∨ ¬[i]χ)) → wr i,j,x ) → D x ((ψ ∧ ¬[i](ϕ ∧ χ)) → wr i,j,x )
by standard modal principles for [i] and D x , and necessitation for

D x 4. L (C i:j:x (ψ,ϕ) ∧ C i:j:x (ψ,χ)) → ( D x (ψ ∧ i ¬ϕ) ∧ D x (ψ ∧ i ¬χ)) 5. L ( D x (ψ ∧ i ¬ϕ) ∧ D x (ψ ∧ i ¬χ)) → D x (ψ ∧ i (¬ϕ ∨ ¬χ))
by standard modal principles for [i] and

D x 6. L D x (ψ ∧ i (¬ϕ ∨ ¬χ)) → D x (ψ ∧ ¬[i](ϕ ∧ χ)) 7. L (C i:j:x (ψ,ϕ) ∧ C i:j:x (ψ,χ)) → (D x ((ψ ∧ ¬[i](ϕ ∧ χ)) → wr i,j,x ) ∧ D x (ψ ∧ ¬[i](ϕ ∧ χ))) from 1-3 and 4-6 8. L (C i:j:x (ψ,ϕ) ∧ C i:j:x (ψ,χ)) → C i:j:x (ψ,ϕ ∧ χ) from 7
L-theorem 2 is a discharge principle for commitment: if according to institution x ϕ is true, then i's commitment towards j in x to ensure ϕ is discharged and is no longer active. In the logic L D x ϕ is equivalent to D x [i]ϕ (by Axiom (x → x ) and Axiom T for [i]). Therefore, L-theorem 2 can be written in the following equivalent form: D x [i]ϕ → ¬C i:j:x (ψ,ϕ). Note also that L-theorem 2 and the L-theorem D x together imply ¬C i:j:x (ψ, ): an agent i cannot be committed to bring about tautologies.

L-theorem 3 is a detachment principle: if i is conditionally committed to j in x to ensure ϕ if ψ holds and, according to institution x, ψ holds then, an unconditional commitment of i to j in x to ensure ϕ comes into being. A similar detachment principle for conditional obligations has been discussed by Bartha [4].

L-theorems 4 and 5 are respectively a disjunction of the antecedents principle and a conjunction of the consequents principle for commitment. Similar properties have been isolated in [START_REF] Singh | Semantical considerations on dialectical and practical commitments[END_REF]. According to L-theorem 4, if i is committed to j in x to ensure ϕ if ψ holds and to ensure ϕ if χ holds then, i is committed to j in x to ensure ϕ if ψ ∨ χ holds. According to L-theorem 5, if i is committed to j in x to ensure ϕ if ψ holds and to ensure χ if ψ holds then, i is committed to j in x to ensure ϕ ∧ χ if ψ holds.

L-theorem 6 is a weakening principle for commitment: if agent i is committed to agent j in x to ensure ϕ ∧ χ if ψ holds and, according to the institution x, χ is true, then i is committed to j to ensure ϕ if ψ holds. So, if an agent is committed to ensure two states of affairs ϕ and χ and his commitment to ensure χ is discharged, then the agent is committed to ensure ϕ. Note indeed that, as highlighted by L-theorem 2, D x χ is the discharge condition for the commitment C i:j:x (ψ,χ).

Before concluding, let me consider how the previous definition of commitment behaves in the case of Moore-like sentences of the form ϕ ∧ ¬[i]ϕ. The following Ltheorem 7 clarifies this point: an agent is committed to ensure that ϕ is true and that he does not see to it that ϕ if and only if, the agent is committed to do something inconsistent. [START_REF] Blackburn | Modal Logic[END_REF] L C i:j:x (ϕ ∧ ¬[i]ϕ) ↔ C i:j:x ⊥.

4 From static to dynamic commitments I here extend the logic L of Section 1 by dynamic operators which enable to describe the dynamics of social commitments. I call L dyn the extended logic. I consider two basic operations on commitment: commitment creation and commitment cancelation. These two kinds of operations have also been studied in [START_REF] Singh | An ontology for commitments in multiagent systems[END_REF] and [START_REF] Verdicchio | A logical model of social commitment for agent communication[END_REF] in which commitments are operationalized as being in a certain number of states and operations of commitment creation and commitment cancelation are responsible for changing the state of a commitment from passive to active and viceversa. The main contribution of this section is to provide a comprehensive logical approach to the dynamics of commitments and, in particular, a model-theoretic semantics and a complete modal logic for commitment dynamics.

Operations of commitment creation are of the form i:j:x+(ψ, ϕ), operations of commitment cancelation are of the form i:j:x-(ψ, ϕ). In particular, i:j:x+(ψ, ϕ) is the event 'the commitment of agent i towards agent j to ensure ϕ if ψ holds is created in the institution x' whereas i:j:x-(ψ, ϕ) is the event 'the commitment of agent i towards agent j to ensure ϕ if ψ holds is canceled from the institution x'.

Commitment creation

The first extension of the logic L is by formulas [i:j:x+(ψ, ϕ)]χ where i, j ranges over Agt and x ranges over Inst. Formula [i:j:x+(ψ, ϕ)]χ describes the effects of the creation in institution x of i's commitment towards j to ensure ϕ if ψ holds. More precisely, [i:j:x+(ψ, ϕ)]χ has to be read 'χ holds, after the creation in the institution x of agent i's commitment towards agent j to ensure ϕ if ψ holds'.

Semantics In order to give semantics to the operators [i:j:x+(ψ, ϕ)] I need to define the model M i:j:x+(ψ,ϕ) which results from the occurrence of the event i:j:x+(ψ, ϕ) in the model M . The elements of the model M i:j:x+(ψ,ϕ) are defined as follows:

Definition 2 (Updated model M i:j:x+(ψ,ϕ) ). For every L-model M , M i:j:x+(ψ,ϕ) is the corresponding updated model with:

W i:j:x+(ψ,ϕ) ={wx|w ∈ W } ∪ {w∼x|w ∈ W }; D i:j:x+(ψ,ϕ) x ={(wx, vx)|(w, v) ∈ Dx} ∪ {(w∼x, v∼x)|(w, v) ∈ Dx}; If y = x then, D i:j:x+(ψ,ϕ) y ={(wx, v∼x)|(w, v) ∈ Dy} ∪ {(w∼x, v∼x)|(w, v) ∈ Dy}; R i:j:x+(ψ,ϕ) ={(wx, vx)|(w, v) ∈ R } ∪ {(w∼x, v∼x)|(w, v) ∈ R };
For z ∈ Agt, R i:j:x+(ψ,ϕ) z ={(wx, vx)|(w, v) ∈ Rz} ∪ {(w∼x, v∼x)|(w, v) ∈ Rz};

V i:j:x+(ψ,ϕ) (wri,j,x) ={wx|M, w |= wri,j,x ∨ (ψ ∧ ¬[i]ϕ)}∪ {w∼x|M, w |= wri,j,x};

For α = wri,j,x, V i:j:x+(ψ,ϕ) (α) ={wx|M, w |= α} ∪ {w∼x|M, w |= α}.

M i:j:x+(ψ,ϕ) is obtained by creating two copies of each world w of the original model M : a copy w x for the regulation state of institution x, also called 'x-copy' of world w; a copy w ∼x for the regulation states of every institution y different from x, also called '∼x-copy' of world w. World w x is the copy of w which is affected by the occurrence of the normative event i:j:x+(ψ, ϕ), whereas w ∼x is the copy of w in which nothing changes. In particular, in w x the truth value of the atom wr i,j,x ('agent j is wronged by agent i in x') is set to true if and only if, wr i,j,x is already true at w, or at w ψ is true and i does not see to it that ϕ (i.e. ψ ∧ ¬[i]ϕ). Moreover, for every copy w x and for every copy w ∼x :

the regulation state of institution x at w x are the 'x-copies' of worlds that were in the regulation state of x at w before the event i:j:x+(ψ, ϕ); the regulation state of every institution y different from x at w x are the '∼x-copies' of worlds that were in the regulation state of y at w before the event i:j:x+(ψ, ϕ); the regulation state of every institution y at w ∼x are the '∼x-copies' of worlds that were in the regulation state of y at w before the event i:j:x+(ψ, ϕ);

the outcome state of every agent i (resp. the set of possible states) at w x are the 'x-copies' of worlds that were in the outcome state of i (resp. in the set of possible states) at w before the event i:j:x+(ψ, ϕ); the outcome state of every agent i (resp. the set of possible states) at w ∼x are the '∼x-copies' of worlds that were in the outcome state of i (resp. in the set of possible states) at w before the event i:j:x+(ψ, ϕ).

As the following proposition highlights the operation of commitment creation is well-defined.

Proposition 1. If M is a L-model then M i:j:x+(ψ,ϕ) is a L-model.
Proof. It is just straightforward to show that R i:j:x+(ψ,ϕ) and every R i:j:x+(ψ,ϕ) z

(with z ∈ Agt) are equivalence relations, and that every D i:j:x+(ψ,ϕ) x (with x ∈ Inst) is a serial relation. It is also a routine to check that the operation i:j:x+(ψ, ϕ) preserves Constraints C1 and C2 in Definition 1.

Let me prove that the operation i:j:x+(ψ, ϕ) also preserves Constraint C3. Suppose that (w x , v x ) ∈ D i:j:x+(ψ,ϕ) x and (v x , u x ) ∈ R i:j:x+(ψ,ϕ) . Then, we have (w, v) ∈ D x and (v, u) ∈ R . By Constraint C3 on L-models, it follows that (w, u) ∈ D x . Consequently, we have (w x , u x ) ∈ D i:j:x+(ψ,ϕ) x

. In a similar way we can prove that if (w ∼x , v ∼x ) ∈ D Thus, at world w of model M it is the case that χ holds, after the creation in the institution x of i's commitment towards j to ensure ϕ if ψ holds if and only if, χ holds at the x-copy w x of world w in the updated model M i:j:x+(ψ,ϕ) .

Example 3. Fig. 2 illustrates by means of an example the semantics of the operation of commitment creation. Formulas C 1:2:x q and C 1:2:y q are true at world w in the initial model (at w agent 1 is committed to agent 2 to ensure q both in the context of institution x and in the context of institution y), whereas formulas C 1:2:x p and C 1:2:y p are both false at w (at w 1 is not committed to agent 2 to ensure p). The operation 1:2:x+( , p) results in an updated model in which 1 becomes committed to 2 in x to ensure p and in which 1 remains committed to 2 in x to ensure q. On the contrary, 1's commitments towards 2 in the context of institution y do not change. Indeed, C 1:2:x p, C 1:2:x q and C 1:2:y q are true at world w x in the updated model, whereas C 1:2:y p is false at w x .

Note that the updated model is nothing else than the duplication of the initial model. The left copy is the 'x-copy' which is affected by the event 1:2:x+( , p), whereas the right copy is the '∼x-copy' in which nothing changes.

w p,q 1 : 2 : x + ( T , p ) R 1 R 2 R 1 R 1 R 1 R 2 R 2 R 2 p,q p,q p q q q p,q p,q w r 1 , 2 , x w r 1 , 2 , x D x D y w x p,q p,q R 1 R 2 R 1 R 1 R 1 R 2 R 2 R 2 p,q p,q p q q q p,q p,q R 1 R 2 R 1 R 1 R 1 R 2 R 2 R 2
p,q p,q p q q q p,q p,q Axiomatization The following lemma is fundamental in order to prove Theorem 2 below and can be easily proved by induction on the structure of χ.

Lemma 1. Take a L-model M . Then, for every w ∼x ∈ W i:j:x+(ψ,ϕ) , we have:

M i:j:x+(ψ,ϕ) , w ∼x |= χ iff M, w |= χ.
As the following theorem highlights, there are reduction axioms for the operators [i:j:x+(ψ, ϕ)]. They are called reduction axioms because, read from left to right, they reduce the complexity of those operators in a formula.

Theorem 2. The following equivalences are valid:

R1. [i:j:x+(ψ, ϕ)]wr i,j,x ↔ (wr i,j,x ∨ (ψ ∧ ¬[i]ϕ)) R2. [i:j:x+(ψ, ϕ)]α ↔ α if α = wr i,j,x R3. [i:j:x+(ψ, ϕ)]¬χ ↔ ¬[i:j:x+(ψ, ϕ)]χ R4. [i:j:x+(ψ, ϕ)](χ 1 ∧ χ 2 ) ↔ ([i:j:x+(ψ, ϕ)]χ 1 ∧ [i:j:x+(ψ, ϕ)]χ 2 ) R5. [i:j:x+(ψ, ϕ)]D x χ ↔ D x [i:j:x+(ψ, ϕ)]χ R6. [i:j:x+(ψ, ϕ)]D y χ ↔ D y χ if y = x R7. [i:j:x+(ψ, ϕ)][i]χ ↔ [i][i:j:x+(ψ, ϕ)]χ R8. [i:j:x+(ψ, ϕ)] χ ↔ [i:j:x+(ψ, ϕ)]χ Proof. We just prove R5 and R6 as examples. (R5) M, w |= [i:j:x+(ψ, ϕ)]D x χ, ⇔ M i:j:x+(ψ,ϕ) , w x |= D x χ, ⇔ for all v x ∈ D x (w x ), M i:j:x+(ψ,ϕ) , v x |= χ, ⇔ for all v ∈ D x (w), M, v |= [i:j:x+(ψ, ϕ)]χ, ⇔ M, w |= D x [i:j:x+(ψ, ϕ)]χ. (R6) Suppose y = x. Then: M, w |= [i:j:x+(ψ, ϕ)]D y χ, ⇔ M i:j:x+(ψ,ϕ) , w x |= D y χ, ⇔ for all v ∼x ∈ D x (w x ), M i:j:x+(ψ,ϕ) , v ∼x |= χ, ⇔ for all v ∈ D x (w), M, v |= χ (by Lemma 1), ⇔ M, w |= D x χ.

Some properties

The following are examples of valid properties of commitment creation, with i, j, h, k ∈ Agt, p, q ∈ Atm, and x, y ∈ Inst:

D x (q ∧ ¬[i]p) ↔ [i:j:x+(q, p)]C i:j:x (q,p) (8) C h:k:x (q,p) → [i:j:x+(ψ, ϕ)]C h:k:x (q,p) (9) ¬C h:k:x (q,p) → [i:j:x+(ψ, ϕ)]¬C h:k:x (q,p) if h = i or k = j (10) C h:k:y (γ,χ) → [i:j:x+(ψ, ϕ)]C h:k:y (γ,χ) if y = x (11) ¬C h:k:y (γ,χ) → [i:j:x+(ψ, ϕ)]¬C h:k:y (γ,χ) if y = x (12)
Proof. We prove L dyn -theorem 8 as an example by applying the reduction axioms of Theorem 2 together with the rule of replacement of proved equivalence.

[i:j:x+(q, p)]C i:j:x (q,p) ⇔ [i:j:x+(q, p)]D x ((q ∧ ¬[i]p) → wr i,j,x )∧ [i:j:x+(q, p)]¬D x (q → [i]p) (by R4), ⇔ D x [i:j:x+(q, p)]((q ∧ ¬[i]p) → wr i,j,x )∧ ¬D x [i:j:x+(q, p)](q

→ [i]p) (by R3), ⇔ D x [i:j:x+(q, p)]((q ∧ ¬[i]p) → wr i,j,x )∧ ¬D x ¬[i:j:x+(q, p)](q ∧ ¬[i]p) (by R3), ⇔ D x [i:j:x+(q, p)]((q ∧ ¬[i]p) → wr i,j,x )∧ ¬D x ¬([i:j:x+(q, p)]q ∧ [i:j:x+(q, p)]¬[i]p) (by R4), ⇔ D x [i:j:x+(q, p)]((q ∧ ¬[i]p) → wr i,j,x )∧ ¬D x ¬(q ∧ ¬[i:j:x+(q, p)][i]p) (by R2 and R3), ⇔ D x [i:j:x+(q, p)]((q ∧ ¬[i]p) → wr i,j,x )∧ ¬D x ¬(q ∧ ¬[i][i:j:x+(q, p)]p) (by R7), ⇔ D x [i:j:x+(q, p)]((q ∧ ¬[i]p) → wr i,j,x )∧ ¬D x ¬(q ∧ ¬[i]p) (by R2), ⇔ D x [i:j:x+(q, p)]((q ∧ ¬[i]p) → wr i,j,x )∧ ¬D x (q → [i]p), ⇔ D x ¬[i:j:x+(q, p)]((q ∧ ¬[i]p) ∧ ¬wr i,j,x )∧ ¬D x (q → [i]p) (by R3), ⇔ D x ¬([i:j:x+(q, p)](q ∧ ¬[i]p) ∧ [i:j:x+(q, p)]¬wr i,j,x )∧ ¬D x (q → [i]p) (by R4), ⇔ D x ([i:j:x+(q, p)](q → [i]p) ∨ [i:j:x+(q, p)]wr i,j,x )∧ ¬D x (q → [i]p)
(by R3 and the valid equivalence [i:j:x+(q, p)]ϕ ↔ ¬[i:j:x+(q, p)]¬ϕ), ⇔ D x ([i:j:x+(q, p)](q

→ [i]p) ∨ wr i,j,x ∨ (q ∧ ¬[i]p))∧ ¬D x (q → [i]p) (by R7), ⇔ D x ((q → [i]p) ∨ wr i,j,x ∨ (q ∧ ¬[i]p))∧ ¬D x (q → [i]p) (by R2, R3, R4, R7), ⇔ D x ∧ ¬D x (q → [i]p), ⇔ ¬D x (q → [i]p), ⇔ D x (q ∧ ¬[i]p).
L dyn -theorem 8 highlights that the operator of commitment creation is well-defined since it captures the desired commitment dynamics. Suppose p and q are propositional atoms in Atm. If the institution x admits a situation in which q is true and agent i does not see to it that p then, after the creation in x of i's commitment towards j to ensure p if q holds, i will be committed to j in x to ensure p if q holds, and viceversa.

According to theorem 9, the operation of creating a commitment in a given institution x does not cancel pre-existing commitments about propositions in the same institution. In other words, the operation of commitment creation is conservative. Note that this property is due to the fact that in the model resulting from the operation of commitment creation, if wr i,j,x is true at world w in the original model then wr i,j,x is set to true at w x in the updated model. Consequently, the set of worlds in the 'x-copy' of the original model in which wr i,j,x is true is larger than the set of worlds in the original model in which wr i,j,x is true. According to theorem 10, the operation of creating a new commitment about propositions from a debtor i to a creditor j in a given institution x does not create additional commitments in the same institution from a debtor h to a creditor k, if either h and i are different debtors or k and j are different creditors. Finally, theorems 11 and 12 highlight some locality aspects of commitment creation, where locality means that the process of creating a commitment in an institution x does not change the commitments in an institution different from x.

REMARK. Note that the following formula is also valid in the logic L dyn for every p, q ∈ Atm:

[i:j:x+(q, p)] (¬[i](q → [i]p) → wr i,j,x ). This means, after the creation in institution x of agent i's commitment towards agent j to ensure p if q holds, it is settled that, if i does not see to it that if ψ then he sees to it that ϕ, then j will be wronged by i in x. In other words, the normative consequences of an operation of commitment creation are necessarily true facts.

Commitment cancelation

The second extension of the logic L is by formulas [i:j:x-(ψ, ϕ)]χ, where i, j ranges over Agt and x ranges over Inst. Formula [i:j:x-(ψ, ϕ)]χ has to be read 'χ holds, after the cancelation from the institution x of agent i's commitment towards agent j to ensure ϕ if ψ holds'.

Semantics In order to give semantics to the operators [i:j:x-(ψ, ϕ)] let me define the model M i:j:x-(ψ,ϕ) which results from the cancelation from the institution x of i's commitment towards j to ensure ϕ if ψ holds.

Definition 3 (Updated model M i:j:x-(ψ,ϕ) ). For every L-model M , M i:j:x-(ψ,ϕ) is the corresponding updated model with:

W i:j:x-(ψ,ϕ) ={wx|w ∈ W } ∪ {w∼x|w ∈ W }; D i:j:x-(ψ,ϕ) x ={(wx, vx)|(w, v) ∈ Dx} ∪ {(w∼x, v∼x)|(w, v) ∈ Dx}; If y = x then, D i:j:x-(ψ,ϕ) y ={(wx, v∼x)|(w, v) ∈ Dy} ∪ {(w∼x, v∼x)|(w, v) ∈ Dy}; R i:j:x-(ψ,ϕ) ={(wx, vx)|(w, v) ∈ R } ∪ {(w∼x, v∼x)|(w, v) ∈ R }; For z ∈ Agt, R i:j:x-(ψ,ϕ) z ={(wx, vx)|(w, v) ∈ Rz} ∪ {(w∼x, v∼x)|(w, v) ∈ Rz}; V i:j:x-(ψ,ϕ) (wri,j,x) ={wx|M, w |= wri,j,x ∧ (ψ → [i]ϕ)}∪
{w∼x|M, w |= wri,j,x};

For α = wri,j,x, V i:j:x-(ψ,ϕ) (α) ={wx|M, w |= α} ∪ {w∼x|M, w |= α}.

M i:j:x-(ψ,ϕ) is also obtained by creating two copies of each world w of the original model M . Again, world w x (the 'x-copy') is the copy of w which is affected by the occurrence of the event i:j:x-(ψ, ϕ), whereas w ∼x (the '∼ x-copy') is the copy in which nothing happens. In particular, in w x the truth value of the atom wr i,j,x is set to true if and only if, at w wr i,j,x is true and if ψ is true then i sees to it that ϕ (i.e. ψ → [i]ϕ). For the rest, model M i:j:x-(ψ,ϕ) has the same structure as the model M i:j:x+(ψ,ϕ) defined in Section 4.1.

Proposition 2. If M is a L-model then M i:j:x-(ψ,ϕ) is a L-model.

The truth condition of [i:j:x-(ψ, ϕ)]χ is the following:

M, w |= [i:j:x-(ψ, ϕ)]χ iff M i:j:x-(ψ,ϕ) , w x |= χ.
Axiomatization The following Lemma 2 is symmetrical to Lemma 1 for commitment creation and is used to prove Theorem 3 below.

Lemma 2. Take a L-model M . Then, for every w ∼x ∈ W i:j:x-(ψ,ϕ) , we have:

M i:j:x-(ψ,ϕ) , w ∼x |= χ iff M, w |= χ.
There are reduction axioms for commitment cancelation which are symmetrical to the reduction axioms for commitment creation.

Theorem 3. The following equivalences are valid:

T1. [i:j:x-(ψ, ϕ)]wr i,j,x ↔ (wr i,j,x ∧ (ψ

→ [i]ϕ)) T2. [i:j:x-(ψ, ϕ)]α ↔ α if α = wr i,j,x T3. [i:j:x-(ψ, ϕ)]¬χ ↔ ¬[i:j:x-(ψ, ϕ)]χ T4. [i:j:x-(ψ, ϕ)](χ 1 ∧ χ 2 ) ↔ ([i:j:x-(ψ, ϕ)]χ 1 ∧ [i:j:x-(ψ, ϕ)]χ 2 ) T5. [i:j:x-(ψ, ϕ)]D x χ ↔ D x [i:j:x-(ψ, ϕ)]χ T6. [i:j:x-(ψ, ϕ)]D y χ ↔ D y χ if y = x T7. [i:j:x-(ψ, ϕ)][i]χ ↔ [i][i:j:x-(ψ, ϕ)]χ T8. [i:j:x-(ψ, ϕ)] χ ↔ [i:j:x-(ψ, ϕ)]χ

Some properties

The following are examples of valid properties of commitment cancelation, with i, j, h, k ∈ Agt, p, q ∈ Atm, and x, y ∈ Inst:

[i:j:x-(q, p)]¬C i:j:x (q,p) (13)

¬C h:k:x (q,p) → [i:j:x-(ψ, ϕ)]¬C h:k:x (q,p) (14) C h:k:x (q,p) → [i:j:x-(ψ, ϕ)]C h:k:x (q,p) if h = i or k = j (15) C h:k:y (γ,χ) → [i:j:x-(ψ, ϕ)]C h:k:y (γ,χ) if y = x (16) ¬C h:k:y (γ,χ) → [i:j:x-(ψ, ϕ)]¬C h:k:y (γ,χ) if y = x (17)
L dyn -theorem 13 highlights that the operators of commitment cancelation are also welldefined. Suppose p and q are propositional atoms in Atm. Then, after the cancelation from institution x of i's commitment towards j to ensure p if q holds, i will not be committed to j in x to ensure p if q holds. According to theorem 14, the operation of canceling a commitment from a given institution x does not create new commitments about propositions in the same institution. Note that this property is due to the fact that in the model resulting from the operation of commitment cancelation, the atom wr i,j,x is set to true at a world w x only if wr i,j,x was already true at w in the original model. Consequently, the set of worlds in the 'x-copy' of the original model in which wr i,j,x is true is smaller than the set of worlds in the original model in which wr i,j,x is true. According to theorem 15, the operation of canceling a commitment about propositions from a debtor i to a creditor j in a given institution x does not cancel a pre-existent commitment in the same institution from a debtor h to a creditor k, if either h and i are different debtors or k and j are different creditors. Similarly to commitment creation, theorems 16 and 17 highlight some locality aspects of commitment cancelation, where locality means that the process of canceling a commitment from an institution x does not change the commitments in an institution different from x.

Completeness

I call L dyn the logic axiomatized by the principles of the logic L plus the axiom schemata of Theorems 2 and 3 and the rule of replacement of proved equivalence. I write L dyn ϕ if ϕ is a L dyn -theorem. In order to prove that the logic L dyn is complete we need first an expressiveness result. Proposition 3. For every L dyn -formula ϕ there exists an L-formula ϕ such that

L dyn ϕ ↔ ϕ .
Proof. By means of the principles R1-R8 in Theorem 2 and T1-T8 in Theorem 3, it is straightforward to prove that for every L dyn formula there is an equivalent L formula. In fact, each reduction axiom R3-R8 and T3-T8, when applied from the left to the right by means of the rule of replacement of proved equivalence, yields a simpler formula, where 'simpler' roughly speaking means that the dynamic operators are pushed inwards. Once the dynamic operators attain an atom they are eliminated by one of the equivalences R1-R2 and T1-T2. Theorem 4. The logic L dyn is complete.

Proof. The theorem is a straightforward consequence of Theorem 1 and Proposition 3, together with the fact that the logic L dyn is a conservative extension of the logic L.

Related works and perspectives

The formal semantics for commitment creation and commitment cancelation proposed in Section 4 can be seen as an application of the logical theory of assignments [START_REF] Van Ditmarsch | Semantic results for ontic and epistemic change[END_REF][START_REF] Van Benthem | Logics of communication and change[END_REF] that has been recently applied to model knowledge and intention dynamics (see, e.g., [START_REF] Van Ditmarsch | Introspective forgetting[END_REF][START_REF] Lorini | Intentions and assignments[END_REF]). It has also to be noted that the semantics of Section 4 corresponds to a two-event action model à la Baltag, Moss and Solecki (BMS) [START_REF] Baltag | The logic of public announcements, common knowledge and private suspicions[END_REF].

Several formal approaches to commitment have been recently proposed in the area of multi-agent systems and in the area of deontic logic. For instance, in [START_REF] Yolum | Commitment machines[END_REF] conditional commitments are modeled as unconditional commitments combined with strict (non material) implication. Bentahar et al. [START_REF] Bentahar | A logical model for commitment and argument network for agent communication[END_REF] provide an analysis of (propositional) dialectical and practical commitments in the context of conversation using a formal language based on an extended version of CTL (Computational Tree Logic) and on dynamic logic. A part of their work is devoted to discuss some intuitive reasoning postulates for commitment. Khan & Lésperance [START_REF] Khan | On the semantics of conditional commitment[END_REF] propose a rich formal analysis of conditional commitment. They use the term 'intention' and 'commitment' interchangeably since, they argue, the logical structure of the two is similar enough. Their account is set within a framework for modeling communicating agents based on the Situation Calculus. Verdicchio & Colombetti [27] also formalize commitments in a variant of CTL. They formally define the concepts of fulfilled commitment, violated commitment and pending commitment. However, all these approaches do not provide a sound and complete logic for the analysis of the static and dynamics aspects of commitments.

A different approach is proposed by Singh [START_REF] Singh | Semantical considerations on dialectical and practical commitments[END_REF] who takes seriously the issue of providing a model theory, and a sound and complete set of reasoning postulates for commitment. Singh focuses on dialectical (propositional) commitments and on practical commitments. However, its logical framework only applies to the static aspect of commitment and does not consider the dynamic dimension which is the main focus of the present contribution.

In this article I only considered unilateral commitments of an agent i towards another agent j. My main objective of future research is to extend the present analysis to bilateral commitments in order to capture interesting social notions such as the notion of agreement and the notion of contract. In fact, as a first approximation, an agreement can be defined as a bilateral commitment among the agents in a group. In more formal terms, two agents i 1 and i 2 have an agreement in the context of institution x to ensure respectively ϕ 1 if ψ 1 holds and ϕ 2 if ψ 2 holds if and only if, i 1 is committed to i 2 to ensure ϕ 1 if ψ 1 holds, and i 2 is committed to i 1 to ensure ϕ 2 if ψ 2 holds, that is: C i1:i2:x (ψ 1 ,ϕ 1 )∧C i2:i1:x (ψ 2 ,ϕ 2 ). Another aspect I intend to investigate in the future is a generalization of the present framework to commitments of an agent towards a group, and to commitments of a group towards an agent (or towards a group).

I also postpone to future work an extension of the logic L and of its dynamic variant L dyn by a temporal modal operator of the form F, where Fϕ means "ϕ will be true at some point in the future". This extension will enable to redefine the commitment modality C i:j:x ϕ introduced in Section 3 by the formula D x (¬F[i]ϕ → wr i,j,x ) ∧ D x ¬F[i]ϕ which makes explicit the temporal aspect of commitment. According to this definition, an agent i is committed to agent j in the context of institution x to ensure ϕ if and only if, i has a duty towards j in the context of institution x to ensure ϕ at some point in the future. This temporal variant of the notion of commitment is analogous to the notion of achievement goal proposed in the domain of BDI logics (see, e.g., [START_REF] Cohen | Intention is choice with commitment[END_REF]).

Fig. 1

 1 Fig.1contains a complete axiomatization of the logic L. We have all all principles of the normal modal logic S5 for every operator [i] and for the operator , and all principles of the normal modal logic KD for every operator D x . ( → i) and (AIA k ) are the two central principles in Xu's axiomatization of the Chellas's STIT operators[i]

  i:j:x+(ψ,ϕ) x and (v ∼x , u ∼x ) ∈ R i:j:x+(ψ,ϕ) then (w ∼x , u ∼x ) ∈ D i:j:x+(ψ,ϕ) x . Now consider the case y = x and suppose that (w x , v ∼x ) ∈ D i:j:x+(ψ,ϕ) y and (v ∼x , u ∼x ) ∈ R i:j:x+(ψ,ϕ) . Then, we have (w, v) ∈ D y and (v, u) ∈ R . By Constraint C3 on L-models, it follows that (w, u) ∈ D y . Consequently, we have (w x , u ∼x ) ∈ D i:j:x+(ψ,ϕ) y . In a similar way we can prove that if (w ∼x , v ∼x ) ∈ D i:j:x+(ψ,ϕ) y and (v ∼x , u ∼x ) ∈ R i:j:x+(ψ,ϕ) then (w ∼x , u ∼x ) ∈ D i:j:x+(ψ,ϕ) y . The truth conditions of the operators [i:j:x+(ψ, ϕ)] are the following: M, w |= [i:j:x+(ψ, ϕ)]χ iff M i:j:x+(ψ,ϕ) , w x |= χ.

Fig. 2 .

 2 Fig. 2. Example of commitment creation. The left side and the right side of the picture respectively represent the model before the operation of commitment creation 1:2:x+( , p) and the model resulting from this operation (the updated model). Vertical circles in the two models represent the regulation states of institution x and of institution y. For instance in the initial model, institution x and institution y have the same regulation state at world w. Inside each regulation state, there are two sets of possible outcomes (the two dotted grids). The rows in each grid are the outcome states of agent 1, whereas the columns are the outcome states of agent 2.

In legal theory it is typically assumed that a directed obligation for i towards j to ensure ϕ correlates to a right for j towards i that ϕ is brought about by i.

Acknowledgements

The author is grateful to the anonymous referees of DEON 2010, Tiago de Lima and Andreas Herzig for their helpful comments on the contents of this work.