:: Arrow's Impossibility Theorem
:: by Freek Wiedijk
::
:: Received August 13, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

definition
let A, B9 be non empty set ;
let B be non empty Subset of B9;
let f be Function of A,B;
let x be Element of A;
:: original:.
redefine funcf . x ->  Element of B;
coherence
 f . x is Element of B
proofend;
end;

theorem Th1: :: ARROW:1
for A being finite set st card A >= 2 holds
for a being Element of A ex b being Element of A st b <> a
proofend;

theorem Th2: :: ARROW:2
for A being finite set st card A >= 3 holds
for a, b being Element of A ex c being Element of A st
( c <> a &amp; c <> b )
proofend;

begin

definition
let A be non empty set ;
defpred S1[ set ] means ( $1 is Relation of A &amp; ( for a, b being Element of A holds
( [a,b] in $1 or [b,a] in $1 ) ) &amp; ( for a, b, c being Element of A st [a,b] in $1 &amp; [b,c] in $1 holds
[a,c] in $1 ) );
defpred S2[ set ] means  for R being set holds
( R in $1 iff S1[R] );
func LinPreorders A ->  set  means :Def1: :: ARROW:def 1
 for R being set holds
( R in it iff ( R is Relation of A &amp; ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) &amp; ( for a, b, c being Element of A st [a,b] in R &amp; [b,c] in R holds
[a,c] in R ) ) );
existence
 ex b1 being set st
