A Modal Logic for Social Welfare Functions*

Hu Liu

Abstract.The focus of social choice theory is on frameworks of aggregating individuals’preferences into a group preference.We present in this paper a modal logic for preference aggregation.The logic is a direct and easily readable formalization of social welfare functions.A standard n-ary modal box is used to characterize n-ary functions on the set of linear orders over alternatives.We show that all possible properties of social welfare functions can be expressed by this simple modal language.We give a complete deductive system for the logic.We present a syntactic proof of Arrow’s impossibility theorem of social welfare functions.

1 Introduction

Social choice theory is a theoretical framework originated in welfare economics and voting theory for analysis of collective decision making.It deals with the problem of combining individual preferences into a decision of a group.The study of social choice theory has been a multi-disciplinary research area.The main part of social choice theory is in Welfare Economics,where several social choice scholars have been awarded the Nobel Prize in Economics(Arrow in 1972,Sen in 1998,Maskin in 2007,Sharpley in 2012).Social choice theory has also been an influential methodology in studying voting and election in Politics,collective decision and multi-criteria decision in Management Science,multi-agent systems in Artificial Intelligence,and distributed systems in Computer Science.

The core of social choice theory is the study of the so-called social welfare functions,which is a function takes as input a set of linear orders over a given set of alternatives,one of each representing a voter’s opinion towards these alternatives,and returns a linear order over the set of alternatives,representing the group preference.Much attention in social choice theory has been on a general approach to this preference aggregation function,which was introduced by K.Arrow in 1951([2]).

Though the root of social choice theory can be traced back to the thirteenth century,it is generally acknowledged that the modern social choice theory was started by Arrow’s seminal monograph“Social Choice and Individual Values”([2]).In his book Arrow introduced an axiomatic method to discuss properties of social welfare functions.He identified certain axioms that are seemingly plausible properties of social welfare functions.His famous impossibility theorem stated that,surprisingly,if there are three or more alternatives,then no social welfare function can satisfy all of these“good”axioms.

Though Arrow and other scholars made use of axiomatic method and logical terms such as“axiom”and“consistency”,frameworks of social choice theory had not been formalized by a logical language until a few years ago.Recently there has been a growing interest in the cross-disciplinary study of logic and social choice theory.Researchers in this new area have either extended methodologies of social choice theory to logical frameworks([7,9,14,18,19,20,27]),or studied problems of social choice theory by logical methods and automated reasoning techniques([1,4,5,8,12,15,17,21,22,25,26,28]).The current paper is on the second approach.We will review some work of this approach in Section 4.

Much attention in this approach has been on modelling the Arrovian framework of social welfare functions into a logical formalism.In [15],Arrow’s theorem was reduced to the problem of verifying that a certain set of first-order formulas does not have a finite model.In[25],by replacing quantifiers with conjunction or disjunction,Arrow’s theorem was represented in propositional logic,and an instance of the theorem(with two individuals and three alternatives)was verified by a SAT solver.Higherorder logic was used in[28]and[21],where proofs of Arrow’s theorem were coded and verified by interactive theorem provers.

Modelling aggregation functions in the general framework of modal logic is another promising direction in this area,where tailor-made modal logics were designed to represent properties of aggregation functions.Pauly in [22]and [23]gave an axiomatization of majority voting with a simple modal logic.In [1],Ågotnes et al.defined an expressive modal language that can represent Arrow’s theorem,Condorcet’s paradox,and so on.Troquard et al.in[26]introduced a logic specifically designed to reason about the strategy-proofness of social choice functions.By using a fragment of the modal logic in[26],Cinà and Endriss presented a syntactic proof of a variant of Arrow’s theorem for social choice functions in [5,6].Jiang et al.in [17]presented a modal logic for representing and reasoning about reason-based social choice.It should be noted that most of these logics were designed for judgment aggregation([19]),which is a more general framework than preference aggregation.Since judgment aggregation subsumes preference aggregation in a natural way,these logics can be easily adapted for representing Arrow’s theorem and other traditional problems in the area.

For an introduction to social choice theory,[10]is a widely used introductory text.A nice review of logic methods in social choice theory can be found in[8].

