# Theory PAPP_Impossibility

```(*
File:     PAPP_Impossibility.thy
Author:   Manuel Eberl, University of Innsbruck
*)
section ‹Lifting the Impossibility Result to Larger Settings›
theory PAPP_Impossibility
imports PAPP_Impossibility_Base_Case Anonymous_PAPP_Lowering
begin

text ‹
In this section, we now prove the main results of this work by combining the base case
with the lifting arguments formalized earlier.

First, we prove the following very simple technical lemma: a set that is infinite or finite with
cardinality at least 2 contains two different elements ‹x› and ‹y›.
›

lemma obtain_2_elements:
assumes "infinite X ∨ card X ≥ 2"
obtains x y where "x ∈ X" "y ∈ X" "x ≠ y"
proof -
from assms have "X ≠ {}"
by auto
then obtain x where "x ∈ X"
by blast
with assms have "infinite X ∨ card (X - {x}) > 0"
by (subst card_Diff_subset) auto
hence "X - {x} ≠ {}"
by (metis card_gt_0_iff finite.emptyI infinite_remove)
then obtain y where "y ∈ X - {x}"
by blast
with ‹x ∈ X› show ?thesis
using that[of x y] by blast
qed

text ‹
We now have all the ingredients to formalise the first main impossibility result: There is
no P-APP rule that satisfies Anonymity, Cardinality-Strategyproofness, and Weak Representation
if ‹k ≥ 3› and ‹m ≥ k + 1› and ‹n› is a multiple of ‹2k›.

The proof simply uses the lowering lemmas we proved earlier to first reduce the committee size
to 3, then reduce the voters to 6, and finally restrict the parties to 4. At that point,
the base case we proved with SAT solving earlier kicks in.

This corresponds to Theorem~1 in the paper.
›
theorem papp_impossibility1:
assumes "k ≥ 3" and "card parties ≥ k + 1" and "finite parties"
shows   "¬card_stratproof_weak_rep_anon_papp (2 * k * l) parties k r"
using assms
proof (induction k arbitrary: parties r rule: less_induct)
case (less k parties r)
show ?case
proof (cases "k = 3")
assume [simp]: "k = 3"
text ‹
If the committee size is 3, we first use our voter-division lemma to
go from a P-APP rule for \$6l\$ voters to one with just 6 voters. Next, we choose 4 arbitrary
parties and use our party-restriction lemma to obtain a P-APP rule for just 4 parties.

But this is exactly our base case, which we already know to be infeasible.
›
show ?thesis
proof
assume "card_stratproof_weak_rep_anon_papp (2 * k * l) parties k r"
then interpret card_stratproof_weak_rep_anon_papp "l * 6" parties 3 r
interpret divide_voters_card_stratproof_weak_rep_anon_papp l 6 parties 3 r ..

have "card parties ≥ 4"
using less.prems by auto
then obtain parties' where parties': "parties' ⊆ parties" "card parties' = 4"
by (metis obtain_subset_with_card_n)
have "∃r. card_stratproof_weak_rep_anon_papp 6 parties' 3 r"
proof (rule card_stratproof_weak_rep_anon_papp_restrict_parties)
show "card_stratproof_weak_rep_anon_papp 6 parties 3 (r ∘ lift_profile)"
by (rule lowered.card_stratproof_weak_rep_anon_papp_axioms)
qed (use parties' in auto)
thus False
using papp_impossibility_base_case[OF parties'(2)] by blast
qed
next
assume "k ≠ 3"
text ‹
If the committee size is greater than 3, we use our other lowering lemma to reduce the
committee size by 1 (while also reducing the number of voters by \$2l\$ and the number of
parties by 1).
›
with less.prems have "k > 3"
by simp

obtain x y where xy: "x ∈ parties" "y ∈ parties" "x ≠ y"
using obtain_2_elements[of parties] less.prems by auto
define parties' where "parties' = parties - {y}"
have [simp]: "card parties' = card parties - 1"
unfolding parties'_def using xy by (subst card_Diff_subset) auto

show ?thesis
proof
assume "card_stratproof_weak_rep_anon_papp (2 * k * l) parties k r"
then interpret card_stratproof_weak_rep_anon_papp
"2 * l * (k - 1 + 1)" "insert y parties'" "k - 1 + 1" r
using ‹k > 3› xy by (simp add: parties'_def insert_absorb mult_ac)
interpret decrease_committee_card_stratproof_weak_rep_anon_papp "2 * l" "k - 1" y parties' r x
by unfold_locales (use ‹k > 3› xy in ‹auto simp: parties'_def›)
have "¬card_stratproof_weak_rep_anon_papp (2 * (k - 1) * l) parties' (k - 1) lowered"
by (rule less.IH) (use ‹k > 3› xy less.prems in auto)
with lowered.card_stratproof_weak_rep_anon_papp_axioms show False
qed
qed
qed

text ‹
If Weak Representation is replaced with Weak Proportional Representation, we can strengthen
the impossibility result by relaxing the conditions on the number of parties to ‹m ≥ 4›.

This works because with Weak Proportional Representation, we can reduce the size of the committee
without changing the number of parties. We use this to again bring \$k\$ down to \$3\$ without
changing \$m\$, at which point we can simply apply our previous impossibility result for
Weak Representation.

This corresponds to Theorem~2 in the paper.
›
corollary papp_impossibility2:
assumes "k ≥ 3" and "card parties ≥ 4" and "finite parties"
shows   "¬card_stratproof_weak_prop_rep_anon_papp (2 * k * l) parties k r"
using assms
proof (induction k arbitrary: parties r rule: less_induct)
case (less k parties r)
show ?case
proof (cases "k = 3")
assume [simp]: "k = 3"
text ‹
For committee size 3, we simply employ our previous impossibility result:
›
show ?thesis
proof
assume "card_stratproof_weak_prop_rep_anon_papp (2 * k * l) parties k r"
then interpret card_stratproof_weak_prop_rep_anon_papp "l * 6" parties 3 r
have "card_stratproof_weak_rep_anon_papp (l * 6) parties 3 r" ..
moreover have "¬card_stratproof_weak_rep_anon_papp (l * 6) parties 3 r"
using papp_impossibility1[of 3 parties l r] less.prems by (simp add: mult_ac)
ultimately show False
qed
next
assume "k ≠ 3"
text ‹
If the committee size is greater than 3, we use our other lowering lemma to reduce the
committee size by 1 (while also reducing the number of voters by \$2l\$).
›

with less.prems have "k > 3"
by simp

have "parties ≠ {}"
using less.prems by auto
then obtain x where x: "x ∈ parties"
by blast

show ?thesis
proof
assume "card_stratproof_weak_prop_rep_anon_papp (2 * k * l) parties k r"
then interpret card_stratproof_weak_prop_rep_anon_papp
"2 * l * (k - 1 + 1)" parties "k - 1 + 1" r
using ‹k > 3› by (simp add:  mult_ac)
interpret decrease_committee_card_stratproof_weak_prop_rep_anon_papp "2 * l" "k - 1" parties r x
by unfold_locales (use ‹k > 3› x in auto)
have "¬card_stratproof_weak_prop_rep_anon_papp (2 * (k - 1) * l) parties (k - 1) lowered"
by (rule less.IH) (use ‹k > 3› less.prems in auto)
with lowered.card_stratproof_weak_prop_rep_anon_papp_axioms show False