for R being set holds
( R in b1 iff ( R is Relation of A &amp; ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) &amp; ( for a, b, c being Element of A st [a,b] in R &amp; [b,c] in R holds
[a,c] in R ) ) )
proofend;
uniqueness
 for b1, b2 being set st ( for R being set holds
( R in b1 iff ( R is Relation of A &amp; ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) &amp; ( for a, b, c being Element of A st [a,b] in R &amp; [b,c] in R holds
[a,c] in R ) ) ) ) &amp; ( for R being set holds
( R in b2 iff ( R is Relation of A &amp; ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) &amp; ( for a, b, c being Element of A st [a,b] in R &amp; [b,c] in R holds
[a,c] in R ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines LinPreorders ARROW:def_1_:_
 for A being non empty set
for b2 being set holds
( b2 = LinPreorders A iff for R being set holds
( R in b2 iff ( R is Relation of A &amp; ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) &amp; ( for a, b, c being Element of A st [a,b] in R &amp; [b,c] in R holds
[a,c] in R ) ) ) );

registration
let A be non empty set ;
cluster LinPreorders A ->  non empty ;
coherence
 not LinPreorders A is empty
proofend;
end;

definition
let A be non empty set ;
defpred S1[ set ] means  for a, b being Element of A st [a,b] in $1 &amp; [b,a] in $1 holds
a = b;
defpred S2[ set ] means  for R being Element of LinPreorders A holds
( R in $1 iff S1[R] );
func LinOrders A ->  Subset of (LinPreorders A) means :Def2: :: ARROW:def 2
 for R being Element of LinPreorders A holds
( R in it iff for a, b being Element of A st [a,b] in R &amp; [b,a] in R holds
a = b );
existence
 ex b1 being Subset of (LinPreorders A) st
for R being Element of LinPreorders A holds
( R in b1 iff for a, b being Element of A st [a,b] in R &amp; [b,a] in R holds
a = b )
proofend;
uniqueness
 for b1, b2 being Subset of (LinPreorders A) st ( for R being Element of LinPreorders A holds
( R in b1 iff for a, b being Element of A st [a,b] in R &amp; [b,a] in R holds
a = b ) ) &amp; ( for R being Element of LinPreorders A holds
( R in b2 iff for a, b being Element of A st [a,b] in R &amp; [b,a] in R holds
a = b ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines LinOrders ARROW:def_2_:_
 for A being non empty set
for b2 being Subset of (LinPreorders A) holds
( b2 = LinOrders A iff for R being Element of LinPreorders A holds
( R in b2 iff for a, b being Element of A st [a,b] in R &amp; [b,a] in R holds
a = b ) );

registration
let A be set ;
cluster Relation-like A -defined A -valued V17(A) reflexive antisymmetric connected transitive for Element of bool [:A,A:];
existence
 ex b1 being Order of A st b1 is connected
proofend;
end;

definition
let A be non empty set ;
redefine func LinOrders A means :Def3: :: ARROW:def 3
 for R being set holds
( R in it iff R is connected Order of A );
compatibility
 for b1 being Subset of (LinPreorders A) holds
( b1 = LinOrders A iff for R being set holds
( R in b1 iff R is connected Order of A ) )
proofend;
end;

:: deftheorem Def3 defines LinOrders ARROW:def_3_:_
 for A being non empty set
for b2 being Subset of (LinPreorders A) holds
( b2 = LinOrders A iff for R being set holds
( R in b2 iff R is connected Order of A ) );

registration
let A be non empty set ;
cluster LinOrders A ->  non empty ;
coherence
 not LinOrders A is empty
proofend;
end;

registration
let A be non empty set ;
cluster  ->  Relation-like for Element of LinPreorders A;
coherence
 for b1 being Element of LinPreorders A holds b1 is Relation-like by Def1;
cluster  ->  Relation-like for Element of LinOrders A;
coherence
 for b1 being Element of LinOrders A holds b1 is Relation-like ;
end;

definition
let o be Relation;
let a, b be set ;
preda <=_ o,b means :Def4: :: ARROW:def 4
[a,b] in o;
end;

:: deftheorem Def4 defines <=_ ARROW:def_4_:_
 for o being Relation
for a, b being set holds
( a <=_ o,b iff [a,b] in o );

notation
let o be Relation;
let a, b be set ;
synonym b >=_ o,a for a <=_ o,b;
antonym b <_ o,a for a <=_ o,b;
antonym a >_ o,b for a <=_ o,b;
end;

theorem Th3: :: ARROW:3
for A being non empty set
for a being Element of A
for o being Element of LinPreorders A holds a <=_ o,a
proofend;

theorem Th4: :: ARROW:4
for A being non empty set
for a, b being Element of A
for o being Element of LinPreorders A holds
( a <=_ o,b or b <=_ o,a )
proofend;

theorem Th5: :: ARROW:5
for A being non empty set
for a, b, c being Element of A
for o being Element of LinPreorders A st ( a <=_ o,b or a <_ o,b ) &amp; ( b <=_ o,c or b <_ o,c ) holds
a <=_ o,c
proofend;

theorem Th6: :: ARROW:6
for A being non empty set
for a, b being Element of A
for o99 being Element of LinOrders A st a <=_ o99,b &amp; b <=_ o99,a holds
a = b
proofend;

theorem Th7: :: ARROW:7
for A being non empty set
for a, b, c being Element of A st a <> b &amp; b <> c &amp; a <> c holds
ex o being Element of LinPreorders A st
( a <_ o,b &amp; b <_ o,c )
proofend;

theorem Th8: :: ARROW:8
for A being non empty set
for b being Element of A ex o being Element of LinPreorders A st
for a being Element of A st a <> b holds
b <_ o,a
proofend;

theorem Th9: :: ARROW:9
for A being non empty set
for b being Element of A ex o being Element of LinPreorders A st
for a being Element of A st a <> b holds
a <_ o,b
proofend;

theorem Th10: :: ARROW:10
for A being non empty set
for a, b, c being Element of A
for o9 being Element of LinPreorders A st a <> b &amp; a <> c holds
ex o being Element of LinPreorders A st
( a <_ o,b &amp; a <_ o,c &amp; ( b <_ o,c implies b <_ o9,c ) &amp; ( b <_ o9,c implies b <_ o,c ) &amp; ( c <_ o,b implies c <_ o9,b ) &amp; ( c <_ o9,b implies c <_ o,b ) )
proofend;

theorem Th11: :: ARROW:11
for A being non empty set
for a, b, c being Element of A
for o9 being Element of LinPreorders A st a <> b &amp; a <> c holds
ex o being Element of LinPreorders A st
( b <_ o,a &amp; c <_ o,a &amp; ( b <_ o,c implies b <_ o9,c ) &amp; ( b <_ o9,c implies b <_ o,c ) &amp; ( c <_ o,b implies c <_ o9,b ) &amp; ( c <_ o9,b implies c <_ o,b ) )
proofend;

theorem :: ARROW:12
for A being non empty set
for a, b being Element of A
for o, o9 being Element of LinOrders A holds
(  not ( ( a <_ o,b implies a <_ o9,b ) &amp; ( a <_ o9,b implies a <_ o,b ) &amp; ( b <_ o,a implies b <_ o9,a ) &amp; ( b <_ o9,a implies b <_ o,a ) &amp; not ( a <_ o,b iff a <_ o9,b ) ) &amp; not ( ( a <_ o,b implies a <_ o9,b ) &amp; ( a <_ o9,b implies a <_ o,b ) &amp; not ( ( a <_ o,b implies a <_ o9,b ) &amp; ( a <_ o9,b implies a <_ o,b ) &amp; ( b <_ o,a implies b <_ o9,a ) &amp; ( b <_ o9,a implies b <_ o,a ) ) ) )
proofend;

theorem Th13: :: ARROW:13
for A being non empty set
for o being Element of LinOrders A
for o9 being Element of LinPreorders A holds
( ( for a, b being Element of A st a <_ o,b holds
a <_ o9,b ) iff for a, b being Element of A holds
( a <_ o,b iff a <_ o9,b ) )
proofend;

begin

theorem Th14: :: ARROW:14
for A, N being non empty finite set
for f being Function of (Funcs (N,(LinPreorders A))),(LinPreorders A) st ( for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds a <_ p . i,b ) holds
a <_ f . p,b ) &amp; ( for p, p9 being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds
( ( a <_ p . i,b implies a <_ p9 . i,b ) &amp; ( a <_ p9 . i,b implies a <_ p . i,b ) &amp; ( b <_ p . i,a implies b <_ p9 . i,a ) &amp; ( b <_ p9 . i,a implies b <_ p . i,a ) ) ) holds
( a <_ f . p,b iff a <_ f . p9,b ) ) &amp; card A >= 3 holds
ex n being Element of N st
for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st a <_ p . n,b holds
a <_ f . p,b
proofend;

theorem :: ARROW:15
for A, N being non empty finite set
for f being Function of (Funcs (N,(LinOrders A))),(LinPreorders A) st ( for p being Element of Funcs (N,(LinOrders A))
for a, b being Element of A st ( for i being Element of N holds a <_ p . i,b ) holds
a <_ f . p,b ) &amp; ( for p, p9 being Element of Funcs (N,(LinOrders A))
for a, b being Element of A st ( for i being Element of N holds
( a <_ p . i,b iff a <_ p9 . i,b ) ) holds
( a <_ f . p,b iff a <_ f . p9,b ) ) &amp; card A >= 3 holds
ex n being Element of N st
for p being Element of Funcs (N,(LinOrders A))
for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b )
proofend;