:: 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 S₁[ 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 S₂[ set ] means for R being set holds
( R in $1 iff S₁[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 b₁ being set st
for R being set holds
( R in b₁ 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 b₁, b₂ being set st ( for R being set holds
( R in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines LinPreorders ARROW:def 1 :
for A being non empty set
for b₂ being set holds
( b₂ = LinPreorders A iff for R being set holds
( R in b₂ 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 S₁[ set ] means for a, b being Element of A st [a,b] in $1 & [b,a] in $1 holds
a = b;
defpred S₂[ set ] means for R being Element of LinPreorders A holds
( R in $1 iff S₁[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 b₁ being Subset of (LinPreorders A) st
for R being Element of LinPreorders A holds
( R in b₁ iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b )

proof end;

uniqueness
for b₁, b₂ being Subset of (LinPreorders A) st ( for R being Element of LinPreorders A holds
( R in b₁ 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 b₂ iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines LinOrders ARROW:def 2 :
for A being non empty set
for b₂ being Subset of (LinPreorders A) holds
( b₂ = LinOrders A iff for R being Element of LinPreorders A holds
( R in b₂ 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 b₁ being Order of A st b₁ 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 b₁ being Subset of (LinPreorders A) holds
( b₁ = LinOrders A iff for R being set holds
( R in b₁ iff R is connected Order of A ) )

proof end;

end;

:: deftheorem Def3 defines LinOrders ARROW:def 3 :
for A being non empty set
for b₂ being Subset of (LinPreorders A) holds
( b₂ = LinOrders A iff for R being set holds
( R in b₂ 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 b₁ being Element of LinPreorders A holds b₁ is Relation-like by Def1;

cluster -> Relation-like for Element of LinOrders A;

coherence
for b₁ being Element of LinOrders A holds b₁ 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;