Quelle  Arrow.thy

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

  proof falls into two parts: showing that a semi-decisive individual is
  fact a dictator, and that a semi-decisive individual exists. I take them
  that order.

  might be good to do some of this in a locale. The complication is
  where various witnesses need to be quantified over.

 ›

(* **************************************** *)

subsection‹Semi-decisiveness Implies Decisiveness›

text‹

  follow cite‹‹Chapter~3*› in "Sen:70a"› quite closely here. Formalising his
  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
 . Everyone else strictly prefers $y$ to each of $x$ to $z$, and
  the relative preferences between $x$ and $z$ from profile $P$.

  model has to be specific about ordering all the other alternatives, but
  are immaterial in the proof that uses this witness. Note also that the
  lemma is used with different instantiations of $x$, $y$ and $z$,
  we need to quantify over them here. This happens implicitly, but in a
  we would have to be more explicit.

  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)
        have "x ∈ A" and "y ∈ A" and "z ∈ A"
          using has3A by auto
        thus "?P' i ⊆ A × A"
          unfolding ij by auto
        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
  is semi-decisive for $x$ and $y$ is actually decisive for $x$ over any
  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
 .)›

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)
        have "x ∈ A" and "y ∈ A" and "z ∈ A"
          using has3A by auto
        thus "?P' i ⊆ A × A"
          using ij by auto
        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
  can be obtained from semi-decisiveness in all cases. Again,
  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$
  $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
 -decisive individual. The required witness is essentially an encoding of
  Condorcet pardox (aka "the paradox of voting" that shows we get tied up
  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 "?P i ⊆ A × A" by auto
      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
  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 simp del: diff_shunt)
    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‹

  we conclude with the celebrated ``possibility'' result. Note that we
  the set of individuals is finite; cite‹"Routley:79"› relaxes this with
  fancier set theory. Having an infinite set of alternatives doesn't
 , 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
(*>*)