van Rooij (2011): Measurement and Interadjective Comparisons

A measure is unique up to a group of transformations, and a statement about measures is meaningful when every such transformation preserves its truth. Van Rooij measures individual–adjective pairs on one scale, so that x is P-er than y is Q compares two values of a single measure, and asks which transformations that measure is unique up to when one transformation applies to every adjective: comparing pairs needs only a co-ordinal scale, a differential across adjectives a co-interval scale, and a factor across adjectives a co-ratio scale. If each adjective's scale is unique up to its own transformations, no comparison across adjectives is meaningful. Bale's universal degrees normalize each adjective's ranking, and so make even ratios across adjectives meaningful from merely ordinal measures, which van Rooij counts against them.

Main statements

• comparative_ordinalLevel, not_comparative_ordinal: x is P-er than y is Q survives one strictly increasing map applied to every adjective, but not a separate map per adjective.
• differential_cardinalFull, factor_ratioFull, not_factor_cardinalFull: a differential across adjectives holds up to a common change of unit and origin, a factor across adjectives up to a common change of unit, and not up to a change of origin.
• factor_universal_ordinal: read through universal degrees, a factor across adjectives survives a separate strictly increasing map per adjective.
• differenceComparative_cardinalUnit: comparing differences on two adjectives survives a common unit with a separate origin per adjective, the weaker co-interval scale of the paper's note 17.

Implementation notes

• A measure on individual–adjective pairs is a profile of SocialChoice with adjectives as its individuals, following the paper's analogy with interpersonal comparisons of utility. The co-ordinal, co-interval and co-ratio scales are Sen's comparability classes ordinalLevel, cardinalFull and ratioFull, and separate scales per adjective are ordinal.
• Measures are real-valued, as in the paper; universal degrees are rational.

TODO

• Section 2's choice structures, after van Benthem, and section 4.3's constructions of a co-ordinal scale from a choice function on pairs and from Klein's modifiers.

References

• [vR11b]
• [Bal08]
• [Sas10]
• [Sen70]

def VanRooij2011.pairs {X : Type u_1} {Ad : Type u_2} {K : Type u_3} (v : SocialChoice.Profile Ad X K) (p : X × Ad) : K

The measure a profile assigns individual–adjective pairs.

Equations

• VanRooij2011.pairs v p = v p.1 p.2

theorem VanRooij2011.pairs_transform {X : Type u_1} {Ad : Type u_2} {K : Type u_3} (f : Ad → K → K) (v : SocialChoice.Profile Ad X K) (p : X × Ad) : pairs (SocialChoice.Profile.transform f v) p = f p.2 (pairs v p)

Comparisons across adjectives

def VanRooij2011.comparative {X : Type u_1} {Ad : Type u_2} (x : X) (P : Ad) (y : X) (Q : Ad) (v : SocialChoice.Profile Ad X ℝ) : Prop

x is P-er than y is Q holds when the pair of x and P measures more than the pair of y and Q.

Equations