This paper defines a simple modal logic for speaking about social welfare functions.The logic is a standard polyadic normal modal logic with ann-ary modality directly encodinging ann-ary social welfare function.The domain of a model is the set of all possible preferences over alternatives (all linear orders over alternatives),in which ann-ary social welfare function is directly represented by an (n+1)-ary relation.Then-ary modal box to characterize the(n+1)-ary relation,and therefore characterize then-ary social welfare function.The logic is therefore more intuitive than the existing ones.Also,by using then-ary modality we avoid having to mention explicitly individuals in the formal language.We show that the logic is expressive enough to represent all possible properties of social welfare functions.We give a complete deductive system for the logic.Therefore,in principle all impossibility theorems can be coded and syntactically proved in the logic.We present a syntactical proof of Arrow’s theorem in the paper.There has been such a proof for a variant of Arrow’s theorem for social choice functions ([5,6]).Ågotnes et al.in [1]gave a syntactic proof of the so-called“Strict Neutrality Lemma”,which is an important step of a proof of Arrow’s theorem([11]).

The rest of the paper is structured as follows.We define the logic’s syntax and semantics in the next section.Also in the next section we present the logic’s expressiveness and axiomatization.A syntactic proof of Arrow’s theorem is given in Section 3.Related work is discussed in Section 4.Section 5 is the conclusion of the paper.

2 Aggregation Logic

2.1 Social Welfare Functions

Social choice theory deals with the problem of aggregating individuals’opinions into a single collective view of a group.It is not only a central problem of certain research areas(Welfare Economics,for example),but also a familiar scenario in our everyday life (a group making a decision on which restaurant to go,for example).In social choice theory,the problem is usually represented by a setNof individuals,each with a preference over a setXof alternatives,making a decision on a group preference overX.A preference is usually a linear order(strict or not strict)overX.We will take the standard view of a strict linear order.

Unless otherwise stated,in this paper we fix a finite nonempty setN={1,...,n}of individuals(voters),and a finite nonempty setX={x1,...,xm}of alternatives(candidates).We letx,y,zrange overX.Let≻stand for alinear order(an irreflexive,transitive and trichotomy binary relation)onX.A statementx ≻ymeans“rankingxabove y”.The set of all linear orders onXis denoted byL(X).We sometimes write a subscript to indicate it being an individual’s preference.For an individuali∈N,≻i∈L(X)represents individuali’s preference over alternatives(herballot).Aprofileis ann-tuple(≻1,...,≻n)∈(L(X))n,one ballot for each individual.Asocial welfare function(SWF)is functionF:(L(X))n →L(X)that maps each profile to a single linear order over alternatives,representing the group’s preference.

Finding the best aggregation rule(the best SWF)has been an old problem that can be traced back to Condorcet’s and Borda’s work in seventeenth century.Such earlier work focused on finding and justifying specific aggregation rules.It was K.Arrow’s work in 1951 ([2])that first provided a systematical method to study aggregation rules,and founded the modern social choice theory.Arrow focused on certain general properties of SWFs and the relationship among these properties.He identified three plausible properties:Non-Dictatorship,Pareto Optimality,and Independence of Irrelevant Alternatives.LetFbe a social welfare function:

·Non-Dictatorship(ND):Fsatisfies(ND),if there is no individualisuch that for all profiles(≻1,...,≻n),we haveF(≻1,...,≻n)=≻i.

·Pareto Optimality(PO):Fsatisfies(PO),if for any profile(≻1,...,≻n)and any alternativesxandy,x ≻i yfor alli∈Nimplies thatx ≻y,where≻=F(≻1,...,≻n).

·Independence of Irrelevant Alternatives(IIA):Fsatisfies (IIA),if given two alternativesxandyand two profilesandif for all individualsi,thenx ≻1yiffx ≻2y,where

Arrow’s impossibility theorem states that the three properties are inconsistent together if there are three or more alternatives.

Theorem 2.1.If there are three or more alternatives,no SWF satisfies ND,PO and IIA.

2.2 Aggregation Logic:Syntax and Semantics

We define an aggregation logic(AL)in this paper.The logic is built on a given set of individualsN={1,...,n}and a given set of alternativesX={x1,...,xm}.Throughout the paper,we letl(possibly with subscripts)range overL(X).

Anatomis a statement in the formx ≻y,wherex,y∈X.LetAt={x ≻y|x,y∈X}denote the set of all atoms.The set of formulas is defined by the following grammar:Wherepranges over atoms,

Thus,it is a standard modal language built on specific atoms.We will writeleither semantically for a linear order inL(X),or syntactically for a set of atoms(or a conjunction of atoms)that defines the linear order.For example,lcan stand either for a linear orderx ≻y ≻zor for a set of atoms{x ≻y,y ≻z,x ≻z}.Its meaning should be clear by context.

