Measurement Semantics

[BS26a] [Ken15] [Kri89] [Sco14] [Zab05]

Formal semantics of measurement: measure functions, the bridge to bare numerals via CARD, the quantity-uniform property, and the connection to existing degree-semantics infrastructure.

Theoretical Foundation

[Sco14]'s The Semantics of Measurement (Ch. 2) aligns measure terms (kilo, liter) with the Num-head CARD, treating both as instances of a single category M. The CARD primitive originates with [Zab05]; its relational shape (numerals as relations between numbers and individuals) follows [Kri89]. Scontras's contribution is the unification: CARD and kilo share the type signature of a measure term, and number marking on basic nouns (one boy vs. two boys) is the same operation as number marking on measure terms (one kilo vs. two kilos).

Measure Functions

A measure function μ maps individuals to non-negative rationals along a specific physical dimension:

μ : Entity → ℚ≥0

The dimension tag (mass, volume, distance, time, cardinality, ...) lives in Features/Dimension.lean; this module imports it and exposes MeasureFn, which carries the tag plus the underlying apply function.

Measure Terms

A measure term (gram, liter, mile) names a specific measure function. Its (intransitive) denotation in [Sco14], eq. (33):

⟦kilo⟧ = λn. λx. μ_kg(x) = n

This is a function from a numeral to a predicate — a modifier of type ⟨n, ⟨e,t⟩⟩. The Lean encoding is MeasureFn.applyNumeral.

CARD

Scontras (eqs. (23) / (36)) gives CARD the parallel form

⟦CARD⟧ = λP. λn. λx. P(x) ∧ μ_CARD(x) = n

so a bare numeral phrase composes with a kind-denoting noun via CARD, yielding a predicate restricted to individuals of the appropriate cardinality. The point of the alignment is that the same #-head machinery governs both one boy (via CARD + μ_CARD) and one kilo of apples (via μ_kg). Here we expose μ_CARD as a MeasureFn (cardMeasure); the CARD Num-head itself lives at the syntactic level.

Connection to Scale Infrastructure

The degree substrate works with plain measure functions μ : E → α into a linear order. This module adds:

• typed dimensions (what μ measures), via Features.Dimension.Dimension
• multiple measure functions per entity (a box has weight AND volume AND cardinality — MeasureFn is not a typeclass)
• the quantity-uniform property (Scontras's QU_μ, eq. (44) p. 43)

Connection to [BS26a]

Features/Dimension.lean provides the typed-dimension substrate (Dimension, QuotientDimension, DimensionType) used by Studies/BaleSchwarz2026.lean to formulate the No Division Hypothesis (eq. (5), p. 135): "Quantity division is not available as an operation for semantic composition." The hypothesis itself is stated and applied in the consuming Studies file, not here.

structure Semantics.Measurement.MeasureFn (E : Type u_1) : Type u_1

A measure function maps entities to non-negative rational magnitudes along a specific dimension.

[Sco14]: degrees are pairs ⟨μ, n⟩ where μ is the measure function and n is the numerical value. A measure function is individuated by its dimension: μ_kg measures mass, μ_L measures volume, μ_CARD counts.

We use ℚ rather than ℝ to match the library's exact-arithmetic convention for computational semantics.

• dimension : Features.Dimension.Dimension

  Which dimension this function measures.

• apply : E → ℚ

  The measure function itself: maps an entity to its magnitude.

• nonneg (e : E) : self.apply e ≥ 0

  Measure values are non-negative.

@[implicit_reducible]

instance Semantics.Measurement.instCoeFunMeasureFnForallRat {E : Type u_1} : CoeFun (MeasureFn E) fun (x : MeasureFn E) => E → ℚ

Apply a measure function to an entity.

Equations

• Semantics.Measurement.instCoeFunMeasureFnForallRat = { coe := fun (μ : Semantics.Measurement.MeasureFn E) => μ.apply }

def Semantics.Measurement.MeasureFn.applyNumeral {E : Type u_1} (μ : MeasureFn E) (n : ℚ) (x : E) : Prop

Apply a measure function to a numeral n, yielding a predicate over entities:

⟦kilo⟧(3) = λx. μ_kg(x) = 3

[Sco14]: measure terms are nouns that name specific measure functions. Their type is ⟨n, ⟨e,t⟩⟩ — they take a numeral and return a predicate. This is the exact (=) case of the shared comparison-over-a- measure primitive Core.Order.Comparison.over: ⟦kilo⟧(n) is Comparison.eq.over μ_kg n. Modified readings (> n, ≥ n, …) are the other Comparisons over the same μ.

Equations

• μ.applyNumeral n x = (x ∈ Core.Order.Comparison.eq.over μ.apply n)

@[simp]

theorem Semantics.Measurement.MeasureFn.applyNumeral_iff {E : Type u_1} (μ : MeasureFn E) (n : ℚ) (x : E) : μ.applyNumeral n x ↔ μ.apply x = n

applyNumeral is exact measure predication: μ(x) = n (definitionally, the .eq interval-membership).

@[implicit_reducible]

instance Semantics.Measurement.instDecidableApplyNumeral {E : Type u_1} (μ : MeasureFn E) (n : ℚ) (x : E) : Decidable (μ.applyNumeral n x)

Equations

• Semantics.Measurement.instDecidableApplyNumeral μ n x = Semantics.Measurement.instDecidableApplyNumeral._aux_1 μ n x

def Semantics.Measurement.cardMeasure (E : Type u_1) (cardFn : E → ℚ) (h : ∀ (e : E), cardFn e ≥ 0) : MeasureFn E

The cardinality measure: μ_CARD x = |x|.

The CARD Num-head originates with [Zab05]; its relational shape (numerals as relations between numbers and individuals) follows [Kri89]. [Sco14] (eqs. (23), (36)) gives CARD the form

⟦CARD⟧ = λP. λn. λx. P(x) ∧ μ_CARD(x) = n

aligning it with measure terms whose intransitive form (eq. (33)) is ⟦kilo⟧ = λn. λx. μ_kg(x) = n. This file exposes the underlying μ_CARD as a MeasureFn; the CARD Num-head itself (which composes with a kind) lives at the syntactic level.

Equations

• Semantics.Measurement.cardMeasure E cardFn h = { dimension := Features.Dimension.Dimension.cardinality, apply := cardFn, nonneg := h }

def Semantics.Measurement.IsQuantityUniform {E : Type u_1} (P : E → Prop) (μ : MeasureFn E) : Prop

A predicate P is quantity-uniform with respect to measure function μ ([Sco14], eq. (44), p. 43; restated as eq. (53), p. 48):

QU_μ(P) ↔ ∀ x y, P(x) ∧ P(y) → μ(x) = μ(y)

Every individual in P's denotation evaluates to the same μ-value. This is a uniformity condition on the predicate, NOT closure under sum (a different condition closer to Krifka's cumulativity). The MP one CARD boy is QU under μ_CARD because every member denotes a single boy; one kilo of apples is QU under μ_kg because every member weighs 1 kg.

