Solt (2018): Proportional Comparatives and Relative Scales

More residents of Ithaca than New York City know their neighbors has a true reading that compares proportions although the absolute counts point the other way. Solt accounts for it with measurement: many and few are unambiguous gradable quantifiers, and a null head Meas introduces a contextual measure function, monotone on the part-whole order, which may be restricted to the parts of a totality and in particular be proportional. The rival ambiguity account, after Partee and Romero, gives many and few a cardinal and a proportional entry. The accounts part on the distribution of readings. With an individual-level predicate or in a partitive the measure is domain-restricted, and then the positive form reads proportionally only while the comparative keeps its cardinal reading; the ambiguity account predicts that both lose it.

Main statements

• percent_iff_proportionalMeasure: n percent is a point on the proportional scale.
• readings_diverge: when the cardinal and proportional readings of a comparative come apart.
• restricted_asymmetry: with only restricted measures, the comparative keeps its cardinal reading and the positive form loses it.
• ambiguity_symmetric: on the ambiguity account both forms read alike.

Implementation notes

The paper reports the populations of Ithaca and New York City in prose and no counts of residents who know their neighbours, so the divergence of the two readings is stated symbolically: a smaller part is the larger share exactly when its totality is small enough. Solt's other 2018 paper, the multidimensionality chapter, is formalized in Studies/Solt2018a.lean.

References

• [Sol18b]
• [Par89]
• [Rom15b]
• [Sol15]
• [Sch06b]
• [AS17]
• [Car77a]
• [Mil77]

The proportional measure function

def Solt2018b.proportionalMeasure {α : Type u_1} (μ : α → ℚ) (tot y : α) : ℚ

The proportional measure function gives a part's measure relative to the totality tot, and 0 when the totality has measure 0, as division by zero does.

Equations

• Solt2018b.proportionalMeasure μ tot y = μ y / μ tot

theorem Solt2018b.proportionalMeasure_eq {α : Type u_1} (μ : α → ℚ) (tot y : α) : proportionalMeasure μ tot y = μ y / μ tot

theorem Solt2018b.proportionalMeasure_zero {α : Type u_1} (μ : α → ℚ) (tot y : α) (h : μ tot = 0) : proportionalMeasure μ tot y = 0

theorem Solt2018b.proportionalMeasure_self_eq_one {α : Type u_1} (μ : α → ℚ) (tot : α) (htot : 0 < μ tot) : proportionalMeasure μ tot tot = 1

The totality is the whole of itself.

theorem Solt2018b.proportionalMeasure_monotonic {α : Type u_1} (μ : α → ℚ) [Preorder α] (hμ : StrictMono μ) (tot : α) {y z : α} (htot : 0 < μ tot) (hyz : y < z) : proportionalMeasure μ tot y < proportionalMeasure μ tot z

