# Theory SCFs

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

(*<*)
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
(*>*)