Theory Sen
theory Sen
imports SCFs
begin
section‹Sen's Liberal Paradox›
subsection‹Social Decision Functions (SDFs)›
text‹To make progress in the face of Arrow's Theorem, the demands placed
on the social choice function need to be weakened. One approach is to only
require that the set of alternatives that society ranks highest (and is
otherwise indifferent about) be non-empty.
Following \<^cite>‹‹Chapter~4*› in "Sen:70a"›, a \emph{Social Decision Function}
(SDF) yields a choice function for every profile.›
definition
SDF :: "('a, 'i) SCF ⇒ 'a set ⇒ 'i set ⇒ ('a set ⇒ 'i set ⇒ ('a, 'i) Profile ⇒ bool) ⇒ bool"
where
"SDF sdf A Is Pcond ≡ (∀P. Pcond A Is P ⟶ choiceFn A (sdf P))"
lemma SDFI[intro]:
"(⋀P. Pcond A Is P ⟹ choiceFn A (sdf P)) ⟹ SDF sdf A Is Pcond"
unfolding SDF_def by simp
lemma SWF_SDF:
assumes finiteA: "finite A"
shows "SWF scf A Is universal_domain ⟹ SDF scf A Is universal_domain"
unfolding SDF_def SWF_def by (blast dest: rpr_choiceFn[OF finiteA])
text‹In contrast to SWFs, there are SDFs satisfying Arrow's (relevant)
requirements. The lemma uses a witness to show the absence of a
dictatorship.›
lemma SDF_nodictator_witness:
assumes has2A: "hasw [x,y] A"
and has2Is: "hasw [i,j] Is"
obtains P
where "profile A Is P"
and "x ⇘(P i)⇙≺ y"
and "y ⇘(P j)⇙≺ x"
proof
let ?P = "λk. (if k = i then ({ (x, u) | u. u ∈ A }
∪ { (y, u) | u. u ∈ A - {x} })
else ({ (y, u) | u. u ∈ A }
∪ { (x, u) | u. u ∈ A - {y} }))
∪ (A - {x,y}) × (A - {x,y})"
show "profile A Is ?P"
proof
fix i assume iis: "i ∈ Is"
from has2A show "rpr A (?P i)"
by - (rule rprI, simp_all add: trans_def, blast+)
next
from has2Is show "Is ≠ {}" by auto
qed
from has2A has2Is
show "x ⇘(?P i)⇙≺ y"
and "y ⇘(?P j)⇙≺ x"
unfolding strict_pref_def by auto
qed
lemma SDF_possibility:
assumes finiteA: "finite A"
and has2A: "has 2 A"
and has2Is: "has 2 Is"
obtains sdf
where "weak_pareto sdf A Is universal_domain"
and "iia sdf A Is"
and "¬(∃j. dictator sdf A Is j)"
and "SDF sdf A Is universal_domain"
proof -
let ?sdf = "λP. { (x, y) . x ∈ A ∧ y ∈ A
∧ ¬ ((∀i ∈ Is. y ⇘(P i)⇙≼ x)
∧ (∃i ∈ Is. y ⇘(P i)⇙≺ x)) }"
have "weak_pareto ?sdf A Is universal_domain"
by (rule, unfold strict_pref_def, auto dest: profile_non_empty)
moreover
have "iia ?sdf A Is" unfolding strict_pref_def by auto
moreover
have "¬(∃j. dictator ?sdf A Is j)"
proof
assume "∃j. dictator ?sdf A Is j"
then obtain j where jIs: "j ∈ Is"
and jD: "∀x ∈ A. ∀y ∈ A. decisive ?sdf A Is {j} x y"
unfolding dictator_def decisive_def by auto
from jIs has_witness_two[OF has2Is] obtain i where ijIs: "hasw [i,j] Is"
by auto
from has_witness_two[OF has2A] obtain x y where xyA: "hasw [x,y] A" by auto
from xyA ijIs obtain P
where profileP: "profile A Is P"
and yPix: "x ⇘(P i)⇙≺ y"
and yPjx: "y ⇘(P j)⇙≺ x"
by (rule SDF_nodictator_witness)
from profileP jD jIs xyA yPjx have "y ⇘(?sdf P)⇙≺ x"
unfolding decisive_def by simp
moreover
from ijIs xyA yPjx yPix have "x ⇘(?sdf P)⇙≼ y"
unfolding strict_pref_def by auto
ultimately show False
unfolding strict_pref_def by blast
qed
moreover
have "SDF ?sdf A Is universal_domain"
proof
fix P assume ud: "universal_domain A Is P"
show "choiceFn A (?sdf P)"
proof(rule r_c_qt_imp_cf[OF finiteA])
show "complete A (?sdf P)" and "refl_on A (?sdf P)"
unfolding strict_pref_def by auto
show "quasi_trans (?sdf P)"
proof
fix x y z assume xy: "x ⇘(?sdf P)⇙≺ y" and yz: "y ⇘(?sdf P)⇙≺ z"
from xy yz have xyzA: "x ∈ A" "y ∈ A" "z ∈ A"
unfolding strict_pref_def by auto
from xy yz have AxRy: "∀i ∈ Is. x ⇘(P i)⇙≼ y"
and ExPy: "∃i ∈ Is. x ⇘(P i)⇙≺ y"
and AyRz: "∀i ∈ Is. y ⇘(P i)⇙≼ z"
unfolding strict_pref_def by auto
from AxRy AyRz ud have AxRz: "∀i ∈ Is. x ⇘(P i)⇙≼ z"
by - (unfold universal_domain_def, blast dest: rpr_le_trans)
from ExPy AyRz ud have ExPz: "∃i ∈ Is. x ⇘(P i)⇙≺ z"
by - (unfold universal_domain_def, blast dest: rpr_less_le_trans)
from xyzA AxRz ExPz show "x ⇘(?sdf P)⇙≺ z" unfolding strict_pref_def by auto
qed
qed
qed
ultimately show thesis ..
qed
text ‹Sen makes several other stronger statements about SDFs later in the
chapter. I leave these for future work.›
subsection‹Sen's Liberal Paradox›
text‹Having side-stepped Arrow's Theorem, Sen proceeds to other conditions
one may ask of an SCF. His analysis of \emph{liberalism}, mechanised in this
section, has attracted much criticism over the years
\<^cite>‹"AnalyseKritik:1996"›.
Following \<^cite>‹‹Chapter~6*› in "Sen:70a"›, a \emph{liberal} social choice rule is
one that, for each individual, there is a pair of alternatives that she is
decisive over.›
definition liberal :: "('a, 'i) SCF ⇒ 'a set ⇒ 'i set ⇒ bool" where
"liberal scf A Is ≡
(∀i ∈ Is. ∃x ∈ A. ∃y ∈ A. x ≠ y
∧ decisive scf A Is {i} x y ∧ decisive scf A Is {i} y x)"
lemma liberalE:
"⟦ liberal scf A Is; i ∈ Is ⟧
⟹ ∃x ∈ A. ∃y ∈ A. x ≠ y
∧ decisive scf A Is {i} x y ∧ decisive scf A Is {i} y x"
by (simp add: liberal_def)
text‹This condition can be weakened to require just two such decisive
individuals; if we required just one, we would allow dictatorships, which
are clearly not liberal.›
definition minimally_liberal :: "('a, 'i) SCF ⇒ 'a set ⇒ 'i set ⇒ bool" where
"minimally_liberal scf A Is ≡
(∃i ∈ Is. ∃j ∈ Is. i ≠ j
∧ (∃x ∈ A. ∃y ∈ A. x ≠ y
∧ decisive scf A Is {i} x y ∧ decisive scf A Is {i} y x)
∧ (∃x ∈ A. ∃y ∈ A. x ≠ y
∧ decisive scf A Is {j} x y ∧ decisive scf A Is {j} y x))"
lemma liberal_imp_minimally_liberal:
assumes has2Is: "has 2 Is"
and L: "liberal scf A Is"
shows "minimally_liberal scf A Is"
proof -
from has_extend_witness[where xs="[]", OF has2Is]
obtain i where i: "i ∈ Is" by auto
with has_extend_witness[where xs="[i]", OF has2Is]
obtain j where j: "j ∈ Is" "i ≠ j" by auto
from L i j show ?thesis
unfolding minimally_liberal_def by (blast intro: liberalE)
qed
text‹
The key observation is that once we have at least two decisive individuals
we can complete the Condorcet (paradox of voting) cycle using the weak
Pareto assumption. The details of the proof don't give more insight.
Firstly we need three types of profile witnesses (one of which we saw
previously). The main proof proceeds by case distinctions on which
alternatives the two liberal agents are decisive for.
›
lemmas liberal_witness_two = SDF_nodictator_witness
lemma liberal_witness_three:
assumes threeA: "hasw [x,y,v] A"
and twoIs: "hasw [i,j] Is"
obtains P
where "profile A Is P"
and "x ⇘(P i)⇙≺ y"
and "v ⇘(P j)⇙≺ x"
and "∀i ∈ Is. y ⇘(P i)⇙≺ v"
proof -
let ?P =
"λa. if a = i then { (x, u) | u. u ∈ A }
∪ { (y, u) | u. u ∈ A - {x} }
∪ (A - {x,y}) × (A - {x,y})
else { (y, u) | u. u ∈ A }
∪ { (v, u) | u. u ∈ A - {y} }
∪ (A - {v,y}) × (A - {v,y})"
have "profile A Is ?P"
proof
fix i assume iis: "i ∈ Is"
show "rpr A (?P i)"
proof
show "complete A (?P i)" by (simp, blast)
from threeA iis show "refl_on A (?P i)" by (simp, blast)
from threeA iis show "trans (?P i)" by (clarsimp simp add: trans_def)
qed
next
from twoIs show "Is ≠ {}" by auto
qed
moreover
from threeA twoIs have "x ⇘(?P i)⇙≺ y" "v ⇘(?P j)⇙≺ x" "∀i ∈ Is. y ⇘(?P i)⇙≺ v"
unfolding strict_pref_def by auto
ultimately show ?thesis ..
qed
lemma liberal_witness_four:
assumes fourA: "hasw [x,y,u,v] A"
and twoIs: "hasw [i,j] Is"
obtains P
where "profile A Is P"
and "x ⇘(P i)⇙≺ y"
and "u ⇘(P j)⇙≺ v"
and "∀i ∈ Is. v ⇘(P i)⇙≺ x ∧ y ⇘(P i)⇙≺ u"
proof -
let ?P =
"λa. if a = i then { (v, w) | w. w ∈ A }
∪ { (x, w) | w. w ∈ A - {v} }
∪ { (y, w) | w. w ∈ A - {v,x} }
∪ (A - {v,x,y}) × (A - {v,x,y})
else { (y, w) | w. w ∈ A }
∪ { (u, w) | w. w ∈ A - {y} }
∪ { (v, w) | w. w ∈ A - {u,y} }
∪ (A - {u,v,y}) × (A - {u,v,y})"
have "profile A Is ?P"
proof
fix i assume iis: "i ∈ Is"
show "rpr A (?P i)"
proof
show "complete A (?P i)" by (simp, blast)
from fourA iis show "refl_on A (?P i)" by (simp, blast)
from fourA iis show "trans (?P i)" by (clarsimp simp add: trans_def)
qed
next
from twoIs show "Is ≠ {}" by auto
qed
moreover
from fourA twoIs have "x ⇘(?P i)⇙≺ y" "u ⇘(?P j)⇙≺ v" "∀i ∈ Is. v ⇘(?P i)⇙≺ x ∧ y ⇘(?P i)⇙≺ u"
by (unfold strict_pref_def, auto)
ultimately show thesis ..
qed
text‹The Liberal Paradox: having two decisive individuals, an SDF and the
weak pareto assumption is inconsistent.›
theorem LiberalParadox:
assumes SDF: "SDF sdf A Is universal_domain"
and ml: "minimally_liberal sdf A Is"
and wp: "weak_pareto sdf A Is universal_domain"
shows False
proof -
from ml obtain i j x y u v
where i: "i ∈ Is" and j: "j ∈ Is" and ij: "i ≠ j"
and x: "x ∈ A" and y: "y ∈ A" and u: "u ∈ A" and v: "v ∈ A"
and xy: "x ≠ y"
and dixy: "decisive sdf A Is {i} x y"
and diyx: "decisive sdf A Is {i} y x"
and uv: "u ≠ v"
and djuv: "decisive sdf A Is {j} u v"
and djvu: "decisive sdf A Is {j} v u"
by (unfold minimally_liberal_def, auto)
from i j ij have twoIs: "hasw [i,j] Is" by simp
{
assume xu: "x = u" and yv: "y = v"
from xy x y have twoA: "hasw [x,y] A" by simp
obtain P
where "profile A Is P" "x ⇘(P i)⇙≺ y" "y ⇘(P j)⇙≺ x"
using liberal_witness_two[OF twoA twoIs] by blast
with i j dixy djvu xu yv have False
by (unfold decisive_def strict_pref_def, blast)
}
moreover
{
assume xu: "x = u" and yv: "y ≠ v"
with xy uv xu x y v have threeA: "hasw [x,y,v] A" by simp
obtain P
where profileP: "profile A Is P"
and xPiy: "x ⇘(P i)⇙≺ y"
and vPjx: "v ⇘(P j)⇙≺ x"
and AyPv: "∀i ∈ Is. y ⇘(P i)⇙≺ v"
using liberal_witness_three[OF threeA twoIs] by blast
from vPjx j djvu xu profileP have vPx: "v ⇘(sdf P)⇙≺ x"
by (unfold decisive_def strict_pref_def, auto)
from xPiy i dixy profileP have xPy: "x ⇘(sdf P)⇙≺ y"
by (unfold decisive_def strict_pref_def, auto)
from AyPv weak_paretoD[OF wp _ y v] profileP have yPv: "y ⇘(sdf P)⇙≺ v"
by auto
from threeA profileP SDF have "choiceSet {x,y,v} (sdf P) ≠ {}"
by (simp add: SDF_def choiceFn_def)
with vPx xPy yPv have False
by (unfold choiceSet_def strict_pref_def, blast)
}
moreover
{
assume xv: "x = v" and yu: "y = u"
from xy x y have twoA: "hasw [x,y] A" by auto
obtain P
where "profile A Is P" "x ⇘(P i)⇙≺ y" "y ⇘(P j)⇙≺ x"
using liberal_witness_two[OF twoA twoIs] by blast
with i j dixy djuv xv yu have False
by (unfold decisive_def strict_pref_def, blast)
}
moreover
{
assume xv: "x = v" and yu: "y ≠ u"
with xy uv u x y have threeA: "hasw [x,y,u] A" by simp
obtain P
where profileP: "profile A Is P"
and xPiy: "x ⇘(P i)⇙≺ y"
and uPjx: "u ⇘(P j)⇙≺ x"
and AyPu: "∀i ∈ Is. y ⇘(P i)⇙≺ u"
using liberal_witness_three[OF threeA twoIs] by blast
from uPjx j djuv xv profileP have uPx: "u ⇘(sdf P)⇙≺ x"
by (unfold decisive_def strict_pref_def, auto)
from xPiy i dixy profileP have xPy: "x ⇘(sdf P)⇙≺ y"
by (unfold decisive_def strict_pref_def, auto)
from AyPu weak_paretoD[OF wp _ y u] profileP have yPu: "y ⇘(sdf P)⇙≺ u"
by auto
from threeA profileP SDF have "choiceSet {x,y,u} (sdf P) ≠ {}"
by (simp add: SDF_def choiceFn_def)
with uPx xPy yPu have False
by (unfold choiceSet_def strict_pref_def, blast)
}
moreover
{
assume xu: "x ≠ u" and xv: "x ≠ v" and yu: "y = u"
with v x y xy uv xu have threeA: "hasw [y,x,v] A" by simp
obtain P
where profileP: "profile A Is P"
and yPix: "y ⇘(P i)⇙≺ x"
and vPjy: "v ⇘(P j)⇙≺ y"
and AxPv: "∀i ∈ Is. x ⇘(P i)⇙≺ v"
using liberal_witness_three[OF threeA twoIs] by blast
from yPix i diyx profileP have yPx: "y ⇘(sdf P)⇙≺ x"
by (unfold decisive_def strict_pref_def, auto)
from vPjy j djvu yu profileP have vPy: "v ⇘(sdf P)⇙≺ y"
by (unfold decisive_def strict_pref_def, auto)
from AxPv weak_paretoD[OF wp _ x v] profileP have xPv: "x ⇘(sdf P)⇙≺ v"
by auto
from threeA profileP SDF have "choiceSet {x,y,v} (sdf P) ≠ {}"
by (simp add: SDF_def choiceFn_def)
with yPx vPy xPv have False
by (unfold choiceSet_def strict_pref_def, blast)
}
moreover
{
assume xu: "x ≠ u" and xv: "x ≠ v" and yv: "y = v"
with u x y xy uv xu have threeA: "hasw [y,x,u] A" by simp
obtain P
where profileP: "profile A Is P"
and yPix: "y ⇘(P i)⇙≺ x"
and uPjy: "u ⇘(P j)⇙≺ y"
and AxPu: "∀i ∈ Is. x ⇘(P i)⇙≺ u"
using liberal_witness_three[OF threeA twoIs] by blast
from yPix i diyx profileP have yPx: "y ⇘(sdf P)⇙≺ x"
by (unfold decisive_def strict_pref_def, auto)
from uPjy j djuv yv profileP have uPy: "u ⇘(sdf P)⇙≺ y"
by (unfold decisive_def strict_pref_def, auto)
from AxPu weak_paretoD[OF wp _ x u] profileP have xPu: "x ⇘(sdf P)⇙≺ u"
by auto
from threeA profileP SDF have "choiceSet {x,y,u} (sdf P) ≠ {}"
by (simp add: SDF_def choiceFn_def)
with yPx uPy xPu have False
by (unfold choiceSet_def strict_pref_def, blast)
}
moreover
{
assume xu: "x ≠ u" and xv: "x ≠ v" and yu: "y ≠ u" and yv: "y ≠ v"
with u v x y xy uv xu have fourA: "hasw [x,y,u,v] A" by simp
obtain P
where profileP: "profile A Is P"
and xPiy: "x ⇘(P i)⇙≺ y"
and uPjv: "u ⇘(P j)⇙≺ v"
and AvPxAyPu: "∀i ∈ Is. v ⇘(P i)⇙≺ x ∧ y ⇘(P i)⇙≺ u"
using liberal_witness_four[OF fourA twoIs] by blast
from xPiy i dixy profileP have xPy: "x ⇘(sdf P)⇙≺ y"
by (unfold decisive_def strict_pref_def, auto)
from uPjv j djuv profileP have uPv: "u ⇘(sdf P)⇙≺ v"
by (unfold decisive_def strict_pref_def, auto)
from AvPxAyPu weak_paretoD[OF wp] profileP x y u v
have vPx: "v ⇘(sdf P)⇙≺ x" and yPu: "y ⇘(sdf P)⇙≺ u" by auto
from fourA profileP SDF have "choiceSet {x,y,u,v} (sdf P) ≠ {}"
by (simp add: SDF_def choiceFn_def)
with xPy uPv vPx yPu have False
by (unfold choiceSet_def strict_pref_def, blast)
}
ultimately show False by blast
qed
end