D'Ambrosio and Hedden, multidimensional adjectives (2024)

An adjective is multidimensional when whether it applies to an object, and whether it applies to one object more than to another, depend on how the objects stand on several underlying dimensions. The paper gives such adjectives a semantics with explicit aggregation: a context supplies a profile of dimensional orderings, represented by value functions, a set of admissible aggregation rules from profiles to an overall ordering, and a standard object. x is at least as F as y holds relative to an admissible rule when it ranks x weakly above y, x is F when it ranks x weakly above the standard, and a sentence is determinately true when it is true relative to every admissible rule. The comparative is vague when more than one rule is admissible, and its vagueness is independent of the completeness and transitivity of the orderings the rules output, which the delineation approach conflates by turning disagreement between precisifications into incomparability. Transposed to social choice, Arrow's theorem makes an adjective governed by all of Arrow's conditions incoherent; giving up weak-ordering outputs admits majority rule or the Pareto rule, and giving up ordinal non-comparability admits utilitarian and Cobb–Douglas aggregation, whose free weights make the comparative vague. Sassoon's quantificational comparatives are the Pareto rule for conjunctive adjectives, a rule violating strong Pareto for disjunctive ones, and a rule violating weak Pareto for dimension-counting ones.

The framework is stated over the social welfare functionals of SocialChoice, with the dimensions as its individuals and the objects as its alternatives. This file states the sorites on Suzy's cardiovascular health under utilitarian weightings and the three verdicts on Sassoon's comparatives.

Implementation notes

• The precisifications of the delineation comparative are the admissible rules with the standard fixed, so that comparative is Kamp1975.kampPreorder.
• Weighting the dimensions of healthy, as the paper's sorites does, is utilitarian aggregation; the cut-off on Suzy's cardiovascular health is where her weighted sum reaches Bill's.

References

• J. D'Ambrosio and B. Hedden, Multidimensional adjectives (2024)
• K. J. Arrow, A difficulty in the concept of social welfare (1951)
• H. Kamp, Two theories about adjectives (1975)
• G. W. Sassoon, A typology of multidimensional adjectives (2013)

Contexts and determinacy

structure DAmbrosioHedden2024.Context (ι : Type u_4) (O : Type u_5) (K : Type u_6) : Type (max (max u_4 u_5) u_6)

A context supplies a multidimensional adjective with its admissible aggregation rules and a standard object. Relative to an admissible rule a and a profile v, x is at least as F as y is a v x y, x is F-er than y is AsymmRel (a v) x y, x and y are equally F is AntisymmRel (a v) x y, and x is F is a v x c.standard.

• adm : Set (SocialChoice.Rule ι O K)

  The aggregation rules the context does not rule out.

• standard : O

  The object that sets the standard for the positive form.

def DAmbrosioHedden2024.Context.Determinately {ι : Type u_1} {O : Type u_2} {K : Type u_3} (c : Context ι O K) (P : SocialChoice.Rule ι O K → Prop) : Prop

A statement is determinately true when it is true relative to every admissible rule.

Equations

• c.Determinately P = ∀ a ∈ c.adm, P a

def DAmbrosioHedden2024.Context.DeterminatelyNot {ι : Type u_1} {O : Type u_2} {K : Type u_3} (c : Context ι O K) (P : SocialChoice.Rule ι O K → Prop) : Prop

A statement is determinately false when it is false relative to every admissible rule.

Equations

• c.DeterminatelyNot P = ∀ a ∈ c.adm, ¬P a

def DAmbrosioHedden2024.Context.Indeterminate {ι : Type u_1} {O : Type u_2} {K : Type u_3} (c : Context ι O K) (P : SocialChoice.Rule ι O K → Prop) : Prop

Neither determinately true nor determinately false.

Equations

• c.Indeterminate P = (¬c.Determinately P ∧ ¬c.DeterminatelyNot P)

def DAmbrosioHedden2024.Context.Incoherent {ι : Type u_1} {O : Type u_2} {K : Type u_3} (c : Context ι O K) : Prop

An adjective is incoherent when no rule is admissible.

Equations

• c.Incoherent = (c.adm = ∅)

def DAmbrosioHedden2024.Context.Sharp {ι : Type u_1} {O : Type u_2} {K : Type u_3} (c : Context ι O K) : Prop

The comparative is sharp when exactly one rule is admissible.

Equations

• c.Sharp = ∃ (a : SocialChoice.Rule ι O K), c.adm = {a}

def DAmbrosioHedden2024.Context.Vague {ι : Type u_1} {O : Type u_2} {K : Type u_3} (c : Context ι O K) : Prop

The comparative is vague when more than one rule is admissible.

Equations

