Degree Semantics Hierarchy #
@cite{klein-1980} @cite{kennedy-2007} @cite{scontras-2014} @cite{bale-schwarz-2022}
Three frameworks for gradable predicate semantics form a strict subsumption hierarchy:
Klein (Delineation) — most general
↑ measureDelineation
Kennedy (Degree) — specialization: single linear scale
↑ MeasureFn.toHasDegree
Scontras / Bale & Schwarz (Measurement) — specialization: typed dimension
Each arrow is an embedding: the lower framework's predictions are a special case of the higher framework's. The hierarchy is strict: delineation can express nonlinear adjectives ("clever") that no degree function can induce.
What each framework adds #
| Framework | Ontology | Comparative | Unique capacity |
|---|---|---|---|
| Klein | No degrees | ∃C. A(x,C) ∧ ¬A(y,C) | Nonlinear adjectives |
| Kennedy | Degrees (D,≤) | μ(x) > μ(y) | Measure phrases, DegP |
| Measurement | Degrees + dim | μ_d(x) > μ_d(y) | Typed dimensions, CARD |
Theorems in this file #
- measure_to_degree: every
MeasureFninduces aHasDegreeinstance - degree_to_delineation: every degree function induces a Klein delineation
- ordering_faithful: the induced delineation's ordering = degree comparison
- degree_delineations_are_linear: all degree-induced delineations are linear
- nonlinear_delineation_exists: a concrete nonlinear delineation witness
- monotone_excludes_nonlinear: monotone delineations are never nonlinear
- delineation_strictly_more_general: delineation ⊋ degree (strict containment)
- nlDel_not_degree_representable: no degree function can induce the nonlinear witness
- nondistinct_iff_equal_measure: Klein's emergent degrees = actual degree equality
- degree_delineation_strict_weak_order: degree orderings are strict weak orders
- very_degree_chain: Klein's
very= two-step degree chain
A MeasureFn E carries a typed dimension (mass, volume, cardinality, ...)
and a non-negative measure apply : E → ℚ. Forgetting the dimension and
non-negativity constraint yields a HasDegree E instance: the degree of
an entity is its measure value.
This is @cite{scontras-2014}'s key insight: measure terms (kilo, liter)
and CARD are all instances of the same degree-assigning operation.
Every measure function induces a degree assignment.
This is MeasureFn.toHasDegree — restated here for the hierarchy.
Equations
Instances For
Any degree function μ : E → D over a linear order induces a Klein
delineation via measureDelineation: entity x is "A-in-C" iff x
strictly exceeds some member of C on μ. This is the embedding from
@cite{kennedy-2007}'s degree semantics into @cite{klein-1980}'s
delineation framework.
The embedding is **faithful**: Klein's ordering under the induced
delineation exactly matches degree comparison (`ordering_iff_degree`).
No information is lost in the translation.
Every degree function induces a Klein delineation.
Equations
Instances For
The full chain: measure function → delineation (composing the two steps).
Equations
Instances For
The degree→delineation embedding is faithful: Klein's ordering under the induced delineation exactly matches degree comparison. This justifies Klein's claim (§4.2) that degrees are dispensable — and simultaneously justifies Kennedy's claim that degree semantics loses nothing over delineation for linear adjectives.
Every degree-induced delineation is monotone.
Every degree-induced delineation is linear: for any two entities in a comparison class, either one ranks above the other or they are nondistinct (equal degree).
Klein's delineation framework is STRICTLY more general than degree semantics. The key witness: nonlinear adjectives like "clever" produce cyclic orderings (both a > b and b > a for different comparison classes). This is impossible for any degree-induced delineation, since degree orderings are asymmetric.
See `Phenomena/Gradability/Studies/Klein1980.lean` for the empirical
motivation and the concrete "clever" witness. Here we prove the
theoretical separation at the framework level.
Monotone delineations cannot be nonlinear: monotonicity forces asymmetry, which excludes cycles. This is the core constraint that degree semantics imposes — and that Klein's framework relaxes.
The strict separation theorem: Klein's delineation framework is strictly more general than degree-based frameworks.
Forward: every degree function induces a monotone delineation (§ 2–3 above).
Backward FAILS: there exist delineations (nonlinear ones) that no degree function can induce, because degree-induced delineations are always monotone, and monotonicity excludes nonlinearity.
This is the formal content of Klein's critique of degree semantics: multi-criteria adjectives like "clever" require the richer delineation framework.
The degree-based frameworks correspond EXACTLY to the monotone fragment of Klein's delineation theory. This is not a coincidence: monotonicity is what ensures a delineation induces a well-behaved ordering (strict weak order), which is exactly what a degree scale provides.
- Forward: degree → monotone delineation (§ 2, `degree_delineation_monotone`)
- Backward: monotone delineation → degree-recoverable (@cite{klein-1980} §4.2,
proved in `Klein1980.lean` as `kleinDegree_measureDelineation`)
Together: `degree semantics = monotone delineation semantics`.
Klein's full framework adds the non-monotone fragment for
multi-criteria adjectives.
Degree functions always yield monotone delineations AND the ordering is faithful. This characterizes exactly what degree semantics buys you within the delineation framework.
The relationship between measurement semantics (@cite{scontras-2014}, @cite{bale-schwarz-2022}) and degree semantics (@cite{kennedy-2007}) is simple: measurement adds typed dimensions to degree functions.
A `MeasureFn E` is a degree function `apply : E → ℚ` PLUS a
`dimension : Dimension` label. The degree function is recoverable
via `MeasureFn.toHasDegree`, but the dimension label is lost.
What dimension typing buys you:
- Multiple measure functions per entity (weight AND volume AND count)
- The No Division Hypothesis: compositional operations respect dimension types
- Measure term semantics: ⟦kilo⟧ = λn.λx. μ_kg(x) = n, typed to mass
What it does NOT buy you: any new ordering structure. Measurement
adjectives are still degree adjectives under the hood.
Measurement semantics is a refinement of degree semantics: every measure function has an underlying degree function.
Measurement additionally provides non-negativity, which degree semantics does not require.
The full chain from measurement to delineation preserves ordering faithfully.
The strict separation theorem (§ 4) shows that nonlinear delineations
exist. This section strengthens the result: the specific nonlinear
witness nlDel is NOT representable by ANY degree function. This is
the definitive impossibility result: no choice of degree type or
measure function can produce the extension pattern of a multi-criteria
adjective like "clever."
The proof is by contradiction: if `nlDel` agreed extensionally with
some `measureDelineation μ`, then monotonicity of `measureDelineation μ`
would transfer to `nlDel`, contradicting its nonlinearity.
The nonlinear witness nlDel cannot be represented by any degree
function over any linearly ordered degree type. No matter what
degrees you assign to j and m, you cannot reproduce the extension
pattern where j is "clever" in {j} and m is "clever" in {m}.
This is the strongest form of the separation: not just "some delineations are nonlinear" but "this specific delineation is provably outside the degree-representable fragment."
@cite{klein-1980} §4.2 defines degrees as equivalence classes under
nondistinctness: degree(u) = {u' : u ≈ u'}. For measure-induced
delineations, this collapses to measure equality: two entities are
nondistinct iff they have the same degree.
This theorem bridges Klein's degree-free framework with Kennedy's
degree-based framework at the level of equivalence classes: Klein's
emergent "degrees" ARE Kennedy's degrees, when the delineation
happens to be measure-induced.
Nondistinctness under a measure-induced delineation = equal measure. This is Klein's §4.2 insight formalized: degrees are dispensable because they are recoverable as nondistinctness classes.
Forward: if μ(a) = μ(b), then no comparison class can distinguish them. Backward: if μ(a) ≠ μ(b), the two-element class {a,b} distinguishes them.
Under a degree-induced delineation, Klein's ordering is a strict weak order: asymmetric and negatively transitive. These two properties fully characterize the ordering structure of linear adjectives and justify the dispensability of degrees.
Asymmetry requires monotonicity (which degree delineations have).
Negative transitivity holds unconditionally. Together they give
transitivity and almost-connectedness as corollaries.
The ordering under a degree delineation is a strict weak order.
Transitivity of degree-induced ordering (corollary of strict weak order).
Klein's very (§4.1, eq 42) narrows the comparison class to the
positive extension. Under a degree-induced delineation, this
corresponds to raising the effective degree threshold: being "very
tall" requires exceeding someone who is themselves tall — a
transitive chain of strict degree comparisons.
Formally: `veryDelineation (measureDelineation μ) C x` iff there
exist y, z such that z ∈ C, μ(z) < μ(y), and μ(y) < μ(x). The
"very" threshold is the minimum degree among entities in C that
themselves exceed some C-member.
Very under a degree delineation requires a two-step chain: x exceeds y, which itself exceeds some member z of C.
Very entails the base predicate for degree delineations: if x exceeds someone who exceeds a C-member, then x exceeds a C-member (by transitivity of <).
Very is strictly stronger than the base: there exist entities that are "tall" but not "very tall." This is the "fairly tall" zone — entities just above the basic threshold but below the very-threshold.