Emiliano Lorini
email: lorini@irit.fr

Dominique Longin
email: longin@irit.fr

Benoit Gaudou
email: gaudou@irit.fr

Andreas Herzig
email: herzig@irit.fr

The logic of acceptance: grounding institutions on agents' attitudes

Keywords: Modal logic, institutions, acceptance, normative systems, multi-agent systems

In the recent years, several formal approaches to the specification of normative multi-agent systems and artificial institutions have been proposed. The aim of this paper is to advance the state of the art in this area by proposing an approach in which a normative multi-agent system is conceived to be autonomous, in the sense that it is able to create, maintain, and eventually change its own institutions by itself, without the intervention of an external designer in this process. In our approach the existence and the dynamics of an institution (norms, rules, institutional facts, etc.) are determined by the (individual and collective) acceptances of its members, and its dynamics depends on the dynamics of these acceptances.

In order to meet this objective, we propose the logic AL (Acceptance Logic) in which the acceptance of a proposition by the agents qua members of an institution is introduced. Such propositions are true w.r.t. an institutional context and correspond to facts that are instituted in an attitude-dependent way.

The second part of the paper is devoted to the logical characterization of some important notions in the theory of institutions. We provide a formalization of the concept of constitutive rule, expressed by a statement of the form "X counts as Y in the context of institution x". Then, we formalize the concepts of obligation and permission (so called regulative rules). In our approach constitutive rules and regulative rules of a certain institution are attitude-dependent facts which are grounded on the acceptances of the members of the institution.

Introduction

The problem of devising artificial institutions and modeling their dynamics is a fundamental problem in the multi-agent system (MAS) domain [START_REF] Dignum | Modelling agent societies: Coordination frameworks and institutions[END_REF]. Following [North, 1990, p. 3], artificial institutions can be conceived as "the rules of the game in a society or the humanly devised constraints that structure agents' interaction". Starting from this concept of institution, many researchers working in the field of normative MAS have been interested in developing models which describe the different kinds of rules and norms that agents have to deal with. In some models of artificial institutions norms are conceived as means to achieve coordination among agents and agents are supposed to comply with them and to obey the authorities of the system [START_REF] Esteva | Formalizing a language for institutions and norms[END_REF]. More sophisticated models of institutions leave to the agents' autonomy the decision whether to comply or not with the specified rules and norms of the institution [ Ågotnes et al., 2007, Lopez y Lopez et al., 2004]. However, all previous models abstract away from the legislative source of the norms of an institution, and from how institutions are created, maintained and changed by their members. More precisely, while it is widely shared in the MAS field that, in order to face complex and dynamical problems, individual agents must be autonomous, less emphasis is devoted to the fact that MASs themselves for exactly the same reasons should be conceived and designed to be autonomous. In fact, etymologically, autonomous means self-binding ('auto' and 'nomos'), and an autonomous MAS should be the vision of an artificial society that is able to create, maintain, and eventually change its own institutions by itself, without the intervention of the external designer in this process.

The aim of this work is to advance the state of the art on artificial institutions and normative multi-agent systems by proposing a logical model in which the existence and the dynamics of an institution (norms, rules, institutional facts, etc.) are determined by the individual and collective attitudes of the agents which identify themselves as members of the institution. In particular, we propose a model in which an institution is grounded on the (individual and collective) acceptances of its members, and its dynamics depends on the dynamics of these acceptances. On this aspect we agree with [START_REF] Mantzavinos | Learning, institutions, and economic performance[END_REF], when the authors say that (p. 77):

"only because institutions are anchored in peoples minds do they ever become behaviorally relevant. The elucidation of the internal aspect is the crucial step in adequately explaining the emergence, evolution, and effects of institutions." [Emphasis added]. This relationship between acceptance and institutions has been emphasized in the philosophical doctrine of Legal Positivism [Hart, 1992]. According to Hart, the foundations of a normative system or institution consist of adherence to, or acceptance of, an ultimate rule of recognition by which the validity of any rule of the institution may be evaluated. 1Other authors working in the field of multi-agent systems have advocated the need for a bottom up approach to the explanation of the origin and the evolution of institutions. According to these authors, institutions and their dynamics should be anchored in the agents' attitudes [Conte et al., 1998, Boella andvan der Torre, 2007]. For instance, in agreement with Hart's theory, [START_REF] Conte | Autonomous norm acceptance[END_REF]] have stressed that the existence of a norm in an institution (but also in a group, organization, etc.) depends on the recognition and acceptance of the norm by the members of the institution. In their perspective, agents in a multi-agent system contribute to the enforcement and the propagation of the norm in the social context.

The fundamental concept in our paper is that of acceptance qua member of an institution. This notion will be informally presented in Section 2. In Section 3 we will introduce a modal logic (called AL for Acceptance Logic) which enables to reason about acceptances of agents and groups of agents. We call the former individual acceptances, and the latter collective acceptances. In Section 4 we will study the logical properties of the notion of acceptance and its interactions with classical notions such that of individual (private) belief and that of mutual belief. On the basis of the concept of acceptance qua member of an institution, we will specify how a group of agents can create and maintain normative and institutional facts which hold only in an attitudedependent way. That is, it is up to the agents, and not to the external designer, to support such facts (Section 5). Then, we will distinguish regulative components and nonregulative components of an institution [Searle, 1995] (Section 6). On the one hand, we will formalize the concept of constitutive rule, that is, the kind of rules accepted by the members of an institution which express classifications between different concepts and establish the relations between "brute" physical facts and institutional facts within the context of the institution (Section 6.1). Since [Searle, 1995, Searle, 1969] and [START_REF] Jones | A formal characterization of institutionalised power[END_REF]], these rules have been expressed in terms of assertions of the form "X counts as Y in the context of institution x" (e.g. in the institutional context of US, a piece of paper with a certain shape, color, etc. counts as a five-dollar bill). On the other hand, regulative rules will be formalized through a notion of obligation and a notion of permission by studying a reduction of deontic logic to the logic of acceptance (Section 6.2). Section 7 will be devoted to show how the logic of acceptance AL can be appropriately refined in order to capture some essential properties of legal institutions in which a special kind of agents called legislators are introduced. We will discuss some general principles which seem adequate for a formal characterization of legal institutions. Finally, in Section 8, we will compare our proposal with related logical works on institutions and normative systems. Special emphasis will be devoted to the comparison between our approach and the modal logic of normative systems and "counts-as" proposed by [START_REF] Grossi | Classificatory aspects of counts-as: An analysis in modal logic[END_REF]. Proofs of the main theorems presented in the paper are collected in the annex.

The concept of acceptance

Some conceptual clarifications of the concept of acceptance qua member of an institution are needed because of the crucial role it plays in explaining the maintenance of social institutions.

Several authors have emphasized the difference between acceptance and belief as particular kinds of individual attitudes. Whereas private beliefs have been studied for decades [Hintikka, 1962] as representative of doxastic mental states, acceptances have only been examined since [Stalnaker, 1984] and since [Cohen, 1992]. Some authors (e.g. [Clarke, 1994]) claim that acceptance implies belief (at least to some minimal degree as argued in [Tollefsen, 2003]). On the contrary, in [Stalnaker, 1984] acceptance is considered to be stronger than belief. Although belief and acceptance seem very close, several authors [Bratman, 1992, Cohen, 1992, Tuomela, 2000] have argued for the importance of keeping the two notions independent. We here agree with this point of view (see Section 4.3).

For the aims of this paper we are particularly interested in a particular feature of acceptance, namely the fact that acceptance is context-dependent (on this point see also [Engel, 1998]). In our approach, this feature is directly encoded in the formal definition of acceptance (see Section 3.1). In fact, one can decide (say for prudential reasons) to reason and act by "accepting" the truth of a proposition in a specific context, and reject the very same proposition in a different context. We will explore the role of acceptance in institutional contexts. Institutional contexts are conceived here as rule-governed social practices on the background of which the agents reason. For example, take the case of a game like Clue. The institutional context is the rule-governed social practice which the agents conform to in order to be competent players. On the background of such contexts, we are interested in the agents' attitudes that can be formally captured. In the context of Clue, for instance, an agent accepts that something has happened qua player of Clue. The state of acceptance qua member of an institution is the kind of acceptance one is committed to when one is "functioning as a member of the institution" [Tuomela, 2002, Tuomela, 2007]. In these situations it may happen that the agent's acceptances are in conflict with his/her beliefs. For instance, a lawyer who is trying to defend a client in a murder case accepts qua lawyer that his/her client is innocent, even she/he believes the contrary.

There exist others differences between belief and acceptance that are not encoded in our formalization of acceptance. According to [Hakli, 2006], the key difference between belief and acceptance is that the former is aimed at truth, whilst the latter depends on an agent's decision. More precisely, while a belief that p is an attitude constitutively aimed at the truth of p, an acceptance is the output of "a decision to treat p as true in one's utterances and actions" without being necessarily (see [Tuomela, 2000] for instance) connected to the actual truth of the proposition.

In the present paper the notion of acceptance qua member of an institution is also applied to the collective level named collective acceptance. The idea of collective attitudes is developed by Searle [Searle, 1995] among others: without supposing the existence of any collective consciousness, he argues that attitudes can be ascribed to a group of agents and that "the forms of collective intentionality cannot (...) be reduced to something else" [Searle, 1995] 2 .

Collective attitudes such as collective acceptance have been studied in social philosophy in opposition to the traditional notions of mutual belief and mutual knowl-edge that are very popular in artificial intelligence and theoretical computer science [START_REF] Fagin | Reasoning about Knowledge[END_REF], Lewis, 1969]. It has been stressed that, while mutual belief is strongly linked to individual beliefs and can be reduced to them, collective attitudes such as collective acceptance cannot be reduced to a composition of individual attitudes. This aspect is particularly emphasized by Gilbert [Gilbert, 1987] who follows Durkheim's non-reductionist view of collective attitudes [Durkheim, 1982]. According to Gilbert, any proper group attitude cannot be defined only as a label on a particular configuration of individual attitudes, as mutual belief is. In [Gilbert, 1989, Tuomela, 2007] it is suggested that a collective acceptance of a set of agents C is based on the fact that the agents in C identify themselves as members of a certain group, institution, team, organization, etc. and recognize each other as members of the same group, institution, team, organization, etc. (this is the view that we adopt in our formalization of acceptance, see Section 3). But mutual belief (and mutual knowledge) does not entail this aspect of mutual recognition and identification with respect to the same social context.

In accordance with [Tuomela, 2002, Tuomela, 2007], in this paper we consider collective acceptance with respect to institutional contexts as an attitude that is held by a set of agents qua members of the same institution. A collective acceptance held by a set of agents C qua members of a certain institution x is the kind of acceptance the agents in C are committed to when they are "functioning together as members of the institution x", that is, when the agents in C identify and recognize each other as members of the institution x. For example, in the context of the institution Greenpeace agents (collectively) accept that their mission is to protect the Earth qua members of Greenpeace. The state of acceptance qua members of Greenpeace is the kind of acceptance these agents are committed to when they are functioning together as members of Greenpeace, that is, when they identify and recognize each other as members of Greenpeace.

Acceptance logic

The logic AL (Acceptance Logic) enables expressing that some agents identify themselves as members of a certain institution and what (groups of) agents accept while functioning together as members of an institution. The principles of AL clarify the relationships between individual acceptances (acceptances of individual agents) and collective acceptances (acceptances of groups of agents).

Syntax

The syntactic primitives of AL are the following: a finite non-empty set of agents AGT ; a countable set of atomic formulas ATM ; and a finite set of labels INST denoting institutions. We note 2 AGT = 2 AGT \ {∅} the set of all non-empty subsets of AGT . The language L AL of the logic AL is given by the following BNF:

ϕ ::= ⊥ | p | ¬ϕ | ϕ ∨ ϕ | A C :x ϕ
where p ranges over ATM , C ranges over 2 AGT and x ranges over INST . We define ∧, →, ↔ and from ∨, ¬ and ⊥ in the usual manner.

The formula A C :x ϕ reads "the agents in C accept that ϕ while functioning together as members of the institution x ". For notational convenience, we write i :x instead of {i }:x .

For example, A C :Greenpeace protectEarth expresses that the agents in C accept that the mission of Greenpeace is to protect the Earth while functioning together as activists in the context of Greenpeace; and A i:Catholic PopeInfallibility expresses that agent i accepts that the Pope is infallible while functioning as a member of the Catholic Church.

The formula A C :x ⊥ has to be read "agents in C are not functioning together as members of the institution x ", because we assume that functioning as a member of an institution is, at least in this minimal sense, a rational activity. Conversely, ¬A C :x ⊥ has to be read "agents in C are functioning together as members of the institution x ". Thus, ¬A C :x ⊥ ∧ A C :x ϕ stands for "agents in C are functioning together as members of the institution x and they accept that ϕ while functioning together as members of x " or simply "agents in C accept that ϕ qua members of the institution x ". Therefore ¬A C :x ϕ has to be read "agents in C do not accept that ϕ be true qua members of x".

AL frames

We use a standard possible worlds semantics. Let the set of all couples of non-empty subsets of agents and institutional contexts be ∆ = 2 AGT × INST . A frame of the logic of acceptance AL (AL frame) is a couple F = W , A where:

• W is a non-empty set of possible worlds;

