Bale and Schwarz (2022): Measurements from "per" without complex dimensions

On Coppock's division theory the preposition per divides quantities, so that 0.9 grams per milliliter denotes the density 0.9 g/mL. On Bale and Schwarz's anaphoric theory per milliliter measures a covert pronoun in milliliters, a pure number that multiplies 0.9 g, and the measure phrase stays in the dimension of mass. The division theory undergenerates: weigh measures weight, so it cannot take a quotient, and the polysemous weigh that would let it predicts a same-density reading of this cube weighs what that cube weighs that the sentence lacks. It also overgenerates: it gives 0.1 grams per milliliter and 0.1 kilograms per liter one meaning, while the anaphoric per, which sees the pronoun's referent, presupposes that the referent measures at least one unit. Where both theories compose they agree.

A world assigns each base dimension a real-valued measure function, and the units are the English measure terms.

Main statements

• not_much_divisionMP: a measurement verb never takes a measure phrase of the division theory, whatever its units.
• density_reading: the polysemous weigh makes this cube weighs what that cube weighs true of a one-kilogram and a two-kilogram cube.
• anaphoricMP_snd: an anaphoric measure phrase has the dimension of its head unit.
• much_divisionMP_iff_anaphoricMP, contains_divisionMP_iff_anaphoricMP: where both theories compose, they derive the same truth conditions.
• divisionMP_kilogram_liter: the division theory identifies 0.1 kilograms per liter with 0.1 grams per milliliter.
• unit_sensitivity: on the anaphoric theory the two pseudo-partitives assert the same thing, but one presupposes a volume of at least a milliliter and the other of at least a liter.
• division_overgenerates: at a world where the sample measures a tenth of a milliliter, the division theory makes the 0.1 milliliter sample contained 0.1 grams of salt per milliliter true, while on the anaphoric theory it is undefined.
• acceptable_iff_mem_dom: a per-sentence is defined at a world where its subject measures as the example states exactly when the example is felicitous.
• density_ne_anaphoricMP: the anaphoric theory makes the sample's density is 0.9 grams per milliliter contradictory, the puzzle the paper ends on.

Implementation notes

• A sentence with per denotes a partial proposition World E →. Prop, after the Heim–Kratzer notation of (43). It maps its truth conditions over the value of the per-phrase, so the sentence is defined where per is: the global projection the paper assumes (p. 557).
• The covert pronoun is a parameter, resolved to the matrix subject.
• (43) compares two quantities of one dimension; the file compares their magnitudes.

References

• [BS22]
• [Cop21]
• [HK98]
• [Nak07]
• [Sch06b]

@[reducible, inline]

abbrev BaleSchwarz2022.World (E : Type u_2) : Type u_2

A world assigns each base dimension D its measure function μ_D.

Equations

• BaleSchwarz2022.World E = (Degree.Dimension → E → ℝ)

def BaleSchwarz2022.World.measure {E : Type u_1} (w : World E) (D : Degree.Dimension) : Degree.DimensionedMeasure E

w.measure D is the measure function μ_D as a measure of dimension D.

Equations

• w.measure D = { dimension := D, toFun := w D }

def BaleSchwarz2022.World.quantity {E : Type u_1} (w : World E) (D : Degree.Dimension) (x : E) : Degree.Quantity ℝ

w.quantity D x is μ_D(x), a quantity of dimension D.

Equations

• w.quantity D x = (w.measure D).quantity x

@[simp]

theorem BaleSchwarz2022.World.quantity_fst {E : Type u_1} (w : World E) (D : Degree.Dimension) (x : E) : (w.quantity D x).1 = w D x

@[simp]

theorem BaleSchwarz2022.World.quantity_snd {E : Type u_1} (w : World E) (D : Degree.Dimension) (x : E) : (w.quantity D x).2 = Degree.QuantityDimension.of D

Measure predication

def BaleSchwarz2022.much {E : Type u_1} (μ : E → Degree.Quantity ℝ) (q : Degree.Quantity ℝ) (x : E) : Prop

much μ q x says that x measures q under μ, λq λx. μ(x) = q. It is the measurement verb weigh with μ = μ_WT ((5)), and the covert MUCH of pseudo-partitives with μ underspecified ((25)).

Equations

• BaleSchwarz2022.much μ q x = (μ x = q)

theorem BaleSchwarz2022.much_quantity_iff {E : Type u_1} {w : World E} {D : Degree.Dimension} {x : E} {q : Degree.Quantity ℝ} : much (w.quantity D) q x ↔ w D x = q.1 ∧ q.2 = Degree.QuantityDimension.of D

