		Search-engine friendly clone of the ACL2 documentation.

Instant-runoff-voting

Fairness-criteria

Some fairness theorems about irv

We prove that irv satisfies the following fairness criteria.

Majority Criterion: If a candidate is preferred by an absolute majority of voters, then that candidate must win.

Theorem: irv-satisfies-the-majority-criterion

(defthm
   irv-satisfies-the-majority-criterion
   (implies (and (< (majority (number-of-voters xs))
                    (acl2::duplicity e (make-nth-choice-list 0 xs)))
                 (irv-ballot-p xs))
            (equal (irv xs) e)))

Condorcet Loser Criteria: A simple definition from Wikipedia is as follows:

...if a candidate would lose a head-to-head competition against every other candidate, then that candidate must not win the overall election.

Note that a given election may or may not have a Condorcet Loser.

Theorem: irv-satisfies-the-condorcet-loser-criterion

(defthm
     irv-satisfies-the-condorcet-loser-criterion
     (implies (and (all-head-to-head-competition-loser-p l cids xs)
                   (acl2::set-equiv (cons l cids)
                                    (candidate-ids xs))
                   (no-duplicatesp-equal (cons l cids))
                   (nat-listp cids)
                   (<= 1 (len cids))
                   (irv-ballot-p xs))
              (not (equal (irv xs) l))))

Majority Loser Criterion: If a majority of voters prefers every other candidate over a given candidate, then that candidate must not win. Or said differently: if a candidate has a majority of last-place votes, then he must not win.

Theorem: irv-satisfies-the-majority-loser-criterion

(defthm
 irv-satisfies-the-majority-loser-criterion
 (implies
      (and (< (majority (number-of-voters xs))
              (acl2::duplicity l
                               (make-nth-choice-list (last-place xs)
                                                     xs)))
           (< 1 (number-of-candidates xs))
           (irv-ballot-p xs))
      (not (equal (irv xs) l))))

Independence of Clones Criterion: If a set of clones contains at least two non-winning candidates, then deleting one of the clones must not change the winner.

This property depends on the definition of pick-candidate, the tie-breaker, in our formalization. Since the tie-breaker is a constrained function, we can't prove it about irv in the general case. Here's an illustration:

(irv '((1 3) (2))) ;; 2 is the winner. 
 
;; 3 is a clone of 1 --- both are non-winning candidates. 
(clone-p 3 1 '((1 3) (2))) 
 
;; Suppose the tie-breaker picked the candidate with the smallest 
;; ID. 
 
;; Now, eliminating one clone changes the winner from 2 to 3. 
(irv (eliminate-candidate 1 '((1 3) (2))))

However, we do prove that this property holds when the winner is elected in the first step, i.e., if he has a majority of first-place votes.

Theorem: irv-satisfies-the-independence-of-clones-criterion-majority-winner

(defthm
  irv-satisfies-the-independence-of-clones-criterion-majority-winner
  (implies (and (natp (first-choice-of-majority-p (candidate-ids xs)
                                                  xs))
                (equal w (irv xs))
                (clone-p clone c xs)
                (not (equal w c))
                (not (equal w clone))
                (irv-ballot-p xs))
           (equal (irv (eliminate-candidate clone xs))
                  w)))

Subtopics

Eliminate-candidates: Remove cids from xs
Sum-nats
Eliminate-other-candidates: Remove all candidates from xs, except for those in cids
Clone-p: Is clone a clone of c in xs?
Last-place: Index of the last-place vote in xs
All-head-to-head-competition-loser-p: Check if l will lose in a head-to-head competition against every candidate in cids
Non-maj-ind-hint
Find-condorcet-loser: Returns a condorcet loser in xs, if any
Last-place-elim-ind-hint