Definition 2.2.Given a SWFF,themodelofFis a pair MF=(L(X),R),whereRis an(n+1)-ary relation onL(X)such thatR(l,l1,...,ln)if and only ifF(l1,...,ln)=l.Eachl∈L(X)is called a state of the model.

From now on,a model always means a model for a social welfare function.We will only consider models for social welfare functions in this paper.A model ofFis nothing butFitself.We may simply write M for MFif the subscript is irrelevant.We can further rewrite a model in the form of a standard Kripke model:Given a model M=(L(X),R),let N=(W,Q,V),whereWis a set of states with|W|=|L(X)|,Qis an+1-ary relation onWsuch thatQww1...wnif and only ifRf(w)f(w1)...f(wn)withfbeing any given one-one mapping fromWtoL(X),andVis a valuation function such thatx ≻y∈V(w)iffx ≻yis true in the linear orderf(w).The two forms of models are semantically equivalent.

Definition 2.3.Given a model M=(L(X),R),a statelin the model,and a formulaφ,M,l|=φis read as thatφis satisfied(or true)atlin M,and is defined as follows:

M,l|=x ≻yiffx ≻yis a true statement in the linear orderl.

M,l|=¬φiff M.

M,l|=φ∧ψiff M,l|=φand M,l|=ψ.

M,l|=Aφiff M,l′|=φfor alll′∈L(X).

M,l|=□(φ1,...,φn)iff for alll1,...,lnwithR(l,l1,...,ln),there exists ani∈Nsuch that M,li|=φi.

Formulaφis true in model M,denoted by M|=φ,if M,l|=φfor every statelin M.Formulaφis valid,denoted by|=φ,if M|=φfor every model M.

Other Boolean connectives are defined as usual.LetEφ=df ¬A¬φ.Thenary operator□is a standardn-ary modal box.The diamond is defined as usual:◇(φ1,...,φn)=df ¬□(¬φ1,...,¬φn).Thus,

·M,l|=◇(φ1,...,φn)iff there existl1,...,lnsuch thatR(l,l1,...,ln)and M,li|=φifor alli∈N.

The intuitive meaning of□is not clear.◇,however,has a clear meaning.An aggregation procedure can be naturally coded by a formula◇(l1,...,ln)∧l,meaning that individuals’preferencesl1,...,lnare aggregated into a group preferencel.We shall use◇more often than□.The polyadic modality as defined is a normaln-ary modal box.

OperatorAis an universal modality whose truth condition depends on all states of a model.Some modal logicians tend to avoid using the operator.For one reason,a modal language with an universal operator does not have the locality property,which is one of the basic characteristics of modal logic.For another reason,adding an universal operator in many cases will increase computational complexity ([16]).There is,however,also support for the usefulness of universal operators([13]).The current framework,as well as the general task of modelling SWFs by modal logic,is a good example where universal operators is a natural and helpful tool,because typical properties of SWFs contain quantification over all alternatives,all ballots or all profiles.

2.3 Expressiveness

The current framework is designed to represent and reason about properties of aggregation functions.To what extent can a logic express such properties? Can a logical language express all possible properties of social functions? Can a logical language characterize every social function,or equivalently,can a logical language distinguish every pair of different social functions? These questions are about the expressive power of a logical language,one of the most important features of a logical framework.

Definition 2.4.Suppose thatLis a logic for social functions,and the notation MF|=L φis proper defined in the logic,where MFis the model built for a social functionF.We say that the logicLisexpressively completeif for any social functionF′,there is a formulaφinLsuch that MF|=L φif and only ifF=F′.In this case,φis called thecharacterizing formulaforF′.

Thus,a logicLis expressively complete if it can characterize any given social function,or in another words,there is a characterizing formula for each social function that can distinguish it from other social functions.Since a domain of discourse in this context is always finite,expressive completeness means that a logic is able to express all possible properties of social functions.This is certainly an important feature for a logic of social functions.It will be particularly useful if we use a logic not only for coding known theorems of social functions or verifying existing proofs of theorems,but also for finding new theorems and proofs.Expressive completeness will guarantee a thorough searching procedure.

Existing logical frameworks of social functions showed the expressive power of their logics by examples.Usually,they showed that certain important properties of social functions can be expressed in their logics.The notion of expressive completeness has not been discussed in literature.

The following theorem shows that the current logic is expressively complete.

Theorem 2.5.LetMF stand for the model built for a social welfare function F.Let φF be a formula of AL defined as that