• A : ∆ → W × W maps every C :x ∈ ∆ to a relation A C :x between possible worlds in W .
We note A C :x (w ) = {w : w , w ∈ A C :x } the set of worlds that the agents in C accept at w while functioning together as members of the institution x .

We impose the following constraints on AL frames, for any world w ∈ W , institutional context x ∈ INST , and sets of agents

C , B ∈ 2 AGT such that B ⊆ C : if w ∈ A B:y (w ) then A C :x (w ) ⊆ A C :x (w ) (S.1) if w ∈ A B:y (w ) then A C :x (w ) ⊆ A C :x (w ) (S.2) if A C :x (w ) = ∅ then A B:x (w ) ⊆ A C :x (w ) (S.3) if w ∈ A C :x (w ) then w ∈ i∈C A i:x (w ) (S.4) if A C :x (w ) = ∅ then A B:x (w ) = ∅ (S.5)
The constraint S.1 is a generalized version of transitivity: given two sets of agents C , B such that B ⊆ C , if w is a world that the agents in B accept at w while functioning together as members of the institution y and w is a world that the agents in C accept at w while functioning together as members of the institution x then, w is a world that the agents in C accept at w while functioning together as members of the institution x.

The constraint S.2 is a generalized version of euclideanity: given two sets of agents C , B such that B ⊆ C , if w is a world that the agents in B accept at w while functioning together as members of the institution y and w is a world that the agents in C accept at w while functioning together as members of the institution x then, w is a world that the agents in C accept at w while functioning together as members of the institution x.

The constraint S.3 is a property of conditional inclusion: given two sets of agents C , B such that B ⊆ C , if there exists a world w that the agents in C accept at w while functioning together as members of the institution x and w is a world that the agents in B accept at w while functioning together as members of the institution x then, w is also a world that the agents in C accept at w while functioning together as members of the institution x.

The constraint S.4 is a sort of weak reflexivity: if w is a world that the agents in C accept at w while functioning together as members of the institution x then, there exists some agent i ∈ C such that w is a world that agent i accepts at w , while functioning as a member of the institution x.

According to the last constraint S.5, given two sets of agents C , B such that B ⊆ C , if there exists a world w that the agents in C accept at w while functioning together as members of the institution x then, there exists a world w that the agents in B accept at w while functioning together as members of the institution x.

AL models and validity

A model of the logic of acceptance AL (AL model) is a couple M = F, V where:

• F is a AL frame;

• V : ATM → 2 W is valuation function associating a set of possible worlds V (p) ⊆ W to each atomic formula p of ATM .

Given M = W , A , V and w ∈ W , the couple M, w is a pointed AL model. Given a formula ϕ, we write M, w |= ϕ and say that ϕ is true at world w in M. The notation M, w |= ϕ means that ϕ is false at world w in M. The truth conditions for the formulas of the logic AL are:

• M, w |= ⊥; • M, w |= p iff w ∈ V (p); • M, w |= ¬ϕ iff M, w |= ϕ; • M, w |= ϕ ∨ ψ iff M, w |= ϕ or M, w |= ψ; • M, w |= A C :x ϕ iff M, w |= ϕ for all w ∈ A C :x (w ).
A

Axiomatization

The axiomatization of AL is as follows:

All principles of propositional calculus (ProTau)

A C :x (ϕ → ψ) → (A C :x ϕ → A C :x ψ) (K) A C :x ϕ → A B:y A C :x ϕ if B ⊆ C (PAccess) ¬A C :x ϕ → A B:y ¬A C :x ϕ if B ⊆ C (NAccess) (¬A C :x ⊥ ∧ A C :x ϕ) → A B:x ϕ if B ⊆ C (Inc) A C :x ( i∈C A i:x ϕ → ϕ) (Unanim) ¬A C :x ⊥ → ¬A B:x ⊥ if B ⊆ C (Mon) From ϕ and ϕ → ψ infer ψ (MP) From ϕ infer A C :x ψ (Nec)
This axiomatization includes all tautologies of propositional calculus (ProTau) and the rule of inference modus ponens (MP). Axiom K and rule of necessitation (Nec) define a minimal normal modal logic. (See [Chellas, 1980, chap. 4].)

Axioms PAccess and NAccess express that a group of agents has always access to what is accepted (resp. not accepted) by its supergroups.

Axiom PAccess concerns the (positive) access to what is accepted by a supergroup: when the agents in a set C function together as members of the institution x , then for all B ⊆ C the agents in B have access to all facts that are accepted by the agents in C . That is, if the agents in C accept that ϕ while functioning together as members of the institution x then, while functioning together as members of x , the agents of every subset B of C accept that the agents in C accept that ϕ.

Axiom NAccess concerns the (negative) access to what is not accepted by a supergroup: if the agents in C do not accept that ϕ while functioning together as members of the institution x then, while functioning together as members of x , the agents of every subset B of C accept that the agents in C do not accept that ϕ.

Example 1. Suppose that three agents i, j, k, while functioning together as members of the UK trade union, accept that their mission is to increase teachers' wages, but they do not accept qua members of the trade union that their mission is to increase railway workers' wages: A {i,j,k}:Union increaseTeacherWage and ¬A {i,j,k}:Union increaseRailwayWage.

By Axiom PAccess we infer that, while functioning as a UK citizen, i accepts that i, j, k accept that their mission is to increase teachers' wages, while functioning together as members of the trade union:

A i:U K A {i,j,k}:Union increaseTeacherWage. By Axiom NAccess we infer that, while functioning as a UK citizen, i accepts that i, j, k do not accept, qua members of the trade union, that their mission is to increase railway workers' wages:

A i:U K ¬A {i,j,k}:Union increaseRailwayWage.

Axiom Inc says that, if the agents in C accept that ϕ qua members of x then for every subset B of C the agents in B accept ϕ while functioning together as members of x . This means that the facts accepted by the agents in C qua members of a certain institution x are necessarily accepted by the agents in all of C 's subsets with respect to the same institution. Therefore Axiom Inc describes the top down process leading from C 's collective acceptance to the individual acceptances of the agents in C .

Example 2. Imagine three agents i, j, k that, qua players of the game Clue, accept that someone called Mrs. Red, has been killed:

¬A {i,j,k}:Clue ⊥ ∧ A {i,j,k}:Clue killedMrsRed . By Axiom Inc we infer that also the two agents i, j, while functioning as Clue players, accept that someone called Mrs. Red has been killed:

A {i,j}:Clue killedMrsRed .

Axiom Unanim expresses a unanimity principle according to which the agents in C , while functioning together as members of x , accept that if each of them individually accepts that ϕ while functioning as a member of x , then ϕ is the case. This axiom describes the bottom up process leading from the individual acceptances of the members of C to the collective acceptance of the group C .

Finally, Axiom Mon expresses an intuitive property of monotonicity about institution membership. It says that, if the agents in C are functioning together as members of the institution x then, for every subset B of C , the agents in B are also functioning together as members of the institution x . As emphasized in Section 2, "the agents in C function together as members of institution x " means for us that "the agents in C identify and recognize each other as members of the same institution x ". Thus, Axiom Mon can be rephrased as follows: if the agents in a set C identify and recognize each other as members of the institution x then, for every subset B of C , the agents in B also identify and recognize each other as members of x .

The following correspondences (in the sense of correspondence theory, see for instance [van Benthem, 2001, Blackburn et al., 2001]) exist between the axioms of the logic AL and the semantic constraints over AL frames given in Section 3.2 (see also proof of Theorem 1 in the Annex): Axiom PAccess corresponds to the constraint S.1, NAccess corresponds to S.2, Inc corresponds to S.3, Unanim corresponds to S.4 and Mon corresponds to S.5.

We call AL the logic axiomatized by the principles given above: ProTau, K, PAccess, NAccess, Inc, Unanim, Mon, MP, Nec. We write AL ϕ if formula ϕ is a theorem of AL and AL ϕ if formula ϕ is not a theorem.

We can prove that AL is sound and complete with respect to the class of AL frames.

Theorem 1. AL ϕ if and only if |= AL ϕ.

By the standard filtration method we can also prove that the logic AL is decidable.

Theorem 2. The logic AL is decidable.

In the following section the properties of the concepts of individual acceptance, collective acceptance and institution membership will be studied. We will also study the relationships between acceptance and belief in a more formal way than in Section 2.

4 General properties

Properties of acceptance and institution membership

The following theorem highlights some interesting properties of collective acceptance and institution membership.

Theorem 3. For every x, y ∈ INST and B, C ∈ 2 AGT such that B ⊆ C :

AL A C :x ¬A C :x ⊥ (3a) AL A C :x i∈C ¬A i:x ⊥ (3b) AL A B:y A C :x ϕ ↔ A C :x ϕ (3c) AL A B:y ¬A C :x ϕ ↔ (A B:y ⊥ ∨ ¬A C :x ϕ) (3d) AL A C :x (A C :x ϕ → ϕ) (3e) AL (A C :x i∈C A i:x ϕ) ↔ A C :x ϕ (3f)
Theorem 3a expresses a property of institution membership. It says that the agents in a group C , while functioning together as members of the institution x, accept that they are functioning together as members of the institution x. Theorem 3b is another way to express the property of institution membership: it expresses that the agents in a group, while functioning together as members of a certain institution, accept that everyone of them is functioning as a member of the institution.

Example 3. Suppose that, during a concert, the agents in C are functioning together as members of the Philharmonic Orchestra. Then, according to Theorem 3a, this fact is accepted by the group C . That is, while functioning together as members of the Philharmonic Orchestra, the agents in C accept that they are functioning together as members of the Philharmonic Orchestra: A C:Orchestra ¬A C:Orchestra ⊥. Moreover, they accept that everyone of them is functioning as a member of the Philharmonic Orchestra: A C:Orchestra i∈C ¬A i:Orchestra ⊥.

Theorem 3c and Theorem 3d together express that a group of agents B can never be wrong in ascribing a collective acceptance to its supergroup C and in recognizing that its supergroup C does not accept something. Furthermore, a group of agents B has always correct access to what is accepted (resp. not accepted) by its supergroups. The right to left direction of Theorem 3c is Axiom PAccess. The left to right direction means that, given two sets of agents B and C such that B ⊆ C , if the agents in B , while functioning together as members of institution y, accept that the agents in C accept ϕ while functioning together as members of institution x then, the agents in C accept ϕ while functioning together as members of institution x. The right to left direction of Theorem 3d is Axiom NAccess. The left to right direction means that, given two sets of agents B and C such that B ⊆ C , if the agents in B , while functioning together as members of institution y, accept that the agents in C do not accept ϕ qua members of institution x then, either the agents in B do not function as members of y or the agents in C do not accept ϕ qua members of institution x.

Theorem 3e and Theorem 3f are variants of the unanimity Axiom Unanim. Theorem 3e says that for every set of agents C , the agents in C , while functioning together as members of x , accept that if they accept that ϕ while functioning together as members of x , then ϕ is the case. Theorem 3f expresses that: if the agents in C , while functioning together as members of x , accept that each of them individually accepts that ϕ while functioning as a member of x , then the agents in C , while functioning together as members of x , accept that ϕ is the case.

The following theorem highlights the relationship between the acceptance of a group of agents and the acceptances of its subgroups.

Theorem 4. For every x ∈ INST and C 1 , C 2 , C 3 ∈ 2 AGT such that C 3 ⊆ C 2 ⊆ C 1 and C 3 = ∅: AL A C1:x (A C2:x ϕ → A C3:x ϕ)
Theorem 4 expresses that every group of agents has to accept the principle of inclusion formalized by Axiom Inc.

Discussion around the unanimity principle

Let us consider more in detail the unanimity property of our logic of acceptance expressed by Axiom Unanim (and Theorems 3e,3f). This property says that collective acceptances emerge from consensus. This is for us a necessary requirement for a notion of collective acceptance which is valid for all institutions and groups. We did not include stronger principles which explain how a collective acceptance of a group of agents C might be constructed. Nevertheless, one might go further and consider other kinds of principles which are specific to certain institutions and groups.

For example, one might want to extend the analysis to formal (legal) institutions in which special agents with the power to affect the acceptances of the other members of the institution are introduced. In legal institutions, one can formalize the rule according to which all facts that are accepted by the legislators of an institution must be universally accepted by all members of this institution. Suppose that x denotes a legal institution (e.g. EU, Association of Symbolic Logic, etc.) which has a non-empty set of agents called legislators, noted Leg(x ) ∈ 2 AGT . (See Section 7 for a precise definition of the function Leg() and a more elaborate analysis of the concepts of legislator and legal institution.) From this, one can formalize a principle stating that everything that the legislators of the legal institution x accept is universally accepted in the legal institution x :

A C :x ( i∈Leg(x ) A i:x ϕ → ϕ) (Legislators)
The Principle Legislators says that, for every group of agents C , while functioning together as members of the institution x , the agents in C accept that if the legislators of x accept that ϕ, then ϕ is the case.

Another interesting principle for the construction of collective acceptance is majority. (In this case, unanimity is not required to obtain a consensus.) This kind of principle applies both to informal and formal institutions. The principle of majority could be introduced as a logical axiom for two specific sets of agents C and B such that B ⊆ C and |C \ B| < |B | (i.e. B represents the majority of agents in C):

