EconCSLib.Foundation.Preference

Abstract interfaces for agent preferences, shared across the library.

Mathlib already provides Preorder (reflexive + transitive) and LinearOrder (total + antisymmetric + decidable). This file adds domain-specific vocabulary on top, without fixing a specific representation.

The library uses two complementary interfaces:

• ambient order instances such as [TotalPreorder A] when a type carries one relevant preference order, for example a payoff type;
• bundled preferences Pref A when several agents may rank the same outcome type differently.

Design

• Weak preference a ≿ b = Mathlib's a ≤ b on a Preorder
• Strict preference a ≻ b = Mathlib's a < b = a ≤ b ∧ ¬(b ≤ a)
• Indifference a ∼ b = a ≤ b ∧ b ≤ a (need not imply a = b without antisymmetry)
• For social choice (ordinal strict preferences): use LinearOrder
• For utility theory (allowing indifference): use Preorder + IsTotal

Main definitions

• Indifferent — a ∼ b iff a ≤ b ∧ b ≤ a
• StrictlyPreferred — a ≻ b iff a < b (alias for readability)
• TotalPreorder — a preorder where ≤ is total (no antisymmetry required)
• Pref — a bundled total preorder, for agent-indexed preferences
• RepresentsPreference — utility function u represents preference ≤

References

• [MSZ] Maschler, Solan, Zamir, Game Theory, Chapter 2, Definitions 2.1–2.7

Relation-level vocabulary

def strict {A : Type u_1} (R : A → A → Prop) (a b : A) : Prop

Strict preference derived from a weak preference relation.

Equations

• strict R a b = (R a b ∧ ¬R b a)

def indiff {A : Type u_1} (R : A → A → Prop) (a b : A) : Prop

Indifference derived from a weak preference relation.

Equations

• indiff R a b = (R a b ∧ R b a)

theorem strict_transitive {A : Type u_1} {R : A → A → Prop} (h : Transitive R) : Transitive (strict R)

Derived strict preference is transitive when the weak relation is transitive.

Indifference and strict preference

def Indifferent {A : Type u_1} [Preorder A] (a b : A) : Prop

Two outcomes are indifferent under a preorder: a ≤ b ∧ b ≤ a. In a PartialOrder this implies a = b; in a general Preorder it does not. [MSZ 2.5]

Equations

• Indifferent a b = (a ≤ b ∧ b ≤ a)

theorem Indifferent.refl {A : Type u_1} [Preorder A] (a : A) : Indifferent a a

Indifference is reflexive.

theorem Indifferent.symm {A : Type u_1} [Preorder A] {a b : A} (h : Indifferent a b) : Indifferent b a

Indifference is symmetric.

theorem Indifferent.trans {A : Type u_1} [Preorder A] {a b c : A} (h₁ : Indifferent a b) (h₂ : Indifferent b c) : Indifferent a c

Indifference is transitive.

@[reducible, inline]

abbrev StrictlyPreferred {A : Type u_1} [Preorder A] (a b : A) : Prop

Strict preference is just < from the preorder. [MSZ 2.5]

Equations

• StrictlyPreferred a b = (a < b)

theorem StrictlyPreferred.asymm {A : Type u_1} [Preorder A] {a b : A} (h : StrictlyPreferred a b) : ¬StrictlyPreferred b a

Strict preference is asymmetric: a ≻ b → ¬(b ≻ a). [MSZ Ex 2.1(a)]

theorem StrictlyPreferred.trans {A : Type u_1} [Preorder A] {a b c : A} (h₁ : StrictlyPreferred a b) (h₂ : StrictlyPreferred b c) : StrictlyPreferred a c

Strict preference is transitive. [MSZ Ex 2.1(a)]

theorem StrictlyPreferred.irrefl {A : Type u_1} [Preorder A] (a : A) : ¬StrictlyPreferred a a

Strict preference is irreflexive. [MSZ Ex 2.1(a)]

Total preorder

class TotalPreorder (A : Type u_1) extends Preorder A : Type u_1

A total preorder: a preorder where ≤ is total (complete). This is weaker than LinearOrder — it does NOT require antisymmetry or decidable equality. Two distinct elements can be indifferent.

This is the appropriate notion for weak preferences in utility theory and matching theory. [MSZ 2.1–2.4]