Then φF is the characterizing formula of F:For any SWF F′,

ProofThe theorem is easy to check and is omitted. □

Though a characterizing formula defined in Theorem 2.5 seems obvious and its representation is not succinct,it shows that in principle our logic is able to express all possible properties of social welfare functions:Every property can be represented by a conjunction of characterizing formulas of SWFs that satisfy the property.

2.4 Axiomatization

The deductive system ofAL(with parametersNandX)consists of the following axioms and rules:

Axioms (IR),(Tran)and (L)guarantee that≻is a strict total order.Axioms (K□),(KA),and rule(Nec)guarantee thatAand□are normal modal operators.Note that the necessity rule for□,namelyis not included because it can be derived by(Nec)and(Incl).Axioms(T),(4)and(B)guarantee thatAcorresponds to an equivalent relation of a model.Theaxiom of inclusion(Incl)deals with the relationship betweenAand□.

The rest axioms are axiom schemes wherelranges overL(X).Theaxiom of occurrence(Occu)states that each linear order inL(X)occurs in a model as a state at least once.Theaxiom of universal domain(UD)says,for any givenl1,...,ln,there exists a state,sayl,such thatRll1,...,ln.That is,F(l1,...,ln)=l.(UD)guarantees that a SWF is defined on all possible profiles.Theaxiom of partial function(PF)says,if a state labelled bylis such that there arel1,...,lnwithRll1,...,ln,then any state that is related withl1,...,lnin the same way must also be labelled byl.By(PF),the output of a SWF is always unique on any input profile,and therefore a SWF is a partial function.Axioms(UD)and(PF)guarantee that a SWF is indeed a function.The condition that each linear order inL(X)can occur only once in a model cannot be guaranteed by an axiom.Instead,we have theaxiom of uniformity(Unif)that states a weaker condition.(Unif)says,if a state labelled bylis such that there arel1,...,lnwithRll1,...,ln,then any state labelled bylmust be related withl1,...,lnin the same way.The axiom (Unif)guarantees,if a linear orderloccurs more than once,all occurrences oflshould have similar behavior in the model,in the sense that as an output of a SWF,they share the same input profiles.

Notions of a proof(⊢φ)and a deduction(Γ⊢φ)are defined as usual.A set of formulas Γ is consistent if Γ⊢φ∧¬φfor noφ.A formulaφis consistent if{φ}is.A set of formulas Γ is a maximal consistent set(MCS)if Γ is consistent and any super-set of Γ is not.

Theorem 2.6(Soundness).For any formula φ,if ⊢φ then|=φ.

ProofBecause a model inclues every linear order overX,axiom(Occu)is valid.Axioms(UD)and(PF)hold because then+1-ary relationRof a model is a function.Axiom (Unif)holds because each linear order occurs only once in a model.Other axioms and rules are rountine. □

The rest of this subsection is for a completeness proof of the system.The canonical model of the deductive system is a tupledefined as usual:Wcis the set of all MCSs;is an (n+1)-ary relation onWcsuch thatiff for all formulas□(φ1,...,φn)∈w,there is anisuch thatφi∈vi,or equivalently,iff ifφi∈vifori∈Nthen◇(φ1,...,φn)∈w;is a binary relation onWcsuch thatiff for all formulasAφ∈w,φ∈v;V cis a function that assigns to each atom a set of MCSs such that for each atomx ≻y,w∈V c(x ≻y)iff(x ≻y)∈w.

Both□andAare normal modalities:we have their K-axioms and necessity rules in the system.Therefore,a truth lemma can be proved by standard techniques:

Lemma 2.7.(i)(Existence Lemma)For any w∈Wc,if ◇(l1,...,ln)∈w,thenthere are v1...vn such thatand l1∈v1,...,ln∈vn.

(ii)(Truth Lemma)For any w∈Wc and any formula φ,Mc,w|=φ iff φ∈w.

ProofThe existence lemma and the truth lemma are verified by a standard proof and are omitted. □

The canonical model Mchas the following properties:

Lemma 2.8.(i)For each w∈Wc,At∩w∈L(X),i.e.the set of atoms in each state defines a linear order.

(iii)Ifthenwvi for every i∈N.

(iv)For any l∈L(X),there is a v∈Wc such that l∈v.(The first l is a linear order,and the second l is a set of atoms.)

(v)For any l1,...,ln∈L(X),there is a v∈Wc such that for some v1,...,vnwith l1∈v1,...,ln∈vn we have

