Scontras (2014): The Semantics of Measurement

Scontras's third chapter studies quantizing nouns, the words that package a substance for counting or measuring. Diagnostics adapted from Rothstein separate three readings of n Q of S and three classes of noun (Data/Examples/Scontras2014): a container noun like glass is a plain predicate whose container reading arises from intersective modification by the preposition of, contributing the filled-with relation ((38), containerReading); a measure term like liter is a relation between a numeral and the instances of the substance that measure it ((41), measureReading); an atomizer like grain partitions the substance into countable units ((77), atomizingReading). The readings differ in what they refer to (Table 3.1): a container reading refers to containers, the quantizing noun's own denotation, while measure and atomizing readings refer to the substance (containerReading_subset, measureReading_subset, atomizingReading_subset); the measure reading is moreover quantity-uniform under the term's measure (measureReading_quantity_uniform). Each of the first two classes has uses as the other, the container noun by a shift on the model of the measure suffix -ful ((47), shiftCM) and the measure term by lexical reinterpretation as the class of containers of a unit quantity ((52), shiftMC); atomizers, being neither predicates of containers nor measures, have no measure use.

Countable units are the maximally self-connected instances of a kind in Grimm's mereotopology, parthood with a connection relation ((72), (73), Mereology.IsConnection) and self-connection ((74), Mereology.SelfConnected), and a partition returns such units ((75), (76), IsMSCPartition); no-overlap alone ((66), DisjointPred Overlap) does not stop the water in a glass from counting as two. Either way the members of a partition form an antichain, so each of them measures one relative atom under the relative-atom measure of (68) (pAtomMeasure_eq_one), which is what lets cardinal numerals count them.

Implementation notes

• Kinds are represented by their instantiation predicates, the ∪k of the chapter, and an atomizer's selectional presupposition ((79), (87)) by an added conjunct rather than a domain condition.
• The chapter's argument that the container-to-measure shift cannot be compositional, since a continuous measure cannot be built from a predicate, is respected by taking (47), which counts filled containers, as the shift; the measure-term-to-container shift is stated as (52) with the remark that world knowledge narrows its output.
• Quantity uniformity, the condition the number marking of the second chapter checks, is that the measure takes one value on the predicate, Set.Subsingleton of its image.
• Of the axioms bridging connection and parthood, integrity (73a) and unity (73b) follow from reflexivity, symmetry and monotonicity (73c) (IsConnection.of_le, IsConnection.of_overlap). Overlap (71) carries the library's non-null clause, with which it agrees on carriers without a null individual (IsClassicalMereology.overlap_iff); on a carrier with one, the clause-free version holds of any two individuals and makes self-connection trivial. The maximality of (75) is mathlib's Maximal.

References

• [Sco14]
• [Chi98]
• [Rot09]
• [Gri12]

The three readings (§3.2, §3.3)

def Scontras2014.ofFilled {E : Type u_1} (filledWith : E → E → Prop) (k : E → Prop) (x : E) : Prop

The preposition of of a container reading (38b) denotes the property of being filled with an instance of the substance k.

Equations

• Scontras2014.ofFilled filledWith k x = ∃ (y : E), k y ∧ filledWith y x

def Scontras2014.containerReading {E : Type u_1} (P : E → Prop) (filledWith : E → E → Prop) (k : E → Prop) (x : E) : Prop

The container reading (38d) of a container noun P with substance k holds of a P filled with the substance, by intersective modification.

Equations

• Scontras2014.containerReading P filledWith k x = (P x ∧ Scontras2014.ofFilled filledWith k x)

def Scontras2014.measureReading {E : Type u_1} {D : Type} (μ : Degree.DimensionedMeasure E D) (k : E → Prop) (n : D) (x : E) : Prop

The measure reading ((41), (42)) of a measure term with measure μ, numeral n and substance k holds of the instances of the substance that measure n.

Equations

• Scontras2014.measureReading μ k n x = (k x ∧ μ.toFun x = n)

def Scontras2014.atomizingReading {E : Type u_1} (π : (E → Prop) → E → Prop) (k : E → Prop) (x : E) : Prop

The atomizing reading (77) of an atomizer with partitioning function π and substance k holds of what π returns for k.

Equations

• Scontras2014.atomizingReading π k x = π k x

def Scontras2014.atomizerReading {E : Type u_1} (props : E → Prop) (π : (E → Prop) → E → Prop) (k : E → Prop) (x : E) : Prop

An atomizer's selectional restriction ((79), (87)) adds the properties its units must have.

Equations

• Scontras2014.atomizerReading props π k x = (props x ∧ Scontras2014.atomizingReading π k x)

theorem Scontras2014.containerReading_subset {E : Type u_1} (P : E → Prop) (filledWith : E → E → Prop) (k : E → Prop) (x : E) : containerReading P filledWith k x → P x

A container reading refers to members of the quantizing noun's denotation (Table 3.1).

theorem Scontras2014.measureReading_subset {E : Type u_1} {D : Type} (μ : Degree.DimensionedMeasure E D) (k : E → Prop) (n : D) (x : E) : measureReading μ k n x → k x