• c.Vague = c.adm.Nontrivial

theorem DAmbrosioHedden2024.Context.incoherent_or_sharp_or_vague {ι : Type u_1} {O : Type u_2} {K : Type u_3} {c : Context ι O K} : c.Incoherent ∨ c.Sharp ∨ c.Vague

The three cases of §4.

theorem DAmbrosioHedden2024.Context.Sharp.determinately_or {ι : Type u_1} {O : Type u_2} {K : Type u_3} {c : Context ι O K} (h : c.Sharp) (P : SocialChoice.Rule ι O K → Prop) : c.Determinately P ∨ c.DeterminatelyNot P

A sharp comparative settles every question.

theorem DAmbrosioHedden2024.Context.indeterminate_of_disagree {ι : Type u_1} {O : Type u_2} {K : Type u_3} {c : Context ι O K} {P : SocialChoice.Rule ι O K → Prop} {a b : SocialChoice.Rule ι O K} (ha : a ∈ c.adm) (hb : b ∈ c.adm) (hPa : P a) (hPb : ¬P b) : c.Indeterminate P

Two admissible rules that disagree on P make P indeterminate.

theorem DAmbrosioHedden2024.Context.Indeterminate.vague {ι : Type u_1} {O : Type u_2} {K : Type u_3} {c : Context ι O K} {P : SocialChoice.Rule ι O K → Prop} (h : c.Indeterminate P) : c.Vague

Indeterminacy needs two admissible rules, so it is comparative vagueness, whether it shows in the comparative or in the positive form.

theorem DAmbrosioHedden2024.Context.determinately_or_of_complete {ι : Type u_1} {O : Type u_2} {K : Type u_3} {c : Context ι O K} (h : c.Determinately SocialChoice.Complete) (v : SocialChoice.Profile ι O K) (x y : O) : c.Determinately fun (a : SocialChoice.Rule ι O K) => a v x y ∨ a v y x

With complete admissible rules, that one of two objects is at least as F as the other is determinate, however indeterminate it is which.

The delineation comparative

@[reducible, inline]

abbrev DAmbrosioHedden2024.Context.delineation {ι : Type u_1} {O : Type u_2} {K : Type u_3} (c : Context ι O K) (v : SocialChoice.Profile ι O K) : Preorder O

The delineation comparative of §2, with the admissible rules as precisifications and the standard fixed, makes x at least as F as y iff every admissible rule that makes y F makes x F.

Equations

• c.delineation v = Kamp1975.kampPreorder (fun (a : SocialChoice.Rule ι O K) (x : O) => a v x c.standard) c.adm

theorem DAmbrosioHedden2024.Context.delineation_incomparable {ι : Type u_1} {O : Type u_2} {K : Type u_3} (c : Context ι O K) {v : SocialChoice.Profile ι O K} {x y : O} {a b : SocialChoice.Rule ι O K} (ha : a ∈ c.adm) (hb : b ∈ c.adm) (hax : a v x c.standard) (hay : ¬a v y c.standard) (hby : b v y c.standard) (hbx : ¬b v x c.standard) : ¬x ≤ y ∧ ¬y ≤ x

Admissible rules that disagree on which of two objects meets the standard leave the two incomparable under the delineation comparative, so what the paper treats as vagueness the delineation approach turns into incompleteness.

The sorites on Suzy's health

inductive DAmbrosioHedden2024.Health : Type

The dimensions of healthy in the sorites of §2.

• musculoskeletal : Health
• cardiovascular : Health

@[instance_reducible]

instance DAmbrosioHedden2024.instDecidableEqHealth : DecidableEq Health

Equations

• DAmbrosioHedden2024.instDecidableEqHealth x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DAmbrosioHedden2024.instFintypeHealth : Fintype Health

Equations

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

inductive DAmbrosioHedden2024.Patient : Type

Bill and a variant of Suzy.

• suzy : Patient
• bill : Patient

@[instance_reducible]

instance DAmbrosioHedden2024.instDecidableEqPatient : DecidableEq Patient

Equations

• DAmbrosioHedden2024.instDecidableEqPatient x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DAmbrosioHedden2024.health {K : Type u_3} (mS mB cB t : K) : SocialChoice.Profile Health Patient K

In the sorites profile Suzy's musculoskeletal health mS sits below Bill's mB, and her cardiovascular health t varies against Bill's cB.

Equations

• DAmbrosioHedden2024.health mS mB cB t DAmbrosioHedden2024.Patient.suzy DAmbrosioHedden2024.Health.musculoskeletal = mS
• DAmbrosioHedden2024.health mS mB cB t DAmbrosioHedden2024.Patient.suzy DAmbrosioHedden2024.Health.cardiovascular = t
• DAmbrosioHedden2024.health mS mB cB t DAmbrosioHedden2024.Patient.bill DAmbrosioHedden2024.Health.musculoskeletal = mB
• DAmbrosioHedden2024.health mS mB cB t DAmbrosioHedden2024.Patient.bill DAmbrosioHedden2024.Health.cardiovascular = cB

