Reasoning about Judgment and Preference Aggregation  Thomas  ◦  Agotnes  Department of Computer  Engineering, Bergen  University College  PB. 7030, N-5020 Bergen,  Norway  tag@hib.no  Wiebe van der Hoek  Department of Computer  Science, University of  Liverpool  Liverpool L69 7ZF, UK  wiebe@csc.liv.ac.uk  Michael Wooldridge  Department of Computer  Science, University of  Liverpool  Liverpool L69 7ZF, UK  mjw@csc.liv.ac.uk  ABSTRACT  Agents that must reach agreements with other agents need to   reason about how their preferences, judgments, and beliefs might be  aggregated with those of others by the social choice mechanisms  that govern their interactions. The recently emerging field of   judgment aggregation studies aggregation from a logical perspective,  and considers how multiple sets of logical formulae can be   aggregated to a single consistent set. As a special case, judgment  aggregation can be seen to subsume classical preference   aggregation. We present a modal logic that is intended to support reasoning  about judgment aggregation scenarios (and hence, as a special case,  about preference aggregation): the logical language is interpreted  directly in judgment aggregation rules. We present a sound and  complete axiomatisation of such rules. We show that the logic can  express aggregation rules such as majority voting; rule properties  such as independence; and results such as the discursive paradox,  Arrow"s theorem and Condorcet"s paradox - which are derivable  as formal theorems of the logic. The logic is parameterised in such  a way that it can be used as a general framework for comparing  the logical properties of different types of aggregation - including  classical preference aggregation.  Categories and Subject Descriptors  I.2.11 [Artificial Intelligence]: Distributed Artificial   IntelligenceMultiagent systems; I.2.4 [Artificial Intelligence]: Knowledge   Representation Formalisms and Methods-Modal logic    1. INTRODUCTION  In this paper, we are interested in knowledge representation   formalisms for systems in which agents need to aggregate their   preferences, judgments, beliefs, etc. For example, an agent may need  to reason about majority voting in a group he is a member of.   Preference aggregation - combining individuals" preference relations  over some set of alternatives into a preference relation which   represents the joint preferences of the group by so-called social   welfare functions - has been extensively studied in social choice theory  [2]. The recently emerging field of judgment aggregation studies  aggregation from a logical perspective, and discusses how, given  a consistent set of logical formulae for each agent, representing  the agent"s beliefs or judgments, we can aggregate these to a   single consistent set of formulae. A variety of judgment aggregation  rules have been developed to this end. As a special case, judgment  aggregation can be seen to subsume preference aggregation [5].  In this paper we present a logic, called Judgment Aggregation  Logic (jal), for reasoning about judgment aggregation. The   formulae of the logic are interpreted as statements about judgment   aggregation rules, and we give a sound and complete axiomatisation of  all such rules. The axiomatisation is parameterised in such a way  that we can instantiate it to get a range of different judgment   aggregation logics. For example, one instance is an axiomatisation, in  our language, of all social welfare functions - thus we get a logic  of classical preference aggregation as well. And this is one of the  main contributions of this paper: we identify the logical properties  of judgment aggregation, and we can compare the logical   properties of different classes of judgment aggregation - and of general  judgment aggregation and preference aggregation in particular.  Of course, a logic is only interesting as long as it is   expressive. One of the goals of this paper is to investigate the   representational and logical capabilities an agent needs for judgment and  preference aggregation; that is, what kind of logical language might  be used to represent and reason about judgment aggregation? An  agent"s knowledge representation language should be able to   express: common aggregation rules such as majority voting;   commonly discussed properties of judgment aggregation rules and   social welfare functions such as independence; paradoxes commonly  used to illustrate judgment aggregation and preference aggregation,  viz. the discursive paradox and Condorcet"s paradox respectively;  and other important properties such as Arrow"s theorem. In order  to illustrate in more detail what such a language would need to be  able to express, take the example of a potential property of social  welfare functions (SWFs) called independence of irrelevant   alternatives (IIA): given two preference profiles (each consisting of one  preference relation for each agent) and two alternatives, if for each  agent the two alternatives have the same order in the two preference  profiles, then the two alternatives must have the same order in the  two preference relations resulting from applying the SWF to the  two preference profiles, respectively. From this example it seems  that a formal language for SWFs should be able to express:  566  978-81-904262-7-5 (RPS) c 2007 IFAAMAS  • Quantification on several levels: over alternatives; over   preference profiles, i.e., over relations over alternatives   (secondorder quantification); and over agents.  • Properties of preference relations for different agents, and  properties of several different preference relations for the same  agent in the same formula.  • Comparison of different preference relations.  • The preference relation resulting from applying a SWF to  other preference relations.  From these points it might seem that such a language would be  rather complex (in particular, these requirements seem to rule out a  standard propositional modal logic). Perhaps surprisingly, the   language of jal is syntactically and semantically rather simple; and yet  the language is, nevertheless, expressive enough to give elegant and  succinct expressions of, e.g., IIA, majority voting, the discursive  dilemma, Condorcet"s paradox and Arrow"s theorem. This means,  for example, that Arrow"s theorem is a formal theorem of jal, i.e.,  a derivable formula; we thus have a formal proof theory for social  choice.  The structure of the rest of the paper is as follows. In the next  section we review the basics of judgment aggregation as well as  preference aggregation, and mention some commonly discussed  properties of judgment aggregation rules and social welfare   functions. In Section 3 we introduce the syntax and semantics of jal,  and study the complexity of the model checking problem.   Formulae of jal are interpreted directly by, and thus represent properties  of, judgment aggregation rules. In Section 4 we demonstrate that  the logic can express commonly discussed properties of judgment  aggregation rules, such as the discursive paradox. We give a sound  and complete axiomatisation of the logic in Section 5, under the   assumption that the agenda the agents make judgments over is finite.  As mentioned above, preference aggregation can be seen as a   special case of judgment aggregation, and in Section 6 we introduce an  alternative interpretation of jal formulae directly in social welfare  functions. We obtain a sound and complete axiomatisation of the  logic for preference aggregation as well. Sections 7 and 8 discusses  related work and concludes.  2. JUDGMENT AND PREFERENCE  AGGREGATION  Judgment aggregation is concerned with judgment aggregation  rules aggregating sets of logical formulae; preference aggregation  is concerned with social welfare functions aggregating preferences  over some set of alternatives. Let n be a number of agents; we write  Σ for the set {1, . . . , n}.  2.1 Judgment Aggregation Rules  Let L be a logic with language L(L). We require that the   language has negation and material implication, with the usual   semantics. We will sometimes refer to L as the underlying logic. An  agenda over L is a non-empty set A ⊆ L(L), where for every   formula φ that does not start with a negation, φ ∈ A iff ¬φ ∈ A. We  sometimes call a member of A an agenda item. A subset A ⊆ A is  consistent unless A entails both ¬φ and φ in L for some φ ∈ L(L);  A is complete if either φ ∈ A or ¬φ ∈ A for every φ ∈ A which  does not start with negation. An (admissible) individual judgment  set is a complete and consistent subset Ai ⊆ A of the agenda. The  idea here is that a judgment set Ai represents the choices from A  made by agent i. Two rationality criteria demand that an agents"  choices at least be internally consistent, and that each agent makes  a decision between every item and its negation. An (admissible)  judgment profile is an n-tuple A1, . . . , An , where Ai is the   individual judgment set of agent i. J(A, L) denotes the set of all individual  (complete and L-consistent) judgment sets over A, and J(A, L)n  the set of all judgment profiles over A. When γ ∈ J(A, L)n  , we use  γi to denote the ith element of γ, i.e., agent i"s individual judgment  set in judgment profile γ.  A judgment aggregation rule (JAR) is a function f that maps each  judgment profile A1, . . . , An to a complete and consistent   collective judgment set f(A1, . . . , An) ∈ J(A, L). Such a rule hence is a  recipe to enforce a rational group decision, given an tuple of   rational choices by the individual agents. Of course, such a rule should  to a certain extent be ‘fair". Some possible properties of a judgment  aggregation rule f over an agenda A:  Non-dictatorship (ND1) There is no agent i such that for every  judgment profile A1, . . . , An , f(A1, . . . , An) = Ai  Independence (IND) For any p ∈ A and judgment profiles  A1, . . . , An and B1, . . . , Bn , if for all agents i (p ∈ Ai iff  p ∈ Bi), then p ∈ f(A1, . . . , An) iff p ∈ f(B1, . . . , Bn)  Unanimity (UNA) For any judgment profile A1, . . . , An and any  p ∈ A, if p ∈ Ai for all agents i, then p ∈ f(A1, . . . , An)  2.2 Social Welfare Functions  Social welfare functions (SWFs) are usually defined in terms of  ordinal preference structures, rather than cardinal structures such as  utility functions. An SWF takes a preference relation, a binary   relation over some set of alternatives, for each agent, and outputs   another preference relation representing the aggregated preferences.  The most well known result about SWFs is Arrow"s theorem [1].  Many variants of the theorem appear in the literature, differing in  assumptions about the preference relations. In this paper, we take  the assumption that all preference relations are linear orders, i.e.,  that neither agents nor the aggregated preference can be indifferent  between distinct alternatives. This gives one of the simplest   formulations of Arrow"s theorem (Theorem 1 below). Cf., e.g., [2] for a  discussion and more general formulations.  Formally, let K be a set of alternatives. We henceforth   implicitly assume that there are always at least two alternatives. A   preference relation (over K) is, here, a total (linear) order on K, i.e.,  a relation R over K which is antisymmetric (i.e., (a, b) ∈ R and  (b, a) ∈ R implies that a = b), transitive (i.e., (a, b) ∈ R and  (b, c) ∈ R implies that (a, c) ∈ R), and total (i.e., either (a, b) ∈  R or (b, a) ∈ R). We sometimes use the infix notation aRb for  (a, b) ∈ R. The set of preference relations over alternatives K is  denoted L(K). Alternatively, we can view L(K) as the set of all  permutations of K. Thus, we shall sometimes use a permutation of  K to denote a member of L(K). For example, when K = {a, b, c},  we will sometimes use the expression acb to denote the relation  {(a, c), (a, b), (c, b), (a, a), (b, b), (c, c)}. aRb means that b is   preferred over a if a and b are different. Rs  denotes the irreflexive  version of R, i.e., Rs  = R \ {(a, a) : a ∈ K}. aRs  b means that b is  preferred over a and that a b.  A preference profile for Σ over alternatives K is a tuple  (R1, . . . , Rn) ∈ L(K)n  , consisting of one preference relation Ri for  each agent i. A social welfare function (SWF) is a function  F : L(K)n  → L(K)  mapping each preference profile to an aggregated preference   relation. The class of all SWFs over alternatives K is denoted F (K).  Properties of SWFs F corresponding to the judgment   aggregation rule properties discussed in Section 2.1 are:  The Sixth Intl. Joint Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS 07) 567  Non-dictatorship (ND2) ¬∃i∈Σ∀(R1, . . . , Rn) ∈ L(K)n  F(R1, . . . , Rn) = Ri (corresponds to ND1)  Independence of irrelevant alternatives (IIA) ∀(R1, . . . , Rn)  ∈ L(K)n  ∀(S1, . . . , Sn) ∈ L(K)n  ∀a ∈ K∀b ∈ K((∀i ∈ Σ(aRib ⇔  aSib)) ⇒ (aF(R1, . . . , Rn)b ⇔ aF(S1, . . . , Sn)b)) (corresponds  to IND)  Pareto Optimality (PO) ∀(R1, . . . , Rn) ∈ L(K)n  ∀a ∈ K∀b ∈ K  ((∀i ∈ ΣaRs  i b) ⇒aF(R1, . . . , Rn)s  b) (corresponds to UNA)  Arrow"s theorem says that the three properties above are   inconsistent if there are more than two alternatives.  Theorem 1 (Arrow). If there are more than two alternatives,  no SWF has all the properties PO, ND2 and IIA.  3. JUDGMENT AGGREGATION LOGIC:  SYNTAX AND SEMANTICS  The language of Judgment Aggregation Logic (jal) is   parameterised by a set of agents Σ = {1, 2, . . . , n} (we will assume that  there are at least two agents) and an agenda A. The following  atomic propositions are used:  Π = {i, σ, hp | p ∈ A, i ∈ Σ}  The language L(Σ, A) of jal is defined by the following grammar:  φ ::= α | φ | φ | φ ∧ φ | ¬φ  where α ∈ Π. This language will be formally interpreted in   structures consisting of an agenda item, a judgment profile and a   judgment aggregation function; informally, i means that the agenda item  is in agent i"s judgment set in the current judgment profile; σ means  that the agenda item is in the aggregated judgment set of the current  judgment profile; hp means that the agenda item is p; φ means that  φ is true in every judgment profile; φ means that φ is true in every  agenda item.  We define ψ = ¬ ¬ψ, intuitively meaning ψ is true for some  judgment profile, and ψ = ¬ ¬ψ, intuitively meaning ψ is true  for some agenda item, as usual, in addition to the usual derived  propositional connectives.  We now define the formal semantics of L(Σ, A). A model wrt.  L(Σ, A) and underlying logic L is a judgment aggregation rule f  over A. Recall that J(A, L)n  denotes the set of complete and   Lconsistent judgment profiles over A. A table is a tuple T = f, γ, p  such that f is a model, γ ∈ J(A, L)n  and p ∈ A. A formula is  interpreted on a table as follows.  f, γ, p |=L hq ⇔ p = q  f, γ, p |=L i ⇔ p ∈ γi  f, γ, p |=L σ ⇔ p ∈ f(γ)  f, γ, p |=L ψ ⇔ ∀γ ∈ J(A, L)n  f, γ , p |=L ψ  f, γ, p |=L ψ ⇔ ∀p ∈ A f, γ, p |=L ψ  f, γ, p |=L φ ∧ ψ ⇔ f, γ, p |=L φ and f, γ, p |=L ψ  f, γ, p |=L ¬φ ⇔ f, γ, p |=L φ  So, e.g., we have that f, γ, p |=L i∈Σ i if everybody chooses p in γ.  Example 1. A committee of three agents are voting on the   following three propositions: the candidate is qualified (p), if the  candidate is qualified he will get an offer (p → q), and the  candidate will get an offer (q). One possible voting scenario  is illustrated in the left part of Table 1. In the table, the results  of proposition-wise majority voting, i.e., the JAR fmaj accepting a  proposition iff it is accepted by a majority of the agents, are also  p p → q q  1 yes yes yes  2 no yes yes  3 yes no no  fmaj yes yes yes  1 mdc  2 mcd  3 cmd  Fmaj mcd  Table 1: Examples  shown. This example can be modelled by taking the agenda to  be A = {p, p → q, q, ¬p, ¬(p → q), ¬q} (recall that agendas are  closed under single negation) and L to be propositional logic. The  agents" votes can be modelled by the following judgment profile:  γ = γ1, γ2, γ3 , where γ1 = {p, p → q, q}, γ2 = {¬p, p → q, q},  γ3 = {p, ¬(p → q), ¬q}. We then have that:  • fmaj, γ, p |=L 1 ∧ ¬2 ∧ 3 (agents 1 and 3 judges p to be true in  the profile γ, while agent 2 does not)  • fmaj, γ, p |=L σ (majority voting on p given the preference  profile γ leads to acceptance of p)  • fmaj, γ, p |=L (1 ∧ 2) (agents 1 and 2 agree on some agenda  item, under the judgment profile γ. Note that this formula  does not depend on which agenda item is on the table.)  • fmaj, γ, p |=L ((1 ↔ 2) ∧ (2 ↔ 3) ∧ (1 ↔ 3)) (there is some  judgment profile on which all agents agree on p. Note that  this formula does not depend on which judgment profile is on  the table.)  • fmaj, γ, p |=L ((1 ↔ 2) ∧ (2 ↔ 3) ∧ (1 ↔ 3)) (there  is some judgment profile on which all agents agree on all  agenda items. Note that this formula does not depend on any  of the elements on the table.)  • fmaj, γ, p |=L σ ↔ G⊆{1,2,3},|G|≥2 i∈G i (the JAR fmaj   implements majority voting)  We write f |=L φ iff f, γ, p |=L φ for every γ over A and p ∈ A;  |=L φ iff f |=L φ for all models f. Given a possible property of a  JAR, such as, e.g., independence, we say that a formula expresses  the property if the formula is true in an aggregation rule f iff f has  the property.  Note that when we are given a formula φ ∈ L(Σ, A), validity,  i.e., |=L φ, is defined with respect to models of the particular   language L(Σ, A) defined over the particular agenda A (and similar  for validity with respect to a JAR, i.e., f |=L φ). The agenda, like  the set of agents Σ, is given when we define the language, and is  thus implicit in the interpretation of the language1  .  Let an outcome o be a maximal conjunction of literals  (¬)1, . . . , (¬)n. The set O is the set of all possible outcomes. Note  that the decision of the society is not incorporated here: an outcome  only collects votes of agents from Σ.  3.1 Model Checking  Model checking is currently one of the most active areas of   research with respect to reasoning in modal logics [4], and it is natural  to investigate the complexity of this problem for judgment   aggregation logic. Intuitively, the model checking problem for judgment  aggregation logic is as follows:  Given f, γ, p and formula φ of jal, is it the case that  f, γ, p |= φ or not?  1  Likewise, in classical modal logic the language is parameterised  with a set of primitive propositions, and validity is defined with  respect to all models with valuations over that particular set.  568 The Sixth Intl. Joint Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS 07)  While this problem is easy to understand mathematically, it presents  some difficulties if we want to analyse it from a computational  point of view. Specifically, the problem lies in the   representation of the judgment aggregation rule, f. Recall that this   function maps judgment profiles to complete and consistent judgment  sets. A JAR must be defined for all judgment profiles over some  agenda, i.e., it must produce an output for all these possible   inputs. But how are we to represent such a rule? The simplest   representation of a function f : X → Y is as the set of ordered pairs  {(x, y) | x ∈ X & y = f(x)}. However, this is not a feasible   representation for JARs, as there will be exponentially many judgment  profiles in the size of the agenda, and so the representation would  be unfeasibly large in practice. If we did assume this   representation for JARs, then it is not hard to see that model checking for our  logic would be decidable in polynomial time: the naive algorithm,  derivable from semantics, serves this purpose.  However, we emphasise that this result is of no practical   significance, since it assumes an unreasonable representation for models  - a representation that simply could not be used in practice for   examples of anything other than trivial size.  So, what is a more realistic representation for JARs? Let us say  a representation Rf of a JAR f is reasonable if: (i) the size of Rf  is polynomial in the size of the agenda; and (ii) there is a   polynomial time algorithm A, which takes as input a representation Rf  and a judgment profile γ, and produces as output f(γ). There are,  of course, many such representations Rf for JARs f. Here, we will  look at one very general one: where the JAR is represented as a  polynomially bounded two-tape Turing machine Tf , which takes  on its first tape a judgment profile, and writes on its second tape  the resulting judgment set. The requirement that the Turing   machine should be polynomially bounded roughly corresponds to the  requirement that a JAR is reasonable to compute; if there is some  JAR that cannot be represented by such a machine, then it is   arguably of little value, since it could not be used in practice2  . With  such a representation, we can investigate the complexity of our  model checking problem.  In modal logics, the usual source of complexity, over and above  the classical logic connectives, is the modal operators. With   respect to judgment aggregation logic, the operator quantifies over  all judgment profiles, and hence over all consistent subsets of the  agenda. It follows that this is a rather powerful operator: as we will  see, it can be used as an np oracle [9, p.339]. In contrast, the   operator quantifies over members of the agenda, and is hence much  weaker, from a computational perspective (we can think of it as a  conjunction over elements of the agenda).  The power of the quantifier suggests that the complexity of  model checking judgment aggregation logic over relatively   succinct representations of JAR is going to be relatively high; we now  prove that the complexity of model checking judgment aggregation  logic is as hard as solving a polynomial number of np-hard   problems [9, pp.424-429].  Theorem 2. The model checking problem for judgment   aggregation logic, assuming the representation of JARs described above,  is Δp  2-hard; it is np-hard even if the formula to be checked is of the  form ψ, where ψ contains no further or operators.  Proof. For Δp  2-hardness, we reduce snsat (sequentially nested  2  Of course, we have no general way of checking whether any  given Turing machine is guaranteed to terminate in polynomial  time; the problem is undecidable. As a consequence, we cannot  always check whether a particular Turing machine representation  of a JAR meets our requirements. However, this does not prevent  specific JARs being so represented, with corresponding proofs that  they terminate in polynomial time.  satisfiability). An instance is given by a series of equations of the  form  z1 = ∃X1.φ1(X1) z2 = ∃X2.φ2(X2, z1) z3 = ∃X3.φ3(X3, z1, z2)  . . .  zk = ∃Xk.φk(Xk, z1, . . . , zk−1)  where X1, . . . , Xk are disjoint sets of variables, and each φi(Y) is a  propositional logic formula over the variables Y; the idea is we first  check whether φ1(X1) is satisfiable, and if it is, we assign z1 the  value true, otherwise assign it false; we then check whether φ2 is  satisfiable under the assumption that z1 takes the value just derived,  and so on. Thus the result of each equation depends on the value of  the previous one. The goal is to determine whether zk is true.  To reduce this problem to judgment aggregation logic model  checking, we first fix the JAR: this rule simply copies whatever  agent 1"s judgment set is. (Clearly this can be implemented by a  polynomially bounded Turing machine.) The agenda is assumed to  contain the variables X1 ∪ · · · ∪ Xk ∪ {z1, . . . , zk} and their negations.  We fix the initial judgment profile γ to be X1 ∪· · ·∪Xk ∪{z1, . . . , zk},  and fix p = x1. Given a variable xi, define x∗  i to be (hxi ∧1). If φi is  one of the formulae φ1, . . . , φk, define φ∗  i to be the formula obtained  from φi by systematically substituting x∗  i for each variable xi and z∗  i  similarly.  Now, we define the function ξi for natural numbers i > 0 as:  ξk =  z∗  1 ↔ (φ∗  1) if i = 1  z∗  i ↔ (φ∗  i ∧i−1  j=1 ξj) otherwise.  And we define the formula to be model checked as:  φ∗  k ∧k−1  j=1 ξj  It is now straightforward from construction that this formula is true  under the interpretation iff zk is true in the snsat instance. The proof  of the latter half of the theorem is immediate from the special case  where k = 1.  3.2 Some Properties  We have thus defined a language which can be used to express  properties of judgment aggregation rules. An interesting question  is then: what are the universal properties of aggregation rules   expressible in the language; which formulae are valid? Here, in order  to illustrate the logic, we discuss some of these logical properties.  In Section 5 we give a complete axiomatisation of all of them.  Recall that we defined the set O of outcomes as the set of all  conjunctions with exactly one, possibly negated, atom from Σ. Let  P = {o ∧ σ, o ∧ ¬σ : o ∈ O}; p ∈ P completely describes the  decisions of the agents and the aggregation function. Let denote  exclusive or.  We have that:  |=L p∈Pp - any agent and the JAR always have to make a decision  |=L (i ∧ ¬j) → ¬i - if some agent can think differently about an  item than i does, then also i can change his mind about it. In  fact this principle can be strengthened to  |=L ( i ∧ ¬j) → (¬i ∧ j)  |=L x - for any x ∈ {i, ¬i, σ, ¬σ : i ∈ Σ} - both the individual  agents and the JAR will always judge some agenda item to  be true, and conversely, some agenda item to be false  |=L (i ∧ j) - there exist admissible judgment sets such that agents  i and j agree on some judgment.  |=L (i ↔ j) - there exist admissible judgment sets such that agents  i and j always agree.  The Sixth Intl. Joint Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS 07) 569  The interpretation of formulae depends on the agenda A and the  underlying logic L, in the quantification over the set J(A, L)n  of   admissible, e.g., complete and L-consistent, judgment profiles. Note  that this means that some jal formula might be valid under one   underlying logic, while not under another. For example, if the agenda  contains some formula which is inconsistent in the underlying logic  (and, by implication, some tautology), then the following hold:  |=L (i ∧ σ) - for every judgment profile, there is some agenda  item (take a tautology) which both agent i and the JAR judges  to be true  But this property does not hold when every agenda item is   consistent with respect to the underlying logic. One such agenda and  underlying logic will be discussed in Section 6.  4. EXPRESSIVITY EXAMPLES  Non-dictatorship can be expressed as follows:  ND =  i∈Σ  ¬(σ ↔ i) (1)  Lemma 1. f |=L ND iff f has the property ND1.  Independence can be expressed as follows:  IND =  o∈O  ((o ∧ σ) → (o → σ)) (2)  Lemma 2. f |=L IND iff f has the property IND.  Unanimity can be expressed as follows:  UNA = ((1 ∧ · · · ∧ n) → σ) (3)  Lemma 3. f |=L UNA iff f has the property UNA.  4.1 The Discursive Paradox  As illustrated in Example 1, the following formula expresses  proposition-wise majority voting over some proposition p  MV = σ ↔  G⊆Σ,|G|> n  2  i∈G  i (4)  i.e., the following property of a JAR f and admissible profile  A1, . . . , An :  p ∈ f(A1, . . . , An) ⇔ |{i : p ∈ Ai}| > |{i : p Ai}|  f |= MV exactly iff f has the above property for all judgment   profiles and propositions.  However, we have the following in our logic. Assume that the  agenda contains at least two distinct formulae and their material  implication (i.e., A contains p, q, p → q for some p, q ∈ L(L)).  Proposition 1 (Discursive Paradox).  |=L (( MV) → ⊥)  when there are at least three agents and the agenda contains at  least two distinct formulae and their material implication.  Proof. Assume the opposite, e.g., that A = {p, p → q, q, ¬p,  ¬(p → q), ¬q, . . .} and there exists an aggregation rule f over A  such that f |=L (σ ↔ G⊆Σ,|G|> n  2 i∈G i). Let γ be the   judgment profile γ = A1, A2, A3 where A1 = {p, p → q, q, . . .}, A2 =  {p, ¬(p → q), ¬q, . . .} and A3 = {¬p, p → q, ¬q, . . .}. We have  that f, γ, p |=L (σ ↔ G⊆Σ,|G|> n  2 i∈G i) for any p , so f, γ, p |=L  σ ↔ G⊆Σ,|G|> n  2 i∈G i. Because f, γ, p |=L 1 ∧ 2, it follows that  f, γ, p |=L σ. In a similar manner it follows that f, γ, p → q |=L σ  and f, γ, q |=L ¬σ. In other words, p ∈ f(γ), p → q ∈ f(γ) and  q f(γ). Since f(γ) is complete, ¬q ∈ f(γ). But that contradicts  the fact that f(γ) is required to be consistent.  Proposition 1 is a logical statement of a variant of the well-known  discursive dilemma: if three agents are voting on propositions p, q  and p → q, proposition-wise majority voting might not yield a  consistent result.  5. AXIOMATISATION  Given an underlying logic L, a finite agenda A over L, and a set  of agents Σ, Judgment Aggregation Logic (jal(L), or just jal when  L is understood) for the language L(Σ, A), is defined in Table 2.  ¬(hp ∧ hq) if p q Atmost  p∈A hp Atleast  hp p ∈ A Agenda  (hp ∧ ϕ) → (hp → ϕ) Once  (hp ∧ x) ∨ (hp ∧ x) CpJS  all instantiations of propositional tautologies taut  (ψ1 → ψ2) → ( ψ1 → ψ2) K  ψ → ψ T  ψ → ψ 4  ¬ ψ → ¬ ψ 5  ( i ∧ ¬j) → o∈O o C  ψ ↔ ψ (COMM)  From p1, . . . pn L q infer  (hp1  ∧ x) ∧ · · · ∧ (hpn ∧ x) →  (hq → x) ∧ (hq → ¬x) Closure  From ϕ → ψ and ϕ infer ψ MP  From ψ infer ψ Nec  Table 2: The logic jal(L) for the language L(Σ, A). p, pi, q range  over the agenda A; φ,ψ,ψi over L(Σ, A); x over {σ, i : i ∈ Σ};  over { , }; i, j over Σ; o over the set of outcomes O. hp means  hq when p = ¬q for some q, otherwise it means h¬p. L is the  underlying logic.  The first 5 axioms represent properties of a table and of judgment  sets. Axiom Atmost says that there is at most one item on the table  at a time, and Atleast says that we always have an item on the table.  Axiom Agenda says that every agenda item will appear on the table,  whereas Once says that every item of the agenda only appears on  the table once. Note that a conjunction hp ∧ x reads: item p is on  the agenda, and x is in favour of it, or x judges it true. Axiom CpJS  corresponds to the requirement that judgment sets are complete.  Note that from Agenda, CsJS and CpJS we derive the scheme x ∧  ¬x, which says that everybody should at least express one opinion  in favour of something, and against something.  The axioms taut − 5 are well familiar from modal logic: they  directly reflect the unrestricted quantification in the truth definition  of and . Axiom C says that for any agenda item for which it  is possible to have opposing opinions, every possible outcome for  that item should be achievable. COMM says that everything that  is true for an arbitrary profile and item, is also true for an arbitrary  item and profile. Closure guarantees that agents behave   consistently with respect to consequence in the logic L. MP and Nec are  standard. We use JAL(L) to denote derivability in jal(L).  Theorem 3. If the agenda is finite, we have that for any formula  ψ ∈ L(Σ, A), JAL(L) ψ iff |=L ψ.  Proof. Soundness is straightforward. For completeness (we   focus on the main idea here and leave out trivial details), we build a  570 The Sixth Intl. Joint Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS 07)  jal table for a consistent formula ψ as follows. In fact, our   axiomatisation completely determines a table, except for the behaviour of  f. To be more precise, let a table description be a conjunction of  the form hp ∧ o ∧ (¬)σ. It is easy to see that table descriptions are  mutually exclusive, and, moreover, we can derive τ∈T τ, where T  is the set of all table descriptions. Let D be the set of all   maximal consistent sets Δ. We don"t want all of those: it might well  be that ψ requires σ to be in a certain way, which is incompatible  with some Δ"s. We define two accessibility relations in the standard  way: R Δ1Δ2 iff for all ψ: ψ ∈ Δ1 ⇒ ψ ∈ Δ2. Similarly for R  with respect to . Both relations are equivalences (due to taut-5),  and moreover, when R Δ1Δ2 and R Δ2Δ3 then for some Δ2, also  R Δ1Δ2 and R Δ2Δ3 (because of axiom COMM).  Let Δ0 be a MCS containing ψ. We now define the set Tables =  {Δ0} ∪ {Δ1, Δ2 | (R Δ0Δ1 and R Δ1Δ2) or (R Δ0Δ1 and R Δ1Δ2)}  Every Δ ∈ Tables can be conceived as a pair γ, p, since every Δ  contains a unique (hq ∧ o ∧ (¬)σ) for every hq and a unique hp.  It is then easy to verify that, for every Δ ∈ Tables, and every  formula ϕ, Δ |= ϕ iff ϕ ∈ Δ, where |= here means truth in the  ordinary modal logic sense when the set of states is taken to be  Tables. Now, we extract an aggregation function f and pairs γ, p as  follows:  For every Δ ∈ Tables, find a conjunction hp ∧ o ∧ (¬)σ. There  will be exactly one such p. This defines the p we are looking for.  Furthermore, the γ is obtained, for every agent i, by finding all q for  which (hq ∧ i) is currently true. Finally, the function f is a table  of all tuples hp, o(p), σ for which (hp ∧ o(o) ∧ σ) is contained in  some set in Tables.  We point out that jal has all the axioms taut, K, T, 4, 5 and the  rules MP and Nec of the modal logic S5. However, uniform   substitution, a principle of all normal modal logics (cf., e.g., [3]), does  not hold. A counter example is the fact that the following is valid:  σ (5)  - no matter what preferences the agents have, the JAR will always  make some judgment - while this is not valid:  (σ ∧ i) (6)  - the JAR will not necessarily make the same judgments as agent i.  So, for example, we have that the discursive paradox is provable  in jal(L): JAL(L) (( MV) → ⊥). An example of a derivation of  the less complicated (valid) property (i ∧ j) is shown in Table 3.  6. PREFERENCE AGGREGATION  Recently, Dietrich and List [5] showed that preference   aggregation can be embedded in judgment aggregation. In this section we  show that our judgment aggregation logic also can be used to   reason about preference aggregation.  Given a set K of alternatives, [5] defines a simple predicate logic  LK  with language L(LK  ) as follows:  • L(LK  ) has one constant a for each alternative a ∈ K,   variables v1, v2, . . ., a binary identity predicate =, a binary   predicate P for strict preference, and the usual propositional and  first order connectives  • Z is the collection of the following axioms:  - ∀v1 ∀v2 (v1Pv2 → ¬v2Pv1)  - ∀v1 ∀v2 ∀v3 ((v1Pv2 ∧ v2Pv3) → v1Pv3)  - ∀v1 ∀v2 (¬v1 = v2 → (v1Pv2 ∨ v2Pv1))  • When Γ ⊆ L(LK  ) and φ is a formula, Γ |= φ is defined to hold  iff Γ ∪ Z entails φ in the standard sense of predicate logic  1 (hp ∧ i) ∨ (hp ∧ i) CpJS(i)  2 (hp ∧ j) ∨ (hp ∧ j) CpJS(j)  3 Call 1 A ∨ B and 2 C ∨ D abbreviation, 1, 2  4 (A ∧ C) ∨ (A ∧ D) ∨ (B ∧ C) ∨ (B ∧ D) taut, 3  5 derive (i ∧ j) from every disjunct of 4 strategy is ∨ elim  6 (hp ∧ i) ∧ (hp ∧ j) assume A ∧ C  7 (hp → (i ∧ j)) Once, 6, K( )  8 (i ∧ j) 7, Agenda  9 (i ∧ j) 8, T( )  10 (hp ∧ i) ∧ (hp ∧ j) assume A ∧ D  11 (hp ∧ x) ↔ (hp ∧ ¬x) Agenda, Closure  12 (hp ∧ i) ∧ (hp ∧ ¬j) 10, 11  13 (hp ∧ i ∧ ¬j) 12, Once, K( )  14 (i ∧ ¬j) 13, taut  15 (i ∧ ¬j) 14, K( )  16 (i ∧ ¬j) 15, COMM  17 ( i ∧ D¬j) 16, K( )  18 (i ∧ j) 17, C  19 (hp ∧ i) ∧ (hp ∧ j) assume B ∧ D  20 goes as 6-9  21 (hp ∧ i) ∧ (hp ∧ j) assume B ∧ C  22 goes as 10 - 18  23 (i ∧ j) ∨-elim, 1, 2, 9, 18,  20, 22  Table 3: jar derivation of (i ∧ j)  It is easy to see that there is an one-to-one correspondence between  the set of preference relations (total linear orders) over K and the set  of LK  -consistent and complete judgment sets over the preference  agenda  AK  = {aPb, ¬aPb : a, b ∈ K, a b}  Given a SWF F over K, the corresponding JAR fF  over the   preference agenda AK  is defined as follows fF  (A1, . . . , An) = A, where  A is the consistent and complete judgment set corresponding to  F(L1, . . . , Ln) where Li is the preference relation corresponding to  the consistent and complete judgment set Ai.  Thus we can use jal to reason about preference aggregation as  follows. Take the logical language L(Σ, AK  ), for some set of agents  Σ, and take the underlying logic to be LK  . We can then interpret our  formulae in an SWF F over K, a preference profile L ∈ L(K) and a  pair (a, b) ⊆ K × K, a b, as follows:  F, L, (a, b) |=swf  φ ⇔ fF  , γL  , aPb |=LK φ  where γL  is the judgment profile corresponding to the preference  profile L.  While in the general judgment aggregation case a formula is   interpreted in the context of an agenda item, in the preference   aggregation case a formula is thus interpreted in the context of a pair of  alternatives.  Example 2. Three agents must decide between going to dinner  (d), a movie (m) or a concert (c). Their individual preferences  are illustrated on the right in Table 1 in Section 3, along with the  result of a SWF Fmaj implementing pair-wise majority voting. Let  L = mdc, mcd, cmd be the preference profile corresponding to the  preferences in the example. We have the following:  • Fmaj, L, (m, d) |=swf  1 ∧ 2 ∧ 3 (all agents agree, under the  individual rankings L, on the relative ranking of m and   dthey agree that d is better than m)  • Fmaj, L, (m, d) |=swf  ¬(1 ↔ 2) (under the individual   rankings L, there is some pair of alternatives on which agents 1  and 2 disagree)  The Sixth Intl. Joint Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS 07) 571  • Fmaj, L, (m, d) |=swf  (1 ∧ 2) (agents 1 and 2 can choose  their preferences such that they will agree on some pair of  alternatives)  • Fmaj, L, (m, d) |=swf  σ ↔ G⊆{1,2,3},|G|≥2 i∈G i (the SWF Fmaj  implements pair-wise majority voting)  As usual, we write F |=swf  φ when F, L, (a, b) |=swf  φ for any L  and (a, b), and so on. Thus, our formulae can be seen as expressing  properties of social welfare functions.  Example 3. Take the formula (i ↔ σ). When this formula is  interpreted as a statement about a social welfare function, it says  that there exists a preference profile such that for all pairs (a, b) of  alternatives, b is preferred over a in the aggregation (by the SWF)  of the preference profile if and only if agent i prefers b over a.  6.1 Expressivity Examples  We make precise the claim in Section 2.2 that the three   mentioned SWF properties correspond to the three mentioned JAR   properties, respectively. Recall the formulae defined in Section 4.  Proposition 2.  F |=swf  ND iff F has the property ND2  F |=swf  IND iff F has the property IIA  F |=swf  UNA iff F has the property PO  The properties expressed above are properties of SWFs. Let us  now look at properties of the set of alternatives K we can express.  Properties involving cardinality is often of interest, for example in  Arrow"s theorem. Let:  MT2 = ( (1 ∧ 2) ∧ (1 ∧ ¬2))  Proposition 3. Let F ∈ F (K). |K| > 2 iff F |=swf  MT2.  Proof. For the direction to the left, let F |=swf  MT2. Thus, there  is a γ such that there exists (a1  , b1  ), (a2  , b2  ) ∈ K × K, where a1  b1  , and a2  b2  , such that (i) a1  Pb1  ∈ γ1, (ii) a1  Pb1  ∈ γ2, (iii)  a2  Pb2  ∈ γ1 and (iv) a2  Pb2  γ2. From (ii) and (iv) we get that  (a1  , b1  ) (a2  , b2  ), and from that and (i) and (iii) it follows that  γ1 contains two different pairs a1  Pb1  and a2  Pb2  each having two  different elements. But that is not possible if |K| = 2, because if K =  {a, b} then AK  = {aPb, ¬aPb, bPa, ¬bPa} and thus it is impossible  that γ1 ⊆ AK  since we cannot have aPb, bPa ∈ γ1.  For the direction to the right, let |K| > 2; let a, b, c be three  distinct elements of K. Let γ1 be the judgment set corresponding  to the ranking abc and γ2 the judgment set corresponding to acb.  Now, for any aggregation rule f, f, γ, aPb |= 1 ∧ 2 and f, γ, bPc |=  1 ∧ ¬2. Thus, F |=swf  MT2, for any SWF F.  We now have everything we need to express Arrow"s statement  as a formula. It follows from his theorem that the formula is valid  on the class of all social welfare functions.  Theorem 4. |=swf  MT2 → ¬(PO ∧ ND ∧ IIA)  Proof. Note that MT2, PO, ND and IIA are true SWF properties,  their truth value wrt. a table is determined solely by the SWF. For  example, F, L, (a, b) |=swf  MT2 iff F |= MT2, for any F, L, a, b.  Let F ∈ F (K), and F, L, (a, b) |=swf  MT2 for some L and a, b. By  Proposition 3, K has more than two alternatives. By Arrow"s   theorem, F cannot have all the properties PO, ND2 and IIA. W.l.o.g  assume that F does not have the PO property. By Proposition 2,  F |=swf  PO. Since PO is a SWF property, this means that  F, L, (a, b) |=swf  PO (satisfaction of PO is independent of L, a, b),  and thus that F, L, (a, b) |=swf  ¬PO ∨ ¬ND ∨ ¬IIA.  Note that the formula in Theorem 4 does not mention any agenda  items (i.e., pairs of alternatives) such as haPb directly in an   expression. This means that the formula is a member of L(Σ, AK  ) for any  set of alternatives K, and is valid no matter which set of alternatives  we assume.  The formula MV which in the general judgment aggregation case  expresses proposition-wise majority voting, expresses in the   preference aggregation case pair-wise majority voting, as illustrated in  Example 2. The preference aggregation correspondent to the   discursive paradox of judgment aggregation is the well known   Condorcet"s voting paradox, stating that pair-wise majority voting can  lead to aggregated preferences which are cyclic (even if the   individual preferences are not). We can express Condorcet"s paradox  as follows, again as a universally valid logical property of SWFs.  Proposition 4. |=swf  MT2 → ¬MV, when there are at least  three agents.  Proof. The proof is similar to the proof of the discursive   paradox. Let fF  , γ, aPb |=LK MT2; there are thus three distinct   elements a, b, c ∈ K. Assume that fF  , γ, aPb |=LK MV. Let  γ be the judgment profile corresponding to the preference   profile X = (abc, cab, bca). We have that fF  , γ , aPb |=LK 1 ∧ 2 and,  since fF  , γ , aPb |=LK MV, we have that fF  , γ , aPb |=LK σ and thus  that aPb ∈ fF  (γ ) and (a, b) ∈ F(X). In a similar manner we get  that (c, a) ∈ F(X) and (b, c) ∈ F(X). But that is impossible, since  by transitivity we would also have that (a, c) ∈ F(X) which   contradicts the fact that F(X) is antisymmetric. Thus, it follows that  fF  , γ, aPb |=LK MV.  6.2 Axiomatisation and Logical Properties  We immediately get, from Theorem 3, a sound and complete  axiomatisation of preference aggregation over a finite set of   alternatives.  Corollary 1. If the set of alternatives K is finite, we have that  for any formula ψ ∈ L(Σ, AK  ), JAL(LK ) ψ iff |=swf  ψ.  Proof. Follows immediately from Theorem 3 and the fact that  for any JAR f, there is a SWF F such that f = fF  .  So, for example, Arrow"s theorem is provable in jal(LK  ): JAL(LK )  MT2 → ¬(PO ∧ ND ∧ IIA).  Every formula which is valid with respect to judgment   aggregation rules is also valid with respect to social welfare functions, so  all general logical properties of JARs are also properties of SWFs.  Depending on the agenda, SWFs may have additional properties,  induced by the logic LK  , which are not always shared by JARs with  other underlying logics. One such property is i. While we have  |=swf  i,  for other agendas there are underlying logics L such that  |=L i  To see the latter, take an agenda with a formula p which is   inconsistent in the underlying logic L - p can never be included in a  judgment set. To see the former, take an arbitrary pair of   alternatives (a, b). There exists some preference profile in which agent i  prefers b over a.  Technically speaking, the formula i holds in SWFs because the  agenda AK  does not contain a formula which (alone) is inconsistent  wrt. the underlying logic LK  . By the same reason, the following  properties also hold in SWFs but not in JARs in general.  |=swf  o∈O  o  572 The Sixth Intl. Joint Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS 07)  - for any pair of alternatives (a, b), any possible combination of the  relative ranking of a and b among the agents is possible.  |=swf  i → ¬i  - given an alternative b which is preferred over some other   alternative a by agent i, there is some other pair of alternatives c and d  such that d is not preferred over c - namely (c, d) = (b, a).  |=swf  ( (i ∨ j) → (i ∧ ¬j))  - if, given preferences of agents and a SWF, for any two alternatives  it is always the case that either agent i or agent j prefers the second  alternative over the first, then there must exist a pair of alternatives  for which the two agents disagree. A justification is that no single  agent can prefer the second alternative over the first for every pair  of alternatives, so in this case if i prefers b over a then j must prefer  a over b. Again, this property does not necessarily hold for other  agendas, because the agenda might contain an inconsistency the  agents could not possibly disagree upon.  Proof theoretically, these additional properties of SWFs are   derived using the Closure rule.  7. RELATED WORK  Formal logics related to social choice have focused mostly on the  logical representation of preferences when the set of alternatives is  large and on the computation properties of computing aggregated  preferences for a given representation [6, 7, 8].  A notable and recent exception is a logical framework for   judgment aggregation developed by Marc Pauly in [10], in order to be  able to characterise the logical relationships between different   judgment aggregation rules. While the motivation is similar to the work  in this paper, the approaches are fundamentally different: in [10],  the possible results from applying a rule to some judgment   profile are taken as primary and described axiomatically; in our   approach the aggregation rule and its possible inputs, i.e., judgment  profiles, are taken as primary and described axiomatically. The two  approaches do not seem to be directly related to each other in the  sense that one can be embedded in the other.  The modal logic arrow logic [11] is designed to reason about any  object that can be graphically represented as an arrow, and has   various modal operators for expressing properties of and relationships  between these arrows. In the preference aggregation logic jal(LK  )  we interpreted formulae in pairs of alternatives - which can be seen  as arrows. Thus, (at least) the preference aggregation variant of our  logic is related to arrow logic. However, while the modal operators  of arrow logic can express properties of preference relations such  as transitivity, they cannot directly express most of the properties  we have discussed in this paper. Nevertheless, the relationship to  arrow logic could be investigated further in future work. In   particular, arrow logics are usually proven complete wrt. an algebra.  This could mean that it might be possible to use such algebras as  the underlying structure to represent individual and collective   preferences. Then, changing the preference profile takes us from one  algebra to another, and a SWF determines the collective preference,  in each of the algebras.  8. DISCUSSION  We have presented a sound and complete logic jal for   representing and reasoning about judgment aggregation. jal is expressive:  it can express judgment aggregation rules such as majority voting;  complicated properties such as independence; and important results  such as the discursive paradox, Arrow"s theorem and Condorcet"s  paradox. We argue that these results show exactly which logical  capabilities an agent needs in order to be able to reason about   judgment aggregation. It is perhaps surprising that a relatively simple  language provides these capabilities. jal provides a proof theory, in  which results such as those mentioned above can be derived3  .  The axiomatisation describes the logical principles of judgment  aggregation, and can also be instantiated to reason about specific  instances of judgment aggregation, such as classical Arrovian   preference aggregation. Thus our framework sheds light on the   differences between the logical principles behind general judgment  aggregation on the one hand and classical preference aggregation  on the other.  In future work it would be interesting to relax the completeness  and consistency requirements of judgment sets, and try to   characterise these in the logical language, as properties of general   judgment sets, instead.  9. ACKNOWLEDGMENTS  We thank the anonymous reviewers for their helpful remarks.  Thomas Ågotnes" work on this paper was supported by grants  166525/V30 and 176853/S10 from the Research Council of   Norway.  10. REFERENCES  [1] K. J. Arrow. Social Choice and Individual Values. Wiley,  1951.  [2] K. J. Arrow, A. K. Sen, and K. Suzumura, eds. Handbook of  Social Choice and Welfare, volume 1. North-Holland, 2002.  [3] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic.  Cambridge University Press, 2001.  [4] E. M. Clarke, O. Grumberg, and D. A. Peled. Model  Checking. The MIT Press: Cambridge, MA, 2000.  [5] F. Dietrich and C. List. Arrow"s theorem in judgment  aggregation. Social Choice and Welfare, 2006. Forthcoming.  [6] C. Lafage and J. Lang. Logical representation of preferences  for group decision making. In Proceedings of the Conference  on Principles of Knowledge Representation and Reasoning  (KR-00), pages 457-470. Morgan Kaufman, 2000.  [7] J. Lang. From preference representation to combinatorial  vote. Proceedings of the Eighth International Conference on  Principles and Knowledge Representation and Reasoning  (KR-02), pages 277-290. Morgan Kaufmann, 2002.  [8] J. Lang. Logical preference representation and combinatorial  vote. Ann. Math. Artif. Intell, 42(1-3):37-71, 2004.  [9] C. H. Papadimitriou. Computational Complexity.  Addison-Wesley: Reading, MA, 1994.  [10] M. Pauly. Axiomatizing collective judgment sets in a  minimal logical language, 2006. Manuscript.  [11] Y. Venema. A crash course in arrow logic. In M. Marx,  M. Masuch, and L. Polos, editors, Arrow Logic and  Multi-Modal Logic, pages 3-34. CSLI Publications,  Stanford, 1996.  3  Dietrich and List [5] prove a general version of Arrow"s theorem  for JARs: for a strongly connected agenda, a JAR has the IND  and UNA properties iff it does not have the ND1 property, where  strong connectedness is an algebraic and logical condition on   agendas. Thus, if we assume that the agenda is strongly connected then  (ND ∧ UNA) ↔ ¬ND1 is valid, and derivable in jar. An interesting  possibility for future work is to try to characterise conditions such  as strong connectedness directly as a logical formula.  The Sixth Intl. Joint Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS 07) 573