:: Arrow's Impossibility Theorem
::  by Freek Wiedijk
::
:: Received August 13, 2007
:: Copyright (c) 2007-2021 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, 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;