[EM] Deduction engine idea for proving property-set incompatibilities for EMs

[Warren Smith]

When trying to prove things like ICC & FBC incompatible, you soon start getting into
large case analyses.  There are 2 problems (a) lots of cases, and (b) not
sure where to begin - lots of possible starting points and not sure which to use.

It may be possible to have a computer overcome both of these problems.
In the below we shall assume anonymity and neutrality of the underlying method
as well as equal-likelihood tie-breaking.

As an example, suppose we want to search for a proof FBC & ICC are incompatible
in 3-candidate elections with 15 voters and rank-equalities allowed.
There are exactly 12 possible vote-types (A>B>C, A=B>C, ... etc) which allows
me to show that the number of possible election-types is exactly
(26 choose 11)=7726160.
For each election there are 7 possible results: A,B,C,AB,BC,CA,ABC
(where the 2-letter results denote ties).

We proceed as follows.  We make a table of 1 byte per election type.
The 7 bits in a byte are used to indicate which of the 7 results are logically possible.
Initially all results are possible in all elections (except for elections for which,
by means of assumed properties such as unanimous winner, etc, we know the winner).
Now we start making deductions. For each election we can, e.g, see if it contains a clone-set,
and if so, record what logical possibilities that rules out.
Or we can consider the ways voters can betray favorites, and see what winner-possibilities
that rules out.

We keep making passes thru all the entries in the table making deductions.
Eventually one of two things wlll happen:
  (i) some election type is found in which ALL logical possibilities are ruled out (empty byte)
      in which case proof done - we've proved the theorem that properties are logically
      incompatible.  [And print out the election.]
  (ii) the table stops changing (reaches a fixpoint) because we've used up all the
       logical power in all the deductions we programmed.  In that case we
       stop and print
       "unable to prove incompatibility with xxx voters and yyy candidates."

The joy of such an engine would be it could handle pretty much ANY set of election-system
properties, and possibly produce incompatibility proofs well beyond the
capabilities of unaided human mathematicians, in great profusion, in fact totally blowing
away all previous humans such as (Nobelist) Ken Arrow and making them obsolete.
On the other hand, it would be a nontrivial feat of programming, and it might be it
doesn't ever get anywhere beyond where humans can get without the engine.  It's a gamble.

Is anybody interested in programming, or helping to program, such an election-methods
deduction engine?

Warren D. Smith
http://rangevoting.org
warren DOT wds AT gmail DOT com