Solt (2018): Multidimensionality, subjectivity and scales

This file formalizes [Sol18a]'s account of ordering subjectivity, the faultless disagreement some gradable adjectives allow about their comparatives: which of two dishes is tastier, but not which of two people is taller. A gradable adjective lexicalizes a family of measure functions indexed by contexts (35). Its comparative is subjective for a pair when two contexts order the pair oppositely (OrderingSubjective), which is incomparability with the contexts read as dimensions (orderingSubjective_iff_incompRel), and settled when every context orders it alike (Settled). Objectivity is a single measure that every context agrees with (Externalizable). Additive measures that never reverse a pair differ only in unit (eq_smul_of_forall_lt_imp_le, the uniqueness half of Hölder's theorem), so an additive family (36) is externalizable exactly when it has no ordering subjectivity (externalizable_iff_forall_not_orderingSubjective), and so is a homogeneous function of such measures (38) (externalizable_derived), such as fullness (39) (fullness_eq).

For a multidimensional adjective such as dirty (41) the context weights the kinds of dirt, and the verdict that all weightings share is the Pareto rule (forall_dirty_le_iff). A pair is settled when one object carries at least as much of every kind of dirt per unit of size and more of some (settled_dirty_iff), and subjective when neither dominates the other (orderingSubjective_dirty_iff), so the class is mixed. A judge-dependent adjective (42) has unconstrained measures, so every pair of distinct individuals is subjective (orderingSubjective_of_surjective) and none is settled (not_settled_of_surjective). These are the three classes of Table 1, matching the experiment of section 2: speakers judged disagreements about the comparatives of measurable adjectives factual, those about evaluative adjectives matters of opinion, and the rest mixed.

Implementation notes

• OrderingSubjective asks for a strict reversal, the disagreement of the dialogues (2) and (5)–(7); section 5.3's "difference in the relative ordering" is broader, but the two coincide on the families formalized.
• Concatenation (36) is the addition of an AddCommMonoid. Additivity alone does not exclude ordering subjectivity, since a positive weighting of additive measures is additive; that the measures of height differ only in unit is what section 5.1 suggests ("this might be the only sort of variation that is possible"). Likewise (38) needs f homogeneous.
• In (41) a context is a weighting positive on every kind of dirt, the kinds and amounts being fixed; the units of amount and size only rescale the score. With unbounded weights a pair is settled exactly when it is Pareto-ordered, where "contexts can only vary so much" (section 5.4) suggests bounded ones.
• "Not constrained in any formal way" (section 5.4) is Function.Surjective, a strong idealization.

TODO

• The five stimulus categories of section 2.2, their rates of 'fact' judgments in Figure 1 (98, 94, 67, 55 and 4 %) and the appendix dialogues are not encoded as example rows; the rates of single adjectives are drawn only in a bar chart.
• The rows of Table 1 for ambiguous adjectives (bumpy, salty) are not formalized. Read as one family over both readings' contexts, such an adjective would settle no pair.
• Section 5.5's intelligent, multidimensional yet purely subjective, and the externally anchored measures of time and temperature are not formalized.

References

• [Sol18a]

Ordering subjectivity

def Solt2018a.OrderingSubjective {C : Type u_1} {E : Type u_2} {K : Type u_3} [Preorder K] (μ : C → E → K) (a b : E) : Prop

Ordering subjectivity (section 5.3) holds of a and b when two contexts order them oppositely, as in the faultless disagreements (2a–b).

Equations

