Theory SCFs

(*
 * Social Choice Functions (SCFs).
 * (C)opyright Peter Gammie, peteg42 at gmail.com, commenced July 2006.
 * License: BSD
 *)

(*<*)
theory SCFs

imports RPRs

begin
(*>*)

(* **************************************** *)

subsection‹Choice Sets, Choice Functions›

text‹A \emph{choice set} is the subset of @{term "A"} where every element
of that subset is (weakly) preferred to every other element of @{term "A"}
with respect to a given RPR. A \emph{choice function} yields a non-empty
choice set whenever @{term "A"} is non-empty.›

definition choiceSet :: "'a set  'a RPR  'a set" where
  "choiceSet A r  { x  A . y  A. xr⇙≼ y }"

definition choiceFn :: "'a set  'a RPR  bool" where
  "choiceFn A r  A'  A. A'  {}  choiceSet A' r  {}"

lemma choiceSetI[intro]:
  " x  A; y. y  A  xr⇙≼ y   x  choiceSet A r"
  unfolding choiceSet_def by simp

lemma choiceFnI[intro]:
  "(A'.  A'  A; A'  {}   choiceSet A' r  {})  choiceFn A r"
  unfolding choiceFn_def by simp

text‹If a complete and reflexive relation is also \emph{quasi-transitive}
it will yield a choice function.›

definition quasi_trans :: "'a RPR  bool" where
  "quasi_trans r  x y z. xr⇙≺ y  yr⇙≺ z  xr⇙≺ z"

lemma quasi_transI[intro]:
  "(x y z.  xr⇙≺ y; yr⇙≺ z   xr⇙≺ z)  quasi_trans r"
  unfolding quasi_trans_def by blast

lemma quasi_transD: " xr⇙≺ y; yr⇙≺ z; quasi_trans r   xr⇙≺ z"
  unfolding quasi_trans_def by blast

lemma trans_imp_quasi_trans: "trans r  quasi_trans r"
  by (rule quasi_transI, unfold strict_pref_def trans_def, blast)

lemma r_c_qt_imp_cf:
  assumes finiteA: "finite A"
      and c: "complete A r"
      and qt: "quasi_trans r"
      and r: "refl_on A r"
  shows "choiceFn A r"
