(* * Sen's SDF results and Liberal Paradox. * (C)opyright Peter Gammie, peteg42 at gmail.com, commenced July 2006. * License: BSD *) (*<*) 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 (*>*)