# [EM] pairwise, fairness, and information content

Craig Carey research at ijs.co.nz
Fri Aug 16 05:45:27 PDT 2002

```At 02\08\16 11:46 +1200 Friday, Craig Carey wrote:
>
>Solving a 2 candidate election without use of pairwise comparing.
>
...
>|      1st     2nd
>|A     a0    a0 - u*(1-v)
>|AB    ab    ab - u*v
>|B     b0    b0 + t + u*(1-w)
>|BA    ba    ba - t + u*w
>|
>|Define: b=b0+ba, a=a0+ab. A usual case has p=1/2.
>|
>|(For all a0,ab,b0,ba,t,u,v,w) [
>| ((0<=t<=b)(0<=u<=a)(0<=v<=1)(0<=w<=1)) implies
>|  [A loses the 1st  .implies. A loses the 2nd] ]

That simple quantifier logic equation can be evaluated in the REDUCE
that is accessible through telnet.

REDLOG and REDUCE can be accessed through telnet:
http://www.zib.de/Symbolik/reduce/

"Test Out REDUCE 3.7":
http://www.zib.de/Symbolik/reduce/testreduce.html

The REDLOG Quantifier Eliminator Software:
http://www.fmi.uni-passau.de/~redlog/

My free polytope simplifying software code that runs in REDLOG:
http://www.ijs.co.nz/polytopes.thm

The following shows then when the idea of P1 which is that removing
support from A never allows A to change from a winner into a loser,
runs OK when more votes than a paper contains are removed from it
(i.e., so that the paper ends up with a negative weight.)

--------------------------------------------------------------------------
|Last login: Tue Sep 18 11:40:02 2001 from 202.89.142.185
|Have a lot of fun...
|Welcome to the REDUCE test server at ZIB
|
|
|REDUCE 3.7, 15-Apr-1999, patched to 11-Apr-2002 ...
|
|
|
|
|3: rlset ofsf;        % Computation over Real Numbers
|
|{}
|
|4: off factor;     % elim some errors
|
|5: precision 20;   % number of decimal digits if rounding
|
|12
|
|6: off fullprec;   % off impl don't print trailing zeros
|
|7: off rounded;    % Sometimes rationals faster than reals. [lose e (=2.718)]
|
|8: on rlrealtime;  % timing
|
|9: a := a0+ab;
|
|a := a0 + ab
|
|10: b := b0+ba;
|
|b := b0 + ba
|
|11: awins1 := (a < q * (a+b));
|
|awins1 :=  - a0*q + a0 - ab*q + ab - b0*q - ba*q < 0
|
|12: awins2 := sub ({a0=a0-u*(1-v), ab=ab-u*v, b0=b0+t+u*(1-w), ba=ba-t+u*w},
|awins1);
|
|awins2 :=  - a0*q + a0 - ab*q + ab - b0*q - ba*q - u < 0
|
----------------------------------------------------------------------------
|13: h0 := ( (0<=t<=b)and(0<=u<=a)and(0<=v<=1)and(0<=w<=1) )
|13:       impl (awins1 impl awins2);
|
|h0 := (( - t <= 0 and  - b0 - ba + t <= 0)
|
| and ( - u <= 0 and  - a0 - ab + u <= 0) and ( - v <= 0 and v - 1 <= 0)
|
| and ( - w <= 0 and w - 1 <= 0)) impl (
|
| - a0*q + a0 - ab*q + ab - b0*q - ba*q < 0
|
| impl  - a0*q + a0 - ab*q + ab - b0*q - ba*q - u < 0)
|
|14: rlqe all ({w,v,t,u,ab,ba,a0,b0}, h0);
|Realtime: 1 s
|
|true
|
----------------------------------------------------------------------------
|15: h0 := ( (0<=t)and(0<=u)and(0<=v<=1)and(0<=w<=1) )
|15:       impl (awins1 impl awins2);
|
|h0 := ( - t <= 0 and  - u <= 0 and ( - v <= 0 and v - 1 <= 0)
|
| and ( - w <= 0 and w - 1 <= 0)) impl (
|
| - a0*q + a0 - ab*q + ab - b0*q - ba*q < 0
|
| impl  - a0*q + a0 - ab*q + ab - b0*q - ba*q - u < 0)
|
|16: h0 := ( (0<=t)and(0<=u) ) impl (awins1 impl awins2);
|
|h0 := ( - t <= 0 and  - u <= 0) impl ( - a0*q + a0 - ab*q + ab - b0*q
| - ba*q < 0
|
| impl  - a0*q + a0 - ab*q + ab - b0*q - ba*q - u < 0)
|
|17: rlqe all ({w,v,t,u,ab,ba,a0,b0}, h0);
|Realtime: 0 s
|
|true
|
----------------------------------------------------------------------------
|18: h0 := ( (0<=t)and(0<=u) ) impl (awins1 impl awins2);
|
|h0 := ( - t <= 0 and  - u <= 0) impl
|     ( - a0*q + a0 - ab*q + ab - b0*q - ba*q < 0
|
| impl  - a0*q + a0 - ab*q + ab - b0*q - ba*q - u < 0)
|
|19:
|19: rlqe all ({w,v,t,u,ab,ba,a0,b0}, h0);
|Realtime: 0 s
|
|true
|
|20:
--------------------------------------------------------------------------

Craig Carey
Auckland, New Zealand

----