A C :x ( i∈B A i:x ϕ → ϕ) (Majority)
The Principle Majority says that, for every group of agents C , while functioning together as members of the institution x , the agents in C accept that if the majority of them accept that ϕ, then ϕ is the case. The following example by Pettit [Pettit, 2001] shows how the majority principle would work.

Example 4. Imagine a three-member court which has to make a judgment on whether a defendant is liable (noted l) for a breach of contract. The three judges i, j and k accept a majority rule to decide on the issue. That is, i, j and k, while functioning together as members of the court, accept that if the majority of them accepts that the defendant is liable (resp. not liable), then the defendant is liable (resp. not liable). Formally, for any B such that B ⊆ {i , j , k } and |B | = 2 we have:

A {i,j ,k }:court ( i∈B A i:court l → l) ∧ A {i,j ,k }:court ( i∈B A i:court ¬l → ¬l)
Therefore, if the three judges accept that two of them accept that the defendant is liable, i.e. A {i,j ,k }:court (A i:court l ∧ A j:court l), by the Principle Majority and Axiom K it follows that the three judges have to accept that the judge is liable, i.e. A {i,j ,k }:court l).

It has to be noted that the previous principle of majority cannot be generalized to all sets of agents without incurring the following very counterintuitive consequence.

Proposition 1. If we suppose that the Principle Majority is valid for any B, C such that B ⊆ C and |C \ B| < |B | then, the following consequence is derivable, for i = j:

(A AGT :x A {i,j }:x ϕ ∧ ¬A AGT :x ⊥) → A AGT :x ϕ
This means that, when the majority principle is generalized to all sets of agents, we can infer that: if all agents, qua members of institution x, accept that two of them accept ϕ while functioning together as members of institution x then, the acceptances of the two agents propagate to all agents in such a way that all agents accept ϕ qua members of institution x.

Relationships between acceptance and belief

As said in Section 2, there is a large literature about the distinction between belief and acceptance. For us, belief and acceptance are clearly different concepts in several senses. In this section we focus on the distinction between acceptance, individual belief and mutual belief. Our aim is to provide further clarifications of the concept of acceptance in terms of its relationships with other kinds of agents' attitudes rather than proposing an extension of the logic AL with individual belief and mutual belief and studying its mathematical properties. Here, we just show how modal operators for belief and mutual belief can be integrated into the logic AL on the basis of some intuitive interaction principles relating acceptance and belief.

For convenience, we note Bel i ϕ the formula that reads "the agent i believes that ϕ is true", and we suppose that belief operators of type Bel i are defined as usual in a KD45 modal logic [Hintikka, 1962]. Belief operators Bel i are interpreted in terms of accessibility relations B i on the set of possible worlds W . These accessibility relations are supposed to be serial, transitive and euclidean. We write B i (w ) for the set {w : w , w ∈ B i }. B i (w ) is the set of worlds that are possible according to agent i. The truth condition is:

M, w |= Bel i ϕ iff M, w |= ϕ for every w ∈ B i (w )
Moreover we introduce the notion of mutual belief which has been extensively studied both in the computer science literature [START_REF] Fagin | Reasoning about Knowledge[END_REF] and in the philosophical literature [Lewis, 1969]. Given a set of agents C ⊆ AGT , MB C ϕ reads "there is a mutual belief in C that ϕ", that is, "everyone in C believes that ϕ, everyone in C believes that everyone in C believes that ϕ, everyone in C believes that everyone in C believes that everyone in C believes that ϕ, and so on". The mutual belief of a set of agents C is interpreted in terms of the transitive closure B + C of the union of the accessibility relations B i for every agent i ∈ C , that is:

M, w |= MB C ϕ iff M, w |= ϕ for every w ∈ B + C (w )
Let the concept of "everybody in group C believes ϕ" be defined as follows:

E C ϕ def = i∈C Bel i ϕ
As shown in [START_REF] Fagin | Reasoning about Knowledge[END_REF], the following axioms and rules of inference provide a sound and complete axiomatization of the logic of individual belief and mutual belief:

All KD45-principles for the operators Bel i (KD45 Bel ) MB C ϕ ↔ E C (ϕ ∧ MB C ϕ) (FixPoint) From ϕ → E C (ϕ ∧ ψ) infer ϕ → MB C ψ (InductionRule)
The first interesting thing to note is that, although collective acceptance and mutual belief have different natures (see the discussion in Section 2), they share the Fix Point property. The following Theorem 5 highlights this aspect.

Theorem 5.

AL A C :x ϕ ↔ i∈C A i:x (ϕ ∧ A C :x ϕ)
Nevertheless we cannot argue that our concept of collective acceptance is stronger than the concept of mutual belief, in particular because the InductionRule does not hold in AL. This is due to the non-reductionist feature of the collective acceptance: it cannot be reduced to a particular configuration of individual acceptances.

The following two sections are devoted to discuss other interesting relations between acceptance and belief. We will first provide an analysis of the shared aspect of collective acceptance expressed in terms of mutual belief. Then, we will briefly consider the problem of the incompatibility between acceptance and belief.

The shared nature of collective acceptance

As emphasized in the philosophical literature [Gilbert, 1989, Tuomela, 1992], a collective acceptance of the agents in a set C must not be confused with (nor reduced to) the sum of the individual acceptance of the agents in C . On the contrary, when the agents in C accept some fact ϕ to be true qua members of a certain institution, it means that every agent in C declares to the other agents of the group C that she/he is willing to accept ϕ to be true. This aspect of acceptance can be formally derived by supposing the following two principles relating individual beliefs with collective acceptances.

A C :x ϕ → Bel i A C :x ϕ if i ∈ C (PIntrAccept) ¬A C :x ϕ → Bel i ¬A C :x ϕ if i ∈ C (NegIntrAccept)
The first principle says that: if the agents in C accept that ϕ while functioning together as members of the institution x then, every agent in C believes this. The second principle says that: if the agents in C do not accept ϕ qua members of x then every agent in C believes this.

We can easily prove that, under the previous two principles, collective acceptance is always shared so much that the group C accepts ϕ if and only if the agents in C mutually believe this. More formally: Proposition 2. For any C :x ∈ ∆, the following formulas are derivable from the axiom D for belief (following from KD45 Bel ), Axiom FixPoint and Rule of inference InductionRule for mutual belief, and the interaction Principles PIntrAccept and NegIntrAccept for acceptance and belief.

A C :x ϕ ↔ MB C A C :x ϕ (2a) ¬A C :x ϕ ↔ MB C ¬A C :x ϕ (2b)
According to Proposition 2a, the agents in C accept that ϕ while functioning together as members of the institution x if and only if there is a mutual belief in C that they accept that ϕ while functioning together as members of the institution x. According to Proposition 2b, the agents in C do not accept that ϕ qua members of x if and only if there is a mutual belief in C that they do not accept that ϕ qua members of x . Hence, accepting (resp. not accepting) a proposition while functioning as members of an institution is always a mutually believed fact (for the members of the group) which is out in the open and that is used by all the members to reason about each other in the institutional context.

Acceptance and belief might be incompatible

Individual belief and individual acceptance are both private mental attitudes but: an individual belief does not depend on context, whilst an individual acceptance is a contextdependent attitude which is entertained by an agent qua member of a given institution. Therefore, an agent can privately disbelieve something she/he accepts while functioning as a member of a given institution. Formally: Bel i ϕ ∧ A i:x ¬ϕ may be true. In a similar way, as emphasized in [Tuomela, 1992], a collective acceptance that ϕ by a group of agents C (qua members of a given institution) might be compatible with the fact that none of the agents in C believes that ϕ (and even that every agent in C believes that ¬ϕ). The following example, inspired by [Tuomela, 1992, p. 285], illustrates this point.

Example 5. At the end of the 80s, the Communist Party of Ruritania accepted that capitalist countries will soon perish (but none of its members really believed so).

This means that the agents in C accept that capitalist countries will perish (ccwp) qua members of the Communist Party of Ruritania (CPR) but nobody in C (privately) believes this. Thus, formally: ¬A C:CPR ⊥ ∧ A C:CPR ccwp ∧ i∈C ¬Bel i ccwp.

In the following Section 5 we will show how institutional facts can be grounded on agents' acceptances in such a way that the existence of the former depends on the latter.

Truth in an institutional context

Recent theories of institutions [Lagerspetz, 2006, Searle, 1995, Tuomela, 2002] share at least the following two theses.

Performativity: the acceptance that a certain fact is true shared by the members of a certain institution may contribute to the truth of this fact within the context of the institution.

Reflexivity: if a certain fact is true within the context of a certain institution, the acceptance of this fact by the members of the institution is present.

More precisely, a certain fact ϕ is true within the context of an institution x if and only if the fact ϕ is accepted to be true by the members of the institution x. Therefore, a necessary condition for the existence of a fact within the context of an institution is that this fact is accepted to exist by the members of the institution. Moreover, the acceptance of a certain fact by the members of an institution is a sufficient condition for the existence of this fact within the context of the institution.

Example 6. If the agents, qua European citizens, accept a certain piece of paper with a certain shape, color, etc. as money, then, within the context of EU, this piece of paper is money (performativity). At the same time, if it is true that a certain piece of paper is money within the context of EU, then the agents qua European citizens accept the piece of paper as money (reflexivity).

Our aim here is to represent in AL those facts that are true within the context of an institution, that is, to define the concept of truth with respect to an institutional context (institutional truth) in a way that respects the previous two principles of reflexivity and performativity. We formalize the notion of institutional truth by means of the operator [x]. A formula [x] ϕ is read "within the institutional context x, it is the case that ϕ". We take the latter to be synonymous of "for every set of agents C , the agents in C accept that ϕ while functioning together as members of the institution x". Formally, for every

x ∈ INST : [x] ϕ def = C∈2 AGT A C :x ϕ
According to our definition, a fact ϕ is true within the context of institution x if and only if, for every group C , the agents in C accept ϕ, while functioning together as members of x . Hence the performativity and the reflexivity principles mentioned above are guaranteed.

It is worth noting that this formal definition of truth with respect to an institution is perfectly adequate to characterize informal institutions in which there are no specialized agents called legislators empowered to change the institution itself on behalf of everybody else. It is a peculiar property of informal institutions the fact that they are based on the general consensus of all their members [Coleman, 1990], that is, a certain fact ϕ is true within the context of an informal institution x if and only if all members of x accept ϕ to be true. In Section 7 we will show how the operator [x] can be appropriately redefined in order to characterize formal (legal) institution and to distinguish them from informal institutions. For the moment, we just suppose that our model only applies to the basic informal institutions of a society in which no legislator is given.

It is straightforward to prove that [x] is a normal modal operator satisfying Axiom K and the necessitation rule. Theorem 6. For every x ∈ INST :

AL [x] (ϕ → ψ) → ([x] ϕ → [x] ψ) (6a) From AL ϕ infer AL [x] ϕ (6b)
Nevertheless, institutional operators of type [x] fail to satisfy Axiom 4 and Axiom 5. That is,

[x] ϕ ∧ ¬ [x] [x] ϕ and ¬ [x] ϕ ∧ ¬ [x] ¬ [x]
ϕ are satisfiable in the logic AL for any x ∈ INST . This means that for every institution x, the members of x might accept ϕ while they do not accept that they accept ϕ and, it might be the case that the members of x do not accept ϕ, while they do not accept that they do not accept ϕ. The operator [x] does to satisfy these two properties because of the restriction imposed on Axioms PAccess and NAccess according to which, the agents in a group B have access to all facts accepted (resp. not accepted) by the agents in another group C , only if B is a subgroup of C . Therefore, in the logic AL, a certain fact ϕ might be accepted by all groups of members of a certain institution x, while some group of members of x does not have access to the fact that all groups of members of x accept ϕ. (See Section 8.1 for a discussion about a different point of view.)

The following operator [Univ ] is defined in order to express facts which are true in all institutions:

[Univ ]

ϕ def = x∈INST [x] ϕ
where [Univ ] ϕ is meant to stand for "ϕ is universally accepted as true". The operator [Univ ] is also a normal modal operator satisfying Axiom K and the necessitation rule:

Theorem 7. AL [Univ ] (ϕ → ψ) → ([Univ ] ϕ → [Univ ] ψ) (7a) From AL ϕ infer AL [Univ ] ϕ (7b)
The operator [Univ ] too fails to satisfy Axiom 4 and Axiom 5. Indeed,

[Univ ] ϕ ∧ ¬ [Univ ] [Univ ] ϕ and ¬ [Univ ] ϕ ∧ ¬ [Univ ] ¬ [Univ ] ϕ are satisfiable in the logic AL.
This means that: ϕ might be universally accepted, while it is not universally accepted that ϕ is universally accepted and; it might be the case that ϕ is not universally accepted, while it is not universally accepted that ϕ is not universally accepted.

In the following section operators of institutional truth of type [x] and the operator of universal truth [Univ ] will be used to define the concepts of constitutive rule and regulative rule. These two concepts are indeed fundamental for a theory of institutions.

Constitutive rules and regulative rules

