Kennedy (2007): Vagueness and Grammar

Kennedy separates relative gradable adjectives (tall, long), whose positive form compares with a contextual standard, from absolute ones, whose standard is an endpoint of the scale: the minimum (wet, bent) or the maximum (full, dry). The positive form is ⟦pos⟧ = λg λx. g(x) ≥ s(g) (27), with the standard s fixed by the scale rather than by a comparison class, and Interpretive Economy (66) derives it from the scale structure. This file states the three positive forms and checks the diagnostics of Section 3.2 that separate them.

Main results

• exists_relativePos_of_lt, maxStandardPos_and_not_iff: definite descriptions, (53)–(54).
• not_maxStandardPos_of_lt_top, not_minStandardPos_iff: the Sorites second premise, (57)–(58).
• isCompl_minStandardPos_maxStandardPos_dual: the denial of a minimum-standard adjective asserts its maximum-standard antonym, (47).
• minStandardPos_of_comparative, not_maxStandardPos_of_comparative, relativePos_undetermined_of_comparative: comparatives, (49)–(51).
• table61_iff_licenses: maximizers and minimizers follow the endpoints of the scale, (61).
• closed_admits_both_endpoints: a totally closed scale admits both endpoint standards, (67)–(68).

References

• [Ken07b]
• [KMcN05]
• [RW04b]

The positive form (§2.3, §3.1)