The monotonicity constraint on the measure Meas introduces (mathlib's StrictMono) is inherited by the proportional measure.

theorem Solt2018b.proportionalMeasure_nonneg {α : Type u_1} (μ : α → ℚ) (hnn : ∀ (x : α), 0 ≤ μ x) (tot y : α) : 0 ≤ proportionalMeasure μ tot y

theorem Solt2018b.proportionalMeasure_le_one {α : Type u_1} (μ : α → ℚ) [Preorder α] (hμ : Monotone μ) (tot y : α) (hy : y ≤ tot) (htot : 0 < μ tot) : proportionalMeasure μ tot y ≤ 1

theorem Solt2018b.proportionalMeasure_mem_unit_interval {α : Type u_1} (μ : α → ℚ) [Preorder α] (hnn : ∀ (x : α), 0 ≤ μ x) (hμ : Monotone μ) (tot y : α) (hy : y ≤ tot) (htot : 0 < μ tot) : proportionalMeasure μ tot y ∈ Set.Icc 0 1

A part of the totality measures between 0 and 1 on the proportional scale.

theorem Solt2018b.proportionalMeasure_const_mul {α : Type u_1} (μ : α → ℚ) (k : ℚ) (hk : k ≠ 0) (tot y : α) : proportionalMeasure (fun (x : α) => k * μ x) tot y = proportionalMeasure μ tot y

Rescaling the underlying measure leaves proportions unchanged, so only the cardinal reading depends on the unit of measurement.

theorem Solt2018b.percent_iff_proportionalMeasure {α : Type u_1} (μ : α → ℚ) [SemilatticeInf α] (x p : α) (n : ℚ) : μ (x ⊓ p) / μ x = n / 100 ↔ proportionalMeasure μ x (x ⊓ p) = n / 100

n percent of x are P on the lexical entry for percent of [AS17], which lexicalizes the division, holds exactly when the proportional measure of the P-part of x is the degree n / 100, a point on the proportional scale.

The two readings of a quantity comparative

def Solt2018b.CardinalReading {α : Type u_1} (μ : α → ℚ) (a b : α) : Prop

On the cardinal reading, more A than B Q says that the A-part with the property outmeasures the B-part.

Equations

• Solt2018b.CardinalReading μ a b = (μ b < μ a)

def Solt2018b.ProportionalReading {α : Type u_1} (μ : α → ℚ) (A B a b : α) : Prop

On the proportional reading, where the measure Meas introduces is proportional to each clause's totality, more A than B Q says that the A-part is the larger share of its totality.

Equations

• Solt2018b.ProportionalReading μ A B a b = (Solt2018b.proportionalMeasure μ B b < Solt2018b.proportionalMeasure μ A a)

theorem Solt2018b.proportionalReading_iff {α : Type u_1} (μ : α → ℚ) {A B a b : α} (hA : 0 < μ A) (hB : 0 < μ B) : ProportionalReading μ A B a b ↔ μ b * μ A < μ a * μ B

theorem Solt2018b.readings_diverge {α : Type u_1} (μ : α → ℚ) {A B a b : α} (hA : 0 < μ A) (hB : 0 < μ B) (h : μ a < μ b) (h' : μ b * μ A < μ a * μ B) : ¬CardinalReading μ a b ∧ ProportionalReading μ A B a b

The readings come apart, since a part that is outmeasured by the other is nonetheless the larger share whenever its totality is small enough, as with Ithaca's thirty thousand residents against New York City's eight million.

The distribution of readings

inductive Solt2018b.MeasureKind : Type

The measure function Meas introduces is unrestricted, restricted to the parts of a totality, or the proportional special case of the latter.

• unrestricted : MeasureKind
• domainRestricted : MeasureKind
• proportional : MeasureKind

@[instance_reducible]

instance Solt2018b.instDecidableEqMeasureKind : DecidableEq MeasureKind

Equations

• Solt2018b.instDecidableEqMeasureKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Solt2018b.instReprMeasureKind : Repr MeasureKind

Equations

• Solt2018b.instReprMeasureKind = { reprPrec := Solt2018b.instReprMeasureKind.repr }

def Solt2018b.instReprMeasureKind.repr : MeasureKind → ℕ → Std.Format

Equations

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

def Solt2018b.MeasureKind.IsRestricted : MeasureKind → Prop

The kinds whose range is a bounded segment of the scale.

Equations

• Solt2018b.MeasureKind.unrestricted.IsRestricted = False
• Solt2018b.MeasureKind.domainRestricted.IsRestricted = True
• Solt2018b.MeasureKind.proportional.IsRestricted = True

@[instance_reducible]

instance Solt2018b.instDecidableIsRestricted (k : MeasureKind) : Decidable k.IsRestricted

Equations

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

inductive Solt2018b.Reading : Type

Cardinal or proportional reading of a quantity word.

• cardinal : Reading
• proportional : Reading

@[instance_reducible]

instance Solt2018b.instDecidableEqReading : DecidableEq Reading

Equations

• Solt2018b.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Solt2018b.instReprReading.repr : Reading → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Solt2018b.instReprReading.repr Solt2018b.Reading.cardinal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solt2018b.Reading.cardinal")).group prec✝

@[instance_reducible]

instance Solt2018b.instReprReading : Repr Reading

Equations

• Solt2018b.instReprReading = { reprPrec := Solt2018b.instReprReading.repr }

inductive Solt2018b.QForm : Type

The positive form, bound by the positive morpheme, and the comparative.

• positive : QForm
• comparative : QForm

@[instance_reducible]

instance Solt2018b.instDecidableEqQForm : DecidableEq QForm

Equations

• Solt2018b.instDecidableEqQForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Solt2018b.instReprQForm.repr : QForm → ℕ → Std.Format

Equations

• Solt2018b.instReprQForm.repr Solt2018b.QForm.positive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solt2018b.QForm.positive")).group prec✝
• Solt2018b.instReprQForm.repr Solt2018b.QForm.comparative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solt2018b.QForm.comparative")).group prec✝

@[instance_reducible]

instance Solt2018b.instReprQForm : Repr QForm

Equations

• Solt2018b.instReprQForm = { reprPrec := Solt2018b.instReprQForm.repr }

def Solt2018b.reading : QForm → MeasureKind → Reading

How each form reads a kind of measure. The comparative compares the degrees the measure delivers, cardinal unless the measure is proportional. The positive morpheme's standard range sits inside the bounded segment that is a restricted measure's range, so either restricted kind gives the positive form its proportional reading.

Equations

• Solt2018b.reading Solt2018b.QForm.comparative Solt2018b.MeasureKind.proportional = Solt2018b.Reading.proportional
• Solt2018b.reading Solt2018b.QForm.comparative x✝ = Solt2018b.Reading.cardinal
• Solt2018b.reading Solt2018b.QForm.positive Solt2018b.MeasureKind.unrestricted = Solt2018b.Reading.cardinal
• Solt2018b.reading Solt2018b.QForm.positive x✝ = Solt2018b.Reading.proportional

def Solt2018b.Licensed (allowed : MeasureKind → Prop) (f : QForm) (r : Reading) : Prop

A context whose available kinds are allowed licenses a reading of a form when some available kind yields it.

Equations

• Solt2018b.Licensed allowed f r = ∃ (k : Solt2018b.MeasureKind), allowed k ∧ Solt2018b.reading f k = r

theorem Solt2018b.unrestricted_licensed (f : QForm) (r : Reading) : Licensed (fun (x : MeasureKind) => True) f r

With every kind available, as under a stage-level predicate, both forms have both readings, as in few egg-laying mammals were found in our survey, perhaps because there are few.

theorem Solt2018b.restricted_positive_iff (r : Reading) : Licensed MeasureKind.IsRestricted QForm.positive r ↔ r = Reading.proportional

With only restricted kinds available, as under an individual-level predicate, which forces a domain-restricted measure, the positive form is proportional, so few egg-laying mammals suckle their young cannot mean that there are few.

theorem Solt2018b.restricted_asymmetry : Licensed MeasureKind.IsRestricted QForm.comparative Reading.cardinal ∧ ¬Licensed MeasureKind.IsRestricted QForm.positive Reading.cardinal

With only restricted kinds available, under an individual-level predicate or in a partitive, the comparative keeps its cardinal reading through an ordinary domain-restricted measure while the positive form loses it.

def Solt2018b.ambiguityKinds : MeasureKind → Prop

The ambiguity account has a cardinal and a proportional entry, and no relative-but-not-proportional measurement.

Equations

• Solt2018b.ambiguityKinds Solt2018b.MeasureKind.domainRestricted = False
• Solt2018b.ambiguityKinds x✝ = True

theorem Solt2018b.ambiguity_symmetric (r : Reading) : Licensed (fun (k : MeasureKind) => ambiguityKinds k ∧ k.IsRestricted) QForm.positive r ↔ Licensed (fun (k : MeasureKind) => ambiguityKinds k ∧ k.IsRestricted) QForm.comparative r

On the ambiguity account, whatever confines the positive form to its proportional reading confines the comparative too. With the inventory reduced to the proportional entry, both forms read alike, and the cardinal reading of more residents of Ithaca than New York City know their neighbors is lost.