A Proof-Theoretical View of Collective Rationality

1 Introduction

The problem of aggregating logically connected propositions into a collective rational outcome by means of a procedure that respects certain fairness desiderata has recently become an important topic in logic, AI and multiagent systems. Judgement Aggregation (JA) is a recent branch of social choice theory that originated from the study of the voting procedures that aggregate the opinions of judges in collegial courts [List and Pettit, 2002; List and Puppe, 2009]. JA has recently become an important theory for studying general aggregation of heterogeneous information [Dietrich and List, 2008a; Endriss, 2011]. Many results in JA show that it is not possible to aggregate individual rational judgements, usually expressed in classical propositional logic, by means of procedures that balance fairness and efficiency. For instance, the majority rule faces the so called discursive dilemmas [List and Pettit, 2002]: even if individual judgements are rational, the outcome that we obtain by majority may not be. Most of the impossibility theorems in judgement aggregation rely on a classical understanding of rationality, i.e. they are about individuals and societies that reason in (fragments of) classical logic. Moreover, most of the models assume that the individual rationality and the collective rationality are to be of a same logical type. The impossibility results in JA can be rephrased by saying that fair aggregation procedures do not preserve individual rationality. Furthermore, the possibility results that have been discussed in the literature on JA usually depend on severe restrictions of the language that the agents use to express their judgements, i.e. on the syntactic structure of the agenda, and not on the inferences that are permissible.

In this paper, we want to provide an analysis of discursive dilemmas and collective rationality by using a prooftheoretical view of logic and reasoning. In particular, we shall use the precise analysis of proofs and inferences provided by the sequent calculus for linear logic [Girard, 1995; Troelstra, 1992]. We intend to contribute to the JA framework along the two following directions. Firstly, we present a proof-theoretical treatment of collective rationality that shows precisely the reasoning steps that lead to collective contradictions. By pinpointing the inference rules that causes the dilemmas, we can extend the map of possibility and impossibility results to substructural reasoning. Secondly, we define a model in which individual rationality can be evaluated with respect to a certain logic L, whereas collective rationality can be defined with respect to a possibly different logic L′ .

The motivations for this work are twofold. On the one hand, reasoning in substructural logics has important application in modelling causal and non-monotonic reasoning or resource bounded inferences. On the other hand, the analysis of the paradoxes in social choice theory by means of a finegrained account of collective rationality suggests new diagnosis of collective inconsistencies.

Several logics for judgement aggregation have been discussed in the literature [List and Puppe, 2009; Endriss, 2011; Dietrich, 2010; 2007]. A preliminary investigation of the relationship between JA and linear logic has been presented in [Porello, 2012]. A significant related work is [Dietrich, 2007]. It includes results in JA that are obtained in general logics, i.e. with respect to a general notion of consequence relation. However, the results there do not apply directly to our analysis of substructural reasoning, since the consequence relations discussed in [Dietrich, 2007] are standard in the Tarskian sense, e.g. they are monotonic.

The remainder of this paper is organised as follows. In Section 2, we present the linear logic approach to proof-theory and we discuss some insights linking linear logic and collective reasoning. Section 3 contains our model of JA and presents a definition of group reasoning in proof-theoretical terms. Section 4 presents a number of possibility and impossibility results for the majority rule with respect to a number of substructural logics. Section 5 contains possibility results for aggregators that take sets of judgements that are rational wrt classical logic and return sets of judgement evaluated wrt fragments of LL. Section 6 extends the previous treatment to classes of aggregators characterised by important axioms in social choice theory. Section 7 sketches an application to preference aggregation. Section 8 concludes.

2 Background on Linear Logic and Sequent Calculi