• VanRooij2011.comparative x P y Q v = ((x, P) ∈ VanRooij2011.pairs v ⁻¹' Set.Ioi (VanRooij2011.pairs v (y, Q)))

def VanRooij2011.differential {X : Type u_1} {Ad : Type u_2} (x : X) (P : Ad) (y : X) (Q : Ad) (d : ℝ) (v : SocialChoice.Profile Ad X ℝ) : Prop

x is d-much P-er than y is Q.

Equations

• VanRooij2011.differential x P y Q d v = Degree.DifferentialComparative (VanRooij2011.pairs v) (x, P) (y, Q) d

def VanRooij2011.factor {X : Type u_1} {Ad : Type u_2} (x : X) (P : Ad) (y : X) (Q : Ad) (n : ℝ) (v : SocialChoice.Profile Ad X ℝ) : Prop

x is n times as P as y is Q.

Equations

• VanRooij2011.factor x P y Q n v = Degree.FactorEquative (VanRooij2011.pairs v) (x, P) (y, Q) n

def VanRooij2011.differenceComparative {X : Type u_1} {Ad : Type u_2} (x y : X) (P : Ad) (z w : X) (Q : Ad) (v : SocialChoice.Profile Ad X ℝ) : Prop

x is P-er than y by more than z is Q-er than w.

Equations

• VanRooij2011.differenceComparative x y P z w Q v = (VanRooij2011.pairs v (z, Q) - VanRooij2011.pairs v (w, Q) < VanRooij2011.pairs v (x, P) - VanRooij2011.pairs v (y, P))

theorem VanRooij2011.comparative_ordinalLevel {X : Type u_1} {Ad : Type u_2} (x y : X) (P Q : Ad) : SocialChoice.Invariant SocialChoice.ordinalLevel (comparative x P y Q)

Comparing across adjectives needs only a co-ordinal scale.

theorem VanRooij2011.not_comparative_ordinal {X : Type u_1} {Ad : Type u_2} (x y : X) (P Q : Ad) [DecidableEq Ad] (hPQ : P ≠ Q) : ¬SocialChoice.Invariant SocialChoice.ordinal (comparative x P y Q)

With a separate strictly increasing map for each adjective, comparing across two adjectives is not meaningful.

theorem VanRooij2011.differential_cardinalFull {X : Type u_1} {Ad : Type u_2} (x y : X) (P Q : Ad) {f : Ad → ℝ → ℝ} {a b : ℝ} (ha : 0 < a) (hf : ∀ (i : Ad) (t : ℝ), f i t = a * t + b) (d : ℝ) (v : SocialChoice.Profile Ad X ℝ) : differential x P y Q (a * d) (SocialChoice.Profile.transform f v) ↔ differential x P y Q d v

A differential across adjectives holds up to a common change of unit and origin, once its amount is rescaled by the unit.

theorem VanRooij2011.factor_ratioFull {X : Type u_1} {Ad : Type u_2} (x y : X) (P Q : Ad) (n : ℝ) : SocialChoice.Invariant SocialChoice.ratioFull (factor x P y Q n)

A factor across adjectives holds up to a common change of unit.

theorem VanRooij2011.not_factor_cardinalFull {X : Type u_1} {Ad : Type u_2} (x y : X) (P Q : Ad) [DecidableEq X] [DecidableEq Ad] (hne : (x, P) ≠ (y, Q)) : ¬SocialChoice.Invariant SocialChoice.cardinalFull (factor x P y Q 2)

A factor across adjectives does not survive a common change of origin.

theorem VanRooij2011.differenceComparative_cardinalUnit {X : Type u_1} {Ad : Type u_2} (x y z w : X) (P Q : Ad) : SocialChoice.Invariant SocialChoice.cardinalUnit (differenceComparative x y P z w Q)

Comparing differences on two adjectives survives a common unit with a separate origin per adjective, since each origin cancels within its own difference; the paper defines this scale in note 17 without drawing the consequence.

Bale's universal degrees

noncomputable def VanRooij2011.universal {X : Type u_1} {Ad : Type u_2} (v : SocialChoice.Profile Ad X ℝ) (C : Finset X) : SocialChoice.Profile Ad X ℚ

Bale's universal degrees of a profile on the comparison class C, adjective by adjective.

Equations

• VanRooij2011.universal v C x P = Degree.universalDegree (fun (x : X) => v x P) C x

theorem VanRooij2011.universal_transform {X : Type u_1} {Ad : Type u_2} {f : Ad → ℝ → ℝ} (hf : f ∈ SocialChoice.ordinal) (v : SocialChoice.Profile Ad X ℝ) (C : Finset X) : universal (SocialChoice.Profile.transform f v) C = universal v C

Universal degrees forget any strictly increasing map applied to an adjective's measure.

theorem VanRooij2011.factor_universal_ordinal {X : Type u_1} {Ad : Type u_2} (C : Finset X) (x y : X) (P Q : Ad) (n : ℚ) : SocialChoice.Invariant SocialChoice.ordinal fun (v : SocialChoice.Profile Ad X ℝ) => Degree.FactorEquative (pairs (universal v C)) (x, P) (y, Q) n

Read through universal degrees, x is n times as P as y is Q survives a separate strictly increasing map per adjective, so a ratio across adjectives becomes meaningful although each adjective's measure is only ordinal.

theorem VanRooij2011.universal_not_affine : ¬∃ (a : ℚ) (b : ℚ), ∀ (i : Fin (Nat.succ 0).succ.succ), Degree.universalDegree ![1, 2, 4] Finset.univ i = a * ![1, 2, 4] i + b

Universal degrees are not in general an affine function of a measure on a ratio scale, since heights of one, two and four give universal degrees of one third, two thirds and one.

Negative adjectives and multidimensional adjectives

theorem VanRooij2011.shorter_iff_taller {E : Type u_4} (height : E → ℝ) (m : ℝ) (x y : E) (d : ℝ) : Degree.DifferentialComparative (fun (z : E) => m - height z) y x d ↔ Degree.DifferentialComparative height x y d

Measuring shortness as a fixed number minus height, after Sassoon, y is d shorter than x holds exactly when x is d taller than y, whatever the number.

theorem VanRooij2011.three_times_as_short_not_meaningful : Degree.FactorEquative ![-6, -2] 0 1 3 ∧ ¬Degree.FactorEquative (fun (i : Fin (Nat.succ 0).succ) => ![-6, -2] i + 1) 0 1 3

Ratios of shortness are not meaningful, since shortnesses of six and two make one three times as short, and moving the origin by one makes the ratio five.

theorem VanRooij2011.not_utilitarian_ordinalLevel : ¬SocialChoice.Invariant SocialChoice.ordinalLevel (SocialChoice.utilitarian ![1, 1])

Aggregating the dimensions of a multidimensional adjective by a weighted sum is not meaningful on a co-ordinal scale, unlike aggregating by the minimum (SocialChoice.maximin_ordinalLevelInvariant).