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.
(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.
(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.
(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
(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.
(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)))