• le : A → A → Prop
• lt : A → A → Prop
• le_refl (a : A) : a ≤ a
• le_trans (a b c : A) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : A) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_total (a b : A) : a ≤ b ∨ b ≤ a

  The preference relation is complete: for any a b, either a ≤ b or b ≤ a.

theorem TotalPreorder.comparable {A : Type u_1} [TotalPreorder A] (a b : A) : a ≤ b ∨ b ≤ a

In a total preorder, any two elements are comparable.

@[implicit_reducible, instance 100]

instance LinearOrder.toTotalPreorder {A : Type u_1} [LinearOrder A] : TotalPreorder A

Every LinearOrder is a TotalPreorder.

Equations

• LinearOrder.toTotalPreorder = { toPreorder := inst✝.toPreorder, le_total := ⋯ }

Bundled preferences

class IsPreference {A : Type u_1} (R : A → A → Prop) : Prop

A weak preference relation is admissible if it is reflexive, transitive, and total.

• reflexive : Reflexive R
• transitive : Transitive R
• total (a b : A) : R a b ∨ R b a

structure Pref (A : Type u_1) : Type u_1

A bundled weak preference relation.

Use this interface when several agents may rank the same outcome type differently. Use [TotalPreorder A] when the outcome type carries one relevant ambient preference order.

• rel : A → A → Prop
• prop : IsPreference self.rel

@[implicit_reducible]

instance instCoeFunPrefForallForallProp {A : Type u_1} : CoeFun (Pref A) fun (x : Pref A) => A → A → Prop

Equations

• instCoeFunPrefForallForallProp = { coe := fun (p : Pref A) => p.rel }

def Pref.lt {A : Type u_1} (p : Pref A) (a b : A) : Prop

p.lt a b: outcome a is strictly preferred to b under preference p.

Equations

• p.lt a b = strict p.rel a b

def Pref.indifferent {A : Type u_1} (p : Pref A) (a b : A) : Prop

p.indiff a b: outcomes a and b are indifferent under preference p.

Equations

• p.indifferent a b = indiff p.rel a b

def Pref.ofTotalPreorder {A : Type u_1} (r : TotalPreorder A) : Pref A

Bundle an explicit total preorder as a preference.

Equations

• Pref.ofTotalPreorder r = { rel := fun (a b : A) => a ≤ b, prop := ⋯ }

def Pref.ofLinearOrder {A : Type u_1} (r : LinearOrder A) : Pref A

Bundle an explicit linear order as a preference.

Equations

• Pref.ofLinearOrder r = { rel := fun (a b : A) => a ≤ b, prop := ⋯ }

def PrefProfile (N : Type u_1) (A : Type u_2) : Type (max u_1 u_2)

A preference profile assigns each agent a bundled preference.

Equations

• PrefProfile N A = (N → Pref A)

Utility representation

structure RepresentsPreference {A : Type u_1} {V : Type u_2} [Preorder A] [Preorder V] (u : A → V) : Prop

A utility function u : A → V represents the preference ≤ on A if a ≤ b ↔ u a ≤ u b. [MSZ 2.7]

• le_iff (a b : A) : a ≤ b ↔ u a ≤ u b

  The representation property: a ≤ b ↔ u(a) ≤ u(b).

theorem RepresentsPreference.lt_iff {A : Type u_1} {V : Type u_2} [Preorder A] [Preorder V] {u : A → V} (h : RepresentsPreference u) (a b : A) : a < b ↔ u a < u b

A utility representation preserves strict preference.

theorem RepresentsPreference.indifferent_iff {A : Type u_1} {V : Type u_2} [Preorder A] [Preorder V] {u : A → V} (h : RepresentsPreference u) (a b : A) : Indifferent a b ↔ Indifferent (u a) (u b)

A utility representation preserves indifference.

Preference relation axioms (vNM)

General axioms for preference relations, stated for an arbitrary binary relation. Lottery-specific axioms (Independence, Continuity) are in Utility.VNMAxioms.

def VNM.Completeness {A : Type u_1} (pref : A → A → Prop) : Prop

Completeness: every pair is comparable.

Equations

• VNM.Completeness pref = ∀ (a b : A), pref a b ∨ pref b a

def VNM.Transitivity {A : Type u_1} (pref : A → A → Prop) : Prop

Transitivity: preference chains compose.

Equations

• VNM.Transitivity pref = ∀ (a b c : A), pref a b → pref b c → pref a c