(vi)Ifandthen l∈w implies l∈w′.

(vii)Ifand l∈w,l∈w′,l1∈v1,...,ln∈vn,then therearesuch thatand

ProofIt is straightforward that(i)holds by axioms(IR),(Tran)and(L).(ii)is direct by axioms(T),(4)and(B).(iii)holds by axiom(Incl).

For(iv),letlbe any linear order inL(X).Then by axiom(Occu),El∈wfor any MCSw.Then by definition,there is avsuch thatandl∈v.

For (v),letl1,...,ln∈L(X).By axiom (UD),E◇(l1,...,ln)∈wfor any statew.Then there is avwithand◇(l1,...,ln)∈v.Then by definition,there arev1,...,vnsuch thatandl1∈v1,...,ln∈vn.

For (vi),suppose its premise holds andl∈w.Byl1∈v1,...,ln∈vnandBy axiom(PF),A(◇(l1,...,ln)→l)∈w.ByByand◇(l1,...,ln)∈w′.Thus,l∈w′.

For(vii),suppose its premise holds.Similarly,we have◇(l1,...,ln)∈w.Then by axiom(Unif),A(l →◇(l1,...,ln))∈w.Then by(l →◇(l1,...,ln))∈w′.Then◇(l1,...,ln)∈w′.By the existence lemma (Lemma 2.7-(i)),there aresuch thatand

Lemma 2.8-(v)states that each profile is aggregated into a state(a linear order that stands for the state)at somewhere in the model.Note that,because anl∈L(X)may occur more than once inWc,(vi)does not guaranteeis a partial function.

The canonical model Mcis not a legitimate model.There are two defects:(1)is not an universal relation;(2)A linear order may occur more than once in Mc.As a consequence,is not a function onWc.

For anyu∈Wc,let Mu=(W,R□,RA,V)be the submodel of Mcgenerated byuusing the binary relationBy Lemma 2.8-(iii),Muis also a generated model of Mcwith respect toStandard techniques can be adapted to show the truth maintenance of generated models.Therefore a truth lemma also holds for Mu:

Lemma 2.9.For any w∈W and any formula φ,Mu,w|=φ iff φ∈w.

ProofOmitted. □

It is easy to check that Muhas the corresponding properties of Lemma 2.8:

Lemma 2.10.(i’)For each w∈W,At∩w∈L(X).

(ii’)RA is an universal relation,i.e.RA=W ×W.

(iii’)If R□wv1...vn then RAwvi for every i∈N.

(iv’)For any l∈L(X),there is a v∈W such that l∈v.

(v’)For any l1,...,ln∈L(X),there is a v∈W such that for some v1,...,vn with l1∈v1,...,ln∈vn we have R□vv1...vn.

(vi’)Ifandthen l∈w implies l∈w′.

(vii’)If R□wv1...vn and l∈w,l∈w′,l1∈v1,...,ln∈vn,then there aresuch thatand

ProofOmitted. □

Muis also not a legitimate model because a linear order may occur more than once in Mu.However,according to the next lemma,Muis semantically equivalent to a legitimate model.

Let M=(L,R)be obtained from Muby lettingL={l|l∈w,w∈W},andRll1...lniff for somew,v1,...,vnwithR□wv1...vn,l1∈v1,...,ln∈vnandl∈w.

Lemma 2.11.(i)Mis a model.

(ii)For any w∈W,any l∈L(X),and any formula φ,Mu,w|=φ iffM,l|=φ,wherel∈w.

ProofFor (i),by 2.10(iv’),L=L(X).By the definition of M and 2.10-(vi’),Rll1...lnandRl′l1...lnimplies thatl=l′.By 2.10(v’),for anyl1...ln∈Lthere is alwithRll1...ln.ThenRas defined is a function onL.Thus,M is a model.

We prove(ii)by induction on the structure ofφ.We only show the case whenφ□(φ1,...,φn).Suppose that Mu,w □(φ1,...,φn).That is,Mu,w ◇(¬φ1,...,¬φn).Then there existv1,...,vnsuch thatR□wv1...vnand Mu,vi ¬φifor all 1≤i ≤n.Letl1∈v1,...,ln∈vn.By inductive hypothesis,M,li ¬φifor all 1≤i ≤n.By the definition ofR,Rll1...ln.Thus,M(φ1,...,φn).

