Theory Arrow_Utility
section "Arrow's Theorem for Utility Functions"
theory Arrow_Utility imports Complex_Main
begin
text‹This theory formalizes the first proof due to
Geanakoplos~\<^cite>‹"Geanakoplos05"›. In contrast to the standard model
of preferences as linear orders, we model preferences as \emph{utility
functions} mapping each alternative to a real number. The type of
alternatives and voters is assumed to be finite.›
typedecl alt
typedecl indi
axiomatization where
alt3: "∃a b c::alt. distinct[a,b,c]" and
finite_alt: "finite(UNIV:: alt set)" and
finite_indi: "finite(UNIV:: indi set)"
lemma third_alt: "a ≠ b ⟹ ∃c::alt. distinct[a,b,c]"
using alt3 by simp metis
lemma alt2: "∃b::alt. b ≠ a"
using alt3 by simp metis
type_synonym pref = "alt ⇒ real"
type_synonym prof = "indi ⇒ pref"
definition
top :: "pref ⇒ alt ⇒ bool" (infixr "<⋅" 60) where
"p <⋅ b ≡ ∀a. a ≠ b ⟶ p a < p b"
definition
bot :: "alt ⇒ pref ⇒ bool" (infixr "⋅<" 60) where
"b ⋅< p ≡ ∀a. a ≠ b ⟶ p b < p a"
definition
extreme :: "pref ⇒ alt ⇒ bool" where
"extreme p b ≡ b ⋅< p ∨ p <⋅ b"
abbreviation
"Extreme P b == ∀i. extreme (P i) b"
lemma [simp]: "r <= s ⟹ r < s+(1::real)"
by arith
lemma [simp]: "r < s ⟹ r < s+(1::real)"
by arith
lemma [simp]: "r <= s ⟹ ¬ s+(1::real) < r"
by arith
lemma [simp]: "(r < s-(1::real)) = (r+1 < s)"
by arith
lemma [simp]: "(s-(1::real) < r) = (s < r+1)"
by arith
lemma less_if_bot[simp]: "⟦ b ⋅< p; x ≠ b ⟧ ⟹ p b < p x"
by(simp add:bot_def)
lemma [simp]: "⟦ p <⋅ b; x ≠ b ⟧ ⟹ p x < p b"
by(simp add:top_def)
lemma [simp]: assumes top: "p <⋅ b" shows "¬ p b < p c"
proof (cases)
assume "b = c" thus ?thesis by simp
next
assume "b ≠ c"
with top have "p c < p b" by (simp add:eq_sym_conv)
thus ?thesis by simp
qed
lemma not_less_if_bot[simp]:
assumes bot: "b ⋅< p" shows "¬ p c < p b"
proof (cases)
assume "b = c" thus ?thesis by simp
next
assume "b ≠ c"
with bot have "p b < p c" by (simp add:eq_sym_conv)
thus ?thesis by simp
qed
lemma top_impl_not_bot[simp]: "p <⋅ b ⟹ ¬ b ⋅< p"
by(unfold bot_def, simp add:alt2)
lemma [simp]: "extreme p b ⟹ (¬ p <⋅ b) = (b ⋅< p)"
apply(unfold extreme_def)
apply(fastforce dest:top_impl_not_bot)
done
lemma [simp]: "extreme p b ⟹ (¬ b ⋅< p) = (p <⋅ b)"
apply(unfold extreme_def)
apply(fastforce dest:top_impl_not_bot)
done
text‹Auxiliary construction to hide details of preference model.›
definition
mktop :: "pref ⇒ alt ⇒ pref" where
"mktop p b ≡ p(b := Max(range p) + 1)"
definition
mkbot :: "pref ⇒ alt ⇒ pref" where
"mkbot p b ≡ p(b := Min(range p) - 1)"
definition
between :: "pref ⇒ alt ⇒ alt ⇒ alt ⇒ pref" where
"between p a b c ≡ p(b := (p a + p c)/2)"
text‹To make things simpler:›
declare between_def[simp]
lemma [simp]: "a ≠ b ⟹ mktop p b a = p a"
by(simp add:mktop_def)
lemma [simp]: "a ≠ b ⟹ mkbot p b a = p a"
by(simp add:mkbot_def)
lemma [simp]: "a ≠ b ⟹ p a < mktop p b b"
by(simp add:mktop_def finite_alt)
lemma [simp]: "a ≠ b ⟹ mkbot p b b < p a"
by(simp add:mkbot_def finite_alt)
lemma [simp]: "mktop p b <⋅ b"
by(simp add:mktop_def top_def finite_alt)
lemma [simp]: "¬ b ⋅< mktop p b"
by(simp add:mktop_def bot_def alt2 finite_alt)
lemma [simp]: "a ≠ b ⟹ ¬ P p a < mkbot (P p) b b"
proof (simp add:mkbot_def finite_alt)
have "¬ P p a + 1 < P p a" by simp
thus "∃x. ¬ P p a + 1 < P p x" ..
qed
text‹The proof starts here.›
locale arrow =
fixes F :: "prof ⇒ pref"
assumes unanimity: "(⋀i. P i a < P i b) ⟹ F P a < F P b"
and IIA:
"(⋀i. (P i a < P i b) = (P' i a < P' i b)) ⟹
(F P a < F P b) = (F P' a < F P' b)"
begin
lemmas IIA' = IIA[THEN iffD1]
definition
dictates :: "indi ⇒ alt ⇒ alt ⇒ bool" ("_ dictates _ < _") where
"(i dictates a < b) ≡ ∀P. P i a < P i b ⟶ F P a < F P b"
definition
dictates2 :: "indi ⇒ alt ⇒ alt ⇒ bool" ("_ dictates _,_") where
"(i dictates a,b) ≡ (i dictates a < b) ∧ (i dictates b < a)"
definition
dictatesx:: "indi ⇒ alt ⇒ bool" ("_ dictates'_except _") where
"(i dictates_except c) ≡ ∀a b. c ∉ {a,b} ⟶ (i dictates a<b)"
definition
dictator :: "indi ⇒ bool" where
"dictator i ≡ ∀a b. (i dictates a<b)"
definition
pivotal :: "indi ⇒ alt ⇒ bool" where
"pivotal i b ≡
∃P. Extreme P b ∧ b ⋅< P i ∧ b ⋅< F P ∧
F (P(i := mktop (P i) b)) <⋅ b"
lemma all_top[simp]: "∀i. P i <⋅ b ⟹ F P <⋅ b"
by (unfold top_def) (simp add: unanimity)
lemma not_extreme:
assumes nex: "¬ extreme p b"
shows "∃a c. distinct[a,b,c] ∧ ¬ p a < p b ∧ ¬ p b < p c"
proof -
obtain a c where abc: "a ≠ b ∧ ¬ p a < p b" "b ≠ c ∧ ¬ p b < p c"
using nex by (unfold extreme_def top_def bot_def) fastforce
show ?thesis
proof (cases "a = c")
assume "a ≠ c" thus ?thesis using abc by simp blast
next
assume ac: "a = c"
obtain d where d: "distinct[a,b,d]" using abc third_alt by blast
show ?thesis
proof (cases "p b < p d")
case False thus ?thesis using abc d by blast
next
case True
hence db: "¬ p d < p b" by arith
from d have "distinct[d,b,c]" by(simp add:ac eq_sym_conv)
thus ?thesis using abc db by blast
qed
qed
qed
lemma extremal:
assumes extremes: "Extreme P b" shows "extreme (F P) b"
proof (rule ccontr)
assume nec: "¬ extreme (F P) b"
hence "∃a c. distinct[a,b,c] ∧ ¬ F P a < F P b ∧ ¬ F P b < F P c"
by(rule not_extreme)
then obtain a c where d: "distinct[a,b,c]" and
ab: "¬ F P a < F P b" and bc: "¬ F P b < F P c" by blast
let ?P = "λi. if P i <⋅ b then between (P i) a c b
else (P i)(c := P i a + 1)"
have "¬ F ?P a < F ?P b"
using extremes d by(simp add:IIA[of _ _ _ P] ab)
moreover have "¬ F ?P b < F ?P c"
using extremes d by(simp add:IIA[of _ _ _ P] bc eq_sym_conv)
moreover have "F ?P a < F ?P c" by(rule unanimity)(insert d, simp)
ultimately show False by arith
qed
lemma pivotal_ind: assumes fin: "finite D"
shows "⋀P. ⟦ D = {i. b ⋅< P i}; Extreme P b; b ⋅< F P ⟧
⟹ ∃i. pivotal i b" (is "⋀P. ?D D P ⟹ ?E P ⟹ ?B P ⟹ _")
using fin
proof (induct)
case (empty P)
from empty(1,2) have "∀i. P i <⋅ b" by simp
hence "F P <⋅ b" by simp
hence False using empty by(blast dest:top_impl_not_bot)
thus ?case ..
next
fix D i P
assume IH: "⋀P. ?D D P ⟹ ?E P ⟹ ?B P ⟹ ∃i. pivotal i b"
and "?E P" and "?B P" and insert: "insert i D = {i. b ⋅< P i}" and "i ∉ D"
from insert have "b ⋅< P i" by blast
let ?P = "P(i := mktop (P i) b)"
show "∃i. pivotal i b"
proof (cases "F ?P <⋅ b")
case True
have "pivotal i b"
proof -
from ‹?E P› ‹?B P› ‹b ⋅< P i› True
show ?thesis by(unfold pivotal_def, blast)
qed
thus ?thesis ..
next
case False
have "D = {i. b ⋅< ?P i}"
by (rule set_eqI) (simp add:‹i ∉ D›, insert insert, blast)
moreover have "Extreme ?P b"
using ‹?E P› by (simp add:extreme_def)
moreover have "b ⋅< F ?P"
using extremal[OF ‹Extreme ?P b›] False by(simp del:fun_upd_apply)
ultimately show ?thesis by(rule IH)
qed
qed
lemma pivotal_exists: "∃i. pivotal i b"
proof -
let ?P = "(λ_ a. if a=b then 0 else 1)::prof"
have "Extreme ?P b" by(simp add:extreme_def bot_def)
moreover have "b ⋅< F ?P"
by(simp add:bot_def unanimity del: less_if_bot not_less_if_bot)
ultimately show "∃i. pivotal i b"
by (rule pivotal_ind[OF finite_subset[OF subset_UNIV finite_indi] refl])
qed
lemma pivotal_xdictates: assumes pivo: "pivotal i b"
shows "i dictates_except b"
proof -
have "⋀a c. ⟦ a ≠ b; b ≠ c ⟧ ⟹ i dictates a < c"
proof (unfold dictates_def, intro allI impI)
fix a c and P::prof
assume abc: "a ≠ b" "b ≠ c" and
ac: "P i a < P i c"
show "F P a < F P c"
proof -
obtain P1 P2 where
"Extreme P1 b" and "b ⋅< F P1" and "b ⋅< P1 i" and "F P2 <⋅ b" and
[simp]: "P2 = P1(i := mktop (P1 i) b)"
using pivo by (unfold pivotal_def) fast
let ?P = "λj. if j=i then between (P j) a b c
else if P1 j <⋅ b then mktop (P j) b else mkbot (P j) b"
have eq: "(F P a < F P c) = (F ?P a < F ?P c)"
using abc by - (rule IIA, auto)
have "F ?P a < F ?P b"
proof (rule IIA')
fix j show "(P2 j a < P2 j b) = (?P j a < ?P j b)"
using ‹Extreme P1 b› by(simp add: ac)
next
show "F P2 a < F P2 b"
using ‹F P2 <⋅ b› abc by(simp add: eq_sym_conv)
qed
also have "… < F ?P c"
proof (rule IIA')
fix j show "(P1 j b < P1 j c) = (?P j b < ?P j c)"
using ‹Extreme P1 b› ‹b ⋅< P1 i› by(simp add: ac)
next
show "F P1 b < F P1 c"
using ‹b ⋅< F P1› abc by(simp add: eq_sym_conv)
qed
finally show ?thesis by(simp add:eq)
qed
qed
thus ?thesis by(unfold dictatesx_def) fast
qed
lemma pivotal_is_dictator:
assumes pivo: "pivotal i b" and ab: "a ≠ b" and d: "j dictates a,b"
shows "i = j"
proof (rule ccontr)
assume pd: "i ≠ j"
obtain P1 P2 where "Extreme P1 b" and "b ⋅< F P1" and "F P2 <⋅ b" and
P2: "P2 = P1(i := mktop (P1 i) b)"
using pivo by (unfold pivotal_def) fast
have "~(P1 j a < P1 j b)" (is "~ ?ab")
proof
assume "?ab"
hence "F P1 a < F P1 b" using d by(simp add: dictates_def dictates2_def)
with ‹b ⋅< F P1› show False by simp
qed
hence "P1 j b < P1 j a" using ‹Extreme P1 b›[THEN spec, of j] ab
unfolding extreme_def top_def bot_def by metis
hence "P2 j b < P2 j a" using pd by (simp add:P2)
hence "F P2 b < F P2 a" using d by(simp add: dictates_def dictates2_def)
with ‹F P2 <⋅ b› show False by simp
qed
theorem dictator: "∃i. dictator i"
proof-
from pivotal_exists[of b] obtain i where pivo: "pivotal i b" ..
{ fix a assume neq: "a ≠ b" have "i dictates a,b"
proof -
obtain c where dist: "distinct[a,b,c]"
using neq third_alt by blast
obtain j where "pivotal j c" using pivotal_exists by fast
hence "j dictates_except c" by(rule pivotal_xdictates)
hence b: "j dictates a,b"
using dist by(simp add:dictatesx_def dictates2_def eq_sym_conv)
with pivo neq have "i = j" by(rule pivotal_is_dictator)
thus ?thesis using b by simp
qed
}
with pivotal_xdictates[OF pivo] have "dictator i"
by(simp add: dictates_def dictatesx_def dictates2_def dictator_def)
(metis less_le)
thus ?thesis ..
qed
end
end