Quelle  Sen.thy

(*
 * 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
  the social choice function need to be weakened. One approach is to only
  that the set of alternatives that society ranks highest (and is
  indifferent about) be non-empty.

  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)
 . The lemma uses a witness to show the absence of a
 .›

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
 . I leave these for future work.›

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

subsection‹Sen's Liberal Paradox›

text‹Having side-stepped Arrow's Theorem, Sen proceeds to other conditions
  may ask of an SCF. His analysis of \emph{liberalism}, mechanised in this
 , has attracted much criticism over the years
 cite‹"AnalyseKritik:1996"›.

  cite‹‹Chapter~6*› in "Sen:70a"›, a \emph{liberal} social choice rule is
  that, for each individual, there is a pair of alternatives that she is
  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
 ; if we required just one, we would allow dictatorships, which
  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‹

  key observation is that once we have at least two decisive individuals
  can complete the Condorcet (paradox of voting) cycle using the weak
  assumption. The details of the proof don't give more insight.

  we need three types of profile witnesses (one of which we saw
 ). The main proof proceeds by case distinctions on which
  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 "?P i ⊆ A × A" by auto
      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 "?P i ⊆ A × A" by auto
      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
  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
(*>*)