The role in Scontras's account: ⟦SG⟧ checks that the modified predicate is QU under some relevant μ, with that μ supplying the "1-ness" presupposition of singular morphology (eq. (54), p. 48). Predicates fail QU when they are not measure-modified — e.g. bare boy is not QU under μ_CARD because two distinct boys can have different cardinalities (one vs. plural).

Equations

• Semantics.Measurement.IsQuantityUniform P μ = ∀ (x y : E), P x → P y → μ.apply x = μ.apply y

inductive Semantics.Measurement.QuantizingNounClass : Type

Classification of quantizing nouns (Scontras Ch. 3): nouns that turn substance terms into countable expressions.

[Sco14] identifies three classes via Rothstein-style diagnostics (Table 3.5, p. 89):

• Measure terms (kilo, liter): name a measure function directly; always license a MEASURE reading.
• Container nouns (glass, box): non-relational predicates with a CONTAINER reading by default but ambiguous toward MEASURE when the container's volume can serve as a measure unit.
• Atomizers (grain, drop, piece): relational, partitioning nouns (eqs. (77), (87)) that impose a partition into self-connected atoms via π; they are counted (by CARD over the partition), not measured.

• measureTerm : QuantizingNounClass
• containerNoun : QuantizingNounClass
• atomizer : QuantizingNounClass

def Semantics.Measurement.instReprQuantizingNounClass.repr : QuantizingNounClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Measurement.instReprQuantizingNounClass : Repr QuantizingNounClass

Equations

• Semantics.Measurement.instReprQuantizingNounClass = { reprPrec := Semantics.Measurement.instReprQuantizingNounClass.repr }

@[implicit_reducible]

instance Semantics.Measurement.instDecidableEqQuantizingNounClass : DecidableEq QuantizingNounClass

Equations

• Semantics.Measurement.instDecidableEqQuantizingNounClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Semantics.Measurement.ContainerReading : Type

Container nouns are ambiguous between two readings (Scontras Ch. 3 §3.2):

• CONTAINER: the noun denotes physical containers; "three glasses of water" refers to three individual glasses containing water.

• MEASURE: the noun functions as a measure term; "three glasses of water" refers to a quantity of water whose volume equals three glass-volumes.

