EconCSLib.SocialChoice.FairDivision.Indivisible.ImpossibilityEF #

Envy-freeness is not always achievable for indivisible goods.

Main result #

ef_impossible_two_agents_one_good — for 2 agents and 1 good that both want, every complete allocation is NOT envy-free.

Proof sketch #

Any complete allocation of a single good {g} between two agents assigns {g} to exactly one agent and ∅ to the other. The agent receiving ∅ envies the other whenever they value g more than nothing.

This is the canonical impossibility: EF always exists for divisible goods (via cut-and-choose), but fails even for the simplest indivisible instance.

References #

Nisan et al., Algorithmic Game Theory, Chapter 11

Main impossibility theorem #

source

theorem SocialChoice.FairDivision.Indivisible.ef_impossible_two_agents_one_good {G : Type u_1} [DecidableEq G] {g : G} (v : Valuation (Fin 2) G) (h0 : v.val 0 ∅ < v.val 0 {g}) (h1 : v.val 1 ∅ < v.val 1 {g}) {A : Allocation (Fin 2) G} (hA : IsAllocation {g} A) :

¬IsEnvyFree v A

EF Impossibility: for indivisible goods, envy-free complete allocations need not exist.

For 2 agents and 1 good g that both agents strictly prefer to nothing, every complete allocation is NOT envy-free.

Proof: any complete allocation of {g} gives g to one agent (say agent i) and ∅ to the other (agent j). Then v_j(A_i) = v_j({g}) > v_j(∅) = v_j(A_j), so agent j envies agent i.

Contrast with SocialChoice.FairDivision.Divisible.CutAndChoose, where EF always exists for two agents with nonatomic divisible measures. [AGT Ch.11]