[Sol18b]: Proportional comparatives and relative scales

More residents of Ithaca than New York City know their neighbors has a salient TRUE reading even though the absolute counts point the other way: the salient interpretation compares proportions, which standard degree analyses of the comparative ([vS84] a.o.) do not deliver. [Sol18b] compares two accounts:

1. Ambiguity ([Par89]; degree-based entries from [Rom15b], Solt's eq. 7): many and few are lexically ambiguous between a cardinal entry λd λP λQ. |P ∩ Q| ≽ d and a proportional entry λd λP λQ. |P ∩ Q| / |P| ≽ d.
2. Measurement-based (Solt's preferred analysis): many/few are unambiguous degree predicates; a null Meas head introduces a context-dependent measure function, which may be domain-restricted (eq. 20) or specifically proportional (eq. 21): μ^c_{DIM-prop;x}(y) = μ^c_DIM(y) / μ^c_DIM(x), with range [0, 1].

The adjudicating evidence (Solt §4) is the distribution of readings: with an individual-level predicate the positive form gets only the proportional reading, while the comparative keeps both (licensedReadings, comparative_keeps_cardinal) — an asymmetry the ambiguity account cannot derive.

Solt's eq. (21) is an instance of spatialNormalizedScore (Semantics/Degree/Aggregation.lean) with a single unit-weighted measure and constant denominator μ_DIM(totality); the monotonicity constraint on measure functions (Solt's eq. 18, after [Sch06]) is the substrate's Degree.admissibleMeasure.

Main declarations

• proportionalMeasure: Solt's eq. (21) proportional measure function
• cardinal_proportional_divergence: the headline example's two readings come apart — cardinal FALSE, proportional TRUE
• licensedReadings, comparative_keeps_cardinal: Solt §4's distribution of readings over predicate level × positive/comparative form
• proportionalMeasure_monotonic, proportionalMeasure_mem_unit_interval, proportionalMeasure_scale_invariant: eq. (21) is a normalized monotone measure — the discrete analogue of conditional measure

Solt's other 2018 paper, the multidimensionality chapter [Sol18a], shares this paper's scale foundation; see Studies/Solt2018Multidim.lean.

The proportional measure function

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

Solt's eq. (21): the proportional measure function for a dimension measured by μ, relative to totality tot, applied to part y; returns μ(y) / μ(tot), and 0 when the totality has zero measure (the spatialNormalizedScore zero-extent convention).

Equations

• Solt2018Proportional.proportionalMeasure μ tot y = Degree.Aggregation.spatialNormalizedScore [1] [μ] (fun (x : α) => μ tot) y

theorem Solt2018Proportional.proportionalMeasure_eq {α : Type u_1} (μ : α → ℚ) (tot y : α) (h : μ tot ≠ 0) : proportionalMeasure μ tot y = μ y / μ tot

proportionalMeasure computed: μ(y) / μ(tot) when μ(tot) ≠ 0.

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

A zero-measure totality (empty domain) yields proportion 0.

The proportional-comparative puzzle

Solt's example (1), More residents of Ithaca than New York City know their neighbors: Ithaca's population is dwarfed by NYC's, so the absolute count of Ithaca residents who know their neighbors is smaller, yet the sentence has a salient TRUE reading comparing proportions. Counts below are illustrative — the paper reports populations only in prose.

structure Solt2018Proportional.City : Type

A city with a total resident count and a count of residents who know their neighbors.

• population : ℚ
• knowsNeighbors : ℚ
• popPos : 0 < self.population
• subBounded : self.knowsNeighbors ≤ self.population

inductive Solt2018Proportional.Residents : Type

The two salient resident pluralities of a city: the residents who know their neighbors, and the totality.

• knowers : Residents
• all : Residents

def Solt2018Proportional.City.card (c : City) : Residents → ℚ

The cardinality measure on a city's resident pluralities (Solt's μ_#).

Equations

• c.card Solt2018Proportional.Residents.knowers = c.knowsNeighbors
• c.card Solt2018Proportional.Residents.all = c.population

def Solt2018Proportional.ithaca : City

Ithaca: small population, high proportion know their neighbors.

Equations

• Solt2018Proportional.ithaca = { population := 30000, knowsNeighbors := 24000, popPos := Solt2018Proportional.ithaca._proof_1, subBounded := Solt2018Proportional.ithaca._proof_2 }

def Solt2018Proportional.nyc : City

New York City: huge population, low proportion know their neighbors.

Equations

• Solt2018Proportional.nyc = { population := 8000000, knowsNeighbors := 800000, popPos := Solt2018Proportional.nyc._proof_1, subBounded := Solt2018Proportional.nyc._proof_2 }

theorem Solt2018Proportional.cardinal_reading_ithaca_lt_nyc : ithaca.card Residents.knowers < nyc.card Residents.knowers

Cardinal reading of (1): FALSE — in absolute terms more NYC residents know their neighbors.

theorem Solt2018Proportional.proportional_reading_ithaca_gt_nyc : proportionalMeasure nyc.card Residents.all Residents.knowers < proportionalMeasure ithaca.card Residents.all Residents.knowers

Proportional reading of (1): TRUE — the proportion of Ithaca residents who know their neighbors exceeds NYC's, via proportionalMeasure with the cardinality measure City.card.

theorem Solt2018Proportional.cardinal_proportional_divergence : ithaca.card Residents.knowers < nyc.card Residents.knowers ∧ proportionalMeasure nyc.card Residents.all Residents.knowers < proportionalMeasure ithaca.card Residents.all Residents.knowers

The two readings of (1) diverge: cardinal FALSE, proportional TRUE. Solt's measurement-based account derives both from one Meas head instantiated with different measure-function varieties.

Distribution of cardinal vs proportional readings

Solt §4 (pp. 1135–1136): with an individual-level predicate ([Car77]; [Mil77], [Par89] for the many/few observation), the Meas head is necessarily domain-restricted, and the standard range introduced by POS sits inside the bounded segment [0, μ(totality)] of the scale — so the positive form is necessarily proportional (Solt's diagram 23). The comparative composes with -er rather than POS, so an ordinary (non-proportional) domain-restricted measure still yields its cardinal reading: both readings survive. Solt's examples (35) vs (36) diagnose the positive restriction; her (1)–(2) — individual-level comparatives with available false cardinal readings — witness the comparative's freedom. The ambiguity account cannot derive this asymmetry: if only proportional many combines with individual-level predicates, the comparative should lose its cardinal reading too.

inductive Solt2018Proportional.Reading : Type

Cardinal vs proportional reading of a quantity word.

• cardinal : Reading
• proportional : Reading

@[instance_reducible]

instance Solt2018Proportional.instDecidableEqReading : DecidableEq Reading

Equations

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

inductive Solt2018Proportional.QForm : Type

Positive (bare, POS-bound) vs comparative (-er) form of many/few.

• positive : QForm
• comparative : QForm

def Solt2018Proportional.licensedReadings : Semantics.Kinds.SortedOntology.PredicateLevel → QForm → List Reading

Solt §4's distribution of readings by predicate level and form: the positive form loses its cardinal reading under an individual-level predicate; the comparative never does.

Equations

• One or more equations did not get rendered due to their size.
• Solt2018Proportional.licensedReadings Semantics.Kinds.SortedOntology.PredicateLevel.stageLevel x✝ = [Solt2018Proportional.Reading.cardinal, Solt2018Proportional.Reading.proportional]
• Solt2018Proportional.licensedReadings Semantics.Kinds.SortedOntology.PredicateLevel.individualLevel Solt2018Proportional.QForm.positive = [Solt2018Proportional.Reading.proportional]

theorem Solt2018Proportional.stage_level_both_readings (f : QForm) : Reading.cardinal ∈ licensedReadings Semantics.Kinds.SortedOntology.PredicateLevel.stageLevel f ∧ Reading.proportional ∈ licensedReadings Semantics.Kinds.SortedOntology.PredicateLevel.stageLevel f

Stage-level predicates license both readings of both forms — Solt's (35), few egg-laying mammals were found in our survey.

theorem Solt2018Proportional.positive_individual_only_proportional : licensedReadings Semantics.Kinds.SortedOntology.PredicateLevel.individualLevel QForm.positive = [Reading.proportional]

The positive form is proportional-only under an individual-level predicate — Solt's (36), #few egg-laying mammals suckle their young, perhaps because there are few.

theorem Solt2018Proportional.comparative_keeps_cardinal : Reading.cardinal ∈ licensedReadings Semantics.Kinds.SortedOntology.PredicateLevel.individualLevel QForm.comparative ∧ Reading.cardinal ∉ licensedReadings Semantics.Kinds.SortedOntology.PredicateLevel.individualLevel QForm.positive

The §4 asymmetry that adjudicates between the accounts: exactly where the positive form loses the cardinal reading, the comparative keeps it (Solt's (1)–(2) retain false cardinal readings).

Structural properties: a normalized monotone measure

With a monotonic measure (Solt's eq. 18 constraint = admissibleMeasure, after [Sch06]), proportionalMeasure is bounded in [0, 1], saturates at the totality, preserves the part order, and is invariant under rescaling of the underlying measure — a normalized monotone measure, the discrete analogue of conditional measure.

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

The proportion of the totality in itself is 1: saturation.

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

Solt's eq. (18) monotonicity constraint is preserved by the eq. (21) construction: an admissibleMeasure yields a strictly monotone proportion whenever the totality has positive measure.

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

The proportional measure is nonnegative when the underlying measure is.

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

The proportional measure of a part of the totality is at most 1.

theorem Solt2018Proportional.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

Probability-style range: for a monotone nonnegative measure and a part y ≤ tot with 0 < μ(tot), the proportion lies in the unit interval.

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

Scale invariance: rescaling the measure by a nonzero constant leaves the proportion unchanged — the proportional reading of (1) does not depend on the unit of counting, only the cardinal reading does.