		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