Ordered differences

Scott's reduction of the one-utility problem to Theorem 3.1 is entirely algebraic. The key point is that reversal lets the two utilities be combined.

def Scott1964.MeasurementStructures.RealizableDifference {A : Type u} (D : A → A → A → A → Prop) : Prop

Representation of comparisons of utility differences.

Equations

• Scott1964.MeasurementStructures.RealizableDifference D = ∃ (f : A → ℝ), ∀ (x y z w : A), D x y z w ↔ f x - f y ≥ f z - f w

def Scott1964.MeasurementStructures.DiffTotal {A : Type u} (D : A → A → A → A → Prop) : Prop

Scott 1964, condition (1_D).

Equations

• Scott1964.MeasurementStructures.DiffTotal D = ∀ (x y z w : A), D x y z w ∨ D z w x y

def Scott1964.MeasurementStructures.DiffPermutation {A : Type u} (D : A → A → A → A → Prop) : Prop

Scott 1964, condition (2_D).

Equations

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

def Scott1964.MeasurementStructures.DiffReversal {A : Type u} (D : A → A → A → A → Prop) : Prop

Scott 1964, condition (3_D).

Equations

• Scott1964.MeasurementStructures.DiffReversal D = ∀ (x y z w : A), D x y z w → D w z y x

theorem Scott1964.MeasurementStructures.RealizableDifference.utilityPair {A : Type u} {D : A → A → A → A → Prop} (hD : RealizableDifference D) : RealizableUtilityPair D

theorem Scott1964.MeasurementStructures.RealizableDifference.reversal {A : Type u} {D : A → A → A → A → Prop} (hD : RealizableDifference D) : DiffReversal D

theorem Scott1964.MeasurementStructures.RealizableDifference.necessary {A : Type u} {D : A → A → A → A → Prop} (hD : RealizableDifference D) : DiffTotal D ∧ DiffPermutation D ∧ DiffReversal D

theorem Scott1964.MeasurementStructures.difference_of_pair_and_reversal {A : Type u} {D : A → A → A → A → Prop} (hp : RealizableUtilityPair D) (hr : DiffReversal D) : RealizableDifference D

The combining-utilities argument in the proof of Theorem 3.2.

theorem Scott1964.MeasurementStructures.realizableDifference_iff_pair_reversal {A : Type u} (D : A → A → A → A → Prop) : RealizableDifference D ↔ RealizableUtilityPair D ∧ DiffReversal D

The exact logical reduction used for Theorem 3.2.

theorem Scott1964.MeasurementStructures.difference_sufficient_of_pair_sufficient {A : Type u} (pairSufficient : ∀ (V : A → A → A → A → Prop), PairTotal V ∧ PairPermutation V → RealizableUtilityPair V) {D : A → A → A → A → Prop} (hD : DiffTotal D ∧ DiffPermutation D ∧ DiffReversal D) : RealizableDifference D

Once Theorem 3.1 is available, its sufficiency immediately yields Scott's Theorem 3.2 through the preceding combining lemma.

theorem Scott1964.MeasurementStructures.theorem_3_2 {A : Type u} [Finite A] (D : A → A → A → A → Prop) : RealizableDifference D ↔ DiffTotal D ∧ DiffPermutation D ∧ DiffReversal D

Scott 1964, Theorem 3.2 (ordered differences). The result also holds when the alternative type is empty.