Icard (2016): Pragmatic considerations on comparative probability

Icard asks what is wrong with comparative probability judgments that no probability measure represents, and answers with a Money Pump without its diachronic step. A subject who prefers gambles on the events judged likelier, would pay for that preference, and agglomerates the preferences faces a canonical decision problem against nature, in which the acts gambling on the likelier side of every strict comparison cost c. Theorem 1 says the uniform mixture Q★ of those acts avoids strict dominance for some cost iff the judgments are representable (representable_iff_exists_not_dominated), through the Main Lemma (represents_iff_maximizes) and Pearce's lemma (neverBest_iff_strictlyDominated).

A measure represents the judgments when the order it induces agrees with them (Agree), so each of the paper's examples fails an axiom of comparative probability. The explorer's cyclic judgments fail transitivity, Ellsberg's fail de Finetti's quasi-additivity, and the World Cup judgments of Kraft, Pratt and Seidenberg, which Holliday and Icard also use, satisfy every de Finetti axiom but are balanced, a failure of Scott's cancellation. When every pair is judged, representability is the comparative-probability substrate's, and Theorem 1 with Scott's theorem makes the dominance criterion cancellation (cancellation_iff_exists_not_dominated).

Implementation notes

• Judgments are a finite family of compared pairs with a Finset of strict indices, the paper's ℰ ⊆ ℘(Ω) × ℘(Ω) with X and Y; the family may repeat a pair, and X ≠ ∅ is a hypothesis where the paper assumes it. A pure act picks a side of each pair, so the paper's Σ is ι → Bool.
• Mixed acts and beliefs are probability measures. A mixed act's payoff and its expected utility are integrals against them, the latter the appendix's 𝔼U(Q) = ∑_σ Q(σ) 𝔼U(σ), and Q★ is the uniform measure on the preferred acts.
• In the refutation direction of the Main Lemma the better mixed act is the pushforward of Q★ along a change of one coordinate rather than the appendix's mixtures Q★*.
• Raiffa's options are read through the paper's weights as probabilities that a choice becomes effective (p. 356): with the coin's weights the preferred act pays 50 − c in every state.

TODO

• The appendix's mixtures Q★* for the two cases of the Main Lemma, with the expected-utility differences it displays (p. 369).
• Note 25's variant for almost representability, without the cost.

References

• [Ica16]
• [Pea84]
• [DMcKS55]
• [Ell61]
• [Rai61]
• [KPS59]
• [Sco64]
• [HI13]

Decision problems against nature

@[simp]

theorem Icard2016.mixedPayoff_dirac {Ω : Type u_1} {A : Type u_2} [MeasurableSpace A] [MeasurableSingletonClass A] (U : A → Ω → ℝ) (a : A) (ω : Ω) : ProbabilityTheory.mixedPayoff U (MeasureTheory.Measure.dirac a) ω = U a ω

theorem Icard2016.mixedPayoff_uniformOn {Ω : Type u_1} {A : Type u_2} [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A] (U : A → Ω → ℝ) [DecidableEq A] (s : Finset A) (ω : Ω) : ProbabilityTheory.mixedPayoff U (ProbabilityTheory.uniformOn ↑s) ω = (∑ a ∈ s, U a ω) / ↑s.card

A uniform mixture pays the average of its acts' payoffs.