Besides providing a logical modelling for resource bounded reasoning, Linear Logic (LL) can be considered an analysis of proofs in classical or intuitionistic logic that provides a closer inspection of inference rules. For example, the structural rules of classical sequent calculus [Troelstra and Schwichtenberg, 2000] weakening (W) and contraction (C) (Table 1) are no longer (globally) valid in LL, as they would allow us to delete or to add arbitrary copies of hypotheses. If we drop weakening and contraction, the rules that define logical connectives in sequent calculus have to be split into two classes: the additives, that combine two proofs by forcing to share the same context, and the multiplicatives, that combine proofs by non-sharing and making copies of the contexts. Accordingly, in LL there are two different types of conjunction, a multiplicative conjunction ⊗ (tensor) and an additive conjunction & (with), and two types of disjunctions, multiplicative � (parallel) and additive ⊕ (plus). Implications can be defined by means of disjunctions and negations as usual. For example, LL implication is A ⊸ B ≡ ¬A�B. Intuitively, LL captures resource bounded reasoning and non-monotonic inferences. For example, suppose the proper axiom e ⊢ c represents the inference "if I have one euro (e), then I buy one coffee (c)". In classical logic, one can infer by means of contraction e ⊢ e ∧ c, namely, that I still have one euro, besides having the coffee. By dropping contraction, LL captures a form of causality: the antecedent has to be consumed during the inferential process.

Given a set of propositional atoms A, the language of LL is defined as follows. 1

The sequent calculus for LL is presented in Table 1. A sequent is an expression Γ ⊢ ∆, where Γ and ∆ denote multisets of occurrences of formulas.

In what follows, we shall assume that the exchange rule (E) always holds. If we also assume that (W) and (C) hold, then the additive and multiplicative rules for the two conjunctions become equivalent. In that case, the propositional operators ⊗ and & collapse and the meaning of the conjunction is the classical one. The same holds for disjunctions. Thus, we shall use the standard notation, i.e. a∧b and a∨b, when we intend to refer to classical logic (CL), namely, in case we assume that the structural rules hold. 2 We denote LCL the language of classical logic.

1 We consider the multiplicative-additive fragment of LL. Another important part of LL is given by the exponentials, that allow for retrieving the usual classical inferences in a controlled way. We leave a discussion of the exponential for future work.

Linear logic is sound and complete wrt to its semantics [Girard, 1995]. Moreover, LL enjoys cut elimination. An analysis of the complexity of proof search for various fragments of LL is presented in [Lincoln et al., 1992].

2.1 Coalitional reasoning in LL

The idea of this work is to model a concept of group reasoning by using the awareness that LL provides of contexts and inferences. We shall model coalitions of agents that support formulas as contexts Γ in the sequent calculus. For example, if the group can infer a conjunction of two sentences, A and B, according to a given voting rule, this might have two interpretations. Firstly, there exists a single winning coalition Γ such that Γ ⊢ A and Γ ⊢ B, therefore Γ ⊢ A & B. Secondly, there exist two different winning coalitions such that Γ ⊢ A and ∆ ⊢ B, therefore Γ,∆ ⊢ A⊗B.

2 Without W and C, also negation behaves differently. For example, the ex falso quodlibet principle is no longer globally valid in linear logic. For sake of simplicity, we shall use a single notation for negation.

Consider the following famous example of discursive dilemma on the agenda of propositions {a, b, a ∧ b, ¬a, ¬b, ¬(a ∧ b)}. We want to take a closer look at the reasoning steps that are required in order to infer the contradiction. Consider the following profile, where three individuals express their opinions about propositions in the agenda as follows.

Each agent has a consistent set of propositions, however, by majority, the collective set {a, b, ¬(a ∧ b)} is not consistent. We can infer the contradiction in the collective set by reasoning in CL as follows.

We start with non-logical axioms {i1, i2} ⊢ a and {i1, i3} ⊢ b. By weakening, we introduce the conjunction of a and b by using the same coalition. Moreover, the group can infer ¬(a∧ b) as we have the axiom: {i2, i3} ⊢ ¬(a ∧ b). Therefore, the group is inconsistent wrt CL, as we can prove a∧b and ¬(a∧ b) by using the winning coalitions. This entails, by (cut), that we can prove ∅. If we drop W and C, the contradiction is not longer derivable. If the group reasons in LL, we have again axioms: {i1, i2} ⊢ a, {i1, i3} ⊢ b. Moreover, suppose we use the additive conjunction to interpret the third axiom: {i2, i3} ⊢ ¬(a & b). The group can infer a ⊗ b by using two different coalitions:

