States-Based Gradable Adjective Semantics

@cite{cariani-santorio-wellwood-2024} @cite{wellwood-2015} @cite{kennedy-2007}

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 Core.Scale) 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.Lexical.Adjective.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.Scale.ComparativeScale S

  Boundedness classification of the background ordering

• contrastPoint : S

  The threshold state delimiting the positive region

def Semantics.Lexical.Adjective.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.Lexical.Adjective.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.Lexical.Adjective.StatesBased.areScaleMates e₁ e₂ = (e₁.scale = e₂.scale ∧ e₁.contrastPoint ≠ e₂.contrastPoint)

def Semantics.Lexical.Adjective.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.Lexical.Adjective.StatesBased.asymEntails e₁ e₂ = (e₂.contrastPoint ≤ e₁.contrastPoint)

theorem Semantics.Lexical.Adjective.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.Lexical.Adjective.StatesBased.admissibleMeasure {S : Type u_1} [Preorder S] {D : Type u_2} [Preorder D] (μ : S → D) : Prop

CSW's monotonicity constraint (eq. 21): a measure function μ is admissible for a background ordering iff it preserves strict order.

If s₁ ≺ s₂ in the background ordering, then μ(s₁) < μ(s₂). This is Mathlib's StrictMono.

Equations

• Semantics.Lexical.Adjective.StatesBased.admissibleMeasure μ = StrictMono μ

def Semantics.Lexical.Adjective.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 eq. 37): "A is more G than B" iff the measure of A's state exceeds the measure of B's state.

The key CSW insight: the comparative uses only the background ordering (via an admissible measure), not the contrast point. The positive region is irrelevant to comparative truth conditions.

Equations

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

theorem Semantics.Lexical.Adjective.StatesBased.comparative_ignores_contrastPoint {S : Type u_1} [Preorder S] {D : Type u_2} [Preorder D] (e₁ e₂ : StatesBasedEntry S) (_h : e₁.scale = e₂.scale) (μ : S → D) (s_a s_b : S) : statesComparativeSem μ s_a s_b ↔ statesComparativeSem μ s_a s_b

The comparative is independent of the contrast point: more accesses only the background ordering, discarding positive-region info (CSW §3.4).

For any two entries e₁, e₂ on the same scale, the comparative truth conditions are identical.

theorem Semantics.Lexical.Adjective.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.

theorem Semantics.Lexical.Adjective.StatesBased.comparative_scalemate_equiv {S : Type u_1} [Preorder S] {D : Type u_2} [Preorder D] (e₁ e₂ : StatesBasedEntry S) (_h : areScaleMates e₁ e₂) (μ : S → D) (s_a s_b : S) : statesComparativeSem μ s_a s_b ↔ statesComparativeSem μ s_a s_b

Scale-mates have identical comparative truth conditions (CSW (72)): "more confident that p than that q" ↔ "more certain that p than that q".

This follows trivially from the fact that comparative semantics depends only on the measure function and the states, not on the entry. The theorem's value is documentary — it makes explicit the CSW insight that the comparative is entry-independent.