Documentation

EconCSLib.Foundation.Utility.VNMAxioms

EconCSLib.Foundation.Utility.VNMAxioms #

The four axioms for expected utility theory, stated as predicates on a preference relation over lotteries.

Main definitions #

Main results #

References #

Lottery-specific axioms #

strict, indiff, Completeness, Transitivity are defined in Foundation.Preference for general binary relations. Here we add the two lottery-specific axioms that reference Lottery.mix.

def VNM.Independence {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {O : Type u_2} [Fintype O] (pref : (Lottery 𝕜 O)(Lottery 𝕜 O)Prop) :

Independence: mixing both sides with a common lottery preserves preference. L₁L₂ ↔ [α L₁, (1-α) N] ≿ [α L₂, (1-α) N] for α > 0.

Equations
Instances For
    def VNM.Continuity {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {O : Type u_2} [Fintype O] (pref : (Lottery 𝕜 O)(Lottery 𝕜 O)Prop) :

    Continuity (Archimedean / MSZ Axiom 2.12): for L₁L₂L₃, there exists θ ∈ [0,1] such that L₂ ∼ [θ L₁, (1-θ) L₃].

    Equations
    Instances For

      Consequences of the axioms #

      theorem VNM.sure_thing_principle {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {O : Type u_2} [Fintype O] {pref : (Lottery 𝕜 O)(Lottery 𝕜 O)Prop} (hind : Independence pref) (L₁ L₂ L₃ L₄ : (Lottery 𝕜 O)) (α : 𝕜) (hα₀ : 0 α) (hα₁ : α 1) :
      strict pref (Lottery.mix α hα₀ hα₁ L₁ L₃) (Lottery.mix α hα₀ hα₁ L₂ L₃) strict pref (Lottery.mix α hα₀ hα₁ L₁ L₄) (Lottery.mix α hα₀ hα₁ L₂ L₄)

      The Sure-Thing Principle [MSZ Ex 2.12]: The common lottery in a mixture does not affect strict preference. If Independence holds, then [α L₁, (1-α) L₃] ≻ [α L₂, (1-α) L₃] iff [α L₁, (1-α) L₄] ≻ [α L₂, (1-α) L₄] for any lotteries L₁, L₂, L₃, L₄ and α ∈ [0,1].

      Exercise 2.5: Independence of the vNM Axioms [MSZ Ex 2.5] #

      For each axiom, we construct a preference relation on Lottery (Fin 3) that violates that axiom while satisfying the other three.

      Counterexample 1: ¬Completeness #

      Use the trivial preference L₁L₂L₁ = L₂. Only identical lotteries are comparable, so completeness fails. The other three axioms hold trivially or by injectivity of mixing.

      Counterexample 2: ¬Continuity #

      Lexicographic preference on probability vectors: compare L(0) first, then L(1). This is a total order satisfying independence, but no mixture of pure outcomes A₀ and A₂ is indifferent to pure A₁.

      Counterexample 3: ¬Transitivity #

      Define L₁L₂ iff L₁(0) ≥ L₂(0) OR L₁(1) ≥ L₂(1). This is complete (for any pair, at least one coordinate comparison holds) and satisfies independence (linear mixing preserves each coordinate comparison). But it is NOT transitive: the "or" allows preference chains that don't compose.

      Counterexample 4: ¬Independence #

      Use a threshold preference: L₁L₂ iff L₁(0) ≥ 1/2 or L₂(0) < 1/2. This partitions lotteries into "high" (L(0) ≥ 1/2) and "low" (L(0) < 1/2); high is preferred to low, and within each class everything is indifferent. Mixing can move a lottery across the threshold, violating independence. Continuity holds because θ=0 or θ=1 always gives indifference.

      Main theorem #

      theorem VNM.axioms_independent :
      (∃ (pref : (Lottery (Fin 3))(Lottery (Fin 3))Prop), ¬Completeness pref Transitivity pref Independence pref Continuity pref) (∃ (pref : (Lottery (Fin 3))(Lottery (Fin 3))Prop), ¬Transitivity pref Completeness pref Independence pref Continuity pref) (∃ (pref : (Lottery (Fin 3))(Lottery (Fin 3))Prop), ¬Independence pref Completeness pref Transitivity pref Continuity pref) ∃ (pref : (Lottery (Fin 3))(Lottery (Fin 3))Prop), ¬Continuity pref Completeness pref Transitivity pref Independence pref

      Exercise 2.5 [MSZ]: The four vNM axioms are independent. For each axiom, there exists a preference relation on lotteries that violates that axiom while satisfying the other three.