(* * Arrow's General Possibility Theorem, following Sen. * (C)opyright Peter Gammie, peteg42 at gmail.com, commenced July 2006. * License: BSD *) (*<*) theory Arrow imports SCFs begin (*>*) section‹Arrow's General Possibility Theorem› text‹ The proof falls into two parts: showing that a semi-decisive individual is in fact a dictator, and that a semi-decisive individual exists. I take them in that order. It might be good to do some of this in a locale. The complication is untangling where various witnesses need to be quantified over. › (* **************************************** *) subsection‹Semi-decisiveness Implies Decisiveness› text‹ I follow \<^cite>‹‹Chapter~3*› in "Sen:70a"› quite closely here. Formalising his appeal to the @{term "iia"} assumption is the main complication here. › text‹The witness for the first lemma: in the profile $P'$, special agent $j$ strictly prefers $x$ to $y$ to $z$, and doesn't care about the other alternatives. Everyone else strictly prefers $y$ to each of $x$ to $z$, and inherits the relative preferences between $x$ and $z$ from profile $P$. The model has to be specific about ordering all the other alternatives, but these are immaterial in the proof that uses this witness. Note also that the following lemma is used with different instantiations of $x$, $y$ and $z$, so we need to quantify over them here. This happens implicitly, but in a locale we would have to be more explicit. This is just tedious.› lemma decisive1_witness: assumes has3A: "hasw [x,y,z] A" and profileP: "profile A Is P" and jIs: "j ∈ Is" obtains P' where "profile A Is P'" and "x ⇘(P' j)⇙≺ y ∧ y ⇘(P' j)⇙≺ z" and "⋀i. i ≠ j ⟹ y ⇘(P' i)⇙≺ x ∧ y ⇘(P' i)⇙≺ z ∧ ((x ⇘(P' i)⇙≼ z) = (x ⇘(P i)⇙≼ z)) ∧ ((z ⇘(P' i)⇙≼ x) = (z ⇘(P i)⇙≼ x))" proof let ?P' = "λi. (if i = j then ({ (x, u) | u. u ∈ A } ∪ { (y, u) | u. u ∈ A - {x} } ∪ { (z, u) | u. u ∈ A - {x,y} }) else ({ (y, u) | u. u ∈ A } ∪ { (x, u) | u. u ∈ A - {y,z} } ∪ { (z, u) | u. u ∈ A - {x,y} } ∪ (if x ⇘(P i)⇙≼ z then {(x,z)} else {}) ∪ (if z ⇘(P i)⇙≼ x then {(z,x)} else {}))) ∪ (A - {x,y,z}) × (A - {x,y,z})" show "profile A Is ?P'" proof fix i assume iIs: "i ∈ Is" show "rpr A (?P' i)" proof(cases "i = j") case True with has3A show ?thesis by - (rule rprI, simp_all add: trans_def, blast+) next case False hence ij: "i ≠ j" . show ?thesis proof from iIs profileP have "complete A (P i)" by (blast dest: rpr_complete) with ij show "complete A (?P' i)" by (simp add: complete_def, blast) from iIs profileP have "refl_on A (P i)" by (auto simp add: rpr_def) with has3A ij show "refl_on A (?P' i)" by (simp, blast) from ij has3A show "trans (?P' i)" by (clarsimp simp add: trans_def) qed qed next from profileP show "Is ≠ {}" by (rule profile_non_empty) qed from has3A show "x ⇘(?P' j)⇙≺ y ∧ y ⇘(?P' j)⇙≺ z" and "⋀i. i ≠ j ⟹ y ⇘(?P' i)⇙≺ x ∧ y ⇘(?P' i)⇙≺ z ∧ ((x ⇘(?P' i)⇙≼ z) = (x ⇘(P i)⇙≼ z)) ∧ ((z ⇘(?P' i)⇙≼ x) = (z ⇘(P i)⇙≼ x))" unfolding strict_pref_def by auto qed text ‹The key lemma: in the presence of Arrow's assumptions, an individual who is semi-decisive for $x$ and $y$ is actually decisive for $x$ over any other alternative $z$. (This is where the quantification becomes important.) › lemma decisive1: assumes has3A: "hasw [x,y,z] A" and iia: "iia swf A Is" and swf: "SWF swf A Is universal_domain" and wp: "weak_pareto swf A Is universal_domain" and sd: "semidecisive swf A Is {j} x y" shows "decisive swf A Is {j} x z" proof from sd show jIs: "{j} ⊆ Is" by blast fix P assume profileP: "profile A Is P" and jxzP: "⋀i. i ∈ {j} ⟹ x ⇘(P i)⇙≺ z" from has3A profileP jIs obtain P' where profileP': "profile A Is P'" and jxyzP': "x ⇘(P' j)⇙≺ y" "y ⇘(P' j)⇙≺ z" and ixyzP': "⋀i. i ≠ j ⟶ y ⇘(P' i)⇙≺ x ∧ y ⇘(P' i)⇙≺ z ∧ ((x ⇘(P' i)⇙≼ z) = (x ⇘(P i)⇙≼ z)) ∧ ((z ⇘(P' i)⇙≼ x) = (z ⇘(P i)⇙≼ x))" by - (rule decisive1_witness, blast+) from iia have "⋀a b. ⟦ a ∈ {x, z}; b ∈ {x, z} ⟧ ⟹ (a ⇘(swf P)⇙≼ b) = (a ⇘(swf P')⇙≼ b)" proof(rule iiaE) from has3A show "{x,z} ⊆ A" by simp next fix i assume iIs: "i ∈ Is" fix a b assume ab: "a ∈ {x, z}" "b ∈ {x, z}" show "(a ⇘(P' i)⇙≼ b) = (a ⇘(P i)⇙≼ b)" proof(cases "i = j") case False with ab iIs ixyzP' profileP profileP' has3A show ?thesis unfolding profile_def by auto next case True from profileP' jIs jxyzP' have "x ⇘(P' j)⇙≺ z" by (auto dest: rpr_less_trans) with True ab iIs jxzP profileP profileP' has3A show ?thesis unfolding profile_def strict_pref_def by auto qed qed (simp_all add: profileP profileP') moreover have "x ⇘(swf P')⇙≺ z" proof - from profileP' sd jxyzP' ixyzP' have "x ⇘(swf P')⇙≺ y" by (simp add: semidecisive_def) moreover from jxyzP' ixyzP' have "⋀i. i ∈ Is ⟹ y ⇘(P' i)⇙≺ z" by (case_tac "i=j", auto) with wp profileP' has3A have "y ⇘(swf P')⇙≺ z" by (auto dest: weak_paretoD) moreover note SWF_rpr[OF swf] profileP' ultimately show "x ⇘(swf P')⇙≺ z" unfolding universal_domain_def by (blast dest: rpr_less_trans) qed ultimately show "x ⇘(swf P)⇙≺ z" unfolding strict_pref_def by blast qed text‹The witness for the second lemma: special agent $j$ strictly prefers $z$ to $x$ to $y$, and everyone else strictly prefers $z$ to $x$ and $y$ to $x$. (In some sense the last part is upside-down with respect to the first witness.)› lemma decisive2_witness: assumes has3A: "hasw [x,y,z] A" and profileP: "profile A Is P" and jIs: "j ∈ Is" obtains P' where "profile A Is P'" and "z ⇘(P' j)⇙≺ x ∧ x ⇘(P' j)⇙≺ y" and "⋀i. i ≠ j ⟹ z ⇘(P' i)⇙≺ x ∧ y ⇘(P' i)⇙≺ x ∧ ((y ⇘(P' i)⇙≼ z) = (y ⇘(P i)⇙≼ z)) ∧ ((z ⇘(P' i)⇙≼ y) = (z ⇘(P i)⇙≼ y))" proof let ?P' = "λi. (if i = j then ({ (z, u) | u. u ∈ A } ∪ { (x, u) | u. u ∈ A - {z} } ∪ { (y, u) | u. u ∈ A - {x,z} }) else ({ (z, u) | u. u ∈ A - {y} } ∪ { (y, u) | u. u ∈ A - {z} } ∪ { (x, u) | u. u ∈ A - {y,z} } ∪ (if y ⇘(P i)⇙≼ z then {(y,z)} else {}) ∪ (if z ⇘(P i)⇙≼ y then {(z,y)} else {}))) ∪ (A - {x,y,z}) × (A - {x,y,z})" show "profile A Is ?P'" proof fix i assume iIs: "i ∈ Is" show "rpr A (?P' i)" proof(cases "i = j") case True with has3A show ?thesis by - (rule rprI, simp_all add: trans_def, blast+) next case False hence ij: "i ≠ j" . show ?thesis proof from iIs profileP have "complete A (P i)" by (auto simp add: rpr_def) with ij show "complete A (?P' i)" by (simp add: complete_def, blast) from iIs profileP have "refl_on A (P i)" by (auto simp add: rpr_def) with has3A ij show "refl_on A (?P' i)" by (simp, blast) from ij has3A show "trans (?P' i)" by (clarsimp simp add: trans_def) qed qed next show "Is ≠ {}" by (rule profile_non_empty[OF profileP]) qed from has3A show "z ⇘(?P' j)⇙≺ x ∧ x ⇘(?P' j)⇙≺ y" and "⋀i. i ≠ j ⟹ z ⇘(?P' i)⇙≺ x ∧ y ⇘(?P' i)⇙≺ x ∧ ((y ⇘(?P' i)⇙≼ z) = (y ⇘(P i)⇙≼ z)) ∧ ((z ⇘(?P' i)⇙≼ y) = (z ⇘(P i)⇙≼ y))" unfolding strict_pref_def by auto qed lemma decisive2: assumes has3A: "hasw [x,y,z] A" and iia: "iia swf A Is" and swf: "SWF swf A Is universal_domain" and wp: "weak_pareto swf A Is universal_domain" and sd: "semidecisive swf A Is {j} x y" shows "decisive swf A Is {j} z y" proof from sd show jIs: "{j} ⊆ Is" by blast fix P assume profileP: "profile A Is P" and jyzP: "⋀i. i ∈ {j} ⟹ z ⇘(P i)⇙≺ y" from has3A profileP jIs obtain P' where profileP': "profile A Is P'" and jxyzP': "z ⇘(P' j)⇙≺ x" "x ⇘(P' j)⇙≺ y" and ixyzP': "⋀i. i ≠ j ⟶ z ⇘(P' i)⇙≺ x ∧ y ⇘(P' i)⇙≺ x ∧ ((y ⇘(P' i)⇙≼ z) = (y ⇘(P i)⇙≼ z)) ∧ ((z ⇘(P' i)⇙≼ y) = (z ⇘(P i)⇙≼ y))" by - (rule decisive2_witness, blast+) from iia have "⋀a b. ⟦ a ∈ {y, z}; b ∈ {y, z} ⟧ ⟹ (a ⇘(swf P)⇙≼ b) = (a ⇘(swf P')⇙≼ b)" proof(rule iiaE) from has3A show "{y,z} ⊆ A" by simp next fix i assume iIs: "i ∈ Is" fix a b assume ab: "a ∈ {y, z}" "b ∈ {y, z}" show "(a ⇘(P' i)⇙≼ b) = (a ⇘(P i)⇙≼ b)" proof(cases "i = j") case False with ab iIs ixyzP' profileP profileP' has3A show ?thesis unfolding profile_def by auto next case True from profileP' jIs jxyzP' have "z ⇘(P' j)⇙≺ y" by (auto dest: rpr_less_trans) with True ab iIs jyzP profileP profileP' has3A show ?thesis unfolding profile_def strict_pref_def by auto qed qed (simp_all add: profileP profileP') moreover have "z ⇘(swf P')⇙≺ y" proof - from profileP' sd jxyzP' ixyzP' have "x ⇘(swf P')⇙≺ y" by (simp add: semidecisive_def) moreover from jxyzP' ixyzP' have "⋀i. i ∈ Is ⟹ z ⇘(P' i)⇙≺ x" by (case_tac "i=j", auto) with wp profileP' has3A have "z ⇘(swf P')⇙≺ x" by (auto dest: weak_paretoD) moreover note SWF_rpr[OF swf] profileP' ultimately show "z ⇘(swf P')⇙≺ y" unfolding universal_domain_def by (blast dest: rpr_less_trans) qed ultimately show "z ⇘(swf P)⇙≺ y" unfolding strict_pref_def by blast qed text ‹The following results permute $x$, $y$ and $z$ to show how decisiveness can be obtained from semi-decisiveness in all cases. Again, quite tedious.› lemma decisive3: assumes has3A: "hasw [x,y,z] A" and iia: "iia swf A Is" and swf: "SWF swf A Is universal_domain" and wp: "weak_pareto swf A Is universal_domain" and sd: "semidecisive swf A Is {j} x z" shows "decisive swf A Is {j} y z" using has3A decisive2[OF _ iia swf wp sd] by (simp, blast) lemma decisive4: assumes has3A: "hasw [x,y,z] A" and iia: "iia swf A Is" and swf: "SWF swf A Is universal_domain" and wp: "weak_pareto swf A Is universal_domain" and sd: "semidecisive swf A Is {j} y z" shows "decisive swf A Is {j} y x" using has3A decisive1[OF _ iia swf wp sd] by (simp, blast) lemma decisive5: assumes has3A: "hasw [x,y,z] A" and iia: "iia swf A Is" and swf: "SWF swf A Is universal_domain" and wp: "weak_pareto swf A Is universal_domain" and sd: "semidecisive swf A Is {j} x y" shows "decisive swf A Is {j} y x" proof - from sd have "decisive swf A Is {j} x z" by (rule decisive1[OF has3A iia swf wp]) hence "semidecisive swf A Is {j} x z" by (rule d_imp_sd) hence "decisive swf A Is {j} y z" by (rule decisive3[OF has3A iia swf wp]) hence "semidecisive swf A Is {j} y z" by (rule d_imp_sd) thus "decisive swf A Is {j} y x" by (rule decisive4[OF has3A iia swf wp]) qed lemma decisive6: assumes has3A: "hasw [x,y,z] A" and iia: "iia swf A Is" and swf: "SWF swf A Is universal_domain" and wp: "weak_pareto swf A Is universal_domain" and sd: "semidecisive swf A Is {j} y x" shows "decisive swf A Is {j} y z" "decisive swf A Is {j} z x" "decisive swf A Is {j} x y" proof - from has3A have has3A': "hasw [y,x,z] A" by auto show "decisive swf A Is {j} y z" by (rule decisive1[OF has3A' iia swf wp sd]) show "decisive swf A Is {j} z x" by (rule decisive2[OF has3A' iia swf wp sd]) show "decisive swf A Is {j} x y" by (rule decisive5[OF has3A' iia swf wp sd]) qed lemma decisive7: assumes has3A: "hasw [x,y,z] A" and iia: "iia swf A Is" and swf: "SWF swf A Is universal_domain" and wp: "weak_pareto swf A Is universal_domain" and sd: "semidecisive swf A Is {j} x y" shows "decisive swf A Is {j} y z" "decisive swf A Is {j} z x" "decisive swf A Is {j} x y" proof - from sd have "decisive swf A Is {j} y x" by (rule decisive5[OF has3A iia swf wp]) hence "semidecisive swf A Is {j} y x" by (rule d_imp_sd) thus "decisive swf A Is {j} y z" "decisive swf A Is {j} z x" "decisive swf A Is {j} x y" by (rule decisive6[OF has3A iia swf wp])+ qed lemma j_decisive_xy: assumes has3A: "hasw [x,y,z] A" and iia: "iia swf A Is" and swf: "SWF swf A Is universal_domain" and wp: "weak_pareto swf A Is universal_domain" and sd: "semidecisive swf A Is {j} x y" and uv: "hasw [u,v] {x,y,z}" shows "decisive swf A Is {j} u v" using uv decisive1[OF has3A iia swf wp sd] decisive2[OF has3A iia swf wp sd] decisive5[OF has3A iia swf wp sd] decisive7[OF has3A iia swf wp sd] by (simp, blast) lemma j_decisive: assumes has3A: "has 3 A" and iia: "iia swf A Is" and swf: "SWF swf A Is universal_domain" and wp: "weak_pareto swf A Is universal_domain" and xyA: "hasw [x,y] A" and sd: "semidecisive swf A Is {j} x y" and uv: "hasw [u,v] A" shows "decisive swf A Is {j} u v" proof - from has_extend_witness'[OF has3A xyA] obtain z where xyzA: "hasw [x,y,z] A" by auto { assume ux: "u = x" and vy: "v = y" with xyzA iia swf wp sd have ?thesis by (auto intro: j_decisive_xy) } moreover { assume ux: "u = x" and vNEy: "v ≠ y" with uv xyA iia swf wp sd have ?thesis by(auto intro: j_decisive_xy[of x y]) } moreover { assume uy: "u = y" and vx: "v = x" with xyzA iia swf wp sd have ?thesis by (auto intro: j_decisive_xy) } moreover { assume uy: "u = y" and vNEx: "v ≠ x" with uv xyA iia swf wp sd have ?thesis by (auto intro: j_decisive_xy) } moreover { assume uNExy: "u ∉ {x,y}" and vx: "v = x" with uv xyA iia swf wp sd have ?thesis by (auto intro: j_decisive_xy[of x y]) } moreover { assume uNExy: "u ∉ {x,y}" and vy: "v = y" with uv xyA iia swf wp sd have ?thesis by (auto intro: j_decisive_xy[of x y]) } moreover { assume uNExy: "u ∉ {x,y}" and vNExy: "v ∉ {x,y}" with uv xyA iia swf wp sd have "decisive swf A Is {j} x u" by (auto intro: j_decisive_xy[where x=x and z=u]) hence sdxu: "semidecisive swf A Is {j} x u" by (rule d_imp_sd) with uNExy vNExy uv xyA iia swf wp have ?thesis by (auto intro: j_decisive_xy[of x]) } ultimately show ?thesis by blast qed text ‹The first result: if $j$ is semidecisive for some alternatives $u$ and $v$, then they are actually a dictator.› lemma sd_imp_dictator: assumes has3A: "has 3 A" and iia: "iia swf A Is" and swf: "SWF swf A Is universal_domain" and wp: "weak_pareto swf A Is universal_domain" and uv: "hasw [u,v] A" and sd: "semidecisive swf A Is {j} u v" shows "dictator swf A Is j" proof fix x y assume x: "x ∈ A" and y: "y ∈ A" show "decisive swf A Is {j} x y" proof(cases "x = y") case True with sd show "decisive swf A Is {j} x y" by (blast intro: d_refl) next case False with x y iia swf wp has3A uv sd show "decisive swf A Is {j} x y" by (auto intro: j_decisive) qed next from sd show "j ∈ Is" by blast qed (* **************************************** *) subsection‹The Existence of a Semi-decisive Individual› text‹The second half of the proof establishes the existence of a semi-decisive individual. The required witness is essentially an encoding of the Condorcet pardox (aka "the paradox of voting" that shows we get tied up in knots if a certain agent didn't have dictatorial powers.› lemma sd_exists_witness: assumes has3A: "hasw [x,y,z] A" and Vs: "Is = V1 ∪ V2 ∪ V3 ∧ V1 ∩ V2 = {} ∧ V1 ∩ V3 = {} ∧ V2 ∩ V3 = {}" and Is: "Is ≠ {}" obtains P where "profile A Is P" and "∀i ∈ V1. x ⇘(P i)⇙≺ y ∧ y ⇘(P i)⇙≺ z" and "∀i ∈ V2. z ⇘(P i)⇙≺ x ∧ x ⇘(P i)⇙≺ y" and "∀i ∈ V3. y ⇘(P i)⇙≺ z ∧ z ⇘(P i)⇙≺ x" proof let ?P = "λi. (if i ∈ V1 then ({ (x, u) | u. u ∈ A } ∪ { (y, u) | u. u ∈ A ∧ u ≠ x } ∪ { (z, u) | u. u ∈ A ∧ u ≠ x ∧ u ≠ y }) else if i ∈ V2 then ({ (z, u) | u. u ∈ A } ∪ { (x, u) | u. u ∈ A ∧ u ≠ z } ∪ { (y, u) | u. u ∈ A ∧ u ≠ x ∧ u ≠ z }) else ({ (y, u) | u. u ∈ A } ∪ { (z, u) | u. u ∈ A ∧ u ≠ y } ∪ { (x, u) | u. u ∈ A ∧ u ≠ y ∧ u ≠ z })) ∪ { (u, v) | u v. u ∈ A - {x,y,z} ∧ v ∈ A - {x,y,z}}" show "profile A Is ?P" proof fix i assume iIs: "i ∈ Is" show "rpr A (?P i)" proof show "complete A (?P i)" by (simp add: complete_def, blast) from has3A iIs show "refl_on A (?P i)" by - (simp, blast) from has3A iIs show "trans (?P i)" by (clarsimp simp add: trans_def) qed next from Is show "Is ≠ {}" . qed from has3A Vs show "∀i ∈ V1. x ⇘(?P i)⇙≺ y ∧ y ⇘(?P i)⇙≺ z" and "∀i ∈ V2. z ⇘(?P i)⇙≺ x ∧ x ⇘(?P i)⇙≺ y" and "∀i ∈ V3. y ⇘(?P i)⇙≺ z ∧ z ⇘(?P i)⇙≺ x" unfolding strict_pref_def by auto qed text ‹This proof is unfortunately long. Many of the statements rely on a lot of context, making it difficult to split it up.› lemma sd_exists: assumes has3A: "has 3 A" and finiteIs: "finite Is" and twoIs: "has 2 Is" and iia: "iia swf A Is" and swf: "SWF swf A Is universal_domain" and wp: "weak_pareto swf A Is universal_domain" shows "∃j u v. hasw [u,v] A ∧ semidecisive swf A Is {j} u v" proof - let ?P = "λS. S ⊆ Is ∧ S ≠ {} ∧ (∃u v. hasw [u,v] A ∧ semidecisive swf A Is S u v)" obtain u v where uvA: "hasw [u,v] A" using has_witness_two[OF has3A] by auto ― ‹The weak pareto requirement implies that the set of all individuals is decisive between any given alternatives.› hence "decisive swf A Is Is u v" by - (rule, auto intro: weak_paretoD[OF wp]) hence "semidecisive swf A Is Is u v" by (rule d_imp_sd) with uvA twoIs has_suc_notempty[where n=1] nat_2[symmetric] have "?P Is" by auto ― ‹Obtain a minimally-sized semi-decisive set.› from ex_has_least_nat[where P="?P" and m="card", OF this] obtain V x y where VIs: "V ⊆ Is" and Vnotempty: "V ≠ {}" and xyA: "hasw [x,y] A" and Vsd: "semidecisive swf A Is V x y" and Vmin: "⋀V'. ?P V' ⟹ card V ≤ card V'" by blast from VIs finiteIs have Vfinite: "finite V" by (rule finite_subset) ― ‹Show that minimal set contains a single individual.› from Vfinite Vnotempty have "∃j. V = {j}" proof(rule finite_set_singleton_contra) assume Vcard: "1 < card V" then obtain j where jV: "{j} ⊆ V" using has_extend_witness[where xs="[]", OF card_has[where n="card V"]] by auto ― ‹Split an individual from the "minimal" set.› let ?V1 = "{j}" let ?V2 = "V - ?V1" let ?V3 = "Is - V" from jV card_Diff_singleton Vcard have V2card: "card ?V2 > 0" "card ?V2 < card V" by auto hence V2notempty: "{} ≠ ?V2" by auto from jV VIs have jV2V3: "Is = ?V1 ∪ ?V2 ∪ ?V3 ∧ ?V1 ∩ ?V2 = {} ∧ ?V1 ∩ ?V3 = {} ∧ ?V2 ∩ ?V3 = {}" by auto ― ‹Show that that individual is semi-decisive for $x$ over $z$.› from has_extend_witness'[OF has3A xyA] obtain z where threeDist: "hasw [x,y,z] A" by auto from sd_exists_witness[OF threeDist jV2V3] VIs Vnotempty obtain P where profileP: "profile A Is P" and V1xyzP: "x ⇘(P j)⇙≺ y ∧ y ⇘(P j)⇙≺ z" and V2xyzP: "∀i ∈ ?V2. z ⇘(P i)⇙≺ x ∧ x ⇘(P i)⇙≺ y" and V3xyzP: "∀i ∈ ?V3. y ⇘(P i)⇙≺ z ∧ z ⇘(P i)⇙≺ x" by (simp, blast) have xPz: "x ⇘(swf P)⇙≺ z" proof(rule rpr_less_le_trans[where y="y"]) from profileP swf show "rpr A (swf P)" by auto next ― ‹V2 is semi-decisive, and everyone else opposes their choice. Ergo they prevail.› show "x ⇘(swf P)⇙≺ y" proof - from profileP V3xyzP have "∀i ∈ ?V3. y ⇘(P i)⇙≺ x" by (blast dest: rpr_less_trans) with profileP V1xyzP V2xyzP Vsd show ?thesis unfolding semidecisive_def by auto qed next ― ‹This result is unfortunately quite tortuous.› from SWF_rpr[OF swf] show "y ⇘(swf P)⇙≼ z" proof(rule rpr_less_not[OF _ _ notI]) from threeDist show "hasw [z, y] A" by auto next assume zPy: "z ⇘(swf P)⇙≺ y" have "semidecisive swf A Is ?V2 z y" proof from VIs show "V - {j} ⊆ Is" by blast next fix P' assume profileP': "profile A Is P'" and V2yz': "⋀i. i ∈ ?V2 ⟹ z ⇘(P' i)⇙≺ y" and nV2yz': "⋀i. i ∈ Is - ?V2 ⟹ y ⇘(P' i)⇙≺ z" from iia have "⋀a b. ⟦ a ∈ {y, z}; b ∈ {y, z} ⟧ ⟹ (a ⇘(swf P)⇙≼ b) = (a ⇘(swf P')⇙≼ b)" proof(rule iiaE) from threeDist show yzA: "{y,z} ⊆ A" by simp next fix i assume iIs: "i ∈ Is" fix a b assume ab: "a ∈ {y, z}" "b ∈ {y, z}" with VIs profileP V2xyzP have V2yzP: "∀i ∈ ?V2. z ⇘(P i)⇙≺ y" by (blast dest: rpr_less_trans) show "(a ⇘(P' i)⇙≼ b) = (a ⇘(P i)⇙≼ b)" proof(cases "i ∈ ?V2") case True with VIs profileP profileP' ab V2yz' V2yzP threeDist show ?thesis unfolding strict_pref_def profile_def by auto next case False from V1xyzP V3xyzP have "∀i ∈ Is - ?V2. y ⇘(P i)⇙≺ z" by auto with iIs False VIs jV profileP profileP' ab nV2yz' threeDist show ?thesis unfolding profile_def strict_pref_def by auto qed qed (simp_all add: profileP profileP') with zPy show "z ⇘(swf P')⇙≺ y" unfolding strict_pref_def by blast qed with VIs Vsd Vmin[where V'="?V2"] V2card V2notempty threeDist show False by auto qed (simp add: profileP threeDist) qed have "semidecisive swf A Is ?V1 x z" proof from jV VIs show "{j} ⊆ Is" by blast next ― ‹Use @{term "iia"} to show the SWF must allow the individual to prevail.› fix P' assume profileP': "profile A Is P'" and V1yz': "⋀i. i ∈ ?V1 ⟹ x ⇘(P' i)⇙≺ z" and nV1yz': "⋀i. i ∈ Is - ?V1 ⟹ z ⇘(P' i)⇙≺ x" from iia have "⋀a b. ⟦ a ∈ {x, z}; b ∈ {x, z} ⟧ ⟹ (a ⇘(swf P)⇙≼ b) = (a ⇘(swf P')⇙≼ b)" proof(rule iiaE) from threeDist show xzA: "{x,z} ⊆ A" by simp next fix i assume iIs: "i ∈ Is" fix a b assume ab: "a ∈ {x, z}" "b ∈ {x, z}" show "(a ⇘(P' i)⇙≼ b) = (a ⇘(P i)⇙≼ b)" proof(cases "i ∈ ?V1") case True with jV VIs profileP V1xyzP have "∀i ∈ ?V1. x ⇘(P i)⇙≺ z" by (blast dest: rpr_less_trans) with True jV VIs profileP profileP' ab V1yz' threeDist show ?thesis unfolding strict_pref_def profile_def by auto next case False from V2xyzP V3xyzP have "∀i ∈ Is - ?V1. z ⇘(P i)⇙≺ x" by auto with iIs False VIs jV profileP profileP' ab nV1yz' threeDist show ?thesis unfolding strict_pref_def profile_def by auto qed qed (simp_all add: profileP profileP') with xPz show "x ⇘(swf P')⇙≺ z" unfolding strict_pref_def by blast qed with jV VIs Vsd Vmin[where V'="?V1"] V2card threeDist show False by auto qed with xyA Vsd show ?thesis by blast qed (* **************************************** *) subsection‹Arrow's General Possibility Theorem› text‹ Finally we conclude with the celebrated ``possibility'' result. Note that we assume the set of individuals is finite; \<^cite>‹"Routley:79"› relaxes this with some fancier set theory. Having an infinite set of alternatives doesn't matter, though the result is a bit more plausible if we assume finiteness \<^cite>‹‹p54› in "Sen:70a"›. › theorem ArrowGeneralPossibility: assumes has3A: "has 3 A" and finiteIs: "finite Is" and has2Is: "has 2 Is" and iia: "iia swf A Is" and swf: "SWF swf A Is universal_domain" and wp: "weak_pareto swf A Is universal_domain" obtains j where "dictator swf A Is j" using sd_imp_dictator[OF has3A iia swf wp] sd_exists[OF has3A finiteIs has2Is iia swf wp] by blast (*<*) end (*>*)