:: Arrow's Impossibility Theorem :: by Freek Wiedijk :: :: Received August 13, 2007 :: Copyright (c) 2007-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, SUBSET_1, FUNCT_1, FINSET_1, CARD_1, XXREAL_0, TARSKI, ARYTM_1, RELAT_1, ZFMISC_1, RELAT_2, ORDERS_1, WELLORD1, FUNCT_2, NAT_1, FINSEQ_1, ARYTM_3, ARROW; notations ORDERS_1, RELAT_1, RELAT_2, RELSET_1, XBOOLE_0, SUBSET_1, TARSKI, FINSET_1, FUNCT_1, FUNCT_2, CARD_1, XXREAL_0, ZFMISC_1, ORDINAL1, NAT_1, NUMBERS, FINSEQ_1, XCMPLX_0, WELLORD1; constructors XXREAL_0, FUNCT_2, REAL_1, FINSEQ_1, INT_1, RELAT_2, PARTFUN1, WELLORD1, RELSET_1; registrations RELSET_1, FINSET_1, NAT_1, INT_1, XREAL_0, XBOOLE_0, ORDINAL1; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin :: Preliminaries 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; redefine func f.x -> Element of B; end; theorem :: ARROW:1 for A being finite set st card A >= 2 holds for a being Element of A holds ex b being Element of A st b <> a; theorem :: ARROW:2 for A being finite set st card A >= 3 holds for a,b being Element of A holds ex c being Element of A st c <> a & c <> b; begin :: Linear preorders and linear orders reserve A for non empty set; reserve a,b,c,x,y,z for Element of A; definition let A; func LinPreorders A -> set means :: ARROW:def 1 for R being set holds R in it iff R is Relation of A & (for a,b holds [a,b] in R or [b,a] in R) & for a,b,c st [a,b] in R & [b,c] in R holds [a,c] in R; end; registration let A; cluster LinPreorders A -> non empty; end; definition let A; func LinOrders A -> Subset of LinPreorders A means :: ARROW:def 2 for R being Element of LinPreorders A holds R in it iff for a,b st [a,b] in R & [b,a] in R holds a = b; end; registration let A be set; cluster connected for Order of A; end; definition let A; redefine func LinOrders A means :: ARROW:def 3 for R being set holds R in it iff R is connected Order of A; end; registration let A; cluster LinOrders A -> non empty; end; registration let A; cluster -> Relation-like for Element of LinPreorders A; cluster -> Relation-like for Element of LinOrders A; end; reserve o,o9 for Element of LinPreorders A; reserve o99 for Element of LinOrders A; definition let o be Relation, a,b be set; pred a <=_o, b means :: ARROW:def 4 [a,b] in o; end; notation let o be Relation, 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 :: ARROW:3 a <=_o, a; theorem :: ARROW:4 a <=_o, b or b <=_o, a; theorem :: ARROW:5 (a <=_o, b or a <_o, b) & (b <=_ o, c or b <_o, c) implies a <=_o, c; theorem :: ARROW:6 a <=_o99, b & b <=_o99, a implies a = b; theorem :: ARROW:7 a <> b & b <> c & a <> c implies ex o st a <_o, b & b <_o, c; theorem :: ARROW:8 ex o st for a st a <> b holds b <_o, a; theorem :: ARROW:9 ex o st for a st a <> b holds a <_o, b; theorem :: ARROW:10 a <> b & a <> c implies ex o st a <_o, b & a <_o, c & (b <_o, c iff b <_o9, c) & (c <_o, b iff c <_o9, b); theorem :: ARROW:11 a <> b & a <> c implies ex o st b <_o, a & c <_o, a & (b <_o, c iff b <_o9, c) & (c <_o, b iff c <_o9, b); theorem :: ARROW:12 for o,o9 being Element of LinOrders A holds (a <_o, b iff a <_o9, b) & (b <_o, a iff b <_o9, a) iff (a <_o, b iff a <_o9, b); theorem :: ARROW:13 for o being Element of LinOrders A, o9 being Element of LinPreorders A holds (for a,b st a <_o, b holds a <_o9, b) iff for a,b holds a <_o, b iff a <_o9, b; begin :: Arrow's theorem :: version with weak orders, the one from the paper reserve A,N for finite non empty set; reserve a,b,c,d,a9,c9 for Element of A; reserve i,n,nb,nc for Element of N; reserve o,oI,oII for Element of LinPreorders A; reserve p,p9,pI,pII,pI9,pII9 for Element of Funcs(N,LinPreorders A); reserve f for Function of Funcs(N,LinPreorders A),LinPreorders A; reserve k,k0 for Nat; theorem :: ARROW:14 (for p,a,b st for i holds a <_p.i, b holds a <_f.p, b) & (for p,p9,a,b st for i holds (a <_p.i, b iff a <_p9.i, b) & (b <_p.i, a iff b <_p9.i, a) holds a <_f.p, b iff a <_f.p9, b) & card A >= 3 implies ex n st for p,a,b st a <_p.n, b holds a <_f.p, b; :: and then a stronger version reserve o,o1 for Element of LinOrders A; reserve o9 for Element of LinPreorders A; reserve p,p9 for Element of Funcs(N,LinOrders A); reserve q,q9 for Element of Funcs(N,LinPreorders A); reserve f for Function of Funcs(N,LinOrders A),LinPreorders A; theorem :: ARROW:15 (for p,a,b st for i holds a <_p.i, b holds a <_f.p, b) & (for p,p9,a,b st for i holds a <_p.i, b iff a <_p9.i, b holds a <_f.p, b iff a <_f.p9, b) & card A >= 3 implies ex n st for p,a,b holds a <_p.n, b iff a <_f.p, b;