theorem BaleSchwarz2022.not_much_quantity_of_snd_ne {E : Type u_1} {w : World E} {D : Degree.Dimension} {x : E} {q : Degree.Quantity ℝ} (h : q.2 ≠ Degree.QuantityDimension.of D) : ¬much (w.quantity D) q x

A measure of dimension D never equates with a quantity of another dimension.

def BaleSchwarz2022.contains {E : Type u_1} (salt : E → Prop) (contain : E → E → Prop) (μ : E → Degree.Quantity ℝ) (q : Degree.Quantity ℝ) (m : E) : Prop

contains salt contain μ q m says that m contains salt of measure q under μ, ∃x[salt(x) ∧ μ(x) = q ∧ contain(m, x)] ((26)).

Equations

• BaleSchwarz2022.contains salt contain μ q m = ∃ (x : E), salt x ∧ BaleSchwarz2022.much μ q x ∧ contain m x

The division theory

noncomputable def BaleSchwarz2022.divisionPer (r q : Degree.Quantity ℝ) : Degree.Quantity ℝ

Coppock's per divides its second argument by its first, ⟦per⟧ = λr λq. q / r ((1)).

Equations

• BaleSchwarz2022.divisionPer r q = q / r

noncomputable def BaleSchwarz2022.divisionMP (n : ℝ) (u r : English.MeasurePhrases.MeasureTerm) : Degree.Quantity ℝ

On the division theory n u per r denotes the quotient n u / r ((2)).

Equations

• BaleSchwarz2022.divisionMP n u r = BaleSchwarz2022.divisionPer r.quantity (Degree.Quantity.pure n * u.quantity)

@[simp]

theorem BaleSchwarz2022.divisionMP_snd {n : ℝ} {u r : English.MeasurePhrases.MeasureTerm} : (divisionMP n u r).2 = Degree.QuantityDimension.of u.dimension / Degree.QuantityDimension.of r.dimension

theorem BaleSchwarz2022.not_much_divisionMP {E : Type u_1} {w : World E} {D : Degree.Dimension} {x : E} {n : ℝ} {u r : English.MeasurePhrases.MeasureTerm} : ¬much (w.quantity D) (divisionMP n u r) x

The division theory undergenerates ((7)): a measure of a base dimension never equates with a per-phrase, whose dimension is a quotient.

noncomputable def BaleSchwarz2022.density {E : Type u_1} (w : World E) (x : E) : Degree.Quantity ℝ

The polysemous weigh of (8) measures density, μ_{WT/VOL}.

Equations

• BaleSchwarz2022.density w x = w.quantity Degree.Dimension.mass x / w.quantity Degree.Dimension.volume x

theorem BaleSchwarz2022.much_quantity_quantity_iff {E : Type u_1} {w : World E} {D : Degree.Dimension} {x y : E} : much (w.quantity D) (w.quantity D y) x ↔ w D x = w D y

With the free relative denoting y's measure, x weighs what y weighs equates the two measures ((12)).

theorem BaleSchwarz2022.density_reading : ∃ (w : World (Fin 2)), much (density w) (density w 1) 0 ∧ ¬much (w.quantity Degree.Dimension.mass) (w.quantity Degree.Dimension.mass 1) 0

The polysemous weigh gives this cube weighs what that cube weighs a same-density reading ((13)) that is true of a one-kilogram and a two-kilogram cube, where the weight reading ((12)) is false.

The anaphoric theory

noncomputable def BaleSchwarz2022.anaphoricPer {E : Type u_1} (w : World E) (r : English.MeasurePhrases.MeasureTerm) (y : E) : Degree.Quantity ℝ

Bale and Schwarz's per measures its pronoun's referent in units of its quantity argument, ⟦per⟧ = λq λx. μ_dim(q)(x) / q ((16)), a pure number.

Equations

• BaleSchwarz2022.anaphoricPer w r y = w.quantity r.dimension y / r.quantity

@[simp]

theorem BaleSchwarz2022.anaphoricPer_fst {E : Type u_1} {w : World E} {y : E} {r : English.MeasurePhrases.MeasureTerm} : (anaphoricPer w r y).1 = w r.dimension y / ↑r.magnitude

@[simp]

theorem BaleSchwarz2022.anaphoricPer_snd {E : Type u_1} {w : World E} {y : E} {r : English.MeasurePhrases.MeasureTerm} : (anaphoricPer w r y).2 = 1

noncomputable def BaleSchwarz2022.anaphoricMP {E : Type u_1} (w : World E) (n : ℝ) (u r : English.MeasurePhrases.MeasureTerm) (y : E) : Degree.Quantity ℝ