However, in LL a ⊗ b and ¬(a & b) are not inconsistent, because a ⊗ b, ¬(a & b) ⊬LL ∅. LL provides then a logical interpretation of the fact that there is no winning coalition for a ∧ b, whereas there are winning coalitions for a and b. Accordingly, we cannot infer a & b, since there is no single coalition that supports both a and b.

In the remainder of this paper, we want to show that this remark corresponds to more general properties of linear logic.

We shall discuss the following logics that are obtained by restricting the language of LL.

Moreover, we shall discuss the logics: L + (W) and L + (C) that are obtained by adding weakening or contraction to the logic L. Note that CL is equivalent to assuming MALL + (W) and (C).

3 The model

Let N be a (finite) set of agents. An agenda XL is a (finite) set of propositions in the language LL of a given logic L that is closed under complements. i.e. non-double negations. Moreover, we shall assume that the agenda does not contain tautologies or contradictions. We slightly rephrase the usual rationality conditions on judgment sets in terms of sequents derivability. A judgement set J is a subset of XL such that J is (wrt L) consistent (J ⊬L ∅), complete (for all φ ∈ XL, φ ∈ J or ¬φ ∈ J) and deductive closed (if J ⊢L φ and φ ∈ XL, φ ∈ J). Denote J(XL) the set of all judgement sets on XL. A profile of judgements sets J is a vector (J1, . . . , Jn), where n = |N|.

We shall discuss agendas defined in a number of languages and logics. We intend to model aggregators that take profiles of judgments sets that are rational according to a given logic L and return a set of judgement which can be evaluated with respect to a (possibly) different logic L′ . In case L and L′ are the same, we are in the standard situation in JA and we will discuss, in the next section, how aggregators behave wrt fragments of linear logic. In case the languages of L and L′ are different, we need to define a translation function from the language of L into the language of L′ . In general, a translation is just a function that maps formulas of one language into the other t : LL → LL′ . An aggregator is then a function F : J(XL)n → J(X ′L′ ) such that F is the composition of an aggregator in the standard JA sense (F ′ : L(X)n → P(X)) with a function T : P(XL) → P(X ′L′) that lifts t to sets of propositions: for J ⊂ XL, T(J) = {t(φ) | φ ∈ J} ⊂ X ′L′ . Thus, we have that F(J) = T(F ′ (J)) ⊆ XL′ . For example, the majority rule M : J(X)n → J(X ′L′) is defined as follows. Let Nφ = {i | φ ∈ Ji}, define M ′ : J(XL)n → P(XL) such that M ′ (J) = {φ ∈ XL | |Nφ| > n/2}; then, given a translation t, M(J) = T(M ′ (J)). Note that our definition allows for aggregators that return sets of judgments that are inconsistent wrt L and that may turn not to be inconsistent wrt L′ . That is why the codomain of F ′ is the powerset P(XL). We shall concentrate on the following additive translation of CL into LL: ADD : LCL → LLL. ADD is defined as follows: for a atomic, ADD(a) = a and ADD(¬a) = ¬a; for A in LCL, ADD(¬A) = ¬(ADD(A)), ADD(A ∧ B) = ADD(A)&ADD(B), ADD(A∨B) = ADD(A)⊕ADD(B) (i.e. we replace each classical connective with its additive counterpart). The translation reflects our interpretation of LL reasoning as coalitional reasoning. In particular, M : J(XCL)n → J(XLL) defined by M(J) = ADD(M ′ (J)) embeds classical formulas that are accepted according to the majority rule into LL by viewing them as additive formulas (i.e. they are collectively accepted because of a winning coalition that supports them). Thus, as we shall see, additives refer to the same winning coalition, whereas multiplicatives shall be used to reason about different winning coalitions.

3.1 Group Reasoning

In order to investigate collective rationality for a number of logics, we introduce the following notion of group reasoning. We say that Nφ is a winning coalition wrt F, and we denote it Wφ, iff φ ∈ F (J). We assume a distinguished set of propositional atoms i1, . . . in one for each agent in N. We model group reasoning in a given logic L as follows. We add to the language of L the set of atoms i1, . . . , in. We define nonlogical or proper axioms Wφ ⊢ φ for any φ ∈ F(J) . 3 The idea is that group reasoning is performed by using as assumptions the formulas that are elected according to F and keeping track of their winning coalitions throughout reasoning.

