ERCIM News No.48, January 2002 [contents]
Coalition Logic for Voting Procedures
by Henk Nieland
Voting is at the core of democracy, ranging from choosing the president of the chess club to parliamentary elections. Hence, fair and non-manipulative voting procedures are very important. However, a satisfactory definition of what is fair has not been given yet. Logic can help in reasoning about correctness and efficiency of voting and other social choice procedures. At CWI social processes were analysed with logics derived from formal methods used in computer science, including a Coalition Logic which could lead to automatic generation of the fairest voting procedure.
Elections are daily bread for our newspapers. Potential EU members must guarantee democratic elections in their country. Such elections should be the basis of a new state in tabula rasa Afghanistan within a few years. However, all voting procedures which have developed during more than two centuries, have drawbacks. With a slightly different, but still plausible voting system in the US, we would now have Gore in the White House instead of Bush. Well known is the Bonn vs Berlin question from ten years ago: should parliament and/or ministries move to Berlin? Here too, it was not the preference of the citizen that was decisive, but the adopted voting procedure, which was determined by a committee of wise men (ie the parliamentary council of elders, in German Ältestenrat).
Half a century ago, the later Nobel laureate Kenneth J. Arrow proved that, given five highly desirable properties that any reasonable voting system should possess, no voting method would always satisfy these properties, thus destroying a dream of social philosophers. Hence, in practice one should look for a compromise. One such property is that the outcome should not exclusively depend on the voting behaviour of one single individual (absence of a dictator). Another is the exclusion of strategic voting, where for example a group can prevent the adoption of a law by not voting according to their own preference, but such that the voting process never reaches a decision.
At CWI, researcher Marc Pauly has developed a language in which notions like coalition are defined, together with their rules of operation. This Coalition Logic enables for example a voting procedure to be tested for undesirable properties like strategic voting. In his PhD thesis, Pauly applies this logic to several practical problems in the area of social choice. Pauly also studied a Game Logic, which enables reasoning about fair division problems. The standard example here is cutting a cake, for which an algorithm based on the two-person I cut, you choose strategy leads to a fair division. Such problems occur for example in settling an inheritance, or converting election results into parliamentary seats.
Paulys new Logics are extensions of logics used to reason about computer programs. There formal methods are applied to prove that a program really does what it is supposed to do. However, interpreted as a game a computer program is rather primitive: there is just one player the computer. With the Game Logic and Coalition Logic one can reason about social processes or games with two or more players.