The anaphoric n u per r, its pronoun resolved to y, denotes n u ⋅ μ_dim(r)(y) / r ((18)).

Equations

• BaleSchwarz2022.anaphoricMP w n u r y = Degree.Quantity.pure n * u.quantity * BaleSchwarz2022.anaphoricPer w r y

@[simp]

theorem BaleSchwarz2022.anaphoricMP_fst {E : Type u_1} {w : World E} {y : E} {n : ℝ} {u r : English.MeasurePhrases.MeasureTerm} : (anaphoricMP w n u r y).1 = n * ↑u.magnitude * (w r.dimension y / ↑r.magnitude)

@[simp]

theorem BaleSchwarz2022.anaphoricMP_snd {E : Type u_1} {w : World E} {y : E} {n : ℝ} {u r : English.MeasurePhrases.MeasureTerm} : (anaphoricMP w n u r y).2 = Degree.QuantityDimension.of u.dimension

The anaphoric measure phrase stays in its head unit's dimension ((19)).

theorem BaleSchwarz2022.much_anaphoricMP_iff {E : Type u_1} {w : World E} {D : Degree.Dimension} {x y : E} {n : ℝ} {u r : English.MeasurePhrases.MeasureTerm} (hu : u.dimension = D) : much (w.quantity D) (anaphoricMP w n u r y) x ↔ w D x = n * ↑u.magnitude * (w r.dimension y / ↑r.magnitude)

The measurement-verb sentence composes ((22)): μ_D(x) = n u ⋅ μ_dim(r)(y) / r.

theorem BaleSchwarz2022.much_divisionMP_iff_anaphoricMP {E : Type u_1} {w : World E} {D : Degree.Dimension} {x y : E} {n : ℝ} {u r : English.MeasurePhrases.MeasureTerm} (hy : w r.dimension y ≠ 0) : much (fun (x : E) => w.quantity D x / w.quantity r.dimension y) (divisionMP n u r) x ↔ much (w.quantity D) (anaphoricMP w n u r y) x

Where both theories compose they agree: (9) and (22) with the pronoun's referent the subject, (31) and (32) with it the container.

theorem BaleSchwarz2022.contains_divisionMP_iff_anaphoricMP {E : Type u_1} {w : World E} {D : Degree.Dimension} {m : E} {n : ℝ} {u r : English.MeasurePhrases.MeasureTerm} {salt : E → Prop} {contain : E → E → Prop} (hm : w r.dimension m ≠ 0) : contains salt contain (fun (x : E) => w.quantity D x / w.quantity r.dimension m) (divisionMP n u r) m ↔ contains salt contain (w.quantity D) (anaphoricMP w n u r m) m

Units of different sizes

theorem BaleSchwarz2022.divisionMP_scales {n k : ℝ} {u u' r r' : English.MeasurePhrases.MeasureTerm} (hk : k ≠ 0) (hu : u'.quantity = Degree.Quantity.pure k * u.quantity) (hr : r'.quantity = Degree.Quantity.pure k * r.quantity) : divisionMP n u' r' = divisionMP n u r

The division theory identifies measure phrases whose units are scaled alike ((36b)).

theorem BaleSchwarz2022.divisionMP_kilogram_liter {n : ℝ} : divisionMP n English.MeasurePhrases.kilogram English.MeasurePhrases.liter = divisionMP n English.MeasurePhrases.gram English.MeasurePhrases.milliliter

So it gives 0.1 kilograms per liter the meaning of 0.1 grams per milliliter, since kg / L = g / mL ((36)).

theorem BaleSchwarz2022.anaphoricMP_scales {E : Type u_1} {w : World E} {y : E} {n k : ℝ} {u u' r r' : English.MeasurePhrases.MeasureTerm} (hk : k ≠ 0) (hu : u'.quantity = Degree.Quantity.pure k * u.quantity) (hr : r'.quantity = Degree.Quantity.pure k * r.quantity) : anaphoricMP w n u' r' y = anaphoricMP w n u r y

So does the anaphoric theory.

The copular puzzle

theorem BaleSchwarz2022.density_ne_of_snd {E : Type u_1} {w : World E} {x : E} {q : Degree.Quantity ℝ} (hq : q.2 = Degree.QuantityDimension.of Degree.Dimension.mass) : density w x ≠ q

No quantity of mass is a density, so the sample's density is 0.9 grams ((47)) is contradictory.

