Klein (1980): A Semantics for Positive and Comparative Adjectives

Klein gives gradable adjectives a semantics without degrees. An adjective is a predicate whose extension is fixed relative to a comparison class, the comparative is derived from the positive by quantifying over comparison classes, and degrees, where they are wanted, are recovered as classes of entities no comparison class tells apart. The delineation vocabulary of Degree.Delineation supplies comparison classes, the induced ordering, monotonicity and the modifiers very and fairly; this file states the paper's claims about them. A nonlinear adjective such as clever switches criterion with the comparison class, so its ordering ranks two entities each above the other, which monotonicity forbids. Klein's as … as is Kamp's at least as over all completions.

Main statements

• clever_not_monotone: the delineation for clever is not monotone, so no measure induces it.
• isStrictWeakOrder_outranks: under monotonicity the ordering is a strict weak order.
• kleinDegree_ofMeasure: Klein's degrees agree with equality of measure.
• preorder_le_iff_kampPreorder_le: the equative is Kamp's at least as over all completions.

Implementation notes

• The measure-induced delineation, its monotonicity and its ordering-to-degree equivalence are substrate (Delineation.ofMeasure, Delineation.outranks_ofMeasure_iff); the study states what the paper adds on top of them.

References

• [Kle80]
• [Kam75]

Linear and nonlinear adjectives (§2.2, §3.3)

Tall is linear, a single criterion and a monotone delineation, while clever can produce cycles: which of two entities counts as clever depends on which criterion the comparison class makes salient.

inductive Klein1980.Clever2 : Type

Two entities, Jude and Mona.

• j : Clever2
• m : Clever2

def Klein1980.cleverDel : Degree.Delineation Clever2

This delineation for clever applies two conflicting criteria. Jude is clever when Mona is absent from the comparison class, Mona when Jude is, and neither when both are present.

Equations

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

theorem Klein1980.clever_nonlinear : cleverDel.IsNonlinear

The clever delineation is nonlinear, since in the class of both each is ordered above the other.

theorem Klein1980.clever_not_monotone : ¬cleverDel.IsMonotone

The clever delineation is not monotone, so no measure function induces it.

Very narrows the comparison class (eq. 42)

Very narrows the comparison class to the positive extension. The substrate's Delineation.very_subset needs Klein's domain restriction, that a delineation classifies only members of its class; measure-induced delineations lack it, yet very A entails A for them by transitivity of the measure order, while being tall does not make one very tall.

theorem Klein1980.very_ofMeasure_subset {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (C : Set E) : (Degree.Delineation.ofMeasure μ).very.toFun C ⊆ (Degree.Delineation.ofMeasure μ).toFun C

Under a measure-induced delineation very A entails A.

theorem Klein1980.exists_mem_not_mem_very : ∃ x ∈ (Degree.Delineation.ofMeasure id).toFun Set.univ, x ∉ (Degree.Delineation.ofMeasure id).very.toFun Set.univ

An entity tall relative to everyone need not be tall relative to the tall; such an entity is fairly tall.

Degrees recovered (§4.2, eq. 62)

Degrees are dispensable but recoverable: the degree of u in a comparison class is the class of entities nondistinct from u, so degrees emerge from comparison classes rather than being primitive.

def Klein1980.kleinDegree {E : Type u_1} (d : Degree.Delineation E) (C : Set E) (u : E) : Set E

Klein's degree of u at a comparison class is the set of entities nondistinct from u.

Equations

• Klein1980.kleinDegree d C u = {v : E | d.Nondistinct C u v}

theorem Klein1980.kleinDegree_ofMeasure {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) {C : Set E} {a b : E} (ha : a ∈ C) (hb : b ∈ C) : b ∈ kleinDegree (Degree.Delineation.ofMeasure μ) C a ↔ μ a = μ b

For measure-induced delineations, two entities share a Klein degree iff they share a measure value.

Non-triviality (§5)

def Klein1980.IsNontrivial {E : Type u_1} (d : Degree.Delineation E) : Prop

A delineation is non-trivial when every comparison class with at least two members contains a member in the extension and a member outside it.

Equations

• Klein1980.IsNontrivial d = ∀ (C : Set E), (∃ a ∈ C, ∃ b ∈ C, a ≠ b) → ∃ u ∈ C, ∃ v ∈ C, u ∈ d.toFun C ∧ v ∉ d.toFun C

The ordering is a strict weak order (§6)

Under monotonicity the context-relative ordering is irreflexive, transitive and has transitive incomparability, the ordering structure a degree scale would give without degrees in the ontology.

theorem Klein1980.isStrictWeakOrder_outranks {E : Type u_1} {d : Degree.Delineation E} (hmono : d.IsMonotone) (C : Set E) : IsStrictWeakOrder E (d.Outranks C)

Under monotonicity the ordering is a strict weak order.

theorem Klein1980.outranks_or_outranks_or_nondistinct {E : Type u_1} (d : Degree.Delineation E) (C : Set E) (u v : E) : d.Outranks C u v ∨ d.Outranks C v u ∨ d.Nondistinct C u v

Any two entities are ordered one way or the other or are nondistinct.

As … as and Kamp's at least as (§5.3)

Both quantify universally over ways of making the predicate precise, completions for Kamp and comparison classes for Klein, so over all completions the two preorders coincide.

theorem Klein1980.preorder_le_iff_kampPreorder_le {E : Type u_1} (d : Degree.Delineation E) (u v : E) : u ≤ v ↔ u ≤ v

Klein's preorder is Kamp's over all completions of the same extension function.