According to many philosophers [Rawls, 1955, Alchourrón and[START_REF] Alchourrón | [END_REF] working on social theory and researchers in the field of normative multi-agent systems [START_REF] Boella | Regulative and constitutive norms in normative multiagent systems[END_REF], institutions are based both on regulative and nonregulative components. In particular, institutions are not only defined in terms of sets of permissions, obligations, and prohibitions (i.e. norms of conduct [Bulygin, 1992]) but also in terms of rules which specify and create new forms of behavior and concepts. Several terms such as constitutive rule [Searle, 1969, Searle, 1995], conceptual rule [Bulygin, 1992] or determinative rule [Von [START_REF] Wright | [END_REF] have been used to identify this non-regulative dimension of institutions. According to Searle for instance "(...) regulative rules regulate antecedently or independently existing forms of behavior (...). But constitutive rules do not merely regulate, they create or define new forms of behavior" [Searle, 1969, p. 33]. In Searle's theory of institutions [Searle, 1969, Searle, 1995], constitutive (i.e. non-regulative) rules are expressed by means of "counts-as" statements of the form "X counts as Y in context x" where the context x refers to the institution/normative system in which the rule is specified. As emphasized in [START_REF] Grossi | Classificatory aspects of counts-as: An analysis in modal logic[END_REF], "counts-as" statements are used to express classifications and subsumption relations between different concepts, that is, they assert just that a concept X is a subconcept of a concept Y. These classifications are fundamental for establishing the relations between "brute" physical facts and objects on the one hand, and institutional facts and objects on the other hand (e.g. money, private property, etc.). For example, in the institutional context of Europe, a piece of paper with a certain shape, color, etc. (a physical object) counts as a five-euro bill (an institutional object).

Constitutive rules

From the concept of institutional truth presented above, a notion of constitutive rule of the form "ϕ counts as ψ in the institutional context x" can be defined in the logic AL. We conceive a constitutive rule as a material implication of the form ϕ → ψ in the scope of an operator [x]. Thus, "ϕ counts as ψ in the institutional context x" only if every group of members of institution x accepts that ϕ entails ψ. Furthermore, we suppose that a constitutive rule is intrinsically contextual, which means that the rule is not universally valid while it is accepted by the members of a certain institution. More precisely, we exclude situations in which [Univ ] (ϕ → ψ) is true (i.e. situations in which it is universally accepted that ϕ entails ψ).

In this perspective, "counts-as" statements with respect to a certain institutional context x do not just express that the members of institution x classify ϕ as ψ in virtue of their acceptances, but also that this classification is proper to the institution, i.e. it is not universally accepted that ϕ entails ψ. (See [START_REF] Grossi | Classificatory aspects of counts-as: An analysis in modal logic[END_REF] for a similar perspective.) In this sense, the notion of "counts-as" presented here is aimed at capturing the proper meaning of the term "constitutive rule", that is, a rule which constitutes something new within the context of an institution.

Thus, for every x ∈ INST the following abbreviation is given:

ϕ x ψ def = [x] (ϕ → ψ) ∧ ¬ [Univ ] (ϕ → ψ)
where ϕ

x ψ stands for "ϕ counts as ψ in the institutional context x".

Example 7. Let consider the institutional context of gestural language. There exists a constitutive rule in this language according to which, the nodding gesture counts as an endorsement of what the speaker is suggesting, i.e. nodding gesture yes. This means that every group of speakers using gestural language accepts that making the nodding gesture entails endorsing what the speaker is suggesting, i.e. [gesture] (nodding → yes), and there are members of other institutions (e.g. different cultural contexts in which the same gesture does not express the same fact) who do not accept this, i.e. ¬ [Univ ] (nodding → yes).

Note that a stronger version of the concept of constitutive rule could be given by supposing that "ϕ counts as ψ in the institutional context x" if and only if ϕ entails ψ within the institutional context x, i.e. [x] (ϕ → ψ), and for every institution y, if y = x then it is not the case that ϕ entails ψ within the institutional context y, i.e. y∈INST ,y =x ¬ [y] (ϕ → ψ). The latter condition implies the condition ¬ [Univ ] (ϕ → ψ) in the definition of the "counts-as" conditional ϕ

x ψ. This stronger version of the concept of constitutive rule is not analyzed in the present paper.

The following two theorems highlight some valid and invalid properties of "countsas" operators of the form x . Similar properties of "counts-as" have been isolated in [START_REF] Jones | A formal characterization of institutionalised power[END_REF] and [START_REF] Grossi | Classificatory aspects of counts-as: An analysis in modal logic[END_REF].

The invalidities 8a-8e show that operators x do not satisfy reflexivity (invalidity 8a), transitivity (invalidity 8b), strengthening of the antecedent (invalidity 8c), weakening of the consequent (invalidity 8d) and cautious monotonicity (invalidity 8e).

On the contrary, operators

x satisfy the properties of right logical equivalence (Theorem 9a), left logical equivalence (Theorem 9b), conjunction of the consequents (Theorem 9c), disjunction of the antecedents (Theorem 9d), cumulative transitivity (Theorem 9e).

Theorem 8. AL ϕ x ϕ (8a) AL ((ϕ 1 x ϕ 2 ) ∧ (ϕ 2 x ϕ 3 )) → (ϕ 1 x ϕ 3 ) (8b) AL (ϕ 1 x ϕ 2 ) → ((ϕ 1 ∧ ϕ 3 ) x ϕ 2 ) (8c) AL (ϕ 1 x ϕ 2 ) → (ϕ 1 x (ϕ 2 ∨ ϕ 3 )) (8d) AL ((ϕ 1 x ϕ 2 ) ∧ (ϕ 1 x ϕ 3 )) → ((ϕ 1 ∧ ϕ 2 ) x ϕ 3 ) (8e) Theorem 9. For every x ∈ INST : From AL (ϕ 2 ↔ ϕ 3 ) infer AL (ϕ 1 x ϕ 2 ) ↔ (ϕ 1 x ϕ 3 ) (9a) From AL (ϕ 1 ↔ ϕ 3 ) infer AL (ϕ 1 x ϕ 2 ) ↔ (ϕ 3 x ϕ 2 ) (9b) AL ((ϕ 1 x ϕ 2 ) ∧ (ϕ 1 x ϕ 3 )) → (ϕ 1 x (ϕ 2 ∧ ϕ 3 )) (9c) AL ((ϕ 1 x ϕ 2 ) ∧ (ϕ 3 x ϕ 2 )) → ((ϕ 1 ∨ ϕ 3 ) x ϕ 2 ) (9d) AL ((ϕ 1 x ϕ 2 ) ∧ ((ϕ 1 ∧ ϕ 2 ) x ϕ 3 )) → (ϕ 1 x ϕ 3 ) (9e)
The invalidities 8a-8e are due to the local nature of the "counts-as" conditional ϕ x ψ. For instance, the fact that ϕ 1 x ϕ 2 and ϕ 2 x ϕ 3 are constitutive rules of the institution x does not necessarily entail that ϕ 1 x ϕ 3 is a constitutive rule of x since it does not necessarily entail ¬ [Univ ] (ϕ 1 → ϕ 3 ). This is the reason why x fails to satisfy transitivity.

Example 8. In the US state of Texas, "to commit a murder counts as to be punishable by the Death Penalty", and "to be punishable by the Death Penalty counts as to be liable to indictment". As the Death Penalty is not universally accepted in all institutions, both these rules are constitutive rules of Texas, i.e. murder

Texas

DeathPenalty and

DeathPenalty

Texas indictable. From this, it does not follow that it is a constitutive rule of Texas that "to commit a murder counts as to be liable to indictment". Indeed,

¬(murder

Texas

indictable) is true. This is due to the fact that "to commit a murder counts as to be liable to indictment" in all countries and institutions, and it is not constitutive of Texas, i.e. [Univ ] (murder → indictable).

Similarly,

x fails to satisfy reflexivity. Indeed, all agents in all possible institutions accept the tautology ϕ → ϕ so that "ϕ counts as ϕ" cannot be intrinsically contextual with respect to a certain institution. For similar reasons, strengthening of the antecedent is not a valid property of the operator x . 3 The following example clarifies this aspect.

Example 9. It is an accepted custom in the US that a person must leave a tip to the waiter that served him/her at a restaurant. That is, it is a constitutive rule of US that "not leaving a tip to the waiter counts as a violation", i.e. ¬leaveTip US viol . From this, it does not follow that it is a constitutive rule of US that "not leaving a tip to the waiter and not paying the bill counts as a violation". Indeed, ¬((¬leaveTip ∧ ¬payBill ) US viol ) is true. This is because "not leaving a tip and not paying the bill counts as a violation" in all countries and institutions, and it is not constitutive of US, i.e. [Univ ] ((¬leaveTip ∧ ¬payBill ) → viol ).

Discussion

The formal analysis of "counts-as" presented in this section is in agreement with the formal analysis of "counts-as" proposed in [START_REF] Grossi | Classificatory aspects of counts-as: An analysis in modal logic[END_REF], where a notion of proper classificatory rule is introduced. A proper classificatory rule is represented by the construction ϕ ⇒ cl+ x ψ which is meant to stand for "ϕ counts as ψ in the normative system x". Proper classificatory rules are distinguished by Grossi et al. from (non-proper) classificatory rules of type ϕ ⇒ cl x ψ. In a way similar to our concept of constitutive rule, proper classificatory rules have the specific property of not being universally valid (i.e. valid in all institutional contexts). That is, differently from nonproper classificatory rules, proper classificatory rules are rules which would not hold without the normative system/institution stating them. 4Non-proper classificatory rules could be expressed in our logical framework by constructions of the form [x] (ϕ → ψ), that is, by removing the condition ¬ [Univ ] (ϕ → ψ) from the definition of ϕ x ψ. In agreement with Grossi et al., we would be able to prove that, differently from constitutive rules of the form ϕ x ψ, such a kind of rules satisfy reflexivity, transitivity, strengthening of the antecedent, weakening of the consequent, and cautious monotonicity. Indeed, the following formulas are all theorems of our logic AL:

Theorem 10. AL [x] (ϕ → ϕ) (10a) AL ([x] (ϕ 1 → ϕ 2 ) ∧ [x] (ϕ 2 → ϕ 3 )) → [x] (ϕ 1 → ϕ 3 ) (10b) AL [x] (ϕ 1 → ϕ 2 ) → [x] ((ϕ 1 ∧ ϕ 3 ) → ϕ 2 ) (10c) AL [x] (ϕ 1 → ϕ 2 ) → [x] (ϕ 1 → (ϕ 2 ∨ ϕ 3 )) (10d) AL ([x] (ϕ 1 → ϕ 2 ) ∧ [x] (ϕ 1 → ϕ 3 )) → [x] ((ϕ 1 ∧ ϕ 2 ) → ϕ 3 ) (10e)
In Section 8.1 a more elaborate and detailed analysis of the logic presented in [START_REF] Grossi | Classificatory aspects of counts-as: An analysis in modal logic[END_REF] will be provided and its formal relationships with our logic of acceptance will be studied.

Another important aspect to be discussed about our formalization of "counts-as" is the problem of contraposition. Indeed, at the present stage, ϕ x ψ is logically equivalent to ¬ψ x ¬ϕ which can be counterintuitive in some situations. However, the problem of contraposition could be solved by distinguishing in the language of the logic AL formulas denoting "brute" physical facts from formulas denoting institutional facts and by imposing that the consequent ψ of a "counts-as" conditional ϕ x ψ is always a formula denoting an institutional fact. Under this assumption, if the negation of the antecedent in the "counts-as" conditional is not an institutional fact (i.e. formula ¬ϕ does not denote an institutional fact), contraposition is not allowed. That is, ϕ x ψ does not imply ¬ψ x ¬ϕ.5 It is worth noting that, this distinction between formulas denoting "brute" physical facts and formulas denoting institutional facts would enable us to account for an aspect of "counts-as" that our current formalization is not able to capture, namely: the function of "counts-as" statements of establishing the relations between physical facts and objects on the one hand (the antecedent of the "counts-as"), and institutional facts and objects on the other hand (the consequent of the "counts-as"), e.g. a certain piece of paper counts as a five-euro bill.

Regulative rules

Constitutive rules as defined in the previous Section 6.1 are still not sufficient for a characterization of institutional reality. An institution is indeed connected to a deontic dimension that up to now is still missing in our analysis. This deontic dimension consists in several concepts such as obligation, permission, prohibition, etc. which are aimed at regulating agents' behaviors and social interactions within the context of the institution.

In order to capture this deontic dimension of institutions, our logic AL can be appropriately extended by introducing a violation atom viol as in Anderson's reduction of deontic logic to alethic logic [Anderson, 1958] and in dynamic deontic logic [Meyer, 1988]. A similar approach has been recently taken in [Grossi, 2008]. By means of the new formal construct viol we can specify the concepts of obligation and that of permission in a way that respects their being also a kind of attitude-dependent facts holding in a specific institutional context.

As far as obligations are concerned, we introduce operators of the form O x which are used to specify what is obligatory in the context of a certain institution x:

O x ϕ def = ¬ϕ x viol
According to this definition, "ϕ is obligatory within the institutional context x" if and only if "¬ϕ counts as a violation within the institutional context x".

Example 10. The formula (driveCar ∧ RightSide) UK viol which is equivalent to O UK (driveCar → ¬RightSide) expresses that in the UK it is obligatory to drive on the left side of the street (i.e. "driving a car on the right side of the street counts as violation in UK").

As the following theorem highlights, our O x operators satisfy axiom K (Theorem 11a) and do not allow obligations about tautologies (Theorem 11b).

Theorem 11. For every x ∈ INST :

AL O x (ϕ → ψ) → (O x ϕ → O x ψ) (11a) AL ¬O x (11b)
On the contrary, obligation operators do not satisfy the necessitation rule. This is due to the negative condition ¬ [Univ ] (¬ϕ → viol ) in the definition of O x ϕ. Indeed, in order to have a normal modal operator for obligation, it is sufficient to remove the negative condition ¬ [Univ ] (ϕ → ψ) from the definition of the "counts-as" conditional ϕ x ψ given in Section 6.1. The following theorem highlights other interesting invalidities of the obligation operators O x .

Theorem 12.

AL ¬O x ⊥ (12a) AL O x ϕ → O x (ϕ ∨ ψ) (12b) AL O x (ϕ ∧ ψ) → O x ϕ (12c)
According to the invalidity 12a, obligation operators do not satisfy the axiom D of Standard Deontic Logic (SDL) [ Åqvist, 2002]. For instance, in the logic AL institutions might be empty, that is, for every C ∈ 2 AGT , A C :x ⊥. If institution x is empty, it does not have any obligation (i.e. O x ⊥). According to the other two invalidities we have that: if ϕ is obligatory within the context of institution x then, it is not necessarily the case that ϕ or ψ is obligatory within the context of the same institution (invalidity 12b) and if ϕ and ψ are obligatory within the context of institution x then, it is not necessarily the case that ϕ is obligatory within the context of the same institution (invalidity 12c). Thus, our obligation operators O x do not incur two classical problems of Standard Deontic Logic which are commonly referred to as "Ross paradox" and "Good Samaritan paradox" [START_REF] Carmo | Deontic logic and contraryto-duties[END_REF]. On the one hand, it seems rather odd to say that the obligation to mail a certain letter entails an obligation to mail the letter or to burn it which can be fulfilled simply by burning the letter (something presumably forbidden) ("Ross paradox"). On the other hand, it seems rather odd to say that if it is obligatory that Mary helps John who has had an accident, then it is obligatory that John has an accident ("Good Samaritan paradox"). Here we do not consider other well-known paradoxes of deontic logic (such as Chisholm paradox for instance) which require an elaborate and detailed analysis of contrary-to-duty obligations and defeasible conditional obligations (on this see [START_REF] Prakken | Dyadic deontic logic and contrary-to-duty obligations[END_REF], Makinson, 1993, Hansen et al., 2007] for instance). Indeed, this issue goes beyond the objectives of the present work.

As far as permissions are concerned we say that "ϕ is permitted within the institutional context x" (noted P x ϕ) if and only if ¬ϕ is not obligatory within the institutional context x. Formally:

P x ϕ def = ¬O x ¬ϕ
That is, we define the permission operator in the standard way as the dual of the obligation operator. 6Before concluding this section, it is important to stress again that in our approach regulative rules of type O x ϕ and P x ϕ as well as constitutive rules of type ϕ x ψ of a certain institution are attitude-dependent facts which are grounded on the acceptances of the members of a certain institution.

Towards legal institutions

In Section 5 we have supposed that ϕ is true within the context of institution x if and only if all members of this institution accept ϕ to be true. At this point, it might be objected that there are facts which are true in an institutional context but only "special" members of the institution are aware of them. For instance, there are laws in every country that are known only by the specialists of the domain (lawyers, judges, members of the Parliament, etc.). Aren't these facts true notwithstanding that many members of the institution are not aware of them?

In order to resist to this objection recall that until now our model applied to the basic informal institutions of a society, that is, rule-governed social practices [Tuomela, 2002] in which no member with "special" powers is introduced.

It is a peculiar property of informal institutions to be based on general consensus [Coleman, 1990], that is, a certain fact ϕ is true within the context of an informal institution x if and only if all members of x accept ϕ to be true. Relative to this restriction, the assumption made in Section 5 is justified because, with respect to informal institutions, there are no specialized agents called legislators empowered to change the institution itself on behalf of everybody else. For instance, in the informal institution of common language, nobody has the power to change the rules for promising. (See [Searle, 1969] for more details.) On the contrary, it is a specificity of legal (formal) institutions to have such specialized agents with special powers to interpret and modify the institution itself. This distinction between informal and formal (legal) institutions has been stressed by many authors working in the field of social and legal theory [Castelfranchi, 2003, North, 1990, Lorini and Longin, 2008[START_REF] Wright | [END_REF]. Consider for instance the following quotation from Von Wright where the terms prescription and custom respectively correspond to the terms formal institution and informal institution used here: "(...) Prescriptions are given or issued by someone. They 'flow' from or have their 'source' in the will of norm-giver (...) Customs, first of all, are not given by any authority to subjects. If we can speak of an authority behind the customs at all this authority would be the community itself" [Von Wright, 1963, p. 7-9].

In the rest of this section we will show how the logic AL can be appropriately refined in order to move beyond informal institutions and to capture some essential properties of formal (legal) institutions in which legislators are introduced. We will discuss some general principles which seem adequate for a formal characterization of legal institutions. For the sake of simplicity and readability of the article, these principles will not be included in the axiomatization of the logic AL and their semantic counterparts will not be studied.

In order to distinguish formal from informal institutions, we introduce a total function Leg which assigns a (possibly empty) set of agents to every institution x:

Leg : INST -→ 2 AGT
Leg(x) denotes the set of legislators of institution x, that is, the set of agents legally responsible over institution x and which are entitled to modify its structure. The function Leg allows distinguishing formal from informal institutions in a simple way. It is indeed reasonable to suppose that informal institutions are those institutions that do not have legislators, that is, x is an informal institution if and only if Leg(x) = ∅. On the contrary, if Leg(x) = ∅, x is a legal or formal institution. In this sense, the cardinality of Leg(x) provides an important property: it allows us to distinguish between legal institutions and informal institutions.

It seems reasonable to suppose that the legislators of a certain legal institution x must function together as members of institution x. This assumption is expressed by the following principle. For any x ∈ INST such that Leg(x) = ∅: ¬A Leg(x):x ⊥ As emphasized in Section 5, legislators are "special" agents who have the power to affect the acceptances of the other members of the institution. In legal institutions, all facts that are accepted by the legislators must be universally accepted by all members of the institution. In this perspective, legal institutions are characterized by the following principle which explains how the collective acceptance of a set C of members of institution x is affected by the acceptance of the legislators of the institution. For every C ∈ 2 AGT and x ∈ INST such that Leg(x) = ∅:

A C :x ( i∈Leg(x ) A i:x ϕ → ϕ) (Legislators)
According to Legislators, for every group of agents C , while functioning together as members of the institution x , the agents in C accept that if the legislators of x accept that ϕ, then ϕ is the case. As emphasized in Section 4.1, the Principle Legislators can be conceived as an additional specification of how collective acceptances of groups of agents are built within the context of an institution. It is worth noting that Legislators is perfectly compatible with the general principle of unanimity of the logic AL described by Axiom Unanim (and the related Theorems 3e, 3f). Indeed, we can reasonably suppose that the members of an institution might accept certain things on the basis of a criterion of unanimity and, at the same time, accept what the legislators accept and decide. 7 We conclude by showing how the concept of institutional truth proposed in Section 5 can be appropriately refined in order to deal with legal institutions. Differently from informal institutions, legal institutions do not necessarily depend on the general consensus of all their members. More precisely, if a certain fact ϕ is true within the context of the legal institution x then, it is not necessarily the case that for every set of agents C , the agents in C accept ϕ while functioning together as members of the legal institution x. In a legal institution it is sufficient that the legislators accept ϕ to be true to make it true for the institution. This means that the notion of institutional truth for legal institutions should be defined as follows. For any x ∈ INST such that Leg(x) = ∅:

[x] L ϕ def = A Leg(x):x ϕ
This means that "within the context of the legal institution x it is the case that ϕ" if and only if "the legislators of institution x accept that ϕ".

From the principles of AL and the definition of the function Leg(), it follows that the operators [x]

L are also normal. Moreover, differently from the [x] operators, which adequately characterize the notion of institutional truth for informal institutions,

L operators satisfy axioms 4 and 5 of modal logic, that is: if the legislators of institution x accept ϕ then, they accept that they accept ϕ (Theorem 13c); if the legislators of an institution x do not accept ϕ, then they accept that they do not accept ϕ (Theorem 13d). 8

Theorem 13. For every x ∈ INST :

AL [x] L (ϕ → ψ) → ([x] L ϕ → [x] L ψ) (13a) From AL ϕ infer AL [x] L ϕ (13b) AL [x] L ϕ → [x] L [x] L ϕ (13c) AL ¬ [x] L ϕ → [x] L ¬ [x] L ϕ (13d)
It is worth noting that the analysis of constitutive rules and regulative rules proposed in Sections 6.1 and 6.2 could be refined in the light of this distinction between informal and legal institutions. In particular, a new form of "counts-as" and two related concepts of obligation and permission could be defined in terms of the previous operator

[x] L .
This is in order to characterize a notion of constitutive rule and a notion of regulative rule which apply straightforwardly to the context of legal institutions, and which go beyond the notions of constitutive rule and regulative rule for informal institutions given in Sections 6.1 and 6.2 and based on the operator [x]. We postpone this kind of analysis to future works.

7 Note that a further principle which seems reasonable for legal institutions is a majority principle for legislators: the legislators of a certain legal institution x accept that if the majority of them accept ϕ, then ϕ is true. This should be conceived as a particular case of the majority principle discussed in Section 4.1. Formally, for any

x ∈ INST such that Leg(x) = ∅, if B ⊆ Leg(x ) and |Leg(x ) \ B | < |B | (i.e. B
represents the majority of the legislators of the institution x ) then: A Leg(x):x ( i∈B A i:x ϕ → ϕ).

8 Note that the operator [x] is stronger than the operator

[x] L , that is, [x] ϕ implies [x] L ϕ.
8 Comparison with other logical approaches to normative systems

In the following two sections our logic AL will be compared with two approaches to normative systems and institutions which have been recently proposed in the multiagent system domain.

Embedding Grossi et al.'s logic of "counts-as" into AL

Because of the interesting formal similarities, we will first compare AL with the modal logic of normative systems proposed in [START_REF] Grossi | Classificatory aspects of counts-as: An analysis in modal logic[END_REF], henceforth abbreviated GMD logic.

In the GMD logic a set of contexts CXT denoting normative systems is introduced. GMD logic is based on a set of modal operators [[x]] (one for every context x in CXT ). Operators [[x]] are similar to our operators [x] defined in Section 5.9 A formula [[x]] ϕ approximately stands for "in the institutional context/normative system x it is the case that ϕ". It is supposed that CXT contains a special context Univ , where the operator [[Univ ]] is used for denoting facts which universally hold. We note CXT 0 = CXT \ {Univ }. The language of the GMD logic is given by the following BNF:

ϕ ::= ⊥ | p | ¬ϕ | ϕ ∨ ϕ | [[x]] ϕ
where p ranges over ATM and x ranges over CXT . ∧, →, ↔ and are defined from ∨, ¬ and ⊥ in the usual manner.

As noted in Section 6.1, operators [ The most striking difference between our logic of acceptance AL and the GMD logic is that in the logic AL the contextual operators [x] are built on the notion of collective acceptance, whereas in the GMD logic the contextual operators [[x]] are given as primitive operators.

Frames of the GMD logic are called multi-context frames. A multi-context frame has the following form:

F GMD = S , {S x } x∈CXT 0 where:
• S is a set of possible worlds;

• {S x } x∈CXT 0 is a family of subsets of S , one for every institutional context x ∈ CXT 0 .

A multi-context model is a tuple M GMD = F GMD , π where:

• F GMD is a multi-context frame;

• π : ATM → 2 S is a valuation function associating a set of possible worlds π(p) ⊆ S to each atomic formula p of ATM .

The truth conditions for formulas of the GMD logic are just standard for contradiction, atomic propositions, negation and disjunction. The following are the truth conditions for

[[x ]] ϕ and [[Univ ]] ϕ. • M GMD , w |= [[x ]] ϕ iff M, w |= ϕ for all w ∈ S x ; • M GMD , w |= [[Univ ]] ϕ iff M, w |= ϕ for all w ∈ S . A formula ϕ is true in a GMD model M GMD iff M GMD , w |= ϕ for every world w in M GMD . ϕ is GMD valid (noted |= GMD ϕ) if and only if ϕ is true in all GMD models. ϕ is GMD satisfiable iff ¬ϕ is not GMD valid.
The GMD logic is axiomatized by the following principles, where x and y denote elements of the set CXT 0 : All principles of propositional calculus (ProTau)

[[x]] (ϕ → ψ) → ([[x]] ϕ → [[x]] ψ) (K [[x]] ) [[Univ ]] (ϕ → ψ) → ([[Univ ]] ϕ → [[Univ ]] ψ) (K [[Univ ]] ) [[x]] ϕ → [[y]] [[x]] ϕ (4 [[x]],[[y]] ) ¬ [[x]] ϕ → [[y]] ¬ [[x]] ϕ (5 [[x]],[[y]] ) [[Univ ]] ϕ → [[Univ ]] [[Univ ]] ϕ (4 [[Univ ]] ) ¬ [[Univ ]] ϕ → [[Univ ]] ¬ [[Univ ]] ϕ (5 [[Univ ]] ) [[Univ ]] ϕ → ϕ (T [[Univ ]] ) [[Univ ]] ϕ → [[x]] ϕ (⊆ [[Univ ]],[[x]] ) From ϕ and ϕ → ψ infer ψ (MP) From ϕ infer [[x]] ψ (Nec [[x]] ) From ϕ infer [[Univ ]] ψ (Nec [[Univ ]] ) We write GMD ϕ if formula ϕ is a theorem of GMD. Axiom K [[x]] and Rule Nec [[x]] express that the operators [[x]] are normal modal oper- ators. Axioms K [[Univ ]] , 4 [[Univ ]] , 5 [[Univ ]] , T [[Univ ]
] and the rule of inference Nec [[Univ ]] express that the universal modality [[Univ ]] is defined in the modal logic system S5. According to the Axioms 4

[[x]],[[y]] and 5 [[x]],[[y]]
, truth and falsehood in institutional contexts/normative systems are absolute because they remain invariant even if they are evaluated from another institutional context/normative system. This means that every normative system y has full access to all facts which are true in a different normative system x. In our view, these two principles are criticizable because they rely on a strong assumption of perfect information, i.e. a normative system has perfect information about the facts that are true in the other normative systems. Axiom ⊆ [[Univ ]], [[x]] expresses the relationship between the universal modality and the contextual modalities.

In [Grossi, 2007] it is proved that the GMD logic is sound and complete with respect to the class of GMD frames.

It is easy to show that the principles of the acceptance logic AL given in Section 3 are not sufficient to derive the principles of the GMD logic. In particular, Axioms

4 [[x]],[[y]] , 5 [[x]],[[y]] , 4 [[Univ ]] , 5 [[Univ ]] and T [[Univ ]] are not derivable in AL.
In order to embed GMD we need to slightly modify the properties of the logic AL. On the one hand, we need to generalize Axioms PAccess and NAccess by supposing that they also hold for the case B ⊆ C. This is in order to infer the formulas

[x] ϕ → [y] [x] ϕ and ¬ [x] ϕ → [y] ¬ [x]
ϕ in the augmented logic AL. Thus, we need to assume that, given two arbitrary sets of agents B and C , the agents in B have access to all facts that the agents in C accept (do not accept), while functioning together as members of a certain institution x. On the other hand, we need to add the principle [Univ ] ϕ → ϕ to the logic AL. The way to embed the GMD logic into our logic AL is illustrated in the following paragraph.

An embedding of GMD logic. Let us slightly modify the logic of acceptance AL in order to provide a correct embedding of GMD. We call AL + the modified logic of acceptance.

AL + has the same language as AL (see Section 3.1). AL + frames are tuples F = W , A where W and A are defined as for AL frames, except that the constraints S.1 and S.2 given in Section 3.2 are supposed to hold also for the case B ⊆ C and the following additional constraint S.6 is imposed. That is, for any world w ∈ W , institutional context x ∈ INST , and sets of agents C , B ∈ 2 AGT we suppose:

if w ∈ A B:y (w ) then A C :x (w ) ⊆ A C :x (w ) (S.1') if w ∈ A B:y (w ) then A C :x (w ) ⊆ A C :x (w ) (S.2')
Furthermore, for any world w ∈ W we suppose:

∃C ∈ 2 AGT , ∃x ∈ INST such that w ∈ A C :x (w ) (S.6)
The axiomatization of AL + is given by the axiom schemes and rules of inference of AL, except that an Axiom corresponding to the Axiom T [[Univ ]] of the GMD logic is added, and the Axioms PAccess and NAccess of the logic AL are generalized in such a way that they also for hold for the case B ⊆ C. That is, for any sets of agents C , B ∈ 2 AGT , we suppose:

A C :x ϕ → A B:y A C :x ϕ (PAccess + ) A C :x ϕ → A B:y ¬A C :x ϕ (NAccess + )
Furthermore, we suppose:

[Univ ] ϕ → ϕ (T Univ ) Axioms PAccess + and NAccess + respectively correspond to the semantic constraints S.1' and S.2', whilst Axiom T Univ corresponds to the semantic constraint S.6.

The definitions of validity and satisfiability in AL + are given accordingly. We write |= AL + ϕ if formula ϕ is valid in all AL + models satisfying the semantic constraints S.3, S.4, S.5 given in Section 3.2 and the constraints S.1', S.2', S.6 given here. We call AL + the logic axiomatized by Axiom T Univ and the principles of the logic AL (Section 3.4), where Axioms PAccess and NAccess are generalized to PAccess + and NAccess + . We write AL + ϕ if formula ϕ is a theorem of AL + .

We can prove that AL + as well is sound and complete. More precisely:

Theorem 14. AL + ϕ if and only if |= AL + ϕ.

Consider the following translation tr from GMD to the new logic AL + :

• tr(⊥) = ⊥ • tr(p) = p • tr(¬ϕ) = ¬tr(ϕ) • tr(ϕ ∨ ψ) = tr(ϕ) ∨ tr(ψ) • tr([[x]] ϕ) = [x] tr(ϕ) • tr([[Univ ]] ϕ) = [Univ ] tr(ϕ),
As the following Theorem 15 shows, tr is a correct embedding of the GMD logic. L ϕ, after defining

[Univ ] L ϕ def = x∈INST [x] L ϕ.
To obtain a correct embedding of the GMD logic, it is sufficient to add to AL the three axioms

[x] L ϕ → [y] L [x] L ϕ, ¬ [x] L ϕ → [y] L ¬ [x] L ϕ

A conceptual comparison with Boella & van der Torre's model

The formal approach to institutions and normative systems proposed by Boella & van der Torre [Boella and van der Torre, 2004a[START_REF] Boella | Regulative and constitutive norms in normative multiagent systems[END_REF], 2007] is similar in some respect to ours. Here we just provide a conceptual comparison between the two approaches. We are not able to provide a more technical comparison. Indeed, our formalism based on modal logic and their formalism based on input-output logic [Makinson and van der Torre, 2000] are too different to be compared in the fashion followed in Section 8.1.

Boella & van der Torre emphasize the relevance of the concept of acceptance for a formal model of institutions. In their model, individual agents accept a norm, together with its associated sanctions and rewards, when they recognize that this norm serves to achieve their desires and believe that the other agents will conform to it. According to them, for a norm to be really effective it must be respected due to its acceptance, and not only to the fear of sanctions. Although they take the concept of acceptance into consideration, they do not analyze it in detail. In particular, in their model there is no distinction between individual acceptance and collective acceptance. On the contrary, this distinction is fundamental in our AL logic in which we clarify the relationships between individual acceptances and collective acceptances and we provide an explanation of how the collective acceptance of a group of agents C is built from the individual acceptances of the agents in C .

Moreover, in Boella & van der Torre's approach, normative systems and institutions are conceived as agents and mental attitudes such as beliefs and goals are ascribed to them. Differently from them, we do not claim that institutions can be conceived as agents. In our approach, we only defend the idea that the institutional reality is built on the top of the agents' attitudes. In particular, we claim that institutions are grounded on the individual and collective acceptances of their members and groups of members, and their dynamics depend on the dynamics of these acceptances.

Conclusion

We have presented in this article a logic of acceptance and applied it to the analysis of institutions. Our logic of acceptance allows to express that agents accept something to be true qua members of a certain institution. Given the properties of this demystified notion of acceptance, we have provided an analysis of the kind of attitude-dependent facts which are typical of institutions. We have formalized the concept of constitutive rule expressed by statements of the form "X counts as Y in the context of institution x". Then, we have introduced a notion of obligation and a notion permission with respect to an institutional context (i.e. so-called regulative rules). While constitutive rules and regulative rules are usually defined from the external perspective of a normative system or institution, in the present work we have anchored these rules in the agents' acceptances.

Directions for future research are manifold. For instance, future works will be devoted to integrate modalities expressing agents' goals and preferences, such as the ones provided in [START_REF] Cohen | Intention is choice with commitment[END_REF], into the logical framework presented in this paper. This is in order to investigate the decision to join (resp. not to join) a given institution and the related decision to accept (resp. not to accept) the norms of the institution with its associated sanctions and rewards. These kinds of decisions are indeed influenced by the inconsistency between the agent's goals and the current norms and rules of the institution. For instance, if the agent's goals conflict with the norms proclaimed by the legislators then, the agent will probably decide not to join the institution.

Another interesting topic to be investigated in future works is the dynamics of individual and collective acceptances in institutional contexts. We have already started to study this topic in a recent work [START_REF] Herzig | What do we accept after an announcement[END_REF]. The idea is to extend the logic of acceptance AL by events of type x !ϕ and corresponding dynamic operators of the form [x !ϕ]. A formula [x !ϕ]ψ, means that ψ is true after every announcement of formula ϕ in the context of institution x . Operators of type [x !ϕ], which are similar to the operators of announcements in dynamic epistemic logic [START_REF] Baltag | The logic of public announcements, common knowledge and private suspicions[END_REF], Gerbrandy and Groeneveld, 1997, van Ditmarsch et al., 2007], express that the members of an institution x learn that ϕ is true in that institution in such a way that their acceptances, qua members of institution x, are updated. Such operators can also be used to describe how the acceptances of the members of institution x change, after that a certain norm (e.g. obligation, permission) is issued or promulgated within the context of this institution.

A Annex: proofs of some theorems This Annex contains some selected proofs of the theorems presented in the paper.

Proof of Theorem 1

Axiom K and rule of inference Nec define a minimal normal modal logic. Thus, they do not have an associated semantic constraint. It is a routine task to check that the Axioms PAccess, NAccess, Inc, Unanim and Mon of the logic AL correspond to their semantic counterparts S.1-S.5 over AL models. In particular, the following correspondences exist between the axioms of the logic AL and the semantic constraints over AL frames.

• Axioms PAccess corresponds to the constraint S.1.

• Axiom NAccess corresponds to the constraint S.2.

• Axiom Inc corresponds to the constraint S.3.

• Axiom Unanim corresponds to the constraint S.4.

• Axiom Mon corresponds to the constraint S.5.

It is a routine, too, to check that all of axioms of the logic AL are in the Sahlqvist class, for which a general completeness result exists. (See [Sahlqvist, 1975, Blackburn et al., 2001].)

Proof of Theorem 2

For notational convenience, we will use the following abbreviation in the proof:

A C :x ϕ def = ¬A C :x ¬ϕ
We have to prove that if ϕ is AL satisfiable then it is satisfiable in a finite AL model.

Suppose that M = W , A , V is a AL model which satisfies ϕ. Our aim is to build a finite AL model which satisfies ϕ. To do this, we use a filtration method [START_REF] Blackburn | Modal Logic[END_REF], Goldblatt, 1992].

Let us introduce the following definition.

Definition 1. A set of formulas Σ is closed under subformulas (cus) if for all formulas ϕ, ϕ : if ϕ ∨ ϕ ∈ Σ then so are ϕ and ϕ ; if ¬ϕ ∈ Σ then so is ϕ; for any

x ∈ INST and C ∈ 2 AGT if A C :x ϕ ∈ Σ then ϕ ∈ Σ.
Let us now consider an arbitrary finite set of formulas Σ ϕ which is closed under subformulas and which contains ϕ. From Σ ϕ we define the set Σ + ϕ as follows. Σ + ϕ is defined as the smallest superset of Σ ϕ such that:

1. for all x, y ∈ INST and

C , B ∈ 2 AGT , if A C :x ϕ ∈ Σ + ϕ then A B:y ϕ ∈ Σ + ϕ ; 2. for all x ∈ INST and C ∈ 2 AGT , if A C :x ϕ ∈ Σ + ϕ then ¬A C :x ϕ ∈ Σ + ϕ ; 3. for all x ∈ INST and C ∈ 2 AGT , A C :x ⊥ ∈ Σ + ϕ ; 4. ⊥ ∈ Σ + ϕ .
The following proposition follows straightforwardly due to the fact that the sets AGT and INST are supposed to be finite.

Proposition 3. Σ +

ϕ is finite and closed under subformulas. We define the relation between the worlds in W of the model M. For every two worlds w, v ∈ W :

• w v iff for all ϕ ∈ Σ + ϕ , M, w |= ϕ iff M, v |= ϕ.
For every world w ∈ W , we note |w| the equivalence class of world w of M with respect to . Moreover, let

W Σ + ϕ = {|w| | w ∈ W }. Now, we have to build a filtrated model M f = W f , A f , V f of the model M.
Definition 2. We define M f as follows.

A. W f = W Σ + ϕ ; B. for every B ∈ 2 AGT and x ∈ INST , |v| ∈ A f B:x (|w|) if and only if: 1. ∀A B:x ϕ ∈ Σ + ϕ , if M, w |= A B:x ϕ then M, v |= ϕ; 2. ∀y ∈ INST and ∀C ∈ 2 AGT , if B ⊆ C then: ∀A C :y ϕ ∈ Σ + ϕ , if M, w |= A C :y ϕ then M, v |= A C :y ϕ; 3. ∀y ∈ INST and ∀C ∈ 2 AGT , if B ⊆ C then: ∀ A C :y ϕ ∈ Σ + ϕ , if M, w |= A C :y ϕ then M, v |= A C :y ϕ; 4. ∀C ∈ 2 AGT , if B ⊆ C then: ∀A C :x ϕ, A C :x ∈ Σ + ϕ , if M, w |= A C :x ∧ A C :x ϕ then M, v |= ϕ; 5. ∃i ∈ B such that ∀A i:x ϕ ∈ Σ + ϕ , if M, v |= A i:x ϕ then M, v |= ϕ. C. V f (p) = {|w| | M, w |= p}, for all propositional atoms in Σ + ϕ . It is straightforward to prove that the model M f is indeed a filtration of M through Σ + ϕ . Lemma 1. M f is a filtration of M through Σ + ϕ .
The next step consists in proving that M f is a AL model.

Lemma 2. M f is a AL model.

Proof. We have to prove that the model M f satisfies the five semantic constraints S.1-S.5 over AL models.

Let us start with constraint S.1. We have to prove that the following condition holds in M f for any x, y ∈ INST and C , B ∈ 2 AGT such that B ⊆ C :

• if |w | ∈ A f B:x (|w|) and |w | ∈ A f C :y (|w |) then |w | ∈ A f C :y (|w|). Suppose |w | ∈ A f B:x (|w|) and w ∈ A f C :y (|w |)
, where B ⊆ C . We have to prove that |w | ∈ A f C :y (|w|). By Definition 2, the latter is equivalent to: Item 5. This item follows straightforwardly from the fact w ∈ A f C :y (|w |). This proves that S.1 holds.

1. ∀A C :y ϕ ∈ Σ + ϕ , if M, w |= A C :y ϕ then M, w |= ϕ; 2. ∀z ∈ INST and ∀D ∈ 2 AGT , if C ⊆ D then: ∀A D:z ϕ ∈ Σ + ϕ , if M, w |= A D:z ϕ then M, w |= A D:z ϕ; 3. ∀z ∈ INST and ∀D ∈ 2 AGT , if C ⊆ D then: ∀ A D:z ϕ ∈ Σ + ϕ , if M, w |= A D:z ϕ then M, w |= A D:z ϕ; 4. ∀D ∈ 2 AGT , if C ⊆ D then: ∀A D:y ϕ, A D:y ∈ Σ + ϕ , if M, w |= A D:y ∧ A D:y ϕ then M, w |= ϕ; 5. ∃i ∈ C such that ∀A i:y ϕ ∈ Σ + ϕ , if M, w |= A i:y ϕ then M, w |= ϕ.
Let us now consider constraint S.2. We have to prove that the following condition holds in M f for any x, y ∈ INST and C , B ∈ 2 AGT such that B ⊆ C :

• if |w | ∈ A f B:x (|w|) and w ∈ A f C :y (|w|) then w ∈ A f C :y (|w |). Suppose |w | ∈ A f B:x (|w|) and w ∈ A f C :y (|w|), where B ⊆ C . We have to prove that |w | ∈ A f C :y (|w |)
. By Definition 2, the latter is equivalent to:

1. ∀A C :y ϕ ∈ Σ + ϕ , if M, w |= A C :y ϕ then M, w |= ϕ; 2. ∀z ∈ INST and ∀D ∈ 2 AGT , if C ⊆ D then: ∀A D:z ϕ ∈ Σ + ϕ , if M, w |= A D:z ϕ then M, w |= A D:z ϕ; 3. ∀z ∈ INST and ∀D ∈ 2 AGT , if C ⊆ D then: ∀ A D:z ϕ ∈ Σ + ϕ , if M, w |= A D:z ϕ then M, w |= A D:z ϕ; 4. ∀D ∈ 2 AGT , if C ⊆ D then: ∀A D:y ϕ, A D:y ∈ Σ + ϕ , if M, w |= A D:y ∧ A D:y ϕ then M, w |= ϕ; 5. ∃i ∈ C such that ∀A i:y ϕ ∈ Σ + ϕ , if M, w |= A i:y ϕ then M, w |= ϕ.
So, to prove S. As a next step we have to prove the model M f satisfies the semantic condition S.3. That is, we have to prove that for any x ∈ INST and C , B ∈ 2 AGT such that B ⊆ C :

• if A f C :x (|w|) = ∅ then A f B:x (|w|) ⊆ A f C :x (|w|).
The following proposition is needed to prove that M f satisfies the condition S.3. M, w |= A B:x implies that ∃w such that w ∈ A B:x (w). As M f is a filtration of M (Lemma 1), from the latter we conclude that ∃|w | such that |w | ∈ A f B:x (|w|). This proves that S.5 holds.

Lemma 3. The model M f contains at most 2 n worlds where n denotes the size of Σ + ϕ .

Proof. From Lemma 1 and Proposition 2.38 given in [Blackburn et al., 2001, p. 79].

Lemma 4. M f is a finite model.

Proof. From Lemma 3 and Proposition 3.

Lemma 5. Formula ϕ is satisfiable in M f .

Proof. From Lemma 1 and Proposition 3, the fact that ϕ is satisfiable in M, the fact that ϕ ∈ Σ + ϕ and the Filtration Theorem given in [Blackburn et al., 2001, p. 79].

Lemma 6. The logic AL has the finite model property.

Proof. We have started with an arbitrary formula ϕ which is satisfiable in a AL model M. We have built a model M f and proved that M f is a finite AL model (Lemma 4). Finally, we have proved that ϕ is satisfiable in M f (Lemma 5). Thus, we can conclude that for every formula ϕ, if ϕ is AL satisfiable then, ϕ is satisfiable in a finite AL model.

Theorem 2 is a direct consequence of Lemma 6.

Proof of Theorem 14

As for the logic AL, it is a routine to prove soundness, whereas completeness is again obtained by Sahlqvist completeness theorem. Indeed, all axioms of AL + are in the Sahlqvist class, for which a general completeness result exists [Sahlqvist, 1975, Blackburn et al., 2001].

Proof of Theorem 15

In order to prove Theorem 15, it is sufficient to prove that if INST = CXT and ϕ is a formula of the GMD logic then: if ϕ is a theorem of GMD then tr(ϕ) is a theorem of AL + and, if ϕ is GMD satisfiable then tr(ϕ) is AL + satisfiable.

Proposition 5. Suppose that INST = CXT and ϕ is a formula of the logic GMD then: if GMD ϕ then AL + tr(ϕ).

Proof. We only need to prove that the translations of the axioms of the GMD logic are theorems of AL + and that the translated rules of inference of GMD preserves validity.

It is straightforward to show that the translation of the rules of inference Nec Proposition 6. Suppose that INST = CXT and ϕ is a formula of the logic GMD then: if ϕ is GMD satisfiable then tr(ϕ) is AL + satisfiable.

Proof. Suppose that ϕ is GMD satisfiable. Thus, there exists a GMD model M GMD = S , {S x } x∈CXT 0 , π which satisfies ϕ. We prove that we can build a AL + model M which satisfies the same formulas as M GMD .

As we have supposed INST = CXT , the AL + model M associated with the GMD model M GMD can be defined as follows.

• W = S ;

• ∀w ∈ W , ∀x ∈ CXT 0 , ∀C ∈ 2 AGT , A C :x (w) = S x ;

• ∀w ∈ W , ∀C ∈ 2 AGT , A C :Univ (w) = S ;

• ∀w ∈ W , ∀p ∈ AT M, w ∈ π(p) if and only if w ∈ V (p).

It is a routine to verify that the previous conditions ensure that the model M is indeed a AL + model. By structural induction on ϕ, it is also a routine to prove that the previous AL + model satisfies the same formulas as the GMD model it is associated. That is, M GMD , w |= ϕ if and only if M, w |= tr(ϕ).

Theorem 15 is an immediate corollary of Proposition 5 and Proposition 6.

Proof of Theorems 3, 4, 5, 6 and 7

Theorems 3 and 4 can be syntactically proved using AL logic axiomatization. Theorem 5 proof is based on Theorem 3. As every A C:x operator is normal, Theorems 6 and 7 can be proved by iteration of the Axiom (K) and the Rule of Necessitation (Nec) for every group of 2 AGT and every institution of INST . We provide in the sequel only the complete proof for Theorems (3a) and (3e).

Proof. Theorem (3a):

( 4) and ( 7)

The proof of Proposition (2b) is similar to the one of Proposition (2a), we only use Lemma (7b) instead of Lemma (7a) and (NegIntrAccept) instead of (PIntrAccept).

Proof of Theorem 8

To prove that these formulas are not valid in AL, we only have to exhibit a model where there is a world where these formulas are false. We give the complete proof only for Theorem (8b), the others are very similar.

Proof. Theorem (8b):

We will build a AL model M in which there is a world w is which the formula is false, i.e.: M, w (ϕ 1 x ϕ 2 ) ∧ (ϕ 2 x ϕ 3 ) ∧ ¬(ϕ 1 x ϕ 3 ). Let ATM = {ϕ 1 , ϕ 2 , ϕ 3 }, AGT = {i}, INST = {x, y, z} and W = {w , w x , w y , w z }. We build the valuation function V : V (ϕ 1 ) = {w y }, V (ϕ 2 ) = {w z } and V (ϕ 3 ) = {w y }, and the relation A : A {i}:x (w ) = {w x }, A {i}:y (w ) = {w y } and A {i}:z (w ) = {w z }.

As we want M to be a AL model, we ensure that it satisfies the constraints S.1-S.5.

• In order to satisfy (S.1) and (S.2) we impose: w y , w x ∈ A {i}:x , w z , w x ∈ A {i}:x , w x , w y ∈ A {i}:y , w z , w y ∈ A {i}:y , w x , w z ∈ A {i}:z and w y , w z ∈ A {i}:z ;

• as there is only one agent in our model, (S.3) and (S.5) are satisfied;

• in order to satisfy (S.4) we impose that: w x , w x ∈ A {i}:x , w y , w y ∈ A {i}:y and w z , w z ∈ A {i}:z ;

In this model M:

• M, w [x] (ϕ 1 → ϕ 2 ) ∧ [x] (ϕ 2 → ϕ 3 ) • M, w ¬ [y] (ϕ 1 → ϕ 2 )

  [x]] and [[Univ ]] are exploited in Grossi et al.'s logic to define contextual conditionals called proper classificatory rules, noted ϕ ⇒ cl+ x ψ, which are an abbreviation of [[x]] (ϕ → ψ) ∧ ¬ [[Univ ]] (ϕ → ψ) and which read "ϕ counts as ψ in the normative system x". The construction ϕ ⇒ cl+ x ψ is similar to our ϕ x ψ.