theorem BaleSchwarz2022.density_ne_pure_mul {E : Type u_1} {w : World E} {x : E} {n : ℝ} {u : English.MeasurePhrases.MeasureTerm} (hu : u.dimension = Degree.Dimension.mass) : density w x ≠ Degree.Quantity.pure n * u.quantity

theorem BaleSchwarz2022.density_ne_anaphoricMP {E : Type u_1} {w : World E} {x y : E} {n : ℝ} {u r : English.MeasurePhrases.MeasureTerm} (hu : u.dimension = Degree.Dimension.mass) : density w x ≠ anaphoricMP w n u r y

On the anaphoric theory so is the sample's density is 0.9 grams per milliliter ((46)), which reports the sample's density.

theorem BaleSchwarz2022.density_eq_divisionMP_iff {E : Type u_1} {w : World E} {x : E} {n : ℝ} {u r : English.MeasurePhrases.MeasureTerm} (hu : u.dimension = Degree.Dimension.mass) (hr : r.dimension = Degree.Dimension.volume) : density w x = divisionMP n u r ↔ w Degree.Dimension.mass x / w Degree.Dimension.volume x = n * ↑u.magnitude / ↑r.magnitude

On the division theory (46) equates the sample's density with n u / r.

Unit sensitivity

noncomputable def BaleSchwarz2022.per {E : Type u_1} (w : World E) (r : English.MeasurePhrases.MeasureTerm) : E →. Degree.Quantity ℝ

The revised per of (43), λq λx: μ_dim(q)(x) ≥ q. μ_dim(q)(x) / q, is anaphoricPer restricted to the referents that measure at least one unit.

Equations

• BaleSchwarz2022.per w r = PFun.res (BaleSchwarz2022.anaphoricPer w r) {y : E | ↑r.magnitude ≤ w r.dimension y}

theorem BaleSchwarz2022.mem_dom_per {E : Type u_1} {w : World E} {y : E} {r : English.MeasurePhrases.MeasureTerm} : y ∈ (per w r).Dom ↔ ↑r.magnitude ≤ w r.dimension y

noncomputable def BaleSchwarz2022.perSentence {E : Type u_1} (r : English.MeasurePhrases.MeasureTerm) (y : E) (φ : World E → Degree.Quantity ℝ → Prop) : World E →. Prop

perSentence r y φ is a sentence whose per-phrase, its pronoun resolved to y, feeds the truth conditions φ. At each world it maps φ over the phrase's value, so the sentence is defined where per is.

Equations

• BaleSchwarz2022.perSentence r y φ w = Part.map (φ w) (BaleSchwarz2022.per w r y)

theorem BaleSchwarz2022.perSentence_eq_res {E : Type u_1} {y : E} {r : English.MeasurePhrases.MeasureTerm} {φ : World E → Degree.Quantity ℝ → Prop} : perSentence r y φ = PFun.res (fun (w : World E) => φ w (anaphoricPer w r y)) {w : World E | ↑r.magnitude ≤ w r.dimension y}

A per-sentence asserts its truth conditions where it presupposes that the pronoun's referent measures at least one unit.

@[simp]

theorem BaleSchwarz2022.mem_dom_perSentence {E : Type u_1} {w : World E} {y : E} {r : English.MeasurePhrases.MeasureTerm} {φ : World E → Degree.Quantity ℝ → Prop} : w ∈ (perSentence r y φ).Dom ↔ ↑r.magnitude ≤ w r.dimension y

noncomputable def BaleSchwarz2022.weighs {E : Type u_1} (n : ℝ) (u r : English.MeasurePhrases.MeasureTerm) (y : E) : World E →. Prop

y weighs n u per r, the pronoun resolved to the subject ((20)).

Equations

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

noncomputable def BaleSchwarz2022.containsPer {E : Type u_1} (salt : E → Prop) (contain : E → E → Prop) (n : ℝ) (u r : English.MeasurePhrases.MeasureTerm) (m : E) : World E →. Prop

m contains n u per r of salt, the pronoun resolved to the container ((41)).

Equations

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

theorem BaleSchwarz2022.weighs_scales {E : Type u_1} {y : E} {n k : ℝ} {u u' r r' : English.MeasurePhrases.MeasureTerm} (hk : k ≠ 0) (hu : u'.quantity = Degree.Quantity.pure k * u.quantity) (hr : r'.quantity = Degree.Quantity.pure k * r.quantity) : weighs n u' r' y = PFun.res (fun (w : World E) => much (w.quantity Degree.Dimension.mass) (anaphoricMP w n u r y) y) {w : World E | k * ↑r.magnitude ≤ w r.dimension y}

