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


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 func f . x -> Element of B;
coherence
f . x is Element of B
proof end;
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
proof end;

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 & c <> b )
proof end;

definition
let A be non empty set ;
defpred S1[ set ] means ( $1 is Relation of A & ( for a, b being Element of A holds
( [a,b] in $1 or [b,a] in $1 ) ) & ( for a, b, c being Element of A st [a,b] in $1 & [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 & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [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 & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for R being set holds
( R in b1 iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) ) ) & ( for R being set holds
( R in b2 iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) ) ) holds
b1 = b2
proof end;
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 & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [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
proof end;
end;

definition
let A be non empty set ;
defpred S1[ set ] means for a, b being Element of A st [a,b] in $1 & [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 & [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 & [b,a] in R holds
a = b )
proof end;
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 & [b,a] in R holds
a = b ) ) & ( for R being Element of LinPreorders A holds
( R in b2 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b ) ) holds
b1 = b2
proof end;
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 & [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
proof end;
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 ) )
proof end;
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
proof end;
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 ;
pred a <=_ o,b means :: ARROW:def 4
[a,b] in o;
end;

:: deftheorem 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 by Def1;

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 ) by Def1;

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 ) & ( b <=_ o,c or b <_ o,c ) holds
a <=_ o,c
proof end;

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 & b <=_ o99,a holds
a = b by Def2;

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

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
proof end;

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
proof end;

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 & a <> c holds
ex o being Element of LinPreorders A st
( a <_ o,b & a <_ o,c & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )
proof end;

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 & a <> c holds
ex o being Element of LinPreorders A st
( b <_ o,a & c <_ o,a & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )
proof end;

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 ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o9,b ) ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) ) ) )
proof end;

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 ) )
proof end;

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 ) & ( 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 ) & ( a <_ p9 . i,b implies a <_ p . i,b ) & ( b <_ p . i,a implies b <_ p9 . i,a ) & ( b <_ p9 . i,a implies b <_ p . i,a ) ) ) holds
( a <_ f . p,b iff a <_ f . p9,b ) ) & 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
proof end;

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 ) & ( 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 ) ) & 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 )
proof end;