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. x ⇘r⇙≼ 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 ⟹ x ⇘r⇙≼ 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. x ⇘r⇙≺ y ∧ y ⇘r⇙≺ z ⟶ x ⇘r⇙≺ z"

lemma quasi_transI[intro]:
  "(⋀x y z. ⟦ x ⇘r⇙≺ y; y ⇘r⇙≺ z ⟧ ⟹ x ⇘r⇙≺ z) ⟹ quasi_trans r"
  unfolding quasi_trans_def by blast

lemma quasi_transD: "⟦ x ⇘r⇙≺ y; y ⇘r⇙≺ z; quasi_trans r ⟧ ⟹ x ⇘r⇙≺ 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 "a ⇘r⇙≺ b ∨ b ⇘r⇙≼ a" unfolding choiceSet_def strict_pref_def by blast
      thus ?thesis
      proof
        assume ab: "b ⇘r⇙≼ a"
        with bCF show ?thesis unfolding choiceSet_def by auto
      next
        assume ab: "a ⇘r⇙≺ 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. i∈Is ⟹ 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
(*>*)