• container : ContainerReading
• measure : ContainerReading

def Semantics.Measurement.instReprContainerReading.repr : ContainerReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Measurement.instReprContainerReading : Repr ContainerReading

Equations

• Semantics.Measurement.instReprContainerReading = { reprPrec := Semantics.Measurement.instReprContainerReading.repr }

@[implicit_reducible]

instance Semantics.Measurement.instDecidableEqContainerReading : DecidableEq ContainerReading

Equations

• Semantics.Measurement.instDecidableEqContainerReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Measurement.licensesMeasureReading : QuantizingNounClass → Option ContainerReading → Prop

Whether a class/reading combination licenses a MEASURE reading (Scontras Ch. 3, Table 3.5 p. 89).

Class	Reading	MEASURE?	Reason
measureTerm	(n/a)	true	Names a measure function directly
containerNoun	.measure	true	Container's volume = measure unit
containerNoun	.container/none	false	Individuated containers
atomizer	(n/a)	false	Atomizers resist MEASURE (Ch. 3.3)

The original framing of this table as a "QU prediction" was misleading. Atomizers fail to license a MEASURE reading because their semantics is inherently relational and partitioning (Scontras eqs. (77)/(87), pp. 89-90), not measure-naming — they don't supply a measure function; instead they take a substance noun and impose a partition into self-connected atoms. The resulting predicates, after partitioning by π, are then counted by CARD (Scontras p. 100: atomizers are nominal and get counted by CARD-formed cardinals just like basic nouns). What's predicted here is MEASURE licensing, not QU-status under all conceivable μ.

Equations

• Semantics.Measurement.licensesMeasureReading Semantics.Measurement.QuantizingNounClass.measureTerm x✝ = True
• Semantics.Measurement.licensesMeasureReading Semantics.Measurement.QuantizingNounClass.containerNoun (some Semantics.Measurement.ContainerReading.measure) = True
• Semantics.Measurement.licensesMeasureReading Semantics.Measurement.QuantizingNounClass.containerNoun (some Semantics.Measurement.ContainerReading.container) = False
• Semantics.Measurement.licensesMeasureReading Semantics.Measurement.QuantizingNounClass.containerNoun none = False
• Semantics.Measurement.licensesMeasureReading Semantics.Measurement.QuantizingNounClass.atomizer x✝ = False

@[implicit_reducible]

instance Semantics.Measurement.instDecidableLicensesMeasureReading (cls : QuantizingNounClass) (r : Option ContainerReading) : Decidable (licensesMeasureReading cls r)

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Measurement.instDecidableLicensesMeasureReading Semantics.Measurement.QuantizingNounClass.measureTerm x✝ = isTrue trivial
• Semantics.Measurement.instDecidableLicensesMeasureReading Semantics.Measurement.QuantizingNounClass.containerNoun (some Semantics.Measurement.ContainerReading.measure) = isTrue trivial
• Semantics.Measurement.instDecidableLicensesMeasureReading Semantics.Measurement.QuantizingNounClass.containerNoun none = isFalse Semantics.Measurement.instDecidableLicensesMeasureReading._proof_2
• Semantics.Measurement.instDecidableLicensesMeasureReading Semantics.Measurement.QuantizingNounClass.atomizer x✝ = isFalse ⋯

theorem Semantics.Measurement.measureTerm_always_licensesMeasure (r : Option ContainerReading) : licensesMeasureReading QuantizingNounClass.measureTerm r

Measure terms always license a MEASURE reading.

theorem Semantics.Measurement.atomizer_no_MEASURE_reading (r : Option ContainerReading) : ¬licensesMeasureReading QuantizingNounClass.atomizer r

Atomizers never license a MEASURE reading ([Sco14] Ch. 3 §3.3, Table 3.5 p. 89). They impose a partition into atoms (eq. (77)) and are counted by CARD, not measured.

theorem Semantics.Measurement.containerNoun_licensesMeasure_iff_measure (r : ContainerReading) : licensesMeasureReading QuantizingNounClass.containerNoun (some r) ↔ r = ContainerReading.measure

Container nouns license a MEASURE reading iff in MEASURE reading.

Formalization-internal observation

[Sco14]'s measure-term denotation gives exact meaning directly:

⟦kilo⟧(n)(x) = (μ_kg(x) = n)               -- eq. (33), p. 37

[Ken15]'s "de-Fregean" analysis gives bare numerals a two-sided meaning via max:

⟦three⟧ = λD. max{n | D(n)} = 3            -- eq. (29), p. 15