For the other direction,suppose that M(φ1,...,φn).Then there existl1...lnsuch thatRll1...lnand M,li ¬φifor all 1≤i ≤n.By the definition ofR,there existw′,v′1,...,v′nsuch thatR□w′v′1...v′n,l∈w′,andBy 2.10(vii’)andl∈w,there existv1,...,vnsuch thatR□wv1...vnandl1∈v1,...,ln∈vn.By inductive hypothesis,Mu,vi ¬φifor all 1≤i ≤n.Then Mu,w □(φ1,...,φn). □

Theorem 2.12(Completeness).For any formula φ,ifφ then ⊢φ.

ProofIt suffices to show that any consistent formulaφis satisfiable in a model.Letube a maximal consistent set such thatφ∈u.By Lemma 2.7,Mc,uφ.Then by Lemma 2.9,Mu,u|φ.Then by Lemma 2.11,M is a model and M,wherel∈u. □

3 Arrow’s Theorem

3.1 Representations of Social Choice Properties

Because the usage of◇in the language resembles a SWF,properties of SWFs can be represented in the logic,as expected,in a direct,easily readable way.Let⊤df p∨¬p.The three properties in Arrow’s theorem can be respectively expressed byALformulasND,PO,andIIAas follows:

·NDE(x ≻y∧◇(⊤,...,y ≻x,...,⊤)),wherey ≻xoccurs in thei-th argument place of◇,and⊤occurs in all other argument places of◇.

·POA(◇(x ≻y,...,x ≻y)→(x ≻y)),wherex ≻yoccurs in all argument places of◇.

·IIA(E(◇(φ1,...,φn)∧φ)→A(◇(φ1,...,φn)→φ)),whereφ1,...,φnandφare in the formx ≻yory ≻x.

Theorem 3.1.Let a modelM(L(X),R)be built from a SWF F.Then

(i)M

(ii)M

(iii)M

ProofFor(i),NDsays,for each individuali,there is a pair of alternativesxandysuch that the formulax ≻y∧◇(⊤,...,y ≻x,...,⊤)is true at some point,sayl.M,l|=◇(⊤,...,y ≻x,...,⊤)means that there arel1...lnsuch thatRll1...lnand M,li|=y ≻x.Because we have also M,l|=x ≻y.Thus,individualiis not a dictator:y ≻xis her preference in the profile(l1...ln),but not in the aggregation preferencel.

The proof of(ii)is straightforward.

For(iii),Suppose thatFhas the IIA property.Suppose M|=E(◇(φ1,...,φn)∧φ).Then there is al∈L(X)such that M,l|=◇(φ1,...,φn)∧φ.Then M,l|=φand there arel1,...,lnsuch thatRll1...lnand M,l1|=φ1,...,M,ln|=φn.Letl′be any linear order inL(X)with M,l′|=◇(φ1,...,φn).We show that M,l′|=φ.By M,l′|=◇(φ1,...,φn),there aresuch thatand MThen by IIA property,φ∈liffφ∈l′.Then,M,l′|=φ.We have M,l′|=◇(φ1,...,φn)→φ.Becausel′is an arbitrary state,M|=A(◇(φ1,...,φn)→φ).For the other direction of (iii),the proof is similar. □

As shown in Section 2.3,all properties of social welfare functions can be coded by the current language.Therefore,all impossibility theorems can be coded and syntactically proved.We give a syntactic proof of Arrow’s theorem in the next subsection as an example.

3.2 A Syntactic Proof of Arrow’s Theorem

Arrow’s impossibility theorem with fixedNandXcan be expressed inALby a formula:PO∧IIA →¬ND.Arrow’s original proof can be seen as a semantic proof of the theorem.By Theorem 3.1 and the completeness of the deductive system,there must have a syntactic proof of the theorem,i.e.we have⊢Pare∧IIA →¬ND.We show such a proof in this subsection.The proof itself is a tedious exercise.It,however,shows the naturalness of the current language.The syntactic proof is easily readable in the sense that it resembles the idea and the structure of a well-known proof of Arrow’s theorem by Sen([24]).

The rule and the formulas in the following lemma are all derivable in the deductive system.We will use these facts in the syntactic proof.

Lemma 3.2.(i)From ⊢φ→ψ to infer ⊢◇(φ1,...,φ,...,φn)→◇(φ1,...,ψ,...,φn).

(ii)From ⊢φ →ψ and ⊢Eφ to infer ⊢Eψ.

(iii)⊢A(φ →ψ)∧Eφ →Eψ.