Definition 1 (Group reasoning). We say that the group infers a formula φ ∈ LL according to L iff, for some sequence of Wj ⊢ φj , there is a proof W1, ...,Wm ⊢L φ.

Thus, the notion of group reasoning depends on the logic L, on the profile, as well as on the aggregation rule that defines the non-logical axioms.

Definition 2. We say that group reasoning is consistent wrt L iff the sequent W1, . . . ,Wm ⊢L ∅ is not derivable in L for any sequence of winning coalition.

Our notion of group consistency corresponds to the standard model-theoretic view of consistency of a set of judgments J (i.e. there exists a valuation that makes the formulas in J true) as follows.

Fact 1. Group reasoning wrt L is consistent iff the set J = {φ | there are W1, . . . ,Wm s.t. W1, . . . ,Wm ⊢L φ} has a model.

For sound and complete calculi, 4 we have that J has a model iff J ⊬ ∅. By slightly extending the terminology in [Endriss et al., 2010], we introduce the following definition of safety of an agenda.

Definition 3. We say that an agenda XL is safe for a class of aggregators F wrt the logic L iff group reasoning wrt L is consistent for any F.

Safety means that there is no profile that leads to an inconsistent outcome wrt L when we aggregate sets by using an aggregator in a given class. In what follows we concentrate on the class consisting just of the majority rules, whereas in Section 6 we discuss other classes of aggregators. According to well-known results in JA [List and Puppe, 2009], the majority rule leads to inconsistency wrt classical logic iff the agenda XCL violates the so called median property: every minimally inconsistent set Y ⊆ XCL (i.e. an inconsistent set Y such that every subset of Y is consistent) has size at most 2. For example, the agenda containing {a, b, ¬(a ∧ b)} violates the median property. By Fact 1, on such agendas also group reasoning is consistent. Thus, our definition of group reasoning allows for rephrasing the standard JA results [List and Puppe, 2009].

Theorem 1. An agenda XCL is safe for the majority rule M : J(XCL)n → J(XCL) wrt CL iff XCL satisfies the median property.

4 Majority and Substructural Reasoning

We can now state an interesting possibility result. If we define agendas in ALL, then the majority rule is always consistent.

3 For sequent calculi with proper axiom, cf. [Troelstra and Schwichtenberg, 2000].

4 All the sequent calculi that we are using here are sound and complete with respect to the semantics of linear logic [Girard, 1995], [Troelstra, 1992].

In what follows, we shall assume that n is odd. The key property for stating this result is the following: (F) in additive linear logic (ALL) (i.e. just the rules for ¬, & and ⊕), every provable sequent contains exactly two formulas (e.g. A ⊢ B). This property has been stated in [Hughes and van Glabbeek, 2003] 5 . If we inspect the additive rules, we see that they cannot add any new proposition. Thus, since every proof starts with axioms A ⊢ A, every provable sequent contains two formulas of ALL. This easily entails that there are no minimal inconsistent subsets of size bigger than three in ALL (if J is inconsistent in ALL, then J ⊢ALL ∅). Thus, majority is safe for every ALL agenda.

Theorem 2. Any agenda XALL is safe for the majority rule M : J(XALL)n → J(XALL) wrt ALL.

It is interesting to stress that Theorem 2 is a possibility results wrt to a logic (i.e. a sound and complete logical calculus that enjoys cut elimination). Thus, the language restriction provided by ALL corresponds to allowing certain types of well-behaved inferences. Moreover, the same language is not safe, if we add more reasoning power. If we add weakening (W) to ALL, then there are agendas that are no longer safe for majority.

Proposition 1. Agendas X in ALL are not safe for majority rule M : J(XALL)n → J(XALL) wrt ALL + (W).

Proof. (Sketch) Take the agenda in ALL that includes {a, b, ¬(a & b)}. For Theorem 2, we know that majority is consistent wrt ALL. Consider a profile such that there are winning coalitions that provide the following axioms: W1 ⊢ a, W2 ⊢ b and W3 ⊢ ¬(a & b) (e.g. the profile in Section 2.1). In ALL + (W), we have the following proof.

