States-Based Gradable Adjective Semantics

[CSW24] [Wel15] [Ken07]

An alternative to Kennedy-style degree semantics (Theory.lean). Gradable adjectives denote properties of states (type ⟨v,t⟩), not measure functions. The positive form works via a background ordering on states and a contrast point that carves out the positive region — no covert pos morpheme is needed.

Key Idea

Each gradable predicate sits on an ordered domain of states (the background ordering). The predicate's contrast point divides the ordering into a positive region (states at or above the contrast point) and the rest. Different predicates on the same ordering have different contrast points: warm and hot share a temperature ordering but hot has a higher contrast point.

Comparative morphology (more) introduces a measure function on states, accessing the background ordering but discarding the contrast point. This explains why "A is more confident that p than that q" has the same truth conditions whether we use confident or certain — both share the confidence ordering (CSW observation (72)).

Architecture

StatesBasedEntry extends ComparativeScale (from Degree) with a contrast point. The background ordering is the ambient [Preorder S]. This is a competing theory to the standard threshold model in Theory.lean; the bridge theorem statesBased_iff_kennedy shows when they agree.

structure Semantics.Gradability.StatesBased.StatesBasedEntry (S : Type u_1) [Preorder S] : Type u_1

A states-based gradable predicate entry.

Each entry names a positive region on a background ordering of states. The contrastPoint determines the lower bound of the positive region: a state s is in the positive region iff contrastPoint ≤ s.

The background ordering comes from the ambient [Preorder S]. scale provides the boundedness classification (open, closed, etc.).

Example: tall and short share a ComparativeScale HeightState but have different contrast points. confident and certain share a confidence ordering but certain has a higher contrast point.

• scale : Core.Order.ComparativeScale S

  Boundedness classification of the background ordering

• contrastPoint : S

  The threshold state delimiting the positive region

def Semantics.Gradability.StatesBased.StatesBasedEntry.inPositiveRegion {S : Type u_1} [Preorder S] (entry : StatesBasedEntry S) (s : S) : Prop

A state is in the positive region iff it is at least as high as the contrast point in the background ordering (CSW eq. 28b).

This is the states-based counterpart to Kennedy's positiveMeaning: instead of d > θ (degree exceeds threshold), we have c ≤ s (state is at or above the contrast point in the preorder).

Equations

• entry.inPositiveRegion s = (entry.contrastPoint ≤ s)

def Semantics.Gradability.StatesBased.StatesBasedEntry.inLowerRegion {S : Type u_1} [Preorder S] (entry : StatesBasedEntry S) (s : S) : Prop

A state is in the lower region iff it is at or below the contrast point. The dual of inPositiveRegion, used for negative-polarity adjectives like short, cool, doubts (CSW §5.2 (63c)).

The same StatesBasedEntry shape hosts either region; whether a lexical entry is positive- or negative-polarity is determined by which membership predicate consumers invoke. Mathlib analogue: Mathlib.Order.UpperLower provides UpperSet and LowerSet as separate types over the same preorder.

Equations

• entry.inLowerRegion s = (s ≤ entry.contrastPoint)

theorem Semantics.Gradability.StatesBased.disjoint_regions {S : Type u_2} [Preorder S] (e_pos e_low : StatesBasedEntry S) (h_strict : ¬e_pos.contrastPoint ≤ e_low.contrastPoint) (s : S) : ¬(e_pos.inPositiveRegion s ∧ e_low.inLowerRegion s)

Two entries with strictly-ordered contrast points carve out disjoint upper/lower regions. If e_pos.contrastPoint > e_low.contrastPoint (encoded as ¬ e_pos.contrastPoint ≤ e_low.contrastPoint), no state is simultaneously above e_pos's point and below e_low's.

This is the substrate witness for negative-polarity-vs-positive- polarity exclusion (e.g., CSW (63a)/(63c): no holder simultaneously confident(p) and doubts(p)).

def Semantics.Gradability.StatesBased.areScaleMates {S : Type u_1} [Preorder S] (e₁ e₂ : StatesBasedEntry S) : Prop

Two entries are scale-mates iff they share a background ordering (same scale) but differ in their contrast points. Scale-mates form clusters like warm/hot, confident/certain, cool/cold. (CSW §3.3: different cut-off points for different adjectives.)

Equations

• Semantics.Gradability.StatesBased.areScaleMates e₁ e₂ = (e₁.scale = e₂.scale ∧ e₁.contrastPoint ≠ e₂.contrastPoint)

def Semantics.Gradability.StatesBased.asymEntails {S : Type u_1} [Preorder S] (e₁ e₂ : StatesBasedEntry S) : Prop

e₁ asymmetrically entails e₂ when e₁'s contrast point is at least as high as e₂'s. Every state in e₁'s positive region is also in e₂'s, but not vice versa.

Example: certain asymmetrically entails confident because certainty requires a higher level of confidence (CSW §5.2).

Equations

• Semantics.Gradability.StatesBased.asymEntails e₁ e₂ = (e₂.contrastPoint ≤ e₁.contrastPoint)

theorem Semantics.Gradability.StatesBased.asymEntails_positive_region {S : Type u_1} [Preorder S] (e₁ e₂ : StatesBasedEntry S) (h : asymEntails e₁ e₂) (s : S) : e₁.inPositiveRegion s → e₂.inPositiveRegion s

Asymmetric entailment implies positive-region inclusion: if e₁ asymmetrically entails e₂, then every state in e₁'s positive region is also in e₂'s positive region.

CSW (65): "Ann is certain that p" entails "Ann is confident that p".

@[reducible, inline]

abbrev Semantics.Gradability.StatesBased.admissibleMeasure {S : Type u_1} [Preorder S] {D : Type u_2} [Preorder D] (μ : S → D) : Prop

