Social welfare functionals

In Sen's framework for social choice with interpersonal comparisons, each individual assigns each alternative a value, and a rule sends every profile of values to an overall relation on the alternatives, read x ⪰ y. Here a profile assigns each alternative its vector of values, one per individual; the individuals may equally be voters, criteria or dimensions.

The informational requirements on a rule are invariance under a class of transformation vectors: strictly increasing maps, common-unit positive affine maps, similarities, and the comparability classes that apply one map to every individual. Arrow's conditions and the strong Pareto, Pareto-indifference and anonymity conditions are predicates on rules.

Main definitions

• SocialChoice.Profile, SocialChoice.Rule: profiles of values and rules on them.
• SocialChoice.Invariant: invariance under a class of transformation vectors, with the classes ordinal, ordinalLevel, cardinalUnit, ratio, cardinalFull and ratioFull.
• SocialChoice.WeakPareto, SocialChoice.Independent, SocialChoice.WeakOrderValued, SocialChoice.IsDictator: Arrow's conditions.

Implementation notes

• A rule is total on profiles, so Arrow's unrestricted-domain condition is built in; a domain restriction is a hypothesis of the statement that needs it.
• Outputs are bare relations, since majority rule is not transitive. AsymmRel is the strict part of an output and AntisymmRel its indifference part.

References

• [Arr50]
• [Sen70]

@[reducible, inline]

abbrev SocialChoice.Profile (ι : Type u_4) (α : Type u_5) (K : Type u_6) : Type (max (max u_4 u_5) u_6)

A profile assigns each alternative its vector of values, one per individual.

Equations

• SocialChoice.Profile ι α K = (α → ι → K)

@[reducible, inline]

abbrev SocialChoice.Rule (ι : Type u_4) (α : Type u_5) (K : Type u_6) : Type (max (max u_5 u_6) u_4)

An aggregation rule assigns to each profile a relation on the alternatives, read x ⪰ y.

Equations

• SocialChoice.Rule ι α K = (SocialChoice.Profile ι α K → α → α → Prop)

def SocialChoice.Profile.transform {ι : Type u_1} {α : Type u_2} {K : Type u_3} (f : ι → K → K) (v : Profile ι α K) : Profile ι α K

A vector of transformations, one per individual, applied to a profile.

Equations

• SocialChoice.Profile.transform f v x i = f i (v x i)

Informational invariance

def SocialChoice.Invariant {ι : Type u_1} {α : Type u_2} {K : Type u_3} {β : Type u_4} (T : Set (ι → K → K)) (a : Profile ι α K → β) : Prop

Invariance of a function of profiles, such as a rule or a statement about values, under a class of transformation vectors.

Equations

• SocialChoice.Invariant T a = ∀ (f : ι → K → K), f ∈ T → ∀ (v : SocialChoice.Profile ι α K), a (SocialChoice.Profile.transform f v) = a v

theorem SocialChoice.Invariant.mono {ι : Type u_1} {α : Type u_2} {K : Type u_3} {β : Type u_4} {S T : Set (ι → K → K)} (h : S ⊆ T) {a : Profile ι α K → β} (ha : Invariant T a) : Invariant S a

def SocialChoice.ordinal {ι : Type u_1} {K : Type u_3} [Preorder K] : Set (ι → K → K)

Vectors of strictly increasing transformations; invariance under them is ordinal non-comparability.

Equations

• SocialChoice.ordinal = {f : ι → K → K | ∀ (i : ι), StrictMono (f i)}

def SocialChoice.ordinalLevel {ι : Type u_1} {K : Type u_3} [Preorder K] : Set (ι → K → K)

Vectors applying one strictly increasing transformation to every individual; invariance under them is ordinal level comparability.

Equations

• SocialChoice.ordinalLevel = {f : ι → K → K | ∃ (u : K → K), StrictMono u ∧ ∀ (i : ι), f i = u}

theorem SocialChoice.ordinalLevel_subset_ordinal {ι : Type u_1} {K : Type u_3} [Preorder K] : ordinalLevel ⊆ ordinal

def SocialChoice.cardinalUnit {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] : Set (ι → K → K)

Common-unit positive affine transformation vectors; invariance under them is cardinal unit comparability.

Equations

• SocialChoice.cardinalUnit = {f : ι → K → K | ∃ (a : K), 0 < a ∧ ∃ (b : ι → K), ∀ (i : ι) (t : K), f i t = a * t + b i}

def SocialChoice.ratio {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] : Set (ι → K → K)

Similarity transformation vectors; invariance under them is ratio-scale non-comparability.

Equations

• SocialChoice.ratio = {f : ι → K → K | ∃ (a : ι → K), (∀ (i : ι), 0 < a i) ∧ ∀ (i : ι) (t : K), f i t = a i * t}