(iv)⊢◇(...,⊤,...,)→(◇(...,φ,...)∨◇(...,¬φ,...),where φ and ¬φ are in the same argument place of ⊤.

(v)⊢Eφ →E(φ∧ψ)∨E(φ∧¬ψ).

ProofOmitted. □

We resemble Sen’s informal proof of Arrow’s theorem([24]).We first formalize the notion of decisiveness,the key notion in Sen’s proof.For a nonempty coalitionG ⊆N,let◇(G(φ),φi1,...,φi|NG|)stand for◇(φ1,...,φn),whereφj=φfor eachj∈G,andφk∈{φi1,...,φi|NG|},one for eachk∈NG.Note that,the order ofG(φ),φi1,...,φi|NG|in◇(G(φ),φi1,...,φi|NG|)may not be their real order in the well-formed formula◇(φ1,...,φn)represented by◇(G(φ),φi1,...,φim).It only means,for allj∈G,φtakes thej-th argument place of◇,and other argument places are taken byφi1,...,φi|NG|.Similarly,let◇(G(φ),G′(ψ),φi1,...,φi|N(G∪G′)|),where bothGandG′are nonempty coalitions andG∩G′=Ø,stand for◇(φ1,...,φn),in whichφj=φfor allj∈G,φh=ψfor allh∈G′,andφk∈{φi1,...,φi|N(G∪G′)|},one for eachk∈N(G ∪G′).

Definition 3.3.Let

Theorem 3.4(Arrow’s Theorem).If AL is built on a SWF with three or more alternatives,then ⊢IIA∧Pare →¬ND.

A full syntactic proof will be lengthy and unnecessary.We shall omit certain obvious steps.

Letx,y,x′,y′be any distinct alternatives.(The other cases,for example wherex=x′,are similar and are omitted.)

By axiom(UD),

4 Related Work

The interdisciplinary study of logic and social choice theory can be roughly divided into two directions.On the one hand,concepts and methodologies in social choice theory have motivated many logical researches,includingjudgmentaggregation and binary aggregation([19,20,14]),the study of aggregating members’individual judgments (represented by logical formulas)into a collective judgment,graph aggregation([9]),the study of aggregating general relations rather than linear orders,belief merging([18]),a logical framework that aggregates possibly contradictory belief bases into group beliefs,reason-based aggregation([7]),in which,instead of preferences,reasons leading to individuals’preferences are given as primary,logic aggregation([27]),the aggregation of different logics,and so on.These logical frameworks enriched the study of logic,and in return extended the boundary of social choice theory.

On the other hand,logic has been taken as a helpful tool in investigating traditional problems of social choice theory.One approach in this direction is by using classical predicate or propositional logic.This approach was identified in [8]as“embedding social choice theory into exciting logical frameworks”.The focus of this approach is on(automatically)verifying existing proofs of social choice theorems or on searching for new theorems and new proofs for social functions,with the help of certain logical theorem provers([15,25,28,21]).

Another approach in this direction,which is the approach taken by the current paper,is by using the framework of modal logic.This approach was identified in[8]as“designing logics for modelling social choice”.Most logics in this approach is designed for the more general framework of judgment aggregation ([19]),and therefore can be naturally restricted to preference aggregation.Our logic in this paper is for preference aggregation.However,it can be adapted for a logic of judgment aggregation.We leave this issue due to length restriction.

Pauly presented in[22]a simple modal logic that can axiomatize specific voting rules,where majority voting,consensus voting,and dictatorship were axiomatized as examples.Pauly’s framework is quite different from the others.The other formalisms were designed for general social functions,instead of for specific functions.Troquard et al.in [26]introduced a logic specifically designed to reason about the strategyproofness of social choice functions,which is a variant of social welfare functions whose output is a winning alternative or a set of winning alternatives.Jiang et al.studied in [17]a logic reason-based social choice.Cinà and Endriss’s logic in [5,6]is a fragment of the logic in [26],and therefore is also a logic for social choice functions.The most related framework to the current one is Ågotnes et al.’s judgment aggregation logic(JAL)presented in[1].

We shall compare our logicALwith Ågotnes et al’sJALin some detail.The two logics have the same motivation of providing a modal language for representing properties of social welfare functions(or judgment aggregation rules).We shall only considerJALin the context of preference aggregation.

A model ofJALis defined by a given social welfare functionF,whose domain consists of the Cartesian product of the set of all profiles and the set of pairs of alternatives.That is,each state in the domain is in the form((l1,...,ln),(x ≻y)),where(l1,...,ln)is a profile andx,y∈X.JALhas three types of atomic formulas:ifori∈N,which is true at state ((l1,...,ln),(x ≻y))where (x ≻y)∈li;hx≻yforx,y∈X,which is true at state((l1,...,ln),(x′ ≻y′))wherex=x′andy=y′;a special propositionσ,which is true at state((l1,...,ln),(x ≻y))where(x ≻y)∈F(l1,...,ln).There are two modalities□and ■.□φis true at a state((l1,...,ln),(x ≻y))if for all profiles (l′1,...,l′n),(l′1,...,l′n),(x ≻y)|=φ.■φis true at a state((l1,...,ln),(x ≻y))if for all atomsx′ ≻y′,((l1,...,ln),(x′ ≻y′))|=φ.

Comparing withAL,the syntax ofJALare more complicated,and its model and semantics are less intuitive.It is not easy to catch an intuitive meaning of a state.A state in anJALmodel does not have a fixed meaning.It depends on formulas to be evaluated at the state.A state((l1,...,ln),(x ≻y))means thatx ≻yis individuali’s preference,ifiis the formula to be evaluated.It means thatx ≻yis a group preference given profile(l1,...,ln),ifσis the formula to be evaluated.It means thatx ≻yis the preference to be considered,ifhx≻yis the formula to be evaluated.As a consequence,meanings of these formulas by themselves are not clear.Only by a mixed usage of these formulas can we have a clear reading.For example,hx≻y∧i∧σmeans thatx ≻yis ani’s preference and also a group’s preference.ALhas a simple model and a simple language with specific meanings.x ≻ymeans that it is a group preference.◇(x1≻y1∧...∧xn ≻yn)means thatx1≻y1,...,xn ≻ynare individuals’ preferences.Universal modalities are used in bothJALandAL.(The semantics ofJAL’s□and ■ does not involve all states.They reflect all profiles and all pairs of alternatives.)

As for the expressiveness,it seems hard to build a characterizing formula inJALfor any given social welfare function.JALseems not being able to express a specific vote that aggregatesl1,...,lnintol.As shown in Theorem 2.5,ALhas the full expressive power for social welfare functions.Therefore,ALis at least as expressive asJAL.Whether or notALis strictly expressive thanJALis unknown to us.

Our logic is built on a fixed number of individuals and a fixed number of alternatives.The alphabet of the language depends on the two parameters:Given a setNof individuals and a setXof alternatives,we will have a set{x ≻y|x,y∈X}with|X|2atoms,and an|N|-ary modality.The problem of whether we can have a logic without the restriction of fixedNandXwas identified in[8].This is a natural question,considering we usually prefer a logic to be as general as possible.However,as far as we know,this restriction was presented in all existing modal logic for social functions with enough expressive power of coding Arrow’s theorem[1,26,5],including the logic in this paper.As argued in[5],with which we agree,it may be not a serious restriction.The logical frameworks for differentNandXresemble to each other.In most cases,we can safely leaveNandXas parameters of the logics.

5 Conclusion

We present in this paper a simple modal logic for talking about social welfare functions.The logic shows how concepts of preference aggregation can be directly formalized in a logical framework.A model is a direct reading of a social welfare function.A syntactic atom of the logic is an atomic preference in the formx ≻y.Ann-ary social welfare function is directly formalized by ann-ary modality of the language,and by an(n+1)-ary relation in the model.As a consequence,properties of preference aggregation are formalized by easily readable formulas,and proofs of impossibility results of social choice theory are easily coded in the logic.We give a complete deductive system for the logic,as well as show that the logic is expressively complete.Therefore,all properties of preference aggregation can be expressed by formulas of the logic,and in general all impossibility theorems can be syntactically proved.

The complexity of our logic is not discussed in this paper.A standard bottom-up algorithm can show that the model checking problem ofALis decidable in polynomial time.(See Section 4.1 in [3]for such an algorithm for basic modal language.)But this result is hardly helpful,as indicated in[1],because it does not take the number of individuals and the number of alternatives as input parameters.In[1],JAL’s model checking problem was proved to beWe shall not expect an easier result forAL.We leave the complexity issue for future work.

There have been quite a few modal theorem provers available.(See the webpage http://www.cs.man.ac.uk/～schmidt/tools/ for an incomplete list.)It would be interesting to see whether a similar tool can be implemented for our logic.With such an automated reasoning tool in hand,we can investigate the possibility of finding new impossibility theorems and new proofs.These problems are more interesting than coding the existing proofs of existing impossibility theorems.