Kennedy explicitly rejects the lower-bound + exhaustification approach (p. 19-20: the de-Fregean meaning "can only be derived [from a lower-bound basis] through the addition of some meaning changing operation, such as exhaustification"). Kennedy's pragmatics for ignorance implicatures with modified numerals is neo-Gricean Quantity (Sauerland-style primary implicatures, eq. (43) p. 22), NOT Maximize Informativity.

The two proposals are independent — different empirical domains (measure terms vs. bare numerals) and different formal mechanisms. They nonetheless yield equivalent truth conditions for n μ-units of stuff whenever n is realized in the image of μ: under that point-realization condition, the max of the at-least-degree property at n equals the exact-measure predicate μ(x) = n. The theorems below state this equivalence as a formalization-internal observation; it is not stated in either source paper.

The key infrastructure is isMaxInf_atLeast_of_hit in Semantics/Entailment/Extremum.lean, which requires only point- realization (∃ e, μ(e) = n) rather than full surjectivity. Mass nouns realize every n ∈ ℚ≥0 (rice is uniformly divisible by hypothesis); count nouns realize only n ∈ ℕ.

theorem Semantics.Measurement.scontras_kennedy_dense {E : Type u_1} (μ : MeasureFn E) (n : ℚ) (x : E) (hHit : ∃ (e : E), μ.apply e = n) : Entailment.IsMaxInf (Core.Order.Comparison.ge.over μ.apply) n x ↔ μ.apply x = n

For a measure function μ on ℚ: when n is realized by some entity, the MIP applied to the at-least degree property at n yields μ(x) = n.

Formalization-internal observation — not stated by Scontras or Kennedy. Bridges Scontras's exact measure-term meaning with the max{n | ...} = n form of Kennedy's de-Fregean analysis.

theorem Semantics.Measurement.scontras_kennedy_card {E : Type u_1} (cardFn : E → ℕ) (n : ℕ) (x : E) (hHit : ∃ (e : E), cardFn e = n) : Entailment.IsMaxInf (Core.Order.Comparison.ge.over cardFn) n x ↔ cardFn x = n

For a cardinality function on ℕ: same point-realization equivalence. Formalization-internal observation — see the prose above.

MeasureFn is the concrete Scontras-flavored substrate (a function plus a typed dimension and a non-negativity proof). The abstract characterizations elsewhere in linglib — Krifka extensivity (Mereology.ExtMeasure), Wellwood admissibility (StrictMono / admissibleMeasure) — are properties that a MeasureFn may carry. The bridges below let consumers move between the concrete and abstract views without re-stipulation.

@[reducible, inline]

abbrev Semantics.Measurement.MeasureFn.IsExtensive {E : Type u_1} [SemilatticeSup E] (μ : MeasureFn E) : Prop

A MeasureFn is extensive in the [Kri98] sense (additive over non-overlapping entities, positive, strictly monotone over the part-whole order; the formalism traces to [Kri89]'s cumulative/quantized distinction). Definitionally Mereology.ExtMeasure E μ.apply; declared as abbrev so the underlying class instance elaborates through it without manual unfolding.

Equations

• μ.IsExtensive = Mereology.ExtMeasure E μ.apply

@[reducible, inline]

abbrev Semantics.Measurement.MeasureFn.IsAdmissible {E : Type u_1} [Preorder E] (μ : MeasureFn E) : Prop

A MeasureFn is admissible (in [Wel15]'s / [Sch06]'s Monotonicity Constraint sense) iff its underlying function is StrictMono on the part-whole order. Definitionally equal to Semantics.Gradability.StatesBased.admissibleMeasure μ.apply — both are StrictMono μ.apply — so consumers can prove the equivalence by Iff.rfl when both abbrevs are in scope.

Equations

• μ.IsAdmissible = StrictMono μ.apply

theorem Semantics.Measurement.extensive_measureFn_qmod_qua {E : Type u_1} [inst : SemilatticeSup E] {μ : MeasureFn E} (hExt : μ.IsExtensive) {R : E → Prop} {n : ℚ} (_hn : 0 < n) : Mereology.QUA (Mereology.QMOD R μ.apply n)

Scontras-Krifka bridge. When a MeasureFn is extensive, applying [Kri89]'s QMOD with that measure function at any positive value produces a QUA predicate. Measure terms ("three kilos of rice") yield quantized predicates because their measure function is extensive.

theorem Semantics.Measurement.MeasureFn.applyNumeral_iff_qmod {E : Type u_1} (μ : MeasureFn E) (n : ℚ) (x : E) : μ.applyNumeral n x ↔ Mereology.QMOD (fun (x : E) => True) μ.apply n x

Bridge to QMOD. Scontras's applyNumeral and Krifka's QMOD check the same condition μ(x) = n when QMOD's restrictor is taken to be trivial.