Theorem 15 .

 15 Let INST = CXT and ϕ be a formula of the GMD logic. Then, ϕ is GMD satisfiable if and only if tr(ϕ) is AL + satisfiable. REMARK. It is worth noting that GMD logic can also be embedded into the variant of AL with legislators presented in Section 7 by the translations tr([[x]] ϕ) = [x] L ϕ and tr([[Univ ]] ϕ) = [Univ ]

  and [Univ ] L ϕ → ϕ and the two corresponding semantic constraints over AL frames: if w ∈ A Leg(y):y (w ) then A Leg(x):x (w ) = A Leg(x):x (w ), and ∃x ∈ INST such that w ∈ A Leg(x):x (w ).

  So, to prove S.1 we just need to prove that the previous items 1-5 are consequences of|w | ∈ A f B:x (|w|) and |w | ∈ A f C :y (|w |) when B ⊆ C . Item 1. Suppose A C :y ϕ ∈ Σ + ϕ and M, w |= A C :y ϕ. As B ⊆ C and |w | ∈ A f B:x (|w|), it follows that M, w |= ϕ.Item 2. Take an arbitrary D such that C ⊆ D and an arbitrary z ∈ INST . As B ⊆ C , we have B ⊆ D. Suppose A D:z ϕ ∈ Σ + ϕ and M, w |= A D:z ϕ. As |w | ∈ A f B:x (|w|), it follows that M, w |= A D:z ϕ. As w ∈ A f C :y (|w |), we conclude that M, w |= A D:z ϕ. Item 3. Take an arbitrary D such that C ⊆ D and an arbitrary z ∈ INST . As B ⊆ C , we have B ⊆ D. Suppose A D:z ϕ ∈ Σ + ϕ and M, w |= A D:z ϕ. As |w | ∈ A f B:x (|w|), it follows that M, w |= A D:z ϕ. As w ∈ A f C :y (|w |), we conclude that M, w |= A D:z ϕ. Item 4. Take an arbitrary D such that C ⊆ D. As B ⊆ C , we have B ⊆ D. Suppose A D:y ϕ, A D:y ∈ Σ + ϕ and M, w |= A D:y ϕ ∧ A D:y . As |w | ∈ A f B:x (|w|), it follows that M, w |= A D:y ϕ ∧ A D:y . As w ∈ A f C :y (|w |), we conclude that M, w |= ϕ.

  2 we just need to prove that items 1-5 are consequences of |w | ∈ A f B:x (|w|) and w ∈ A f C :y (|w|). Item 1. Suppose A C :y ϕ ∈ Σ + ϕ and M, w |= A C :y ϕ. By construction of Σ + ϕ we have A C :y ¬ϕ ∈ Σ + ϕ . As |w | ∈ A f B:x (|w|) and B ⊆ C, it follows that M, w |= A C :y ϕ. As |w | ∈ A f C :y (|w|), we conclude that M, w |= ϕ. Item 2. Take an arbitrary D such that C ⊆ D and an arbitrary z ∈ INST . As B ⊆ C , we have B ⊆ D. Suppose A D:z ϕ ∈ Σ + ϕ and M, w |= A D:z ϕ. By construction of Σ + ϕ we have A D:z ¬ϕ ∈ Σ + ϕ . As |w | ∈ A f B:x (|w|) and B ⊆ D, it follows that M, w |= A D:z ϕ. As |w | ∈ A f C :y (|w|), we conclude that M, w |= A D:z ϕ. Item 3. Take an arbitrary D such that C ⊆ D and an arbitrary z ∈ INST . As B ⊆ C , we have B ⊆ D. Suppose A D:z ϕ ∈ Σ + ϕ and M, w |= A D:z ϕ. By construction of Σ + ϕ we have A D:z ¬ϕ ∈ Σ + ϕ . As |w | ∈ A f B:x (|w|) and C ⊆ D, it follows that M, w |= A D:z ϕ. As |w | ∈ A f C :y (|w|), we conclude that M, w |= A D:z ϕ. Item 4. Take an arbitrary D such that C ⊆ D. As B ⊆ C , we have B ⊆ D. Suppose A D:y ϕ, A D:y ∈ Σ + ϕ and M, w |= A D:y ϕ ∧ A D:y . By construction of Σ + ϕ we have A D:y ⊥, A D:y ¬ϕ ∈ Σ + ϕ . As |w | ∈ A f B:x (|w|) and C ⊆ D, it follows that M, w |= A D:y ϕ ∧ A D:y . As |w | ∈ A f C :y (|w|), we conclude that M, w |= ϕ. Item 5. This item follows straightforwardly from the fact w ∈ A f C :y (|w|). This proves that S.2 holds.