The monotonicity-preservation requirement on measure functions used in monotonicity-requiring constructions: μ is admissible for a background ordering iff s₁ ≺ s₂ entails μ(s₁) < μ(s₂). This is Mathlib's StrictMono.

Single-name canonical Prop for a multi-tradition convergence. This one Prop names the same condition that appears under different labels across the literature; linglib hosts it once here and lets every consumer credit its own source:

• [Sch02] [Sch06] — Monotonicity Constraint on the measure function in nominal pseudopartitives.
• [Kri89] — extensive measure functions on quantized objects.
• [Wel15] — μ admissibility for much-comparatives; Semantics/Measurement.lean::admissibleMeasure_of_mereoDim bridges to the bundled MereoDim typeclass.
• [CSW24] (eq. 21) — CSW use this exact formulation for confidence orderings.
• [Pas19b] (def 4) — μ_int monotonicity on the part-whole structure of mental states.
• [YZXW+25] — EpistemicThreshold.isProbabilistic is a strengthening of this (Monotone, not StrictMono).

The bundled-typeclass form is MereoDim in Semantics/Mereology.lean (with [PartialOrder] carriers); the unbundled-Prop form is here (with [Preorder], more permissive). Use MereoDim when typeclass inference is desired; use admissibleMeasure when the witness is passed explicitly.

Equations

• Semantics.Gradability.StatesBased.admissibleMeasure μ = StrictMono μ

def Semantics.Gradability.StatesBased.statesComparativeSem {S : Type u_1} {D : Type u_2} [Preorder D] (μ : S → D) (s_a s_b : S) : Prop

Comparative semantics on states (CSW (32)): "A is more G than B" iff the measure of A's state exceeds the measure of B's state.

The key CSW insight (§3.4): the comparative uses only the background ordering (via an admissible measure), not the contrast point. This is captured architecturally by the type signature — statesComparativeSem takes no StatesBasedEntry parameter, so the contrast point that distinguishes scale-mates (confident/certain, warm/hot) is invisible to the comparative. Scale-mate comparative equivalence (CSW (72)) holds by construction.

Equations

• Semantics.Gradability.StatesBased.statesComparativeSem μ s_a s_b = (μ s_b < μ s_a)

theorem Semantics.Gradability.StatesBased.statesComparativeSem_of_lt {S : Type u_1} [Preorder S] {D : Type u_2} [Preorder D] (μ : S → D) (h : admissibleMeasure μ) {s_a s_b : S} (hlt : s_b < s_a) : statesComparativeSem μ s_a s_b

An admissible measure makes the background ordering entail the comparative: if s_b ≺ s_a in the background ordering and μ is admissible (StrictMono, CSW (21)/(31)), then A is more G of s_a than s_b. This is the spine that ties the measure-comparative to the background ordering — over a Preorder only the forward direction holds (the reverse needs a linear order, which CSW's connectedness-agnostic ordering need not be).

The max-quantified comparative (CSW (46)/(47), Wellwood §2–3)

statesComparativeSem above is the unique-state collapse of the comparative (direct two-state measure comparison). CSW fn 25 explicitly reject this as the general picture: the faithful comparative compares a matrix state's measure against the maximum of the than-clause degree set. The full form is contrast-blind (no StatesBasedEntry argument), so scale-mate equivalence (CSW (72)) holds by construction.

def Semantics.Gradability.StatesBased.thanDegrees {S : Type u_1} {D : Type u_2} [Preorder D] (Pthan : S → Prop) (μ : S → D) : Set D

The than-clause degree set (CSW (46)): the degrees met by some Pthan-state.

Equations

• Semantics.Gradability.StatesBased.thanDegrees Pthan μ = {d : D | ∃ (s : S), Pthan s ∧ d ≤ μ s}

def Semantics.Gradability.StatesBased.statesComparative {S : Type u_1} {D : Type u_2} [Preorder D] (Pmatrix Pthan : S → Prop) (μ : S → D) : Prop

The max-quantified comparative (CSW (47)): some Pmatrix-state's measure strictly exceeds the maximum of the Pthan degree set.

Equations

• Semantics.Gradability.StatesBased.statesComparative Pmatrix Pthan μ = ∃ (δ : D), IsGreatest (Semantics.Gradability.StatesBased.thanDegrees Pthan μ) δ ∧ ∃ (s : S), Pmatrix s ∧ δ < μ s

theorem Semantics.Gradability.StatesBased.statesComparative_unique_reduces {S : Type u_1} {D : Type u_2} [Preorder D] (μ : S → D) (s_a s_b : S) : statesComparative (fun (x : S) => x = s_a) (fun (x : S) => x = s_b) μ ↔ statesComparativeSem μ s_a s_b

Under unique matrix and than states, the max-quantified comparative reduces to the direct comparison statesComparativeSem (= μ s_b < μ s_a) — the simplification CSW fn 25 set aside. So the collapse is a corollary of the faithful form, not the definition.

theorem Semantics.Gradability.StatesBased.statesBased_iff_kennedy {S : Type u_2} [LinearOrder S] {D : Type u_3} [LinearOrder D] (μ : S → D) (hMono : StrictMono μ) (contrastPt : S) (θ : D) (hBridge : μ contrastPt = θ) (s : S) : contrastPt ≤ s ↔ θ ≤ μ s

When a monotone measure maps the contrast point to a Kennedy threshold, the states-based positive form agrees with degree-based comparison.

CSW's framework and Kennedy's are equivalent over linearly ordered scales with measure functions: contrastPoint ≤ s ↔ θ ≤ μ(s).

Note: CSW use weak inequality ≿ for the positive form. The existing positiveMeaning in Theory.lean uses strict <. This theorem uses weak ≤ on both sides, matching CSW.