proof
  fix B assume B: "B  A" "B  {}"
  with finite_subset finiteA have finiteB: "finite B" by auto
  from finiteB B show "choiceSet B r  {}"
  proof(induct rule: finite_subset_induct')
    case empty with B show ?case by auto
  next
    case (insert a B)
    hence finiteB: "finite B"
        and aA: "a  A"
        and AB: "B  A"
        and aB: "a  B"
        and cF: "B  {}  choiceSet B r  {}" by - blast
    show ?case
    proof(cases "B = {}")
      case True with aA r show ?thesis
        unfolding choiceSet_def by blast
    next
      case False
      with cF obtain b where bCF: "b  choiceSet B r" by blast
      from AB aA bCF complete_refl_on[OF c r]
      have "ar⇙≺ b  br⇙≼ a" unfolding choiceSet_def strict_pref_def by blast
      thus ?thesis
      proof
        assume ab: "br⇙≼ a"
        with bCF show ?thesis unfolding choiceSet_def by auto
      next
        assume ab: "ar⇙≺ b"
        have "a  choiceSet (insert a B) r"
        proof(rule ccontr)
          assume aCF: "a  choiceSet (insert a B) r"
          from aB have "b. b  B  a  b" by auto
          with aCF aA AB c r obtain b' where B: "b'  B" "b'r⇙≺ a"
            unfolding choiceSet_def complete_def strict_pref_def by blast
          with ab qt have "b'r⇙≺ b" by (blast dest: quasi_transD)
          with bCF B show False unfolding choiceSet_def strict_pref_def by blast
        qed
        thus ?thesis by auto
      qed
    qed
  qed
qed

lemma rpr_choiceFn: " finite A; rpr A r   choiceFn A r"
  unfolding rpr_def by (blast dest: trans_imp_quasi_trans r_c_qt_imp_cf)

(* **************************************** *)

subsection‹Social Choice Functions (SCFs)›

text ‹A \emph{social choice function} (SCF), also called a
\emph{collective choice rule} by Sen cite‹p28› in "Sen:70a", is a function that
somehow aggregates society's opinions, expressed as a profile, into a
preference relation.›

type_synonym ('a, 'i) SCF = "('a, 'i) Profile  'a RPR"

text ‹The least we require of an SCF is that it be \emph{complete} and
some function of the profile. The latter condition is usually implied by
other conditions, such as @{term "iia"}.›

definition
  SCF :: "('a, 'i) SCF  'a set  'i set  ('a set  'i set  ('a, 'i) Profile  bool)  bool"
where
  "SCF scf A Is Pcond  (P. Pcond A Is P  (complete A (scf P)))"

lemma SCFI[intro]:
  assumes c: "P. Pcond A Is P  complete A (scf P)"
  shows "SCF scf A Is Pcond"
  unfolding SCF_def using assms by blast

lemma SCF_completeD[dest]: " SCF scf A Is Pcond; Pcond A Is P   complete A (scf P)"
  unfolding SCF_def by blast

(* **************************************** *)

subsection‹Social Welfare Functions (SWFs)›

text ‹A \emph{Social Welfare Function} (SWF) is an SCF that expresses the
society's opinion as a single RPR.

In some situations it might make sense to restrict the allowable
profiles.›

definition
  SWF :: "('a, 'i) SCF  'a set  'i set  ('a set  'i set  ('a, 'i) Profile  bool)  bool"
where
  "SWF swf A Is Pcond  (P. Pcond A Is P  rpr A (swf P))"

lemma SWF_rpr[dest]: " SWF swf A Is Pcond; Pcond A Is P   rpr A (swf P)"
  unfolding SWF_def by simp

(* **************************************** *)

subsection‹General Properties of an SCF›

text‹An SCF has a \emph{universal domain} if it works for all profiles.›

definition universal_domain :: "'a set  'i set  ('a, 'i) Profile  bool" where
  "universal_domain A Is P  profile A Is P"

declare universal_domain_def[simp]

text‹An SCF is \emph{weakly Pareto-optimal} if, whenever everyone strictly
prefers @{term "x"} to @{term "y"}, the SCF does too.›

definition
  weak_pareto :: "('a, 'i) SCF  'a set  'i set  ('a set  'i set  ('a, 'i) Profile  bool)  bool"
where
  "weak_pareto scf A Is Pcond 
     (P x y. Pcond A Is P  x  A  y  A  (i  Is. x(P i)⇙≺ y)  x(scf P)⇙≺ y)"

lemma weak_paretoI[intro]:
  "(P x y. Pcond A Is P; x  A; y  A; i. iIs  x(P i)⇙≺ y  x(scf P)⇙≺ y)
   weak_pareto scf A Is Pcond"
  unfolding weak_pareto_def by simp

lemma weak_paretoD:
  " weak_pareto scf A Is Pcond; Pcond A Is P; x  A; y  A;
     (i. i  Is  x(P i)⇙≺ y)   x(scf P)⇙≺ y"
  unfolding weak_pareto_def by simp

text‹

An SCF satisfies \emph{independence of irrelevant alternatives} if, for two
preference profiles @{term "P"} and @{term "P'"} where for all individuals
@{term "i"}, alternatives @{term "x"} and @{term "y"} drawn from set @{term
"S"} have the same order in @{term "P i"} and @{term "P' i"}, then
alternatives @{term "x"} and @{term "y"} have the same order in @{term "scf
P"} and @{term "scf P'"}.

›

definition iia :: "('a, 'i) SCF  'a set  'i set  bool" where
  "iia scf S Is 
    (P P' x y. profile S Is P  profile S Is P'
       x  S  y  S
       (i  Is. ((x(P i)⇙≼ y)  (x(P' i)⇙≼ y))  ((y(P i)⇙≼ x)  (y(P' i)⇙≼ x)))
          ((x(scf P)⇙≼ y)  (x(scf P')⇙≼ y)))"

lemma iiaI[intro]:
  "(P P' x y.
     profile S Is P; profile S Is P';
      x  S; y  S;
      i. i  Is  ((x(P i)⇙≼ y)  (x(P' i)⇙≼ y))  ((y(P i)⇙≼ x)  (y(P' i)⇙≼ x))
      ((x(swf P)⇙≼ y)  (x(swf P')⇙≼ y)))
   iia swf S Is"
  unfolding iia_def by simp

lemma iiaE:
  " iia swf S Is;
     {x,y}  S;
     a  {x, y}; b  {x, y};
     i a b.  a  {x, y}; b  {x, y}; i  Is   (a(P' i)⇙≼ b)  (a(P i)⇙≼ b);
     profile S Is P; profile S Is P' 
   (a(swf P)⇙≼ b)  (a(swf P')⇙≼ b)"
  unfolding iia_def by (simp, blast)

(* **************************************** *)

subsection‹Decisiveness and Semi-decisiveness›

text‹This notion is the key to Arrow's Theorem, and hinges on the use of
strict preference cite‹p42› in "Sen:70a".›

text‹A coalition @{term "C"} of agents is \emph{semi-decisive} for @{term
"x"} over @{term "y"} if, whenever the coalition prefers @{term "x"} to
@{term "y"} and all other agents prefer the converse, the coalition
prevails.›

definition semidecisive :: "('a, 'i) SCF  'a set  'i set  'i set  'a  'a  bool" where
  "semidecisive scf A Is C x y 
    C  Is  (P. profile A Is P  (i  C. x(P i)⇙≺ y)  (i  Is - C. y(P i)⇙≺ x)
       x(scf P)⇙≺ y)"

lemma semidecisiveI[intro]:
  " C  Is;
    P.  profile A Is P; i. i  C  x(P i)⇙≺ y; i. i  Is - C  y(P i)⇙≺ x 
      x(scf P)⇙≺ y   semidecisive scf A Is C x y"
  unfolding semidecisive_def by simp

lemma semidecisive_coalitionD[dest]: "semidecisive scf A Is C x y  C  Is"
  unfolding semidecisive_def by simp

lemma sd_refl: " C  Is; C  {}   semidecisive scf A Is C x x"
  unfolding semidecisive_def strict_pref_def by blast

text‹A coalition @{term "C"} is \emph{decisive} for @{term "x"} over
@{term "y"} if, whenever the coalition prefers @{term "x"} to @{term "y"},
the coalition prevails.›

definition decisive :: "('a, 'i) SCF  'a set  'i set  'i set  'a  'a  bool" where
  "decisive scf A Is C x y 
    C  Is  (P. profile A Is P  (i  C. x(P i)⇙≺ y)  x(scf P)⇙≺ y)"

lemma decisiveI[intro]:
  " C  Is; P.  profile A Is P; i. i  C  x(P i)⇙≺ y   x(scf P)⇙≺ y 
     decisive scf A Is C x y"
  unfolding decisive_def by simp

lemma d_imp_sd: "decisive scf A Is C x y  semidecisive scf A Is C x y"
  unfolding decisive_def by (rule semidecisiveI, blast+)

lemma decisive_coalitionD[dest]: "decisive scf A Is C x y  C  Is"
  unfolding decisive_def by simp

text ‹Anyone is trivially decisive for @{term "x"} against @{term "x"}.›

lemma d_refl: " C  Is; C  {}   decisive scf A Is C x x"
  unfolding decisive_def strict_pref_def by simp

text‹Agent @{term "j"} is a \emph{dictator} if her preferences always
prevail. This is the same as saying that she is decisive for all @{term "x"}
and @{term "y"}.›

definition dictator :: "('a, 'i) SCF  'a set  'i set  'i  bool" where
  "dictator scf A Is j  j  Is  (x  A. y  A. decisive scf A Is {j} x y)"

lemma dictatorI[intro]:
  " j  Is; x y.  x  A; y  A   decisive scf A Is {j} x y   dictator scf A Is j"
  unfolding dictator_def by simp

lemma dictator_individual[dest]: "dictator scf A Is j  j  Is"
  unfolding dictator_def by simp

(*<*)
end
(*>*)