Proposition 4 .

 4 For every x ∈ INST and C ∈ 2 AGT , if A f C :x (|w|) = ∅ then ∃w ∈ |w| such that M, w |= A C :x .Proof. Let us suppose that A f C :x (|w|) = ∅, and M, w |= A C :x ⊥ for all w ∈ |w|. We are going to show that the two facts are inconsistent.ConditionA f C :x (|w|) = ∅ implies that ∃|w | ∈ W f such that: if A C :x ϕ ∈ Σ + ϕ then, if M, w |= A C :x ϕ then M, w |= ϕ. As we have A C :x ⊥ ∈ Σ + ϕ (by construction of Σ +ϕ ) and we have supposed M, w |= A C :x ⊥, we can infer that M, w |= ⊥.

  [[x]] , Nec[[Univ ]] and MP preserve validity. As the AL + operators [x] and [Univ ] are normal, it is a routine to verify that the translation of the GMD Axioms K[[x]] and K [[Univ ]] are theorems of AL + . Furthermore, by the definitions of [x] ϕ and [Univ ] ϕ, it is just trivial to prove that that the translation of the GMD Axiom ⊆ [[Univ ]],[[x]] is a theorem of AL + . The translation of the GMD Axiom T [[Univ ]] is a theorem of AL + as well. Indeed, this corresponds to the Axiom T Univ of the logic AL + . By Axioms PAccess + and NAccess + we can prove that the translations of the GMD Axioms 4 [[x]],[[y]] and 5 [[x]],[[y]] are theorems of AL + . By the same principles, we can prove that the translations of the GMD Axioms 4 [[Univ ]] and 5 [[Univ ]] are theorems of AL + .

  1) AL A C :x ⊥ ∨ ¬A C :x ⊥, by (ProTau) (2) AL ¬A C :x ⊥ → A C :x ¬A C :x ⊥, by (NAccess) (3) AL A C :x ⊥ → A C :x ¬A C :x ⊥, by (ProTau), (Nec) and (K) (4) AL A C :x ¬A C :x ⊥, from (1), (2) and (3) by (ProTau) (4) MB C A C :x ϕ → A C :x ϕ, from (1), (2), (3) by (ProTau) (5) A C :x ϕ → Bel i A C :x ϕ, by (PIntrAccept), for every i ∈ C (6) A C :x ϕ → E C (A C :x ϕ ∧ A C :x ϕ), from (5), by (ProTau) and definition of E C (7) A C :x ϕ → MB C A C :x ϕ, from (6) by inference rule (InductionRule) (left to right direction of Theorem (2a)) (8) A C :x ϕ ↔ MB C A C :x ϕ, from (

  and thus M, w ¬ [Univ ] (ϕ 1 → ϕ 2 ) • M, w ¬ [z] (ϕ 2 → ϕ 3 ) and thus M, w ¬ [Univ ] (ϕ 2 → ϕ 3 ) • M, w [x] (ϕ 1 → ϕ 3 ) ∧ [y] (ϕ 1 → ϕ 3 ) ∧ [z] (ϕ 1 → ϕ 3 ), i.e. M, w [Univ ] (ϕ 1 → ϕ 3 )We have built a AL model which satisfies the formula (ϕ is not valid in AL. By Theorem 1, we conclude that (ϕ1 x ϕ 2 ) ∧ (ϕ 2 x ϕ 3 ) → (ϕ 1 x ϕ 3 ) is not a theorem of AL.

  formula ϕ is true in a AL model M if and only if M, w |= ϕ for every world w in M. ϕ is AL valid (noted |= AL ϕ) if and only if ϕ is true in all AL models. ϕ is AL satisfiable if and only if ¬ϕ is not AL valid.

In Hart's theory, the rule of recognition is the rule which specifies the ultimate criteria of validity in a legal system.

A deeper discussion on this point remains out of the scope of this paper. Some interesting arguments for collective intentionality can be found in[Tollefsen, 2002].

Other authors have defended the idea that strengthening of the antecedent and transitivity should not be valid properties of "counts-as" conditionals (e.g.[START_REF] Gelati | Normative autonomy and normative co-ordination: Declarative power, representation, and mandate[END_REF]).

See[START_REF] Grossi | The many faces of counts-as: A formal analysis of constitutive rules[END_REF] for a refinement of this typology of rules.

See also[Grossi, 2008] for a different solution on how to solve the problem of contraposition in a normal modal logic of "counts-as".

We do not consider here the classical distinction between weak permission and strong permission[START_REF] Alchourrón | Normative systems[END_REF], Raz, 1975[START_REF] Wright | [END_REF]. According to legal theory, a weak permission corresponds to the absence in a normative system of a norm prohibiting ϕ (this is represented by our permission operator Px). A strong permission corresponds to the existence in the normative system of an explicit norm, issued by the legislators, according to which ϕ is permitted. For a logical analysis of the distinction between weak and strong permission see our related work[START_REF] Lorini | A logical account of institutions: from acceptances to norms via legislators[END_REF].

Here we use the notation[[x]] in order to distinguish their operators from ours.

Let us now prove that M f satisfies the condition S.3. Consider an arbitrary x ∈ INST and C , B ∈ 2 AGT such that B ⊆ C . Suppose that A f C :x (|w|) = ∅ and w ∈ A f B:x (|w|). We have to prove that w ∈ A f C :x (|w|). By Definition 2, the latter is equivalent to: So, to prove that M f satisfies the condition S.3 we just need to prove that items 1-5 are consequences of

This proves that S.3 holds. Now, we prove that the model M f satisfies the semantic condition S.4. That is, we prove that for any x ∈ INST and C ∈ 2 AGT :

We have to prove that |w | ∈ i∈C A i:x (|w |). By Definition 2, the latter is equivalent to the fact that ∃i ∈ C such that:

Thus, we have to suppose |w | ∈ A f C :x (|w|) and prove that ∃i ∈ C which satisfies items 1-5. Items 2 and 3 trivially hold for all ∃i ∈ C . Moreover, items 1 and 5 are the same condition. Therefore, we just need to prove that |w | ∈ A f C :x (|w|) implies that ∃i ∈ C which satisfies items 1 and 4.

From

By Axiom Inc of the logic AL and by construction of Σ + ϕ the following property holds for all i ∈ C . For all

From the previous two facts, we conclude that ∃i ∈ C such that:

This proves that S.4 holds.

It remains to be proved that the model M f satisfies the semantic condition S.5. That is, we have to prove that for any x ∈ INST and C , B ∈ 2 AGT such that B ⊆ C :

In order to prove this, we prove first that Proof. Theorem (3e):

(1) AL A C :x ((¬A C :x ⊥ ∧ A C :x ϕ) → A i:x ϕ), for every i ∈ C, from Axiom (Inc) by inference rule (Nec),

(2 2) and ( 3) by (ProTau) and (K)

(5 4) by (ProTau) and (K) 5) and ( 6) by (ProTau) 7) and ( 8) by (ProTau)