theorem DAmbrosioHedden2024.health_utilitarian_iff {K : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {w : Health → K} {mS mB cB t : K} (hw : 0 < w Health.cardiovascular) : SocialChoice.utilitarian w (health mS mB cB t) Patient.suzy Patient.bill ↔ cB + w Health.musculoskeletal / w Health.cardiovascular * (mB - mS) ≤ t

Suzy is at least as healthy as Bill under weights w iff her cardiovascular health reaches Bill's plus the weighted musculoskeletal deficit.

theorem DAmbrosioHedden2024.health_mono {K : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {w : Health → K} {mS mB cB t t' : K} (hw : 0 ≤ w Health.cardiovascular) (h : t ≤ t') : SocialChoice.utilitarian w (health mS mB cB t) Patient.suzy Patient.bill → SocialChoice.utilitarian w (health mS mB cB t') Patient.suzy Patient.bill

The inductive premise of the sorites holds, since better cardiovascular health keeps Suzy at least as healthy as Bill.

theorem DAmbrosioHedden2024.not_health_of_lt {K : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {w : Health → K} {mS mB cB t : K} (hm : mS < mB) (ht : t < cB) (hw : ∀ (i : Health), 0 ≤ w i) (hpos : ∃ (i : Health), 0 < w i) : ¬SocialChoice.utilitarian w (health mS mB cB t) Patient.suzy Patient.bill

The first Suzy, worse than Bill on both dimensions, is not at least as healthy as Bill under any positive weighting.

theorem DAmbrosioHedden2024.health_indeterminate {K : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {w w' : Health → K} {mS mB cB t : K} (c : Context Health Patient K) (hw : SocialChoice.utilitarian w ∈ c.adm) (hw' : SocialChoice.utilitarian w' ∈ c.adm) (hc : 0 < w Health.cardiovascular) (hc' : 0 < w' Health.cardiovascular) (ht : cB + w Health.musculoskeletal / w Health.cardiovascular * (mB - mS) ≤ t) (ht' : t < cB + w' Health.musculoskeletal / w' Health.cardiovascular * (mB - mS)) : c.Indeterminate fun (a : SocialChoice.Rule Health Patient K) => a (health mS mB cB t) Patient.suzy Patient.bill

In a context admitting two weightings with different cut-offs, every Suzy between the cut-offs is a borderline case of at least as healthy as Bill.

theorem DAmbrosioHedden2024.vague_of_cutoff_lt {K : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {w w' : Health → K} {mS mB cB : K} (c : Context Health Patient K) (hw : SocialChoice.utilitarian w ∈ c.adm) (hw' : SocialChoice.utilitarian w' ∈ c.adm) (hc : 0 < w Health.cardiovascular) (hc' : 0 < w' Health.cardiovascular) (h : cB + w Health.musculoskeletal / w Health.cardiovascular * (mB - mS) < cB + w' Health.musculoskeletal / w' Health.cardiovascular * (mB - mS)) : c.Vague

Two admissible weightings with different cut-offs make at least as healthy as vague.

Vagueness against structure

theorem DAmbrosioHedden2024.vague_determinately_weakOrderValued {K : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {w w' : Health → K} {mS mB cB : K} (c : Context Health Patient K) (hadm : c.adm = {SocialChoice.utilitarian w, SocialChoice.utilitarian w'}) (hc : 0 < w Health.cardiovascular) (hc' : 0 < w' Health.cardiovascular) (h : cB + w Health.musculoskeletal / w Health.cardiovascular * (mB - mS) < cB + w' Health.musculoskeletal / w' Health.cardiovascular * (mB - mS)) : c.Vague ∧ c.Determinately SocialChoice.WeakOrderValued

With two utilitarian weightings of different cut-offs, the comparative is vague, yet determinately a weak ordering.

theorem DAmbrosioHedden2024.indeterminate_complete {K : Type u_3} [Field K] [LinearOrder K] {w : Health → K} {mS mB cB t : K} (c : Context Health Patient K) (hu : SocialChoice.utilitarian w ∈ c.adm) (hp : SocialChoice.paretoRule ∈ c.adm) (hm : mS < mB) (ht : cB < t) : c.Indeterminate SocialChoice.Complete

With a utilitarian weighting beside the Pareto rule, on a profile where Suzy trades musculoskeletal for cardiovascular health, it is indeterminate whether the comparative is complete.

Arrow's theorem and incoherence

def DAmbrosioHedden2024.Arrovian {ι : Type u_1} {O : Type u_2} {K : Type u_3} [Preorder K] (a : SocialChoice.Rule ι O K) : Prop

Arrow's conditions, transposed to dimensional aggregation.

Equations

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

theorem DAmbrosioHedden2024.arrow {ι : Type u_1} {O : Type u_2} [Fintype ι] [Fintype O] (h₃ : 3 ≤ Fintype.card O) (a : SocialChoice.Rule ι O ℝ) : ¬Arrovian a

By Arrow's impossibility theorem, with finitely many dimensions and at least three objects no rule meets all of Arrow's conditions.

theorem DAmbrosioHedden2024.Context.incoherent_of_arrovian {ι : Type u_1} {O : Type u_2} [Fintype ι] [Fintype O] (h₃ : 3 ≤ Fintype.card O) (c : Context ι O ℝ) (h : c.Determinately Arrovian) : c.Incoherent

An adjective whose admissible rules are all Arrovian is incoherent.

Escaping Arrow by weakening the outputs

def DAmbrosioHedden2024.Acyclic {O : Type u_2} (r : O → O → Prop) : Prop

A relation is acyclic, as the paper states it, when two strict steps yield a weak step.

Equations

• DAmbrosioHedden2024.Acyclic r = ∀ (x y z : O), AsymmRel r x y → AsymmRel r y z → r x z

def DAmbrosioHedden2024.condorcet : SocialChoice.Profile (Fin 3) (Fin 3) ℕ

Condorcet's profile has three dimensions ranking three objects cyclically.

Equations

• DAmbrosioHedden2024.condorcet = ![![2, 0, 1], ![1, 2, 0], ![0, 1, 2]]

theorem DAmbrosioHedden2024.majority_condorcet : AsymmRel (SocialChoice.majority condorcet) 0 1 ∧ AsymmRel (SocialChoice.majority condorcet) 1 2 ∧ AsymmRel (SocialChoice.majority condorcet) 2 0

Condorcet's paradox is that majority rule ranks the three objects in a strict cycle.

theorem DAmbrosioHedden2024.not_acyclic_majority_condorcet : ¬Acyclic (SocialChoice.majority condorcet)

Majority rule violates even acyclicity, by Condorcet's cycle.

Sassoon's comparatives

def DAmbrosioHedden2024.sassoon {ι : Type u_1} {O : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] (θ : ι → K) : Degree.DimensionBindingType → SocialChoice.Rule ι O K

The comparative the paper attributes to Sassoon for each binding type is universal quantification over the dimensions for conjunctive adjectives (healthy), existential for disjunctive ones (sick), and for mixed ones (intelligent) counting the dimensions on which the thresholds θ are met.

Equations

• DAmbrosioHedden2024.sassoon θ Degree.DimensionBindingType.conjunctive = fun (v : SocialChoice.Profile ι O K) (x y : O) => ∀ (i : ι), v y i ≤ v x i
• DAmbrosioHedden2024.sassoon θ Degree.DimensionBindingType.disjunctive = fun (v : SocialChoice.Profile ι O K) (x y : O) => ∃ (i : ι), v y i ≤ v x i
• DAmbrosioHedden2024.sassoon θ Degree.DimensionBindingType.mixed = fun (v : SocialChoice.Profile ι O K) (x y : O) => {i : ι | θ i ≤ v y i}.card ≤ {i : ι | θ i ≤ v x i}.card

theorem DAmbrosioHedden2024.sassoon_conjunctive {ι : Type u_1} {O : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] (θ : ι → K) : sassoon θ Degree.DimensionBindingType.conjunctive = SocialChoice.paretoRule

The universal comparative is the Pareto rule, and inherits its incomparable trade-offs.

theorem DAmbrosioHedden2024.not_strongPareto_sassoon_disjunctive {ι : Type u_1} {O : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] (θ : ι → K) [Nontrivial ι] [Nontrivial O] [Nontrivial K] : ¬SocialChoice.StrongPareto (sassoon θ Degree.DimensionBindingType.disjunctive)

The existential comparative violates strong Pareto, since an object tied with another on one dimension and below it on all others counts as at least as F.

theorem DAmbrosioHedden2024.not_weakPareto_sassoon_mixed {ι : Type u_1} {O : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] (θ : ι → K) [Nonempty ι] [Nontrivial O] [NoMaxOrder K] : ¬SocialChoice.WeakPareto (sassoon θ Degree.DimensionBindingType.mixed)

Dimension counting violates weak Pareto, since two objects meeting the thresholds on the same dimensions are tied, even when one is strictly above the other on every dimension.