Theory Fishburn_Impossibility
section ‹Main impossibility result›
theory Fishburn_Impossibility
imports
Social_Choice_Functions
begin
subsection ‹Setting of the base case›
text ‹
Suppose we have an anonymous, Fishburn-strategyproof, and Pareto-efficient SCF
for three agents $A1$ to $A3$ and three alternatives $a$, $b$, and $c$. We will derive
a contradiction from this.
›
locale fb_impossibility_3_3 =
strategyproof_anonymous_scf agents alts scf Fishb +
pareto_efficient_scf agents alts scf
for agents :: "'agent set" and alts :: "'alt set" and scf A1 A2 A3 a b c +
assumes agents_eq: "agents = {A1, A2, A3}"
assumes alts_eq: "alts = {a, b, c}"
assumes distinct_agents: "distinct [A1, A2, A3]"
assumes distinct_alts: "distinct [a, b, c]"
begin
text ‹
We first give some simple rules that will allow us to break down the strategyproofness
and support conditions more easily later.
›
lemma agents_neq [simp]: "A1 ≠ A2" "A2 ≠ A1" "A1 ≠ A3" "A3 ≠ A1" "A2 ≠ A3" "A3 ≠ A2"
using distinct_agents by auto
lemma alts_neq [simp]: "a ≠ b" "a ≠ c" "b ≠ c" "b ≠ a" "c ≠ a" "c ≠ b"
using distinct_alts by auto
lemma agent_in_agents [simp]: "A1 ∈ agents" "A2 ∈ agents" "A3 ∈ agents"
by (simp_all add: agents_eq)
lemma alt_in_alts [simp]: "a ∈ alts" "b ∈ alts" "c ∈ alts"
by (simp_all add: alts_eq)
lemma Bex_alts: "(∃x∈alts. P x) ⟷ P a ∨ P b ∨ P c"
by (simp add: alts_eq)
lemma eval_pareto_loser_aux:
assumes "is_pref_profile R"
shows "x ∈ pareto_losers R ⟷ (∃y∈{a,b,c}. x ≺[Pareto(R)] y)"
proof -
interpret pref_profile_wf agents alts R by fact
have *: "y ∈ {a,b,c}" if "x ≺[Pareto(R)] y" for y
using Pareto.strict_not_outside[of x y] that by (simp add: alts_eq)
show ?thesis by (auto simp: pareto_losers_def dest: *)
qed
lemma eval_Pareto:
assumes "is_pref_profile R"
shows "x ≺[Pareto(R)] y ⟷ (∀i∈{A1,A2,A3}. x ≼[R i] y) ∧ (∃i∈{A1,A2,A3}. ¬x ≽[R i] y)"
proof -
interpret R: pref_profile_wf agents alts by fact
show ?thesis unfolding R.Pareto_strict_iff by (auto simp: strongly_preferred_def agents_eq)
qed
lemmas eval_pareto = eval_pareto_loser_aux eval_Pareto
lemma pareto_efficiency: "is_pref_profile R ⟹ x ∈ pareto_losers R ⟹ x ∉ scf R"
using pareto_efficient[of R] by blast
lemma Ball_scf:
assumes "is_pref_profile R"
shows "(∀x∈scf R. P x) ⟷ (a ∉ scf R ∨ P a) ∧ (b ∉ scf R ∨ P b) ∧ (c ∉ scf R ∨ P c)"
using scf_alts[OF assms] unfolding alts_eq by blast
lemma Ball_scf_diff:
assumes "is_pref_profile R1" "is_pref_profile R2"
shows "(∀x∈scf R1 - scf R2. P x) ⟷
(a ∈ scf R2 ∨ a ∉ scf R1 ∨ P a) ∧ (b ∈ scf R2 ∨ b ∉ scf R1 ∨ P b) ∧
(c ∈ scf R2 ∨ c ∉ scf R1 ∨ P c)"
using assms[THEN scf_alts] unfolding alts_eq by blast
lemma scf_nonempty':
assumes "is_pref_profile R"
shows "∃x∈alts. x ∈ scf R"
using scf_nonempty[OF assms] scf_alts[OF assms] by blast
subsection ‹Definition of Preference Profiles and Fact Gathering›
text ‹
We now define the 21 preference profile that will lead to the impossibility result.
›