Kennedy 2007: Interpretive Economy

Kennedy's classification of gradable adjectives by scale structure, and the derivation of standard type from scale boundedness [Ken07] [KMcN05] [RW04b]. Interpretive Economy ([Ken07] eq. (66)) maximises the contribution of conventional (scalar) meaning: when a scale has the relevant endpoint, the contextual/relative standard is ruled out in favour of the endpoint. A totally closed scale, however, has both endpoints, and Interpretive Economy is silent on the choice between them — such adjectives show interpretive variability (eq. (67)–(68), opaque/transparent, open/exposed); out of context the maximum is preferred on pragmatic grounds (a maximum standard entails a minimum one, and stronger meanings are favoured).

Main definitions

• ieAdmits : Boundedness → PositiveStandard → Prop — the standards Interpretive Economy admits for a scale; a totally closed scale admits both endpoint standards.
• interpretiveEconomy : Boundedness → PositiveStandard — the out-of-context default standard: the unique admitted standard where IE determines one, and the pragmatically preferred maximum for totally closed scales.
• IsClassA — relative (Class A) adjectives, those whose default standard requires a comparison class.

Main theorems

• ieAdmits_interpretiveEconomy — the default standard is always IE-admissible.
• ieAdmits_closed_minEndpoint, ieAdmits_closed_maxEndpoint — interpretive variability of totally closed scales: IE admits both endpoints.
• not_ieAdmits_contextual_of_isLicensed — IE rules out the relative standard whenever the scale has an endpoint.

def Degree.ieAdmits : Core.Order.Boundedness → PositiveStandard → Prop

The positive-form standards that Interpretive Economy admits for a scale. IE maximises the contribution of conventional (scalar) meaning, so the contextual/relative standard is admitted only on a totally open scale (which has no endpoint to use). A one-sided closed scale admits its single endpoint; a totally closed scale admits both endpoint standards — IE rules out the relative reading but is silent on the min/max choice ([Ken07] eq. (66), the opaque/transparent and open/exposed cases of eq. (67)–(68)).

Equations

• Degree.ieAdmits Core.Order.Boundedness.open_ x✝ = (x✝ = Degree.PositiveStandard.contextual)
• Degree.ieAdmits Core.Order.Boundedness.lowerBounded x✝ = (x✝ = Degree.PositiveStandard.minEndpoint)
• Degree.ieAdmits Core.Order.Boundedness.upperBounded x✝ = (x✝ = Degree.PositiveStandard.maxEndpoint)
• Degree.ieAdmits Core.Order.Boundedness.closed x✝ = (x✝ = Degree.PositiveStandard.minEndpoint ∨ x✝ = Degree.PositiveStandard.maxEndpoint)

@[implicit_reducible]

instance Degree.instDecidableIeAdmits (b : Core.Order.Boundedness) (s : PositiveStandard) : Decidable (ieAdmits b s)

Equations

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

def Degree.interpretiveEconomy : Core.Order.Boundedness → PositiveStandard

The out-of-context default positive standard. Where Interpretive Economy admits a unique standard (open / one-sided closed scales) this is forced; for a totally closed scale IE admits both endpoints (ieAdmits) and the default is the maximum on pragmatic grounds — a maximum standard entails a minimum one and stronger meanings are preferred ([Ken07] eq. (66) discussion). So this is Interpretive Economy plus a strengthening default for closed scales, not IE alone; the genuine (variable) IE claim is ieAdmits.

Equations

• Degree.interpretiveEconomy Core.Order.Boundedness.open_ = Degree.PositiveStandard.contextual
• Degree.interpretiveEconomy Core.Order.Boundedness.lowerBounded = Degree.PositiveStandard.minEndpoint
• Degree.interpretiveEconomy Core.Order.Boundedness.upperBounded = Degree.PositiveStandard.maxEndpoint
• Degree.interpretiveEconomy Core.Order.Boundedness.closed = Degree.PositiveStandard.maxEndpoint

theorem Degree.interpretiveEconomy_open : interpretiveEconomy Core.Order.Boundedness.open_ = PositiveStandard.contextual

theorem Degree.interpretiveEconomy_lowerBounded : interpretiveEconomy Core.Order.Boundedness.lowerBounded = PositiveStandard.minEndpoint

theorem Degree.interpretiveEconomy_upperBounded : interpretiveEconomy Core.Order.Boundedness.upperBounded = PositiveStandard.maxEndpoint

theorem Degree.interpretiveEconomy_closed : interpretiveEconomy Core.Order.Boundedness.closed = PositiveStandard.maxEndpoint

The default standard for a totally closed scale is the maximum — a pragmatic preference (stronger meaning), not an Interpretive-Economy determination; the minimum is equally admitted (ieAdmits_closed_minEndpoint).

theorem Degree.ieAdmits_interpretiveEconomy (b : Core.Order.Boundedness) : ieAdmits b (interpretiveEconomy b)

The default standard is always among those Interpretive Economy admits.

theorem Degree.ieAdmits_closed_minEndpoint : ieAdmits Core.Order.Boundedness.closed PositiveStandard.minEndpoint

Interpretive variability of totally closed scales: IE admits the minimum standard, so the interpretiveEconomy maximum default is a pragmatic preference, not a semantic determination ([Ken07] eq. (67)–(68): opaque/transparent, open/exposed).

theorem Degree.ieAdmits_closed_maxEndpoint : ieAdmits Core.Order.Boundedness.closed PositiveStandard.maxEndpoint

A totally closed scale also admits the maximum standard.

theorem Degree.not_ieAdmits_contextual_of_isLicensed {b : Core.Order.Boundedness} (h : b.IsLicensed) : ¬ieAdmits b PositiveStandard.contextual

Interpretive Economy rules out the relative (contextual) standard whenever the scale has an endpoint (Boundedness.IsLicensed).

def Degree.IsClassA (b : Core.Order.Boundedness) : Prop

A boundedness is Class A (relative) iff its default standard requires a comparison class — i.e. iff the scale is open. Kennedy's tall, expensive, big.

Equations

• Degree.IsClassA b = (Degree.interpretiveEconomy b).RequiresComparisonClass

@[implicit_reducible]

instance Degree.instDecidablePredBoundednessIsClassA : DecidablePred IsClassA

Equations

• Degree.instDecidablePredBoundednessIsClassA b = Degree.instDecidablePredBoundednessIsClassA._aux_1 b