Proof of Proposition 1

Proof. Let suppose that the majority Principle (Majority) holds for any sets of agents C and B such that B ⊆ C and |C \ B| < |B |. We will prove by induction on the set C n , that there exists a set C n such that:

We begin by showing that (P 2 ) holds.

(1) AL ¬A AGT :x ⊥ ∧ A AGT :x A {i,j }:x ϕ → A {i,j }:x A {i,j }:x ϕ, by (Inc).

(2) AL ¬A AGT :x ⊥ ∧ A AGT :x A {i,j }:x ϕ → A {i,j }:x ϕ, from (1) by Theorem (3c)

(2) entails that (P 2 ) holds.

We suppose that (P n ) holds for any n such that C n ⊂ AGT . Under this hypothesis we will show that (P n+1 ) holds. We suppose that C n+1 is defined as:

(3) AL (¬A AGT :x ⊥ ∧ A AGT :x A {i,j }:x ϕ) → A Cn:x ϕ, by induction hypothesis 3) by (Nec), (K) and standard properties of normal modal operator A Cn+1:x

(5) AL (¬A AGT :x ⊥ ∧ A AGT :x A {i,j }:x ϕ) → A Cn+1:x A Cn:x ϕ ∧ ¬A Cn+1:x ⊥, from ( 4) by (PAccess), (NAccess), (Mon) and (ProTau) (6) AL ¬A Cn+1:x ⊥ → ¬A Cn:x ⊥, by (Mon) (7) AL A Cn+1:x ¬A Cn+1:x ⊥ → A Cn+1:x ¬A Cn:x ⊥, from ( 6) by (Nec), (K) (8) AL ¬A Cn+1:x ⊥ → A Cn+1:x ¬A Cn:x ⊥, from ( 7) by (NAccess) and (ProTau) ( 9) AL (¬A AGT :x ⊥ ∧ A AGT :x A {i,j }:x ϕ) → A Cn+1:x (A Cn:x ϕ ∧ ¬A Cn:x ⊥), from ( 5) and ( 8) by (ProTau) and standard properties of normal modal operator 9) by (Inc), (K), (Nec) and (ProTau)