theorem Icard2016.expectedPayoff_eq_sum_sum {Ω : Type u_1} [Fintype Ω] [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {A : Type u_2} [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A] (U : A → Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] (μ : MeasureTheory.Measure A) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.expectedPayoff U P μ = ∑ a : A, μ.real {a} * ∑ ω : Ω, P.real {ω} * U a ω

The expected payoff of the mixed act μ is the μ-average of the pure acts' expected payoffs, 𝔼U(Q) = ∑_σ Q(σ) 𝔼U(σ) of the appendix.

theorem Icard2016.neverBest_iff_strictlyDominated {Ω : Type u_1} [Fintype Ω] [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {A : Type u_2} [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A] (U : A → Ω → ℝ) (σ : MeasureTheory.Measure A) [MeasureTheory.IsProbabilityMeasure σ] : (∀ (P : MeasureTheory.Measure Ω), MeasureTheory.IsProbabilityMeasure P → ∃ (ν : MeasureTheory.Measure A), MeasureTheory.IsProbabilityMeasure ν ∧ ProbabilityTheory.expectedPayoff U P σ < ProbabilityTheory.expectedPayoff U P ν) ↔ ProbabilityTheory.IsStrictlyPayoffDominated U σ

Pearce's lemma, the paper's Lemma 2 (p. 361), which it calls folklore in game theory and cites as [Pea84]'s Lemma 3. In a finite decision problem against nature, a mixed act is a best response to no belief iff it is strictly dominated by a mixed act.

Judgments and the canonical decision problem

structure Icard2016.Judgments (Ω : Type u_3) (ι : Type u_4) : Type (max u_3 u_4)

A subject's comparative judgments judge, for each compared pair (left i, right i) of events, left i strictly more likely when i ∈ strict and the two equally likely otherwise.

• left : ι → Set Ω

  The event on the left of comparison i.

• right : ι → Set Ω

  The event on the right of comparison i.

• strict : Finset ι

  The comparisons judged strict, the paper's X.

@[reducible, inline]

abbrev Icard2016.Act (ι : Type u_3) : Type u_3

A pure act picks, for each compared pair, the side it gambles on, true for left.

Equations

• Icard2016.Act ι = (ι → Bool)

structure Icard2016.Stakes (ι : Type u_3) : Type u_3

The stakes of the canonical decision problem are a positive weight and a pair of utilities, good above bad, for each comparison.

• weight : ι → ℝ

  The weight of comparison i.

• good : ι → ℝ

  The utility of the good outcome of comparison i.

• bad : ι → ℝ

  The utility of the bad outcome of comparison i.

• weight_pos (i : ι) : 0 < self.weight i
• bad_lt_good (i : ι) : self.bad i < self.good i

def Icard2016.Stakes.const {ι : Type u_2} (w g b : ℝ) (hw : 0 < w) (hgb : b < g) : Stakes ι

Stakes.const w g b gives every comparison the weight w and the utilities g above b.

Equations

• Icard2016.Stakes.const w g b hw hgb = { weight := fun (x : ι) => w, good := fun (x : ι) => g, bad := fun (x : ι) => b, weight_pos := ⋯, bad_lt_good := ⋯ }

def Icard2016.Judgments.side {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) (i : ι) : Bool → Set Ω

The event on side t of comparison i.

Equations

• J.side i true = J.left i
• J.side i false = J.right i

def Icard2016.Judgments.Preferred {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) (φ : Act ι) : Prop

The acts the subject prefers, the paper's Σ★, are those gambling on the left of every strict comparison.

Equations

• J.Preferred φ = ∀ i ∈ J.strict, φ i = true

@[instance_reducible]

instance Icard2016.Judgments.instDecidablePredActPreferred {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) : DecidablePred J.Preferred

Equations

• J.instDecidablePredActPreferred x✝ = Finset.decidableDforallFinset

theorem Icard2016.Judgments.preferred_const_true {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) : J.Preferred fun (x : ι) => true

theorem Icard2016.Judgments.not_preferred_const_false {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) (hX : J.strict.Nonempty) : ¬J.Preferred fun (x : ι) => false

noncomputable def Icard2016.Judgments.preutility {Ω : Type u_1} {ι : Type u_2} [Fintype ι] (J : Judgments Ω ι) (s : Stakes ι) (φ : Act ι) (ω : Ω) : ℝ

The preutility of act φ in state ω is the weighted payoff of its gambles.

Equations

• J.preutility s φ ω = ∑ i : ι, s.weight i * if ω ∈ J.side i (φ i) then s.good i else s.bad i

noncomputable def Icard2016.Judgments.utility {Ω : Type u_1} {ι : Type u_2} [Fintype ι] (J : Judgments Ω ι) (s : Stakes ι) (c : ℝ) (φ : Act ι) (ω : Ω) : ℝ

The canonical decision problem D_{w,c} charges the preferred acts the cost c.

Equations

• J.utility s c φ ω = J.preutility s φ ω - if J.Preferred φ then c else 0

def Icard2016.Judgments.preferredCard {Ω : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) : ℕ

The number of preferred acts.

Equations

• J.preferredCard = (Finset.filter J.Preferred Finset.univ).card

theorem Icard2016.Judgments.preferredCard_pos {Ω : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) : 0 < J.preferredCard

noncomputable def Icard2016.Judgments.uniformPreferred {Ω : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) : MeasureTheory.Measure (Act ι)

The uniform mixture Q★ over the preferred acts.

Equations

• J.uniformPreferred = ProbabilityTheory.uniformOn ↑(Finset.filter J.Preferred Finset.univ)

instance Icard2016.Judgments.instIsProbabilityMeasureActUniformPreferred {Ω : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) : MeasureTheory.IsProbabilityMeasure J.uniformPreferred

theorem Icard2016.Judgments.uniformPreferred_real_singleton {Ω : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) (φ : Act ι) : J.uniformPreferred.real {φ} = if J.Preferred φ then 1 / ↑J.preferredCard else 0

theorem Icard2016.Judgments.uniformPreferred_eq_dirac_of_strict_eq_univ {Ω : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) (h : J.strict = Finset.univ) : J.uniformPreferred = MeasureTheory.Measure.dirac fun (x : ι) => true

When every comparison is strict, Q★ is the single act gambling on every left side.

def Icard2016.Judgments.Agree {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) (r : Set Ω → Set Ω → Prop) : Prop

A relation r on events agrees with the judgments, the paper's word for a measure (p. 368), when it makes each strict comparison strict and each indifference hold both ways.

Equations

• J.Agree r = ∀ (i : ι), (i ∈ J.strict → ComparativeProbability.Strict r (J.left i) (J.right i)) ∧ (i ∉ J.strict → r (J.left i) (J.right i) ∧ r (J.right i) (J.left i))

def Icard2016.Judgments.Represents {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) : Prop

P represents the judgments (p. 359), P(E) > P(F) on strict comparisons and P(E) = P(F) on indifferences, when the order it induces agrees with them.

Equations

• J.Represents P = J.Agree P.inducedGe

def Icard2016.Judgments.Representable {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) [MeasurableSpace Ω] : Prop

The judgments are probabilistically representable.

Equations

• J.Representable = ∃ (P : MeasureTheory.Measure Ω), MeasureTheory.IsProbabilityMeasure P ∧ J.Represents P

theorem Icard2016.Judgments.Agree.representable {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {J : Judgments Ω ι} {r : Set Ω → Set Ω → Prop} (h : J.Agree r) (hr : ComparativeProbability.Representable r) : J.Representable

Judgments that agree with a representable relation are representable.

The Main Lemma

noncomputable def Icard2016.Judgments.sideValue {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) [MeasurableSpace Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) (i : ι) (t : Bool) : ℝ

The P-expected payoff of the unit gamble on side t of comparison i, the paper's b_{E_i} and b_{F_i}.

Equations

• J.sideValue s P i t = P.real (J.side i t) * s.good i + (1 - P.real (J.side i t)) * s.bad i

theorem Icard2016.Judgments.sideValue_true_sub_false {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) [MeasurableSpace Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) (i : ι) : J.sideValue s P i true - J.sideValue s P i false = (P.real (J.left i) - P.real (J.right i)) * (s.good i - s.bad i)

theorem Icard2016.Judgments.sum_mu_utility {Ω : Type u_1} [Fintype Ω] {ι : Type u_2} [Fintype ι] (J : Judgments Ω ι) [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (c : ℝ) (φ : Act ι) : ∑ ω : Ω, P.real {ω} * J.utility s c φ ω = ∑ i : ι, s.weight i * J.sideValue s P i (φ i) - if J.Preferred φ then c else 0

The expected utility of a pure act is its weighted side values less the cost.

theorem Icard2016.Judgments.expectedUtility_eq_sum_sideValue {Ω : Type u_1} [Fintype Ω] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (c : ℝ) (μ : MeasureTheory.Measure (Act ι)) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.expectedPayoff (J.utility s c) P μ = ∑ φ : Act ι, μ.real {φ} * (∑ i : ι, s.weight i * J.sideValue s P i (φ i) - if J.Preferred φ then c else 0)

noncomputable def Icard2016.Judgments.preferredValue {Ω : Type u_1} {ι : Type u_2} [Fintype ι] (J : Judgments Ω ι) [MeasurableSpace Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) : ℝ

The value of the preferred acts before the cost.

Equations

• J.preferredValue s P = ∑ i : ι, s.weight i * J.sideValue s P i true

theorem Icard2016.Judgments.sideValue_eq_of_represents {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) [MeasurableSpace Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) (hP : J.Represents P) {i : ι} (hi : i ∉ J.strict) (t : Bool) : J.sideValue s P i t = J.sideValue s P i true

theorem Icard2016.Judgments.sideValue_false_lt_true_of_represents {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) [MeasurableSpace Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hP : J.Represents P) {i : ι} (hi : i ∈ J.strict) : J.sideValue s P i false < J.sideValue s P i true

noncomputable def Icard2016.Judgments.margin {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) [MeasurableSpace Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) (hX : J.strict.Nonempty) : ℝ

The margin by which the preferred acts beat any deviation on a strict comparison.

Equations

• J.margin s P hX = J.strict.inf' hX fun (i : ι) => s.weight i * (J.sideValue s P i true - J.sideValue s P i false)

theorem Icard2016.Judgments.margin_pos {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) [MeasurableSpace Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hP : J.Represents P) (hX : J.strict.Nonempty) : 0 < J.margin s P hX

theorem Icard2016.Judgments.margin_le {Ω : Type u_1} {ι : Type u_2} (J : Judgments Ω ι) [MeasurableSpace Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) (hX : J.strict.Nonempty) {i : ι} (hi : i ∈ J.strict) : J.margin s P hX ≤ s.weight i * (J.sideValue s P i true - J.sideValue s P i false)

theorem Icard2016.Judgments.pureValue_of_preferred {Ω : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) [MeasurableSpace Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) (hP : J.Represents P) {φ : Act ι} (hφ : J.Preferred φ) : ∑ i : ι, s.weight i * J.sideValue s P i (φ i) = J.preferredValue s P

A preferred act is worth the preferred value under a representing measure.

theorem Icard2016.Judgments.pureValue_le_of_not_preferred {Ω : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) [MeasurableSpace Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hP : J.Represents P) (hX : J.strict.Nonempty) {φ : Act ι} (hφ : ¬J.Preferred φ) : ∑ i : ι, s.weight i * J.sideValue s P i (φ i) ≤ J.preferredValue s P - J.margin s P hX

A non-preferred act loses at least the margin under a representing measure.

theorem Icard2016.Judgments.expectedUtility_le_of_represents {Ω : Type u_1} [Fintype Ω] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hP : J.Represents P) (hX : J.strict.Nonempty) {c : ℝ} (hcm : c ≤ J.margin s P hX) (μ : MeasureTheory.Measure (Act ι)) [MeasureTheory.IsProbabilityMeasure μ] : ProbabilityTheory.expectedPayoff (J.utility s c) P μ ≤ J.preferredValue s P - c

Under a representing measure the expected utility of a mixed act is at most the preferred value less the cost, with equality on Q★.

theorem Icard2016.Judgments.expectedUtility_uniformPreferred_of_represents {Ω : Type u_1} [Fintype Ω] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hP : J.Represents P) (c : ℝ) : ProbabilityTheory.expectedPayoff (J.utility s c) P J.uniformPreferred = J.preferredValue s P - c

theorem Icard2016.Judgments.expectedUtility_map_gt {Ω : Type u_1} [Fintype Ω] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {c : ℝ} (f : Act ι → Act ι) (hle : ∀ (φ : Act ι), J.Preferred φ → ∑ ω : Ω, P.real {ω} * J.utility s c φ ω ≤ ∑ ω : Ω, P.real {ω} * J.utility s c (f φ) ω) (hlt : ∃ (φ : Act ι), J.Preferred φ ∧ ∑ ω : Ω, P.real {ω} * J.utility s c φ ω < ∑ ω : Ω, P.real {ω} * J.utility s c (f φ) ω) : ProbabilityTheory.expectedPayoff (J.utility s c) P J.uniformPreferred < ProbabilityTheory.expectedPayoff (J.utility s c) P (MeasureTheory.Measure.map f J.uniformPreferred)

The pushforward of Q★ along a change of one coordinate beats Q★ when the change never hurts a preferred act and helps one.

theorem Icard2016.Judgments.represents_iff_maximizes {Ω : Type u_1} [Fintype Ω] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (s : Stakes ι) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (hX : J.strict.Nonempty) : J.Represents P ↔ ∃ (c : ℝ), 0 < c ∧ ProbabilityTheory.MaximizesPayoff (J.utility s c) P J.uniformPreferred

Main Lemma (Lemma 1). A measure represents the judgments iff, for some cost, the uniform preferred act maximizes its expected utility in the canonical decision problem.

Theorem 1

theorem Icard2016.Judgments.representable_iff_exists_not_dominated {Ω : Type u_1} [Fintype Ω] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (s : Stakes ι) (hX : J.strict.Nonempty) : J.Representable ↔ ∃ (c : ℝ), 0 < c ∧ ¬ProbabilityTheory.IsStrictlyPayoffDominated (J.utility s c) J.uniformPreferred

Theorem 1. The judgments are probabilistically representable iff, for some cost, the uniform preferred act Q★ is not strictly dominated in the canonical decision problem.

Balanced judgments

In each of the paper's examples every state lies in as many left sides as right sides: trading the preferred gambles for the others "changes nothing whichever team wins" (p. 358). Such judgments are a failure of Scott's cancellation, so none is representable, and under constant stakes the trade is a pure act that dominates Q★.

def Icard2016.Judgments.Balanced {Ω : Type u_1} {ι : Type u_2} [Fintype ι] (J : Judgments Ω ι) : Prop

The judged pairs are balanced when every state lies in as many left sides as right sides.

Equations

• J.Balanced = ∀ (ω : Ω), ∑ i : ι, (J.left i).indicator 1 ω = ∑ i : ι, (J.right i).indicator 1 ω

theorem Icard2016.Judgments.preutility_const_false_of_balanced {Ω : Type u_1} {ι : Type u_2} [Fintype ι] (J : Judgments Ω ι) (hJ : J.Balanced) {w g b : ℝ} (hw : 0 < w) (hgb : b < g) (ω : Ω) : J.preutility (Stakes.const w g b hw hgb) (fun (x : ι) => false) ω = J.preutility (Stakes.const w g b hw hgb) (fun (x : ι) => true) ω

Under constant stakes, the act gambling on every right side pays what the act gambling on every left side pays, in every state, when the judgments are balanced.

theorem Icard2016.Judgments.dominated_of_balanced {Ω : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) [Nonempty ι] (hJ : J.Balanced) (hX : J.strict = Finset.univ) {w g b : ℝ} (hw : 0 < w) (hgb : b < g) {c : ℝ} (hc : 0 < c) : ProbabilityTheory.IsStrictlyPayoffDominated (J.utility (Stakes.const w g b hw hgb) c) J.uniformPreferred

Balanced strict judgments leave Q★ strictly dominated under any constant stakes, by the act that gambles on every right side and pays no cost.

theorem Icard2016.Judgments.not_representable_of_balanced {Ω : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (J : Judgments Ω ι) [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Finite Ω] (hJ : J.Balanced) (hX : J.strict.Nonempty) : ¬J.Representable

Balanced judgments with a strict comparison are not representable, since a representing measure would give both sides the same total mass yet make each left side at least as heavy and one strictly heavier.

One weak relation on all pairs

When every pair of events is judged, the paper notes (p. 359) that a single weak relation ≿ records the judgments, with ≻ and ∼ defined from it. Icard's representability is then the substrate's, so Theorem 1 joins Scott's characterization by cancellation.

def Icard2016.Judgments.ofRel {Ω : Type u_1} [Fintype Ω] (r : Set Ω → Set Ω → Prop) [DecidableRel r] : Judgments Ω { p : Set Ω × Set Ω // r p.1 p.2 }

ofRel r judges each pair A ≿ B of a weak relation r, strictly when B ≿ A fails and as an indifference otherwise.

Equations

• One or more equations did not get rendered due to their size.

theorem Icard2016.Judgments.ofRel_representable_iff {Ω : Type u_1} [Fintype Ω] [MeasurableSpace Ω] (r : Set Ω → Set Ω → Prop) [DecidableRel r] [Std.Total r] : (ofRel r).Representable ↔ ComparativeProbability.Representable r

With every pair judged, the judgments of a total relation are representable exactly when the relation is.

theorem Icard2016.Judgments.ofRel_strict_nonempty {Ω : Type u_1} [Fintype Ω] (r : Set Ω → Set Ω → Prop) [DecidableRel r] [ComparativeProbability.IsLikelihoodMono r] [ComparativeProbability.IsNontrivial r] : (ofRel r).strict.Nonempty

A non-trivial monotone relation judges the whole space strictly more likely than ∅.

theorem Icard2016.cancellation_iff_exists_not_dominated {Ω : Type u_1} [Fintype Ω] [MeasurableSpace Ω] [DiscreteMeasurableSpace Ω] (r : Set Ω → Set Ω → Prop) [ComparativeProbability.IsQualitativeProbability r] (s : Stakes { p : Set Ω × Set Ω // r p.1 p.2 }) : ComparativeProbability.Cancellation r ↔ ∃ (c : ℝ), 0 < c ∧ ¬ProbabilityTheory.IsStrictlyPayoffDominated ((Judgments.ofRel r).utility s c) (Judgments.ofRel r).uniformPreferred

With every pair judged by a qualitative probability, Scott's cancellation holds exactly when Q★ avoids strict dominance for some cost, by Theorem 1 joined with Scott's theorem. This makes precise the paper's remark (p. 350) that the argument justifies the axioms of the representation theorems "insofar as they are shown to be extensionally equivalent to representability". It reaches Scott's cancellation, which is equivalent to representability, and not de Finetti's axioms, which are hypotheses here and fall short of it from five states on.

The examples

noncomputable def Icard2016.unitStakes (ι : Type u_3) : Stakes ι

Unit weights and a unit good outcome, the stakes of the explorer and the World Cup.

Equations

• Icard2016.unitStakes ι = Icard2016.Stakes.const 1 1 0 Icard2016.unitStakes._proof_1 Icard2016.unitStakes._proof_1

The explorer (§1, §3, §7)

def Icard2016.explorer : Judgments (Fin 3) (Fin 3)

The explorer of §1 judges the treasure likelier on island A than B, on B than C, and on C than A.

Equations

• Icard2016.explorer = { left := ![{0}, {1}, {2}], right := ![{1}, {2}, {0}], strict := Finset.univ }

theorem Icard2016.explorer_not_agree (r : Set (Fin 3) → Set (Fin 3) → Prop) [IsTrans (Set (Fin 3)) r] : ¬explorer.Agree r

No transitive relation agrees with cyclic judgments, so "given intransitive judgments, there can be no numerical probability measure that agrees with these judgments" (p. 349).

theorem Icard2016.explorer_not_representable : ¬explorer.Representable

def Icard2016.explorerMixture : Finset (Act (Fin 3))

The acts A2, A3, A4 of the table in §7, each gambling on exactly one left side; on the islands A, B, C they pay 0, 1, 2, 1, 2, 0 and 2, 0, 1.

Equations

• Icard2016.explorerMixture = {![false, false, true], ![false, true, false], ![true, false, false]}

theorem Icard2016.explorer_mixture_payoff (c : ℝ) (ω : Fin 3) : ProbabilityTheory.mixedPayoff (explorer.utility (unitStakes (Fin 3)) c) (ProbabilityTheory.uniformOn ↑explorerMixture) ω = 1

The uniform mixture of A2, A3, A4 "guarantees payoff 1 in all states" (p. 365).

theorem Icard2016.explorer_dominated {c : ℝ} (hc : 0 < c) : ProbabilityTheory.IsStrictlyPayoffDominated (explorer.utility (unitStakes (Fin 3)) c) explorer.uniformPreferred

In §7 the explorer's preferred act A1 pays 1 − c on every island and is strictly dominated by the uniform mixture of A2, A3, A4, which pays 1.

Raiffa on Ellsberg (§3)

def Icard2016.ellsberg : Judgments (Fin 3) (Fin 2)

In the Ellsberg urn of §3 ([Ell61]), with balls red (0), black (1) and yellow (2), red is judged likelier than black, and black or yellow likelier than red or yellow.

Equations

• Icard2016.ellsberg = { left := ![{0}, {1, 2}], right := ![{1}, {0, 2}], strict := Finset.univ }

noncomputable def Icard2016.coinStakes : Stakes (Fin 2)

The coin-flip weights of Raiffa's comment ([Rai61]), with a hundred utiles at stake.

Equations

• Icard2016.coinStakes = Icard2016.Stakes.const (1 / 2) 100 0 Icard2016.coinStakes._proof_1 Icard2016.coinStakes._proof_2

theorem Icard2016.ellsberg_not_agree (r : Set (Fin 3) → Set (Fin 3) → Prop) [ComparativeProbability.IsQualitativeAdditive r] : ¬ellsberg.Agree r

The Ellsberg judgments violate de Finetti's quasi-additivity (note 7), since adding yellow to both sides of "red over black" gives "red or yellow over black or yellow", which they reverse.

theorem Icard2016.ellsberg_not_representable : ¬ellsberg.Representable

theorem Icard2016.ellsberg_balanced : ellsberg.Balanced

theorem Icard2016.ellsberg_dominated {c : ℝ} (hc : 0 < c) : ProbabilityTheory.IsStrictlyPayoffDominated (ellsberg.utility coinStakes c) ellsberg.uniformPreferred

In Raiffa's argument the subject pays to play option 1, gamble 1 on heads and gamble 4 on tails, over option 2, gambles 2 and 3, although "for both options, the objective probability of receiving the payoff of 100 is one-half" (p. 355). With the coin's weights the preferred act pays 50 − c whatever the ball and option 2 pays 50.

Kraft, Pratt and Seidenberg's World Cup (§4)

def Icard2016.worldCup : Judgments (Fin 5) (Fin 4)

The World Cup judgments of §4, with Argentina, Brazil, China, Denmark and England as the worlds 0–4. Denmark is judged likelier than Argentina or China, Argentina or England than China or Denmark, Brazil or China than Argentina or Denmark, and Argentina, China or Denmark than Brazil or England.

Equations

• Icard2016.worldCup = { left := ![{3}, {0, 4}, {1, 2}, {0, 2, 3}], right := ![{0, 2}, {2, 3}, {0, 3}, {1, 4}], strict := Finset.univ }

theorem Icard2016.worldCup_balanced : worldCup.Balanced

theorem Icard2016.worldCup_not_representable : ¬worldCup.Representable

The World Cup judgments are not representable, since they are balanced, a failure of cancellation.

theorem Icard2016.worldCup_dominated {c : ℝ} (hc : 0 < c) : ProbabilityTheory.IsStrictlyPayoffDominated (worldCup.utility (unitStakes (Fin 4)) c) worldCup.uniformPreferred

In §4's system of bets, trading the four preferred gambles G1, G3, G5, G7 for the four others changes nothing whichever team wins, so paying for the trade is strict dominance. (The paper's G2 reads "Argentina or Chile", a slip for China.)

def Icard2016.worldCupToKps : Fin 5 ≃ Fin 5

The World Cup teams as Kraft, Pratt and Seidenberg's atoms p, q, r, s, t (0–4), with Argentina q, Brazil r, China s, Denmark p and England t.

Equations

• Icard2016.worldCupToKps = { toFun := ![1, 2, 3, 0, 4], invFun := ![3, 0, 1, 2, 4], left_inv := Icard2016.worldCupToKps._proof_1, right_inv := Icard2016.worldCupToKps._proof_2 }

theorem Icard2016.worldCup_agree_qualitativeProbability : ∃ (r : Set (Fin 5) → Set (Fin 5) → Prop), ComparativeProbability.IsQualitativeProbability r ∧ worldCup.Agree r ∧ ¬ComparativeProbability.Representable r

Note 12. The World Cup judgments agree with a qualitative probability, the Kraft–Pratt–Seidenberg order relabelled, which satisfies quasi-additivity and every other de Finetti axiom; yet neither they nor that order is representable.