A measure reading refers to instances of the substance (Table 3.1).

theorem Scontras2014.measureReading_quantity_uniform {E : Type u_1} {D : Type} (μ : Degree.DimensionedMeasure E D) (k : E → Prop) (n : D) : (μ.toFun '' {x : E | measureReading μ k n x}).Subsingleton

The measure reading with numeral n is quantity-uniform under the term's measure, since the measure takes the single value n on it.

Derived uses (§3.2.3)

def Scontras2014.shiftCM {E : Type u_1} (P : E → Prop) (filledWith : E → E → Prop) (card : E → ℕ) (k : E → Prop) (n : ℕ) (x : E) : Prop

The container-to-measure shift (47), on the model of -ful, measures the substance by the number of containers it fills.

Equations

• Scontras2014.shiftCM P filledWith card k n x = (k x ∧ ∃ (y : E), P y ∧ filledWith x y ∧ card y = n)

theorem Scontras2014.shiftCM_subset {E : Type u_1} (P : E → Prop) (filledWith : E → E → Prop) (card : E → ℕ) (k : E → Prop) (n : ℕ) (x : E) : shiftCM P filledWith card k n x → k x

A shifted container noun yields a measure reading, which refers to the substance.

def Scontras2014.shiftMC {E : Type u_1} {D : Type} [Preorder D] [One D] (μ : Degree.DimensionedMeasure E D) (filledWith : E → E → Prop) (x : E) : Prop

The measure-term-to-container shift (52) yields the objects filled with a unit quantity of some substance, which lexical reinterpretation narrows to a salient class of containers.

Equations

• Scontras2014.shiftMC μ filledWith x = ∃ (k : E → Prop) (y : E), Scontras2014.measureReading μ k 1 y ∧ filledWith y x

theorem Scontras2014.containerReading_shiftMC {E : Type u_1} {D : Type} [Preorder D] [One D] (μ : Degree.DimensionedMeasure E D) (filledWith : E → E → Prop) (k : E → Prop) (x : E) : containerReading (shiftMC μ filledWith) filledWith k x ↔ shiftMC μ filledWith x ∧ ∃ (y : E), k y ∧ filledWith y x

A shifted measure term with an of-phrase yields a container reading.

Partitions and relative atoms (§3.3.1)

def Scontras2014.IsMSCPartition {E : Type u_1} [PartialOrder E] (C : E → E → Prop) (k Q : E → Prop) : Prop

A partition of the kind k ((75), (76)) returns maximally self-connected instances of it, instances of k maximal among its self-connected instances.

Equations

• Scontras2014.IsMSCPartition C k Q = ∀ (y : E), Q y → Maximal (fun (x : E) => Mereology.SelfConnected C x ∧ k x) y

noncomputable def Scontras2014.pAtomMeasure {E : Type u_1} [PartialOrder E] (Q : E → Prop) (y : E) : ℕ

The relative-atom measure of Q (68) counts the Q-atoms, members of Q with no member of Q as a proper part, that are parts of y.

Equations

• Scontras2014.pAtomMeasure Q y = {x : E | Q x ∧ x ≤ y ∧ ¬∃ (z : E), Q z ∧ z < x}.ncard

theorem Scontras2014.isAntichain_of_isMSCPartition {E : Type u_1} [PartialOrder E] {C : E → E → Prop} {k Q : E → Prop} (h : IsMSCPartition C k Q) : IsAntichain (fun (x1 x2 : E) => x1 ≤ x2) {x : E | Q x}

The members of a maximally self-connected partition form an antichain, so one cannot be a proper part of another.

theorem Scontras2014.isAntichain_of_disjointPred {E : Type u_1} [PartialOrder E] [NoBotOrder E] {Q : E → Prop} (h : Mereology.DisjointPred Mereology.Overlap {x : E | Q x}) : IsAntichain (fun (x1 x2 : E) => x1 ≤ x2) {x : E | Q x}

The members of a non-overlapping partition (66) form an antichain.

theorem Scontras2014.atoms_eq_singleton {E : Type u_1} [PartialOrder E] {Q : E → Prop} (h : IsAntichain (fun (x1 x2 : E) => x1 ≤ x2) {x : E | Q x}) {y : E} (hy : Q y) : {x : E | Q x ∧ x ≤ y ∧ ¬∃ (z : E), Q z ∧ z < x} = {y}

In an antichain every member is its only atom below itself.

theorem Scontras2014.pAtomMeasure_eq_one {E : Type u_1} [PartialOrder E] {Q : E → Prop} (h : IsAntichain (fun (x1 x2 : E) => x1 ≤ x2) {x : E | Q x}) {y : E} (hy : Q y) : pAtomMeasure Q y = 1

Each member of a partition measures one relative atom, so cardinal numerals count them.

theorem Scontras2014.atomizingReading_subset {E : Type u_1} [PartialOrder E] {C : E → E → Prop} {π : (E → Prop) → E → Prop} {k : E → Prop} (hπ : IsMSCPartition C k (π k)) (x : E) : atomizingReading π k x → k x

By (77) with (76), the atomizing reading refers to maximally self-connected instances of the substance, hence to the substance.