Since W3 ⊢ ¬(a & b), group reasoning is inconsistent, as W1,W2,W3 entails a contradiction.

Weakening entails that A ⊗ B ⊢ A & B is provable [Girard, 1995]. Thus, by adding weakening, the group can infer that two different coalitions that support A and B (respectively) also support their additive conjunction. Basically, that is what happens, from a logical point of view, when we infer the contradiction in CL of the discursive dilemma. Note that the impossibility stated by Proposition 1 does not depend on the language of the agenda. Proposition 1 shows that language restrictions may not be sufficient to guarantee consistency, and that corresponds to the fact that there are minimally inconsistent sets of cardinality 3 in ALL + W.

By adding contraction (C) to ALL, agendas in ALL are still safe for the majority rules. The reason is that contraction can only shrink the number of formulas in a provable sequent. Thus, if there is no provable sequent with more that two formulas in ALL, the same holds for ALL + (C).

5 This property holds, provided we do not include the logical constants for true and false in the language of ALL. Moreover, it implies that for ALL is redundant to assume that the agenda does not contain tautologies or contradictions.

We consider now the majority rule defined on multiplicative agendas, namely M : J(XMLL)n → J(XMLL). In this case, we have no general possibility result and the median property characterises again safe agendas.

Theorem3. An agenda XMLL is safe forM : J(XMLL)n → J(XMLL) iff XMLL satisfies the median property.

Proof. (Sketch) For one direction, take for example the agenda {A,B, ¬A, ¬B,A ⊗ B, ¬(A ⊗ B)}. It violates the median property, as A, B, ¬(A⊗B) is minimally inconsistent and it has size 3 (i.e. A, B, ¬(A⊗B) ⊢ ∅). Take a profile with three individuals that provides proper axioms {i1, i2} ⊢ A, {i1, i3} ⊢ B and {i2, i3} ⊢ ¬(A ⊗ B). The profile makes group reasoning by majority inconsistent wrt MLL.

On the other hand, suppose XMLL satisifies the median property. For sake of contradiction, suppose that M(J) is inconsistent wrt MLL. Thus there is a minimal inconsistent set in M(J) with cardinality 2, as the agenda by definition does not contain contradictions. Thus, there are formulas A and B such that A,B ⊢MLL ∅. That means that there are two sequences of coalitions W1, . . .Wl andWl+1, . . .Wm such that W1, . . .Wl ⊢ A and Wl+1, . . .Wm ⊢ B. Since the intersection of Wj is not empty (|Wj| ≥ n/2), it entails that there is an individual such that his judgement set entails A and B, against the consistency of each individual judgement set.

5 Extending group reasoning

In this section, in order to meet the standard hypothesis in JA, we focus on the case in which individuals reason in CL and we will evaluate group reasoning wrt fragments of LL. By Theorem 2, we know that every agenda in ALL is safe for the majority rule. Thus, by using the additive translation ADD we know that agendas in CL are safe for M : J(XCL)n → J(XALL) with M(J) = ADD(M ′ (J)) wrt group reasoning in ALL.

Corollary 1. Any agenda XCL is safe for the majority rule M : J(XCL)n → J(XALL) wrt ALL.

We can extend the previous result, by showing that the majority is always consistent wrt reasoning in LL, provided the additive translation that we have introduced. We define the deductive closure of a set X wrt to L and we denote clL(X), as the set {A | X ⊢L A}.

Corollary 2. Every agendas XCL is safe for the majority rule wrt clMALL(M(J)).

Proof. (Sketch) By Theorem 2, M(J) is always consistent wrt ALL. If a set is consistent wrt a logic L, then its deductive closure wrt L is consistent (provided that the logic is sound). Since the rules of MALL are sound for sets of formulas in ALL, clMALL(M(J)) is consistent.

Note that the same argument cannot be applied to adding weakening. The reason is that (W) is not sound wrt MALL. Accordingly, Proposition 1 shows that adding weakening makes M(J) inconsistent. Theorem 2 shows that majority guarantee consistent outcomes, provided we keep track of the winning coalitions that support accepted formulas. Additive connectives presuppose a same winning coalition for a given formula A, whereas multiplicatives can be used in order to consistently combine formulas supported by different winning coalitions.