(11) AL (¬A AGT :x ⊥∧A AGT :x A {i,j }:x ϕ) → A Cn+1:x ϕ, from ( 10) by (Majority), (K), (Nec) and (ProTau)

Thus ( 11) entails (P n+1 ). As (P 2 ) holds and from (P n ) we can infer that (P n+1 ) for n < |AGT |, we can thus deduce by induction that (P n ) holds for n ≤ |AGT |. In particular, we can deduce from the extension of the Principles (Majority) for every set of agents C and B such that B ⊆ C and |C \ B| < |B |, that the following counterintuitive formula holds:

Proof. Lemma (7a) and (7b):

(1) 1), (2), and (ProTau), for i ∈ C

The proof of Lemma (7b) is similar to the one of Lemma (7a), we only use Axiom (PIntrAccept) instead of Axiom (NegIntrAccept).

Proof. Propositions (2a) and (2b):

(1)

Proof of Theorem 9

Proof. Theorems (9a) and (9b): Since [x] and [Univ ] are normal modal operators, they satisfy the rule of equivalence RE [Chellas, 1980]. Theorems (9a) and (9b) follow straightforwardly from RE.

Proof. Theorem (9c):

(1) AL (( 3) and ( 4) by (ProTau) 2) and ( 5) and (ProTau)

Proof. Theorems (9d) and (9e):

The proofs of Theorems (9d) and (9e) are very similar to the previous one. Both apply (Nec), (K) and propositional tautologies.

Proof of Theorem 10

All these theorems follow from the necessitation rule (Nec) and logical tautologies. Proofs also need Axiom (K) and theorems (M) and (C) 10 [Chellas, 1980] for the distribution over conjunction. We give the complete proof of Theorem (10b) as an example.

Proof. Theorem (10b):

(1) AL ((ϕ 1 → ϕ 2 ) ∧ (ϕ 2 → ϕ 3 )) → (ϕ 1 → ϕ 3 ), by (ProTau)

(2) AL [x] (((ϕ 1 → ϕ 2 ) ∧ (ϕ 2 → ϕ 3 )) → (ϕ 1 → ϕ 3 )), from (1) by (Nec)

(3) AL [x] ((ϕ 1 → ϕ 2 ) ∧ (ϕ 2 → ϕ 3 )) → [x] (ϕ 1 → ϕ 3 ), from (2) by (K) and (C).

10 The conjunction of both (M) and (C) give the equivalence:

Proof of Theorem 11

Proof. Theorem (11a):

This theorem comes straightforwardly from Theorems 6a, 6b, 7a, 7b, and the following propositional tautologies: (4) AL → ¬O x , from (1), ( 2) and ( 3) by (ProTau)