def Kennedy2007.MinStandardPos {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [OrderBot D] (μ : Entity → D) (x : Entity) : Prop

A minimum-standard adjective (wet) holds of x when its degree is above the scale minimum.

Equations

• Kennedy2007.MinStandardPos μ x = (⊥ < μ x)

def Kennedy2007.MaxStandardPos {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [OrderTop D] (μ : Entity → D) (x : Entity) : Prop

A maximum-standard adjective (dry) holds of x when its degree is the scale maximum.

Equations

• Kennedy2007.MaxStandardPos μ x = (μ x = ⊤)

def Kennedy2007.RelativePos {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (θ : D) (x : Entity) : Prop

A relative adjective (long) holds of x when its degree exceeds a contextual threshold.

Equations

• Kennedy2007.RelativePos μ θ x = (θ < μ x)

Definite descriptions (§3.2, (53)–(54))

theorem Kennedy2007.exists_relativePos_of_lt {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) {a b : Entity} (h : μ b < μ a) : ∃ (θ : D), RelativePos μ θ a ∧ ¬RelativePos μ θ b

The long one succeeds because two objects of different length can always be told apart by a contextual standard.

theorem Kennedy2007.maxStandardPos_and_not_iff {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [OrderTop D] (μ : Entity → D) (a b : Entity) : MaxStandardPos μ a ∧ ¬MaxStandardPos μ b ↔ μ a = ⊤ ∧ μ b ≠ ⊤

In the full one (54), a maximum-standard adjective tells two objects apart only when one is at the maximum and the other is not, so two partially full jars leave nothing to pick out.

The Sorites second premise (§3.2, (57)–(58))

theorem Kennedy2007.not_maxStandardPos_of_lt_top {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [OrderTop D] {μ : Entity → D} {x : Entity} (h : μ x < ⊤) : ¬MaxStandardPos μ x

A theater with one fewer occupied seat than a full one is not full (57), since any degree below the maximum fails a maximum standard.

theorem Kennedy2007.not_minStandardPos_iff {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [OrderBot D] (μ : Entity → D) (x : Entity) : ¬MinStandardPos μ x ↔ μ x = ⊥

A rod with no bend is not bent (58), since exactly the minimum fails a minimum standard.

theorem Kennedy2007.isCompl_minStandardPos_maxStandardPos_dual {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [OrderBot D] (μ : Entity → D) : IsCompl {x : Entity | MinStandardPos μ x} {x : Entity | MaxStandardPos (⇑OrderDual.toDual ∘ μ) x}

The door is not open entails the door is closed (47). A minimum standard and the maximum standard of the antonym, which measures on the dual scale, split the domain between them, since the minimum of the one is the maximum of the other.

Comparatives (§3.2, (49)–(52))

theorem Kennedy2007.minStandardPos_of_comparative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [OrderBot D] {μ : Entity → D} {a b : Entity} (h : μ b < μ a) : MinStandardPos μ a

The floor is wetter than the countertop entails the floor is wet (49).

theorem Kennedy2007.not_maxStandardPos_of_comparative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [OrderTop D] {μ : Entity → D} {a b : Entity} (h : μ b < μ a) : ¬MaxStandardPos μ b

The floor is drier than the countertop entails the countertop is not dry (50).

theorem Kennedy2007.relativePos_undetermined_of_comparative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) {a b : Entity} (h : μ b < μ a) : (∃ (θ : D), RelativePos μ θ a) ∧ ∃ (θ : D), ¬RelativePos μ θ a

Rod A is longer than rod B entails neither that A is long nor that it is not (51).

Degree modifiers (§3.2, (61))

inductive Kennedy2007.DegreeModifier : Type

A degree modifier is a maximizer (completely, fully) or a minimizer (slightly, partially).

• maximizer : DegreeModifier
• minimizer : DegreeModifier

@[instance_reducible]

instance Kennedy2007.instDecidableEqDegreeModifier : DecidableEq DegreeModifier

Equations

• Kennedy2007.instDecidableEqDegreeModifier x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kennedy2007.Licenses : DegreeModifier → Degree.Boundedness → Prop

A modifier is licensed on a scale that has the endpoint it picks out.

Equations

• Kennedy2007.Licenses Kennedy2007.DegreeModifier.maximizer x✝ = x✝.HasMax
• Kennedy2007.Licenses Kennedy2007.DegreeModifier.minimizer x✝ = x✝.HasMin

@[instance_reducible]

instance Kennedy2007.instDecidableLicenses (m : DegreeModifier) (b : Degree.Boundedness) : Decidable (Licenses m b)

Equations

• Kennedy2007.instDecidableLicenses Kennedy2007.DegreeModifier.maximizer x✝ = Kennedy2007.instDecidableLicenses._aux_1 x✝
• Kennedy2007.instDecidableLicenses Kennedy2007.DegreeModifier.minimizer x✝ = Kennedy2007.instDecidableLicenses._aux_3 x✝

def Kennedy2007.table61Pos : Degree.Boundedness → DegreeModifier → Bool

The A_pos row of table (61) says whether a maximizer or minimizer is acceptable with the positive member of an antonym pair, by the pair's scale type.

Equations

• Kennedy2007.table61Pos Degree.Boundedness.open_ x✝ = false
• Kennedy2007.table61Pos Degree.Boundedness.lowerClosed Kennedy2007.DegreeModifier.maximizer = false
• Kennedy2007.table61Pos Degree.Boundedness.lowerClosed Kennedy2007.DegreeModifier.minimizer = true
• Kennedy2007.table61Pos Degree.Boundedness.upperClosed Kennedy2007.DegreeModifier.maximizer = true
• Kennedy2007.table61Pos Degree.Boundedness.upperClosed Kennedy2007.DegreeModifier.minimizer = false
• Kennedy2007.table61Pos Degree.Boundedness.closed x✝ = true

def Kennedy2007.table61Neg : Degree.Boundedness → DegreeModifier → Bool

The A_neg row of table (61) says the same for the negative member.

Equations

• Kennedy2007.table61Neg Degree.Boundedness.open_ x✝ = false
• Kennedy2007.table61Neg Degree.Boundedness.lowerClosed Kennedy2007.DegreeModifier.maximizer = true
• Kennedy2007.table61Neg Degree.Boundedness.lowerClosed Kennedy2007.DegreeModifier.minimizer = false
• Kennedy2007.table61Neg Degree.Boundedness.upperClosed Kennedy2007.DegreeModifier.maximizer = false
• Kennedy2007.table61Neg Degree.Boundedness.upperClosed Kennedy2007.DegreeModifier.minimizer = true
• Kennedy2007.table61Neg Degree.Boundedness.closed x✝ = true

def Kennedy2007.table61 (p : Polarity) (b : Degree.Boundedness) (m : DegreeModifier) : Bool

table61 is table (61) as printed, indexed by the member of the pair.

Equations

• Kennedy2007.table61 p b m = if p = Polarity.positive then Kennedy2007.table61Pos b m else Kennedy2007.table61Neg b m

theorem Kennedy2007.table61_iff_licenses (p : Polarity) (b : Degree.Boundedness) (m : DegreeModifier) : table61 p b m = true ↔ Licenses m (p • b)

Every cell of (61) is the endpoint structure of the adjective's own scale.

theorem Kennedy2007.fragment_pairs_table61 : Licenses DegreeModifier.maximizer English.Adjectives.full.boundedness ∧ Licenses DegreeModifier.maximizer English.Adjectives.empty.boundedness ∧ Licenses DegreeModifier.minimizer English.Adjectives.wet.boundedness ∧ ¬Licenses DegreeModifier.maximizer English.Adjectives.wet.boundedness ∧ Licenses DegreeModifier.maximizer English.Adjectives.dry.boundedness ∧ ¬Licenses DegreeModifier.minimizer English.Adjectives.dry.boundedness ∧ Licenses DegreeModifier.minimizer English.Adjectives.bent.boundedness ∧ ¬Licenses DegreeModifier.maximizer English.Adjectives.bent.boundedness ∧ Licenses DegreeModifier.maximizer English.Adjectives.straight.boundedness ∧ ¬Licenses DegreeModifier.maximizer English.Adjectives.tall.boundedness ∧ ¬Licenses DegreeModifier.minimizer English.Adjectives.short.boundedness

The Fragment's antonym pairs fill table (61) with completely full/empty, slightly wet but ??completely wet, completely dry but ??slightly dry, slightly bent but ??fully bent, fully straight, and nothing on the open height scale.

Interpretive Economy (§4.2–§4.3)

theorem Kennedy2007.open_requires_comparison_class : Degree.Boundedness.open_.IsRelative

An open scale offers no endpoint, so its standard is contextual and the adjective needs a comparison class.

theorem Kennedy2007.closed_admits_both_endpoints : Degree.Boundedness.closed.Admits Degree.PositiveStandard.minEndpoint ∧ Degree.Boundedness.closed.Admits Degree.PositiveStandard.maxEndpoint

A totally closed scale is interpretively variable, admitting both endpoint standards ((67)–(68), opaque/transparent, open/exposed); the maximum is only the default.