6 Axiomatic analysis

In the previous sections, we presented our treatment for a concrete aggregation procedure, i.e the majority rule. In this section, we discuss substructural reasoning wrt classes of aggregation functions defined by means of well-known axioms in JA and social choice theory. We shall discuss the following axioms that specifies classes of aggregators F. We say that an aggregator is complement-free iff and aggregator never returns A and ¬A. 6 Some of the axioms have been adapted in order to cope with aggregators that associate different logics.

Weak rationality (WR): F(J) is complete and complement-free wrt L.

Anonymity (A): For any profile J and permutation σ : N → N, F(J1, . . . , Jn) = F(Jσ(1), . . . , Jσ(n)).

Neutrality (N): For any A and B in XL and profile J, if for all i A ∈ Ji ⇔ B ∈ Ji, then t(A) ∈ F(J) ⇔ t(B) ∈ F (J).

Independence (I): For any A ∈ XL and profiles J, J′ ∈ J(XL)n , if A ∈ Ji ⇔ A ∈ J ′ i , then t(A) ∈ F(J) ⇔ t(A) ∈ F (J′ ).

Monotonicity (M): For any A ∈ XL and profiles J = (J1, . . . , Ji, . . . , Jn) and J′ = (J1, . . . , J ′ i , . . . , Jn) if A /∈ Ji and A ∈ J ′ i , then t(A) ∈ F(J) ⇒ t(A) ∈ F(J')

Acceptance-rejection neutrality (arN): For any A,B ∈ XL and any profile J ∈ J(XL)n , we have that if A ∈ Ji ⇔ B /∈ Ji for all agents i ∈ N, then t(A) ∈ F(J) ⇔ t(B) /∈ F(J).

(A) states that the aggregator does not favour any particular agent and (N) implies that it does not favour any particular proposition. (I) means that the outcome of F wrt a proposition A in two different profiles only depends on the patterns of acceptance in the two profiles. (M) implies that, by increasing the support of a proposition, F does not change its acceptance. (arN) has been introduced in [Dietrich and List, 2008b; 2009] in order to characterise aggregators in case of a weaker assumption of individual rationality, namely in case individual judgements sets are just assumed to be consistent. (arN) means that the aggregator is not biased either for or against the acceptance of any proposition.

By adapting May's theorem [May, 1952], it is known that the majority rule is characterised by the following axioms [List and Puppe, 2009; Endriss et al., 2010]

Proposition 2. F : J(XL)n → J(XL) is the majority rule iff F satisfies (WR), (A), (N), (I) and (M).

Since the notion of weak rationality does not depend on a particular logic, just on the minimal assumption that a logic contains some syntactic form of negation, the characterisation holds also for the majority rule defined on any L that we have previously introduced.

6 This condition is weaker than consistency as it excludes just inconsistent sets that include a formula and its syntactic negation.

By Theorem 2, we know that, wrt to reasoning in ALL, there are procedures that satisfy (WR), (A), (N), (I) and (M), namely the majority rule. We discuss possible extension of such class by weakening some of the axioms that characterise majority. In particular, since MLL or ALL + W are not safe for majority, it means that they are not safe for any class of aggregators that includes majority. Thus, we focus on ALL.

Proposition 3. Agendas in XALL are not safe for aggregators F satisfying (WR), (A), and (N).

Proof. We show that there is an agenda in ALL and an aggregator that satisfies the axioms above that return an inconsistent outcome. Take and agenda in ALL that consists of {a, ¬a, a & b, ¬(a & b)}. Consider a profile with 3 agents such that agent J1 = {¬a, ¬(a & b)}, J2 = {a, a & b} and J3 = {a, ¬(a & b)}. Take the aggregator F such that A ∈ F(J) if 0 or 1 agents has A ∈ Ji and A /∈ F(J) if more than one agent has A ∈ Ji. F is clearly satisfies (WR), (A), and (N). Thus, there are winning coalitions: {i1} ⊢ ¬a, {i2} ⊢ a & b and ¬a, a & b ⊢ALL ∅.

By analogous arguments, we have the following result.

Proposition 4. Agendas in XALL are not safe for aggregators F that satisfy (WR), (A), and (I).

Uniform quota rules are characterised by (A), (N), (I) and (M) [Endriss et al., 2010]. Again, ALL is not safe for this class.

Proposition 5. Agendas in XALL are not safe for aggregators F satisfying (A), (N), (I) and (M).

It is enough to set the threshold for acceptance to q ≥ 1 (i.e. take the union of all formulas that are accepted by some agent) to make the collective set inconsistent on any agenda in ALL. Therefore, reasoning in ALL does not provide new possibility results for classes of aggregators. In order to guarantee consistency, we need then to apply further restrictions on the agenda in ALL that strengthen the median property [Endriss et al., 2010]. We conclude this section with a positive result concerning acceptance-rejection neutrality. We focus on the case in which individual judgements sets are just assumed to be consistent (i.e. they do not need to be complete or deductively closed). Denote Jc(XL) the set of consistent judgement sets wrt L. Dietrich and List [2009] have shown that every aggregator that is acceptance-rejection neutral and always returns consistent sets of judgement must be a dictatorship of some individual (namely, the aggregator always copies the judgement set of some individual). The theorem does not hold for the majority rule, provided we evaluate group reasoning wrt to ALL or its linear closure.

Proposition 6. The majority rule M : Jc(XCL)n → Jc(XALL) is an acceptance-rejection neutral aggregator that is safe wrt ALL.

7 An application to preference aggregation

We want to sketch an application of our results to preference aggregation. It is possible to express preference orderings in JA by means of suitable sets of propositions [Dokow and Holzman, 2010; Grandi and Endriss, 2011]. For example, one introduces a propositional atom pa>b for each pair of alternative such that a > b according to the preference order. The usual axioms that characterise preference orderings can be expressed by means of integrity constraint that are written in classical logic. For example, transitivity amounts to assuming a set of constraints of the form: pa>b ∧pb>c → pa>c. Moreover, pa>b and pb>a behave as negations. Accordingly, it is possible to view a Condorcet's paradox as a case of discursive dilemma for a suitable agenda of propositions in CL.

The set obtained by majority violates the integrity constraint imposed by transitivity. We apply our analysis of group reasoning to preference aggregation as follows. We can represent transitivity constraints by means of proper axioms in two ways: additively, pa>b & pb>c ⊢ pa>c and multiplicatively, pa>b ⊗ pb>c ⊢ pa>c. According to our previous analysis, the multiplicative interpretation would make group reasoning inconsistent, as we can infer {i1, i2}, {i1, i3} ⊢ pa>b ⊗ pb>c which by transitivity entails {i1, i2}, {i1, i3} ⊢ pa>c against {i2, i3} ⊢ ¬pa>c. However, the additive version of transitivity does not cause inconsistencies. Intuitively, the additive axiom is weaker: it requires that transitivity holds only in case there exists a single winning coalition supporting both pa>b and pb>c. The additive interpretation of transitivity suggests a narrower account of collective rationality: reasoning applies only when the same group accepts the premises.

8 Conclusion

We have analysed collective rationality by means of the proof theory of linear logic. By inspecting fragments of substructural reasoning, we have shown that is possible to provide new possibility results. In particular, ALL provides general safety results. It is worth stressing that the distinction between the possibility result for ALL and the impossibility result for ALL + W does not depend on the language of the agenda, rather it depends on the fine properties of reasoning encoded in sequent calculus. Moreover, we have modelled aggregators that take judgements sets in CL, just as in the standard JA, and we have shown that it is safe to view collective rationality in ALL or MALL. Thus, if we stick to our intuitive interpretation of LL that views additives as referring to a single winning coalition and multiplicatives as combining possibly different winning coalitions, we have a consistent interpretation of collective rationality. We have shown that our safety results are no longer valid for weaker classes of aggregator, thus for them substructural logics do not provide an interesting way out. We believe that the significance of this approach is that proof theory allows for pinpointing the logical causes of inconsistency and for exploring the relationships between axioms of social choice theory and inference rules. We have pointed at possible applications in preference aggregation, once we express the constraints on preferences as formulas in our logics. Future work shall investigate in detail this aspects.