Scaling the units by k keeps a per-sentence's assertion and raises the bound its presupposition sets from one unit to k units.

theorem BaleSchwarz2022.containsPer_scales {E : Type u_1} {m : E} {n k : ℝ} {u u' r r' : English.MeasurePhrases.MeasureTerm} {salt : E → Prop} {contain : E → E → Prop} (hk : k ≠ 0) (hu : u'.quantity = Degree.Quantity.pure k * u.quantity) (hr : r'.quantity = Degree.Quantity.pure k * r.quantity) : containsPer salt contain n u' r' m = PFun.res (fun (w : World E) => contains salt contain (w.quantity Degree.Dimension.mass) (anaphoricMP w n u r m) m) {w : World E | k * ↑r.magnitude ≤ w r.dimension m}

theorem BaleSchwarz2022.unit_sensitivity {E : Type u_1} {m : E} {n : ℝ} {salt : E → Prop} {contain : E → E → Prop} : ∃ (A : World E → Prop), containsPer salt contain n English.MeasurePhrases.gram English.MeasurePhrases.milliliter m = PFun.res A {w : World E | 1 ≤ w Degree.Dimension.volume m} ∧ containsPer salt contain n English.MeasurePhrases.kilogram English.MeasurePhrases.liter m = PFun.res A {w : World E | 1000 ≤ w Degree.Dimension.volume m}

The anaphoric theory is unit sensitive ((27), (36)). The mixture contains 0.1 grams per milliliter of salt and the mixture contains 0.1 kilograms per liter of salt assert the same thing, but the first presupposes that the mixture measures at least a milliliter and the second at least a liter.

theorem BaleSchwarz2022.contains_divisionMP_satisfiable {n : ℝ} {u r : English.MeasurePhrases.MeasureTerm} (hu : u.dimension = Degree.Dimension.mass) {v : ℝ} (hv : v ≠ 0) : ∃ (w : World (Fin 2)), w r.dimension 0 = v ∧ contains (fun (x : Fin 2) => x = 1) (fun (a b : Fin 2) => a = 0 ∧ b = 1) (fun (x : Fin 2) => w.quantity Degree.Dimension.mass x / w.quantity r.dimension 0) (divisionMP n u r) 0

The division theory's truth conditions for m contains n u per r of salt ((31)) can hold whatever m measures in the per-unit's dimension.

theorem BaleSchwarz2022.division_overgenerates : ∃ (w : World (Fin 2)), contains (fun (x : Fin 2) => x = 1) (fun (a b : Fin 2) => a = 0 ∧ b = 1) (fun (x : Fin 2) => w.quantity Degree.Dimension.mass x / w.quantity Degree.Dimension.volume 0) (divisionMP (1 / 10) English.MeasurePhrases.gram English.MeasurePhrases.milliliter) 0 ∧ w ∉ (containsPer (fun (x : Fin 2) => x = 1) (fun (a b : Fin 2) => a = 0 ∧ b = 1) (1 / 10) English.MeasurePhrases.gram English.MeasurePhrases.milliliter 0).Dom

So the division theory overgenerates ((38b)): where the sample measures a tenth of a milliliter it makes the 0.1 milliliter sample contained 0.1 grams of salt per milliliter true, while on the anaphoric theory the sentence is undefined there.

The paper's examples

structure BaleSchwarz2022.Scenario : Type

An example's per-unit, and the measure in that unit's dimension that its subject is stated to have, in the dimension's reference unit.

• per : English.MeasurePhrases.MeasureTerm
• subjectMeasure : ℚ

def BaleSchwarz2022.scenario? (e : Datum) : Option Scenario

scenario? e reads the scenario off a row that states its subject's measure.

Equations

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

theorem BaleSchwarz2022.rows_unit_sensitivity (e : Datum) : e ∈ Examples.all → ∀ s ∈ scenario? e, s.per.magnitude ≤ s.subjectMeasure ↔ e.judgment = Judgment.acceptable

The subject measures at least one per-unit exactly in the felicitous examples ((37), (38), (44), (45)).

theorem BaleSchwarz2022.acceptable_iff_mem_dom {E : Type u_1} {w : World E} {y : E} {φ : World E → Degree.Quantity ℝ → Prop} {e : Datum} (he : e ∈ Examples.all) {s : Scenario} (hs : s ∈ scenario? e) (hy : w s.per.dimension y = ↑s.subjectMeasure) : e.judgment = Judgment.acceptable ↔ w ∈ (perSentence s.per y φ).Dom

At a world where its subject measures as the example states, a per-sentence is defined exactly when the example is felicitous.