# Theory Arrow

```(*
* Arrow's General Possibility Theorem, following Sen.
* (C)opyright Peter Gammie, peteg42 at gmail.com, commenced July 2006.
*)

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