def SocialChoice.cardinalFull {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] : Set (ι → K → K)

Vectors applying one positive affine transformation to every individual; invariance under them is cardinal full comparability.

Equations

• SocialChoice.cardinalFull = {f : ι → K → K | ∃ (a : K), 0 < a ∧ ∃ (b : K), ∀ (i : ι) (t : K), f i t = a * t + b}

def SocialChoice.ratioFull {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] : Set (ι → K → K)

Vectors applying one similarity transformation to every individual; invariance under them is ratio-scale full comparability.

Equations

• SocialChoice.ratioFull = {f : ι → K → K | ∃ (a : K), 0 < a ∧ ∀ (i : ι) (t : K), f i t = a * t}

theorem SocialChoice.cardinalFull_subset_cardinalUnit {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] : cardinalFull ⊆ cardinalUnit

theorem SocialChoice.ratioFull_subset_cardinalFull {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] : ratioFull ⊆ cardinalFull

theorem SocialChoice.ratioFull_subset_ratio {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] : ratioFull ⊆ ratio

theorem SocialChoice.cardinalFull_subset_ordinalLevel {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] [IsStrictOrderedRing K] : cardinalFull ⊆ ordinalLevel

theorem SocialChoice.cardinalUnit_subset_ordinal {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] [IsStrictOrderedRing K] : cardinalUnit ⊆ ordinal

theorem SocialChoice.ratio_subset_ordinal {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] [IsStrictOrderedRing K] : ratio ⊆ ordinal

Conditions on rules

def SocialChoice.ParetoIndifferent {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Pareto indifference says that alternatives with the same vector of values are indifferent.

Equations

• SocialChoice.ParetoIndifferent a = ∀ (v : SocialChoice.Profile ι α K) (x y : α), v x = v y → AntisymmRel (a v) x y

def SocialChoice.Independent {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Independence of irrelevant alternatives says that the verdict on a pair depends only on the vectors of that pair.

Equations

• SocialChoice.Independent a = ∀ (v w : SocialChoice.Profile ι α K) (x y : α), v x = w x → v y = w y → (a v x y ↔ a w x y)

def SocialChoice.Transitive {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Every output is transitive.

Equations

• SocialChoice.Transitive a = ∀ (v : SocialChoice.Profile ι α K), IsTrans α (a v)

def SocialChoice.Complete {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Every output is complete.

Equations

• SocialChoice.Complete a = ∀ (v : SocialChoice.Profile ι α K), Std.Total (a v)

def SocialChoice.WeakOrderValued {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Every output is a weak ordering, a complete preorder.

Equations

• SocialChoice.WeakOrderValued a = (SocialChoice.Transitive a ∧ SocialChoice.Complete a)

def SocialChoice.QuasiOrderValued {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Every output is a quasi-ordering, a preorder.

Equations

• SocialChoice.QuasiOrderValued a = ∀ (v : SocialChoice.Profile ι α K), IsPreorder α (a v)

def SocialChoice.Anonymous {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Anonymity says that permuting the individuals leaves the output unchanged.

Equations

• SocialChoice.Anonymous a = ∀ (σ : Equiv.Perm ι) (v : SocialChoice.Profile ι α K), (a fun (x : α) => v x ∘ ⇑σ) = a v

theorem SocialChoice.WeakOrderValued.quasiOrderValued {ι : Type u_1} {α : Type u_2} {K : Type u_3} {a : Rule ι α K} (h : WeakOrderValued a) : QuasiOrderValued a

def SocialChoice.WeakPareto {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) [Preorder K] : Prop

Weak Pareto says that an alternative every individual ranks strictly above another is strictly preferred.

Equations

• SocialChoice.WeakPareto a = ∀ (v : SocialChoice.Profile ι α K) (x y : α), (∀ (i : ι), v y i < v x i) → AsymmRel (a v) x y

def SocialChoice.StrongPareto {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) [Preorder K] : Prop

Strong Pareto says that an alternative every individual ranks weakly above another is weakly preferred, and strictly so if some individual ranks it strictly above.

Equations

• SocialChoice.StrongPareto a = ∀ (v : SocialChoice.Profile ι α K) (x y : α), v y ≤ v x → a v x y ∧ ((∃ (i : ι), v y i < v x i) → AsymmRel (a v) x y)

def SocialChoice.IsDictator {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) [Preorder K] (i : ι) : Prop

Individual i is a dictator when its strict rankings are the strict overall rankings.

Equations

• SocialChoice.IsDictator a i = ∀ (v : SocialChoice.Profile ι α K) (x y : α), v y i < v x i → AsymmRel (a v) x y

def SocialChoice.NonDictatorial {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) [Preorder K] : Prop

No individual is a dictator.

Equations

• SocialChoice.NonDictatorial a = ∀ (i : ι), ¬SocialChoice.IsDictator a i