• Solt2018a.OrderingSubjective μ a b = ∃ (c : C) (c' : C), μ c b < μ c a ∧ μ c' a < μ c' b

def Solt2018a.Settled {C : Type u_1} {E : Type u_2} {K : Type u_3} [Preorder K] (μ : C → E → K) (a b : E) : Prop

The comparative a is Adj-er than b is settled when every context ranks a above b, so that a disagreement about it is factual, as in (2c).

Equations

• Solt2018a.Settled μ a b = ∀ (c : C), μ c b < μ c a

def Solt2018a.Externalizable {C : Type u_1} {E : Type u_2} {K : Type u_3} [Preorder K] (μ : C → E → K) : Prop

A family is externalizable when one measure ν orders every pair as every context does, the principled order-preserving mapping to the numbers of section 5.2.

Equations

• Solt2018a.Externalizable μ = ∃ (ν : E → K), ∀ (c : C) (a b : E), μ c b < μ c a ↔ ν b < ν a

theorem Solt2018a.OrderingSubjective.symm {C : Type u_1} {E : Type u_2} {K : Type u_3} [Preorder K] {μ : C → E → K} {a b : E} (h : OrderingSubjective μ a b) : OrderingSubjective μ b a

theorem Solt2018a.orderingSubjective_comm {C : Type u_1} {E : Type u_2} {K : Type u_3} [Preorder K] {μ : C → E → K} {a b : E} : OrderingSubjective μ a b ↔ OrderingSubjective μ b a

theorem Solt2018a.Settled.not_orderingSubjective {C : Type u_1} {E : Type u_2} {K : Type u_3} [Preorder K] {μ : C → E → K} {a b : E} (h : Settled μ a b) : ¬OrderingSubjective μ a b

theorem Solt2018a.Externalizable.not_orderingSubjective {C : Type u_1} {E : Type u_2} {K : Type u_3} [Preorder K] {μ : C → E → K} {a b : E} (h : Externalizable μ) : ¬OrderingSubjective μ a b

theorem Solt2018a.Externalizable.settled_iff {C : Type u_1} {E : Type u_2} {K : Type u_3} [Preorder K] {μ : C → E → K} {a b : E} (h : Externalizable μ) (c : C) : Settled μ a b ↔ μ c b < μ c a

In an externalizable family a comparative true in one context is true in all.

theorem Solt2018a.orderingSubjective_iff_incompRel {C : Type u_1} {E : Type u_2} {K : Type u_3} [LinearOrder K] {μ : C → E → K} {a b : E} : OrderingSubjective μ a b ↔ IncompRel (fun (x1 x2 : C → K) => x1 ≤ x2) (fun (c : C) => μ c a) fun (c : C) => μ c b

Ordering subjectivity is incomparability of the two individuals' measures across contexts, a trade-off with the contexts as dimensions.

theorem Solt2018a.Externalizable.of_forall_eq_smul {C : Type u_1} {E : Type u_2} {K : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {μ : C → E → K} (h : ∀ (c c' : C), ∃ (k : K), 0 < k ∧ μ c' = k • μ c) : Externalizable μ

A family whose contexts differ by positive factors is externalizable.

Additive measures

theorem Solt2018a.eq_smul_of_forall_lt_imp_le {E : Type u_2} {K : Type u_3} [AddCommMonoid E] [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {μ μ' : E →+ K} {u : E} (hu : 0 < μ u) (h : ∀ (a b : E), μ b < μ a → μ' b ≤ μ' a) : ⇑μ' = (μ' u / μ u) • ⇑μ

Additive measures (36) that never order a pair oppositely differ only in unit, each being the other rescaled by their ratio at a standard element u. This is the uniqueness half of Hölder's theorem.

theorem Solt2018a.forall_not_orderingSubjective_iff {C : Type u_1} {E : Type u_2} {K : Type u_3} [AddCommMonoid E] [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {μ : C → E →+ K} {u : E} (hu : ∀ (c : C), 0 < (μ c) u) : (∀ (a b : E), ¬OrderingSubjective (fun (c : C) => ⇑(μ c)) a b) ↔ ∀ (c c' : C), ⇑(μ c') = ((μ c') u / (μ c) u) • ⇑(μ c)

An additive family (36) has no ordering subjectivity exactly when its measures differ in unit alone, as height in inches and height in centimeters do (section 5.1).

theorem Solt2018a.externalizable_iff_forall_not_orderingSubjective {C : Type u_1} {E : Type u_2} {K : Type u_3} [AddCommMonoid E] [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {μ : C → E →+ K} {u : E} (hu : ∀ (c : C), 0 < (μ c) u) : (Externalizable fun (c : C) => ⇑(μ c)) ↔ ∀ (a b : E), ¬OrderingSubjective (fun (c : C) => ⇑(μ c)) a b

An additive family (36) with a positive standard is externalizable exactly when it has no ordering subjectivity (section 5.2).

Derived measures

def Solt2018a.fullness {E : Type u_2} {K : Type u_3} [Field K] {X : Type u_4} (vol : E → K) (content capacity : X → E) (x : X) : K

Fullness (39) is the volume of a container's contents over the volume it can hold.

Equations

• Solt2018a.fullness vol content capacity x = vol (content x) / vol (capacity x)

theorem Solt2018a.fullness_smul {E : Type u_2} {K : Type u_3} [Field K] {X : Type u_4} {content capacity : X → E} {k : K} (hk : k ≠ 0) (vol : E → K) : fullness (k • vol) content capacity = fullness vol content capacity

The unit of volume cancels in fullness.

theorem Solt2018a.externalizable_derived {C : Type u_1} {E : Type u_2} {K : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {ι : Type u_5} {m : C → ι → E → K} {f : (ι → K) → K} (hf : ∀ (k : ι → K), (∀ (i : ι), 0 < k i) → ∃ (φ : K), 0 < φ ∧ ∀ (y : ι → K), f (k * y) = φ * f y) (hm : ∀ (c c' : C), ∃ (k : ι → K), (∀ (i : ι), 0 < k i) ∧ ∀ (i : ι) (x : E), m c' i x = k i * m c i x) : Externalizable fun (c : C) (x : E) => f fun (i : ι) => m c i x

A context-independent derived family (38), a fixed function f of component measures, is externalizable when the components differ across contexts only in unit and rescaling the components rescales f by a positive factor.

theorem Solt2018a.fullness_eq {C : Type u_1} {E : Type u_2} {K : Type u_3} [Field K] {X : Type u_4} {content capacity : X → E} [LinearOrder K] [IsStrictOrderedRing K] [AddCommMonoid E] [Archimedean K] {μ : C → E →+ K} {u : E} (hu : ∀ (c : C), 0 < (μ c) u) (h : ∀ (a b : E), ¬OrderingSubjective (fun (c : C) => ⇑(μ c)) a b) (c c' : C) : fullness (⇑(μ c')) content capacity = fullness (⇑(μ c)) content capacity

Full inherits the objectivity of volume, since an additive family of volume measures without ordering subjectivity determines one fullness measure for every context.

Multidimensional measures

def Solt2018a.dirty {E : Type u_2} {K : Type u_3} {ι : Type u_4} [Fintype ι] [Field K] [LinearOrder K] (amount : SocialChoice.Profile ι E K) (size : E → K) (k : { k : ι → K // ∀ (i : ι), 0 < k i }) (x : E) : K

Dirty (41) is the weighted sum of the amounts of the kinds of dirt on an object over its size, the context being a weighting positive on every kind.

Equations

• Solt2018a.dirty amount size k x = ↑k ⬝ᵥ amount x / size x

theorem Solt2018a.dirty_eq {E : Type u_2} {K : Type u_3} {ι : Type u_4} [Fintype ι] [Field K] [LinearOrder K] {amount : SocialChoice.Profile ι E K} {size : E → K} (k : { k : ι → K // ∀ (i : ι), 0 < k i }) (x : E) : dirty amount size k x = ↑k ⬝ᵥ (size x)⁻¹ • amount x

theorem Solt2018a.forall_dirty_le_iff {E : Type u_2} {K : Type u_3} {ι : Type u_4} [Fintype ι] [Field K] [LinearOrder K] {amount : SocialChoice.Profile ι E K} {size : E → K} {a b : E} [IsStrictOrderedRing K] : (∀ (k : { k : ι → K // ∀ (i : ι), 0 < k i }), dirty amount size k a ≤ dirty amount size k b) ↔ (size a)⁻¹ • amount a ≤ (size b)⁻¹ • amount b

Every weighting ranks a at most as dirty as b exactly when b carries at least as much of every kind of dirt per unit of size, so the Pareto rule is the verdict all weightings share.

theorem Solt2018a.orderingSubjective_dirty_iff {E : Type u_2} {K : Type u_3} {ι : Type u_4} [Fintype ι] [Field K] [LinearOrder K] {amount : SocialChoice.Profile ι E K} {size : E → K} {a b : E} [IsStrictOrderedRing K] : OrderingSubjective (dirty amount size) a b ↔ IncompRel (fun (x1 x2 : ι → K) => x1 ≤ x2) ((size a)⁻¹ • amount a) ((size b)⁻¹ • amount b)

Two weightings rank a and b oppositely exactly when neither carries at least as much of every kind of dirt per unit of size, as with the shirt clean but for a grass stain and the dingy one of section 3.

theorem Solt2018a.settled_dirty_iff {E : Type u_2} {K : Type u_3} {ι : Type u_4} [Fintype ι] [Field K] [LinearOrder K] {amount : SocialChoice.Profile ι E K} {size : E → K} {a b : E} [IsStrictOrderedRing K] : Settled (dirty amount size) a b ↔ (size b)⁻¹ • amount b < (size a)⁻¹ • amount a

Every weighting ranks a dirtier than b exactly when a carries at least as much of every kind of dirt per unit of size, and more of some.

Judge-dependent measures

theorem Solt2018a.orderingSubjective_of_surjective {E : Type u_2} {K : Type u_3} {J : Type u_4} [LinearOrder K] {μ : J → E → K} {a b : E} [Nontrivial K] (hμ : Function.Surjective μ) (hab : a ≠ b) : OrderingSubjective μ a b

A judge-dependent adjective (42) has a measure per judge, and when the judges' tastes are unconstrained any two individuals can be ranked either way.

theorem Solt2018a.not_settled_of_surjective {E : Type u_2} {K : Type u_3} {J : Type u_4} [LinearOrder K] {μ : J → E → K} {a b : E} [Nonempty K] (hμ : Function.Surjective μ) : ¬Settled μ a b

No comparative of a judge-dependent adjective is settled, since some judge ranks every pair alike.