EconCSLib.SocialChoice.Basic

Generic social-choice vocabulary: alternatives, feasible sets, and instance-level rules/correspondences. Bundled preferences come from Foundation.Preference so that social choice, fair division, and matching use the same semantic object.

Main definitions

• SocialChoice.Instance N A — a generic social-choice instance over feasible alternatives and agent preferences
• SocialChoice.SolutionConcept N A — predicate selecting acceptable alternatives relative to an instance
• SocialChoice.Rule N A — a single-valued feasible choice
• SocialChoice.Correspondence N A — a set-valued choice rule

References

• [MSZ] Maschler, Solan, Zamir, Game Theory, Chapter 21
• Arrow, K.J. (1951). Social Choice and Individual Values.

Generic instances and rules

structure SocialChoice.Instance (N : Type u_1) (A : Type u_2) : Type (max u_1 u_2)

A generic social-choice instance consists of feasible alternatives together with each agent's preference over the alternative space.

• feasible : A → Prop

  Feasible alternatives for this instance.

• pref : N → Pref A

  Each agent's weak preference over alternatives.

def SocialChoice.SolutionConcept (N : Type u_1) (A : Type u_2) : Type (max u_2 u_1)

A solution concept is a predicate selecting acceptable alternatives relative to a social-choice instance.

Equations

• SocialChoice.SolutionConcept N A = (SocialChoice.Instance N A → A → Prop)

def SocialChoice.Rule (N : Type u_1) (A : Type u_2) : Type (max u_2 u_1)

A rule returns a feasible alternative for every instance.

Equations

• SocialChoice.Rule N A = ((I : SocialChoice.Instance N A) → { a : A // I.feasible a })

def SocialChoice.Correspondence (N : Type u_1) (A : Type u_2) : Type (max u_2 u_1)

A correspondence is a set-valued choice rule on instances.

Equations

• SocialChoice.Correspondence N A = (SocialChoice.Instance N A → Set A)